From 28d4e2ad2598ff377f121ff2a2a9b0794f386110 Mon Sep 17 00:00:00 2001 From: qadeer Date: Sun, 4 May 2014 21:17:12 -0700 Subject: second checkpoint --- Test/linear/Answer | 10 ++-- Test/og/Answer | 90 ++++++++++++++--------------- Test/og/DeviceCache.bpl | 138 ++++++++++++++++++++++----------------------- Test/og/FlanaganQadeer.bpl | 1 + Test/og/lock.bpl | 4 +- Test/og/lock2.bpl | 5 +- Test/og/multiset.bpl | 2 + Test/og/parallel1.bpl | 3 +- Test/og/parallel2.bpl | 6 +- Test/og/parallel5.bpl | 8 +-- Test/og/ticket.bpl | 8 ++- 11 files changed, 136 insertions(+), 139 deletions(-) (limited to 'Test') diff --git a/Test/linear/Answer b/Test/linear/Answer index 9fabc440..ff1246e6 100644 --- a/Test/linear/Answer +++ b/Test/linear/Answer @@ -10,11 +10,11 @@ typecheck.bpl(51,4): Error: Only variable can be passed to linear parameter b typecheck.bpl(53,4): Error: The domains of formal and actual parameters must be the same typecheck.bpl(55,4): Error: The domains of formal and actual parameters must be the same typecheck.bpl(57,4): Error: Only a linear argument can be passed to linear parameter a -typecheck.bpl(61,4): Error: Linear variable a can occur only once as an input parameter of a parallel call -typecheck.bpl(67,0): Error: Output variable d must be available at a return -typecheck.bpl(76,0): Error: Global variable g must be available at a return -typecheck.bpl(81,7): Error: unavailable source for a linear read -typecheck.bpl(82,0): Error: Output variable r must be available at a return +typecheck.bpl(62,4): Error: Linear variable a can occur only once as an input parameter of a parallel call +typecheck.bpl(69,0): Error: Output variable d must be available at a return +typecheck.bpl(78,0): Error: Global variable g must be available at a return +typecheck.bpl(83,7): Error: unavailable source for a linear read +typecheck.bpl(84,0): Error: Output variable r must be available at a return 15 type checking errors detected in typecheck.bpl -------------------- list.bpl -------------------- diff --git a/Test/og/Answer b/Test/og/Answer index a02a2838..b82acad4 100644 --- a/Test/og/Answer +++ b/Test/og/Answer @@ -1,59 +1,58 @@ -------------------- foo.bpl -------------------- -foo.bpl(14,3): Error: Non-interference check failed +foo.bpl(28,3): Error: Non-interference check failed Execution trace: - foo.bpl(6,5): anon0 - (0,0): inline$Impl_YieldChecker_PC_0$0$L0 + foo.bpl(5,3): anon0 + foo.bpl(5,3): anon0$1 + foo.bpl(12,3): inline$Incr_1$0$this_A + (0,0): inline$Impl_YieldChecker_PC_1$1$L0 -Boogie program verifier finished with 4 verified, 1 error +Boogie program verifier finished with 9 verified, 1 error -------------------- bar.bpl -------------------- -bar.bpl(13,3): Error: Non-interference check failed +bar.bpl(26,3): Error: Non-interference check failed Execution trace: - bar.bpl(6,5): anon0 - (0,0): inline$Impl_YieldChecker_PC_0$0$L0 -bar.bpl(13,3): Error: Non-interference check failed + bar.bpl(5,3): anon0 + bar.bpl(5,3): anon0$1 + bar.bpl(12,3): inline$Incr_1$0$this_A + (0,0): inline$Impl_YieldChecker_PC_1$1$L0 +bar.bpl(26,3): Error: Non-interference check failed Execution trace: - bar.bpl(23,5): anon0 - (0,0): inline$Impl_YieldChecker_PC_0$0$L0 + bar.bpl(36,3): anon0 + bar.bpl(36,3): anon0$1 + (0,0): inline$Impl_YieldChecker_PC_1$1$L0 -Boogie program verifier finished with 3 verified, 2 errors +Boogie program verifier finished with 8 verified, 2 errors -------------------- one.bpl -------------------- -Boogie program verifier finished with 2 verified, 0 errors +Boogie program verifier finished with 3 verified, 0 errors -------------------- parallel1.bpl -------------------- -parallel1.bpl(10,1): Error: Non-interference check failed -Execution trace: - parallel1.bpl(6,5): anon0 - (0,0): inline$Proc_YieldChecker_PC_0$0$L0 -parallel1.bpl(14,3): Error: Non-interference check failed +parallel1.bpl(28,3): Error: Non-interference check failed Execution trace: - parallel1.bpl(6,5): anon0 - (0,0): inline$Impl_YieldChecker_PC_0$0$L0 + parallel1.bpl(5,3): anon0 + parallel1.bpl(5,3): anon0$1 + parallel1.bpl(12,3): inline$Incr_1$0$this_A + (0,0): inline$Impl_YieldChecker_PC_1$1$L0 -Boogie program verifier finished with 3 verified, 2 errors +Boogie program verifier finished with 7 verified, 1 error -------------------- linear-set.bpl -------------------- -Boogie program verifier finished with 2 verified, 0 errors +Boogie program verifier finished with 4 verified, 0 errors -------------------- linear-set2.bpl -------------------- -Boogie program verifier finished with 2 verified, 0 errors +Boogie program verifier finished with 4 verified, 0 errors -------------------- FlanaganQadeer.bpl -------------------- -Boogie program verifier finished with 3 verified, 0 errors - --------------------- DeviceCacheSimplified.bpl -------------------- - -Boogie program verifier finished with 5 verified, 0 errors +Boogie program verifier finished with 6 verified, 0 errors -------------------- parallel2.bpl -------------------- -Boogie program verifier finished with 4 verified, 0 errors +Boogie program verifier finished with 8 verified, 0 errors -------------------- parallel4.bpl -------------------- parallel4.bpl(24,3): Error BP5001: This assertion might not hold. @@ -61,40 +60,35 @@ Execution trace: (0,0): og_init parallel4.bpl(22,5): anon0$1 -Boogie program verifier finished with 2 verified, 1 error +Boogie program verifier finished with 5 verified, 1 error -------------------- parallel5.bpl -------------------- -Boogie program verifier finished with 4 verified, 0 errors +Boogie program verifier finished with 8 verified, 0 errors -------------------- akash.bpl -------------------- -Boogie program verifier finished with 3 verified, 0 errors +Boogie program verifier finished with 6 verified, 0 errors -------------------- t1.bpl -------------------- -t1.bpl(51,5): Error: Non-interference check failed +t1.bpl(58,5): Error: Non-interference check failed Execution trace: (0,0): og_init - (0,0): inline$Impl_YieldChecker_A_0$0$L1 + t1.bpl(78,13): anon0 + t1.bpl(78,13): anon0$1 + (0,0): inline$SetG_1$0$Entry + t1.bpl(78,13): anon0$2 + (0,0): inline$Impl_YieldChecker_A_1$1$L2 -Boogie program verifier finished with 2 verified, 1 error +Boogie program verifier finished with 5 verified, 1 error -------------------- new1.bpl -------------------- -Boogie program verifier finished with 2 verified, 0 errors +Boogie program verifier finished with 4 verified, 0 errors -------------------- perm.bpl -------------------- -Boogie program verifier finished with 2 verified, 0 errors - --------------------- async.bpl -------------------- -async.bpl(14,1): Error: Non-interference check failed -Execution trace: - async.bpl(7,3): anon0 - async.bpl(7,3): anon0$1 - (0,0): inline$Proc_YieldChecker_P_0$1$L0 - -Boogie program verifier finished with 1 verified, 1 error +Boogie program verifier finished with 4 verified, 0 errors -------------------- DeviceCache.bpl -------------------- @@ -106,11 +100,11 @@ Boogie program verifier finished with 28 verified, 0 errors -------------------- lock.bpl -------------------- -Boogie program verifier finished with 6 verified, 0 errors +Boogie program verifier finished with 8 verified, 0 errors -------------------- lock2.bpl -------------------- -Boogie program verifier finished with 6 verified, 0 errors +Boogie program verifier finished with 8 verified, 0 errors -------------------- multiset.bpl -------------------- @@ -118,4 +112,4 @@ Boogie program verifier finished with 85 verified, 0 errors -------------------- civl-paper.bpl -------------------- -Boogie program verifier finished with 29 verified, 0 errors +Boogie program verifier finished with 28 verified, 0 errors diff --git a/Test/og/DeviceCache.bpl b/Test/og/DeviceCache.bpl index 0f6383ef..23f36ae5 100644 --- a/Test/og/DeviceCache.bpl +++ b/Test/og/DeviceCache.bpl @@ -22,18 +22,20 @@ function {:inline} Inv(ghostLock: X, currsize: int, newsize: int) : (bool) (ghostLock == nil <==> currsize == newsize) } -procedure {:yields} {:phase 1} YieldToReadCache({:linear "tid"} tid': X) returns ({:linear "tid"} tid: X) -requires {:phase 1} Inv(ghostLock, currsize, newsize) && tid' != nil; -ensures {:phase 1} Inv(ghostLock, currsize, newsize) && tid != nil && tid == tid' && old(currsize) <= currsize; +procedure {:yields} {:phase 1} YieldToReadCache({:cnst "tid"} tid: X) +requires {:phase 1} Inv(ghostLock, currsize, newsize) && tid != nil; +ensures {:phase 1} Inv(ghostLock, currsize, newsize) && old(currsize) <= currsize; { - tid := tid'; + yield; + assert {:phase 1} Inv(ghostLock, currsize, newsize) && old(currsize) <= currsize; } -procedure {:yields} {:phase 1} YieldToWriteCache({:linear "tid"} tid': X) returns ({:linear "tid"} tid: X) -requires {:phase 1} Inv(ghostLock, currsize, newsize) && ghostLock == tid' && tid' != nil; -ensures {:phase 1} Inv(ghostLock, currsize, newsize) && ghostLock == tid && tid != nil && tid == tid' && old(currsize) == currsize && old(newsize) == newsize; +procedure {:yields} {:phase 1} YieldToWriteCache({:cnst "tid"} tid: X) +requires {:phase 1} Inv(ghostLock, currsize, newsize) && ghostLock == tid && tid != nil; +ensures {:phase 1} Inv(ghostLock, currsize, newsize) && ghostLock == tid && old(currsize) == currsize && old(newsize) == newsize; { - tid := tid'; + yield; + assert {:phase 1} Inv(ghostLock, currsize, newsize) && tid != nil && ghostLock == tid && old(currsize) == currsize && old(newsize) == newsize; } procedure Allocate({:linear "tid"} xls': [X]bool) returns ({:linear "tid"} xls: [X]bool, {:linear "tid"} xl: X); @@ -47,7 +49,8 @@ requires {:phase 1} xls' == mapconstbool(true); yield; - call xls := Init(xls'); + xls := xls'; + call Init(xls); yield; assert {:phase 1} Inv(ghostLock, currsize, newsize); @@ -64,134 +67,127 @@ requires {:phase 1} xls' == mapconstbool(true); } } -procedure {:yields} {:phase 1} Thread({:linear "tid"} tid': X) -requires {:phase 1} tid' != nil; +procedure {:yields} {:phase 1} Thread({:cnst "tid"} tid: X) +requires {:phase 1} tid != nil; requires {:phase 1} Inv(ghostLock, currsize, newsize); { var start, size, bytesRead: int; - var {:linear "tid"} tid: X; - tid := tid'; havoc start, size; assume (0 <= start && 0 <= size); call bytesRead := Read(tid, start, size); } -procedure {:yields} {:phase 1} Read({:linear "tid"} tid': X, start : int, size : int) returns (bytesRead : int) -requires {:phase 1} tid' != nil; +procedure {:yields} {:phase 1} Read({:cnst "tid"} tid: X, start : int, size : int) returns (bytesRead : int) +requires {:phase 1} tid != nil; requires {:phase 1} 0 <= start && 0 <= size; requires {:phase 1} Inv(ghostLock, currsize, newsize); ensures {:phase 1} 0 <= bytesRead && bytesRead <= size; { var i, tmp: int; - var {:linear "tid"} tid: X; - tid := tid'; - par tid := YieldToReadCache(tid); + par YieldToReadCache(tid); bytesRead := size; - call tid := acquire(tid); - call tid, i := ReadCurrsize(tid); - call tid, tmp := ReadNewsize(tid); + call acquire(tid); + call i := ReadCurrsize(tid); + call tmp := ReadNewsize(tid); if (start + size <= i) { - call tid := release(tid); + call release(tid); goto COPY_TO_BUFFER; } else if (tmp > i) { bytesRead := if (start <= i) then (i - start) else 0; - call tid := release(tid); + call release(tid); goto COPY_TO_BUFFER; } else { - call tid := WriteNewsize(tid, start + size); - call tid := release(tid); + call WriteNewsize(tid, start + size); + call release(tid); goto READ_DEVICE; } READ_DEVICE: - par tid := YieldToWriteCache(tid); - call tid := WriteCache(tid, start + size); - par tid := YieldToWriteCache(tid); - call tid := acquire(tid); - call tid, tmp := ReadNewsize(tid); - call tid := WriteCurrsize(tid, tmp); - call tid := release(tid); + 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 tid := YieldToReadCache(tid); - call tid := ReadCache(tid, start, bytesRead); + par YieldToReadCache(tid); + call ReadCache(tid, start, bytesRead); } -procedure {:yields} {:phase 1} WriteCache({:linear "tid"} tid': X, index: int) returns ({:linear "tid"} tid: X) +procedure {:yields} {:phase 1} WriteCache({:cnst "tid"} tid: X, index: int) requires {:phase 1} Inv(ghostLock, currsize, newsize); -requires {:phase 1} ghostLock == tid' && tid' != nil; -ensures {:phase 1} tid == tid' && ghostLock == tid; +requires {:phase 1} ghostLock == tid && tid != nil; +ensures {:phase 1} ghostLock == tid; ensures {:phase 1} Inv(ghostLock, currsize, newsize) && old(currsize) == currsize && old(newsize) == newsize; { var j: int; - tid := tid'; - par tid := YieldToWriteCache(tid); - call tid, j := ReadCurrsize(tid); + par YieldToWriteCache(tid); + call j := ReadCurrsize(tid); while (j < index) - invariant {:phase 1} ghostLock == tid && currsize <= j && tid == tid'; + invariant {:phase 1} ghostLock == tid && currsize <= j && tid == tid; invariant {:phase 1} Inv(ghostLock, currsize, newsize) && old(currsize) == currsize && old(newsize) == newsize; { - par tid := YieldToWriteCache(tid); - call tid := WriteCacheEntry(tid, j); + par YieldToWriteCache(tid); + call WriteCacheEntry(tid, j); j := j + 1; } - par tid := YieldToWriteCache(tid); + par YieldToWriteCache(tid); } -procedure {:yields} {:phase 1} ReadCache({:linear "tid"} tid': X, start: int, bytesRead: int) returns ({:linear "tid"} tid: X) +procedure {:yields} {:phase 1} ReadCache({:cnst "tid"} tid: X, start: int, bytesRead: int) requires {:phase 1} Inv(ghostLock, currsize, newsize); -requires {:phase 1} tid' != nil; +requires {:phase 1} tid != nil; requires {:phase 1} 0 <= start && 0 <= bytesRead; requires {:phase 1} (bytesRead == 0 || start + bytesRead <= currsize); -ensures {:phase 1} tid == tid'; ensures {:phase 1} Inv(ghostLock, currsize, newsize); { var j: int; - tid := tid'; - par tid := YieldToReadCache(tid); + par YieldToReadCache(tid); j := 0; while(j < bytesRead) invariant {:phase 1} 0 <= j; invariant {:phase 1} bytesRead == 0 || start + bytesRead <= currsize; - invariant {:phase 1} Inv(ghostLock, currsize, newsize) && tid == tid'; + invariant {:phase 1} Inv(ghostLock, currsize, newsize); { assert {:phase 1} start + j < currsize; - call tid := ReadCacheEntry(tid, start + j); + call ReadCacheEntry(tid, start + j); j := j + 1; - par tid := YieldToReadCache(tid); + par YieldToReadCache(tid); } - par tid := YieldToReadCache(tid); + par YieldToReadCache(tid); } -procedure {:yields} {:phase 0,1} Init({:linear "tid"} xls':[X]bool) returns ({:linear "tid"} xls:[X]bool); -ensures {:atomic} |{ A: assert xls' == mapconstbool(true); xls := xls'; currsize := 0; newsize := 0; lock := nil; ghostLock := nil; return true; }|; +procedure {:yields} {:phase 0,1} Init({:cnst "tid"} xls:[X]bool); +ensures {:atomic} |{ A: assert xls == mapconstbool(true); currsize := 0; newsize := 0; lock := nil; ghostLock := nil; return true; }|; -procedure {:yields} {:phase 0,1} ReadCurrsize({:linear "tid"} tid': X) returns ({:linear "tid"} tid: X, val: int); -ensures {:right} |{A: assert tid' != nil; assert lock == tid' || ghostLock == tid'; tid := tid'; val := currsize; return true; }|; +procedure {:yields} {:phase 0,1} ReadCurrsize({:cnst "tid"} tid: X) returns (val: int); +ensures {:right} |{A: assert tid != nil; assert lock == tid || ghostLock == tid; val := currsize; return true; }|; -procedure {:yields} {:phase 0,1} ReadNewsize({:linear "tid"} tid': X) returns ({:linear "tid"} tid: X, val: int); -ensures {:right} |{A: assert tid' != nil; assert lock == tid' || ghostLock == tid'; tid := tid'; val := newsize; return true; }|; +procedure {:yields} {:phase 0,1} ReadNewsize({:cnst "tid"} tid: X) returns (val: int); +ensures {:right} |{A: assert tid != nil; assert lock == tid || ghostLock == tid; val := newsize; return true; }|; -procedure {:yields} {:phase 0,1} WriteNewsize({:linear "tid"} tid': X, val: int) returns ({:linear "tid"} tid: X); -ensures {:atomic} |{A: assert tid' != nil; assert lock == tid' && ghostLock == nil; tid := tid'; newsize := val; ghostLock := tid; return true; }|; +procedure {:yields} {:phase 0,1} WriteNewsize({:cnst "tid"} tid: X, val: int); +ensures {:atomic} |{A: assert tid != nil; assert lock == tid && ghostLock == nil; newsize := val; ghostLock := tid; return true; }|; -procedure {:yields} {:phase 0,1} WriteCurrsize({:linear "tid"} tid': X, val: int) returns ({:linear "tid"} tid: X); -ensures {:atomic} |{A: assert tid' != nil; assert lock == tid' && ghostLock == tid'; tid := tid'; currsize := val; ghostLock := nil; return true; }|; +procedure {:yields} {:phase 0,1} WriteCurrsize({:cnst "tid"} tid: X, val: int); +ensures {:atomic} |{A: assert tid != nil; assert lock == tid && ghostLock == tid; currsize := val; ghostLock := nil; return true; }|; -procedure {:yields} {:phase 0,1} ReadCacheEntry({:linear "tid"} tid': X, index: int) returns ({:linear "tid"} tid: X); -ensures {:atomic} |{ A: assert 0 <= index && index < currsize; tid := tid'; return true; }|; +procedure {:yields} {:phase 0,1} ReadCacheEntry({:cnst "tid"} tid: X, index: int); +ensures {:atomic} |{ A: assert 0 <= index && index < currsize; return true; }|; -procedure {:yields} {:phase 0,1} WriteCacheEntry({:linear "tid"} tid': X, index: int) returns ({:linear "tid"} tid: X); -ensures {:right} |{ A: assert tid' != nil; assert currsize <= index && ghostLock == tid'; tid := tid'; return true; }|; +procedure {:yields} {:phase 0,1} WriteCacheEntry({:cnst "tid"} tid: X, index: int); +ensures {:right} |{ A: assert tid != nil; assert currsize <= index && ghostLock == tid; return true; }|; -procedure {:yields} {:phase 0,1} acquire({:linear "tid"} tid': X) returns ({:linear "tid"} tid: X); -ensures {:right} |{ A: assert tid' != nil; tid := tid'; assume lock == nil; lock := tid; return true; }|; +procedure {:yields} {:phase 0,1} acquire({:cnst "tid"} tid: X); +ensures {:right} |{ A: assert tid != nil; assume lock == nil; lock := tid; return true; }|; -procedure {:yields} {:phase 0,1} release({:linear "tid"} tid': X) returns ({:linear "tid"} tid: X); -ensures {:left} |{ A: assert tid' != nil; assert lock == tid'; tid := tid'; lock := nil; return true; }|; +procedure {:yields} {:phase 0,1} release({:cnst "tid"} tid: X); +ensures {:left} |{ A: assert tid != nil; assert lock == tid; lock := nil; return true; }|; diff --git a/Test/og/FlanaganQadeer.bpl b/Test/og/FlanaganQadeer.bpl index e8df9515..2fddf217 100644 --- a/Test/og/FlanaganQadeer.bpl +++ b/Test/og/FlanaganQadeer.bpl @@ -17,6 +17,7 @@ procedure {:yields} {:phase 1} main() var {:linear "tid"} tid: X; var val: int; + yield; while (*) { yield; diff --git a/Test/og/lock.bpl b/Test/og/lock.bpl index 4a6e002d..8357d36d 100644 --- a/Test/og/lock.bpl +++ b/Test/og/lock.bpl @@ -2,6 +2,7 @@ var {:phase 2} b: bool; procedure {:yields} {:phase 2} main() { + yield; while (*) { yield; @@ -14,6 +15,7 @@ procedure {:yields} {:phase 2} main() procedure {:yields} {:phase 2} Customer() { + yield; while (*) { yield; @@ -26,8 +28,6 @@ procedure {:yields} {:phase 2} Customer() yield; } - - yield; } procedure {:yields} {:phase 1,2} Enter() diff --git a/Test/og/lock2.bpl b/Test/og/lock2.bpl index b173ecd4..9f5e0be8 100644 --- a/Test/og/lock2.bpl +++ b/Test/og/lock2.bpl @@ -2,6 +2,7 @@ var {:phase 2} b: int; procedure {:yields} {:phase 2} main() { + yield; while (*) { yield; @@ -14,6 +15,7 @@ procedure {:yields} {:phase 2} main() procedure {:yields} {:phase 2} Customer() { + yield; while (*) { yield; @@ -26,14 +28,13 @@ procedure {:yields} {:phase 2} Customer() yield; } - - yield; } procedure {:yields} {:phase 1,2} Enter() ensures {:atomic} |{ A: assume b == 0; b := 1; return true; }|; { var _old, curr: int; + yield; while (true) { yield; call _old := CAS(0, 1); diff --git a/Test/og/multiset.bpl b/Test/og/multiset.bpl index 3305b63f..459cb470 100644 --- a/Test/og/multiset.bpl +++ b/Test/og/multiset.bpl @@ -339,6 +339,8 @@ procedure {:yields} {:phase 1} Yield1() requires {:phase 1} Inv(valid, elt, owner); ensures {:phase 1} Inv(valid, elt, owner); { + yield; + assert {:phase 1} Inv(valid, elt, owner); } procedure {:yields} {:phase 2} Yield12() diff --git a/Test/og/parallel1.bpl b/Test/og/parallel1.bpl index 18050e09..427dc72d 100644 --- a/Test/og/parallel1.bpl +++ b/Test/og/parallel1.bpl @@ -37,7 +37,8 @@ procedure {:yields} {:phase 1} PD() procedure {:yields} {:phase 1} Main() { - while (true) + yield; + while (*) { par PB() | PC() | PD(); } diff --git a/Test/og/parallel2.bpl b/Test/og/parallel2.bpl index 4a3c1849..1bce7c8a 100644 --- a/Test/og/parallel2.bpl +++ b/Test/og/parallel2.bpl @@ -27,7 +27,7 @@ procedure {:yields} {:phase 1} t({:linear "tid"} i': int) returns ({:linear "tid yield; call Write(i, 42); - call i := Yield(i); + call Yield(i); assert {:phase 1} a[i] == 42; } @@ -41,11 +41,9 @@ procedure {:yields} {:phase 1} u({:linear "tid"} i': int) returns ({:linear "tid assert {:phase 1} a[i] == 42; } -procedure {:yields} {:phase 1} Yield({:linear "tid"} i': int) returns ({:linear "tid"} i: int) -ensures {:phase 1} i == i'; +procedure {:yields} {:phase 1} Yield({:cnst "tid"} i: int) ensures {:phase 1} old(a)[i] == a[i]; { - i := i'; yield; assert {:phase 1} old(a)[i] == a[i]; } \ No newline at end of file diff --git a/Test/og/parallel5.bpl b/Test/og/parallel5.bpl index 330b970d..a73af06e 100644 --- a/Test/og/parallel5.bpl +++ b/Test/og/parallel5.bpl @@ -17,7 +17,7 @@ procedure {:yields} {:phase 1} main() var {:linear "tid"} j: int; call i := Allocate(); call j := Allocate(); - par i := t(i) | j := Yield(j); + par i := t(i) | Yield(j); par i := u(i) | j := u(j); } @@ -27,7 +27,7 @@ procedure {:yields} {:phase 1} t({:linear "tid"} i': int) returns ({:linear "tid yield; call Write(i, 42); - call i := Yield(i); + call Yield(i); assert {:phase 1} a[i] == 42; } @@ -41,11 +41,9 @@ procedure {:yields} {:phase 1} u({:linear "tid"} i': int) returns ({:linear "tid assert {:phase 1} a[i] == 42; } -procedure {:yields} {:phase 1} Yield({:linear "tid"} i': int) returns ({:linear "tid"} i: int) -ensures {:phase 1} i == i'; +procedure {:yields} {:phase 1} Yield({:cnst "tid"} i: int) ensures {:phase 1} old(a)[i] == a[i]; { - i := i'; yield; assert {:phase 1} old(a)[i] == a[i]; } \ No newline at end of file diff --git a/Test/og/ticket.bpl b/Test/og/ticket.bpl index ea08dcb5..fb347935 100644 --- a/Test/og/ticket.bpl +++ b/Test/og/ticket.bpl @@ -65,7 +65,8 @@ requires {:phase 3} true; { var {:linear "tid"} tid: X; tid := tid'; - + + par Yield1() | Yield2() | Yield(); while (*) invariant {:phase 1} Inv1(T, t); invariant {:phase 2} tid != nil && Inv2(T, s, cs); @@ -108,18 +109,23 @@ ensures {:right} |{ A: tid := tid'; havoc m, t; assume !T[m]; T[m] := true; retu procedure {:yields} {:phase 3} Yield() { + yield; } procedure {:yields} {:phase 2} Yield2() requires {:phase 2} Inv2(T, s, cs); ensures {:phase 2} Inv2(T, s, cs); { + yield; + assert {:phase 2} Inv2(T, s, cs); } procedure {:yields} {:phase 1} Yield1() requires {:phase 1} Inv1(T, t); ensures {:phase 1} Inv1(T,t); { + yield; + assert {:phase 1} Inv1(T,t); } procedure {:yields} {:phase 0,3} Init({:linear "tid"} xls':[X]bool) returns ({:linear "tid"} xls:[X]bool); -- cgit v1.2.3