Skip to content

Commit

Permalink
[Civl] Fix primitives (#833)
Browse files Browse the repository at this point in the history 
This PR attempts to fix up the layer 0 primitives used in the Treiber
stack example so that they make more sense. There is considerable
improvement from before. One annoying thing still left is the presence
of ```assume``` statements in the definition of ```AtomicLoadNode#0```.
These ```assume``` statements are converted into ```assert``` statements
in the next layer up inside ```AtomicLoadNode```. But it would be better
to refactor the proof somehow to have the ```assert``` statements at the
lowest layer.

Co-authored-by: Shaz Qadeer <[email protected]>
  • Loading branch information
@shazqadeer
shazqadeer and Shaz Qadeer authored Jan 13, 2024
1 parent 8634eb3 commit 6ad1aff
Showing 1 changed file with 47 additions and 46 deletions.
93 changes: 47 additions & 46 deletions Test/civl/samples/treiber-stack.bpl
View file
Original file line number Diff line number Diff line change
Expand Up @@ -9,7 +9,7 @@ type X; // module type parameter
var {:layer 4, 5} Stack: Map (RefTreiber X) (Vec X);
var {:layer 0, 4} ts: Lheap (Treiber X);

atomic action {:layer 5} AtomicTreiberAlloc() returns (loc_t: Lval (Loc (Treiber X)))
atomic action {:layer 5} AtomicAlloc() returns (loc_t: Lval (Loc (Treiber X)))
modifies Stack;
{
var ref_t: RefTreiber X;
Expand All @@ -18,13 +18,22 @@ modifies Stack;
assume !Map_Contains(Stack, ref_t);
Stack := Map_Update(Stack, ref_t, Vec_Empty());
}
yield procedure {:layer 4} TreiberAlloc() returns (loc_t: Lval (Loc (Treiber X)))
refines AtomicTreiberAlloc;
preserves call DomYieldInv#4();
yield procedure {:layer 4} Alloc() returns (loc_t: Lval (Loc (Treiber X)))
refines AtomicAlloc;
preserves call YieldInvDom#4();
{
var top: Ref (Node X);
var stack: Lheap (Node X);
var treiber: Treiber X;
var lmap_t: Lheap (Treiber X);
var ref_t: RefTreiber X;
call loc_t := Alloc#0();
top := Nil();
call stack := Lmap_Empty();
treiber := Treiber(top, stack);
call loc_t, lmap_t := Lmap_Alloc(treiber);
call {:layer 4} Lmap_Assume(lmap_t, ts);
ref_t := Ref(loc_t->val);
call AllocTreiber(lmap_t, ref_t);
call {:layer 4} Stack := Copy(Map_Update(Stack, ref_t, Vec_Empty()));
call {:layer 4} AbsLemma(ts->val->val[ref_t]->top, ts->val->val[ref_t]->stack->val);
}
Expand All @@ -40,7 +49,7 @@ yield procedure {:layer 4} Push(ref_t: RefTreiber X, x: X) returns (success: boo
refines AtomicPush;
preserves call YieldInv#2(ref_t);
preserves call YieldInv#4(ref_t);
preserves call DomYieldInv#4();
preserves call YieldInvDom#4();
{
var {:layer 4} old_top: RefNode X;
var {:layer 4} old_stack: Map (RefNode X) (Node X);
Expand Down Expand Up @@ -71,7 +80,7 @@ refines AtomicPop;
preserves call YieldInv#2(ref_t);
preserves call YieldInv#3(ref_t);
preserves call YieldInv#4(ref_t);
preserves call DomYieldInv#4();
preserves call YieldInvDom#4();
{
call {:layer 4} AbsLemma(ts->val->val[ref_t]->top, ts->val->val[ref_t]->stack->val);
call success, x := PopIntermediate(ref_t);
Expand Down Expand Up @@ -142,7 +151,7 @@ preserves call YieldInv#2(ref_t);
new_ref_n := Ref(new_loc_n->val);
call success := WriteTopOfStack(ref_t, ref_n, new_ref_n);
if (success) {
call AllocInStack(ref_t, new_ref_n, lmap_n);
call AllocNode(ref_t, new_ref_n, lmap_n);
}
}

Expand All @@ -168,14 +177,6 @@ refines AtomicReadTopOfStack#Push;
call ref_n := ReadTopOfStack(ref_t);
}

atomic action {:layer 1, 2} AtomicReadTopOfStack(ref_t: RefTreiber X) returns (ref_n: RefNode X)
{
assert Map_Contains(ts->val, ref_t);
ref_n := ts->val->val[ref_t]->top;
}
yield procedure {:layer 0} ReadTopOfStack(ref_t: RefTreiber X) returns (ref_n: RefNode X);
refines AtomicReadTopOfStack;

right action {:layer 3} AtomicLoadNode(ref_t: RefTreiber X, ref_n: RefNode X) returns (node: Node X)
{
assert Map_Contains(ts->val, ref_t);
Expand All @@ -189,6 +190,27 @@ preserves call YieldInv#2(ref_t);
call node := LoadNode#0(ref_t, ref_n);
}

atomic action {:layer 3} AtomicWriteTopOfStack#Pop(ref_t: RefTreiber X, old_ref_n: RefNode X, new_ref_n: RefNode X) returns (r: bool)
modifies ts;
{
assert NilDomain(ts, ref_t)[new_ref_n];
call r := AtomicWriteTopOfStack(ref_t, old_ref_n, new_ref_n);
}
yield procedure {:layer 2} WriteTopOfStack#Pop(ref_t: RefTreiber X, old_ref_n: RefNode X, new_ref_n: RefNode X) returns (r: bool)
refines AtomicWriteTopOfStack#Pop;
preserves call YieldInv#2(ref_t);
{
call r := WriteTopOfStack(ref_t, old_ref_n, new_ref_n);
}

atomic action {:layer 1, 2} AtomicReadTopOfStack(ref_t: RefTreiber X) returns (ref_n: RefNode X)
{
assert Map_Contains(ts->val, ref_t);
ref_n := ts->val->val[ref_t]->top;
}
yield procedure {:layer 0} ReadTopOfStack(ref_t: RefTreiber X) returns (ref_n: RefNode X);
refines AtomicReadTopOfStack;

atomic action {:layer 1,2} AtomicLoadNode#0(ref_t: RefTreiber X, ref_n: RefNode X) returns (node: Node X)
{
assume Map_Contains(ts->val, ref_t);
Expand All @@ -198,29 +220,16 @@ atomic action {:layer 1,2} AtomicLoadNode#0(ref_t: RefTreiber X, ref_n: RefNode
yield procedure {:layer 0} LoadNode#0(ref_t: RefTreiber X, ref_n: RefNode X) returns (node: Node X);
refines AtomicLoadNode#0;

left action {:layer 1, 2} AtomicAllocInStack(ref_t: RefTreiber X, ref_n: RefNode X, {:linear_in} lmap_n: Lheap (Node X))
left action {:layer 1, 2} AtomicAllocNode(ref_t: RefTreiber X, ref_n: RefNode X, {:linear_in} lmap_n: Lheap (Node X))
modifies ts;
{
var lmap_n', lmap_n'': Lheap (Node X);
assert Map_Contains(ts->val, ref_t);
call lmap_n'', lmap_n' := Lmap_Move(lmap_n, ts->val->val[ref_t]->stack, ref_n);
ts->val->val[ref_t]->stack := lmap_n';
}
yield procedure {:layer 0} AllocInStack(ref_t: RefTreiber X, ref_n: RefNode X, {:linear_in} lmap_n: Lheap (Node X));
refines AtomicAllocInStack;

atomic action {:layer 3} AtomicWriteTopOfStack#Pop(ref_t: RefTreiber X, old_ref_n: RefNode X, new_ref_n: RefNode X) returns (r: bool)
modifies ts;
{
assert NilDomain(ts, ref_t)[new_ref_n];
call r := AtomicWriteTopOfStack(ref_t, old_ref_n, new_ref_n);
}
yield procedure {:layer 2} WriteTopOfStack#Pop(ref_t: RefTreiber X, old_ref_n: RefNode X, new_ref_n: RefNode X) returns (r: bool)
refines AtomicWriteTopOfStack#Pop;
preserves call YieldInv#2(ref_t);
{
call r := WriteTopOfStack(ref_t, old_ref_n, new_ref_n);
}
yield procedure {:layer 0} AllocNode(ref_t: RefTreiber X, ref_n: RefNode X, {:linear_in} lmap_n: Lheap (Node X));
refines AtomicAllocNode;

atomic action {:layer 1, 3} AtomicWriteTopOfStack(ref_t: RefTreiber X, old_ref_n: RefNode X, new_ref_n: RefNode X) returns (r: bool)
modifies ts;
Expand All @@ -239,22 +248,14 @@ modifies ts;
yield procedure {:layer 0} WriteTopOfStack(ref_t: RefTreiber X, old_ref_n: RefNode X, new_ref_n: RefNode X) returns (r: bool);
refines AtomicWriteTopOfStack;

atomic action {:layer 1, 4} AtomicAlloc#0() returns (loc_t: Lval (Loc (Treiber X)))
atomic action {:layer 1, 4} AtomicAllocTreiber({:linear_in} lmap_t: Lheap (Treiber X), ref_t: RefTreiber X)
modifies ts;
{
var top: Ref (Node X);
var stack: Lheap (Node X);
var treiber: Treiber X;
var lmap_t: Lheap (Treiber X);
top := Nil();
call stack := Lmap_Empty();
treiber := Treiber(top, stack);
call loc_t, lmap_t := Lmap_Alloc(treiber);
call Lmap_Assume(lmap_t, ts);
call lmap_t, ts := Lmap_Move(lmap_t, ts, Ref(loc_t->val));
var lmap_t': Lheap (Treiber X);
call lmap_t', ts := Lmap_Move(lmap_t, ts, ref_t);
}
yield procedure {:layer 0} Alloc#0() returns (loc_t: Lval (Loc (Treiber X)));
refines AtomicAlloc#0;
yield procedure {:layer 0} AllocTreiber({:linear_in} lmap_t: Lheap (Treiber X), ref_t: RefTreiber X);
refines AtomicAllocTreiber;

function {:inline} NilDomain(ts: Lheap (Treiber X), ref_t: RefTreiber X): [RefNode X]bool {
ts->val->val[ref_t]->stack->val->dom->val[Nil() := true]
Expand Down Expand Up @@ -322,5 +323,5 @@ invariant Map_At(Stack, ref_t) == (var t := ts->val->val[ref_t]; Abs(t->top, t->
invariant (var t := ts->val->val[ref_t]; Between(t->stack->val->val, t->top, t->top, Nil()));
invariant (var t := ts->val->val[ref_t]; IsSubset(BetweenSet(t->stack->val->val, t->top, Nil()), NilDomain(ts, ref_t)));

yield invariant {:layer 4} DomYieldInv#4();
yield invariant {:layer 4} YieldInvDom#4();
invariant Stack->dom == ts->val->dom;

0 comments on commit 6ad1aff

Please sign in to comment.