From 4c6dd519143fdbc8ecada56d58103d098c6bd18c Mon Sep 17 00:00:00 2001 From: qadeer Date: Wed, 22 Apr 2015 09:26:56 -0700 Subject: renamed og to civl --- Test/civl/DeviceCache.bpl | 210 +++++++++++++ Test/civl/DeviceCache.bpl.expect | 2 + Test/civl/FlanaganQadeer.bpl | 75 +++++ Test/civl/FlanaganQadeer.bpl.expect | 2 + Test/civl/Program1.bpl | 33 +++ Test/civl/Program1.bpl.expect | 2 + Test/civl/Program2.bpl | 37 +++ Test/civl/Program2.bpl.expect | 2 + Test/civl/Program3.bpl | 36 +++ Test/civl/Program3.bpl.expect | 2 + Test/civl/Program4.bpl | 68 +++++ Test/civl/Program4.bpl.expect | 2 + Test/civl/Program5.bpl | 79 +++++ Test/civl/Program5.bpl.expect | 2 + Test/civl/akash.bpl | 106 +++++++ Test/civl/akash.bpl.expect | 2 + Test/civl/bar.bpl | 57 ++++ Test/civl/bar.bpl.expect | 13 + Test/civl/chris.bpl | 28 ++ Test/civl/chris.bpl.expect | 2 + Test/civl/chris2.bpl | 34 +++ Test/civl/chris2.bpl.expect | 18 ++ Test/civl/civl-paper.bpl | 175 +++++++++++ Test/civl/civl-paper.bpl.expect | 2 + Test/civl/foo.bpl | 57 ++++ Test/civl/foo.bpl.expect | 8 + Test/civl/ghost.bpl | 46 +++ Test/civl/ghost.bpl.expect | 2 + Test/civl/linear-set.bpl | 105 +++++++ Test/civl/linear-set.bpl.expect | 2 + Test/civl/linear-set2.bpl | 106 +++++++ Test/civl/linear-set2.bpl.expect | 2 + Test/civl/lock-introduced.bpl | 100 +++++++ Test/civl/lock-introduced.bpl.expect | 2 + Test/civl/lock.bpl | 57 ++++ Test/civl/lock.bpl.expect | 2 + Test/civl/lock2.bpl | 63 ++++ Test/civl/lock2.bpl.expect | 2 + Test/civl/multiset.bpl | 324 ++++++++++++++++++++ Test/civl/multiset.bpl.expect | 2 + Test/civl/new1.bpl | 42 +++ Test/civl/new1.bpl.expect | 2 + Test/civl/one.bpl | 18 ++ Test/civl/one.bpl.expect | 2 + Test/civl/par-incr.bpl | 31 ++ Test/civl/par-incr.bpl.expect | 2 + Test/civl/parallel1.bpl | 48 +++ Test/civl/parallel1.bpl.expect | 8 + Test/civl/parallel2.bpl | 59 ++++ Test/civl/parallel2.bpl.expect | 2 + Test/civl/parallel4.bpl | 45 +++ Test/civl/parallel4.bpl.expect | 6 + Test/civl/parallel5.bpl | 59 ++++ Test/civl/parallel5.bpl.expect | 2 + Test/civl/perm.bpl | 49 +++ Test/civl/perm.bpl.expect | 2 + Test/civl/t1.bpl | 103 +++++++ Test/civl/t1.bpl.expect | 9 + Test/civl/termination.bpl | 18 ++ Test/civl/termination.bpl.expect | 3 + Test/civl/termination2.bpl | 19 ++ Test/civl/termination2.bpl.expect | 2 + Test/civl/ticket.bpl | 147 +++++++++ Test/civl/ticket.bpl.expect | 2 + Test/civl/treiber-stack.bpl | 202 +++++++++++++ Test/civl/treiber-stack.bpl.expect | 2 + Test/civl/wsq.bpl | 560 +++++++++++++++++++++++++++++++++++ Test/civl/wsq.bpl.expect | 2 + Test/og/DeviceCache.bpl | 210 ------------- Test/og/DeviceCache.bpl.expect | 2 - Test/og/FlanaganQadeer.bpl | 75 ----- Test/og/FlanaganQadeer.bpl.expect | 2 - Test/og/Program1.bpl | 33 --- Test/og/Program1.bpl.expect | 2 - Test/og/Program2.bpl | 37 --- Test/og/Program2.bpl.expect | 2 - Test/og/Program3.bpl | 36 --- Test/og/Program3.bpl.expect | 2 - Test/og/Program4.bpl | 68 ----- Test/og/Program4.bpl.expect | 2 - Test/og/Program5.bpl | 79 ----- Test/og/Program5.bpl.expect | 2 - Test/og/akash.bpl | 106 ------- Test/og/akash.bpl.expect | 2 - Test/og/bar.bpl | 57 ---- Test/og/bar.bpl.expect | 13 - Test/og/chris.bpl | 28 -- Test/og/chris.bpl.expect | 2 - Test/og/chris2.bpl | 34 --- Test/og/chris2.bpl.expect | 18 -- Test/og/civl-paper.bpl | 175 ----------- Test/og/civl-paper.bpl.expect | 2 - Test/og/foo.bpl | 57 ---- Test/og/foo.bpl.expect | 8 - Test/og/ghost.bpl | 46 --- Test/og/ghost.bpl.expect | 2 - Test/og/linear-set.bpl | 105 ------- Test/og/linear-set.bpl.expect | 2 - Test/og/linear-set2.bpl | 106 ------- Test/og/linear-set2.bpl.expect | 2 - Test/og/lock-introduced.bpl | 100 ------- Test/og/lock-introduced.bpl.expect | 2 - Test/og/lock.bpl | 57 ---- Test/og/lock.bpl.expect | 2 - Test/og/lock2.bpl | 63 ---- Test/og/lock2.bpl.expect | 2 - Test/og/multiset.bpl | 324 -------------------- Test/og/multiset.bpl.expect | 2 - Test/og/new1.bpl | 42 --- Test/og/new1.bpl.expect | 2 - Test/og/one.bpl | 18 -- Test/og/one.bpl.expect | 2 - Test/og/par-incr.bpl | 31 -- Test/og/par-incr.bpl.expect | 2 - Test/og/parallel1.bpl | 48 --- Test/og/parallel1.bpl.expect | 8 - Test/og/parallel2.bpl | 59 ---- Test/og/parallel2.bpl.expect | 2 - Test/og/parallel4.bpl | 45 --- Test/og/parallel4.bpl.expect | 6 - Test/og/parallel5.bpl | 59 ---- Test/og/parallel5.bpl.expect | 2 - Test/og/perm.bpl | 49 --- Test/og/perm.bpl.expect | 2 - Test/og/t1.bpl | 103 ------- Test/og/t1.bpl.expect | 9 - Test/og/termination.bpl | 18 -- Test/og/termination.bpl.expect | 3 - Test/og/termination2.bpl | 19 -- Test/og/termination2.bpl.expect | 2 - Test/og/ticket.bpl | 147 --------- Test/og/ticket.bpl.expect | 2 - Test/og/treiber-stack.bpl | 202 ------------- Test/og/treiber-stack.bpl.expect | 2 - Test/og/wsq.bpl | 560 ----------------------------------- Test/og/wsq.bpl.expect | 2 - 136 files changed, 3315 insertions(+), 3315 deletions(-) create mode 100644 Test/civl/DeviceCache.bpl create mode 100644 Test/civl/DeviceCache.bpl.expect create mode 100644 Test/civl/FlanaganQadeer.bpl create mode 100644 Test/civl/FlanaganQadeer.bpl.expect create mode 100644 Test/civl/Program1.bpl create mode 100644 Test/civl/Program1.bpl.expect create mode 100644 Test/civl/Program2.bpl create mode 100644 Test/civl/Program2.bpl.expect create mode 100644 Test/civl/Program3.bpl create mode 100644 Test/civl/Program3.bpl.expect create mode 100644 Test/civl/Program4.bpl create mode 100644 Test/civl/Program4.bpl.expect create mode 100644 Test/civl/Program5.bpl create mode 100644 Test/civl/Program5.bpl.expect create mode 100644 Test/civl/akash.bpl create mode 100644 Test/civl/akash.bpl.expect create mode 100644 Test/civl/bar.bpl create mode 100644 Test/civl/bar.bpl.expect create mode 100644 Test/civl/chris.bpl create mode 100644 Test/civl/chris.bpl.expect create mode 100644 Test/civl/chris2.bpl create mode 100644 Test/civl/chris2.bpl.expect create mode 100644 Test/civl/civl-paper.bpl create mode 100644 Test/civl/civl-paper.bpl.expect create mode 100644 Test/civl/foo.bpl create mode 100644 Test/civl/foo.bpl.expect create mode 100644 Test/civl/ghost.bpl create mode 100644 Test/civl/ghost.bpl.expect create mode 100644 Test/civl/linear-set.bpl create mode 100644 Test/civl/linear-set.bpl.expect create mode 100644 Test/civl/linear-set2.bpl create mode 100644 Test/civl/linear-set2.bpl.expect create mode 100644 Test/civl/lock-introduced.bpl create mode 100644 Test/civl/lock-introduced.bpl.expect create mode 100644 Test/civl/lock.bpl create mode 100644 Test/civl/lock.bpl.expect create mode 100644 Test/civl/lock2.bpl create mode 100644 Test/civl/lock2.bpl.expect create mode 100644 Test/civl/multiset.bpl create mode 100644 Test/civl/multiset.bpl.expect create mode 100644 Test/civl/new1.bpl create mode 100644 Test/civl/new1.bpl.expect create mode 100644 Test/civl/one.bpl create mode 100644 Test/civl/one.bpl.expect create mode 100644 Test/civl/par-incr.bpl create mode 100644 Test/civl/par-incr.bpl.expect create mode 100644 Test/civl/parallel1.bpl create mode 100644 Test/civl/parallel1.bpl.expect create mode 100644 Test/civl/parallel2.bpl create mode 100644 Test/civl/parallel2.bpl.expect create mode 100644 Test/civl/parallel4.bpl create mode 100644 Test/civl/parallel4.bpl.expect create mode 100644 Test/civl/parallel5.bpl create mode 100644 Test/civl/parallel5.bpl.expect create mode 100644 Test/civl/perm.bpl create mode 100644 Test/civl/perm.bpl.expect create mode 100644 Test/civl/t1.bpl create mode 100644 Test/civl/t1.bpl.expect create mode 100644 Test/civl/termination.bpl create mode 100644 Test/civl/termination.bpl.expect create mode 100644 Test/civl/termination2.bpl create mode 100644 Test/civl/termination2.bpl.expect create mode 100644 Test/civl/ticket.bpl create mode 100644 Test/civl/ticket.bpl.expect create mode 100644 Test/civl/treiber-stack.bpl create mode 100644 Test/civl/treiber-stack.bpl.expect create mode 100644 Test/civl/wsq.bpl create mode 100644 Test/civl/wsq.bpl.expect delete mode 100644 Test/og/DeviceCache.bpl delete mode 100644 Test/og/DeviceCache.bpl.expect delete mode 100644 Test/og/FlanaganQadeer.bpl delete mode 100644 Test/og/FlanaganQadeer.bpl.expect delete mode 100644 Test/og/Program1.bpl delete mode 100644 Test/og/Program1.bpl.expect delete mode 100644 Test/og/Program2.bpl delete mode 100644 Test/og/Program2.bpl.expect delete mode 100644 Test/og/Program3.bpl delete mode 100644 Test/og/Program3.bpl.expect delete mode 100644 Test/og/Program4.bpl delete mode 100644 Test/og/Program4.bpl.expect delete mode 100644 Test/og/Program5.bpl delete mode 100644 Test/og/Program5.bpl.expect delete mode 100644 Test/og/akash.bpl delete mode 100644 Test/og/akash.bpl.expect delete mode 100644 Test/og/bar.bpl delete mode 100644 Test/og/bar.bpl.expect delete mode 100644 Test/og/chris.bpl delete mode 100644 Test/og/chris.bpl.expect delete mode 100644 Test/og/chris2.bpl delete mode 100644 Test/og/chris2.bpl.expect delete mode 100644 Test/og/civl-paper.bpl delete mode 100644 Test/og/civl-paper.bpl.expect delete mode 100644 Test/og/foo.bpl delete mode 100644 Test/og/foo.bpl.expect delete mode 100644 Test/og/ghost.bpl delete mode 100644 Test/og/ghost.bpl.expect delete mode 100644 Test/og/linear-set.bpl delete mode 100644 Test/og/linear-set.bpl.expect delete mode 100644 Test/og/linear-set2.bpl delete mode 100644 Test/og/linear-set2.bpl.expect delete mode 100644 Test/og/lock-introduced.bpl delete mode 100644 Test/og/lock-introduced.bpl.expect delete mode 100644 Test/og/lock.bpl delete mode 100644 Test/og/lock.bpl.expect delete mode 100644 Test/og/lock2.bpl delete mode 100644 Test/og/lock2.bpl.expect delete mode 100644 Test/og/multiset.bpl delete mode 100644 Test/og/multiset.bpl.expect delete mode 100644 Test/og/new1.bpl delete mode 100644 Test/og/new1.bpl.expect delete mode 100644 Test/og/one.bpl delete mode 100644 Test/og/one.bpl.expect delete mode 100644 Test/og/par-incr.bpl delete mode 100644 Test/og/par-incr.bpl.expect delete mode 100644 Test/og/parallel1.bpl delete mode 100644 Test/og/parallel1.bpl.expect delete mode 100644 Test/og/parallel2.bpl delete mode 100644 Test/og/parallel2.bpl.expect delete mode 100644 Test/og/parallel4.bpl delete mode 100644 Test/og/parallel4.bpl.expect delete mode 100644 Test/og/parallel5.bpl delete mode 100644 Test/og/parallel5.bpl.expect delete mode 100644 Test/og/perm.bpl delete mode 100644 Test/og/perm.bpl.expect delete mode 100644 Test/og/t1.bpl delete mode 100644 Test/og/t1.bpl.expect delete mode 100644 Test/og/termination.bpl delete mode 100644 Test/og/termination.bpl.expect delete mode 100644 Test/og/termination2.bpl delete mode 100644 Test/og/termination2.bpl.expect delete mode 100644 Test/og/ticket.bpl delete mode 100644 Test/og/ticket.bpl.expect delete mode 100644 Test/og/treiber-stack.bpl delete mode 100644 Test/og/treiber-stack.bpl.expect delete mode 100644 Test/og/wsq.bpl delete mode 100644 Test/og/wsq.bpl.expect (limited to 'Test') diff --git a/Test/civl/DeviceCache.bpl b/Test/civl/DeviceCache.bpl new file mode 100644 index 00000000..f439b607 --- /dev/null +++ b/Test/civl/DeviceCache.bpl @@ -0,0 +1,210 @@ +// RUN: %boogie -noinfer -typeEncoding:m -useArrayTheory "%s" > "%t" +// RUN: %diff "%s.expect" "%t" +type X; +function {:builtin "MapConst"} mapconstbool(bool): [X]bool; +const nil: X; +var {:layer 0,1} ghostLock: X; +var {:layer 0,1} lock: X; +var {:layer 0,1} currsize: int; +var {:layer 0,1} newsize: int; + +function {:builtin "MapConst"} MapConstBool(bool) : [X]bool; +function {:inline} {:linear "tid"} TidCollector(x: X) : [X]bool +{ + MapConstBool(false)[x := true] +} +function {:inline} {:linear "tid"} TidSetCollector(x: [X]bool) : [X]bool +{ + x +} + +function {:inline} Inv(ghostLock: X, currsize: int, newsize: int) : (bool) +{ + 0 <= currsize && currsize <= newsize && + (ghostLock == nil <==> currsize == newsize) +} + +procedure {:yields} {:layer 1} Yield() +requires {:layer 1} Inv(ghostLock, currsize, newsize); +ensures {:layer 1} Inv(ghostLock, currsize, newsize); +{ + yield; + assert {:layer 1} Inv(ghostLock, currsize, newsize); +} + +procedure {:yields} {:layer 1} YieldToReadCache({:linear "tid"} tid: X) +requires {:layer 1} Inv(ghostLock, currsize, newsize) && tid != nil; +ensures {:layer 1} Inv(ghostLock, currsize, newsize) && old(currsize) <= currsize; +{ + yield; + assert {:layer 1} Inv(ghostLock, currsize, newsize) && old(currsize) <= currsize; +} + +procedure {:yields} {:layer 1} YieldToWriteCache({:linear "tid"} tid: X) +requires {:layer 1} Inv(ghostLock, currsize, newsize) && ghostLock == tid && tid != nil; +ensures {:layer 1} Inv(ghostLock, currsize, newsize) && ghostLock == tid && old(currsize) == currsize && old(newsize) == newsize; +{ + yield; + assert {:layer 1} Inv(ghostLock, currsize, newsize) && tid != nil && ghostLock == tid && old(currsize) == currsize && old(newsize) == newsize; +} + +procedure {:yields} {:layer 1} Allocate() returns ({:linear "tid"} xl: X) +ensures {:layer 1} xl != nil; +{ + yield; + call xl := AllocateLow(); + yield; +} + +procedure {:yields} {:layer 1} main({:linear_in "tid"} xls: [X]bool) +requires {:layer 1} xls == mapconstbool(true); +{ + var {:linear "tid"} tid: X; + + yield; + + call Init(xls); + + yield; + assert {:layer 1} Inv(ghostLock, currsize, newsize); + + while (*) + invariant {:layer 1} Inv(ghostLock, currsize, newsize); + { + par tid := Allocate() | Yield(); + yield; + assert {:layer 1} Inv(ghostLock, currsize, newsize); + async call Thread(tid); + yield; + assert {:layer 1} Inv(ghostLock, currsize, newsize); + } + yield; +} + +procedure {:yields} {:layer 1} Thread({:linear "tid"} tid: X) +requires {:layer 1} tid != nil; +requires {:layer 1} Inv(ghostLock, currsize, newsize); +{ + var start, size, bytesRead: int; + + havoc start, size; + assume (0 <= start && 0 <= size); + call bytesRead := Read(tid, start, size); +} + +procedure {:yields} {:layer 1} Read({:linear "tid"} tid: X, start : int, size : int) returns (bytesRead : int) +requires {:layer 1} tid != nil; +requires {:layer 1} 0 <= start && 0 <= size; +requires {:layer 1} Inv(ghostLock, currsize, newsize); +ensures {:layer 1} 0 <= bytesRead && bytesRead <= size; +{ + var i, tmp: int; + + par YieldToReadCache(tid); + bytesRead := size; + call acquire(tid); + call i := ReadCurrsize(tid); + call tmp := ReadNewsize(tid); + if (start + size <= i) { + call release(tid); + goto COPY_TO_BUFFER; + } else if (tmp > i) { + bytesRead := if (start <= i) then (i - start) else 0; + call release(tid); + goto COPY_TO_BUFFER; + } else { + call WriteNewsize(tid, start + size); + call release(tid); + goto READ_DEVICE; + } + +READ_DEVICE: + par YieldToWriteCache(tid); + call WriteCache(tid, start + size); + par YieldToWriteCache(tid); + call acquire(tid); + call tmp := ReadNewsize(tid); + call WriteCurrsize(tid, tmp); + call release(tid); + +COPY_TO_BUFFER: + par YieldToReadCache(tid); + call ReadCache(tid, start, bytesRead); +} + +procedure {:yields} {:layer 1} WriteCache({:linear "tid"} tid: X, index: int) +requires {:layer 1} Inv(ghostLock, currsize, newsize); +requires {:layer 1} ghostLock == tid && tid != nil; +ensures {:layer 1} ghostLock == tid; +ensures {:layer 1} Inv(ghostLock, currsize, newsize) && old(currsize) == currsize && old(newsize) == newsize; +{ + var j: int; + + par YieldToWriteCache(tid); + call j := ReadCurrsize(tid); + while (j < index) + invariant {:layer 1} ghostLock == tid && currsize <= j && tid == tid; + invariant {:layer 1} Inv(ghostLock, currsize, newsize) && old(currsize) == currsize && old(newsize) == newsize; + { + par YieldToWriteCache(tid); + call WriteCacheEntry(tid, j); + j := j + 1; + } + par YieldToWriteCache(tid); +} + +procedure {:yields} {:layer 1} ReadCache({:linear "tid"} tid: X, start: int, bytesRead: int) +requires {:layer 1} Inv(ghostLock, currsize, newsize); +requires {:layer 1} tid != nil; +requires {:layer 1} 0 <= start && 0 <= bytesRead; +requires {:layer 1} (bytesRead == 0 || start + bytesRead <= currsize); +ensures {:layer 1} Inv(ghostLock, currsize, newsize); +{ + var j: int; + + par YieldToReadCache(tid); + + j := 0; + while(j < bytesRead) + invariant {:layer 1} 0 <= j; + invariant {:layer 1} bytesRead == 0 || start + bytesRead <= currsize; + invariant {:layer 1} Inv(ghostLock, currsize, newsize); + { + assert {:layer 1} start + j < currsize; + call ReadCacheEntry(tid, start + j); + j := j + 1; + par YieldToReadCache(tid); + } + + par YieldToReadCache(tid); +} + +procedure {:yields} {:layer 0,1} Init({:linear_in "tid"} xls:[X]bool); +ensures {:atomic} |{ A: assert xls == mapconstbool(true); currsize := 0; newsize := 0; lock := nil; ghostLock := nil; return true; }|; + +procedure {:yields} {:layer 0,1} ReadCurrsize({:linear "tid"} tid: X) returns (val: int); +ensures {:right} |{A: assert tid != nil; assert lock == tid || ghostLock == tid; val := currsize; return true; }|; + +procedure {:yields} {:layer 0,1} ReadNewsize({:linear "tid"} tid: X) returns (val: int); +ensures {:right} |{A: assert tid != nil; assert lock == tid || ghostLock == tid; val := newsize; return true; }|; + +procedure {:yields} {:layer 0,1} WriteNewsize({:linear "tid"} tid: X, val: int); +ensures {:atomic} |{A: assert tid != nil; assert lock == tid && ghostLock == nil; newsize := val; ghostLock := tid; return true; }|; + +procedure {:yields} {:layer 0,1} WriteCurrsize({:linear "tid"} tid: X, val: int); +ensures {:atomic} |{A: assert tid != nil; assert lock == tid && ghostLock == tid; currsize := val; ghostLock := nil; return true; }|; + +procedure {:yields} {:layer 0,1} ReadCacheEntry({:linear "tid"} tid: X, index: int); +ensures {:atomic} |{ A: assert 0 <= index && index < currsize; return true; }|; + +procedure {:yields} {:layer 0,1} WriteCacheEntry({:linear "tid"} tid: X, index: int); +ensures {:right} |{ A: assert tid != nil; assert currsize <= index && ghostLock == tid; return true; }|; + +procedure {:yields} {:layer 0,1} acquire({:linear "tid"} tid: X); +ensures {:right} |{ A: assert tid != nil; assume lock == nil; lock := tid; return true; }|; + +procedure {:yields} {:layer 0,1} release({:linear "tid"} tid: X); +ensures {:left} |{ A: assert tid != nil; assert lock == tid; lock := nil; return true; }|; + +procedure {:yields} {:layer 0,1} AllocateLow() returns ({:linear "tid"} tid: X); +ensures {:atomic} |{ A: assume tid != nil; return true; }|; diff --git a/Test/civl/DeviceCache.bpl.expect b/Test/civl/DeviceCache.bpl.expect new file mode 100644 index 00000000..9ec7a92d --- /dev/null +++ b/Test/civl/DeviceCache.bpl.expect @@ -0,0 +1,2 @@ + +Boogie program verifier finished with 30 verified, 0 errors diff --git a/Test/civl/FlanaganQadeer.bpl b/Test/civl/FlanaganQadeer.bpl new file mode 100644 index 00000000..7345b5b2 --- /dev/null +++ b/Test/civl/FlanaganQadeer.bpl @@ -0,0 +1,75 @@ +// RUN: %boogie -noinfer -typeEncoding:m -useArrayTheory "%s" > "%t" +// RUN: %diff "%s.expect" "%t" +type X; +const nil: X; +var {:layer 0,1} l: X; +var {:layer 0,1} x: int; + +function {:builtin "MapConst"} MapConstBool(bool) : [X]bool; +function {:inline} {:linear "tid"} TidCollector(x: X) : [X]bool +{ + MapConstBool(false)[x := true] +} + +procedure {:yields} {:layer 1} Allocate() returns ({:linear "tid"} xl: X) +ensures {:layer 1} xl != nil; +{ + yield; + call xl := AllocateLow(); + yield; +} + +procedure {:yields} {:layer 1} main() +{ + var {:linear "tid"} tid: X; + var val: int; + + yield; + while (*) + { + call tid := Allocate(); + havoc val; + async call foo(tid, val); + yield; + } + yield; +} +procedure {:yields} {:layer 0,1} Lock(tid: X); +ensures {:atomic} |{A: assume l == nil; l := tid; return true; }|; + +procedure {:yields} {:layer 0,1} Unlock(); +ensures {:atomic} |{A: l := nil; return true; }|; + +procedure {:yields} {:layer 0,1} Set(val: int); +ensures {:atomic} |{A: x := val; return true; }|; + +procedure {:yields} {:layer 0,1} AllocateLow() returns ({:linear "tid"} xl: X); +ensures {:atomic} |{ A: assume xl != nil; return true; }|; + +procedure {:yields} {:layer 1} foo({:linear_in "tid"} tid': X, val: int) +requires {:layer 1} tid' != nil; +{ + var {:linear "tid"} tid: X; + tid := tid'; + + yield; + call Lock(tid); + call tid := Yield(tid); + call Set(val); + call tid := Yield(tid); + assert {:layer 1} x == val; + call tid := Yield(tid); + call Unlock(); + yield; +} + +procedure {:yields} {:layer 1} Yield({:linear_in "tid"} tid': X) returns ({:linear "tid"} tid: X) +requires {:layer 1} tid' != nil; +ensures {:layer 1} tid == tid'; +ensures {:layer 1} old(l) == tid ==> old(l) == l && old(x) == x; +{ + tid := tid'; + yield; + assert {:layer 1} tid != nil; + assert {:layer 1} (old(l) == tid ==> old(l) == l && old(x) == x); +} \ No newline at end of file diff --git a/Test/civl/FlanaganQadeer.bpl.expect b/Test/civl/FlanaganQadeer.bpl.expect new file mode 100644 index 00000000..fef5ddc0 --- /dev/null +++ b/Test/civl/FlanaganQadeer.bpl.expect @@ -0,0 +1,2 @@ + +Boogie program verifier finished with 4 verified, 0 errors diff --git a/Test/civl/Program1.bpl b/Test/civl/Program1.bpl new file mode 100644 index 00000000..f405b92a --- /dev/null +++ b/Test/civl/Program1.bpl @@ -0,0 +1,33 @@ +// RUN: %boogie -noinfer -typeEncoding:m -useArrayTheory "%s" > "%t" +// RUN: %diff "%s.expect" "%t" +var {:layer 0,1} x:int; + +procedure {:yields} {:layer 1} p() +requires {:layer 1} x >= 5; +ensures {:layer 1} x >= 8; +{ + yield; + assert {:layer 1} x >= 5; + call Incr(1); + yield; + assert {:layer 1} x >= 6; + call Incr(1); + yield; + assert {:layer 1} x >= 7; + call Incr(1); + yield; + assert {:layer 1} x >= 8; +} + +procedure {:yields} {:layer 1} q() +{ + yield; + call Incr(3); + yield; +} + +procedure {:yields} {:layer 0,1} Incr(val: int); +ensures {:atomic} +|{A: + x := x + val; return true; +}|; diff --git a/Test/civl/Program1.bpl.expect b/Test/civl/Program1.bpl.expect new file mode 100644 index 00000000..3de74d3e --- /dev/null +++ b/Test/civl/Program1.bpl.expect @@ -0,0 +1,2 @@ + +Boogie program verifier finished with 2 verified, 0 errors diff --git a/Test/civl/Program2.bpl b/Test/civl/Program2.bpl new file mode 100644 index 00000000..75c83c67 --- /dev/null +++ b/Test/civl/Program2.bpl @@ -0,0 +1,37 @@ +// RUN: %boogie -noinfer -typeEncoding:m -useArrayTheory "%s" > "%t" +// RUN: %diff "%s.expect" "%t" +var {:layer 0,1} x:int; + +procedure {:yields} {:layer 1} yield_x(n: int) +requires {:layer 1} x >= n; +ensures {:layer 1} x >= n; +{ + yield; + assert {:layer 1} x >= n; +} + +procedure {:yields} {:layer 1} p() +requires {:layer 1} x >= 5; +ensures {:layer 1} x >= 8; +{ + call yield_x(5); + call Incr(1); + call yield_x(6); + call Incr(1); + call yield_x(7); + call Incr(1); + call yield_x(8); +} + +procedure {:yields} {:layer 1} q() +{ + yield; + call Incr(3); + yield; +} + +procedure {:yields} {:layer 0,1} Incr(val: int); +ensures {:atomic} +|{A: + x := x + val; return true; +}|; diff --git a/Test/civl/Program2.bpl.expect b/Test/civl/Program2.bpl.expect new file mode 100644 index 00000000..5b2909f1 --- /dev/null +++ b/Test/civl/Program2.bpl.expect @@ -0,0 +1,2 @@ + +Boogie program verifier finished with 3 verified, 0 errors diff --git a/Test/civl/Program3.bpl b/Test/civl/Program3.bpl new file mode 100644 index 00000000..f8c4e132 --- /dev/null +++ b/Test/civl/Program3.bpl @@ -0,0 +1,36 @@ +// RUN: %boogie -noinfer -typeEncoding:m -useArrayTheory "%s" > "%t" +// RUN: %diff "%s.expect" "%t" +var {:layer 0,1} x:int; + +procedure {:yields} {:layer 1} yield_x() +ensures {:layer 1} x >= old(x); +{ + yield; + assert {:layer 1} x >= old(x); +} + +procedure {:yields} {:layer 1} p() +requires {:layer 1} x >= 5; +ensures {:layer 1} x >= 8; +{ + call yield_x(); + call Incr(1); + call yield_x(); + call Incr(1); + call yield_x(); + call Incr(1); + call yield_x(); +} + +procedure {:yields} {:layer 1} q() +{ + yield; + call Incr(3); + yield; +} + +procedure {:yields} {:layer 0,1} Incr(val: int); +ensures {:atomic} +|{A: + x := x + val; return true; +}|; diff --git a/Test/civl/Program3.bpl.expect b/Test/civl/Program3.bpl.expect new file mode 100644 index 00000000..5b2909f1 --- /dev/null +++ b/Test/civl/Program3.bpl.expect @@ -0,0 +1,2 @@ + +Boogie program verifier finished with 3 verified, 0 errors diff --git a/Test/civl/Program4.bpl b/Test/civl/Program4.bpl new file mode 100644 index 00000000..7f2f9c44 --- /dev/null +++ b/Test/civl/Program4.bpl @@ -0,0 +1,68 @@ +// RUN: %boogie -noinfer -typeEncoding:m -useArrayTheory "%s" > "%t" +// RUN: %diff "%s.expect" "%t" +type Tid; +var {:layer 0,1} a:[Tid]int; + +procedure {:yields} {:layer 1} main() { + var {:linear "tid"} tid:Tid; + + yield; + while (true) { + call tid := Allocate(); + async call P(tid); + yield; + } + yield; +} + +procedure {:yields} {:layer 1} P({:linear "tid"} tid: Tid) +ensures {:layer 1} a[tid] == old(a)[tid] + 1; +{ + var t:int; + + yield; + assert {:layer 1} a[tid] == old(a)[tid]; + call t := Read(tid); + yield; + assert {:layer 1} a[tid] == t; + call Write(tid, t + 1); + yield; + assert {:layer 1} a[tid] == t + 1; +} + +procedure {:yields} {:layer 1} Allocate() returns ({:linear "tid"} tid: Tid) +{ + yield; + call tid := AllocateLow(); + yield; +} + +procedure {:yields} {:layer 0,1} Read({:linear "tid"} tid: Tid) returns (val: int); +ensures {:atomic} +|{A: + val := a[tid]; return true; +}|; + +procedure {:yields} {:layer 0,1} Write({:linear "tid"} tid: Tid, val: int); +ensures {:atomic} +|{A: + a[tid] := val; return true; +}|; + +procedure {:yields} {:layer 0,1} AllocateLow() returns ({:linear "tid"} tid: Tid); +ensures {:atomic} |{ A: return true; }|; + + + +function {:builtin "MapConst"} MapConstBool(bool): [Tid]bool; +function {:builtin "MapOr"} MapOr([Tid]bool, [Tid]bool) : [Tid]bool; + +function {:inline} {:linear "tid"} TidCollector(x: Tid) : [Tid]bool +{ + MapConstBool(false)[x := true] +} +function {:inline} {:linear "tid"} TidSetCollector(x: [Tid]bool) : [Tid]bool +{ + x +} + diff --git a/Test/civl/Program4.bpl.expect b/Test/civl/Program4.bpl.expect new file mode 100644 index 00000000..5b2909f1 --- /dev/null +++ b/Test/civl/Program4.bpl.expect @@ -0,0 +1,2 @@ + +Boogie program verifier finished with 3 verified, 0 errors diff --git a/Test/civl/Program5.bpl b/Test/civl/Program5.bpl new file mode 100644 index 00000000..7ede3124 --- /dev/null +++ b/Test/civl/Program5.bpl @@ -0,0 +1,79 @@ +// RUN: %boogie -noinfer -typeEncoding:m -useArrayTheory "%s" > "%t" +// RUN: %diff "%s.expect" "%t" +type Tid; +const unique nil: Tid; + +function {:inline} UNALLOC():int { 0 } +function {:inline} WHITE():int { 1 } +function {:inline} GRAY():int { 2 } +function {:inline} BLACK():int { 3 } +function {:inline} Unalloc(i:int) returns(bool) { i <= 0 } +function {:inline} White(i:int) returns(bool) { i == 1 } +function {:inline} Gray(i:int) returns(bool) { i == 2 } +function {:inline} Black(i:int) returns(bool) { i >= 3 } + +procedure {:yields} {:layer 2} YieldColorOnlyGetsDarker() +ensures {:layer 2} Color >= old(Color); +{ + yield; + assert {:layer 2} Color >= old(Color); +} + +procedure {:yields} {:layer 2,3} WriteBarrier({:linear "tid"} tid:Tid) +ensures {:atomic} |{ A: assert tid != nil; goto B, C; + B: assume White(Color); Color := GRAY(); return true; + C: return true;}|; +{ + var colorLocal:int; + yield; + call colorLocal := GetColorNoLock(); + call YieldColorOnlyGetsDarker(); + if (White(colorLocal)) { call WriteBarrierSlow(tid); } + yield; +} + +procedure {:yields} {:layer 1,2} WriteBarrierSlow({:linear "tid"} tid:Tid) +ensures {:atomic} |{ A: assert tid != nil; goto B, C; + B: assume White(Color); Color := GRAY(); return true; + C: return true; }|; +{ + var colorLocal:int; + yield; + call AcquireLock(tid); + call colorLocal := GetColorLocked(tid); + if (White(colorLocal)) { call SetColorLocked(tid, GRAY()); } + call ReleaseLock(tid); + yield; +} + +procedure {:yields} {:layer 0,1} AcquireLock({:linear "tid"} tid: Tid); + ensures {:right} |{ A: assert tid != nil; assume lock == nil; lock := tid; return true; }|; + +procedure {:yields} {:layer 0,1} ReleaseLock({:linear "tid"} tid: Tid); + ensures {:left} |{ A: assert tid != nil; assert lock == tid; lock := nil; return true; }|; + +procedure {:yields} {:layer 0,1} SetColorLocked({:linear "tid"} tid:Tid, newCol:int); + ensures {:atomic} |{A: assert tid != nil; assert lock == tid; Color := newCol; return true;}|; + +procedure {:yields} {:layer 0,1} GetColorLocked({:linear "tid"} tid:Tid) returns (col:int); + ensures {:both} |{A: assert tid != nil; assert lock == tid; col := Color; return true;}|; + +procedure {:yields} {:layer 0,2} GetColorNoLock() returns (col:int); + ensures {:atomic} |{A: col := Color; return true;}|; + + + +function {:builtin "MapConst"} MapConstBool(bool): [Tid]bool; +function {:builtin "MapOr"} MapOr([Tid]bool, [Tid]bool) : [Tid]bool; + +var {:layer 0} Color:int; +var {:layer 0} lock:Tid; + +function {:inline} {:linear "tid"} TidCollector(x: Tid) : [Tid]bool +{ + MapConstBool(false)[x := true] +} +function {:inline} {:linear "tid"} TidSetCollector(x: [Tid]bool) : [Tid]bool +{ + x +} diff --git a/Test/civl/Program5.bpl.expect b/Test/civl/Program5.bpl.expect new file mode 100644 index 00000000..d7c0ff95 --- /dev/null +++ b/Test/civl/Program5.bpl.expect @@ -0,0 +1,2 @@ + +Boogie program verifier finished with 18 verified, 0 errors diff --git a/Test/civl/akash.bpl b/Test/civl/akash.bpl new file mode 100644 index 00000000..c826b810 --- /dev/null +++ b/Test/civl/akash.bpl @@ -0,0 +1,106 @@ +// RUN: %boogie -noinfer -typeEncoding:m -useArrayTheory "%s" > "%t" +// RUN: %diff "%s.expect" "%t" +function {:builtin "MapConst"} mapconstbool(bool) : [int]bool; + +function {:builtin "MapConst"} MapConstBool(bool) : [int]bool; +function {:inline} {:linear "tid"} TidCollector(x: int) : [int]bool +{ + MapConstBool(false)[x := true] +} + +function {:inline} {:linear "1"} SetCollector1(x: [int]bool) : [int]bool +{ + x +} + +function {:inline} {:linear "2"} SetCollector2(x: [int]bool) : [int]bool +{ + x +} + +var {:layer 0,1} g: int; +var {:layer 0,1} h: int; + +procedure {:yields} {:layer 0,1} SetG(val:int); +ensures {:atomic} |{A: g := val; return true; }|; + +procedure {:yields} {:layer 0,1} SetH(val:int); +ensures {:atomic} |{A: h := val; return true; }|; + +procedure {:yields} {:layer 1} Allocate() returns ({:linear "tid"} xl: int) +ensures {:layer 1} xl != 0; +{ + yield; + call xl := AllocateLow(); + yield; +} + +procedure {:yields} {:layer 0,1} AllocateLow() returns ({:linear "tid"} xls: int); +ensures {:atomic} |{ A: assume xls != 0; return true; }|; + +procedure {:yields} {:layer 1} A({:linear_in "tid"} tid_in: int, {:linear_in "1"} x: [int]bool, {:linear_in "2"} y: [int]bool) returns ({:linear "tid"} tid_out: int) +requires {:layer 1} x == mapconstbool(true); +requires {:layer 1} y == mapconstbool(true); +{ + var {:linear "tid"} tid_child: int; + tid_out := tid_in; + + yield; + call SetG(0); + yield; + assert {:layer 1} g == 0 && x == mapconstbool(true); + + yield; + call tid_child := Allocate(); + async call B(tid_child, x); + + yield; + call SetH(0); + + yield; + assert {:layer 1} h == 0 && y == mapconstbool(true); + + yield; + call tid_child := Allocate(); + async call C(tid_child, y); + + yield; +} + +procedure {:yields} {:layer 1} B({:linear_in "tid"} tid_in: int, {:linear_in "1"} x_in: [int]bool) +requires {:layer 1} x_in != mapconstbool(false); +{ + var {:linear "tid"} tid_out: int; + var {:linear "1"} x: [int]bool; + tid_out := tid_in; + x := x_in; + + yield; + + call SetG(1); + + yield; + + call SetG(2); + + yield; +} + +procedure {:yields} {:layer 1} C({:linear_in "tid"} tid_in: int, {:linear_in "2"} y_in: [int]bool) +requires {:layer 1} y_in != mapconstbool(false); +{ + var {:linear "tid"} tid_out: int; + var {:linear "2"} y: [int]bool; + tid_out := tid_in; + y := y_in; + + yield; + + call SetH(1); + + yield; + + call SetH(2); + + yield; +} \ No newline at end of file diff --git a/Test/civl/akash.bpl.expect b/Test/civl/akash.bpl.expect new file mode 100644 index 00000000..fef5ddc0 --- /dev/null +++ b/Test/civl/akash.bpl.expect @@ -0,0 +1,2 @@ + +Boogie program verifier finished with 4 verified, 0 errors diff --git a/Test/civl/bar.bpl b/Test/civl/bar.bpl new file mode 100644 index 00000000..4eef8378 --- /dev/null +++ b/Test/civl/bar.bpl @@ -0,0 +1,57 @@ +// RUN: %boogie -noinfer "%s" > "%t" +// RUN: %diff "%s.expect" "%t" +var {:layer 0,1} g:int; + +procedure {:yields} {:layer 1} PB() +{ + yield; + call Incr(); + yield; +} + +procedure {:yields} {:layer 0,1} Incr(); +ensures {:atomic} +|{A: + g := g + 1; return true; +}|; + +procedure {:yields} {:layer 0,1} Set(v: int); +ensures {:atomic} +|{A: + g := v; return true; +}|; + +procedure {:yields} {:layer 1} PC() +ensures {:layer 1} g == old(g); +{ + yield; + assert {:layer 1} g == old(g); +} + +procedure {:yields} {:layer 1} PE() +{ + call PC(); +} + +procedure {:yields} {:layer 1} PD() +{ + yield; + call Set(3); + call PC(); + assert {:layer 1} g == 3; +} + +procedure {:yields} {:layer 1} Main2() +{ + yield; + while (*) + { + async call PB(); + yield; + async call PE(); + yield; + async call PD(); + yield; + } + yield; +} diff --git a/Test/civl/bar.bpl.expect b/Test/civl/bar.bpl.expect new file mode 100644 index 00000000..8999ae7f --- /dev/null +++ b/Test/civl/bar.bpl.expect @@ -0,0 +1,13 @@ +bar.bpl(28,3): Error: Non-interference check failed +Execution trace: + bar.bpl(7,3): anon0 + (0,0): anon00 + bar.bpl(14,3): inline$Incr_1$0$this_A + (0,0): inline$Impl_YieldChecker_PC_1$0$L0 +bar.bpl(28,3): Error: Non-interference check failed +Execution trace: + bar.bpl(38,3): anon0 + (0,0): anon00 + (0,0): inline$Impl_YieldChecker_PC_1$0$L0 + +Boogie program verifier finished with 3 verified, 2 errors diff --git a/Test/civl/chris.bpl b/Test/civl/chris.bpl new file mode 100644 index 00000000..b54292ef --- /dev/null +++ b/Test/civl/chris.bpl @@ -0,0 +1,28 @@ +// RUN: %boogie -noinfer -typeEncoding:m -useArrayTheory "%s" > "%t" +// RUN: %diff "%s.expect" "%t" +var{:layer 1} x:int; + +procedure{:yields}{:layer 2} Havoc() + ensures{:atomic} |{ A: return true; }|; +{ + yield; +} + +procedure{:yields}{:layer 1} Recover() + ensures{:atomic} |{ A: assert x == 5; return true; }|; +{ + yield; +} + +procedure{:yields}{:layer 3} P() + ensures{:atomic} |{ A: return true; }|; + requires{:layer 2,3} x == 5; + ensures {:layer 2,3} x == 5; +{ + + yield; assert{:layer 2,3} x == 5; + call Havoc(); + yield; assert{:layer 3} x == 5; + call Recover(); + yield; assert{:layer 2,3} x == 5; +} diff --git a/Test/civl/chris.bpl.expect b/Test/civl/chris.bpl.expect new file mode 100644 index 00000000..be6b95ba --- /dev/null +++ b/Test/civl/chris.bpl.expect @@ -0,0 +1,2 @@ + +Boogie program verifier finished with 6 verified, 0 errors diff --git a/Test/civl/chris2.bpl b/Test/civl/chris2.bpl new file mode 100644 index 00000000..73f112ed --- /dev/null +++ b/Test/civl/chris2.bpl @@ -0,0 +1,34 @@ +// RUN: %boogie -noinfer -typeEncoding:m -useArrayTheory "%s" > "%t" +// RUN: %diff "%s.expect" "%t" +var{:layer 20} x:int; + +procedure{:yields}{:layer 20,25} p_gt1_lower(); + ensures{:both} + |{ + A: + x := x + 1; + return true; + }|; + +procedure{:yields}{:layer 25,40} p_gt1() + ensures{:both} + |{ + A: + x := x + 1; + return true; + }|; +{ + yield; + call p_gt1_lower(); + yield; +} + +procedure{:yields}{:layer 20,40} p_gt2(); + ensures{:both} + |{ + A: + assert x == 0; + return true; + }|; + + diff --git a/Test/civl/chris2.bpl.expect b/Test/civl/chris2.bpl.expect new file mode 100644 index 00000000..2bf339f7 --- /dev/null +++ b/Test/civl/chris2.bpl.expect @@ -0,0 +1,18 @@ +(0,0): Error BP5003: A postcondition might not hold on this return path. +chris2.bpl(30,5): Related location: Gate not preserved by p_gt1_lower +Execution trace: + (0,0): this_A +(0,0): Error BP5003: A postcondition might not hold on this return path. +(0,0): Related location: Gate failure of p_gt2 not preserved by p_gt1_lower +Execution trace: + (0,0): this_A +(0,0): Error BP5003: A postcondition might not hold on this return path. +chris2.bpl(30,5): Related location: Gate not preserved by p_gt1 +Execution trace: + (0,0): this_A +(0,0): Error BP5003: A postcondition might not hold on this return path. +(0,0): Related location: Gate failure of p_gt2 not preserved by p_gt1 +Execution trace: + (0,0): this_A + +Boogie program verifier finished with 1 verified, 4 errors diff --git a/Test/civl/civl-paper.bpl b/Test/civl/civl-paper.bpl new file mode 100644 index 00000000..a7042c6a --- /dev/null +++ b/Test/civl/civl-paper.bpl @@ -0,0 +1,175 @@ +// RUN: %boogie -noinfer -typeEncoding:m -useArrayTheory "%s" > "%t" +// RUN: %diff "%s.expect" "%t" +type X; +const nil: X; + +function {:builtin "MapConst"} MapConstBool(bool) : [X]bool; +function {:inline} {:linear "tid"} TidCollector(x: X) : [X]bool +{ + MapConstBool(false)[x := true] +} + +type lmap; +function {:linear "mem"} dom(lmap): [int]bool; +function map(lmap): [int]int; +function cons([int]bool, [int]int) : lmap; +axiom (forall x: [int]bool, y: [int]int :: {cons(x,y)} dom(cons(x, y)) == x && map(cons(x,y)) == y); + +var {:layer 0,3} {:linear "mem"} g: lmap; +var {:layer 0,3} lock: X; +var {:layer 0,1} b: bool; + +const p: int; + +procedure {:yields} {:layer 1} Yield1() +requires {:layer 1} InvLock(lock, b); +ensures {:layer 1} InvLock(lock, b); +{ + yield; + assert {:layer 1} InvLock(lock, b); +} + +function {:inline} InvLock(lock: X, b: bool) : bool +{ + lock != nil <==> b +} + +procedure {:yields} {:layer 2} Yield2() +{ + yield; +} + +procedure {:yields} {:layer 3} Yield3() +requires {:layer 3} Inv(g); +ensures {:layer 3} Inv(g); +{ + yield; + assert {:layer 3} Inv(g); +} + +function {:inline} Inv(g: lmap) : bool +{ + dom(g)[p] && dom(g)[p+4] && map(g)[p] == map(g)[p+4] +} + +procedure {:yields} {:layer 3} P({:linear "tid"} tid: X) +requires {:layer 1} tid != nil && InvLock(lock, b); +ensures {:layer 1} InvLock(lock, b); +requires {:layer 3} tid != nil && Inv(g); +ensures {:layer 3} Inv(g); +{ + var t: int; + var {:linear "mem"} l: lmap; + + par Yield3() | Yield1(); + call AcquireProtected(tid); + call l := TransferFromGlobalProtected(tid); + call t := Load(l, p); + call l := Store(l, p, t+1); + call t := Load(l, p+4); + call l := Store(l, p+4, t+1); + call TransferToGlobalProtected(tid, l); + call ReleaseProtected(tid); + par Yield3() | Yield1(); +} + + +procedure {:yields} {:layer 2,3} TransferToGlobalProtected({:linear "tid"} tid: X, {:linear_in "mem"} l: lmap) +ensures {:both} |{ A: assert tid != nil && lock == tid; g := l; return true; }|; +requires {:layer 1} InvLock(lock, b); +ensures {:layer 1} InvLock(lock, b); +{ + par Yield1() | Yield2(); + call TransferToGlobal(tid, l); + par Yield1() | Yield2(); +} + +procedure {:yields} {:layer 2,3} TransferFromGlobalProtected({:linear "tid"} tid: X) returns ({:linear "mem"} l: lmap) +ensures {:both} |{ A: assert tid != nil && lock == tid; l := g; return true; }|; +requires {:layer 1} InvLock(lock, b); +ensures {:layer 1} InvLock(lock, b); +{ + par Yield1() | Yield2(); + call l := TransferFromGlobal(tid); + par Yield1() | Yield2(); +} + +procedure {:yields} {:layer 2,3} AcquireProtected({:linear "tid"} tid: X) +ensures {:right} |{ A: assert tid != nil; assume lock == nil; lock := tid; return true; }|; +requires {:layer 1} tid != nil && InvLock(lock, b); +ensures {:layer 1} InvLock(lock, b); +{ + par Yield1() | Yield2(); + call Acquire(tid); + par Yield1() | Yield2(); +} + +procedure {:yields} {:layer 2,3} ReleaseProtected({:linear "tid"} tid: X) +ensures {:left} |{ A: assert tid != nil && lock == tid; lock := nil; return true; }|; +requires {:layer 1} InvLock(lock, b); +ensures {:layer 1} InvLock(lock, b); +{ + par Yield1() | Yield2(); + call Release(tid); + par Yield1() | Yield2(); +} + +procedure {:yields} {:layer 1,2} Acquire({:linear "tid"} tid: X) +requires {:layer 1} tid != nil && InvLock(lock, b); +ensures {:layer 1} InvLock(lock, b); +ensures {:atomic} |{ A: assume lock == nil; lock := tid; return true; }|; +{ + var status: bool; + var tmp: X; + + par Yield1(); + L: + assert {:layer 1} InvLock(lock, b); + call status := CAS(tid, false, true); + par Yield1(); + goto A, B; + + A: + assume status; + par Yield1(); + return; + + B: + assume !status; + goto L; +} + +procedure {:yields} {:layer 1,2} Release({:linear "tid"} tid: X) +ensures {:atomic} |{ A: lock := nil; return true; }|; +requires {:layer 1} InvLock(lock, b); +ensures {:layer 1} InvLock(lock, b); +{ + par Yield1(); + call CLEAR(tid, false); + par Yield1(); +} + +procedure {:yields} {:layer 0,2} TransferToGlobal({:linear "tid"} tid: X, {:linear_in "mem"} l: lmap); +ensures {:atomic} |{ A: g := l; return true; }|; + +procedure {:yields} {:layer 0,2} TransferFromGlobal({:linear "tid"} tid: X) returns ({:linear "mem"} l: lmap); +ensures {:atomic} |{ A: l := g; return true; }|; + +procedure {:yields} {:layer 0,3} Load({:linear "mem"} l: lmap, a: int) returns (v: int); +ensures {:both} |{ A: v := map(l)[a]; return true; }|; + +procedure {:yields} {:layer 0,3} Store({:linear_in "mem"} l_in: lmap, a: int, v: int) returns ({:linear "mem"} l_out: lmap); +ensures {:both} |{ A: assume l_out == cons(dom(l_in), map(l_in)[a := v]); return true; }|; + +procedure {:yields} {:layer 0,1} CAS(tid: X, prev: bool, next: bool) returns (status: bool); +ensures {:atomic} |{ +A: goto B, C; +B: assume b == prev; b := next; status := true; lock := tid; return true; +C: status := false; return true; +}|; + +procedure {:yields} {:layer 0,1} CLEAR(tid: X, next: bool); +ensures {:atomic} |{ +A: b := next; lock := nil; return true; +}|; + diff --git a/Test/civl/civl-paper.bpl.expect b/Test/civl/civl-paper.bpl.expect new file mode 100644 index 00000000..4bcd03fb --- /dev/null +++ b/Test/civl/civl-paper.bpl.expect @@ -0,0 +1,2 @@ + +Boogie program verifier finished with 35 verified, 0 errors diff --git a/Test/civl/foo.bpl b/Test/civl/foo.bpl new file mode 100644 index 00000000..7eeab890 --- /dev/null +++ b/Test/civl/foo.bpl @@ -0,0 +1,57 @@ +// RUN: %boogie -noinfer "%s" > "%t" +// RUN: %diff "%s.expect" "%t" +var {:layer 0,1} g:int; + +procedure {:yields} {:layer 1} PB() +{ + yield; + call Incr(); + yield; +} + +procedure {:yields} {:layer 0,1} Incr(); +ensures {:atomic} +|{A: + g := g + 1; return true; +}|; + +procedure {:yields} {:layer 0,1} Set(v: int); +ensures {:atomic} +|{A: + g := v; return true; +}|; + +procedure {:yields} {:layer 1} PC() +ensures {:layer 1} g == 3; +{ + yield; + call Set(3); + yield; + assert {:layer 1} g == 3; +} + +procedure {:yields} {:layer 1} PE() +{ + call PC(); +} + +procedure {:yields} {:layer 1} PD() +{ + call PC(); + assert {:layer 1} g == 3; +} + +procedure {:yields} {:layer 1} Main() +{ + yield; + while (*) + { + async call PB(); + yield; + async call PE(); + yield; + async call PD(); + yield; + } + yield; +} diff --git a/Test/civl/foo.bpl.expect b/Test/civl/foo.bpl.expect new file mode 100644 index 00000000..0d9de9db --- /dev/null +++ b/Test/civl/foo.bpl.expect @@ -0,0 +1,8 @@ +foo.bpl(30,3): Error: Non-interference check failed +Execution trace: + foo.bpl(7,3): anon0 + (0,0): anon00 + foo.bpl(14,3): inline$Incr_1$0$this_A + (0,0): inline$Impl_YieldChecker_PC_1$0$L0 + +Boogie program verifier finished with 4 verified, 1 error diff --git a/Test/civl/ghost.bpl b/Test/civl/ghost.bpl new file mode 100644 index 00000000..74d16acf --- /dev/null +++ b/Test/civl/ghost.bpl @@ -0,0 +1,46 @@ +// RUN: %boogie -noinfer -typeEncoding:m -useArrayTheory "%s" > "%t" +// RUN: %diff "%s.expect" "%t" +var {:layer 0} x: int; + +procedure {:yields} {:layer 0,1} Incr(); +ensures {:right} |{ A: x := x + 1; return true; }|; + +procedure ghost(y: int) returns (z: int) +requires y == 1; +ensures z == 2; +{ + z := y + 1; +} + +procedure {:yields} {:layer 1,2} Incr2() +ensures {:right} |{ A: x := x + 2; return true; }|; +{ + var {:ghost} a: int; + var {:ghost} b: int; + + yield; + call a := ghost(1); + assert {:layer 1} a == 2; + par Incr() | Incr(); + yield; +} + +procedure ghost_0() returns (z: int) +ensures z == x; +{ + z := x; +} + +procedure {:yields} {:layer 1,2} Incr2_0() +ensures {:right} |{ A: x := x + 2; return true; }|; +{ + var {:ghost} a: int; + var {:ghost} b: int; + + yield; + call a := ghost_0(); + par Incr() | Incr(); + call b := ghost_0(); + assert {:layer 1} b == a + 2; + yield; +} diff --git a/Test/civl/ghost.bpl.expect b/Test/civl/ghost.bpl.expect new file mode 100644 index 00000000..9823d44a --- /dev/null +++ b/Test/civl/ghost.bpl.expect @@ -0,0 +1,2 @@ + +Boogie program verifier finished with 6 verified, 0 errors diff --git a/Test/civl/linear-set.bpl b/Test/civl/linear-set.bpl new file mode 100644 index 00000000..e481291a --- /dev/null +++ b/Test/civl/linear-set.bpl @@ -0,0 +1,105 @@ +// RUN: %boogie -noinfer -typeEncoding:m -useArrayTheory "%s" > "%t" +// RUN: %diff "%s.expect" "%t" +type X; +function {:builtin "MapConst"} MapConstInt(int) : [X]int; +function {:builtin "MapConst"} MapConstBool(bool) : [X]bool; +function {:builtin "MapOr"} MapOr([X]bool, [X]bool) : [X]bool; + +function {:inline} None() : [X]bool +{ + MapConstBool(false) +} + +function {:inline} All() : [X]bool +{ + MapConstBool(true) +} + +function {:inline} {:linear "x"} XCollector(xs: [X]bool) : [X]bool +{ + xs +} + +var {:layer 0,1} x: int; +var {:layer 0,1} l: [X]bool; + + +procedure {:yields} {:layer 1} Split({:linear_in "x"} xls: [X]bool) returns ({:linear "x"} xls1: [X]bool, {:linear "x"} xls2: [X]bool) +ensures {:layer 1} xls == MapOr(xls1, xls2) && xls1 != None() && xls2 != None(); +{ + yield; + call xls1, xls2 := SplitLow(xls); + yield; +} + +procedure {:yields} {:layer 1} Allocate() returns ({:linear "tid"} xls: [X]bool) +{ + yield; + call xls := AllocateLow(); + yield; +} + +procedure {:yields} {:layer 0,1} Set(v: int); +ensures {:atomic} |{A: x := v; return true; }|; + +procedure {:yields} {:layer 0,1} Lock(tidls: [X]bool); +ensures {:atomic} |{A: assume l == None(); l := tidls; return true; }|; + +procedure {:yields} {:layer 0,1} Unlock(); +ensures {:atomic} |{A: l := None(); return true; }|; + +procedure {:yields} {:layer 0,1} SplitLow({:linear_in "x"} xls: [X]bool) returns ({:linear "x"} xls1: [X]bool, {:linear "x"} xls2: [X]bool); +ensures {:atomic} |{ A: assume xls == MapOr(xls1, xls2) && xls1 != None() && xls2 != None(); return true; }|; + +procedure {:yields} {:layer 0,1} AllocateLow() returns ({:linear "tid"} xls: [X]bool); +ensures {:atomic} |{ A: return true; }|; + +procedure {:yields} {:layer 1} main({:linear_in "tid"} tidls': [X]bool, {:linear_in "x"} xls': [X]bool) +requires {:layer 1} tidls' != None() && xls' == All(); +{ + var {:linear "tid"} tidls: [X]bool; + var {:linear "x"} xls: [X]bool; + var {:linear "tid"} lsChild: [X]bool; + var {:linear "x"} xls1: [X]bool; + var {:linear "x"} xls2: [X]bool; + + tidls := tidls'; + xls := xls'; + yield; + call Set(42); + yield; + assert {:layer 1} xls == All(); + assert {:layer 1} x == 42; + call xls1, xls2 := Split(xls); + call lsChild := Allocate(); + assume (lsChild != None()); + yield; + async call thread(lsChild, xls1); + call lsChild := Allocate(); + assume (lsChild != None()); + yield; + async call thread(lsChild, xls2); + yield; +} + +procedure {:yields} {:layer 1} thread({:linear_in "tid"} tidls': [X]bool, {:linear_in "x"} xls': [X]bool) +requires {:layer 1} tidls' != None() && xls' != None(); +{ + var {:linear "x"} xls: [X]bool; + var {:linear "tid"} tidls: [X]bool; + + tidls := tidls'; + xls := xls'; + + yield; + call Lock(tidls); + yield; + assert {:layer 1} tidls != None() && xls != None(); + call Set(0); + yield; + assert {:layer 1} tidls != None() && xls != None(); + assert {:layer 1} x == 0; + assert {:layer 1} tidls != None() && xls != None(); + call Unlock(); + yield; +} diff --git a/Test/civl/linear-set.bpl.expect b/Test/civl/linear-set.bpl.expect new file mode 100644 index 00000000..fef5ddc0 --- /dev/null +++ b/Test/civl/linear-set.bpl.expect @@ -0,0 +1,2 @@ + +Boogie program verifier finished with 4 verified, 0 errors diff --git a/Test/civl/linear-set2.bpl b/Test/civl/linear-set2.bpl new file mode 100644 index 00000000..24d8a13a --- /dev/null +++ b/Test/civl/linear-set2.bpl @@ -0,0 +1,106 @@ +// RUN: %boogie -noinfer -typeEncoding:m -useArrayTheory "%s" > "%t" +// RUN: %diff "%s.expect" "%t" +type X; +function {:builtin "MapConst"} MapConstInt(int) : [X]int; +function {:builtin "MapConst"} MapConstBool(bool) : [X]bool; +function {:builtin "MapOr"} MapOr([X]bool, [X]bool) : [X]bool; + +function {:inline} None() : [X]bool +{ + MapConstBool(false) +} + +function {:inline} All() : [X]bool +{ + MapConstBool(true) +} + +function {:inline} {:linear "x"} XCollector(xs: [X]bool) : [X]bool +{ + xs +} + +var {:layer 0,1} x: int; +var {:layer 0,1} l: X; +const nil: X; + +procedure {:yields} {:layer 1} Split({:linear_in "x"} xls: [X]bool) returns ({:linear "x"} xls1: [X]bool, {:linear "x"} xls2: [X]bool) +ensures {:layer 1} xls == MapOr(xls1, xls2) && xls1 != None() && xls2 != None(); +{ + yield; + call xls1, xls2 := SplitLow(xls); + yield; +} + +procedure {:yields} {:layer 1} Allocate() returns ({:linear "tid"} xls: X) +ensures {:layer 1} xls != nil; +{ + yield; + call xls := AllocateLow(); + yield; +} + +procedure {:yields} {:layer 0,1} Set(v: int); +ensures {:atomic} |{A: x := v; return true; }|; + +procedure {:yields} {:layer 0,1} Lock(tidls: X); +ensures {:atomic} |{A: assume l == nil; l := tidls; return true; }|; + +procedure {:yields} {:layer 0,1} Unlock(); +ensures {:atomic} |{A: l := nil; return true; }|; + +procedure {:yields} {:layer 0,1} SplitLow({:linear_in "x"} xls: [X]bool) returns ({:linear "x"} xls1: [X]bool, {:linear "x"} xls2: [X]bool); +ensures {:atomic} |{ A: assume xls == MapOr(xls1, xls2) && xls1 != None() && xls2 != None(); return true; }|; + +procedure {:yields} {:layer 0,1} AllocateLow() returns ({:linear "tid"} xls: X); +ensures {:atomic} |{ A: assume xls != nil; return true; }|; + +procedure {:yields} {:layer 1} main({:linear_in "tid"} tidls': X, {:linear_in "x"} xls': [X]bool) +requires {:layer 1} tidls' != nil && xls' == All(); +{ + var {:linear "tid"} tidls: X; + var {:linear "x"} xls: [X]bool; + var {:linear "tid"} lsChild: X; + var {:linear "x"} xls1: [X]bool; + var {:linear "x"} xls2: [X]bool; + + tidls := tidls'; + xls := xls'; + + yield; + call Set(42); + yield; + assert {:layer 1} xls == All(); + assert {:layer 1} x == 42; + call xls1, xls2 := Split(xls); + call lsChild := Allocate(); + yield; + async call thread(lsChild, xls1); + call lsChild := Allocate(); + yield; + async call thread(lsChild, xls2); + yield; +} + +procedure {:yields} {:layer 1} thread({:linear_in "tid"} tidls': X, {:linear_in "x"} xls': [X]bool) +requires {:layer 1} tidls' != nil && xls' != None(); +{ + var {:linear "x"} xls: [X]bool; + var {:linear "tid"} tidls: X; + + tidls := tidls'; + xls := xls'; + + yield; + call Lock(tidls); + yield; + assert {:layer 1} tidls != nil && xls != None(); + call Set(0); + yield; + assert {:layer 1} tidls != nil && xls != None(); + assert {:layer 1} x == 0; + yield; + assert {:layer 1} tidls != nil && xls != None(); + call Unlock(); + yield; +} diff --git a/Test/civl/linear-set2.bpl.expect b/Test/civl/linear-set2.bpl.expect new file mode 100644 index 00000000..fef5ddc0 --- /dev/null +++ b/Test/civl/linear-set2.bpl.expect @@ -0,0 +1,2 @@ + +Boogie program verifier finished with 4 verified, 0 errors diff --git a/Test/civl/lock-introduced.bpl b/Test/civl/lock-introduced.bpl new file mode 100644 index 00000000..c9650215 --- /dev/null +++ b/Test/civl/lock-introduced.bpl @@ -0,0 +1,100 @@ +// RUN: %boogie -noinfer -typeEncoding:m -useArrayTheory "%s" > "%t" +// RUN: %diff "%s.expect" "%t" +function {:builtin "MapConst"} MapConstBool(bool) : [X]bool; +function {:inline} {:linear "tid"} TidCollector(x: X) : [X]bool +{ + MapConstBool(false)[x := true] +} + +type X; +const nil: X; +var {:layer 0,2} b: bool; +var {:layer 1,3} lock: X; + +procedure {:yields} {:layer 3} Customer({:linear "tid"} tid: X) +requires {:layer 2} tid != nil; +requires {:layer 2} InvLock(lock, b); +ensures {:layer 2} InvLock(lock, b); +{ + yield; + assert {:layer 2} InvLock(lock, b); + while (*) + invariant {:layer 2} InvLock(lock, b); + { + call Enter(tid); + call Leave(tid); + yield; + assert {:layer 2} InvLock(lock, b); + } + yield; + assert {:layer 2} InvLock(lock, b); +} + +function {:inline} InvLock(lock: X, b: bool) : bool +{ + lock != nil <==> b +} + +procedure {:yields} {:layer 2,3} Enter({:linear "tid"} tid: X) +requires {:layer 2} tid != nil; +requires {:layer 2} InvLock(lock, b); +ensures {:layer 2} InvLock(lock, b); +ensures {:right} |{ A: assume lock == nil && tid != nil; lock := tid; return true; }|; +{ + yield; + assert {:layer 2} InvLock(lock, b); + call LowerEnter(tid); + yield; + assert {:layer 2} InvLock(lock, b); +} + +procedure {:yields} {:layer 2,3} Leave({:linear "tid"} tid:X) +requires {:layer 2} InvLock(lock, b); +ensures {:layer 2} InvLock(lock, b); +ensures {:atomic} |{ A: assert lock == tid && tid != nil; lock := nil; return true; }|; +{ + yield; + assert {:layer 2} InvLock(lock, b); + call LowerLeave(); + yield; + assert {:layer 2} InvLock(lock, b); +} + +procedure {:yields} {:layer 1,2} LowerEnter({:linear "tid"} tid: X) +ensures {:atomic} |{ A: assume !b; b := true; lock := tid; return true; }|; +{ + var status: bool; + yield; + L: + call status := CAS(false, true); + yield; + goto A, B; + + A: + assume status; + yield; + return; + + B: + assume !status; + goto L; +} + +procedure {:yields} {:layer 1,2} LowerLeave() +ensures {:atomic} |{ A: b := false; lock := nil; return true; }|; +{ + yield; + call SET(false); + yield; +} + +procedure {:yields} {:layer 0,1} CAS(prev: bool, next: bool) returns (status: bool); +ensures {:atomic} |{ +A: goto B, C; +B: assume b == prev; b := next; status := true; return true; +C: status := false; return true; +}|; + +procedure {:yields} {:layer 0,1} SET(next: bool); +ensures {:atomic} |{ A: b := next; return true; }|; + diff --git a/Test/civl/lock-introduced.bpl.expect b/Test/civl/lock-introduced.bpl.expect new file mode 100644 index 00000000..f62a8f46 --- /dev/null +++ b/Test/civl/lock-introduced.bpl.expect @@ -0,0 +1,2 @@ + +Boogie program verifier finished with 12 verified, 0 errors diff --git a/Test/civl/lock.bpl b/Test/civl/lock.bpl new file mode 100644 index 00000000..9341591f --- /dev/null +++ b/Test/civl/lock.bpl @@ -0,0 +1,57 @@ +// RUN: %boogie -noinfer -typeEncoding:m -useArrayTheory "%s" > "%t" +// RUN: %diff "%s.expect" "%t" +var {:layer 0,2} b: bool; + +procedure {:yields} {:layer 2} main() +{ + yield; + while (*) + { + async call Customer(); + yield; + } + yield; +} + +procedure {:yields} {:layer 2} Customer() +{ + yield; + while (*) + { + call Enter(); + yield; + call Leave(); + yield; + } + yield; +} + +procedure {:yields} {:layer 1,2} Enter() +ensures {:atomic} |{ A: assume !b; b := true; return true; }|; +{ + var status: bool; + yield; + L: + call status := CAS(false, true); + yield; + goto A, B; + + A: + assume status; + yield; + return; + + B: + assume !status; + goto L; +} + +procedure {:yields} {:layer 0,2} CAS(prev: bool, next: bool) returns (status: bool); +ensures {:atomic} |{ +A: goto B, C; +B: assume b == prev; b := next; status := true; return true; +C: status := false; return true; +}|; + +procedure {:yields} {:layer 0,2} Leave(); +ensures {:atomic} |{ A: b := false; return true; }|; diff --git a/Test/civl/lock.bpl.expect b/Test/civl/lock.bpl.expect new file mode 100644 index 00000000..05d394c7 --- /dev/null +++ b/Test/civl/lock.bpl.expect @@ -0,0 +1,2 @@ + +Boogie program verifier finished with 5 verified, 0 errors diff --git a/Test/civl/lock2.bpl b/Test/civl/lock2.bpl new file mode 100644 index 00000000..4809a8f5 --- /dev/null +++ b/Test/civl/lock2.bpl @@ -0,0 +1,63 @@ +// RUN: %boogie -noinfer -typeEncoding:m -useArrayTheory "%s" > "%t" +// RUN: %diff "%s.expect" "%t" +var {:layer 0,2} b: int; + +procedure {:yields} {:layer 2} main() +{ + yield; + while (*) + { + async call Customer(); + yield; + } + yield; +} + +procedure {:yields} {:layer 2} Customer() +{ + yield; + while (*) + { + call Enter(); + yield; + call Leave(); + yield; + } + yield; +} + +procedure {:yields} {:layer 1,2} Enter() +ensures {:atomic} |{ A: assume b == 0; b := 1; return true; }|; +{ + var _old, curr: int; + yield; + while (true) { + call _old := CAS(0, 1); + yield; + if (_old == 0) { + break; + } + while (true) { + call curr := Read(); + yield; + if (curr == 0) { + break; + } + } + yield; + } + yield; +} + +procedure {:yields} {:layer 0,2} Read() returns (val: int); +ensures {:atomic} |{ A: val := b; return true; }|; + +procedure {:yields} {:layer 0,2} CAS(prev: int, next: int) returns (_old: int); +ensures {:atomic} |{ +A: _old := b; goto B, C; +B: assume _old == prev; b := next; return true; +C: assume _old != prev; return true; +}|; + +procedure {:yields} {:layer 0,2} Leave(); +ensures {:atomic} |{ A: b := 0; return true; }|; diff --git a/Test/civl/lock2.bpl.expect b/Test/civl/lock2.bpl.expect new file mode 100644 index 00000000..05d394c7 --- /dev/null +++ b/Test/civl/lock2.bpl.expect @@ -0,0 +1,2 @@ + +Boogie program verifier finished with 5 verified, 0 errors diff --git a/Test/civl/multiset.bpl b/Test/civl/multiset.bpl new file mode 100644 index 00000000..7fb0a081 --- /dev/null +++ b/Test/civl/multiset.bpl @@ -0,0 +1,324 @@ +// RUN: %boogie -noinfer -typeEncoding:m -useArrayTheory "%s" > "%t" +// RUN: %diff "%s.expect" "%t" +type X; + +const unique null : int; +const unique nil: X; +const unique done: X; + +var {:layer 0} elt : [int]int; +var {:layer 0} valid : [int]bool; +var {:layer 0} lock : [int]X; +var {:layer 0} owner : [int]X; +const max : int; + +function {:builtin "MapConst"} MapConstBool(bool) : [X]bool; +function {:inline} {:linear "tid"} TidCollector(x: X) : [X]bool +{ + MapConstBool(false)[x := true] +} + +axiom (max > 0); + +procedure {:yields} {:layer 0} acquire(i : int, {:linear "tid"} tid: X); +ensures {:right} |{ A: + assert 0 <= i && i < max; + assert tid != nil && tid != done; + assume lock[i] == nil; + lock[i] := tid; + return true; + }|; + + +procedure {:yields} {:layer 0} release(i : int, {:linear "tid"} tid: X); +ensures {:left} |{ A: + assert 0 <= i && i < max; + assert lock[i] == tid; + assert tid != nil && tid != done; + lock[i] := nil; + return true; + }|; + + +procedure {:yields} {:layer 0,1} getElt(j : int, {:linear "tid"} tid: X) returns (elt_j:int); +ensures {:both} |{ A: + assert 0 <= j && j < max; + assert lock[j] == tid; + assert tid != nil && tid != done; + elt_j := elt[j]; + return true; + }|; + + +procedure {:yields} {:layer 0,1} setElt(j : int, x : int, {:linear "tid"} tid: X); +ensures {:both} |{ A: + assert x != null; + assert owner[j] == nil; + assert 0 <= j && j < max; + assert lock[j] == tid; + assert tid != nil && tid != done; + elt[j] := x; + owner[j] := tid; + return true; + }|; + + +procedure {:yields} {:layer 0,2} setEltToNull(j : int, {:linear "tid"} tid: X); +ensures {:left} |{ A: + assert owner[j] == tid; + assert 0 <= j && j < max; + assert lock[j] == tid; + assert !valid[j]; + assert tid != nil && tid != done; + elt[j] := null; + owner[j] := nil; + return true; + }|; + +procedure {:yields} {:layer 0,2} setValid(j : int, {:linear "tid"} tid: X); +ensures {:both} |{ A: + assert 0 <= j && j < max; + assert lock[j] == tid; + assert tid != nil && tid != done; + assert owner[j] == tid; + valid[j] := true; + owner[j] := done; + return true; + }|; + +procedure {:yields} {:layer 0,2} isEltThereAndValid(j : int, x : int, {:linear "tid"} tid: X) returns (fnd:bool); +ensures {:both} |{ A: + assert 0 <= j && j < max; + assert lock[j] == tid; + assert tid != nil && tid != done; + fnd := (elt[j] == x) && valid[j]; + return true; + }|; + +procedure {:yields} {:layer 1,2} FindSlot(x : int, {:linear "tid"} tid: X) returns (r : int) +requires {:layer 1} Inv(valid, elt, owner) && x != null && tid != nil && tid != done; +ensures {:layer 1} Inv(valid, elt, owner); +ensures {:right} |{ A: assert tid != nil && tid != done; + assert x != null; + goto B, C; + B: assume (0 <= r && r < max); + assume elt[r] == null; + assume owner[r] == nil; + assume !valid[r]; + elt[r] := x; + owner[r] := tid; + return true; + C: assume (r == -1); return true; + }|; +{ + var j : int; + var elt_j : int; + + par Yield1(); + + j := 0; + while(j < max) + invariant {:layer 1} Inv(valid, elt, owner); + invariant {:layer 1} 0 <= j; + { + call acquire(j, tid); + call elt_j := getElt(j, tid); + if(elt_j == null) + { + call setElt(j, x, tid); + call release(j, tid); + r := j; + + par Yield1(); + return; + } + call release(j,tid); + + par Yield1(); + + j := j + 1; + } + r := -1; + + par Yield1(); + return; +} + +procedure {:yields} {:layer 2} Insert(x : int, {:linear "tid"} tid: X) returns (result : bool) +requires {:layer 1} Inv(valid, elt, owner) && x != null && tid != nil && tid != done; +ensures {:layer 1} Inv(valid, elt, owner); +requires {:layer 2} Inv(valid, elt, owner) && x != null && tid != nil && tid != done; +ensures {:layer 2} Inv(valid, elt, owner); +ensures {:atomic} |{ var r:int; + A: goto B, C; + B: assume (0 <= r && r < max); + assume valid[r] == false; + assume elt[r] == null; + assume owner[r] == nil; + elt[r] := x; valid[r] := true; owner[r] := done; + result := true; return true; + C: result := false; return true; + }|; + { + var i: int; + par Yield12(); + call i := FindSlot(x, tid); + + if(i == -1) + { + result := false; + par Yield12(); + return; + } + par Yield1(); + assert {:layer 1} i != -1; + assert {:layer 2} i != -1; + call acquire(i, tid); + assert {:layer 2} elt[i] == x; + assert {:layer 2} valid[i] == false; + call setValid(i, tid); + call release(i, tid); + result := true; + par Yield12(); + return; +} + +procedure {:yields} {:layer 2} InsertPair(x : int, y : int, {:linear "tid"} tid: X) returns (result : bool) +requires {:layer 1} Inv(valid, elt, owner) && x != null && y != null && tid != nil && tid != done; +ensures {:layer 1} Inv(valid, elt, owner); +requires {:layer 2} Inv(valid, elt, owner) && x != null && y != null && tid != nil && tid != done; +ensures {:layer 2} Inv(valid, elt, owner); +ensures {:atomic} |{ var rx:int; + var ry:int; + A: goto B, C; + B: assume (0 <= rx && rx < max && 0 <= ry && ry < max && rx != ry); + assume valid[rx] == false; + assume valid[ry] == false; + assume elt[rx] == null; + assume elt[rx] == null; + elt[rx] := x; + elt[ry] := y; + valid[rx] := true; + valid[ry] := true; + owner[rx] := done; + owner[ry] := done; + result := true; return true; + C: result := false; return true; + }|; + { + var i : int; + var j : int; + par Yield12(); + + call i := FindSlot(x, tid); + + if (i == -1) + { + result := false; + par Yield12(); + return; + } + + par Yield1(); + call j := FindSlot(y, tid); + + if(j == -1) + { + par Yield1(); + call acquire(i,tid); + call setEltToNull(i, tid); + call release(i,tid); + result := false; + par Yield12(); + return; + } + + par Yield1(); + assert {:layer 2} i != -1 && j != -1; + call acquire(i, tid); + call acquire(j, tid); + assert {:layer 2} elt[i] == x; + assert {:layer 2} elt[j] == y; + assert {:layer 2} valid[i] == false; + assert {:layer 2} valid[j] == false; + call setValid(i, tid); + call setValid(j, tid); + call release(j, tid); + call release(i, tid); + result := true; + par Yield12(); + return; +} + +procedure {:yields} {:layer 2} LookUp(x : int, {:linear "tid"} tid: X, old_valid:[int]bool, old_elt:[int]int) returns (found : bool) +requires {:layer 1} {:layer 2} old_valid == valid && old_elt == elt; +requires {:layer 1} {:layer 2} Inv(valid, elt, owner); +requires {:layer 1} {:layer 2} (tid != nil && tid != done); +ensures {:layer 1} {:layer 2} Inv(valid, elt, owner); +ensures {:atomic} |{ A: assert tid != nil && tid != done; + assert x != null; + assume found ==> (exists ii:int :: 0 <= ii && ii < max && valid[ii] && elt[ii] == x); + assume !found ==> (forall ii:int :: 0 <= ii && ii < max ==> !(old_valid[ii] && old_elt[ii] == x)); + return true; + }|; +{ + var j : int; + var isThere : bool; + + par Yield12() | YieldLookUp(old_valid, old_elt); + + j := 0; + + while(j < max) + invariant {:layer 1} {:layer 2} Inv(valid, elt, owner); + invariant {:layer 1} {:layer 2} (forall ii:int :: 0 <= ii && ii < j ==> !(old_valid[ii] && old_elt[ii] == x)); + invariant {:layer 1} {:layer 2} (forall ii:int :: 0 <= ii && ii < max && old_valid[ii] ==> valid[ii] && old_elt[ii] == elt[ii]); + invariant {:layer 1} {:layer 2} 0 <= j; + { + call acquire(j, tid); + call isThere := isEltThereAndValid(j, x, tid); + if(isThere) + { + call release(j, tid); + found := true; + par Yield12() | YieldLookUp(old_valid, old_elt); + return; + } + call release(j,tid); + par Yield12() | YieldLookUp(old_valid, old_elt); + j := j + 1; + } + found := false; + + par Yield12() | YieldLookUp(old_valid, old_elt); + return; +} + +procedure {:yields} {:layer 1} Yield1() +requires {:layer 1} Inv(valid, elt, owner); +ensures {:layer 1} Inv(valid, elt, owner); +{ + yield; + assert {:layer 1} Inv(valid, elt, owner); +} + +procedure {:yields} {:layer 2} Yield12() +requires {:layer 1} {:layer 2} Inv(valid, elt, owner); +ensures {:layer 1} {:layer 2} Inv(valid, elt, owner); +{ + yield; + assert {:layer 1} {:layer 2} Inv(valid, elt, owner); +} + +function {:inline} Inv(valid: [int]bool, elt: [int]int, owner: [int]X): (bool) +{ + (forall i:int :: 0 <= i && i < max ==> (elt[i] == null <==> (!valid[i] && owner[i] == nil))) +} + +procedure {:yields} {:layer 2} YieldLookUp(old_valid: [int]bool, old_elt: [int]int) +requires {:layer 1} {:layer 2} (forall ii:int :: 0 <= ii && ii < max && old_valid[ii] ==> valid[ii] && old_elt[ii] == elt[ii]); +ensures {:layer 1} {:layer 2} (forall ii:int :: 0 <= ii && ii < max && old_valid[ii] ==> valid[ii] && old_elt[ii] == elt[ii]); +{ + yield; + assert {:layer 1} {:layer 2} (forall ii:int :: 0 <= ii && ii < max && old_valid[ii] ==> valid[ii] && old_elt[ii] == elt[ii]); +} diff --git a/Test/civl/multiset.bpl.expect b/Test/civl/multiset.bpl.expect new file mode 100644 index 00000000..d72077a6 --- /dev/null +++ b/Test/civl/multiset.bpl.expect @@ -0,0 +1,2 @@ + +Boogie program verifier finished with 78 verified, 0 errors diff --git a/Test/civl/new1.bpl b/Test/civl/new1.bpl new file mode 100644 index 00000000..b80b6315 --- /dev/null +++ b/Test/civl/new1.bpl @@ -0,0 +1,42 @@ +// RUN: %boogie -noinfer -typeEncoding:m -useArrayTheory "%s" > "%t" +// RUN: %diff "%s.expect" "%t" +function {:builtin "MapConst"} mapconstbool(x:bool): [int]bool; + +var {:layer 0,1} g:int; + +function {:inline} {:linear "Perm"} SetCollectorPerm(x: [int]bool) : [int]bool +{ + x +} + +procedure {:yields} {:layer 1} PB({:linear_in "Perm"} permVar_in:[int]bool) +requires {:layer 1} permVar_in[0] && g == 0; +{ + var {:linear "Perm"} permVar_out: [int]bool; + permVar_out := permVar_in; + + yield; + assert {:layer 1} permVar_out[0]; + assert {:layer 1} g == 0; + + call IncrG(); + + yield; + assert {:layer 1} permVar_out[0]; + assert {:layer 1} g == 1; +} + +procedure {:yields} {:layer 1} Main({:linear_in "Perm"} Permissions: [int]bool) +requires {:layer 1} Permissions == mapconstbool(true); +{ + yield; + call SetG(0); + async call PB(Permissions); + yield; +} + +procedure {:yields} {:layer 0,1} SetG(val:int); +ensures {:atomic} |{A: g := val; return true; }|; + +procedure {:yields} {:layer 0,1} IncrG(); +ensures {:atomic} |{A: g := g + 1; return true; }|; diff --git a/Test/civl/new1.bpl.expect b/Test/civl/new1.bpl.expect new file mode 100644 index 00000000..3de74d3e --- /dev/null +++ b/Test/civl/new1.bpl.expect @@ -0,0 +1,2 @@ + +Boogie program verifier finished with 2 verified, 0 errors diff --git a/Test/civl/one.bpl b/Test/civl/one.bpl new file mode 100644 index 00000000..663b2da0 --- /dev/null +++ b/Test/civl/one.bpl @@ -0,0 +1,18 @@ +// RUN: %boogie -noinfer "%s" > "%t" +// RUN: %diff "%s.expect" "%t" +var {:layer 0,1} x:int; + +procedure {:yields} {:layer 0,1} Set(v: int); +ensures {:atomic} +|{A: + x := v; return true; +}|; + +procedure {:yields} {:layer 1} B() +{ + yield; + call Set(5); + yield; + assert {:layer 1} x == 5; +} + diff --git a/Test/civl/one.bpl.expect b/Test/civl/one.bpl.expect new file mode 100644 index 00000000..6abb715b --- /dev/null +++ b/Test/civl/one.bpl.expect @@ -0,0 +1,2 @@ + +Boogie program verifier finished with 1 verified, 0 errors diff --git a/Test/civl/par-incr.bpl b/Test/civl/par-incr.bpl new file mode 100644 index 00000000..7be8f561 --- /dev/null +++ b/Test/civl/par-incr.bpl @@ -0,0 +1,31 @@ +// RUN: %boogie -noinfer -typeEncoding:m -useArrayTheory "%s" > "%t" +// RUN: %diff "%s.expect" "%t" + +var {:layer 0} x: int; + +procedure {:yields} {:layer 0,1} Incr(); +ensures {:right} |{ A: x := x + 1; return true; }|; + +procedure {:yields} {:layer 1,2} Incr2() +ensures {:right} |{ A: x := x + 2; return true; }|; +{ + yield; + par Incr() | Incr(); + yield; +} + +procedure {:yields} {:layer 1} Yield() +{ + yield; +} + +procedure {:yields} {:layer 2,3} Incr4() +ensures {:atomic} |{ A: x := x + 4; return true; }|; +{ + yield; + par Incr2() | Incr2() | Yield(); + yield; +} + + + diff --git a/Test/civl/par-incr.bpl.expect b/Test/civl/par-incr.bpl.expect new file mode 100644 index 00000000..00ddb38b --- /dev/null +++ b/Test/civl/par-incr.bpl.expect @@ -0,0 +1,2 @@ + +Boogie program verifier finished with 4 verified, 0 errors diff --git a/Test/civl/parallel1.bpl b/Test/civl/parallel1.bpl new file mode 100644 index 00000000..20dd3c79 --- /dev/null +++ b/Test/civl/parallel1.bpl @@ -0,0 +1,48 @@ +// RUN: %boogie -noinfer "%s" > "%t" +// RUN: %diff "%s.expect" "%t" +var {:layer 0,1} g:int; + +procedure {:yields} {:layer 1} PB() +{ + yield; + call Incr(); + yield; +} + +procedure {:yields} {:layer 0,1} Incr(); +ensures {:atomic} +|{A: + g := g + 1; return true; +}|; + +procedure {:yields} {:layer 0,1} Set(v: int); +ensures {:atomic} +|{A: + g := v; return true; +}|; + +procedure {:yields} {:layer 1} PC() +ensures {:layer 1} g == 3; +{ + yield; + call Set(3); + yield; + assert {:layer 1} g == 3; +} + +procedure {:yields} {:layer 1} PD() +{ + call PC(); + assert {:layer 1} g == 3; + yield; +} + +procedure {:yields} {:layer 1} Main() +{ + yield; + while (*) + { + par PB() | PC() | PD(); + } + yield; +} diff --git a/Test/civl/parallel1.bpl.expect b/Test/civl/parallel1.bpl.expect new file mode 100644 index 00000000..588c9c5b --- /dev/null +++ b/Test/civl/parallel1.bpl.expect @@ -0,0 +1,8 @@ +parallel1.bpl(30,3): Error: Non-interference check failed +Execution trace: + parallel1.bpl(7,3): anon0 + (0,0): anon00 + parallel1.bpl(14,3): inline$Incr_1$0$this_A + (0,0): inline$Impl_YieldChecker_PC_1$0$L0 + +Boogie program verifier finished with 3 verified, 1 error diff --git a/Test/civl/parallel2.bpl b/Test/civl/parallel2.bpl new file mode 100644 index 00000000..c28edf2b --- /dev/null +++ b/Test/civl/parallel2.bpl @@ -0,0 +1,59 @@ +// RUN: %boogie -noinfer -typeEncoding:m -useArrayTheory "%s" > "%t" +// RUN: %diff "%s.expect" "%t" +var {:layer 0,1} a:[int]int; + +function {:builtin "MapConst"} MapConstBool(bool) : [int]bool; +function {:inline} {:linear "tid"} TidCollector(x: int) : [int]bool +{ + MapConstBool(false)[x := true] +} + +procedure {:yields} {:layer 1} Allocate() returns ({:linear "tid"} tid: int) +{ + yield; + call tid := AllocateLow(); + yield; +} + +procedure {:yields} {:layer 0,1} Write(idx: int, val: int); +ensures {:atomic} |{A: a[idx] := val; return true; }|; + +procedure {:yields} {:layer 1} main() +{ + var {:linear "tid"} i: int; + var {:linear "tid"} j: int; + call i := Allocate(); + call j := Allocate(); + par i := t(i) | j := t(j); + par i := u(i) | j := u(j); +} + +procedure {:yields} {:layer 1} t({:linear_in "tid"} i': int) returns ({:linear "tid"} i: int) +{ + i := i'; + + yield; + call Write(i, 42); + call Yield(i); + assert {:layer 1} a[i] == 42; +} + +procedure {:yields} {:layer 1} u({:linear_in "tid"} i': int) returns ({:linear "tid"} i: int) +{ + i := i'; + + yield; + call Write(i, 42); + yield; + assert {:layer 1} a[i] == 42; +} + +procedure {:yields} {:layer 1} Yield({:linear "tid"} i: int) +ensures {:layer 1} old(a)[i] == a[i]; +{ + yield; + assert {:layer 1} old(a)[i] == a[i]; +} + +procedure {:yields} {:layer 0,1} AllocateLow() returns ({:linear "tid"} tid: int); +ensures {:atomic} |{ A: return true; }|; diff --git a/Test/civl/parallel2.bpl.expect b/Test/civl/parallel2.bpl.expect new file mode 100644 index 00000000..05d394c7 --- /dev/null +++ b/Test/civl/parallel2.bpl.expect @@ -0,0 +1,2 @@ + +Boogie program verifier finished with 5 verified, 0 errors diff --git a/Test/civl/parallel4.bpl b/Test/civl/parallel4.bpl new file mode 100644 index 00000000..f06ff4b8 --- /dev/null +++ b/Test/civl/parallel4.bpl @@ -0,0 +1,45 @@ +// RUN: %boogie -noinfer -typeEncoding:m -useArrayTheory "%s" > "%t" +// RUN: %diff "%s.expect" "%t" +var {:layer 0,1} a:int; + +procedure {:yields} {:layer 1} Allocate() returns ({:linear "tid"} tid: int) +{ + yield; + call tid := AllocateLow(); + yield; +} + +function {:builtin "MapConst"} MapConstBool(bool) : [int]bool; +function {:inline} {:linear "tid"} TidCollector(x: int) : [int]bool +{ + MapConstBool(false)[x := true] +} + +procedure {:yields} {:layer 1} main() +{ + var {:linear "tid"} i: int; + var {:linear "tid"} j: int; + call i := Allocate(); + call j := Allocate(); + par i := t(i) | j := t(j); +} + +procedure {:yields} {:layer 1} t({:linear_in "tid"} i': int) returns ({:linear "tid"} i: int) +{ + i := i'; + call Yield(); + assert {:layer 1} a == old(a); + call Incr(); + yield; +} + +procedure {:yields} {:layer 0,1} Incr(); +ensures {:atomic} |{A: a := a + 1; return true; }|; + +procedure {:yields} {:layer 1} Yield() +{ + yield; +} + +procedure {:yields} {:layer 0,1} AllocateLow() returns ({:linear "tid"} tid: int); +ensures {:atomic} |{ A: return true; }|; diff --git a/Test/civl/parallel4.bpl.expect b/Test/civl/parallel4.bpl.expect new file mode 100644 index 00000000..25ad398c --- /dev/null +++ b/Test/civl/parallel4.bpl.expect @@ -0,0 +1,6 @@ +parallel4.bpl(31,3): Error BP5001: This assertion might not hold. +Execution trace: + parallel4.bpl(29,5): anon0 + (0,0): anon01 + +Boogie program verifier finished with 3 verified, 1 error diff --git a/Test/civl/parallel5.bpl b/Test/civl/parallel5.bpl new file mode 100644 index 00000000..87afc888 --- /dev/null +++ b/Test/civl/parallel5.bpl @@ -0,0 +1,59 @@ +// RUN: %boogie -noinfer -typeEncoding:m -useArrayTheory "%s" > "%t" +// RUN: %diff "%s.expect" "%t" +var {:layer 0,1} a:[int]int; + +procedure {:yields} {:layer 1} Allocate() returns ({:linear "tid"} tid: int) +{ + yield; + call tid := AllocateLow(); + yield; +} + +function {:builtin "MapConst"} MapConstBool(bool) : [int]bool; +function {:inline} {:linear "tid"} TidCollector(x: int) : [int]bool +{ + MapConstBool(false)[x := true] +} + +procedure {:yields} {:layer 0,1} Write(idx: int, val: int); +ensures {:atomic} |{A: a[idx] := val; return true; }|; + +procedure {:yields} {:layer 1} main() +{ + var {:linear "tid"} i: int; + var {:linear "tid"} j: int; + call i := Allocate(); + call j := Allocate(); + par i := t(i) | Yield(j); + par i := u(i) | j := u(j); +} + +procedure {:yields} {:layer 1} t({:linear_in "tid"} i': int) returns ({:linear "tid"} i: int) +{ + i := i'; + + yield; + call Write(i, 42); + call Yield(i); + assert {:layer 1} a[i] == 42; +} + +procedure {:yields} {:layer 1} u({:linear_in "tid"} i': int) returns ({:linear "tid"} i: int) +{ + i := i'; + + yield; + call Write(i, 42); + yield; + assert {:layer 1} a[i] == 42; +} + +procedure {:yields} {:layer 1} Yield({:linear "tid"} i: int) +ensures {:layer 1} old(a)[i] == a[i]; +{ + yield; + assert {:layer 1} old(a)[i] == a[i]; +} + +procedure {:yields} {:layer 0,1} AllocateLow() returns ({:linear "tid"} tid: int); +ensures {:atomic} |{ A: return true; }|; diff --git a/Test/civl/parallel5.bpl.expect b/Test/civl/parallel5.bpl.expect new file mode 100644 index 00000000..05d394c7 --- /dev/null +++ b/Test/civl/parallel5.bpl.expect @@ -0,0 +1,2 @@ + +Boogie program verifier finished with 5 verified, 0 errors diff --git a/Test/civl/perm.bpl b/Test/civl/perm.bpl new file mode 100644 index 00000000..5bc75324 --- /dev/null +++ b/Test/civl/perm.bpl @@ -0,0 +1,49 @@ +// RUN: %boogie -noinfer -typeEncoding:m -useArrayTheory "%s" > "%t" +// RUN: %diff "%s.expect" "%t" +var {:layer 0,1} x: int; +function {:builtin "MapConst"} ch_mapconstbool(x: bool) : [int]bool; + +function {:builtin "MapOr"} ch_mapunion(x: [int]bool, y: [int]bool) : [int]bool; + +function {:inline} {:linear "Perm"} SetCollectorPerm(x: [int]bool) : [int]bool +{ + x +} + +procedure {:yields} {:layer 1} mainE({:linear_in "Perm"} permVar_in: [int]bool) + requires {:layer 1} permVar_in == ch_mapconstbool(true); + requires {:layer 1} x == 0; +{ + var {:linear "Perm"} permVar_out: [int]bool; + + permVar_out := permVar_in; + + yield; + assert {:layer 1} x == 0; + assert {:layer 1} permVar_out == ch_mapconstbool(true); + + async call foo(permVar_out); + yield; +} + +procedure {:yields} {:layer 1} foo({:linear_in "Perm"} permVar_in: [int]bool) + requires {:layer 1} permVar_in != ch_mapconstbool(false); + requires {:layer 1} permVar_in[1]; + requires {:layer 1} x == 0; +{ + var {:linear "Perm"} permVar_out: [int]bool; + permVar_out := permVar_in; + + yield; + assert {:layer 1} permVar_out[1]; + assert {:layer 1} x == 0; + + call Incr(); + + yield; + assert {:layer 1} permVar_out[1]; + assert {:layer 1} x == 1; +} + +procedure {:yields} {:layer 0,1} Incr(); +ensures {:atomic} |{A: x := x + 1; return true; }|; \ No newline at end of file diff --git a/Test/civl/perm.bpl.expect b/Test/civl/perm.bpl.expect new file mode 100644 index 00000000..3de74d3e --- /dev/null +++ b/Test/civl/perm.bpl.expect @@ -0,0 +1,2 @@ + +Boogie program verifier finished with 2 verified, 0 errors diff --git a/Test/civl/t1.bpl b/Test/civl/t1.bpl new file mode 100644 index 00000000..675b3842 --- /dev/null +++ b/Test/civl/t1.bpl @@ -0,0 +1,103 @@ +// RUN: %boogie -noinfer -typeEncoding:m -useArrayTheory "%s" > "%t" +// RUN: %diff "%s.expect" "%t" +function {:builtin "MapConst"} mapconstbool(bool) : [int]bool; + +function {:builtin "MapConst"} MapConstBool(bool) : [int]bool; +function {:inline} {:linear "tid"} TidCollector(x: int) : [int]bool +{ + MapConstBool(false)[x := true] +} + +function {:inline} {:linear "1"} SetCollector1(x: [int]bool) : [int]bool +{ + x +} + +function {:inline} {:linear "2"} SetCollector2(x: [int]bool) : [int]bool +{ + x +} + +var {:layer 0,1} g: int; +var {:layer 0,1} h: int; + +procedure {:yields} {:layer 0,1} SetG(val:int); +ensures {:atomic} |{A: g := val; return true; }|; + +procedure {:yields} {:layer 0,1} SetH(val:int); +ensures {:atomic} |{A: h := val; return true; }|; + +procedure {:yields} {:layer 1} Yield({:linear "1"} x: [int]bool) +requires {:layer 1} x == mapconstbool(true) && g == 0; +ensures {:layer 1} x == mapconstbool(true) && g == 0; +{ + yield; + assert {:layer 1} x == mapconstbool(true) && g == 0; +} + +procedure {:yields} {:layer 1} Allocate() returns ({:linear "tid"} xl: int) +ensures {:layer 1} xl != 0; +{ + yield; + call xl := AllocateLow(); + yield; +} + +procedure {:yields} {:layer 0,1} AllocateLow() returns ({:linear "tid"} xls: int); +ensures {:atomic} |{ A: assume xls != 0; return true; }|; + +procedure {:yields} {:layer 1} A({:linear_in "tid"} tid_in: int, {:linear_in "1"} x: [int]bool, {:linear_in "2"} y: [int]bool) returns ({:linear "tid"} tid_out: int) +requires {:layer 1} x == mapconstbool(true); +requires {:layer 1} y == mapconstbool(true); +{ + var {:linear "tid"} tid_child: int; + tid_out := tid_in; + + yield; + call SetG(0); + + par tid_child := Allocate() | Yield(x); + + async call B(tid_child, x); + + yield; + assert {:layer 1} x == mapconstbool(true); + assert {:layer 1} g == 0; + + call SetH(0); + + yield; + assert {:layer 1} h == 0 && y == mapconstbool(true); + + yield; + call tid_child := Allocate(); + async call C(tid_child, y); + + yield; +} + +procedure {:yields} {:layer 1} B({:linear_in "tid"} tid_in: int, {:linear_in "1"} x_in: [int]bool) +requires {:layer 1} x_in != mapconstbool(false); +{ + var {:linear "tid"} tid_out: int; + var {:linear "1"} x: [int]bool; + tid_out := tid_in; + x := x_in; + + yield; + call SetG(1); + yield; +} + +procedure {:yields} {:layer 1} C({:linear_in "tid"} tid_in: int, {:linear_in "2"} y_in: [int]bool) +requires {:layer 1} y_in != mapconstbool(false); +{ + var {:linear "tid"} tid_out: int; + var {:linear "2"} y: [int]bool; + tid_out := tid_in; + y := y_in; + + yield; + call SetH(1); + yield; +} diff --git a/Test/civl/t1.bpl.expect b/Test/civl/t1.bpl.expect new file mode 100644 index 00000000..0b0c936e --- /dev/null +++ b/Test/civl/t1.bpl.expect @@ -0,0 +1,9 @@ +t1.bpl(65,5): Error: Non-interference check failed +Execution trace: + t1.bpl(84,13): anon0 + (0,0): anon05 + (0,0): inline$SetG_1$0$Entry + t1.bpl(25,21): inline$SetG_1$0$this_A + (0,0): inline$Impl_YieldChecker_A_1$0$L1 + +Boogie program verifier finished with 4 verified, 1 error diff --git a/Test/civl/termination.bpl b/Test/civl/termination.bpl new file mode 100644 index 00000000..2d5542dd --- /dev/null +++ b/Test/civl/termination.bpl @@ -0,0 +1,18 @@ +// RUN: %boogie -noinfer -typeEncoding:m -useArrayTheory "%s" > "%t" +// RUN: %diff "%s.expect" "%t" +procedure {:yields} {:layer 0} X(); +ensures {:atomic} |{ A: return true; }|; + +procedure {:yields} {:layer 0} Y(); +ensures {:left} |{ A: return true; }|; + +procedure {:yields} {:layer 1} main() { + yield; + call X(); + while (*) + { + call Y(); + } + yield; + assert {:layer 1} true; +} diff --git a/Test/civl/termination.bpl.expect b/Test/civl/termination.bpl.expect new file mode 100644 index 00000000..d216a01d --- /dev/null +++ b/Test/civl/termination.bpl.expect @@ -0,0 +1,3 @@ +termination.bpl(9,31): Error: Implementation main fails simulation check C at layer 1. Transactions must be separated by a yield. + +1 type checking errors detected in termination.bpl diff --git a/Test/civl/termination2.bpl b/Test/civl/termination2.bpl new file mode 100644 index 00000000..840c27c1 --- /dev/null +++ b/Test/civl/termination2.bpl @@ -0,0 +1,19 @@ +// RUN: %boogie -noinfer -typeEncoding:m -useArrayTheory "%s" > "%t" +// RUN: %diff "%s.expect" "%t" +procedure {:yields} {:layer 0} X(); +ensures {:atomic} |{ A: return true; }|; + +procedure {:yields} {:layer 0} Y(); +ensures {:left} |{ A: return true; }|; + +procedure {:yields} {:layer 1} main() { + yield; + call X(); + while (*) + invariant {:terminates} {:layer 1} true; + { + call Y(); + } + yield; + assert {:layer 1} true; +} diff --git a/Test/civl/termination2.bpl.expect b/Test/civl/termination2.bpl.expect new file mode 100644 index 00000000..6abb715b --- /dev/null +++ b/Test/civl/termination2.bpl.expect @@ -0,0 +1,2 @@ + +Boogie program verifier finished with 1 verified, 0 errors diff --git a/Test/civl/ticket.bpl b/Test/civl/ticket.bpl new file mode 100644 index 00000000..91863e1a --- /dev/null +++ b/Test/civl/ticket.bpl @@ -0,0 +1,147 @@ +// RUN: %boogie -noinfer -typeEncoding:m -useArrayTheory "%s" > "%t" +// RUN: %diff "%s.expect" "%t" +function RightOpen(n: int) : [int]bool; +function RightClosed(n: int) : [int]bool; +axiom (forall x: int, y: int :: RightOpen(x)[y] <==> y < x); +axiom (forall x: int, y: int :: RightClosed(x)[y] <==> y <= x); + +type X; +function {:builtin "MapConst"} mapconstbool(bool): [X]bool; +const nil: X; +var {:layer 0,2} t: int; +var {:layer 0,2} s: int; +var {:layer 0,2} cs: X; +var {:layer 0,2} T: [int]bool; + +function {:builtin "MapConst"} MapConstBool(bool) : [X]bool; +function {:inline} {:linear "tid"} TidCollector(x: X) : [X]bool +{ + MapConstBool(false)[x := true] +} +function {:inline} {:linear "tid"} TidSetCollector(x: [X]bool) : [X]bool +{ + x +} + +function {:inline} Inv1(tickets: [int]bool, ticket: int): (bool) +{ + tickets == RightOpen(ticket) +} + +function {:inline} Inv2(tickets: [int]bool, ticket: int, lock: X): (bool) +{ + if (lock == nil) then tickets == RightOpen(ticket) else tickets == RightClosed(ticket) +} + +procedure {:yields} {:layer 2} Allocate({:linear_in "tid"} xls':[X]bool) returns ({:linear "tid"} xls: [X]bool, {:linear "tid"} xl: X) +ensures {:layer 1} {:layer 2} xl != nil; +{ + yield; + call xls, xl := AllocateLow(xls'); + yield; +} + +procedure {:yields} {:layer 2} main({:linear_in "tid"} xls':[X]bool) +requires {:layer 2} xls' == mapconstbool(true); +{ + var {:linear "tid"} tid: X; + var {:linear "tid"} xls: [X]bool; + + yield; + + call Init(xls'); + xls := xls'; + + par Yield1() | Yield2(); + + while (*) + invariant {:layer 1} Inv1(T, t); + invariant {:layer 2} Inv2(T, s, cs); + { + par xls, tid := Allocate(xls) | Yield1() | Yield2(); + async call Customer(tid); + par Yield1() | Yield2(); + } + par Yield1() | Yield2(); +} + +procedure {:yields} {:layer 2} Customer({:linear_in "tid"} tid: X) +requires {:layer 1} Inv1(T, t); +requires {:layer 2} tid != nil && Inv2(T, s, cs); +{ + par Yield1() | Yield2(); + while (*) + invariant {:layer 1} Inv1(T, t); + invariant {:layer 2} Inv2(T, s, cs); + { + call Enter(tid); + par Yield1() | Yield2() | YieldSpec(tid); + call Leave(tid); + par Yield1() | Yield2(); + } + par Yield1() | Yield2(); +} + +procedure {:yields} {:layer 2} Enter({:linear "tid"} tid: X) +requires {:layer 1} Inv1(T, t); +ensures {:layer 1} Inv1(T,t); +requires {:layer 2} tid != nil && Inv2(T, s, cs); +ensures {:layer 2} Inv2(T, s, cs) && cs == tid; +{ + var m: int; + + par Yield1() | Yield2(); + call m := GetTicketAbstract(tid); + par Yield1(); + call WaitAndEnter(tid, m); + par Yield1() | Yield2() | YieldSpec(tid); +} + +procedure {:yields} {:layer 1,2} GetTicketAbstract({:linear "tid"} tid: X) returns (m: int) +requires {:layer 1} Inv1(T, t); +ensures {:layer 1} Inv1(T, t); +ensures {:right} |{ A: havoc m, t; assume !T[m]; T[m] := true; return true; }|; +{ + par Yield1(); + call m := GetTicket(tid); + par Yield1(); +} + +procedure {:yields} {:layer 2} YieldSpec({:linear "tid"} tid: X) +requires {:layer 2} tid != nil && cs == tid; +ensures {:layer 2} cs == tid; +{ + yield; + assert {:layer 2} tid != nil && cs == tid; +} + +procedure {:yields} {:layer 2} Yield2() +requires {:layer 2} Inv2(T, s, cs); +ensures {:layer 2} Inv2(T, s, cs); +{ + yield; + assert {:layer 2} Inv2(T, s, cs); +} + +procedure {:yields} {:layer 1} Yield1() +requires {:layer 1} Inv1(T, t); +ensures {:layer 1} Inv1(T,t); +{ + yield; + assert {:layer 1} Inv1(T,t); +} + +procedure {:yields} {:layer 0,2} Init({:linear "tid"} xls:[X]bool); +ensures {:atomic} |{ A: assert xls == mapconstbool(true); cs := nil; t := 0; s := 0; T := RightOpen(0); return true; }|; + +procedure {:yields} {:layer 0,1} GetTicket({:linear "tid"} tid: X) returns (m: int); +ensures {:atomic} |{ A: m := t; t := t + 1; T[m] := true; return true; }|; + +procedure {:yields} {:layer 0,2} WaitAndEnter({:linear "tid"} tid: X, m:int); +ensures {:atomic} |{ A: assume m <= s; cs := tid; return true; }|; + +procedure {:yields} {:layer 0,2} Leave({:linear "tid"} tid: X); +ensures {:atomic} |{ A: s := s + 1; cs := nil; return true; }|; + +procedure {:yields} {:layer 0,2} AllocateLow({:linear_in "tid"} xls':[X]bool) returns ({:linear "tid"} xls: [X]bool, {:linear "tid"} xl: X); +ensures {:atomic} |{ A: assume xl != nil; return true; }|; diff --git a/Test/civl/ticket.bpl.expect b/Test/civl/ticket.bpl.expect new file mode 100644 index 00000000..28c26eab --- /dev/null +++ b/Test/civl/ticket.bpl.expect @@ -0,0 +1,2 @@ + +Boogie program verifier finished with 16 verified, 0 errors diff --git a/Test/civl/treiber-stack.bpl b/Test/civl/treiber-stack.bpl new file mode 100644 index 00000000..e1c509ab --- /dev/null +++ b/Test/civl/treiber-stack.bpl @@ -0,0 +1,202 @@ +// RUN: %boogie -noinfer -typeEncoding:m -useArrayTheory "%s" > "%t" +// RUN: %diff "%s.expect" "%t" +type Node = int; +const unique null: Node; +type lmap; +function {:linear "Node"} dom(lmap): [Node]bool; +function map(lmap): [Node]Node; +function {:builtin "MapConst"} MapConstBool(bool) : [Node]bool; + +function EmptyLmap(): (lmap); +axiom (dom(EmptyLmap()) == MapConstBool(false)); + +function Add(x: lmap, i: Node, v: Node): (lmap); +axiom (forall x: lmap, i: Node, v: Node :: dom(Add(x, i, v)) == dom(x)[i:=true] && map(Add(x, i, v)) == map(x)[i := v]); + +function Remove(x: lmap, i: Node): (lmap); +axiom (forall x: lmap, i: Node :: dom(Remove(x, i)) == dom(x)[i:=false] && map(Remove(x, i)) == map(x)); + +procedure {:yields} {:layer 0,1} ReadTopOfStack() returns (v:Node); +ensures {:right} |{ A: assume dom(Stack)[v] || dom(Used)[v]; return true; }|; + +procedure {:yields} {:layer 0,1} Load(i:Node) returns (v:Node); +ensures {:right} |{ A: assert dom(Stack)[i] || dom(Used)[i]; goto B,C; + B: assume dom(Stack)[i]; v := map(Stack)[i]; return true; + C: assume !dom(Stack)[i]; return true; }|; + +procedure {:yields} {:layer 0,1} Store({:linear_in "Node"} l_in:lmap, i:Node, v:Node) returns ({:linear "Node"} l_out:lmap); +ensures {:both} |{ A: assert dom(l_in)[i]; l_out := Add(l_in, i, v); return true; }|; + +procedure {:yields} {:layer 0,1} TransferToStack(oldVal: Node, newVal: Node, {:linear_in "Node"} l_in:lmap) returns (r: bool, {:linear "Node"} l_out:lmap); +ensures {:atomic} |{ A: assert dom(l_in)[newVal]; + goto B,C; + B: assume oldVal == TopOfStack; TopOfStack := newVal; l_out := EmptyLmap(); Stack := Add(Stack, newVal, map(l_in)[newVal]); r := true; return true; + C: assume oldVal != TopOfStack; l_out := l_in; r := false; return true; }|; + +procedure {:yields} {:layer 0,1} TransferFromStack(oldVal: Node, newVal: Node) returns (r: bool); +ensures {:atomic} |{ A: goto B,C; + B: assume oldVal == TopOfStack; TopOfStack := newVal; Used := Add(Used, oldVal, map(Stack)[oldVal]); Stack := Remove(Stack, oldVal); r := true; return true; + C: assume oldVal != TopOfStack; r := false; return true; }|; + +var {:layer 0} TopOfStack: Node; +var {:linear "Node"} {:layer 0} Stack: lmap; + + +function {:inline} Inv(TopOfStack: Node, Stack: lmap) : (bool) +{ + BetweenSet(map(Stack), TopOfStack, null)[TopOfStack] && + Subset(BetweenSet(map(Stack), TopOfStack, null), Union(Singleton(null), dom(Stack))) +} + +var {:linear "Node"} {:layer 0} Used: lmap; + +procedure {:yields} {:layer 1} push(x: Node, {:linear_in "Node"} x_lmap: lmap) +requires {:layer 1} dom(x_lmap)[x]; +requires {:layer 1} Inv(TopOfStack, Stack); +ensures {:layer 1} Inv(TopOfStack, Stack); +ensures {:atomic} |{ A: Stack := Add(Stack, x, TopOfStack); TopOfStack := x; return true; }|; +{ + var t: Node; + var g: bool; + var {:linear "Node"} t_lmap: lmap; + + yield; + assert {:layer 1} Inv(TopOfStack, Stack); + t_lmap := x_lmap; + while (true) + invariant {:layer 1} dom(t_lmap) == dom(x_lmap); + invariant {:layer 1} Inv(TopOfStack, Stack); + { + call t := ReadTopOfStack(); + call t_lmap := Store(t_lmap, x, t); + call g, t_lmap := TransferToStack(t, x, t_lmap); + if (g) { + assert {:layer 1} map(Stack)[x] == t; + break; + } + yield; + assert {:layer 1} dom(t_lmap) == dom(x_lmap); + assert {:layer 1} Inv(TopOfStack, Stack); + } + yield; + assert {:expand} {:layer 1} Inv(TopOfStack, Stack); +} + +procedure {:yields} {:layer 1} pop() +requires {:layer 1} Inv(TopOfStack, Stack); +ensures {:layer 1} Inv(TopOfStack, Stack); +ensures {:atomic} |{ var t: Node; + A: assume TopOfStack != null; t := TopOfStack; Used := Add(Used, t, map(Stack)[t]); TopOfStack := map(Stack)[t]; Stack := Remove(Stack, t); return true; }|; +{ + var g: bool; + var x: Node; + var t: Node; + + yield; + assert {:layer 1} Inv(TopOfStack, Stack); + while (true) + invariant {:layer 1} Inv(TopOfStack, Stack); + { + call t := ReadTopOfStack(); + if (t != null) { + call x := Load(t); + call g := TransferFromStack(t, x); + if (g) { + break; + } + } + yield; + assert {:layer 1} Inv(TopOfStack, Stack); + } + yield; + assert {:layer 1} Inv(TopOfStack, Stack); +} + +function Equal([int]bool, [int]bool) returns (bool); +function Subset([int]bool, [int]bool) returns (bool); + +function Empty() returns ([int]bool); +function Singleton(int) returns ([int]bool); +function Reachable([int,int]bool, int) returns ([int]bool); +function Union([int]bool, [int]bool) returns ([int]bool); + +axiom(forall x:int :: !Empty()[x]); + +axiom(forall x:int, y:int :: {Singleton(y)[x]} Singleton(y)[x] <==> x == y); +axiom(forall y:int :: {Singleton(y)} Singleton(y)[y]); + +axiom(forall x:int, S:[int]bool, T:[int]bool :: {Union(S,T)[x]}{Union(S,T),S[x]}{Union(S,T),T[x]} Union(S,T)[x] <==> S[x] || T[x]); + +axiom(forall S:[int]bool, T:[int]bool :: {Equal(S,T)} Equal(S,T) <==> Subset(S,T) && Subset(T,S)); +axiom(forall x:int, S:[int]bool, T:[int]bool :: {S[x],Subset(S,T)}{T[x],Subset(S,T)} S[x] && Subset(S,T) ==> T[x]); +axiom(forall S:[int]bool, T:[int]bool :: {Subset(S,T)} Subset(S,T) || (exists x:int :: S[x] && !T[x])); + +//////////////////// +// Between predicate +//////////////////// +function Between(f: [int]int, x: int, y: int, z: int) returns (bool); +function Avoiding(f: [int]int, x: int, y: int, z: int) returns (bool); + + +////////////////////////// +// Between set constructor +////////////////////////// +function BetweenSet(f: [int]int, x: int, z: int) returns ([int]bool); + +//////////////////////////////////////////////////// +// axioms relating Between and BetweenSet +//////////////////////////////////////////////////// +axiom(forall f: [int]int, x: int, y: int, z: int :: {BetweenSet(f, x, z)[y]} BetweenSet(f, x, z)[y] <==> Between(f, x, y, z)); +axiom(forall f: [int]int, x: int, y: int, z: int :: {Between(f, x, y, z), BetweenSet(f, x, z)} Between(f, x, y, z) ==> BetweenSet(f, x, z)[y]); +axiom(forall f: [int]int, x: int, z: int :: {BetweenSet(f, x, z)} Between(f, x, x, x)); +axiom(forall f: [int]int, x: int, z: int :: {BetweenSet(f, x, z)} Between(f, z, z, z)); + + +////////////////////////// +// Axioms for Between +////////////////////////// + +// reflexive +axiom(forall f: [int]int, x: int :: Between(f, x, x, x)); + +// step +axiom(forall f: [int]int, x: int, y: int, z: int, w:int :: {Between(f, y, z, w), f[x]} Between(f, x, f[x], f[x])); + +// reach +axiom(forall f: [int]int, x: int, y: int :: {f[x], Between(f, x, y, y)} Between(f, x, y, y) ==> x == y || Between(f, x, f[x], y)); + +// cycle +axiom(forall f: [int]int, x: int, y:int :: {f[x], Between(f, x, y, y)} f[x] == x && Between(f, x, y, y) ==> x == y); + +// sandwich +axiom(forall f: [int]int, x: int, y: int :: {Between(f, x, y, x)} Between(f, x, y, x) ==> x == y); + +// order1 +axiom(forall f: [int]int, x: int, y: int, z: int :: {Between(f, x, y, y), Between(f, x, z, z)} Between(f, x, y, y) && Between(f, x, z, z) ==> Between(f, x, y, z) || Between(f, x, z, y)); + +// order2 +axiom(forall f: [int]int, x: int, y: int, z: int :: {Between(f, x, y, z)} Between(f, x, y, z) ==> Between(f, x, y, y) && Between(f, y, z, z)); + +// transitive1 +axiom(forall f: [int]int, x: int, y: int, z: int :: {Between(f, x, y, y), Between(f, y, z, z)} Between(f, x, y, y) && Between(f, y, z, z) ==> Between(f, x, z, z)); + +// transitive2 +axiom(forall f: [int]int, x: int, y: int, z: int, w: int :: {Between(f, x, y, z), Between(f, y, w, z)} Between(f, x, y, z) && Between(f, y, w, z) ==> Between(f, x, y, w) && Between(f, x, w, z)); + +// transitive3 +axiom(forall f: [int]int, x: int, y: int, z: int, w: int :: {Between(f, x, y, z), Between(f, x, w, y)} Between(f, x, y, z) && Between(f, x, w, y) ==> Between(f, x, w, z) && Between(f, w, y, z)); + +// This axiom is required to deal with the incompleteness of the trigger for the reflexive axiom. +// It cannot be proved using the rest of the axioms. +axiom(forall f: [int]int, u:int, x: int :: {Between(f, u, x, x)} Between(f, u, x, x) ==> Between(f, u, u, x)); + +// relation between Avoiding and Between +axiom(forall f: [int]int, x: int, y: int, z: int :: {Avoiding(f, x, y, z)} Avoiding(f, x, y, z) <==> (Between(f, x, y, z) || (Between(f, x, y, y) && !Between(f, x, z, z)))); +axiom(forall f: [int]int, x: int, y: int, z: int :: {Between(f, x, y, z)} Between(f, x, y, z) <==> (Avoiding(f, x, y, z) && Avoiding(f, x, z, z))); + +// update +axiom(forall f: [int]int, u: int, v: int, x: int, p: int, q: int :: {Avoiding(f[p := q], u, v, x)} Avoiding(f[p := q], u, v, x) <==> ((Avoiding(f, u, v, p) && Avoiding(f, u, v, x)) || (Avoiding(f, u, p, x) && p != x && Avoiding(f, q, v, p) && Avoiding(f, q, v, x)))); + +axiom (forall f: [int]int, p: int, q: int, u: int, w: int :: {BetweenSet(f[p := q], u, w)} Avoiding(f, u, w, p) ==> Equal(BetweenSet(f[p := q], u, w), BetweenSet(f, u, w))); +axiom (forall f: [int]int, p: int, q: int, u: int, w: int :: {BetweenSet(f[p := q], u, w)} p != w && Avoiding(f, u, p, w) && Avoiding(f, q, w, p) ==> Equal(BetweenSet(f[p := q], u, w), Union(BetweenSet(f, u, p), BetweenSet(f, q, w)))); +axiom (forall f: [int]int, p: int, q: int, u: int, w: int :: {BetweenSet(f[p := q], u, w)} Avoiding(f, u, w, p) || (p != w && Avoiding(f, u, p, w) && Avoiding(f, q, w, p)) || Equal(BetweenSet(f[p := q], u, w), Empty())); \ No newline at end of file diff --git a/Test/civl/treiber-stack.bpl.expect b/Test/civl/treiber-stack.bpl.expect new file mode 100644 index 00000000..be6b95ba --- /dev/null +++ b/Test/civl/treiber-stack.bpl.expect @@ -0,0 +1,2 @@ + +Boogie program verifier finished with 6 verified, 0 errors diff --git a/Test/civl/wsq.bpl b/Test/civl/wsq.bpl new file mode 100644 index 00000000..f4964258 --- /dev/null +++ b/Test/civl/wsq.bpl @@ -0,0 +1,560 @@ +// RUN: %boogie -noinfer -typeEncoding:m -useArrayTheory "%s" > "%t" +// RUN: %diff "%s.expect" "%t" +type Tid; +const nil: Tid; + +function {:builtin "MapConst"} MapConstBool(bool) : [Tid]bool; +function {:inline} {:linear "tid"} TidCollector(x: Tid) : [Tid]bool +{ + MapConstBool(false)[x := true] +} + + + +var {:layer 0,3} H: int; +var {:layer 0,3} T: int; +var {:layer 0,3} items: [int]int; +var {:layer 0} status: [int]bool; +var {:layer 0,3} take_in_cs: bool; +var {:layer 0,3} put_in_cs: bool; +var {:layer 0,3} steal_in_cs: [Tid]bool; +var {:layer 0,3} h_ss: [Tid]int; +var {:layer 0,3} t_ss: [Tid]int; + +const IN_Q: bool; +const NOT_IN_Q: bool; +axiom IN_Q == true; +axiom NOT_IN_Q == false; + +const unique EMPTY: int; +const unique NIL: Tid; +const unique ptTid: Tid; +axiom ptTid != NIL; + +function {:inline} stealerTid(tid: Tid):(bool) { tid != NIL && tid != ptTid } + +function {:inline} ideasInv(put_in_cs:bool, + items:[int]int, + status: [int]bool, + H:int, T:int, + take_in_cs:bool, + steal_in_cs:[Tid]bool, + h_ss:[Tid]int, + t_ss:[Tid]int + ):(bool) +{ + ( + ( (take_in_cs) && h_ss[ptTid] < t_ss[ptTid] ==> (t_ss[ptTid] == T && H <= T && + items[T] != EMPTY && status[T] == IN_Q) ) && + (put_in_cs ==> !take_in_cs) && (take_in_cs ==> !put_in_cs) && + (( (take_in_cs) && H != h_ss[ptTid]) ==> H > h_ss[ptTid]) && + (forall td:Tid :: (stealerTid(td) && steal_in_cs[td] && H == h_ss[td] && H < t_ss[td]) ==> (items[H] != EMPTY && status[H] == IN_Q)) && + (forall td:Tid :: (stealerTid(td) && steal_in_cs[td] && H != h_ss[td]) ==> H > h_ss[td]) + ) +} + +function {:inline} queueInv(steal_in_cs:[Tid]bool, + put_in_cs:bool, + take_in_cs:bool, + items:[int]int, status: [int]bool, _H:int, _T:int):(bool) +{ + ( (forall i:int :: (_H <= i && i <= _T) ==> (status[i] == IN_Q && items[i] != EMPTY)) ) +} + +function {:inline} emptyInv(put_in_cs:bool, take_in_cs:bool, items:[int]int, status:[int]bool, T:int):(bool) +{ + (forall i:int :: (i>=T && !put_in_cs && !take_in_cs) ==> status[i] == NOT_IN_Q && items[i] == EMPTY) +} + +function {:inline} putInv(items:[int]int, status: [int]bool, H:int, T:int):(bool) +{ + (forall i:int :: (H <= i && i < T) ==> (status[i] == IN_Q && items[i] != EMPTY)) +} + +function {:inline} takeInv(items:[int]int, status: [int]bool, H:int, T:int, t:int, h:int):(bool) +{ + (forall i:int :: (h <= i && i <= t) ==> (status[i] == IN_Q && + items[i] != EMPTY) && + t == T + ) +} + +procedure {:yields} {:layer 3} put({:linear "tid"} tid:Tid, task: int) +requires {:layer 3} {:expand} queueInv(steal_in_cs,put_in_cs,take_in_cs,items, status, H, T-1) && tid == ptTid && task != EMPTY && !take_in_cs && !put_in_cs; +requires {:layer 3} {:expand} ideasInv(put_in_cs,items, status, H, T, take_in_cs, steal_in_cs, h_ss, t_ss); +requires {:layer 3} {:expand} emptyInv(put_in_cs, take_in_cs, items,status,T); +ensures {:layer 3} {:expand} queueInv(steal_in_cs,put_in_cs,take_in_cs,items, status, H, T-1) && tid == ptTid && !take_in_cs && !put_in_cs; +ensures {:layer 3} {:expand} ideasInv(put_in_cs,items, status, H, T, take_in_cs, steal_in_cs, h_ss, t_ss); +ensures {:layer 3} {:expand} emptyInv(put_in_cs, take_in_cs, items,status,T); +ensures {:atomic} |{ var i: int; A: assume status[i] == NOT_IN_Q; status[i] := IN_Q; return true; }|; +{ + var t: int; + var {:ghost} oldH:int; + var {:ghost} oldT:int; + var {:ghost} oldStatusT:bool; + + + oldH := H; + oldT := T; + yield; + assert {:layer 3} {:expand} queueInv(steal_in_cs,put_in_cs,take_in_cs,items, status, H, T-1) && tid == ptTid && !take_in_cs && !put_in_cs; + assert {:layer 3} {:expand} {:expand} ideasInv(put_in_cs,items, status, H, T, take_in_cs, steal_in_cs, h_ss, t_ss); + assert {:layer 3} oldH <= H && oldT == T; + assert {:layer 3} {:expand} emptyInv(put_in_cs, take_in_cs, items,status,T); + + call t := readT_put(tid); + + oldH := H; + oldT := T; + yield; + assert {:layer 3} {:expand} queueInv(steal_in_cs,put_in_cs,take_in_cs,items, status, H, T-1) && tid == ptTid && !take_in_cs && put_in_cs; + assert {:layer 3} {:expand} ideasInv(put_in_cs,items, status, H, T, take_in_cs, steal_in_cs, h_ss, t_ss); + assert {:layer 3} tid == ptTid && t == T; + assert {:layer 3} oldH <= H && oldT == T; + assert {:layer 3} (forall i:int :: i>=T ==> status[i] == NOT_IN_Q && items[i] == EMPTY); + + call writeItems_put(tid,t, task); + + oldH := H; + oldT := T; + oldStatusT := status[T]; + yield; + assert {:layer 3} {:expand} queueInv(steal_in_cs,put_in_cs,take_in_cs,items, status, H, T) && t == T && tid == ptTid && !take_in_cs && put_in_cs; + assert {:layer 3} {:expand} ideasInv(put_in_cs,items, status, H, T, take_in_cs, steal_in_cs, h_ss, t_ss); + assert {:layer 3} items[t] == task; + assert {:layer 3} oldH <= H && oldT == T; + assert {:layer 3} (forall i:int :: i>T ==> status[i] == NOT_IN_Q && items[i] == EMPTY); + + + call writeT_put(tid, t+1); + + oldH := H; + oldT := T; + yield; + assert {:layer 3} {:expand} queueInv(steal_in_cs,put_in_cs,take_in_cs,items, status, H, T-1) && tid == ptTid && !take_in_cs && !put_in_cs; + assert {:layer 3} {:expand} ideasInv(put_in_cs,items, status, H, T, take_in_cs, steal_in_cs, h_ss, t_ss); + assert {:layer 3} T == t + 1; + assert {:layer 3} oldH <= H && oldT == T; + assert {:layer 3} {:expand} emptyInv(put_in_cs, take_in_cs, items,status,T); +} + +procedure {:yields} {:layer 3} take({:linear "tid"} tid:Tid) returns (task: int, taskstatus: bool) +requires {:layer 3} {:expand} queueInv(steal_in_cs,put_in_cs,take_in_cs,items, status, H, T-1) && tid == ptTid && !take_in_cs && !put_in_cs; +requires {:layer 3} {:expand} ideasInv(put_in_cs,items, status, H, T, take_in_cs, steal_in_cs, h_ss, t_ss); +ensures {:layer 3} queueInv(steal_in_cs,put_in_cs,take_in_cs,items, status, H, T-1) && tid == ptTid && !take_in_cs && !put_in_cs && (task != EMPTY ==> taskstatus == IN_Q); +ensures {:layer 3} ideasInv(put_in_cs,items, status, H, T, take_in_cs, steal_in_cs, h_ss, t_ss); +ensures {:atomic} |{ var i: int; A: goto B,C; B: assume status[i] == IN_Q; status[i] := NOT_IN_Q; return true; C: return true;}|; +{ + var h, t: int; + var chk: bool; + var {:ghost} oldH:int; + var {:ghost} oldT:int; + + oldH := H; + oldT := T; + yield; + assert {:layer 3} queueInv(steal_in_cs,put_in_cs,take_in_cs,items, status, H, T-1) && tid == ptTid && !take_in_cs && !put_in_cs; + assert {:layer 3} ideasInv(put_in_cs,items, status, H, T, take_in_cs, steal_in_cs, h_ss, t_ss); + assert {:layer 3} oldH <= H && oldT == T; + + LOOP_ENTRY_1: + + while(true) + invariant {:layer 3} queueInv(steal_in_cs,put_in_cs,take_in_cs,items, status, H, T-1) && tid == ptTid && !take_in_cs && !put_in_cs; + invariant {:layer 3} ideasInv(put_in_cs,items, status, H, T, take_in_cs, steal_in_cs, h_ss, t_ss); + { + + oldH := H; + oldT := T; + yield; + assert {:layer 3} queueInv(steal_in_cs,put_in_cs,take_in_cs,items, status, H, T-1) && tid == ptTid && !take_in_cs && !put_in_cs; + assert {:layer 3} ideasInv(put_in_cs,items, status, H, T, take_in_cs, steal_in_cs, h_ss, t_ss); + assert {:layer 3} oldH <= H && oldT == T; + + call t := readT_take_init(tid); + + oldH := H; + oldT := T; + yield; + assert {:layer 3} queueInv(steal_in_cs,put_in_cs,take_in_cs,items, status, H, T-1) && tid == ptTid && !take_in_cs && !put_in_cs; + assert {:layer 3} ideasInv(put_in_cs,items, status, H, T, take_in_cs, steal_in_cs, h_ss, t_ss); + assert {:layer 3} t == T; + assert {:layer 3} items[t-1] == EMPTY ==> H > t-1; + assert {:layer 3} oldH <= H && oldT == T; + + t := t-1; + call writeT_take(tid, t); + + oldH := H; + oldT := T; + yield; + assert {:layer 3} queueInv(steal_in_cs,put_in_cs,take_in_cs,items, status, H, T) && tid == ptTid && !take_in_cs && !put_in_cs && t_ss[tid] == t; + assert {:layer 3} ideasInv(put_in_cs,items, status, H, T, take_in_cs, steal_in_cs, h_ss, t_ss); + assert {:layer 3} t == T; + assert {:layer 3} items[t] == EMPTY ==> H > t; + assert {:layer 3} oldH <= H && oldT == T; + + call h := readH_take(tid); + + oldH := H; + oldT := T; + yield; + assert {:layer 3} queueInv(steal_in_cs,put_in_cs,take_in_cs,items, status, H, T) && tid == ptTid && take_in_cs && !put_in_cs && h_ss[tid] == h && t_ss[tid] == t; + assert {:layer 3} {:expand} ideasInv(put_in_cs,items, status, H, T, take_in_cs, steal_in_cs, h_ss, t_ss); + assert {:layer 3} t == T; + assert {:layer 3} h <= H; + assert {:layer 3} items[t] == EMPTY ==> H > t; + assert {:layer 3} oldH <= H; + assert {:layer 3} oldT == T; + assert {:layer 3} h <= H; + assert {:layer 3} oldH == h; + + if(t= h; + assert {:layer 3} queueInv(steal_in_cs,put_in_cs,take_in_cs,items, status, H, T) && tid == ptTid && take_in_cs && h_ss[tid] == h && t_ss[tid] == t; + assert {:layer 3} ideasInv(put_in_cs,items, status, H, T, take_in_cs, steal_in_cs, h_ss, t_ss); + assert {:layer 3} t == T && task == items[T]; + assert {:layer 3} T > H ==> items[T] != EMPTY; + assert {:layer 3} oldH <= H && oldT == T && !put_in_cs && take_in_cs; + + if(t>h) { + call takeExitCS(tid); + + oldH := H; + oldT := T; + yield; + assert {:layer 3} queueInv(steal_in_cs,put_in_cs,take_in_cs,items, status, H, T-1) && tid == ptTid && !take_in_cs && h_ss[tid] == h && t_ss[tid] == t; + assert {:layer 3} ideasInv(put_in_cs,items, status, H, T, take_in_cs, steal_in_cs, h_ss, t_ss); + assert {:layer 3} t == T && task == items[t] && task != EMPTY && taskstatus == IN_Q; + assert {:layer 3} oldH <= H && oldT == T && !put_in_cs && !take_in_cs; + return; + } + call writeT_take_eq(tid, h+1); + oldH := H; + oldT := T; + + yield; + assert {:layer 3} queueInv(steal_in_cs,put_in_cs,take_in_cs,items, status, H, T-1) && tid == ptTid && h_ss[tid] == h && t_ss[tid] == t; + assert {:layer 3} ideasInv(put_in_cs,items, status, H, T, take_in_cs, steal_in_cs, h_ss, t_ss); + assert {:layer 3} T == h + 1; + assert {:layer 3} oldH <= H; + assert {:layer 3} oldT == T; + assert {:layer 3} task == items[t]; + assert {:layer 3} !put_in_cs; + + call chk := CAS_H_take(tid, h,h+1); + + + oldH := H; + oldT := T; + yield; + assert {:layer 3} chk ==> (h+1 == oldH && h_ss[tid] == oldH -1 && task != EMPTY); + assert {:layer 3} queueInv(steal_in_cs,put_in_cs,take_in_cs,items, status, H, T-1) && tid == ptTid && h_ss[tid] == h && t_ss[tid] == t; + assert {:layer 3} ideasInv(put_in_cs,items, status, H, T, take_in_cs, steal_in_cs, h_ss, t_ss); + assert {:layer 3} h+1 == T; + assert {:layer 3} task == items[t]; + assert {:layer 3} !take_in_cs; + assert {:layer 3} !put_in_cs; + assert {:layer 3} oldH <= H && oldT == T; + + if(!chk) { + + oldH := H; + oldT := T; + yield; + assert {:layer 3} queueInv(steal_in_cs,put_in_cs,take_in_cs,items, status, H, T-1) && tid == ptTid && h_ss[tid] == h && t_ss[tid] == t; + assert {:layer 3} ideasInv(put_in_cs,items, status, H, T, take_in_cs, steal_in_cs, h_ss, t_ss); + assert {:layer 3} h+1 == T && task == items[t] && !take_in_cs && !put_in_cs; + assert {:layer 3} oldH <= H && oldT == T; + + goto LOOP_ENTRY_1; + } + + oldH := H; + oldT := T; + yield; + assert {:layer 3} queueInv(steal_in_cs,put_in_cs,take_in_cs,items, status, H, T-1) && tid == ptTid && h_ss[tid] == h && t_ss[tid] == t; + assert {:layer 3} ideasInv(put_in_cs,items, status, H, T, take_in_cs, steal_in_cs, h_ss, t_ss); + assert {:layer 3} h+1 == T && task == items[t] && !take_in_cs && !put_in_cs; + assert {:layer 3} oldH <= H && oldT == T && task != EMPTY && taskstatus == IN_Q; + + return; + } + + oldH := H; + oldT := T; + yield; + assert {:layer 3} queueInv(steal_in_cs,put_in_cs,take_in_cs,items, status, H, T) && tid == ptTid && !put_in_cs; + assert {:layer 3} ideasInv(put_in_cs,items, status, H, T, take_in_cs, steal_in_cs, h_ss, t_ss); + assert {:layer 3} oldH <= H && oldT == T; + +} + + +procedure {:yields}{:layer 3} steal({:linear "tid"} tid:Tid) returns (task: int, taskstatus: bool) +requires {:layer 3} queueInv(steal_in_cs,put_in_cs,take_in_cs,items, status, H, T-1) && stealerTid(tid) && + !steal_in_cs[tid]; +requires {:layer 3} ideasInv(put_in_cs,items, status, H, T, take_in_cs, steal_in_cs, h_ss, t_ss); +ensures {:layer 3} queueInv(steal_in_cs,put_in_cs,take_in_cs,items, status, H, T-1) && + !steal_in_cs[tid] && (task != EMPTY ==> taskstatus == IN_Q); +ensures {:layer 3} ideasInv(put_in_cs,items, status, H, T, take_in_cs, steal_in_cs, h_ss, t_ss); +ensures {:atomic} |{ var i: int; A: goto B,C; B: assume status[i] == IN_Q; status[i] := NOT_IN_Q; return true; C: return true;}|; +{ + var h, t: int; + var chk: bool; + var {:ghost} oldH:int; + var {:ghost} oldT:int; + + oldH := H; + oldT := T; + yield; + assert {:layer 3} stealerTid(tid); + assert {:layer 3} queueInv(steal_in_cs,put_in_cs,take_in_cs,items, status, H, T-1); + assert {:layer 3} ideasInv(put_in_cs,items, status, H, T, take_in_cs, steal_in_cs, h_ss, t_ss); + assert {:layer 3} oldH <= H; + assert {:layer 3} !steal_in_cs[tid]; + + LOOP_ENTRY_2: + while(true) + invariant {:layer 3} stealerTid(tid); + invariant {:layer 3} queueInv(steal_in_cs,put_in_cs,take_in_cs,items, status, H, T-1); + invariant {:layer 3} ideasInv(put_in_cs,items, status, H, T, take_in_cs, steal_in_cs, h_ss, t_ss); + invariant {:layer 3} !steal_in_cs[tid]; + { + oldH := H; + oldT := T; + yield; + assert {:layer 3} stealerTid(tid); + assert {:layer 3} queueInv(steal_in_cs,put_in_cs,take_in_cs,items, status, H, T-1); + assert {:layer 3} ideasInv(put_in_cs,items, status, H, T, take_in_cs, steal_in_cs, h_ss, t_ss); + assert {:layer 3} oldH <= H; + assert {:layer 3} !steal_in_cs[tid]; + + call h := readH_steal(tid); + + oldH := H; + oldT := T; + yield; + assert {:layer 3} H >= h; + assert {:layer 3} !steal_in_cs[tid]; + assert {:layer 3} h_ss[tid] == h; + assert {:layer 3} queueInv(steal_in_cs,put_in_cs,take_in_cs,items, status, H, T-1); + assert {:layer 3} {:expand} ideasInv(put_in_cs,items, status, H, T, take_in_cs, steal_in_cs, h_ss, t_ss); + assert {:layer 3} oldH <= H; + + call t := readT_steal(tid); + + + oldH := H; + oldT := T; + yield; + assert {:layer 3} steal_in_cs[tid]; + assert {:layer 3} stealerTid(tid) && H >= h && steal_in_cs[tid] && h_ss[tid] == h; + assert {:layer 3} queueInv(steal_in_cs,put_in_cs,take_in_cs,items, status, H, T-1); + assert {:layer 3} ideasInv(put_in_cs,items, status, H, T, take_in_cs, steal_in_cs, h_ss, t_ss); + assert {:layer 3} oldH <= H && t == t_ss[tid]; + assert {:layer 3} (h < t && take_in_cs && (h_ss[ptTid] < t_ss[ptTid]) && h == H) ==> (H < T); + assert {:layer 3} H >= h; + + if( h>= t) { + + task := EMPTY; + call stealExitCS(tid); + + oldH := H; + oldT := T; + yield; + assert {:layer 3} !steal_in_cs[tid]; + assert {:layer 3} stealerTid(tid) && !steal_in_cs[tid] && h_ss[tid] == h; + assert {:layer 3} queueInv(steal_in_cs,put_in_cs,take_in_cs,items, status, H, T-1); + assert {:layer 3} ideasInv(put_in_cs,items, status, H, T, take_in_cs, steal_in_cs, h_ss, t_ss); + assert {:layer 3} oldH <= H; + return; + } + + call task, taskstatus := readItems(tid, h); + + + oldH := H; + oldT := T; + yield; + assert {:layer 3} stealerTid(tid) && steal_in_cs[tid] && h_ss[tid] == h; + assert {:layer 3} queueInv(steal_in_cs,put_in_cs,take_in_cs,items, status, H, T-1); + assert {:layer 3} ideasInv(put_in_cs,items, status, H, T, take_in_cs, steal_in_cs, h_ss, t_ss); + assert {:layer 3} oldH <= H; + assert {:layer 3} oldH == H && H == h && h_ss[tid] == h ==> task != EMPTY; + assert {:layer 3} (take_in_cs && (h_ss[ptTid] < t_ss[ptTid]) && h == H) ==> (H < T); + assert {:layer 3} h == H ==> status[H] == IN_Q; + + call chk := CAS_H_steal(tid, h,h+1); + + oldH := H; + oldT := T; + yield; + assert {:layer 3} h_ss[tid] == h; + assert {:layer 3} chk ==> (h+1 == oldH && h_ss[tid] == h && task != EMPTY && taskstatus == IN_Q); + assert {:layer 3} (take_in_cs && (h_ss[ptTid] < t_ss[ptTid]) && chk) ==> ((oldH-1) < T); + assert {:layer 3} {:expand} ideasInv(put_in_cs,items, status, H, T, take_in_cs, steal_in_cs, h_ss, t_ss); + assert {:layer 3} stealerTid(tid) && !steal_in_cs[tid]; + assert {:layer 3} queueInv(steal_in_cs,put_in_cs,take_in_cs,items, status, H, T-1); + assert {:layer 3} oldH <= H; + + if(!chk) { + goto LOOP_ENTRY_2; + } + + oldH := H; + oldT := T; + yield; + assert {:layer 3} stealerTid(tid) && !steal_in_cs[tid]; + assert {:layer 3} queueInv(steal_in_cs,put_in_cs,take_in_cs,items, status, H, T-1); + assert {:layer 3} ideasInv(put_in_cs,items, status, H, T, take_in_cs, steal_in_cs, h_ss, t_ss); + assert {:layer 3} oldH <= H && task != EMPTY; + return; + } + + oldH := H; + oldT := T; + yield; + assert {:layer 3} chk && task != EMPTY; + assert {:layer 3} stealerTid(tid) && !steal_in_cs[tid]; + assert {:layer 3} oldH <= H; +} + +procedure {:yields}{:layer 0,3} readH_take({:linear "tid"} tid:Tid) returns (y: int); +ensures {:atomic} |{A: assert tid == ptTid; + y := H; + take_in_cs := true; + h_ss[tid] := H; + return true;}|; + +procedure {:yields}{:layer 0,3} readH_steal({:linear "tid"} tid:Tid) returns (y: int); +ensures {:atomic} |{A: assert stealerTid(tid); + assert !steal_in_cs[tid]; + y := H; + h_ss[tid] := H; + return true;}|; + +procedure {:yields}{:layer 0,3} readT_take_init({:linear "tid"} tid:Tid) returns (y: int); +ensures {:atomic} |{A: assert tid != NIL; assert tid == ptTid; y := T; return true;}|; + +procedure {:yields}{:layer 0,3} readT_put({:linear "tid"} tid:Tid) returns (y: int); +ensures {:atomic} |{A: assert tid != NIL; + assert tid == ptTid; + put_in_cs := true; + y := T; + return true;}|; + +procedure {:yields}{:layer 0,3} readT_steal({:linear "tid"} tid:Tid) returns (y: int); +ensures {:atomic} |{A: assert tid != NIL; + assert stealerTid(tid); + assert !steal_in_cs[tid]; + y := T; + t_ss[tid] := T; + steal_in_cs[tid] := true; + return true;}|; + +procedure {:yields}{:layer 0,3} readItems({:linear "tid"} tid:Tid, ind: int) returns (y: int, b:bool); +ensures {:atomic} |{A: y := items[ind]; b := status[ind]; return true; }|; + +procedure {:yields}{:layer 0,3} writeT_put({:linear "tid"} tid:Tid, val: int); +ensures {:atomic} |{A: assert tid == ptTid; + T := T+1; + put_in_cs := false; + return true; }|; + +procedure {:yields}{:layer 0,3} writeT_take({:linear "tid"} tid:Tid, val: int); +ensures {:atomic} |{A: assert tid == ptTid; + T := val; + t_ss[tid] := val; + return true; }|; + +procedure {:yields}{:layer 0,3} writeT_take_abort({:linear "tid"} tid:Tid, val: int); +ensures {:atomic} |{A: assert tid == ptTid; + assert take_in_cs; + T := val; + take_in_cs := false; + return true; }|; + +procedure {:yields}{:layer 0,3} writeT_take_eq({:linear "tid"} tid:Tid, val: int); +ensures {:atomic} |{A: assert tid == ptTid; + T := val; + return true; }|; + +procedure {:yields}{:layer 0,3} takeExitCS({:linear "tid"} tid:Tid); +ensures {:atomic} |{A: assert tid == ptTid; + take_in_cs := false; + return true; }|; + +procedure {:yields}{:layer 0,3} stealExitCS({:linear "tid"} tid:Tid); +ensures {:atomic} |{A: assert stealerTid(tid); + assert steal_in_cs[tid]; + steal_in_cs[tid] := false; + return true; }|; + + +procedure {:yields}{:layer 0,3} writeItems({:linear "tid"} tid:Tid, idx: int, val: int); +ensures {:atomic} |{A: assert tid == ptTid; + assert val != EMPTY; + items[idx] := val; + status[idx] := IN_Q; + return true; }|; + + +procedure {:yields}{:layer 0,3} writeItems_put({:linear "tid"} tid:Tid, idx: int, val: int); +ensures {:atomic} |{A: assert tid == ptTid; + assert val != EMPTY; + items[idx] := val; + status[idx] := IN_Q; + return true; }|; + +procedure {:yields}{:layer 0,3} CAS_H_take({:linear "tid"} tid:Tid, prevVal :int, val: int) + returns (result: bool); +ensures {:atomic} |{ A: assert tid == ptTid; + goto B, C; + B: assume H == prevVal; + take_in_cs := false; + status[H] := NOT_IN_Q; + H := H+1; + result := true; + return true; + C: assume H != prevVal; result := false; + take_in_cs := false; + return true; +}|; + +procedure {:yields}{:layer 0,3} CAS_H_steal({:linear "tid"} tid:Tid, prevVal :int, val: int) + returns (result: bool); +ensures {:atomic} |{ A: assert stealerTid(tid); + goto B, C; + B: assume H == prevVal; + status[H] := NOT_IN_Q; + H := H+1; + result := true; + steal_in_cs[tid] := false; + return true; + C: assume H != prevVal; + result := false; + steal_in_cs[tid] := false; + return true; + }|; \ No newline at end of file diff --git a/Test/civl/wsq.bpl.expect b/Test/civl/wsq.bpl.expect new file mode 100644 index 00000000..5b2909f1 --- /dev/null +++ b/Test/civl/wsq.bpl.expect @@ -0,0 +1,2 @@ + +Boogie program verifier finished with 3 verified, 0 errors diff --git a/Test/og/DeviceCache.bpl b/Test/og/DeviceCache.bpl deleted file mode 100644 index f439b607..00000000 --- a/Test/og/DeviceCache.bpl +++ /dev/null @@ -1,210 +0,0 @@ -// RUN: %boogie -noinfer -typeEncoding:m -useArrayTheory "%s" > "%t" -// RUN: %diff "%s.expect" "%t" -type X; -function {:builtin "MapConst"} mapconstbool(bool): [X]bool; -const nil: X; -var {:layer 0,1} ghostLock: X; -var {:layer 0,1} lock: X; -var {:layer 0,1} currsize: int; -var {:layer 0,1} newsize: int; - -function {:builtin "MapConst"} MapConstBool(bool) : [X]bool; -function {:inline} {:linear "tid"} TidCollector(x: X) : [X]bool -{ - MapConstBool(false)[x := true] -} -function {:inline} {:linear "tid"} TidSetCollector(x: [X]bool) : [X]bool -{ - x -} - -function {:inline} Inv(ghostLock: X, currsize: int, newsize: int) : (bool) -{ - 0 <= currsize && currsize <= newsize && - (ghostLock == nil <==> currsize == newsize) -} - -procedure {:yields} {:layer 1} Yield() -requires {:layer 1} Inv(ghostLock, currsize, newsize); -ensures {:layer 1} Inv(ghostLock, currsize, newsize); -{ - yield; - assert {:layer 1} Inv(ghostLock, currsize, newsize); -} - -procedure {:yields} {:layer 1} YieldToReadCache({:linear "tid"} tid: X) -requires {:layer 1} Inv(ghostLock, currsize, newsize) && tid != nil; -ensures {:layer 1} Inv(ghostLock, currsize, newsize) && old(currsize) <= currsize; -{ - yield; - assert {:layer 1} Inv(ghostLock, currsize, newsize) && old(currsize) <= currsize; -} - -procedure {:yields} {:layer 1} YieldToWriteCache({:linear "tid"} tid: X) -requires {:layer 1} Inv(ghostLock, currsize, newsize) && ghostLock == tid && tid != nil; -ensures {:layer 1} Inv(ghostLock, currsize, newsize) && ghostLock == tid && old(currsize) == currsize && old(newsize) == newsize; -{ - yield; - assert {:layer 1} Inv(ghostLock, currsize, newsize) && tid != nil && ghostLock == tid && old(currsize) == currsize && old(newsize) == newsize; -} - -procedure {:yields} {:layer 1} Allocate() returns ({:linear "tid"} xl: X) -ensures {:layer 1} xl != nil; -{ - yield; - call xl := AllocateLow(); - yield; -} - -procedure {:yields} {:layer 1} main({:linear_in "tid"} xls: [X]bool) -requires {:layer 1} xls == mapconstbool(true); -{ - var {:linear "tid"} tid: X; - - yield; - - call Init(xls); - - yield; - assert {:layer 1} Inv(ghostLock, currsize, newsize); - - while (*) - invariant {:layer 1} Inv(ghostLock, currsize, newsize); - { - par tid := Allocate() | Yield(); - yield; - assert {:layer 1} Inv(ghostLock, currsize, newsize); - async call Thread(tid); - yield; - assert {:layer 1} Inv(ghostLock, currsize, newsize); - } - yield; -} - -procedure {:yields} {:layer 1} Thread({:linear "tid"} tid: X) -requires {:layer 1} tid != nil; -requires {:layer 1} Inv(ghostLock, currsize, newsize); -{ - var start, size, bytesRead: int; - - havoc start, size; - assume (0 <= start && 0 <= size); - call bytesRead := Read(tid, start, size); -} - -procedure {:yields} {:layer 1} Read({:linear "tid"} tid: X, start : int, size : int) returns (bytesRead : int) -requires {:layer 1} tid != nil; -requires {:layer 1} 0 <= start && 0 <= size; -requires {:layer 1} Inv(ghostLock, currsize, newsize); -ensures {:layer 1} 0 <= bytesRead && bytesRead <= size; -{ - var i, tmp: int; - - par YieldToReadCache(tid); - bytesRead := size; - call acquire(tid); - call i := ReadCurrsize(tid); - call tmp := ReadNewsize(tid); - if (start + size <= i) { - call release(tid); - goto COPY_TO_BUFFER; - } else if (tmp > i) { - bytesRead := if (start <= i) then (i - start) else 0; - call release(tid); - goto COPY_TO_BUFFER; - } else { - call WriteNewsize(tid, start + size); - call release(tid); - goto READ_DEVICE; - } - -READ_DEVICE: - par YieldToWriteCache(tid); - call WriteCache(tid, start + size); - par YieldToWriteCache(tid); - call acquire(tid); - call tmp := ReadNewsize(tid); - call WriteCurrsize(tid, tmp); - call release(tid); - -COPY_TO_BUFFER: - par YieldToReadCache(tid); - call ReadCache(tid, start, bytesRead); -} - -procedure {:yields} {:layer 1} WriteCache({:linear "tid"} tid: X, index: int) -requires {:layer 1} Inv(ghostLock, currsize, newsize); -requires {:layer 1} ghostLock == tid && tid != nil; -ensures {:layer 1} ghostLock == tid; -ensures {:layer 1} Inv(ghostLock, currsize, newsize) && old(currsize) == currsize && old(newsize) == newsize; -{ - var j: int; - - par YieldToWriteCache(tid); - call j := ReadCurrsize(tid); - while (j < index) - invariant {:layer 1} ghostLock == tid && currsize <= j && tid == tid; - invariant {:layer 1} Inv(ghostLock, currsize, newsize) && old(currsize) == currsize && old(newsize) == newsize; - { - par YieldToWriteCache(tid); - call WriteCacheEntry(tid, j); - j := j + 1; - } - par YieldToWriteCache(tid); -} - -procedure {:yields} {:layer 1} ReadCache({:linear "tid"} tid: X, start: int, bytesRead: int) -requires {:layer 1} Inv(ghostLock, currsize, newsize); -requires {:layer 1} tid != nil; -requires {:layer 1} 0 <= start && 0 <= bytesRead; -requires {:layer 1} (bytesRead == 0 || start + bytesRead <= currsize); -ensures {:layer 1} Inv(ghostLock, currsize, newsize); -{ - var j: int; - - par YieldToReadCache(tid); - - j := 0; - while(j < bytesRead) - invariant {:layer 1} 0 <= j; - invariant {:layer 1} bytesRead == 0 || start + bytesRead <= currsize; - invariant {:layer 1} Inv(ghostLock, currsize, newsize); - { - assert {:layer 1} start + j < currsize; - call ReadCacheEntry(tid, start + j); - j := j + 1; - par YieldToReadCache(tid); - } - - par YieldToReadCache(tid); -} - -procedure {:yields} {:layer 0,1} Init({:linear_in "tid"} xls:[X]bool); -ensures {:atomic} |{ A: assert xls == mapconstbool(true); currsize := 0; newsize := 0; lock := nil; ghostLock := nil; return true; }|; - -procedure {:yields} {:layer 0,1} ReadCurrsize({:linear "tid"} tid: X) returns (val: int); -ensures {:right} |{A: assert tid != nil; assert lock == tid || ghostLock == tid; val := currsize; return true; }|; - -procedure {:yields} {:layer 0,1} ReadNewsize({:linear "tid"} tid: X) returns (val: int); -ensures {:right} |{A: assert tid != nil; assert lock == tid || ghostLock == tid; val := newsize; return true; }|; - -procedure {:yields} {:layer 0,1} WriteNewsize({:linear "tid"} tid: X, val: int); -ensures {:atomic} |{A: assert tid != nil; assert lock == tid && ghostLock == nil; newsize := val; ghostLock := tid; return true; }|; - -procedure {:yields} {:layer 0,1} WriteCurrsize({:linear "tid"} tid: X, val: int); -ensures {:atomic} |{A: assert tid != nil; assert lock == tid && ghostLock == tid; currsize := val; ghostLock := nil; return true; }|; - -procedure {:yields} {:layer 0,1} ReadCacheEntry({:linear "tid"} tid: X, index: int); -ensures {:atomic} |{ A: assert 0 <= index && index < currsize; return true; }|; - -procedure {:yields} {:layer 0,1} WriteCacheEntry({:linear "tid"} tid: X, index: int); -ensures {:right} |{ A: assert tid != nil; assert currsize <= index && ghostLock == tid; return true; }|; - -procedure {:yields} {:layer 0,1} acquire({:linear "tid"} tid: X); -ensures {:right} |{ A: assert tid != nil; assume lock == nil; lock := tid; return true; }|; - -procedure {:yields} {:layer 0,1} release({:linear "tid"} tid: X); -ensures {:left} |{ A: assert tid != nil; assert lock == tid; lock := nil; return true; }|; - -procedure {:yields} {:layer 0,1} AllocateLow() returns ({:linear "tid"} tid: X); -ensures {:atomic} |{ A: assume tid != nil; return true; }|; diff --git a/Test/og/DeviceCache.bpl.expect b/Test/og/DeviceCache.bpl.expect deleted file mode 100644 index 9ec7a92d..00000000 --- a/Test/og/DeviceCache.bpl.expect +++ /dev/null @@ -1,2 +0,0 @@ - -Boogie program verifier finished with 30 verified, 0 errors diff --git a/Test/og/FlanaganQadeer.bpl b/Test/og/FlanaganQadeer.bpl deleted file mode 100644 index 7345b5b2..00000000 --- a/Test/og/FlanaganQadeer.bpl +++ /dev/null @@ -1,75 +0,0 @@ -// RUN: %boogie -noinfer -typeEncoding:m -useArrayTheory "%s" > "%t" -// RUN: %diff "%s.expect" "%t" -type X; -const nil: X; -var {:layer 0,1} l: X; -var {:layer 0,1} x: int; - -function {:builtin "MapConst"} MapConstBool(bool) : [X]bool; -function {:inline} {:linear "tid"} TidCollector(x: X) : [X]bool -{ - MapConstBool(false)[x := true] -} - -procedure {:yields} {:layer 1} Allocate() returns ({:linear "tid"} xl: X) -ensures {:layer 1} xl != nil; -{ - yield; - call xl := AllocateLow(); - yield; -} - -procedure {:yields} {:layer 1} main() -{ - var {:linear "tid"} tid: X; - var val: int; - - yield; - while (*) - { - call tid := Allocate(); - havoc val; - async call foo(tid, val); - yield; - } - yield; -} -procedure {:yields} {:layer 0,1} Lock(tid: X); -ensures {:atomic} |{A: assume l == nil; l := tid; return true; }|; - -procedure {:yields} {:layer 0,1} Unlock(); -ensures {:atomic} |{A: l := nil; return true; }|; - -procedure {:yields} {:layer 0,1} Set(val: int); -ensures {:atomic} |{A: x := val; return true; }|; - -procedure {:yields} {:layer 0,1} AllocateLow() returns ({:linear "tid"} xl: X); -ensures {:atomic} |{ A: assume xl != nil; return true; }|; - -procedure {:yields} {:layer 1} foo({:linear_in "tid"} tid': X, val: int) -requires {:layer 1} tid' != nil; -{ - var {:linear "tid"} tid: X; - tid := tid'; - - yield; - call Lock(tid); - call tid := Yield(tid); - call Set(val); - call tid := Yield(tid); - assert {:layer 1} x == val; - call tid := Yield(tid); - call Unlock(); - yield; -} - -procedure {:yields} {:layer 1} Yield({:linear_in "tid"} tid': X) returns ({:linear "tid"} tid: X) -requires {:layer 1} tid' != nil; -ensures {:layer 1} tid == tid'; -ensures {:layer 1} old(l) == tid ==> old(l) == l && old(x) == x; -{ - tid := tid'; - yield; - assert {:layer 1} tid != nil; - assert {:layer 1} (old(l) == tid ==> old(l) == l && old(x) == x); -} \ No newline at end of file diff --git a/Test/og/FlanaganQadeer.bpl.expect b/Test/og/FlanaganQadeer.bpl.expect deleted file mode 100644 index fef5ddc0..00000000 --- a/Test/og/FlanaganQadeer.bpl.expect +++ /dev/null @@ -1,2 +0,0 @@ - -Boogie program verifier finished with 4 verified, 0 errors diff --git a/Test/og/Program1.bpl b/Test/og/Program1.bpl deleted file mode 100644 index f405b92a..00000000 --- a/Test/og/Program1.bpl +++ /dev/null @@ -1,33 +0,0 @@ -// RUN: %boogie -noinfer -typeEncoding:m -useArrayTheory "%s" > "%t" -// RUN: %diff "%s.expect" "%t" -var {:layer 0,1} x:int; - -procedure {:yields} {:layer 1} p() -requires {:layer 1} x >= 5; -ensures {:layer 1} x >= 8; -{ - yield; - assert {:layer 1} x >= 5; - call Incr(1); - yield; - assert {:layer 1} x >= 6; - call Incr(1); - yield; - assert {:layer 1} x >= 7; - call Incr(1); - yield; - assert {:layer 1} x >= 8; -} - -procedure {:yields} {:layer 1} q() -{ - yield; - call Incr(3); - yield; -} - -procedure {:yields} {:layer 0,1} Incr(val: int); -ensures {:atomic} -|{A: - x := x + val; return true; -}|; diff --git a/Test/og/Program1.bpl.expect b/Test/og/Program1.bpl.expect deleted file mode 100644 index 3de74d3e..00000000 --- a/Test/og/Program1.bpl.expect +++ /dev/null @@ -1,2 +0,0 @@ - -Boogie program verifier finished with 2 verified, 0 errors diff --git a/Test/og/Program2.bpl b/Test/og/Program2.bpl deleted file mode 100644 index 75c83c67..00000000 --- a/Test/og/Program2.bpl +++ /dev/null @@ -1,37 +0,0 @@ -// RUN: %boogie -noinfer -typeEncoding:m -useArrayTheory "%s" > "%t" -// RUN: %diff "%s.expect" "%t" -var {:layer 0,1} x:int; - -procedure {:yields} {:layer 1} yield_x(n: int) -requires {:layer 1} x >= n; -ensures {:layer 1} x >= n; -{ - yield; - assert {:layer 1} x >= n; -} - -procedure {:yields} {:layer 1} p() -requires {:layer 1} x >= 5; -ensures {:layer 1} x >= 8; -{ - call yield_x(5); - call Incr(1); - call yield_x(6); - call Incr(1); - call yield_x(7); - call Incr(1); - call yield_x(8); -} - -procedure {:yields} {:layer 1} q() -{ - yield; - call Incr(3); - yield; -} - -procedure {:yields} {:layer 0,1} Incr(val: int); -ensures {:atomic} -|{A: - x := x + val; return true; -}|; diff --git a/Test/og/Program2.bpl.expect b/Test/og/Program2.bpl.expect deleted file mode 100644 index 5b2909f1..00000000 --- a/Test/og/Program2.bpl.expect +++ /dev/null @@ -1,2 +0,0 @@ - -Boogie program verifier finished with 3 verified, 0 errors diff --git a/Test/og/Program3.bpl b/Test/og/Program3.bpl deleted file mode 100644 index f8c4e132..00000000 --- a/Test/og/Program3.bpl +++ /dev/null @@ -1,36 +0,0 @@ -// RUN: %boogie -noinfer -typeEncoding:m -useArrayTheory "%s" > "%t" -// RUN: %diff "%s.expect" "%t" -var {:layer 0,1} x:int; - -procedure {:yields} {:layer 1} yield_x() -ensures {:layer 1} x >= old(x); -{ - yield; - assert {:layer 1} x >= old(x); -} - -procedure {:yields} {:layer 1} p() -requires {:layer 1} x >= 5; -ensures {:layer 1} x >= 8; -{ - call yield_x(); - call Incr(1); - call yield_x(); - call Incr(1); - call yield_x(); - call Incr(1); - call yield_x(); -} - -procedure {:yields} {:layer 1} q() -{ - yield; - call Incr(3); - yield; -} - -procedure {:yields} {:layer 0,1} Incr(val: int); -ensures {:atomic} -|{A: - x := x + val; return true; -}|; diff --git a/Test/og/Program3.bpl.expect b/Test/og/Program3.bpl.expect deleted file mode 100644 index 5b2909f1..00000000 --- a/Test/og/Program3.bpl.expect +++ /dev/null @@ -1,2 +0,0 @@ - -Boogie program verifier finished with 3 verified, 0 errors diff --git a/Test/og/Program4.bpl b/Test/og/Program4.bpl deleted file mode 100644 index 7f2f9c44..00000000 --- a/Test/og/Program4.bpl +++ /dev/null @@ -1,68 +0,0 @@ -// RUN: %boogie -noinfer -typeEncoding:m -useArrayTheory "%s" > "%t" -// RUN: %diff "%s.expect" "%t" -type Tid; -var {:layer 0,1} a:[Tid]int; - -procedure {:yields} {:layer 1} main() { - var {:linear "tid"} tid:Tid; - - yield; - while (true) { - call tid := Allocate(); - async call P(tid); - yield; - } - yield; -} - -procedure {:yields} {:layer 1} P({:linear "tid"} tid: Tid) -ensures {:layer 1} a[tid] == old(a)[tid] + 1; -{ - var t:int; - - yield; - assert {:layer 1} a[tid] == old(a)[tid]; - call t := Read(tid); - yield; - assert {:layer 1} a[tid] == t; - call Write(tid, t + 1); - yield; - assert {:layer 1} a[tid] == t + 1; -} - -procedure {:yields} {:layer 1} Allocate() returns ({:linear "tid"} tid: Tid) -{ - yield; - call tid := AllocateLow(); - yield; -} - -procedure {:yields} {:layer 0,1} Read({:linear "tid"} tid: Tid) returns (val: int); -ensures {:atomic} -|{A: - val := a[tid]; return true; -}|; - -procedure {:yields} {:layer 0,1} Write({:linear "tid"} tid: Tid, val: int); -ensures {:atomic} -|{A: - a[tid] := val; return true; -}|; - -procedure {:yields} {:layer 0,1} AllocateLow() returns ({:linear "tid"} tid: Tid); -ensures {:atomic} |{ A: return true; }|; - - - -function {:builtin "MapConst"} MapConstBool(bool): [Tid]bool; -function {:builtin "MapOr"} MapOr([Tid]bool, [Tid]bool) : [Tid]bool; - -function {:inline} {:linear "tid"} TidCollector(x: Tid) : [Tid]bool -{ - MapConstBool(false)[x := true] -} -function {:inline} {:linear "tid"} TidSetCollector(x: [Tid]bool) : [Tid]bool -{ - x -} - diff --git a/Test/og/Program4.bpl.expect b/Test/og/Program4.bpl.expect deleted file mode 100644 index 5b2909f1..00000000 --- a/Test/og/Program4.bpl.expect +++ /dev/null @@ -1,2 +0,0 @@ - -Boogie program verifier finished with 3 verified, 0 errors diff --git a/Test/og/Program5.bpl b/Test/og/Program5.bpl deleted file mode 100644 index 7ede3124..00000000 --- a/Test/og/Program5.bpl +++ /dev/null @@ -1,79 +0,0 @@ -// RUN: %boogie -noinfer -typeEncoding:m -useArrayTheory "%s" > "%t" -// RUN: %diff "%s.expect" "%t" -type Tid; -const unique nil: Tid; - -function {:inline} UNALLOC():int { 0 } -function {:inline} WHITE():int { 1 } -function {:inline} GRAY():int { 2 } -function {:inline} BLACK():int { 3 } -function {:inline} Unalloc(i:int) returns(bool) { i <= 0 } -function {:inline} White(i:int) returns(bool) { i == 1 } -function {:inline} Gray(i:int) returns(bool) { i == 2 } -function {:inline} Black(i:int) returns(bool) { i >= 3 } - -procedure {:yields} {:layer 2} YieldColorOnlyGetsDarker() -ensures {:layer 2} Color >= old(Color); -{ - yield; - assert {:layer 2} Color >= old(Color); -} - -procedure {:yields} {:layer 2,3} WriteBarrier({:linear "tid"} tid:Tid) -ensures {:atomic} |{ A: assert tid != nil; goto B, C; - B: assume White(Color); Color := GRAY(); return true; - C: return true;}|; -{ - var colorLocal:int; - yield; - call colorLocal := GetColorNoLock(); - call YieldColorOnlyGetsDarker(); - if (White(colorLocal)) { call WriteBarrierSlow(tid); } - yield; -} - -procedure {:yields} {:layer 1,2} WriteBarrierSlow({:linear "tid"} tid:Tid) -ensures {:atomic} |{ A: assert tid != nil; goto B, C; - B: assume White(Color); Color := GRAY(); return true; - C: return true; }|; -{ - var colorLocal:int; - yield; - call AcquireLock(tid); - call colorLocal := GetColorLocked(tid); - if (White(colorLocal)) { call SetColorLocked(tid, GRAY()); } - call ReleaseLock(tid); - yield; -} - -procedure {:yields} {:layer 0,1} AcquireLock({:linear "tid"} tid: Tid); - ensures {:right} |{ A: assert tid != nil; assume lock == nil; lock := tid; return true; }|; - -procedure {:yields} {:layer 0,1} ReleaseLock({:linear "tid"} tid: Tid); - ensures {:left} |{ A: assert tid != nil; assert lock == tid; lock := nil; return true; }|; - -procedure {:yields} {:layer 0,1} SetColorLocked({:linear "tid"} tid:Tid, newCol:int); - ensures {:atomic} |{A: assert tid != nil; assert lock == tid; Color := newCol; return true;}|; - -procedure {:yields} {:layer 0,1} GetColorLocked({:linear "tid"} tid:Tid) returns (col:int); - ensures {:both} |{A: assert tid != nil; assert lock == tid; col := Color; return true;}|; - -procedure {:yields} {:layer 0,2} GetColorNoLock() returns (col:int); - ensures {:atomic} |{A: col := Color; return true;}|; - - - -function {:builtin "MapConst"} MapConstBool(bool): [Tid]bool; -function {:builtin "MapOr"} MapOr([Tid]bool, [Tid]bool) : [Tid]bool; - -var {:layer 0} Color:int; -var {:layer 0} lock:Tid; - -function {:inline} {:linear "tid"} TidCollector(x: Tid) : [Tid]bool -{ - MapConstBool(false)[x := true] -} -function {:inline} {:linear "tid"} TidSetCollector(x: [Tid]bool) : [Tid]bool -{ - x -} diff --git a/Test/og/Program5.bpl.expect b/Test/og/Program5.bpl.expect deleted file mode 100644 index d7c0ff95..00000000 --- a/Test/og/Program5.bpl.expect +++ /dev/null @@ -1,2 +0,0 @@ - -Boogie program verifier finished with 18 verified, 0 errors diff --git a/Test/og/akash.bpl b/Test/og/akash.bpl deleted file mode 100644 index c826b810..00000000 --- a/Test/og/akash.bpl +++ /dev/null @@ -1,106 +0,0 @@ -// RUN: %boogie -noinfer -typeEncoding:m -useArrayTheory "%s" > "%t" -// RUN: %diff "%s.expect" "%t" -function {:builtin "MapConst"} mapconstbool(bool) : [int]bool; - -function {:builtin "MapConst"} MapConstBool(bool) : [int]bool; -function {:inline} {:linear "tid"} TidCollector(x: int) : [int]bool -{ - MapConstBool(false)[x := true] -} - -function {:inline} {:linear "1"} SetCollector1(x: [int]bool) : [int]bool -{ - x -} - -function {:inline} {:linear "2"} SetCollector2(x: [int]bool) : [int]bool -{ - x -} - -var {:layer 0,1} g: int; -var {:layer 0,1} h: int; - -procedure {:yields} {:layer 0,1} SetG(val:int); -ensures {:atomic} |{A: g := val; return true; }|; - -procedure {:yields} {:layer 0,1} SetH(val:int); -ensures {:atomic} |{A: h := val; return true; }|; - -procedure {:yields} {:layer 1} Allocate() returns ({:linear "tid"} xl: int) -ensures {:layer 1} xl != 0; -{ - yield; - call xl := AllocateLow(); - yield; -} - -procedure {:yields} {:layer 0,1} AllocateLow() returns ({:linear "tid"} xls: int); -ensures {:atomic} |{ A: assume xls != 0; return true; }|; - -procedure {:yields} {:layer 1} A({:linear_in "tid"} tid_in: int, {:linear_in "1"} x: [int]bool, {:linear_in "2"} y: [int]bool) returns ({:linear "tid"} tid_out: int) -requires {:layer 1} x == mapconstbool(true); -requires {:layer 1} y == mapconstbool(true); -{ - var {:linear "tid"} tid_child: int; - tid_out := tid_in; - - yield; - call SetG(0); - yield; - assert {:layer 1} g == 0 && x == mapconstbool(true); - - yield; - call tid_child := Allocate(); - async call B(tid_child, x); - - yield; - call SetH(0); - - yield; - assert {:layer 1} h == 0 && y == mapconstbool(true); - - yield; - call tid_child := Allocate(); - async call C(tid_child, y); - - yield; -} - -procedure {:yields} {:layer 1} B({:linear_in "tid"} tid_in: int, {:linear_in "1"} x_in: [int]bool) -requires {:layer 1} x_in != mapconstbool(false); -{ - var {:linear "tid"} tid_out: int; - var {:linear "1"} x: [int]bool; - tid_out := tid_in; - x := x_in; - - yield; - - call SetG(1); - - yield; - - call SetG(2); - - yield; -} - -procedure {:yields} {:layer 1} C({:linear_in "tid"} tid_in: int, {:linear_in "2"} y_in: [int]bool) -requires {:layer 1} y_in != mapconstbool(false); -{ - var {:linear "tid"} tid_out: int; - var {:linear "2"} y: [int]bool; - tid_out := tid_in; - y := y_in; - - yield; - - call SetH(1); - - yield; - - call SetH(2); - - yield; -} \ No newline at end of file diff --git a/Test/og/akash.bpl.expect b/Test/og/akash.bpl.expect deleted file mode 100644 index fef5ddc0..00000000 --- a/Test/og/akash.bpl.expect +++ /dev/null @@ -1,2 +0,0 @@ - -Boogie program verifier finished with 4 verified, 0 errors diff --git a/Test/og/bar.bpl b/Test/og/bar.bpl deleted file mode 100644 index 4eef8378..00000000 --- a/Test/og/bar.bpl +++ /dev/null @@ -1,57 +0,0 @@ -// RUN: %boogie -noinfer "%s" > "%t" -// RUN: %diff "%s.expect" "%t" -var {:layer 0,1} g:int; - -procedure {:yields} {:layer 1} PB() -{ - yield; - call Incr(); - yield; -} - -procedure {:yields} {:layer 0,1} Incr(); -ensures {:atomic} -|{A: - g := g + 1; return true; -}|; - -procedure {:yields} {:layer 0,1} Set(v: int); -ensures {:atomic} -|{A: - g := v; return true; -}|; - -procedure {:yields} {:layer 1} PC() -ensures {:layer 1} g == old(g); -{ - yield; - assert {:layer 1} g == old(g); -} - -procedure {:yields} {:layer 1} PE() -{ - call PC(); -} - -procedure {:yields} {:layer 1} PD() -{ - yield; - call Set(3); - call PC(); - assert {:layer 1} g == 3; -} - -procedure {:yields} {:layer 1} Main2() -{ - yield; - while (*) - { - async call PB(); - yield; - async call PE(); - yield; - async call PD(); - yield; - } - yield; -} diff --git a/Test/og/bar.bpl.expect b/Test/og/bar.bpl.expect deleted file mode 100644 index 8999ae7f..00000000 --- a/Test/og/bar.bpl.expect +++ /dev/null @@ -1,13 +0,0 @@ -bar.bpl(28,3): Error: Non-interference check failed -Execution trace: - bar.bpl(7,3): anon0 - (0,0): anon00 - bar.bpl(14,3): inline$Incr_1$0$this_A - (0,0): inline$Impl_YieldChecker_PC_1$0$L0 -bar.bpl(28,3): Error: Non-interference check failed -Execution trace: - bar.bpl(38,3): anon0 - (0,0): anon00 - (0,0): inline$Impl_YieldChecker_PC_1$0$L0 - -Boogie program verifier finished with 3 verified, 2 errors diff --git a/Test/og/chris.bpl b/Test/og/chris.bpl deleted file mode 100644 index b54292ef..00000000 --- a/Test/og/chris.bpl +++ /dev/null @@ -1,28 +0,0 @@ -// RUN: %boogie -noinfer -typeEncoding:m -useArrayTheory "%s" > "%t" -// RUN: %diff "%s.expect" "%t" -var{:layer 1} x:int; - -procedure{:yields}{:layer 2} Havoc() - ensures{:atomic} |{ A: return true; }|; -{ - yield; -} - -procedure{:yields}{:layer 1} Recover() - ensures{:atomic} |{ A: assert x == 5; return true; }|; -{ - yield; -} - -procedure{:yields}{:layer 3} P() - ensures{:atomic} |{ A: return true; }|; - requires{:layer 2,3} x == 5; - ensures {:layer 2,3} x == 5; -{ - - yield; assert{:layer 2,3} x == 5; - call Havoc(); - yield; assert{:layer 3} x == 5; - call Recover(); - yield; assert{:layer 2,3} x == 5; -} diff --git a/Test/og/chris.bpl.expect b/Test/og/chris.bpl.expect deleted file mode 100644 index be6b95ba..00000000 --- a/Test/og/chris.bpl.expect +++ /dev/null @@ -1,2 +0,0 @@ - -Boogie program verifier finished with 6 verified, 0 errors diff --git a/Test/og/chris2.bpl b/Test/og/chris2.bpl deleted file mode 100644 index 73f112ed..00000000 --- a/Test/og/chris2.bpl +++ /dev/null @@ -1,34 +0,0 @@ -// RUN: %boogie -noinfer -typeEncoding:m -useArrayTheory "%s" > "%t" -// RUN: %diff "%s.expect" "%t" -var{:layer 20} x:int; - -procedure{:yields}{:layer 20,25} p_gt1_lower(); - ensures{:both} - |{ - A: - x := x + 1; - return true; - }|; - -procedure{:yields}{:layer 25,40} p_gt1() - ensures{:both} - |{ - A: - x := x + 1; - return true; - }|; -{ - yield; - call p_gt1_lower(); - yield; -} - -procedure{:yields}{:layer 20,40} p_gt2(); - ensures{:both} - |{ - A: - assert x == 0; - return true; - }|; - - diff --git a/Test/og/chris2.bpl.expect b/Test/og/chris2.bpl.expect deleted file mode 100644 index 2bf339f7..00000000 --- a/Test/og/chris2.bpl.expect +++ /dev/null @@ -1,18 +0,0 @@ -(0,0): Error BP5003: A postcondition might not hold on this return path. -chris2.bpl(30,5): Related location: Gate not preserved by p_gt1_lower -Execution trace: - (0,0): this_A -(0,0): Error BP5003: A postcondition might not hold on this return path. -(0,0): Related location: Gate failure of p_gt2 not preserved by p_gt1_lower -Execution trace: - (0,0): this_A -(0,0): Error BP5003: A postcondition might not hold on this return path. -chris2.bpl(30,5): Related location: Gate not preserved by p_gt1 -Execution trace: - (0,0): this_A -(0,0): Error BP5003: A postcondition might not hold on this return path. -(0,0): Related location: Gate failure of p_gt2 not preserved by p_gt1 -Execution trace: - (0,0): this_A - -Boogie program verifier finished with 1 verified, 4 errors diff --git a/Test/og/civl-paper.bpl b/Test/og/civl-paper.bpl deleted file mode 100644 index a7042c6a..00000000 --- a/Test/og/civl-paper.bpl +++ /dev/null @@ -1,175 +0,0 @@ -// RUN: %boogie -noinfer -typeEncoding:m -useArrayTheory "%s" > "%t" -// RUN: %diff "%s.expect" "%t" -type X; -const nil: X; - -function {:builtin "MapConst"} MapConstBool(bool) : [X]bool; -function {:inline} {:linear "tid"} TidCollector(x: X) : [X]bool -{ - MapConstBool(false)[x := true] -} - -type lmap; -function {:linear "mem"} dom(lmap): [int]bool; -function map(lmap): [int]int; -function cons([int]bool, [int]int) : lmap; -axiom (forall x: [int]bool, y: [int]int :: {cons(x,y)} dom(cons(x, y)) == x && map(cons(x,y)) == y); - -var {:layer 0,3} {:linear "mem"} g: lmap; -var {:layer 0,3} lock: X; -var {:layer 0,1} b: bool; - -const p: int; - -procedure {:yields} {:layer 1} Yield1() -requires {:layer 1} InvLock(lock, b); -ensures {:layer 1} InvLock(lock, b); -{ - yield; - assert {:layer 1} InvLock(lock, b); -} - -function {:inline} InvLock(lock: X, b: bool) : bool -{ - lock != nil <==> b -} - -procedure {:yields} {:layer 2} Yield2() -{ - yield; -} - -procedure {:yields} {:layer 3} Yield3() -requires {:layer 3} Inv(g); -ensures {:layer 3} Inv(g); -{ - yield; - assert {:layer 3} Inv(g); -} - -function {:inline} Inv(g: lmap) : bool -{ - dom(g)[p] && dom(g)[p+4] && map(g)[p] == map(g)[p+4] -} - -procedure {:yields} {:layer 3} P({:linear "tid"} tid: X) -requires {:layer 1} tid != nil && InvLock(lock, b); -ensures {:layer 1} InvLock(lock, b); -requires {:layer 3} tid != nil && Inv(g); -ensures {:layer 3} Inv(g); -{ - var t: int; - var {:linear "mem"} l: lmap; - - par Yield3() | Yield1(); - call AcquireProtected(tid); - call l := TransferFromGlobalProtected(tid); - call t := Load(l, p); - call l := Store(l, p, t+1); - call t := Load(l, p+4); - call l := Store(l, p+4, t+1); - call TransferToGlobalProtected(tid, l); - call ReleaseProtected(tid); - par Yield3() | Yield1(); -} - - -procedure {:yields} {:layer 2,3} TransferToGlobalProtected({:linear "tid"} tid: X, {:linear_in "mem"} l: lmap) -ensures {:both} |{ A: assert tid != nil && lock == tid; g := l; return true; }|; -requires {:layer 1} InvLock(lock, b); -ensures {:layer 1} InvLock(lock, b); -{ - par Yield1() | Yield2(); - call TransferToGlobal(tid, l); - par Yield1() | Yield2(); -} - -procedure {:yields} {:layer 2,3} TransferFromGlobalProtected({:linear "tid"} tid: X) returns ({:linear "mem"} l: lmap) -ensures {:both} |{ A: assert tid != nil && lock == tid; l := g; return true; }|; -requires {:layer 1} InvLock(lock, b); -ensures {:layer 1} InvLock(lock, b); -{ - par Yield1() | Yield2(); - call l := TransferFromGlobal(tid); - par Yield1() | Yield2(); -} - -procedure {:yields} {:layer 2,3} AcquireProtected({:linear "tid"} tid: X) -ensures {:right} |{ A: assert tid != nil; assume lock == nil; lock := tid; return true; }|; -requires {:layer 1} tid != nil && InvLock(lock, b); -ensures {:layer 1} InvLock(lock, b); -{ - par Yield1() | Yield2(); - call Acquire(tid); - par Yield1() | Yield2(); -} - -procedure {:yields} {:layer 2,3} ReleaseProtected({:linear "tid"} tid: X) -ensures {:left} |{ A: assert tid != nil && lock == tid; lock := nil; return true; }|; -requires {:layer 1} InvLock(lock, b); -ensures {:layer 1} InvLock(lock, b); -{ - par Yield1() | Yield2(); - call Release(tid); - par Yield1() | Yield2(); -} - -procedure {:yields} {:layer 1,2} Acquire({:linear "tid"} tid: X) -requires {:layer 1} tid != nil && InvLock(lock, b); -ensures {:layer 1} InvLock(lock, b); -ensures {:atomic} |{ A: assume lock == nil; lock := tid; return true; }|; -{ - var status: bool; - var tmp: X; - - par Yield1(); - L: - assert {:layer 1} InvLock(lock, b); - call status := CAS(tid, false, true); - par Yield1(); - goto A, B; - - A: - assume status; - par Yield1(); - return; - - B: - assume !status; - goto L; -} - -procedure {:yields} {:layer 1,2} Release({:linear "tid"} tid: X) -ensures {:atomic} |{ A: lock := nil; return true; }|; -requires {:layer 1} InvLock(lock, b); -ensures {:layer 1} InvLock(lock, b); -{ - par Yield1(); - call CLEAR(tid, false); - par Yield1(); -} - -procedure {:yields} {:layer 0,2} TransferToGlobal({:linear "tid"} tid: X, {:linear_in "mem"} l: lmap); -ensures {:atomic} |{ A: g := l; return true; }|; - -procedure {:yields} {:layer 0,2} TransferFromGlobal({:linear "tid"} tid: X) returns ({:linear "mem"} l: lmap); -ensures {:atomic} |{ A: l := g; return true; }|; - -procedure {:yields} {:layer 0,3} Load({:linear "mem"} l: lmap, a: int) returns (v: int); -ensures {:both} |{ A: v := map(l)[a]; return true; }|; - -procedure {:yields} {:layer 0,3} Store({:linear_in "mem"} l_in: lmap, a: int, v: int) returns ({:linear "mem"} l_out: lmap); -ensures {:both} |{ A: assume l_out == cons(dom(l_in), map(l_in)[a := v]); return true; }|; - -procedure {:yields} {:layer 0,1} CAS(tid: X, prev: bool, next: bool) returns (status: bool); -ensures {:atomic} |{ -A: goto B, C; -B: assume b == prev; b := next; status := true; lock := tid; return true; -C: status := false; return true; -}|; - -procedure {:yields} {:layer 0,1} CLEAR(tid: X, next: bool); -ensures {:atomic} |{ -A: b := next; lock := nil; return true; -}|; - diff --git a/Test/og/civl-paper.bpl.expect b/Test/og/civl-paper.bpl.expect deleted file mode 100644 index 4bcd03fb..00000000 --- a/Test/og/civl-paper.bpl.expect +++ /dev/null @@ -1,2 +0,0 @@ - -Boogie program verifier finished with 35 verified, 0 errors diff --git a/Test/og/foo.bpl b/Test/og/foo.bpl deleted file mode 100644 index 7eeab890..00000000 --- a/Test/og/foo.bpl +++ /dev/null @@ -1,57 +0,0 @@ -// RUN: %boogie -noinfer "%s" > "%t" -// RUN: %diff "%s.expect" "%t" -var {:layer 0,1} g:int; - -procedure {:yields} {:layer 1} PB() -{ - yield; - call Incr(); - yield; -} - -procedure {:yields} {:layer 0,1} Incr(); -ensures {:atomic} -|{A: - g := g + 1; return true; -}|; - -procedure {:yields} {:layer 0,1} Set(v: int); -ensures {:atomic} -|{A: - g := v; return true; -}|; - -procedure {:yields} {:layer 1} PC() -ensures {:layer 1} g == 3; -{ - yield; - call Set(3); - yield; - assert {:layer 1} g == 3; -} - -procedure {:yields} {:layer 1} PE() -{ - call PC(); -} - -procedure {:yields} {:layer 1} PD() -{ - call PC(); - assert {:layer 1} g == 3; -} - -procedure {:yields} {:layer 1} Main() -{ - yield; - while (*) - { - async call PB(); - yield; - async call PE(); - yield; - async call PD(); - yield; - } - yield; -} diff --git a/Test/og/foo.bpl.expect b/Test/og/foo.bpl.expect deleted file mode 100644 index 0d9de9db..00000000 --- a/Test/og/foo.bpl.expect +++ /dev/null @@ -1,8 +0,0 @@ -foo.bpl(30,3): Error: Non-interference check failed -Execution trace: - foo.bpl(7,3): anon0 - (0,0): anon00 - foo.bpl(14,3): inline$Incr_1$0$this_A - (0,0): inline$Impl_YieldChecker_PC_1$0$L0 - -Boogie program verifier finished with 4 verified, 1 error diff --git a/Test/og/ghost.bpl b/Test/og/ghost.bpl deleted file mode 100644 index 74d16acf..00000000 --- a/Test/og/ghost.bpl +++ /dev/null @@ -1,46 +0,0 @@ -// RUN: %boogie -noinfer -typeEncoding:m -useArrayTheory "%s" > "%t" -// RUN: %diff "%s.expect" "%t" -var {:layer 0} x: int; - -procedure {:yields} {:layer 0,1} Incr(); -ensures {:right} |{ A: x := x + 1; return true; }|; - -procedure ghost(y: int) returns (z: int) -requires y == 1; -ensures z == 2; -{ - z := y + 1; -} - -procedure {:yields} {:layer 1,2} Incr2() -ensures {:right} |{ A: x := x + 2; return true; }|; -{ - var {:ghost} a: int; - var {:ghost} b: int; - - yield; - call a := ghost(1); - assert {:layer 1} a == 2; - par Incr() | Incr(); - yield; -} - -procedure ghost_0() returns (z: int) -ensures z == x; -{ - z := x; -} - -procedure {:yields} {:layer 1,2} Incr2_0() -ensures {:right} |{ A: x := x + 2; return true; }|; -{ - var {:ghost} a: int; - var {:ghost} b: int; - - yield; - call a := ghost_0(); - par Incr() | Incr(); - call b := ghost_0(); - assert {:layer 1} b == a + 2; - yield; -} diff --git a/Test/og/ghost.bpl.expect b/Test/og/ghost.bpl.expect deleted file mode 100644 index 9823d44a..00000000 --- a/Test/og/ghost.bpl.expect +++ /dev/null @@ -1,2 +0,0 @@ - -Boogie program verifier finished with 6 verified, 0 errors diff --git a/Test/og/linear-set.bpl b/Test/og/linear-set.bpl deleted file mode 100644 index e481291a..00000000 --- a/Test/og/linear-set.bpl +++ /dev/null @@ -1,105 +0,0 @@ -// RUN: %boogie -noinfer -typeEncoding:m -useArrayTheory "%s" > "%t" -// RUN: %diff "%s.expect" "%t" -type X; -function {:builtin "MapConst"} MapConstInt(int) : [X]int; -function {:builtin "MapConst"} MapConstBool(bool) : [X]bool; -function {:builtin "MapOr"} MapOr([X]bool, [X]bool) : [X]bool; - -function {:inline} None() : [X]bool -{ - MapConstBool(false) -} - -function {:inline} All() : [X]bool -{ - MapConstBool(true) -} - -function {:inline} {:linear "x"} XCollector(xs: [X]bool) : [X]bool -{ - xs -} - -var {:layer 0,1} x: int; -var {:layer 0,1} l: [X]bool; - - -procedure {:yields} {:layer 1} Split({:linear_in "x"} xls: [X]bool) returns ({:linear "x"} xls1: [X]bool, {:linear "x"} xls2: [X]bool) -ensures {:layer 1} xls == MapOr(xls1, xls2) && xls1 != None() && xls2 != None(); -{ - yield; - call xls1, xls2 := SplitLow(xls); - yield; -} - -procedure {:yields} {:layer 1} Allocate() returns ({:linear "tid"} xls: [X]bool) -{ - yield; - call xls := AllocateLow(); - yield; -} - -procedure {:yields} {:layer 0,1} Set(v: int); -ensures {:atomic} |{A: x := v; return true; }|; - -procedure {:yields} {:layer 0,1} Lock(tidls: [X]bool); -ensures {:atomic} |{A: assume l == None(); l := tidls; return true; }|; - -procedure {:yields} {:layer 0,1} Unlock(); -ensures {:atomic} |{A: l := None(); return true; }|; - -procedure {:yields} {:layer 0,1} SplitLow({:linear_in "x"} xls: [X]bool) returns ({:linear "x"} xls1: [X]bool, {:linear "x"} xls2: [X]bool); -ensures {:atomic} |{ A: assume xls == MapOr(xls1, xls2) && xls1 != None() && xls2 != None(); return true; }|; - -procedure {:yields} {:layer 0,1} AllocateLow() returns ({:linear "tid"} xls: [X]bool); -ensures {:atomic} |{ A: return true; }|; - -procedure {:yields} {:layer 1} main({:linear_in "tid"} tidls': [X]bool, {:linear_in "x"} xls': [X]bool) -requires {:layer 1} tidls' != None() && xls' == All(); -{ - var {:linear "tid"} tidls: [X]bool; - var {:linear "x"} xls: [X]bool; - var {:linear "tid"} lsChild: [X]bool; - var {:linear "x"} xls1: [X]bool; - var {:linear "x"} xls2: [X]bool; - - tidls := tidls'; - xls := xls'; - yield; - call Set(42); - yield; - assert {:layer 1} xls == All(); - assert {:layer 1} x == 42; - call xls1, xls2 := Split(xls); - call lsChild := Allocate(); - assume (lsChild != None()); - yield; - async call thread(lsChild, xls1); - call lsChild := Allocate(); - assume (lsChild != None()); - yield; - async call thread(lsChild, xls2); - yield; -} - -procedure {:yields} {:layer 1} thread({:linear_in "tid"} tidls': [X]bool, {:linear_in "x"} xls': [X]bool) -requires {:layer 1} tidls' != None() && xls' != None(); -{ - var {:linear "x"} xls: [X]bool; - var {:linear "tid"} tidls: [X]bool; - - tidls := tidls'; - xls := xls'; - - yield; - call Lock(tidls); - yield; - assert {:layer 1} tidls != None() && xls != None(); - call Set(0); - yield; - assert {:layer 1} tidls != None() && xls != None(); - assert {:layer 1} x == 0; - assert {:layer 1} tidls != None() && xls != None(); - call Unlock(); - yield; -} diff --git a/Test/og/linear-set.bpl.expect b/Test/og/linear-set.bpl.expect deleted file mode 100644 index fef5ddc0..00000000 --- a/Test/og/linear-set.bpl.expect +++ /dev/null @@ -1,2 +0,0 @@ - -Boogie program verifier finished with 4 verified, 0 errors diff --git a/Test/og/linear-set2.bpl b/Test/og/linear-set2.bpl deleted file mode 100644 index 24d8a13a..00000000 --- a/Test/og/linear-set2.bpl +++ /dev/null @@ -1,106 +0,0 @@ -// RUN: %boogie -noinfer -typeEncoding:m -useArrayTheory "%s" > "%t" -// RUN: %diff "%s.expect" "%t" -type X; -function {:builtin "MapConst"} MapConstInt(int) : [X]int; -function {:builtin "MapConst"} MapConstBool(bool) : [X]bool; -function {:builtin "MapOr"} MapOr([X]bool, [X]bool) : [X]bool; - -function {:inline} None() : [X]bool -{ - MapConstBool(false) -} - -function {:inline} All() : [X]bool -{ - MapConstBool(true) -} - -function {:inline} {:linear "x"} XCollector(xs: [X]bool) : [X]bool -{ - xs -} - -var {:layer 0,1} x: int; -var {:layer 0,1} l: X; -const nil: X; - -procedure {:yields} {:layer 1} Split({:linear_in "x"} xls: [X]bool) returns ({:linear "x"} xls1: [X]bool, {:linear "x"} xls2: [X]bool) -ensures {:layer 1} xls == MapOr(xls1, xls2) && xls1 != None() && xls2 != None(); -{ - yield; - call xls1, xls2 := SplitLow(xls); - yield; -} - -procedure {:yields} {:layer 1} Allocate() returns ({:linear "tid"} xls: X) -ensures {:layer 1} xls != nil; -{ - yield; - call xls := AllocateLow(); - yield; -} - -procedure {:yields} {:layer 0,1} Set(v: int); -ensures {:atomic} |{A: x := v; return true; }|; - -procedure {:yields} {:layer 0,1} Lock(tidls: X); -ensures {:atomic} |{A: assume l == nil; l := tidls; return true; }|; - -procedure {:yields} {:layer 0,1} Unlock(); -ensures {:atomic} |{A: l := nil; return true; }|; - -procedure {:yields} {:layer 0,1} SplitLow({:linear_in "x"} xls: [X]bool) returns ({:linear "x"} xls1: [X]bool, {:linear "x"} xls2: [X]bool); -ensures {:atomic} |{ A: assume xls == MapOr(xls1, xls2) && xls1 != None() && xls2 != None(); return true; }|; - -procedure {:yields} {:layer 0,1} AllocateLow() returns ({:linear "tid"} xls: X); -ensures {:atomic} |{ A: assume xls != nil; return true; }|; - -procedure {:yields} {:layer 1} main({:linear_in "tid"} tidls': X, {:linear_in "x"} xls': [X]bool) -requires {:layer 1} tidls' != nil && xls' == All(); -{ - var {:linear "tid"} tidls: X; - var {:linear "x"} xls: [X]bool; - var {:linear "tid"} lsChild: X; - var {:linear "x"} xls1: [X]bool; - var {:linear "x"} xls2: [X]bool; - - tidls := tidls'; - xls := xls'; - - yield; - call Set(42); - yield; - assert {:layer 1} xls == All(); - assert {:layer 1} x == 42; - call xls1, xls2 := Split(xls); - call lsChild := Allocate(); - yield; - async call thread(lsChild, xls1); - call lsChild := Allocate(); - yield; - async call thread(lsChild, xls2); - yield; -} - -procedure {:yields} {:layer 1} thread({:linear_in "tid"} tidls': X, {:linear_in "x"} xls': [X]bool) -requires {:layer 1} tidls' != nil && xls' != None(); -{ - var {:linear "x"} xls: [X]bool; - var {:linear "tid"} tidls: X; - - tidls := tidls'; - xls := xls'; - - yield; - call Lock(tidls); - yield; - assert {:layer 1} tidls != nil && xls != None(); - call Set(0); - yield; - assert {:layer 1} tidls != nil && xls != None(); - assert {:layer 1} x == 0; - yield; - assert {:layer 1} tidls != nil && xls != None(); - call Unlock(); - yield; -} diff --git a/Test/og/linear-set2.bpl.expect b/Test/og/linear-set2.bpl.expect deleted file mode 100644 index fef5ddc0..00000000 --- a/Test/og/linear-set2.bpl.expect +++ /dev/null @@ -1,2 +0,0 @@ - -Boogie program verifier finished with 4 verified, 0 errors diff --git a/Test/og/lock-introduced.bpl b/Test/og/lock-introduced.bpl deleted file mode 100644 index c9650215..00000000 --- a/Test/og/lock-introduced.bpl +++ /dev/null @@ -1,100 +0,0 @@ -// RUN: %boogie -noinfer -typeEncoding:m -useArrayTheory "%s" > "%t" -// RUN: %diff "%s.expect" "%t" -function {:builtin "MapConst"} MapConstBool(bool) : [X]bool; -function {:inline} {:linear "tid"} TidCollector(x: X) : [X]bool -{ - MapConstBool(false)[x := true] -} - -type X; -const nil: X; -var {:layer 0,2} b: bool; -var {:layer 1,3} lock: X; - -procedure {:yields} {:layer 3} Customer({:linear "tid"} tid: X) -requires {:layer 2} tid != nil; -requires {:layer 2} InvLock(lock, b); -ensures {:layer 2} InvLock(lock, b); -{ - yield; - assert {:layer 2} InvLock(lock, b); - while (*) - invariant {:layer 2} InvLock(lock, b); - { - call Enter(tid); - call Leave(tid); - yield; - assert {:layer 2} InvLock(lock, b); - } - yield; - assert {:layer 2} InvLock(lock, b); -} - -function {:inline} InvLock(lock: X, b: bool) : bool -{ - lock != nil <==> b -} - -procedure {:yields} {:layer 2,3} Enter({:linear "tid"} tid: X) -requires {:layer 2} tid != nil; -requires {:layer 2} InvLock(lock, b); -ensures {:layer 2} InvLock(lock, b); -ensures {:right} |{ A: assume lock == nil && tid != nil; lock := tid; return true; }|; -{ - yield; - assert {:layer 2} InvLock(lock, b); - call LowerEnter(tid); - yield; - assert {:layer 2} InvLock(lock, b); -} - -procedure {:yields} {:layer 2,3} Leave({:linear "tid"} tid:X) -requires {:layer 2} InvLock(lock, b); -ensures {:layer 2} InvLock(lock, b); -ensures {:atomic} |{ A: assert lock == tid && tid != nil; lock := nil; return true; }|; -{ - yield; - assert {:layer 2} InvLock(lock, b); - call LowerLeave(); - yield; - assert {:layer 2} InvLock(lock, b); -} - -procedure {:yields} {:layer 1,2} LowerEnter({:linear "tid"} tid: X) -ensures {:atomic} |{ A: assume !b; b := true; lock := tid; return true; }|; -{ - var status: bool; - yield; - L: - call status := CAS(false, true); - yield; - goto A, B; - - A: - assume status; - yield; - return; - - B: - assume !status; - goto L; -} - -procedure {:yields} {:layer 1,2} LowerLeave() -ensures {:atomic} |{ A: b := false; lock := nil; return true; }|; -{ - yield; - call SET(false); - yield; -} - -procedure {:yields} {:layer 0,1} CAS(prev: bool, next: bool) returns (status: bool); -ensures {:atomic} |{ -A: goto B, C; -B: assume b == prev; b := next; status := true; return true; -C: status := false; return true; -}|; - -procedure {:yields} {:layer 0,1} SET(next: bool); -ensures {:atomic} |{ A: b := next; return true; }|; - diff --git a/Test/og/lock-introduced.bpl.expect b/Test/og/lock-introduced.bpl.expect deleted file mode 100644 index f62a8f46..00000000 --- a/Test/og/lock-introduced.bpl.expect +++ /dev/null @@ -1,2 +0,0 @@ - -Boogie program verifier finished with 12 verified, 0 errors diff --git a/Test/og/lock.bpl b/Test/og/lock.bpl deleted file mode 100644 index 9341591f..00000000 --- a/Test/og/lock.bpl +++ /dev/null @@ -1,57 +0,0 @@ -// RUN: %boogie -noinfer -typeEncoding:m -useArrayTheory "%s" > "%t" -// RUN: %diff "%s.expect" "%t" -var {:layer 0,2} b: bool; - -procedure {:yields} {:layer 2} main() -{ - yield; - while (*) - { - async call Customer(); - yield; - } - yield; -} - -procedure {:yields} {:layer 2} Customer() -{ - yield; - while (*) - { - call Enter(); - yield; - call Leave(); - yield; - } - yield; -} - -procedure {:yields} {:layer 1,2} Enter() -ensures {:atomic} |{ A: assume !b; b := true; return true; }|; -{ - var status: bool; - yield; - L: - call status := CAS(false, true); - yield; - goto A, B; - - A: - assume status; - yield; - return; - - B: - assume !status; - goto L; -} - -procedure {:yields} {:layer 0,2} CAS(prev: bool, next: bool) returns (status: bool); -ensures {:atomic} |{ -A: goto B, C; -B: assume b == prev; b := next; status := true; return true; -C: status := false; return true; -}|; - -procedure {:yields} {:layer 0,2} Leave(); -ensures {:atomic} |{ A: b := false; return true; }|; diff --git a/Test/og/lock.bpl.expect b/Test/og/lock.bpl.expect deleted file mode 100644 index 05d394c7..00000000 --- a/Test/og/lock.bpl.expect +++ /dev/null @@ -1,2 +0,0 @@ - -Boogie program verifier finished with 5 verified, 0 errors diff --git a/Test/og/lock2.bpl b/Test/og/lock2.bpl deleted file mode 100644 index 4809a8f5..00000000 --- a/Test/og/lock2.bpl +++ /dev/null @@ -1,63 +0,0 @@ -// RUN: %boogie -noinfer -typeEncoding:m -useArrayTheory "%s" > "%t" -// RUN: %diff "%s.expect" "%t" -var {:layer 0,2} b: int; - -procedure {:yields} {:layer 2} main() -{ - yield; - while (*) - { - async call Customer(); - yield; - } - yield; -} - -procedure {:yields} {:layer 2} Customer() -{ - yield; - while (*) - { - call Enter(); - yield; - call Leave(); - yield; - } - yield; -} - -procedure {:yields} {:layer 1,2} Enter() -ensures {:atomic} |{ A: assume b == 0; b := 1; return true; }|; -{ - var _old, curr: int; - yield; - while (true) { - call _old := CAS(0, 1); - yield; - if (_old == 0) { - break; - } - while (true) { - call curr := Read(); - yield; - if (curr == 0) { - break; - } - } - yield; - } - yield; -} - -procedure {:yields} {:layer 0,2} Read() returns (val: int); -ensures {:atomic} |{ A: val := b; return true; }|; - -procedure {:yields} {:layer 0,2} CAS(prev: int, next: int) returns (_old: int); -ensures {:atomic} |{ -A: _old := b; goto B, C; -B: assume _old == prev; b := next; return true; -C: assume _old != prev; return true; -}|; - -procedure {:yields} {:layer 0,2} Leave(); -ensures {:atomic} |{ A: b := 0; return true; }|; diff --git a/Test/og/lock2.bpl.expect b/Test/og/lock2.bpl.expect deleted file mode 100644 index 05d394c7..00000000 --- a/Test/og/lock2.bpl.expect +++ /dev/null @@ -1,2 +0,0 @@ - -Boogie program verifier finished with 5 verified, 0 errors diff --git a/Test/og/multiset.bpl b/Test/og/multiset.bpl deleted file mode 100644 index 7fb0a081..00000000 --- a/Test/og/multiset.bpl +++ /dev/null @@ -1,324 +0,0 @@ -// RUN: %boogie -noinfer -typeEncoding:m -useArrayTheory "%s" > "%t" -// RUN: %diff "%s.expect" "%t" -type X; - -const unique null : int; -const unique nil: X; -const unique done: X; - -var {:layer 0} elt : [int]int; -var {:layer 0} valid : [int]bool; -var {:layer 0} lock : [int]X; -var {:layer 0} owner : [int]X; -const max : int; - -function {:builtin "MapConst"} MapConstBool(bool) : [X]bool; -function {:inline} {:linear "tid"} TidCollector(x: X) : [X]bool -{ - MapConstBool(false)[x := true] -} - -axiom (max > 0); - -procedure {:yields} {:layer 0} acquire(i : int, {:linear "tid"} tid: X); -ensures {:right} |{ A: - assert 0 <= i && i < max; - assert tid != nil && tid != done; - assume lock[i] == nil; - lock[i] := tid; - return true; - }|; - - -procedure {:yields} {:layer 0} release(i : int, {:linear "tid"} tid: X); -ensures {:left} |{ A: - assert 0 <= i && i < max; - assert lock[i] == tid; - assert tid != nil && tid != done; - lock[i] := nil; - return true; - }|; - - -procedure {:yields} {:layer 0,1} getElt(j : int, {:linear "tid"} tid: X) returns (elt_j:int); -ensures {:both} |{ A: - assert 0 <= j && j < max; - assert lock[j] == tid; - assert tid != nil && tid != done; - elt_j := elt[j]; - return true; - }|; - - -procedure {:yields} {:layer 0,1} setElt(j : int, x : int, {:linear "tid"} tid: X); -ensures {:both} |{ A: - assert x != null; - assert owner[j] == nil; - assert 0 <= j && j < max; - assert lock[j] == tid; - assert tid != nil && tid != done; - elt[j] := x; - owner[j] := tid; - return true; - }|; - - -procedure {:yields} {:layer 0,2} setEltToNull(j : int, {:linear "tid"} tid: X); -ensures {:left} |{ A: - assert owner[j] == tid; - assert 0 <= j && j < max; - assert lock[j] == tid; - assert !valid[j]; - assert tid != nil && tid != done; - elt[j] := null; - owner[j] := nil; - return true; - }|; - -procedure {:yields} {:layer 0,2} setValid(j : int, {:linear "tid"} tid: X); -ensures {:both} |{ A: - assert 0 <= j && j < max; - assert lock[j] == tid; - assert tid != nil && tid != done; - assert owner[j] == tid; - valid[j] := true; - owner[j] := done; - return true; - }|; - -procedure {:yields} {:layer 0,2} isEltThereAndValid(j : int, x : int, {:linear "tid"} tid: X) returns (fnd:bool); -ensures {:both} |{ A: - assert 0 <= j && j < max; - assert lock[j] == tid; - assert tid != nil && tid != done; - fnd := (elt[j] == x) && valid[j]; - return true; - }|; - -procedure {:yields} {:layer 1,2} FindSlot(x : int, {:linear "tid"} tid: X) returns (r : int) -requires {:layer 1} Inv(valid, elt, owner) && x != null && tid != nil && tid != done; -ensures {:layer 1} Inv(valid, elt, owner); -ensures {:right} |{ A: assert tid != nil && tid != done; - assert x != null; - goto B, C; - B: assume (0 <= r && r < max); - assume elt[r] == null; - assume owner[r] == nil; - assume !valid[r]; - elt[r] := x; - owner[r] := tid; - return true; - C: assume (r == -1); return true; - }|; -{ - var j : int; - var elt_j : int; - - par Yield1(); - - j := 0; - while(j < max) - invariant {:layer 1} Inv(valid, elt, owner); - invariant {:layer 1} 0 <= j; - { - call acquire(j, tid); - call elt_j := getElt(j, tid); - if(elt_j == null) - { - call setElt(j, x, tid); - call release(j, tid); - r := j; - - par Yield1(); - return; - } - call release(j,tid); - - par Yield1(); - - j := j + 1; - } - r := -1; - - par Yield1(); - return; -} - -procedure {:yields} {:layer 2} Insert(x : int, {:linear "tid"} tid: X) returns (result : bool) -requires {:layer 1} Inv(valid, elt, owner) && x != null && tid != nil && tid != done; -ensures {:layer 1} Inv(valid, elt, owner); -requires {:layer 2} Inv(valid, elt, owner) && x != null && tid != nil && tid != done; -ensures {:layer 2} Inv(valid, elt, owner); -ensures {:atomic} |{ var r:int; - A: goto B, C; - B: assume (0 <= r && r < max); - assume valid[r] == false; - assume elt[r] == null; - assume owner[r] == nil; - elt[r] := x; valid[r] := true; owner[r] := done; - result := true; return true; - C: result := false; return true; - }|; - { - var i: int; - par Yield12(); - call i := FindSlot(x, tid); - - if(i == -1) - { - result := false; - par Yield12(); - return; - } - par Yield1(); - assert {:layer 1} i != -1; - assert {:layer 2} i != -1; - call acquire(i, tid); - assert {:layer 2} elt[i] == x; - assert {:layer 2} valid[i] == false; - call setValid(i, tid); - call release(i, tid); - result := true; - par Yield12(); - return; -} - -procedure {:yields} {:layer 2} InsertPair(x : int, y : int, {:linear "tid"} tid: X) returns (result : bool) -requires {:layer 1} Inv(valid, elt, owner) && x != null && y != null && tid != nil && tid != done; -ensures {:layer 1} Inv(valid, elt, owner); -requires {:layer 2} Inv(valid, elt, owner) && x != null && y != null && tid != nil && tid != done; -ensures {:layer 2} Inv(valid, elt, owner); -ensures {:atomic} |{ var rx:int; - var ry:int; - A: goto B, C; - B: assume (0 <= rx && rx < max && 0 <= ry && ry < max && rx != ry); - assume valid[rx] == false; - assume valid[ry] == false; - assume elt[rx] == null; - assume elt[rx] == null; - elt[rx] := x; - elt[ry] := y; - valid[rx] := true; - valid[ry] := true; - owner[rx] := done; - owner[ry] := done; - result := true; return true; - C: result := false; return true; - }|; - { - var i : int; - var j : int; - par Yield12(); - - call i := FindSlot(x, tid); - - if (i == -1) - { - result := false; - par Yield12(); - return; - } - - par Yield1(); - call j := FindSlot(y, tid); - - if(j == -1) - { - par Yield1(); - call acquire(i,tid); - call setEltToNull(i, tid); - call release(i,tid); - result := false; - par Yield12(); - return; - } - - par Yield1(); - assert {:layer 2} i != -1 && j != -1; - call acquire(i, tid); - call acquire(j, tid); - assert {:layer 2} elt[i] == x; - assert {:layer 2} elt[j] == y; - assert {:layer 2} valid[i] == false; - assert {:layer 2} valid[j] == false; - call setValid(i, tid); - call setValid(j, tid); - call release(j, tid); - call release(i, tid); - result := true; - par Yield12(); - return; -} - -procedure {:yields} {:layer 2} LookUp(x : int, {:linear "tid"} tid: X, old_valid:[int]bool, old_elt:[int]int) returns (found : bool) -requires {:layer 1} {:layer 2} old_valid == valid && old_elt == elt; -requires {:layer 1} {:layer 2} Inv(valid, elt, owner); -requires {:layer 1} {:layer 2} (tid != nil && tid != done); -ensures {:layer 1} {:layer 2} Inv(valid, elt, owner); -ensures {:atomic} |{ A: assert tid != nil && tid != done; - assert x != null; - assume found ==> (exists ii:int :: 0 <= ii && ii < max && valid[ii] && elt[ii] == x); - assume !found ==> (forall ii:int :: 0 <= ii && ii < max ==> !(old_valid[ii] && old_elt[ii] == x)); - return true; - }|; -{ - var j : int; - var isThere : bool; - - par Yield12() | YieldLookUp(old_valid, old_elt); - - j := 0; - - while(j < max) - invariant {:layer 1} {:layer 2} Inv(valid, elt, owner); - invariant {:layer 1} {:layer 2} (forall ii:int :: 0 <= ii && ii < j ==> !(old_valid[ii] && old_elt[ii] == x)); - invariant {:layer 1} {:layer 2} (forall ii:int :: 0 <= ii && ii < max && old_valid[ii] ==> valid[ii] && old_elt[ii] == elt[ii]); - invariant {:layer 1} {:layer 2} 0 <= j; - { - call acquire(j, tid); - call isThere := isEltThereAndValid(j, x, tid); - if(isThere) - { - call release(j, tid); - found := true; - par Yield12() | YieldLookUp(old_valid, old_elt); - return; - } - call release(j,tid); - par Yield12() | YieldLookUp(old_valid, old_elt); - j := j + 1; - } - found := false; - - par Yield12() | YieldLookUp(old_valid, old_elt); - return; -} - -procedure {:yields} {:layer 1} Yield1() -requires {:layer 1} Inv(valid, elt, owner); -ensures {:layer 1} Inv(valid, elt, owner); -{ - yield; - assert {:layer 1} Inv(valid, elt, owner); -} - -procedure {:yields} {:layer 2} Yield12() -requires {:layer 1} {:layer 2} Inv(valid, elt, owner); -ensures {:layer 1} {:layer 2} Inv(valid, elt, owner); -{ - yield; - assert {:layer 1} {:layer 2} Inv(valid, elt, owner); -} - -function {:inline} Inv(valid: [int]bool, elt: [int]int, owner: [int]X): (bool) -{ - (forall i:int :: 0 <= i && i < max ==> (elt[i] == null <==> (!valid[i] && owner[i] == nil))) -} - -procedure {:yields} {:layer 2} YieldLookUp(old_valid: [int]bool, old_elt: [int]int) -requires {:layer 1} {:layer 2} (forall ii:int :: 0 <= ii && ii < max && old_valid[ii] ==> valid[ii] && old_elt[ii] == elt[ii]); -ensures {:layer 1} {:layer 2} (forall ii:int :: 0 <= ii && ii < max && old_valid[ii] ==> valid[ii] && old_elt[ii] == elt[ii]); -{ - yield; - assert {:layer 1} {:layer 2} (forall ii:int :: 0 <= ii && ii < max && old_valid[ii] ==> valid[ii] && old_elt[ii] == elt[ii]); -} diff --git a/Test/og/multiset.bpl.expect b/Test/og/multiset.bpl.expect deleted file mode 100644 index d72077a6..00000000 --- a/Test/og/multiset.bpl.expect +++ /dev/null @@ -1,2 +0,0 @@ - -Boogie program verifier finished with 78 verified, 0 errors diff --git a/Test/og/new1.bpl b/Test/og/new1.bpl deleted file mode 100644 index b80b6315..00000000 --- a/Test/og/new1.bpl +++ /dev/null @@ -1,42 +0,0 @@ -// RUN: %boogie -noinfer -typeEncoding:m -useArrayTheory "%s" > "%t" -// RUN: %diff "%s.expect" "%t" -function {:builtin "MapConst"} mapconstbool(x:bool): [int]bool; - -var {:layer 0,1} g:int; - -function {:inline} {:linear "Perm"} SetCollectorPerm(x: [int]bool) : [int]bool -{ - x -} - -procedure {:yields} {:layer 1} PB({:linear_in "Perm"} permVar_in:[int]bool) -requires {:layer 1} permVar_in[0] && g == 0; -{ - var {:linear "Perm"} permVar_out: [int]bool; - permVar_out := permVar_in; - - yield; - assert {:layer 1} permVar_out[0]; - assert {:layer 1} g == 0; - - call IncrG(); - - yield; - assert {:layer 1} permVar_out[0]; - assert {:layer 1} g == 1; -} - -procedure {:yields} {:layer 1} Main({:linear_in "Perm"} Permissions: [int]bool) -requires {:layer 1} Permissions == mapconstbool(true); -{ - yield; - call SetG(0); - async call PB(Permissions); - yield; -} - -procedure {:yields} {:layer 0,1} SetG(val:int); -ensures {:atomic} |{A: g := val; return true; }|; - -procedure {:yields} {:layer 0,1} IncrG(); -ensures {:atomic} |{A: g := g + 1; return true; }|; diff --git a/Test/og/new1.bpl.expect b/Test/og/new1.bpl.expect deleted file mode 100644 index 3de74d3e..00000000 --- a/Test/og/new1.bpl.expect +++ /dev/null @@ -1,2 +0,0 @@ - -Boogie program verifier finished with 2 verified, 0 errors diff --git a/Test/og/one.bpl b/Test/og/one.bpl deleted file mode 100644 index 663b2da0..00000000 --- a/Test/og/one.bpl +++ /dev/null @@ -1,18 +0,0 @@ -// RUN: %boogie -noinfer "%s" > "%t" -// RUN: %diff "%s.expect" "%t" -var {:layer 0,1} x:int; - -procedure {:yields} {:layer 0,1} Set(v: int); -ensures {:atomic} -|{A: - x := v; return true; -}|; - -procedure {:yields} {:layer 1} B() -{ - yield; - call Set(5); - yield; - assert {:layer 1} x == 5; -} - diff --git a/Test/og/one.bpl.expect b/Test/og/one.bpl.expect deleted file mode 100644 index 6abb715b..00000000 --- a/Test/og/one.bpl.expect +++ /dev/null @@ -1,2 +0,0 @@ - -Boogie program verifier finished with 1 verified, 0 errors diff --git a/Test/og/par-incr.bpl b/Test/og/par-incr.bpl deleted file mode 100644 index 7be8f561..00000000 --- a/Test/og/par-incr.bpl +++ /dev/null @@ -1,31 +0,0 @@ -// RUN: %boogie -noinfer -typeEncoding:m -useArrayTheory "%s" > "%t" -// RUN: %diff "%s.expect" "%t" - -var {:layer 0} x: int; - -procedure {:yields} {:layer 0,1} Incr(); -ensures {:right} |{ A: x := x + 1; return true; }|; - -procedure {:yields} {:layer 1,2} Incr2() -ensures {:right} |{ A: x := x + 2; return true; }|; -{ - yield; - par Incr() | Incr(); - yield; -} - -procedure {:yields} {:layer 1} Yield() -{ - yield; -} - -procedure {:yields} {:layer 2,3} Incr4() -ensures {:atomic} |{ A: x := x + 4; return true; }|; -{ - yield; - par Incr2() | Incr2() | Yield(); - yield; -} - - - diff --git a/Test/og/par-incr.bpl.expect b/Test/og/par-incr.bpl.expect deleted file mode 100644 index 00ddb38b..00000000 --- a/Test/og/par-incr.bpl.expect +++ /dev/null @@ -1,2 +0,0 @@ - -Boogie program verifier finished with 4 verified, 0 errors diff --git a/Test/og/parallel1.bpl b/Test/og/parallel1.bpl deleted file mode 100644 index 20dd3c79..00000000 --- a/Test/og/parallel1.bpl +++ /dev/null @@ -1,48 +0,0 @@ -// RUN: %boogie -noinfer "%s" > "%t" -// RUN: %diff "%s.expect" "%t" -var {:layer 0,1} g:int; - -procedure {:yields} {:layer 1} PB() -{ - yield; - call Incr(); - yield; -} - -procedure {:yields} {:layer 0,1} Incr(); -ensures {:atomic} -|{A: - g := g + 1; return true; -}|; - -procedure {:yields} {:layer 0,1} Set(v: int); -ensures {:atomic} -|{A: - g := v; return true; -}|; - -procedure {:yields} {:layer 1} PC() -ensures {:layer 1} g == 3; -{ - yield; - call Set(3); - yield; - assert {:layer 1} g == 3; -} - -procedure {:yields} {:layer 1} PD() -{ - call PC(); - assert {:layer 1} g == 3; - yield; -} - -procedure {:yields} {:layer 1} Main() -{ - yield; - while (*) - { - par PB() | PC() | PD(); - } - yield; -} diff --git a/Test/og/parallel1.bpl.expect b/Test/og/parallel1.bpl.expect deleted file mode 100644 index 588c9c5b..00000000 --- a/Test/og/parallel1.bpl.expect +++ /dev/null @@ -1,8 +0,0 @@ -parallel1.bpl(30,3): Error: Non-interference check failed -Execution trace: - parallel1.bpl(7,3): anon0 - (0,0): anon00 - parallel1.bpl(14,3): inline$Incr_1$0$this_A - (0,0): inline$Impl_YieldChecker_PC_1$0$L0 - -Boogie program verifier finished with 3 verified, 1 error diff --git a/Test/og/parallel2.bpl b/Test/og/parallel2.bpl deleted file mode 100644 index c28edf2b..00000000 --- a/Test/og/parallel2.bpl +++ /dev/null @@ -1,59 +0,0 @@ -// RUN: %boogie -noinfer -typeEncoding:m -useArrayTheory "%s" > "%t" -// RUN: %diff "%s.expect" "%t" -var {:layer 0,1} a:[int]int; - -function {:builtin "MapConst"} MapConstBool(bool) : [int]bool; -function {:inline} {:linear "tid"} TidCollector(x: int) : [int]bool -{ - MapConstBool(false)[x := true] -} - -procedure {:yields} {:layer 1} Allocate() returns ({:linear "tid"} tid: int) -{ - yield; - call tid := AllocateLow(); - yield; -} - -procedure {:yields} {:layer 0,1} Write(idx: int, val: int); -ensures {:atomic} |{A: a[idx] := val; return true; }|; - -procedure {:yields} {:layer 1} main() -{ - var {:linear "tid"} i: int; - var {:linear "tid"} j: int; - call i := Allocate(); - call j := Allocate(); - par i := t(i) | j := t(j); - par i := u(i) | j := u(j); -} - -procedure {:yields} {:layer 1} t({:linear_in "tid"} i': int) returns ({:linear "tid"} i: int) -{ - i := i'; - - yield; - call Write(i, 42); - call Yield(i); - assert {:layer 1} a[i] == 42; -} - -procedure {:yields} {:layer 1} u({:linear_in "tid"} i': int) returns ({:linear "tid"} i: int) -{ - i := i'; - - yield; - call Write(i, 42); - yield; - assert {:layer 1} a[i] == 42; -} - -procedure {:yields} {:layer 1} Yield({:linear "tid"} i: int) -ensures {:layer 1} old(a)[i] == a[i]; -{ - yield; - assert {:layer 1} old(a)[i] == a[i]; -} - -procedure {:yields} {:layer 0,1} AllocateLow() returns ({:linear "tid"} tid: int); -ensures {:atomic} |{ A: return true; }|; diff --git a/Test/og/parallel2.bpl.expect b/Test/og/parallel2.bpl.expect deleted file mode 100644 index 05d394c7..00000000 --- a/Test/og/parallel2.bpl.expect +++ /dev/null @@ -1,2 +0,0 @@ - -Boogie program verifier finished with 5 verified, 0 errors diff --git a/Test/og/parallel4.bpl b/Test/og/parallel4.bpl deleted file mode 100644 index f06ff4b8..00000000 --- a/Test/og/parallel4.bpl +++ /dev/null @@ -1,45 +0,0 @@ -// RUN: %boogie -noinfer -typeEncoding:m -useArrayTheory "%s" > "%t" -// RUN: %diff "%s.expect" "%t" -var {:layer 0,1} a:int; - -procedure {:yields} {:layer 1} Allocate() returns ({:linear "tid"} tid: int) -{ - yield; - call tid := AllocateLow(); - yield; -} - -function {:builtin "MapConst"} MapConstBool(bool) : [int]bool; -function {:inline} {:linear "tid"} TidCollector(x: int) : [int]bool -{ - MapConstBool(false)[x := true] -} - -procedure {:yields} {:layer 1} main() -{ - var {:linear "tid"} i: int; - var {:linear "tid"} j: int; - call i := Allocate(); - call j := Allocate(); - par i := t(i) | j := t(j); -} - -procedure {:yields} {:layer 1} t({:linear_in "tid"} i': int) returns ({:linear "tid"} i: int) -{ - i := i'; - call Yield(); - assert {:layer 1} a == old(a); - call Incr(); - yield; -} - -procedure {:yields} {:layer 0,1} Incr(); -ensures {:atomic} |{A: a := a + 1; return true; }|; - -procedure {:yields} {:layer 1} Yield() -{ - yield; -} - -procedure {:yields} {:layer 0,1} AllocateLow() returns ({:linear "tid"} tid: int); -ensures {:atomic} |{ A: return true; }|; diff --git a/Test/og/parallel4.bpl.expect b/Test/og/parallel4.bpl.expect deleted file mode 100644 index 25ad398c..00000000 --- a/Test/og/parallel4.bpl.expect +++ /dev/null @@ -1,6 +0,0 @@ -parallel4.bpl(31,3): Error BP5001: This assertion might not hold. -Execution trace: - parallel4.bpl(29,5): anon0 - (0,0): anon01 - -Boogie program verifier finished with 3 verified, 1 error diff --git a/Test/og/parallel5.bpl b/Test/og/parallel5.bpl deleted file mode 100644 index 87afc888..00000000 --- a/Test/og/parallel5.bpl +++ /dev/null @@ -1,59 +0,0 @@ -// RUN: %boogie -noinfer -typeEncoding:m -useArrayTheory "%s" > "%t" -// RUN: %diff "%s.expect" "%t" -var {:layer 0,1} a:[int]int; - -procedure {:yields} {:layer 1} Allocate() returns ({:linear "tid"} tid: int) -{ - yield; - call tid := AllocateLow(); - yield; -} - -function {:builtin "MapConst"} MapConstBool(bool) : [int]bool; -function {:inline} {:linear "tid"} TidCollector(x: int) : [int]bool -{ - MapConstBool(false)[x := true] -} - -procedure {:yields} {:layer 0,1} Write(idx: int, val: int); -ensures {:atomic} |{A: a[idx] := val; return true; }|; - -procedure {:yields} {:layer 1} main() -{ - var {:linear "tid"} i: int; - var {:linear "tid"} j: int; - call i := Allocate(); - call j := Allocate(); - par i := t(i) | Yield(j); - par i := u(i) | j := u(j); -} - -procedure {:yields} {:layer 1} t({:linear_in "tid"} i': int) returns ({:linear "tid"} i: int) -{ - i := i'; - - yield; - call Write(i, 42); - call Yield(i); - assert {:layer 1} a[i] == 42; -} - -procedure {:yields} {:layer 1} u({:linear_in "tid"} i': int) returns ({:linear "tid"} i: int) -{ - i := i'; - - yield; - call Write(i, 42); - yield; - assert {:layer 1} a[i] == 42; -} - -procedure {:yields} {:layer 1} Yield({:linear "tid"} i: int) -ensures {:layer 1} old(a)[i] == a[i]; -{ - yield; - assert {:layer 1} old(a)[i] == a[i]; -} - -procedure {:yields} {:layer 0,1} AllocateLow() returns ({:linear "tid"} tid: int); -ensures {:atomic} |{ A: return true; }|; diff --git a/Test/og/parallel5.bpl.expect b/Test/og/parallel5.bpl.expect deleted file mode 100644 index 05d394c7..00000000 --- a/Test/og/parallel5.bpl.expect +++ /dev/null @@ -1,2 +0,0 @@ - -Boogie program verifier finished with 5 verified, 0 errors diff --git a/Test/og/perm.bpl b/Test/og/perm.bpl deleted file mode 100644 index 5bc75324..00000000 --- a/Test/og/perm.bpl +++ /dev/null @@ -1,49 +0,0 @@ -// RUN: %boogie -noinfer -typeEncoding:m -useArrayTheory "%s" > "%t" -// RUN: %diff "%s.expect" "%t" -var {:layer 0,1} x: int; -function {:builtin "MapConst"} ch_mapconstbool(x: bool) : [int]bool; - -function {:builtin "MapOr"} ch_mapunion(x: [int]bool, y: [int]bool) : [int]bool; - -function {:inline} {:linear "Perm"} SetCollectorPerm(x: [int]bool) : [int]bool -{ - x -} - -procedure {:yields} {:layer 1} mainE({:linear_in "Perm"} permVar_in: [int]bool) - requires {:layer 1} permVar_in == ch_mapconstbool(true); - requires {:layer 1} x == 0; -{ - var {:linear "Perm"} permVar_out: [int]bool; - - permVar_out := permVar_in; - - yield; - assert {:layer 1} x == 0; - assert {:layer 1} permVar_out == ch_mapconstbool(true); - - async call foo(permVar_out); - yield; -} - -procedure {:yields} {:layer 1} foo({:linear_in "Perm"} permVar_in: [int]bool) - requires {:layer 1} permVar_in != ch_mapconstbool(false); - requires {:layer 1} permVar_in[1]; - requires {:layer 1} x == 0; -{ - var {:linear "Perm"} permVar_out: [int]bool; - permVar_out := permVar_in; - - yield; - assert {:layer 1} permVar_out[1]; - assert {:layer 1} x == 0; - - call Incr(); - - yield; - assert {:layer 1} permVar_out[1]; - assert {:layer 1} x == 1; -} - -procedure {:yields} {:layer 0,1} Incr(); -ensures {:atomic} |{A: x := x + 1; return true; }|; \ No newline at end of file diff --git a/Test/og/perm.bpl.expect b/Test/og/perm.bpl.expect deleted file mode 100644 index 3de74d3e..00000000 --- a/Test/og/perm.bpl.expect +++ /dev/null @@ -1,2 +0,0 @@ - -Boogie program verifier finished with 2 verified, 0 errors diff --git a/Test/og/t1.bpl b/Test/og/t1.bpl deleted file mode 100644 index 675b3842..00000000 --- a/Test/og/t1.bpl +++ /dev/null @@ -1,103 +0,0 @@ -// RUN: %boogie -noinfer -typeEncoding:m -useArrayTheory "%s" > "%t" -// RUN: %diff "%s.expect" "%t" -function {:builtin "MapConst"} mapconstbool(bool) : [int]bool; - -function {:builtin "MapConst"} MapConstBool(bool) : [int]bool; -function {:inline} {:linear "tid"} TidCollector(x: int) : [int]bool -{ - MapConstBool(false)[x := true] -} - -function {:inline} {:linear "1"} SetCollector1(x: [int]bool) : [int]bool -{ - x -} - -function {:inline} {:linear "2"} SetCollector2(x: [int]bool) : [int]bool -{ - x -} - -var {:layer 0,1} g: int; -var {:layer 0,1} h: int; - -procedure {:yields} {:layer 0,1} SetG(val:int); -ensures {:atomic} |{A: g := val; return true; }|; - -procedure {:yields} {:layer 0,1} SetH(val:int); -ensures {:atomic} |{A: h := val; return true; }|; - -procedure {:yields} {:layer 1} Yield({:linear "1"} x: [int]bool) -requires {:layer 1} x == mapconstbool(true) && g == 0; -ensures {:layer 1} x == mapconstbool(true) && g == 0; -{ - yield; - assert {:layer 1} x == mapconstbool(true) && g == 0; -} - -procedure {:yields} {:layer 1} Allocate() returns ({:linear "tid"} xl: int) -ensures {:layer 1} xl != 0; -{ - yield; - call xl := AllocateLow(); - yield; -} - -procedure {:yields} {:layer 0,1} AllocateLow() returns ({:linear "tid"} xls: int); -ensures {:atomic} |{ A: assume xls != 0; return true; }|; - -procedure {:yields} {:layer 1} A({:linear_in "tid"} tid_in: int, {:linear_in "1"} x: [int]bool, {:linear_in "2"} y: [int]bool) returns ({:linear "tid"} tid_out: int) -requires {:layer 1} x == mapconstbool(true); -requires {:layer 1} y == mapconstbool(true); -{ - var {:linear "tid"} tid_child: int; - tid_out := tid_in; - - yield; - call SetG(0); - - par tid_child := Allocate() | Yield(x); - - async call B(tid_child, x); - - yield; - assert {:layer 1} x == mapconstbool(true); - assert {:layer 1} g == 0; - - call SetH(0); - - yield; - assert {:layer 1} h == 0 && y == mapconstbool(true); - - yield; - call tid_child := Allocate(); - async call C(tid_child, y); - - yield; -} - -procedure {:yields} {:layer 1} B({:linear_in "tid"} tid_in: int, {:linear_in "1"} x_in: [int]bool) -requires {:layer 1} x_in != mapconstbool(false); -{ - var {:linear "tid"} tid_out: int; - var {:linear "1"} x: [int]bool; - tid_out := tid_in; - x := x_in; - - yield; - call SetG(1); - yield; -} - -procedure {:yields} {:layer 1} C({:linear_in "tid"} tid_in: int, {:linear_in "2"} y_in: [int]bool) -requires {:layer 1} y_in != mapconstbool(false); -{ - var {:linear "tid"} tid_out: int; - var {:linear "2"} y: [int]bool; - tid_out := tid_in; - y := y_in; - - yield; - call SetH(1); - yield; -} diff --git a/Test/og/t1.bpl.expect b/Test/og/t1.bpl.expect deleted file mode 100644 index 0b0c936e..00000000 --- a/Test/og/t1.bpl.expect +++ /dev/null @@ -1,9 +0,0 @@ -t1.bpl(65,5): Error: Non-interference check failed -Execution trace: - t1.bpl(84,13): anon0 - (0,0): anon05 - (0,0): inline$SetG_1$0$Entry - t1.bpl(25,21): inline$SetG_1$0$this_A - (0,0): inline$Impl_YieldChecker_A_1$0$L1 - -Boogie program verifier finished with 4 verified, 1 error diff --git a/Test/og/termination.bpl b/Test/og/termination.bpl deleted file mode 100644 index 2d5542dd..00000000 --- a/Test/og/termination.bpl +++ /dev/null @@ -1,18 +0,0 @@ -// RUN: %boogie -noinfer -typeEncoding:m -useArrayTheory "%s" > "%t" -// RUN: %diff "%s.expect" "%t" -procedure {:yields} {:layer 0} X(); -ensures {:atomic} |{ A: return true; }|; - -procedure {:yields} {:layer 0} Y(); -ensures {:left} |{ A: return true; }|; - -procedure {:yields} {:layer 1} main() { - yield; - call X(); - while (*) - { - call Y(); - } - yield; - assert {:layer 1} true; -} diff --git a/Test/og/termination.bpl.expect b/Test/og/termination.bpl.expect deleted file mode 100644 index d216a01d..00000000 --- a/Test/og/termination.bpl.expect +++ /dev/null @@ -1,3 +0,0 @@ -termination.bpl(9,31): Error: Implementation main fails simulation check C at layer 1. Transactions must be separated by a yield. - -1 type checking errors detected in termination.bpl diff --git a/Test/og/termination2.bpl b/Test/og/termination2.bpl deleted file mode 100644 index 840c27c1..00000000 --- a/Test/og/termination2.bpl +++ /dev/null @@ -1,19 +0,0 @@ -// RUN: %boogie -noinfer -typeEncoding:m -useArrayTheory "%s" > "%t" -// RUN: %diff "%s.expect" "%t" -procedure {:yields} {:layer 0} X(); -ensures {:atomic} |{ A: return true; }|; - -procedure {:yields} {:layer 0} Y(); -ensures {:left} |{ A: return true; }|; - -procedure {:yields} {:layer 1} main() { - yield; - call X(); - while (*) - invariant {:terminates} {:layer 1} true; - { - call Y(); - } - yield; - assert {:layer 1} true; -} diff --git a/Test/og/termination2.bpl.expect b/Test/og/termination2.bpl.expect deleted file mode 100644 index 6abb715b..00000000 --- a/Test/og/termination2.bpl.expect +++ /dev/null @@ -1,2 +0,0 @@ - -Boogie program verifier finished with 1 verified, 0 errors diff --git a/Test/og/ticket.bpl b/Test/og/ticket.bpl deleted file mode 100644 index 91863e1a..00000000 --- a/Test/og/ticket.bpl +++ /dev/null @@ -1,147 +0,0 @@ -// RUN: %boogie -noinfer -typeEncoding:m -useArrayTheory "%s" > "%t" -// RUN: %diff "%s.expect" "%t" -function RightOpen(n: int) : [int]bool; -function RightClosed(n: int) : [int]bool; -axiom (forall x: int, y: int :: RightOpen(x)[y] <==> y < x); -axiom (forall x: int, y: int :: RightClosed(x)[y] <==> y <= x); - -type X; -function {:builtin "MapConst"} mapconstbool(bool): [X]bool; -const nil: X; -var {:layer 0,2} t: int; -var {:layer 0,2} s: int; -var {:layer 0,2} cs: X; -var {:layer 0,2} T: [int]bool; - -function {:builtin "MapConst"} MapConstBool(bool) : [X]bool; -function {:inline} {:linear "tid"} TidCollector(x: X) : [X]bool -{ - MapConstBool(false)[x := true] -} -function {:inline} {:linear "tid"} TidSetCollector(x: [X]bool) : [X]bool -{ - x -} - -function {:inline} Inv1(tickets: [int]bool, ticket: int): (bool) -{ - tickets == RightOpen(ticket) -} - -function {:inline} Inv2(tickets: [int]bool, ticket: int, lock: X): (bool) -{ - if (lock == nil) then tickets == RightOpen(ticket) else tickets == RightClosed(ticket) -} - -procedure {:yields} {:layer 2} Allocate({:linear_in "tid"} xls':[X]bool) returns ({:linear "tid"} xls: [X]bool, {:linear "tid"} xl: X) -ensures {:layer 1} {:layer 2} xl != nil; -{ - yield; - call xls, xl := AllocateLow(xls'); - yield; -} - -procedure {:yields} {:layer 2} main({:linear_in "tid"} xls':[X]bool) -requires {:layer 2} xls' == mapconstbool(true); -{ - var {:linear "tid"} tid: X; - var {:linear "tid"} xls: [X]bool; - - yield; - - call Init(xls'); - xls := xls'; - - par Yield1() | Yield2(); - - while (*) - invariant {:layer 1} Inv1(T, t); - invariant {:layer 2} Inv2(T, s, cs); - { - par xls, tid := Allocate(xls) | Yield1() | Yield2(); - async call Customer(tid); - par Yield1() | Yield2(); - } - par Yield1() | Yield2(); -} - -procedure {:yields} {:layer 2} Customer({:linear_in "tid"} tid: X) -requires {:layer 1} Inv1(T, t); -requires {:layer 2} tid != nil && Inv2(T, s, cs); -{ - par Yield1() | Yield2(); - while (*) - invariant {:layer 1} Inv1(T, t); - invariant {:layer 2} Inv2(T, s, cs); - { - call Enter(tid); - par Yield1() | Yield2() | YieldSpec(tid); - call Leave(tid); - par Yield1() | Yield2(); - } - par Yield1() | Yield2(); -} - -procedure {:yields} {:layer 2} Enter({:linear "tid"} tid: X) -requires {:layer 1} Inv1(T, t); -ensures {:layer 1} Inv1(T,t); -requires {:layer 2} tid != nil && Inv2(T, s, cs); -ensures {:layer 2} Inv2(T, s, cs) && cs == tid; -{ - var m: int; - - par Yield1() | Yield2(); - call m := GetTicketAbstract(tid); - par Yield1(); - call WaitAndEnter(tid, m); - par Yield1() | Yield2() | YieldSpec(tid); -} - -procedure {:yields} {:layer 1,2} GetTicketAbstract({:linear "tid"} tid: X) returns (m: int) -requires {:layer 1} Inv1(T, t); -ensures {:layer 1} Inv1(T, t); -ensures {:right} |{ A: havoc m, t; assume !T[m]; T[m] := true; return true; }|; -{ - par Yield1(); - call m := GetTicket(tid); - par Yield1(); -} - -procedure {:yields} {:layer 2} YieldSpec({:linear "tid"} tid: X) -requires {:layer 2} tid != nil && cs == tid; -ensures {:layer 2} cs == tid; -{ - yield; - assert {:layer 2} tid != nil && cs == tid; -} - -procedure {:yields} {:layer 2} Yield2() -requires {:layer 2} Inv2(T, s, cs); -ensures {:layer 2} Inv2(T, s, cs); -{ - yield; - assert {:layer 2} Inv2(T, s, cs); -} - -procedure {:yields} {:layer 1} Yield1() -requires {:layer 1} Inv1(T, t); -ensures {:layer 1} Inv1(T,t); -{ - yield; - assert {:layer 1} Inv1(T,t); -} - -procedure {:yields} {:layer 0,2} Init({:linear "tid"} xls:[X]bool); -ensures {:atomic} |{ A: assert xls == mapconstbool(true); cs := nil; t := 0; s := 0; T := RightOpen(0); return true; }|; - -procedure {:yields} {:layer 0,1} GetTicket({:linear "tid"} tid: X) returns (m: int); -ensures {:atomic} |{ A: m := t; t := t + 1; T[m] := true; return true; }|; - -procedure {:yields} {:layer 0,2} WaitAndEnter({:linear "tid"} tid: X, m:int); -ensures {:atomic} |{ A: assume m <= s; cs := tid; return true; }|; - -procedure {:yields} {:layer 0,2} Leave({:linear "tid"} tid: X); -ensures {:atomic} |{ A: s := s + 1; cs := nil; return true; }|; - -procedure {:yields} {:layer 0,2} AllocateLow({:linear_in "tid"} xls':[X]bool) returns ({:linear "tid"} xls: [X]bool, {:linear "tid"} xl: X); -ensures {:atomic} |{ A: assume xl != nil; return true; }|; diff --git a/Test/og/ticket.bpl.expect b/Test/og/ticket.bpl.expect deleted file mode 100644 index 28c26eab..00000000 --- a/Test/og/ticket.bpl.expect +++ /dev/null @@ -1,2 +0,0 @@ - -Boogie program verifier finished with 16 verified, 0 errors diff --git a/Test/og/treiber-stack.bpl b/Test/og/treiber-stack.bpl deleted file mode 100644 index e1c509ab..00000000 --- a/Test/og/treiber-stack.bpl +++ /dev/null @@ -1,202 +0,0 @@ -// RUN: %boogie -noinfer -typeEncoding:m -useArrayTheory "%s" > "%t" -// RUN: %diff "%s.expect" "%t" -type Node = int; -const unique null: Node; -type lmap; -function {:linear "Node"} dom(lmap): [Node]bool; -function map(lmap): [Node]Node; -function {:builtin "MapConst"} MapConstBool(bool) : [Node]bool; - -function EmptyLmap(): (lmap); -axiom (dom(EmptyLmap()) == MapConstBool(false)); - -function Add(x: lmap, i: Node, v: Node): (lmap); -axiom (forall x: lmap, i: Node, v: Node :: dom(Add(x, i, v)) == dom(x)[i:=true] && map(Add(x, i, v)) == map(x)[i := v]); - -function Remove(x: lmap, i: Node): (lmap); -axiom (forall x: lmap, i: Node :: dom(Remove(x, i)) == dom(x)[i:=false] && map(Remove(x, i)) == map(x)); - -procedure {:yields} {:layer 0,1} ReadTopOfStack() returns (v:Node); -ensures {:right} |{ A: assume dom(Stack)[v] || dom(Used)[v]; return true; }|; - -procedure {:yields} {:layer 0,1} Load(i:Node) returns (v:Node); -ensures {:right} |{ A: assert dom(Stack)[i] || dom(Used)[i]; goto B,C; - B: assume dom(Stack)[i]; v := map(Stack)[i]; return true; - C: assume !dom(Stack)[i]; return true; }|; - -procedure {:yields} {:layer 0,1} Store({:linear_in "Node"} l_in:lmap, i:Node, v:Node) returns ({:linear "Node"} l_out:lmap); -ensures {:both} |{ A: assert dom(l_in)[i]; l_out := Add(l_in, i, v); return true; }|; - -procedure {:yields} {:layer 0,1} TransferToStack(oldVal: Node, newVal: Node, {:linear_in "Node"} l_in:lmap) returns (r: bool, {:linear "Node"} l_out:lmap); -ensures {:atomic} |{ A: assert dom(l_in)[newVal]; - goto B,C; - B: assume oldVal == TopOfStack; TopOfStack := newVal; l_out := EmptyLmap(); Stack := Add(Stack, newVal, map(l_in)[newVal]); r := true; return true; - C: assume oldVal != TopOfStack; l_out := l_in; r := false; return true; }|; - -procedure {:yields} {:layer 0,1} TransferFromStack(oldVal: Node, newVal: Node) returns (r: bool); -ensures {:atomic} |{ A: goto B,C; - B: assume oldVal == TopOfStack; TopOfStack := newVal; Used := Add(Used, oldVal, map(Stack)[oldVal]); Stack := Remove(Stack, oldVal); r := true; return true; - C: assume oldVal != TopOfStack; r := false; return true; }|; - -var {:layer 0} TopOfStack: Node; -var {:linear "Node"} {:layer 0} Stack: lmap; - - -function {:inline} Inv(TopOfStack: Node, Stack: lmap) : (bool) -{ - BetweenSet(map(Stack), TopOfStack, null)[TopOfStack] && - Subset(BetweenSet(map(Stack), TopOfStack, null), Union(Singleton(null), dom(Stack))) -} - -var {:linear "Node"} {:layer 0} Used: lmap; - -procedure {:yields} {:layer 1} push(x: Node, {:linear_in "Node"} x_lmap: lmap) -requires {:layer 1} dom(x_lmap)[x]; -requires {:layer 1} Inv(TopOfStack, Stack); -ensures {:layer 1} Inv(TopOfStack, Stack); -ensures {:atomic} |{ A: Stack := Add(Stack, x, TopOfStack); TopOfStack := x; return true; }|; -{ - var t: Node; - var g: bool; - var {:linear "Node"} t_lmap: lmap; - - yield; - assert {:layer 1} Inv(TopOfStack, Stack); - t_lmap := x_lmap; - while (true) - invariant {:layer 1} dom(t_lmap) == dom(x_lmap); - invariant {:layer 1} Inv(TopOfStack, Stack); - { - call t := ReadTopOfStack(); - call t_lmap := Store(t_lmap, x, t); - call g, t_lmap := TransferToStack(t, x, t_lmap); - if (g) { - assert {:layer 1} map(Stack)[x] == t; - break; - } - yield; - assert {:layer 1} dom(t_lmap) == dom(x_lmap); - assert {:layer 1} Inv(TopOfStack, Stack); - } - yield; - assert {:expand} {:layer 1} Inv(TopOfStack, Stack); -} - -procedure {:yields} {:layer 1} pop() -requires {:layer 1} Inv(TopOfStack, Stack); -ensures {:layer 1} Inv(TopOfStack, Stack); -ensures {:atomic} |{ var t: Node; - A: assume TopOfStack != null; t := TopOfStack; Used := Add(Used, t, map(Stack)[t]); TopOfStack := map(Stack)[t]; Stack := Remove(Stack, t); return true; }|; -{ - var g: bool; - var x: Node; - var t: Node; - - yield; - assert {:layer 1} Inv(TopOfStack, Stack); - while (true) - invariant {:layer 1} Inv(TopOfStack, Stack); - { - call t := ReadTopOfStack(); - if (t != null) { - call x := Load(t); - call g := TransferFromStack(t, x); - if (g) { - break; - } - } - yield; - assert {:layer 1} Inv(TopOfStack, Stack); - } - yield; - assert {:layer 1} Inv(TopOfStack, Stack); -} - -function Equal([int]bool, [int]bool) returns (bool); -function Subset([int]bool, [int]bool) returns (bool); - -function Empty() returns ([int]bool); -function Singleton(int) returns ([int]bool); -function Reachable([int,int]bool, int) returns ([int]bool); -function Union([int]bool, [int]bool) returns ([int]bool); - -axiom(forall x:int :: !Empty()[x]); - -axiom(forall x:int, y:int :: {Singleton(y)[x]} Singleton(y)[x] <==> x == y); -axiom(forall y:int :: {Singleton(y)} Singleton(y)[y]); - -axiom(forall x:int, S:[int]bool, T:[int]bool :: {Union(S,T)[x]}{Union(S,T),S[x]}{Union(S,T),T[x]} Union(S,T)[x] <==> S[x] || T[x]); - -axiom(forall S:[int]bool, T:[int]bool :: {Equal(S,T)} Equal(S,T) <==> Subset(S,T) && Subset(T,S)); -axiom(forall x:int, S:[int]bool, T:[int]bool :: {S[x],Subset(S,T)}{T[x],Subset(S,T)} S[x] && Subset(S,T) ==> T[x]); -axiom(forall S:[int]bool, T:[int]bool :: {Subset(S,T)} Subset(S,T) || (exists x:int :: S[x] && !T[x])); - -//////////////////// -// Between predicate -//////////////////// -function Between(f: [int]int, x: int, y: int, z: int) returns (bool); -function Avoiding(f: [int]int, x: int, y: int, z: int) returns (bool); - - -////////////////////////// -// Between set constructor -////////////////////////// -function BetweenSet(f: [int]int, x: int, z: int) returns ([int]bool); - -//////////////////////////////////////////////////// -// axioms relating Between and BetweenSet -//////////////////////////////////////////////////// -axiom(forall f: [int]int, x: int, y: int, z: int :: {BetweenSet(f, x, z)[y]} BetweenSet(f, x, z)[y] <==> Between(f, x, y, z)); -axiom(forall f: [int]int, x: int, y: int, z: int :: {Between(f, x, y, z), BetweenSet(f, x, z)} Between(f, x, y, z) ==> BetweenSet(f, x, z)[y]); -axiom(forall f: [int]int, x: int, z: int :: {BetweenSet(f, x, z)} Between(f, x, x, x)); -axiom(forall f: [int]int, x: int, z: int :: {BetweenSet(f, x, z)} Between(f, z, z, z)); - - -////////////////////////// -// Axioms for Between -////////////////////////// - -// reflexive -axiom(forall f: [int]int, x: int :: Between(f, x, x, x)); - -// step -axiom(forall f: [int]int, x: int, y: int, z: int, w:int :: {Between(f, y, z, w), f[x]} Between(f, x, f[x], f[x])); - -// reach -axiom(forall f: [int]int, x: int, y: int :: {f[x], Between(f, x, y, y)} Between(f, x, y, y) ==> x == y || Between(f, x, f[x], y)); - -// cycle -axiom(forall f: [int]int, x: int, y:int :: {f[x], Between(f, x, y, y)} f[x] == x && Between(f, x, y, y) ==> x == y); - -// sandwich -axiom(forall f: [int]int, x: int, y: int :: {Between(f, x, y, x)} Between(f, x, y, x) ==> x == y); - -// order1 -axiom(forall f: [int]int, x: int, y: int, z: int :: {Between(f, x, y, y), Between(f, x, z, z)} Between(f, x, y, y) && Between(f, x, z, z) ==> Between(f, x, y, z) || Between(f, x, z, y)); - -// order2 -axiom(forall f: [int]int, x: int, y: int, z: int :: {Between(f, x, y, z)} Between(f, x, y, z) ==> Between(f, x, y, y) && Between(f, y, z, z)); - -// transitive1 -axiom(forall f: [int]int, x: int, y: int, z: int :: {Between(f, x, y, y), Between(f, y, z, z)} Between(f, x, y, y) && Between(f, y, z, z) ==> Between(f, x, z, z)); - -// transitive2 -axiom(forall f: [int]int, x: int, y: int, z: int, w: int :: {Between(f, x, y, z), Between(f, y, w, z)} Between(f, x, y, z) && Between(f, y, w, z) ==> Between(f, x, y, w) && Between(f, x, w, z)); - -// transitive3 -axiom(forall f: [int]int, x: int, y: int, z: int, w: int :: {Between(f, x, y, z), Between(f, x, w, y)} Between(f, x, y, z) && Between(f, x, w, y) ==> Between(f, x, w, z) && Between(f, w, y, z)); - -// This axiom is required to deal with the incompleteness of the trigger for the reflexive axiom. -// It cannot be proved using the rest of the axioms. -axiom(forall f: [int]int, u:int, x: int :: {Between(f, u, x, x)} Between(f, u, x, x) ==> Between(f, u, u, x)); - -// relation between Avoiding and Between -axiom(forall f: [int]int, x: int, y: int, z: int :: {Avoiding(f, x, y, z)} Avoiding(f, x, y, z) <==> (Between(f, x, y, z) || (Between(f, x, y, y) && !Between(f, x, z, z)))); -axiom(forall f: [int]int, x: int, y: int, z: int :: {Between(f, x, y, z)} Between(f, x, y, z) <==> (Avoiding(f, x, y, z) && Avoiding(f, x, z, z))); - -// update -axiom(forall f: [int]int, u: int, v: int, x: int, p: int, q: int :: {Avoiding(f[p := q], u, v, x)} Avoiding(f[p := q], u, v, x) <==> ((Avoiding(f, u, v, p) && Avoiding(f, u, v, x)) || (Avoiding(f, u, p, x) && p != x && Avoiding(f, q, v, p) && Avoiding(f, q, v, x)))); - -axiom (forall f: [int]int, p: int, q: int, u: int, w: int :: {BetweenSet(f[p := q], u, w)} Avoiding(f, u, w, p) ==> Equal(BetweenSet(f[p := q], u, w), BetweenSet(f, u, w))); -axiom (forall f: [int]int, p: int, q: int, u: int, w: int :: {BetweenSet(f[p := q], u, w)} p != w && Avoiding(f, u, p, w) && Avoiding(f, q, w, p) ==> Equal(BetweenSet(f[p := q], u, w), Union(BetweenSet(f, u, p), BetweenSet(f, q, w)))); -axiom (forall f: [int]int, p: int, q: int, u: int, w: int :: {BetweenSet(f[p := q], u, w)} Avoiding(f, u, w, p) || (p != w && Avoiding(f, u, p, w) && Avoiding(f, q, w, p)) || Equal(BetweenSet(f[p := q], u, w), Empty())); \ No newline at end of file diff --git a/Test/og/treiber-stack.bpl.expect b/Test/og/treiber-stack.bpl.expect deleted file mode 100644 index be6b95ba..00000000 --- a/Test/og/treiber-stack.bpl.expect +++ /dev/null @@ -1,2 +0,0 @@ - -Boogie program verifier finished with 6 verified, 0 errors diff --git a/Test/og/wsq.bpl b/Test/og/wsq.bpl deleted file mode 100644 index f4964258..00000000 --- a/Test/og/wsq.bpl +++ /dev/null @@ -1,560 +0,0 @@ -// RUN: %boogie -noinfer -typeEncoding:m -useArrayTheory "%s" > "%t" -// RUN: %diff "%s.expect" "%t" -type Tid; -const nil: Tid; - -function {:builtin "MapConst"} MapConstBool(bool) : [Tid]bool; -function {:inline} {:linear "tid"} TidCollector(x: Tid) : [Tid]bool -{ - MapConstBool(false)[x := true] -} - - - -var {:layer 0,3} H: int; -var {:layer 0,3} T: int; -var {:layer 0,3} items: [int]int; -var {:layer 0} status: [int]bool; -var {:layer 0,3} take_in_cs: bool; -var {:layer 0,3} put_in_cs: bool; -var {:layer 0,3} steal_in_cs: [Tid]bool; -var {:layer 0,3} h_ss: [Tid]int; -var {:layer 0,3} t_ss: [Tid]int; - -const IN_Q: bool; -const NOT_IN_Q: bool; -axiom IN_Q == true; -axiom NOT_IN_Q == false; - -const unique EMPTY: int; -const unique NIL: Tid; -const unique ptTid: Tid; -axiom ptTid != NIL; - -function {:inline} stealerTid(tid: Tid):(bool) { tid != NIL && tid != ptTid } - -function {:inline} ideasInv(put_in_cs:bool, - items:[int]int, - status: [int]bool, - H:int, T:int, - take_in_cs:bool, - steal_in_cs:[Tid]bool, - h_ss:[Tid]int, - t_ss:[Tid]int - ):(bool) -{ - ( - ( (take_in_cs) && h_ss[ptTid] < t_ss[ptTid] ==> (t_ss[ptTid] == T && H <= T && - items[T] != EMPTY && status[T] == IN_Q) ) && - (put_in_cs ==> !take_in_cs) && (take_in_cs ==> !put_in_cs) && - (( (take_in_cs) && H != h_ss[ptTid]) ==> H > h_ss[ptTid]) && - (forall td:Tid :: (stealerTid(td) && steal_in_cs[td] && H == h_ss[td] && H < t_ss[td]) ==> (items[H] != EMPTY && status[H] == IN_Q)) && - (forall td:Tid :: (stealerTid(td) && steal_in_cs[td] && H != h_ss[td]) ==> H > h_ss[td]) - ) -} - -function {:inline} queueInv(steal_in_cs:[Tid]bool, - put_in_cs:bool, - take_in_cs:bool, - items:[int]int, status: [int]bool, _H:int, _T:int):(bool) -{ - ( (forall i:int :: (_H <= i && i <= _T) ==> (status[i] == IN_Q && items[i] != EMPTY)) ) -} - -function {:inline} emptyInv(put_in_cs:bool, take_in_cs:bool, items:[int]int, status:[int]bool, T:int):(bool) -{ - (forall i:int :: (i>=T && !put_in_cs && !take_in_cs) ==> status[i] == NOT_IN_Q && items[i] == EMPTY) -} - -function {:inline} putInv(items:[int]int, status: [int]bool, H:int, T:int):(bool) -{ - (forall i:int :: (H <= i && i < T) ==> (status[i] == IN_Q && items[i] != EMPTY)) -} - -function {:inline} takeInv(items:[int]int, status: [int]bool, H:int, T:int, t:int, h:int):(bool) -{ - (forall i:int :: (h <= i && i <= t) ==> (status[i] == IN_Q && - items[i] != EMPTY) && - t == T - ) -} - -procedure {:yields} {:layer 3} put({:linear "tid"} tid:Tid, task: int) -requires {:layer 3} {:expand} queueInv(steal_in_cs,put_in_cs,take_in_cs,items, status, H, T-1) && tid == ptTid && task != EMPTY && !take_in_cs && !put_in_cs; -requires {:layer 3} {:expand} ideasInv(put_in_cs,items, status, H, T, take_in_cs, steal_in_cs, h_ss, t_ss); -requires {:layer 3} {:expand} emptyInv(put_in_cs, take_in_cs, items,status,T); -ensures {:layer 3} {:expand} queueInv(steal_in_cs,put_in_cs,take_in_cs,items, status, H, T-1) && tid == ptTid && !take_in_cs && !put_in_cs; -ensures {:layer 3} {:expand} ideasInv(put_in_cs,items, status, H, T, take_in_cs, steal_in_cs, h_ss, t_ss); -ensures {:layer 3} {:expand} emptyInv(put_in_cs, take_in_cs, items,status,T); -ensures {:atomic} |{ var i: int; A: assume status[i] == NOT_IN_Q; status[i] := IN_Q; return true; }|; -{ - var t: int; - var {:ghost} oldH:int; - var {:ghost} oldT:int; - var {:ghost} oldStatusT:bool; - - - oldH := H; - oldT := T; - yield; - assert {:layer 3} {:expand} queueInv(steal_in_cs,put_in_cs,take_in_cs,items, status, H, T-1) && tid == ptTid && !take_in_cs && !put_in_cs; - assert {:layer 3} {:expand} {:expand} ideasInv(put_in_cs,items, status, H, T, take_in_cs, steal_in_cs, h_ss, t_ss); - assert {:layer 3} oldH <= H && oldT == T; - assert {:layer 3} {:expand} emptyInv(put_in_cs, take_in_cs, items,status,T); - - call t := readT_put(tid); - - oldH := H; - oldT := T; - yield; - assert {:layer 3} {:expand} queueInv(steal_in_cs,put_in_cs,take_in_cs,items, status, H, T-1) && tid == ptTid && !take_in_cs && put_in_cs; - assert {:layer 3} {:expand} ideasInv(put_in_cs,items, status, H, T, take_in_cs, steal_in_cs, h_ss, t_ss); - assert {:layer 3} tid == ptTid && t == T; - assert {:layer 3} oldH <= H && oldT == T; - assert {:layer 3} (forall i:int :: i>=T ==> status[i] == NOT_IN_Q && items[i] == EMPTY); - - call writeItems_put(tid,t, task); - - oldH := H; - oldT := T; - oldStatusT := status[T]; - yield; - assert {:layer 3} {:expand} queueInv(steal_in_cs,put_in_cs,take_in_cs,items, status, H, T) && t == T && tid == ptTid && !take_in_cs && put_in_cs; - assert {:layer 3} {:expand} ideasInv(put_in_cs,items, status, H, T, take_in_cs, steal_in_cs, h_ss, t_ss); - assert {:layer 3} items[t] == task; - assert {:layer 3} oldH <= H && oldT == T; - assert {:layer 3} (forall i:int :: i>T ==> status[i] == NOT_IN_Q && items[i] == EMPTY); - - - call writeT_put(tid, t+1); - - oldH := H; - oldT := T; - yield; - assert {:layer 3} {:expand} queueInv(steal_in_cs,put_in_cs,take_in_cs,items, status, H, T-1) && tid == ptTid && !take_in_cs && !put_in_cs; - assert {:layer 3} {:expand} ideasInv(put_in_cs,items, status, H, T, take_in_cs, steal_in_cs, h_ss, t_ss); - assert {:layer 3} T == t + 1; - assert {:layer 3} oldH <= H && oldT == T; - assert {:layer 3} {:expand} emptyInv(put_in_cs, take_in_cs, items,status,T); -} - -procedure {:yields} {:layer 3} take({:linear "tid"} tid:Tid) returns (task: int, taskstatus: bool) -requires {:layer 3} {:expand} queueInv(steal_in_cs,put_in_cs,take_in_cs,items, status, H, T-1) && tid == ptTid && !take_in_cs && !put_in_cs; -requires {:layer 3} {:expand} ideasInv(put_in_cs,items, status, H, T, take_in_cs, steal_in_cs, h_ss, t_ss); -ensures {:layer 3} queueInv(steal_in_cs,put_in_cs,take_in_cs,items, status, H, T-1) && tid == ptTid && !take_in_cs && !put_in_cs && (task != EMPTY ==> taskstatus == IN_Q); -ensures {:layer 3} ideasInv(put_in_cs,items, status, H, T, take_in_cs, steal_in_cs, h_ss, t_ss); -ensures {:atomic} |{ var i: int; A: goto B,C; B: assume status[i] == IN_Q; status[i] := NOT_IN_Q; return true; C: return true;}|; -{ - var h, t: int; - var chk: bool; - var {:ghost} oldH:int; - var {:ghost} oldT:int; - - oldH := H; - oldT := T; - yield; - assert {:layer 3} queueInv(steal_in_cs,put_in_cs,take_in_cs,items, status, H, T-1) && tid == ptTid && !take_in_cs && !put_in_cs; - assert {:layer 3} ideasInv(put_in_cs,items, status, H, T, take_in_cs, steal_in_cs, h_ss, t_ss); - assert {:layer 3} oldH <= H && oldT == T; - - LOOP_ENTRY_1: - - while(true) - invariant {:layer 3} queueInv(steal_in_cs,put_in_cs,take_in_cs,items, status, H, T-1) && tid == ptTid && !take_in_cs && !put_in_cs; - invariant {:layer 3} ideasInv(put_in_cs,items, status, H, T, take_in_cs, steal_in_cs, h_ss, t_ss); - { - - oldH := H; - oldT := T; - yield; - assert {:layer 3} queueInv(steal_in_cs,put_in_cs,take_in_cs,items, status, H, T-1) && tid == ptTid && !take_in_cs && !put_in_cs; - assert {:layer 3} ideasInv(put_in_cs,items, status, H, T, take_in_cs, steal_in_cs, h_ss, t_ss); - assert {:layer 3} oldH <= H && oldT == T; - - call t := readT_take_init(tid); - - oldH := H; - oldT := T; - yield; - assert {:layer 3} queueInv(steal_in_cs,put_in_cs,take_in_cs,items, status, H, T-1) && tid == ptTid && !take_in_cs && !put_in_cs; - assert {:layer 3} ideasInv(put_in_cs,items, status, H, T, take_in_cs, steal_in_cs, h_ss, t_ss); - assert {:layer 3} t == T; - assert {:layer 3} items[t-1] == EMPTY ==> H > t-1; - assert {:layer 3} oldH <= H && oldT == T; - - t := t-1; - call writeT_take(tid, t); - - oldH := H; - oldT := T; - yield; - assert {:layer 3} queueInv(steal_in_cs,put_in_cs,take_in_cs,items, status, H, T) && tid == ptTid && !take_in_cs && !put_in_cs && t_ss[tid] == t; - assert {:layer 3} ideasInv(put_in_cs,items, status, H, T, take_in_cs, steal_in_cs, h_ss, t_ss); - assert {:layer 3} t == T; - assert {:layer 3} items[t] == EMPTY ==> H > t; - assert {:layer 3} oldH <= H && oldT == T; - - call h := readH_take(tid); - - oldH := H; - oldT := T; - yield; - assert {:layer 3} queueInv(steal_in_cs,put_in_cs,take_in_cs,items, status, H, T) && tid == ptTid && take_in_cs && !put_in_cs && h_ss[tid] == h && t_ss[tid] == t; - assert {:layer 3} {:expand} ideasInv(put_in_cs,items, status, H, T, take_in_cs, steal_in_cs, h_ss, t_ss); - assert {:layer 3} t == T; - assert {:layer 3} h <= H; - assert {:layer 3} items[t] == EMPTY ==> H > t; - assert {:layer 3} oldH <= H; - assert {:layer 3} oldT == T; - assert {:layer 3} h <= H; - assert {:layer 3} oldH == h; - - if(t= h; - assert {:layer 3} queueInv(steal_in_cs,put_in_cs,take_in_cs,items, status, H, T) && tid == ptTid && take_in_cs && h_ss[tid] == h && t_ss[tid] == t; - assert {:layer 3} ideasInv(put_in_cs,items, status, H, T, take_in_cs, steal_in_cs, h_ss, t_ss); - assert {:layer 3} t == T && task == items[T]; - assert {:layer 3} T > H ==> items[T] != EMPTY; - assert {:layer 3} oldH <= H && oldT == T && !put_in_cs && take_in_cs; - - if(t>h) { - call takeExitCS(tid); - - oldH := H; - oldT := T; - yield; - assert {:layer 3} queueInv(steal_in_cs,put_in_cs,take_in_cs,items, status, H, T-1) && tid == ptTid && !take_in_cs && h_ss[tid] == h && t_ss[tid] == t; - assert {:layer 3} ideasInv(put_in_cs,items, status, H, T, take_in_cs, steal_in_cs, h_ss, t_ss); - assert {:layer 3} t == T && task == items[t] && task != EMPTY && taskstatus == IN_Q; - assert {:layer 3} oldH <= H && oldT == T && !put_in_cs && !take_in_cs; - return; - } - call writeT_take_eq(tid, h+1); - oldH := H; - oldT := T; - - yield; - assert {:layer 3} queueInv(steal_in_cs,put_in_cs,take_in_cs,items, status, H, T-1) && tid == ptTid && h_ss[tid] == h && t_ss[tid] == t; - assert {:layer 3} ideasInv(put_in_cs,items, status, H, T, take_in_cs, steal_in_cs, h_ss, t_ss); - assert {:layer 3} T == h + 1; - assert {:layer 3} oldH <= H; - assert {:layer 3} oldT == T; - assert {:layer 3} task == items[t]; - assert {:layer 3} !put_in_cs; - - call chk := CAS_H_take(tid, h,h+1); - - - oldH := H; - oldT := T; - yield; - assert {:layer 3} chk ==> (h+1 == oldH && h_ss[tid] == oldH -1 && task != EMPTY); - assert {:layer 3} queueInv(steal_in_cs,put_in_cs,take_in_cs,items, status, H, T-1) && tid == ptTid && h_ss[tid] == h && t_ss[tid] == t; - assert {:layer 3} ideasInv(put_in_cs,items, status, H, T, take_in_cs, steal_in_cs, h_ss, t_ss); - assert {:layer 3} h+1 == T; - assert {:layer 3} task == items[t]; - assert {:layer 3} !take_in_cs; - assert {:layer 3} !put_in_cs; - assert {:layer 3} oldH <= H && oldT == T; - - if(!chk) { - - oldH := H; - oldT := T; - yield; - assert {:layer 3} queueInv(steal_in_cs,put_in_cs,take_in_cs,items, status, H, T-1) && tid == ptTid && h_ss[tid] == h && t_ss[tid] == t; - assert {:layer 3} ideasInv(put_in_cs,items, status, H, T, take_in_cs, steal_in_cs, h_ss, t_ss); - assert {:layer 3} h+1 == T && task == items[t] && !take_in_cs && !put_in_cs; - assert {:layer 3} oldH <= H && oldT == T; - - goto LOOP_ENTRY_1; - } - - oldH := H; - oldT := T; - yield; - assert {:layer 3} queueInv(steal_in_cs,put_in_cs,take_in_cs,items, status, H, T-1) && tid == ptTid && h_ss[tid] == h && t_ss[tid] == t; - assert {:layer 3} ideasInv(put_in_cs,items, status, H, T, take_in_cs, steal_in_cs, h_ss, t_ss); - assert {:layer 3} h+1 == T && task == items[t] && !take_in_cs && !put_in_cs; - assert {:layer 3} oldH <= H && oldT == T && task != EMPTY && taskstatus == IN_Q; - - return; - } - - oldH := H; - oldT := T; - yield; - assert {:layer 3} queueInv(steal_in_cs,put_in_cs,take_in_cs,items, status, H, T) && tid == ptTid && !put_in_cs; - assert {:layer 3} ideasInv(put_in_cs,items, status, H, T, take_in_cs, steal_in_cs, h_ss, t_ss); - assert {:layer 3} oldH <= H && oldT == T; - -} - - -procedure {:yields}{:layer 3} steal({:linear "tid"} tid:Tid) returns (task: int, taskstatus: bool) -requires {:layer 3} queueInv(steal_in_cs,put_in_cs,take_in_cs,items, status, H, T-1) && stealerTid(tid) && - !steal_in_cs[tid]; -requires {:layer 3} ideasInv(put_in_cs,items, status, H, T, take_in_cs, steal_in_cs, h_ss, t_ss); -ensures {:layer 3} queueInv(steal_in_cs,put_in_cs,take_in_cs,items, status, H, T-1) && - !steal_in_cs[tid] && (task != EMPTY ==> taskstatus == IN_Q); -ensures {:layer 3} ideasInv(put_in_cs,items, status, H, T, take_in_cs, steal_in_cs, h_ss, t_ss); -ensures {:atomic} |{ var i: int; A: goto B,C; B: assume status[i] == IN_Q; status[i] := NOT_IN_Q; return true; C: return true;}|; -{ - var h, t: int; - var chk: bool; - var {:ghost} oldH:int; - var {:ghost} oldT:int; - - oldH := H; - oldT := T; - yield; - assert {:layer 3} stealerTid(tid); - assert {:layer 3} queueInv(steal_in_cs,put_in_cs,take_in_cs,items, status, H, T-1); - assert {:layer 3} ideasInv(put_in_cs,items, status, H, T, take_in_cs, steal_in_cs, h_ss, t_ss); - assert {:layer 3} oldH <= H; - assert {:layer 3} !steal_in_cs[tid]; - - LOOP_ENTRY_2: - while(true) - invariant {:layer 3} stealerTid(tid); - invariant {:layer 3} queueInv(steal_in_cs,put_in_cs,take_in_cs,items, status, H, T-1); - invariant {:layer 3} ideasInv(put_in_cs,items, status, H, T, take_in_cs, steal_in_cs, h_ss, t_ss); - invariant {:layer 3} !steal_in_cs[tid]; - { - oldH := H; - oldT := T; - yield; - assert {:layer 3} stealerTid(tid); - assert {:layer 3} queueInv(steal_in_cs,put_in_cs,take_in_cs,items, status, H, T-1); - assert {:layer 3} ideasInv(put_in_cs,items, status, H, T, take_in_cs, steal_in_cs, h_ss, t_ss); - assert {:layer 3} oldH <= H; - assert {:layer 3} !steal_in_cs[tid]; - - call h := readH_steal(tid); - - oldH := H; - oldT := T; - yield; - assert {:layer 3} H >= h; - assert {:layer 3} !steal_in_cs[tid]; - assert {:layer 3} h_ss[tid] == h; - assert {:layer 3} queueInv(steal_in_cs,put_in_cs,take_in_cs,items, status, H, T-1); - assert {:layer 3} {:expand} ideasInv(put_in_cs,items, status, H, T, take_in_cs, steal_in_cs, h_ss, t_ss); - assert {:layer 3} oldH <= H; - - call t := readT_steal(tid); - - - oldH := H; - oldT := T; - yield; - assert {:layer 3} steal_in_cs[tid]; - assert {:layer 3} stealerTid(tid) && H >= h && steal_in_cs[tid] && h_ss[tid] == h; - assert {:layer 3} queueInv(steal_in_cs,put_in_cs,take_in_cs,items, status, H, T-1); - assert {:layer 3} ideasInv(put_in_cs,items, status, H, T, take_in_cs, steal_in_cs, h_ss, t_ss); - assert {:layer 3} oldH <= H && t == t_ss[tid]; - assert {:layer 3} (h < t && take_in_cs && (h_ss[ptTid] < t_ss[ptTid]) && h == H) ==> (H < T); - assert {:layer 3} H >= h; - - if( h>= t) { - - task := EMPTY; - call stealExitCS(tid); - - oldH := H; - oldT := T; - yield; - assert {:layer 3} !steal_in_cs[tid]; - assert {:layer 3} stealerTid(tid) && !steal_in_cs[tid] && h_ss[tid] == h; - assert {:layer 3} queueInv(steal_in_cs,put_in_cs,take_in_cs,items, status, H, T-1); - assert {:layer 3} ideasInv(put_in_cs,items, status, H, T, take_in_cs, steal_in_cs, h_ss, t_ss); - assert {:layer 3} oldH <= H; - return; - } - - call task, taskstatus := readItems(tid, h); - - - oldH := H; - oldT := T; - yield; - assert {:layer 3} stealerTid(tid) && steal_in_cs[tid] && h_ss[tid] == h; - assert {:layer 3} queueInv(steal_in_cs,put_in_cs,take_in_cs,items, status, H, T-1); - assert {:layer 3} ideasInv(put_in_cs,items, status, H, T, take_in_cs, steal_in_cs, h_ss, t_ss); - assert {:layer 3} oldH <= H; - assert {:layer 3} oldH == H && H == h && h_ss[tid] == h ==> task != EMPTY; - assert {:layer 3} (take_in_cs && (h_ss[ptTid] < t_ss[ptTid]) && h == H) ==> (H < T); - assert {:layer 3} h == H ==> status[H] == IN_Q; - - call chk := CAS_H_steal(tid, h,h+1); - - oldH := H; - oldT := T; - yield; - assert {:layer 3} h_ss[tid] == h; - assert {:layer 3} chk ==> (h+1 == oldH && h_ss[tid] == h && task != EMPTY && taskstatus == IN_Q); - assert {:layer 3} (take_in_cs && (h_ss[ptTid] < t_ss[ptTid]) && chk) ==> ((oldH-1) < T); - assert {:layer 3} {:expand} ideasInv(put_in_cs,items, status, H, T, take_in_cs, steal_in_cs, h_ss, t_ss); - assert {:layer 3} stealerTid(tid) && !steal_in_cs[tid]; - assert {:layer 3} queueInv(steal_in_cs,put_in_cs,take_in_cs,items, status, H, T-1); - assert {:layer 3} oldH <= H; - - if(!chk) { - goto LOOP_ENTRY_2; - } - - oldH := H; - oldT := T; - yield; - assert {:layer 3} stealerTid(tid) && !steal_in_cs[tid]; - assert {:layer 3} queueInv(steal_in_cs,put_in_cs,take_in_cs,items, status, H, T-1); - assert {:layer 3} ideasInv(put_in_cs,items, status, H, T, take_in_cs, steal_in_cs, h_ss, t_ss); - assert {:layer 3} oldH <= H && task != EMPTY; - return; - } - - oldH := H; - oldT := T; - yield; - assert {:layer 3} chk && task != EMPTY; - assert {:layer 3} stealerTid(tid) && !steal_in_cs[tid]; - assert {:layer 3} oldH <= H; -} - -procedure {:yields}{:layer 0,3} readH_take({:linear "tid"} tid:Tid) returns (y: int); -ensures {:atomic} |{A: assert tid == ptTid; - y := H; - take_in_cs := true; - h_ss[tid] := H; - return true;}|; - -procedure {:yields}{:layer 0,3} readH_steal({:linear "tid"} tid:Tid) returns (y: int); -ensures {:atomic} |{A: assert stealerTid(tid); - assert !steal_in_cs[tid]; - y := H; - h_ss[tid] := H; - return true;}|; - -procedure {:yields}{:layer 0,3} readT_take_init({:linear "tid"} tid:Tid) returns (y: int); -ensures {:atomic} |{A: assert tid != NIL; assert tid == ptTid; y := T; return true;}|; - -procedure {:yields}{:layer 0,3} readT_put({:linear "tid"} tid:Tid) returns (y: int); -ensures {:atomic} |{A: assert tid != NIL; - assert tid == ptTid; - put_in_cs := true; - y := T; - return true;}|; - -procedure {:yields}{:layer 0,3} readT_steal({:linear "tid"} tid:Tid) returns (y: int); -ensures {:atomic} |{A: assert tid != NIL; - assert stealerTid(tid); - assert !steal_in_cs[tid]; - y := T; - t_ss[tid] := T; - steal_in_cs[tid] := true; - return true;}|; - -procedure {:yields}{:layer 0,3} readItems({:linear "tid"} tid:Tid, ind: int) returns (y: int, b:bool); -ensures {:atomic} |{A: y := items[ind]; b := status[ind]; return true; }|; - -procedure {:yields}{:layer 0,3} writeT_put({:linear "tid"} tid:Tid, val: int); -ensures {:atomic} |{A: assert tid == ptTid; - T := T+1; - put_in_cs := false; - return true; }|; - -procedure {:yields}{:layer 0,3} writeT_take({:linear "tid"} tid:Tid, val: int); -ensures {:atomic} |{A: assert tid == ptTid; - T := val; - t_ss[tid] := val; - return true; }|; - -procedure {:yields}{:layer 0,3} writeT_take_abort({:linear "tid"} tid:Tid, val: int); -ensures {:atomic} |{A: assert tid == ptTid; - assert take_in_cs; - T := val; - take_in_cs := false; - return true; }|; - -procedure {:yields}{:layer 0,3} writeT_take_eq({:linear "tid"} tid:Tid, val: int); -ensures {:atomic} |{A: assert tid == ptTid; - T := val; - return true; }|; - -procedure {:yields}{:layer 0,3} takeExitCS({:linear "tid"} tid:Tid); -ensures {:atomic} |{A: assert tid == ptTid; - take_in_cs := false; - return true; }|; - -procedure {:yields}{:layer 0,3} stealExitCS({:linear "tid"} tid:Tid); -ensures {:atomic} |{A: assert stealerTid(tid); - assert steal_in_cs[tid]; - steal_in_cs[tid] := false; - return true; }|; - - -procedure {:yields}{:layer 0,3} writeItems({:linear "tid"} tid:Tid, idx: int, val: int); -ensures {:atomic} |{A: assert tid == ptTid; - assert val != EMPTY; - items[idx] := val; - status[idx] := IN_Q; - return true; }|; - - -procedure {:yields}{:layer 0,3} writeItems_put({:linear "tid"} tid:Tid, idx: int, val: int); -ensures {:atomic} |{A: assert tid == ptTid; - assert val != EMPTY; - items[idx] := val; - status[idx] := IN_Q; - return true; }|; - -procedure {:yields}{:layer 0,3} CAS_H_take({:linear "tid"} tid:Tid, prevVal :int, val: int) - returns (result: bool); -ensures {:atomic} |{ A: assert tid == ptTid; - goto B, C; - B: assume H == prevVal; - take_in_cs := false; - status[H] := NOT_IN_Q; - H := H+1; - result := true; - return true; - C: assume H != prevVal; result := false; - take_in_cs := false; - return true; -}|; - -procedure {:yields}{:layer 0,3} CAS_H_steal({:linear "tid"} tid:Tid, prevVal :int, val: int) - returns (result: bool); -ensures {:atomic} |{ A: assert stealerTid(tid); - goto B, C; - B: assume H == prevVal; - status[H] := NOT_IN_Q; - H := H+1; - result := true; - steal_in_cs[tid] := false; - return true; - C: assume H != prevVal; - result := false; - steal_in_cs[tid] := false; - return true; - }|; \ No newline at end of file diff --git a/Test/og/wsq.bpl.expect b/Test/og/wsq.bpl.expect deleted file mode 100644 index 5b2909f1..00000000 --- a/Test/og/wsq.bpl.expect +++ /dev/null @@ -1,2 +0,0 @@ - -Boogie program verifier finished with 3 verified, 0 errors -- cgit v1.2.3