diff options
| author |  stasiran <unknown> | 2014-01-15 12:36:04 -0800 |
|---|---|---|
| committer | stasiran <unknown> | 2014-01-15 12:36:04 -0800 |
| commit | 38c3164cd4899505ee38f988f8642fd254c2a4cf (patch) | |
| tree | 800f19ea14706ad213e0d48c824213924636290d /Test/og/treiber-stack.bpl | |
| parent | aa7f8fa6f35963604f3a131ce65cf2238dacfc71 (diff) | |
Added Treiber stack (not yet readable by QED version of Boogie.)
Diffstat (limited to 'Test/og/treiber-stack.bpl')
| -rw-r--r-- | Test/og/treiber-stack.bpl | 65 |
1 files changed, 65 insertions, 0 deletions
diff --git a/Test/og/treiber-stack.bpl b/Test/og/treiber-stack.bpl new file mode 100644 index 00000000..bc5e0b10 --- /dev/null +++ b/Test/og/treiber-stack.bpl @@ -0,0 +1,65 @@ +
+record Node
+{
+ data: int;
+ next: Node;
+}
+
+const unique null: Node;
+invariant IsNull(null.alloc);
+//invariant null.next == null;
+
+var TOP: Node;
+
+const unique EMPTY: int;
+
+procedure {:isatomic} CAS(oldVal: Node, newVal: Node)
+returns (r: bool)
+{
+ r := (TOP == oldVal);
+ if(r)
+ {
+ TOP := newVal;
+ }
+}
+
+// invariant ReachBetween(Node_next, TOP, null, null) && (forall n: Node :: Connected(Node_next, TOP, n) && n != null ==> IsAlloc(n.alloc)) && (forall n1,n2: Node :: IsDealloc(n1.alloc) ==> n2.next != n1) && (forall n: Node :: !IsAlloc(n.alloc) ==> n.next == null)
+
+procedure push(v: int)
+{
+ var t, x: Node;
+ var g: bool;
+
+ x := New Node;
+ x.data := v;
+
+ while(true)
+ {
+ t := TOP; // Connected(t, TOP)
+ x.next := t; // !Connected(x, TOP)
+ call g := CAS(t, x); // x.next == t, !Connected(x, TOP)
+ if(g) { break; }
+ }
+}
+
+procedure pop()
+returns (v: int)
+{
+ var t, x: Node;
+ var g: bool;
+
+ while(true)
+ {
+ t := TOP; // Connected(t, TOP)
+ if(t == null)
+ {
+ v := EMPTY;
+ return;
+ }
+ x := t.next; // Connected(t, TOP)
+ call g := CAS(t, x); // Connected(t, TOP), x == t.next
+ if(g) { break; }
+ }
+
+ v := t.data;
+}
\ No newline at end of file |