diff options
| author |  qadeer <qadeer@microsoft.com> | 2015-04-22 09:26:56 -0700 |
|---|---|---|
| committer | qadeer <qadeer@microsoft.com> | 2015-04-22 09:26:56 -0700 |
| commit | 4c6dd519143fdbc8ecada56d58103d098c6bd18c (patch) | |
| tree | abdbf5f883d31236a221a5b95f5f0364e75caf36 /Test/civl/lock-introduced.bpl | |
| parent | 95a9ed0282811aa2bc3170f41b8b63508918b28e (diff) | |
renamed og to civl
Diffstat (limited to 'Test/civl/lock-introduced.bpl')
| -rw-r--r-- | Test/civl/lock-introduced.bpl | 100 |
1 files changed, 100 insertions, 0 deletions
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; }|;
+
|