From c1912b6562b4eb2cc7a8123e212d6cedf81ec5bc Mon Sep 17 00:00:00 2001 From: Shaz Qadeer Date: Sat, 13 Jan 2024 04:14:57 -0800 Subject: [PATCH] update --- Test/civl/samples/treiber-stack.bpl | 93 +++++++++++++++-------------- 1 file changed, 47 insertions(+), 46 deletions(-) diff --git a/Test/civl/samples/treiber-stack.bpl b/Test/civl/samples/treiber-stack.bpl index 52410bab1..cd8d063ee 100644 --- a/Test/civl/samples/treiber-stack.bpl +++ b/Test/civl/samples/treiber-stack.bpl @@ -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; @@ -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); } @@ -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); @@ -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); @@ -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); } } @@ -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); @@ -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); @@ -198,7 +220,7 @@ 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); @@ -206,21 +228,8 @@ modifies ts; 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; @@ -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] @@ -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;