From aa88c55bdebce5d924235e7026943555d0756c21 Mon Sep 17 00:00:00 2001 From: Shaz Qadeer Date: Sat, 27 Jan 2024 20:40:44 -0800 Subject: [PATCH] [Civl] eliminate use of Lset (#844) --- Test/civl/regression-tests/linear-test.bpl | 9 -- .../regression-tests/linear-test.bpl.expect | 2 +- Test/civl/regression-tests/linear_types.bpl | 23 ----- .../regression-tests/linear_types_error.bpl | 49 ---------- .../linear_types_error.bpl.expect | 10 -- Test/civl/samples/alloc-mem.bpl | 92 ++++++++++--------- Test/civl/samples/alloc-mem.bpl.expect | 2 +- Test/civl/samples/bluetooth.bpl | 65 ++++++++----- Test/civl/samples/bluetooth.bpl.expect | 2 +- Test/civl/samples/civl-paper.bpl | 43 +++++---- Test/civl/samples/civl-paper.bpl.expect | 2 +- 11 files changed, 115 insertions(+), 184 deletions(-) delete mode 100644 Test/civl/regression-tests/linear_types.bpl delete mode 100644 Test/civl/regression-tests/linear_types_error.bpl delete mode 100644 Test/civl/regression-tests/linear_types_error.bpl.expect diff --git a/Test/civl/regression-tests/linear-test.bpl b/Test/civl/regression-tests/linear-test.bpl index 63170a0f9..37d4a7157 100644 --- a/Test/civl/regression-tests/linear-test.bpl +++ b/Test/civl/regression-tests/linear-test.bpl @@ -7,12 +7,3 @@ yield procedure {:layer 1} foo1({:linear "A"} x: int, {:linear "A"} y: int) { assert {:layer 1} x != y; } - -yield procedure {:layer 1} foo3({:layer 1} {:linear_in} x: Lset int, i: [int]bool) returns ({:layer 1} y: Lset int) -requires {:layer 1} IsSubset(i, x->dom); -{ - var {:layer 1} v: Lset int; - y := x; - call {:layer 1} v := Lset_Get(y, i); - assert {:layer 1} IsDisjoint(y->dom, i); -} \ No newline at end of file diff --git a/Test/civl/regression-tests/linear-test.bpl.expect b/Test/civl/regression-tests/linear-test.bpl.expect index 41374b000..37fad75c9 100644 --- a/Test/civl/regression-tests/linear-test.bpl.expect +++ b/Test/civl/regression-tests/linear-test.bpl.expect @@ -1,2 +1,2 @@ -Boogie program verifier finished with 2 verified, 0 errors +Boogie program verifier finished with 1 verified, 0 errors diff --git a/Test/civl/regression-tests/linear_types.bpl b/Test/civl/regression-tests/linear_types.bpl deleted file mode 100644 index ac148f18b..000000000 --- a/Test/civl/regression-tests/linear_types.bpl +++ /dev/null @@ -1,23 +0,0 @@ -// RUN: %parallel-boogie "%s" > "%t" -// RUN: %diff "%s.expect" "%t" - -atomic action {:layer 1, 2} A3({:linear_in} path: Lset int, {:linear_out} l: Lset int) returns (path': Lset int) { - call path' := Lset_Empty(); - call Lset_Put(path', path); - call Lset_Split(path', l); -} - -atomic action {:layer 1, 2} A5({:linear_in} path: Lheap int) returns (path': Lheap int) { - path' := path; -} - -var {:layer 0, 2} g: Lheap int; - -datatype Foo { Foo(f: Lheap int) } - -atomic action {:layer 1, 2} A10({:linear_in} a: Foo) returns (b: Foo) -{ - var x: Lheap int; - Foo(x) := a; - b := Foo(x); -} diff --git a/Test/civl/regression-tests/linear_types_error.bpl b/Test/civl/regression-tests/linear_types_error.bpl deleted file mode 100644 index a8891f09a..000000000 --- a/Test/civl/regression-tests/linear_types_error.bpl +++ /dev/null @@ -1,49 +0,0 @@ -// RUN: %parallel-boogie "%s" > "%t" -// RUN: %diff "%s.expect" "%t" - -atomic action {:layer 1, 2} A0(path: Lheap int) returns (l: Lheap int) { } - -atomic action {:layer 1, 2} A1(path: Lheap int) returns (path': Lheap int) { - path' := path; -} - -atomic action {:layer 1, 2} A2(path: Lheap int) returns (path': Lheap int) { var k: Lset (Ref int); - call path' := Lmap_Empty(); - call k := Lmap_Free(path); -} - -var {:layer 0, 2} g: Lheap int; - -datatype Foo { Foo(f: Lheap int) } - -atomic action {:layer 1, 2} A5({:linear_out} path: Lheap int) { } - -atomic action {:layer 1, 2} A11({:linear_in} a: Foo) returns (b: Foo) -{ - var x: Lheap int; - Foo(x) := a; -} - -atomic action {:layer 1, 2} A12({:linear_in} a: Foo) returns (b: Foo) -{ - var x: Lheap int; - b := a; - Foo(x) := a; -} - -atomic action {:layer 1, 2} A13({:linear_in} a: Foo) returns (b: Foo) -{ - var x: Lheap int; - b := Foo(x); -} - -yield procedure {:layer 1} Foo1(x: Lheap int) -{ - call Lmap_Assume(x, x); -} - -yield procedure {:layer 1} Foo2(x: Foo) -{ - call Lmap_Assume(x->f, x->f); -} - diff --git a/Test/civl/regression-tests/linear_types_error.bpl.expect b/Test/civl/regression-tests/linear_types_error.bpl.expect deleted file mode 100644 index e6d2f50df..000000000 --- a/Test/civl/regression-tests/linear_types_error.bpl.expect +++ /dev/null @@ -1,10 +0,0 @@ -linear_types_error.bpl(4,73): Error: Output variable l must be available at a return -linear_types_error.bpl(8,0): Error: Input variable path must be available at a return -linear_types_error.bpl(13,0): Error: Input variable path must be available at a return -linear_types_error.bpl(19,64): Error: Input variable path must be available at a return -linear_types_error.bpl(25,0): Error: Output variable b must be available at a return -linear_types_error.bpl(31,14): Error: unavailable source for a linear read -linear_types_error.bpl(37,9): Error: unavailable source for a linear read -linear_types_error.bpl(42,2): Error: Linear variable x can occur only once as an input parameter -linear_types_error.bpl(47,2): Error: Linear variable x can occur only once as an input parameter -9 type checking errors detected in linear_types_error.bpl diff --git a/Test/civl/samples/alloc-mem.bpl b/Test/civl/samples/alloc-mem.bpl index b3a98f59a..4d7f17df0 100644 --- a/Test/civl/samples/alloc-mem.bpl +++ b/Test/civl/samples/alloc-mem.bpl @@ -1,15 +1,19 @@ // RUN: %parallel-boogie "%s" > "%t" // RUN: %diff "%s.expect" "%t" -function {:inline} PoolInv(unallocated:[int]bool, pool:Lset int) : (bool) +type {:linear "mem"} X = int; +function {:inline}{:linear "mem"} SetCollector(x: Set int): [int]bool { x->val } +function {:inline}{:linear "mem"} MapCollector(x: Map int int): [int]bool { SetCollector(x->dom) } + +function {:inline} PoolInv(unallocated:[int]bool, pool:Set int) : (bool) { - (forall x:int :: unallocated[x] ==> Lset_Contains(pool, x)) + (forall x:int :: unallocated[x] ==> Set_Contains(pool, x)) } yield procedure {:layer 2} Main () preserves call Yield(); { - var {:layer 1,2} l:Lmap int int; + var {:layer 1,2} {:linear "mem"} l:Map int int; var i:int; while (*) invariant {:yields} true; @@ -20,13 +24,13 @@ preserves call Yield(); } } -yield procedure {:layer 2} Thread ({:layer 1,2} {:linear_in} local_in:Lmap int int, i:int) +yield procedure {:layer 2} Thread ({:layer 1,2} {:linear_in "mem"} local_in:Map int int, i:int) preserves call Yield(); -requires {:layer 1,2} Map_Contains(local_in->val, i); +requires {:layer 1,2} Map_Contains(local_in, i); { var y, o:int; - var {:layer 1,2} local:Lmap int int; - var {:layer 1,2} l:Lmap int int; + var {:layer 1,2} {:linear "mem"} local:Map int int; + var {:layer 1,2} {:linear "mem"} l:Map int int; call local := Write(local_in, i, 42); call o := Read(local, i); @@ -43,56 +47,55 @@ requires {:layer 1,2} Map_Contains(local_in->val, i); } } -right action {:layer 2} atomic_Alloc() returns (l:Lmap int int, i:int) +right action {:layer 2} atomic_Alloc() returns ({:linear "mem"} l:Map int int, i:int) modifies pool; { - assume Lset_Contains(pool, i); + assume Set_Contains(pool, i); call l, pool := AllocLinear(i, pool); } yield procedure {:layer 1} -Alloc() returns ({:layer 1} l:Lmap int int, i:int) +Alloc() returns ({:layer 1} {:linear "mem"} l:Map int int, i:int) refines atomic_Alloc; preserves call Yield(); -ensures {:layer 1} Map_Contains(l->val, i); +ensures {:layer 1} Map_Contains(l, i); { call i := PickAddr(); call {:layer 1} l, pool := AllocLinear(i, pool); } -left action {:layer 2} atomic_Free({:linear_in} l:Lmap int int, i:int) +left action {:layer 2} atomic_Free({:linear_in "mem"} l:Map int int, i:int) modifies pool; { - var t:Lset int; - assert Map_Contains(l->val, i); - call t := Lmap_Free(l); - call Lset_Put(pool, t); + assert Map_Contains(l, i); + pool := Set_Union(pool, l->dom); } -yield procedure {:layer 1} Free({:layer 1} {:linear_in} l:Lmap int int, i:int) +yield procedure {:layer 1} Free({:layer 1} {:linear_in "mem"} l:Map int int, i:int) refines atomic_Free; -requires {:layer 1} Map_Contains(l->val, i); +requires {:layer 1} Map_Contains(l, i); preserves call Yield(); { call {:layer 1} pool := FreeLinear(l, i, pool); call ReturnAddr(i); } -both action {:layer 2} atomic_Read (l:Lmap int int, i:int) returns (o:int) +both action {:layer 2} atomic_Read ({:linear "mem"} l:Map int int, i:int) returns (o:int) { - assert Map_Contains(l->val, i); - o := l->val->val[i]; + assert Map_Contains(l, i); + o := l->val[i]; } -both action {:layer 2} atomic_Write ({:linear_in} l:Lmap int int, i:int, o:int) returns (l':Lmap int int) +both action {:layer 2} atomic_Write ({:linear_in "mem"} l:Map int int, i:int, o:int) + returns ({:linear "mem"} l':Map int int) { - assert Map_Contains(l->val, i); + assert Map_Contains(l, i); l' := l; - l'->val->val[i] := o; + l'->val[i] := o; } yield procedure {:layer 1} -Read ({:layer 1} l:Lmap int int, i:int) returns (o:int) +Read ({:layer 1} {:linear "mem"} l:Map int int, i:int) returns (o:int) refines atomic_Read; requires call YieldMem(l, i); ensures call Yield(); @@ -101,50 +104,49 @@ ensures call Yield(); } yield procedure {:layer 1} -Write ({:layer 1} {:linear_in} l:Lmap int int, i:int, o:int) returns ({:layer 1} l':Lmap int int) +Write ({:layer 1} {:linear_in "mem"} l:Map int int, i:int, o:int) + returns ({:layer 1} {:linear "mem"} l':Map int int) refines atomic_Write; requires call Yield(); -requires {:layer 1} Map_Contains(l->val, i); +requires {:layer 1} Map_Contains(l, i); ensures call YieldMem(l', i); { call WriteLow(i, o); call {:layer 1} l' := WriteLinear(l, i, o); } -pure action AllocLinear (i:int, {:linear_in} pool:Lset int) returns (l:Lmap int int, pool':Lset int) +pure action AllocLinear (i:int, {:linear_in "mem"} pool:Set int) + returns ({:linear "mem"} l:Map int int, {:linear "mem"} pool':Set int) { var m:[int]int; - var t:Lset int; - assert Lset_Contains(pool, i); - pool' := pool; - call t := Lset_Get(pool', MapOne(i)); - call l := Lmap_Create(t, m); + assert Set_Contains(pool, i); + pool' := Set_Remove(pool, i); + l := Map(Set_Singleton(i), m); } -pure action FreeLinear ({:linear_in} l:Lmap int int, i:int, {:linear_in} pool:Lset int) returns (pool':Lset int) +pure action FreeLinear ({:linear_in "mem"} l:Map int int, i:int, {:linear_in "mem"} pool:Set int) + returns ({:linear "mem"} pool':Set int) { - var t: Lset int; - assert Map_Contains(l->val, i); - call t := Lmap_Free(l); - pool' := pool; - call Lset_Put(pool', t); + assert Map_Contains(l, i); + pool' := Set_Union(pool, l->dom); } -pure action WriteLinear ({:layer 1} {:linear_in} l:Lmap int int, i:int, o:int) returns ({:layer 1} l':Lmap int int) +pure action WriteLinear ({:layer 1} {:linear_in "mem"} l:Map int int, i:int, o:int) + returns ({:layer 1} {:linear "mem"} l':Map int int) { - assert Map_Contains(l->val, i); + assert Map_Contains(l, i); l' := l; - l'->val->val[i] := o; + l'->val[i] := o; } yield invariant {:layer 1} Yield (); invariant PoolInv(unallocated, pool); -yield invariant {:layer 1} YieldMem ({:layer 1} l:Lmap int int, i:int); +yield invariant {:layer 1} YieldMem ({:layer 1} {:linear "mem"} l:Map int int, i:int); invariant PoolInv(unallocated, pool); -invariant Map_Contains(l->val, i) && Map_At(l->val, i) == mem[i]; +invariant Map_Contains(l, i) && Map_At(l, i) == mem[i]; -var {:layer 1, 2} pool:Lset int; +var {:layer 1, 2} {:linear "mem"} pool:Set int; var {:layer 0, 1} mem:[int]int; var {:layer 0, 1} unallocated:[int]bool; diff --git a/Test/civl/samples/alloc-mem.bpl.expect b/Test/civl/samples/alloc-mem.bpl.expect index 0999d9ead..0c0d03d71 100644 --- a/Test/civl/samples/alloc-mem.bpl.expect +++ b/Test/civl/samples/alloc-mem.bpl.expect @@ -1,2 +1,2 @@ -Boogie program verifier finished with 13 verified, 0 errors +Boogie program verifier finished with 20 verified, 0 errors diff --git a/Test/civl/samples/bluetooth.bpl b/Test/civl/samples/bluetooth.bpl index b74205853..5dd71c065 100644 --- a/Test/civl/samples/bluetooth.bpl +++ b/Test/civl/samples/bluetooth.bpl @@ -12,10 +12,12 @@ see cav2020-3.bpl for another example inspired by a concurrent garbage collector. */ -datatype Perm { Left(i: int), Right(i: int) } +datatype {:linear "perm"} Perm { Left(i: int), Right(i: int) } + +function {:inline}{:linear "perm"} PermCollector(x: Set Perm): [Perm]bool { x->val } function Size(set: [T]bool): int; -axiom {:ctor "Lset"} (forall set: [T]bool :: Size(set) >= 0); +axiom (forall set: [T]bool :: Size(set) >= 0); pure procedure SizeLemma(X: [T]bool, x: T); ensures Size(X[x := false]) + 1 == Size(X[x := true]); @@ -26,7 +28,7 @@ ensures X == Y || Size(X) < Size(Y); var {:layer 0,3} stoppingFlag: bool; var {:layer 0,2} stopped: bool; -var {:layer 1,2} usersInDriver: Lset Perm; +var {:layer 1,2} {:linear "perm"} usersInDriver: Set Perm; var {:layer 0,1} pendingIo: int; var {:layer 0,1} stoppingEvent: bool; @@ -34,16 +36,16 @@ yield invariant {:layer 2} Inv2(); invariant stopped ==> stoppingFlag; yield invariant {:layer 1} Inv1(); -invariant stoppingEvent ==> stoppingFlag && usersInDriver->dom == MapConst(false); -invariant pendingIo == Size(usersInDriver->dom) + (if stoppingFlag then 0 else 1); +invariant stoppingEvent ==> stoppingFlag && usersInDriver->val == MapConst(false); +invariant pendingIo == Size(usersInDriver->val) + (if stoppingFlag then 0 else 1); // user code yield procedure {:layer 2} -User(i: int, {:layer 1,2} l: Lset Perm, {:layer 1,2} r: Lset Perm) +User(i: int, {:layer 1,2} {:linear "perm"} l: Set Perm, {:linear "perm"} {:layer 1,2} r: Set Perm) preserves call Inv2(); preserves call Inv1(); -requires {:layer 1, 2} l->dom == MapOne(Left(i)) && r->dom == MapOne(Right(i)); +requires {:layer 1, 2} l->val == MapOne(Left(i)) && r->val == MapOne(Right(i)); { while (*) invariant {:yields} true; @@ -56,51 +58,64 @@ requires {:layer 1, 2} l->dom == MapOne(Left(i)) && r->dom == MapOne(Right(i)); } } -atomic action {:layer 2} AtomicEnter#1(i: int, {:linear_in} l: Lset Perm, r: Lset Perm) +atomic action {:layer 2} AtomicEnter#1(i: int, {:linear_in "perm"} l: Set Perm, {:linear "perm"} r: Set Perm) modifies usersInDriver; { assume !stoppingFlag; - call Lset_Put(usersInDriver, l); + usersInDriver := Set_Union(usersInDriver, l); } yield procedure {:layer 1} -Enter#1(i: int, {:layer 1} {:linear_in} l: Lset Perm, {:layer 1} r: Lset Perm) +Enter#1(i: int, {:layer 1} {:linear_in "perm"} l: Set Perm, {:layer 1} {:linear "perm"} r: Set Perm) refines AtomicEnter#1; preserves call Inv1(); -requires {:layer 1} l->dom == MapOne(Left(i)) && r->dom == MapOne(Right(i)); +requires {:layer 1} l->val == MapOne(Left(i)) && r->val == MapOne(Right(i)); { call Enter(); - call {:layer 1} SizeLemma(usersInDriver->dom, Left(i)); - call {:layer 1} Lset_Put(usersInDriver, l); + call {:layer 1} SizeLemma(usersInDriver->val, Left(i)); + call {:layer 1} usersInDriver := A(usersInDriver, l); +} + +pure action A({:linear_in "perm"} usersInDriver: Set Perm, {:linear_in "perm"} l: Set Perm) + returns ({:linear "perm"} usersInDriver': Set Perm) +{ + usersInDriver' := Set_Union(usersInDriver, l); } -left action {:layer 2} AtomicCheckAssert#1(i: int, r: Lset Perm) +left action {:layer 2} AtomicCheckAssert#1(i: int, {:linear "perm"} r: Set Perm) { - assert r->dom == MapOne(Right(i)) && usersInDriver->dom[Left(i)]; + assert r->val == MapOne(Right(i)) && usersInDriver->val[Left(i)]; assert !stopped; } yield procedure {:layer 1} -CheckAssert#1(i: int, {:layer 1} r: Lset Perm) +CheckAssert#1(i: int, {:layer 1} {:linear "perm"} r: Set Perm) refines AtomicCheckAssert#1; preserves call Inv1(); { call CheckAssert(); } -left action {:layer 2} AtomicExit(i: int, {:linear_out} l: Lset Perm, r: Lset Perm) +left action {:layer 2} AtomicExit(i: int, {:linear_out "perm"} l: Set Perm, {:linear "perm"} r: Set Perm) modifies usersInDriver; { - assert l->dom == MapOne(Left(i)) && r->dom == MapOne(Right(i)); - call Lset_Split(usersInDriver, l); + assert l->val == MapOne(Left(i)) && r->val == MapOne(Right(i)); + call usersInDriver := B(usersInDriver, l); } yield procedure {:layer 1} -Exit(i: int, {:layer 1} {:linear_out} l: Lset Perm, {:layer 1} r: Lset Perm) +Exit(i: int, {:layer 1} {:linear_out "perm"} l: Set Perm, {:layer 1} {:linear "perm"} r: Set Perm) refines AtomicExit; preserves call Inv1(); { call DeleteReference(); - call {:layer 1} SizeLemma(usersInDriver->dom, Left(i)); - call {:layer 1} Lset_Split(usersInDriver, l); - call {:layer 1} SubsetSizeRelationLemma(MapConst(false), usersInDriver->dom); + call {:layer 1} SizeLemma(usersInDriver->val, Left(i)); + call {:layer 1} usersInDriver := B(usersInDriver, l); + call {:layer 1} SubsetSizeRelationLemma(MapConst(false), usersInDriver->val); +} + +pure action B({:linear_in "perm"} usersInDriver: Set Perm, {:linear_out "perm"} l: Set Perm) + returns ({:linear "perm"} usersInDriver': Set Perm) +{ + assert Set_IsSubset(l, usersInDriver); + usersInDriver' := Set_Difference(usersInDriver, l); } // stopper code @@ -121,13 +136,13 @@ preserves call Inv1(); { call SetStoppingFlag(i); call DeleteReference(); - call {:layer 1} SubsetSizeRelationLemma(MapConst(false), usersInDriver->dom); + call {:layer 1} SubsetSizeRelationLemma(MapConst(false), usersInDriver->val); } atomic action {:layer 2} AtomicWaitAndStop() modifies stopped; { - assume usersInDriver->dom == MapConst(false); + assume usersInDriver->val == MapConst(false); stopped := true; } yield procedure {:layer 1} WaitAndStop() diff --git a/Test/civl/samples/bluetooth.bpl.expect b/Test/civl/samples/bluetooth.bpl.expect index d4fb07c44..c4cf5ccf4 100644 --- a/Test/civl/samples/bluetooth.bpl.expect +++ b/Test/civl/samples/bluetooth.bpl.expect @@ -1,2 +1,2 @@ -Boogie program verifier finished with 25 verified, 0 errors +Boogie program verifier finished with 30 verified, 0 errors diff --git a/Test/civl/samples/civl-paper.bpl b/Test/civl/samples/civl-paper.bpl index 83019099b..1c788662e 100644 --- a/Test/civl/samples/civl-paper.bpl +++ b/Test/civl/samples/civl-paper.bpl @@ -4,7 +4,11 @@ type {:linear "tid"} X; const nil: X; -var {:layer 0,3} g: Lmap int int; +type {:linear "mem"} Y = int; +function {:inline}{:linear "mem"} SetCollector(x: Set int): [int]bool { x->val } +function {:inline}{:linear "mem"} MapCollector(x: Map int int): [int]bool { SetCollector(x->dom) } + +var {:layer 0,3} {:linear "mem"} g: Map int int; var {:layer 0,3} lock: X; var {:layer 0,1} b: bool; @@ -14,7 +18,7 @@ yield invariant {:layer 1} InvLock(); invariant lock != nil <==> b; yield invariant {:layer 3} InvMem(); -invariant Map_Contains(g->val, p) && Map_Contains(g->val, p+4) && Map_At(g->val, p) == Map_At(g->val, p+4); +invariant Map_Contains(g, p) && Map_Contains(g, p+4) && Map_At(g, p) == Map_At(g, p+4); yield procedure {:layer 3} P({:linear "tid"} tid: X) requires {:layer 1,3} tid != nil; @@ -22,7 +26,7 @@ preserves call InvLock(); preserves call InvMem(); { var t: int; - var l: Lmap int int; + var {:linear "mem"} l: Map int int; call AcquireProtected(tid); call l := TransferFromGlobalProtected(tid); @@ -34,24 +38,24 @@ preserves call InvMem(); call ReleaseProtected(tid); } -both action {:layer 3} AtomicTransferToGlobalProtected({:linear "tid"} tid: X, {:linear_in} l: Lmap int int) +both action {:layer 3} AtomicTransferToGlobalProtected({:linear "tid"} tid: X, {:linear_in "mem"} l: Map int int) modifies g; { assert tid != nil && lock == tid; g := l; } yield procedure {:layer 2} -TransferToGlobalProtected({:linear "tid"} tid: X, {:linear_in} l: Lmap int int) +TransferToGlobalProtected({:linear "tid"} tid: X, {:linear_in "mem"} l: Map int int) refines AtomicTransferToGlobalProtected; preserves call InvLock(); { call TransferToGlobal(tid, l); } -both action {:layer 3} AtomicTransferFromGlobalProtected({:linear "tid"} tid: X) returns (l: Lmap int int) +both action {:layer 3} AtomicTransferFromGlobalProtected({:linear "tid"} tid: X) returns ({:linear "mem"} l: Map int int) modifies g; -{ assert tid != nil && lock == tid; l := g; call g := Lmap_Empty(); } +{ assert tid != nil && lock == tid; l := g; g := Map_Empty(); } yield procedure {:layer 2} -TransferFromGlobalProtected({:linear "tid"} tid: X) returns (l: Lmap int int) +TransferFromGlobalProtected({:linear "tid"} tid: X) returns ({:linear "mem"} l: Map int int) refines AtomicTransferFromGlobalProtected; preserves call InvLock(); { @@ -115,30 +119,31 @@ preserves call InvLock(); call CLEAR(tid, false); } -atomic action {:layer 1,2} AtomicTransferToGlobal({:linear "tid"} tid: X, {:linear_in} l: Lmap int int) +atomic action {:layer 1,2} AtomicTransferToGlobal({:linear "tid"} tid: X, {:linear_in "mem"} l: Map int int) modifies g; { g := l; } -yield procedure {:layer 0} TransferToGlobal({:linear "tid"} tid: X, {:linear_in} l: Lmap int int); +yield procedure {:layer 0} TransferToGlobal({:linear "tid"} tid: X, {:linear_in "mem"} l: Map int int); refines AtomicTransferToGlobal; -atomic action {:layer 1,2} AtomicTransferFromGlobal({:linear "tid"} tid: X) returns (l: Lmap int int) +atomic action {:layer 1,2} AtomicTransferFromGlobal({:linear "tid"} tid: X) returns ({:linear "mem"} l: Map int int) modifies g; -{ l := g; call g := Lmap_Empty(); } +{ l := g; g := Map_Empty(); } -yield procedure {:layer 0} TransferFromGlobal({:linear "tid"} tid: X) returns (l: Lmap int int); +yield procedure {:layer 0} TransferFromGlobal({:linear "tid"} tid: X) returns ({:linear "mem"} l: Map int int); refines AtomicTransferFromGlobal; -both action {:layer 1,3} AtomicLoad(l: Lmap int int, a: int) returns (v: int) -{ v := l->val->val[a]; } +both action {:layer 1,3} AtomicLoad({:linear "mem"} l: Map int int, a: int) returns (v: int) +{ v := l->val[a]; } -yield procedure {:layer 0} Load(l: Lmap int int, a: int) returns (v: int); +yield procedure {:layer 0} Load({:linear "mem"} l: Map int int, a: int) returns (v: int); refines AtomicLoad; -both action {:layer 1,3} AtomicStore({:linear_in} l_in: Lmap int int, a: int, v: int) returns (l_out: Lmap int int) -{ l_out := l_in; l_out->val->val[a] := v; } +both action {:layer 1,3} AtomicStore({:linear_in "mem"} l_in: Map int int, a: int, v: int) + returns ({:linear "mem"} l_out: Map int int) +{ l_out := l_in; l_out->val[a] := v; } -yield procedure {:layer 0} Store({:linear_in} l_in: Lmap int int, a: int, v: int) returns (l_out: Lmap int int); +yield procedure {:layer 0} Store({:linear_in "mem"} l_in: Map int int, a: int, v: int) returns ({:linear "mem"} l_out: Map int int); refines AtomicStore; atomic action {:layer 1} AtomicCAS(tid: X, prev: bool, next: bool) returns (status: bool) diff --git a/Test/civl/samples/civl-paper.bpl.expect b/Test/civl/samples/civl-paper.bpl.expect index 103f21a1e..129e60e25 100644 --- a/Test/civl/samples/civl-paper.bpl.expect +++ b/Test/civl/samples/civl-paper.bpl.expect @@ -1,2 +1,2 @@ -Boogie program verifier finished with 37 verified, 0 errors +Boogie program verifier finished with 39 verified, 0 errors