diff options
author | qadeer <unknown> | 2013-12-04 10:51:50 -0800 |
---|---|---|
committer | qadeer <unknown> | 2013-12-04 10:51:50 -0800 |
commit | 3c260ee33f3c9c680581f9684a2334fbb2a0fa9b (patch) | |
tree | f9641de5470f0d6ae0f9b5738fad661f74ee7502 /Test/og/lock.bpl | |
parent | 45b844f3d0e3897dc34bae8af12f32524a48e01a (diff) |
first check in
Diffstat (limited to 'Test/og/lock.bpl')
-rw-r--r-- | Test/og/lock.bpl | 52 |
1 files changed, 52 insertions, 0 deletions
diff --git a/Test/og/lock.bpl b/Test/og/lock.bpl new file mode 100644 index 00000000..4c019846 --- /dev/null +++ b/Test/og/lock.bpl @@ -0,0 +1,52 @@ +var b: bool;
+
+procedure {:yields} {:entrypoint} main()
+{
+ while (*)
+ {
+ async call Customer();
+ }
+}
+
+procedure {:yields} {:stable} Customer()
+{
+ while (*)
+ {
+ yield;
+
+ call Enter();
+
+ yield;
+
+ call Leave();
+ }
+}
+
+procedure {:yields} Enter()
+ensures {:atomic} {:phase 0} |{ A: assume !b; b := true; return true; }|;
+{
+ var status: bool;
+ L:
+ yield;
+ call status := CAS(false, true);
+ goto A, B;
+
+ A:
+ assume status;
+ yield;
+ return;
+
+ B:
+ assume !status;
+ goto L;
+}
+
+procedure 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} Leave();
+ensures {:atomic} |{ A: b := false; return true; }|;
|