diff options
author | Checkmate50 <dgeisler50@gmail.com> | 2016-06-06 23:14:18 -0600 |
---|---|---|
committer | Checkmate50 <dgeisler50@gmail.com> | 2016-06-06 23:14:18 -0600 |
commit | d652155ae013f36a1ee17653a8e458baad2d9c2c (patch) | |
tree | 067d600fe3cd1723afc11682935f0123a1eab653 /Test/civl/lock2.bpl | |
parent | d7fc0deb2ca6d7ebee094b6ea5430d9b41f163ec (diff) |
Merging complete. Everything looks good *crosses fingers*
Diffstat (limited to 'Test/civl/lock2.bpl')
-rw-r--r-- | Test/civl/lock2.bpl | 63 |
1 files changed, 63 insertions, 0 deletions
diff --git a/Test/civl/lock2.bpl b/Test/civl/lock2.bpl new file mode 100644 index 00000000..e84d0a6f --- /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; }|; |