various bug fixes

added "cnst" feature

2 files changed, 108 insertions, 2 deletions

diff --git a/Test/og/civl-paper.bpl b/Test/og/civl-paper.bpl
new file mode 100644
index 00000000..03da6a48
--- /dev/null
+++ b/Test/og/civl-paper.bpl
@@ -0,0 +1,106 @@
+type X;

+const nil: X;

+

+type lmap;

+function {:linear "mem"} dom(lmap): [int]bool;

+function map(lmap): [int]int;

+function cons([int]bool, [int]int) : lmap;

+axiom (forall x: [int]bool, y: [int]int :: {cons(x,y)} dom(cons(x, y)) == x && map(cons(x,y)) == y);

+

+var {:qed} {:linear "mem"} g: lmap;

+

+const p: int;

+

+procedure {:yields} TransferToGlobal({:cnst "tid"} tid: X, {:linear "mem"} l: lmap);

+ensures {:both 1} |{ A: assert tid != nil && lock == tid; g := l; return true; }|;

+

+procedure {:yields} TransferFromGlobal({:cnst "tid"} tid: X) returns ({:linear "mem"} l: lmap);

+ensures {:both 1} |{ A: assert tid != nil && lock == tid; l := g; return true; }|;

+

+procedure {:yields} Load({:cnst "tid"} tid: X, {:cnst "mem"} l: lmap, a: int) returns (v: int);

+ensures {:both 1} |{ A: assert tid != nil && lock == tid; v := map(l)[a]; return true; }|;

+

+procedure {:yields} Store({:cnst "tid"} tid: X, {:linear "mem"} l_in: lmap, a: int, v: int) returns ({:linear "mem"} l_out: lmap);

+ensures {:both 1} |{ A: assert tid != nil && lock == tid; assume l_out == cons(dom(l_in), map(l_in)[a := v]); return true; }|;

+

+procedure {:yields} P({:cnst "tid"} tid: X)

+requires {:phase 2} tid != nil && Inv(g);

+ensures {:phase 2} Inv(g);

+{

+    var t: int;

+    var {:linear "mem"} l: lmap;

+

+    par Yield();

+    call Acquire(tid);

+    call l := TransferFromGlobal(tid);

+    call t := Load(tid, l, p);

+    call l := Store(tid, l, p, t+1);

+    call t := Load(tid, l, p+4);

+    call l := Store(tid, l, p+4, t+1);

+    call TransferToGlobal(tid, l);

+    call Release(tid);

+    par Yield();

+}

+

+procedure {:yields} {:stable} Yield()

+requires {:phase 2} Inv(g);

+ensures {:phase 2} Inv(g);

+{

+    yield;

+    assert {:phase 2} Inv(g);

+}

+

+function {:inline} Inv(g: lmap) : bool

+{

+    dom(g)[p] && dom(g)[p+4] && map(g)[p] == map(g)[p+4]

+}

+

+

+var {:qed} b: bool;

+var {:qed} lock: X;

+

+procedure {:yields} Acquire({:cnst "tid"} tid: X)

+free requires {:phase 1} InvLock(lock, b);

+ensures {:right 1} |{ A: assert tid != nil; assume lock == nil; b := true; lock := tid; return true; }|;

+{

+    var status: bool;

+    var tmp: X;

+

+    par YieldLock();

+    L: 

+	assert {:phase 1} InvLock(lock, b);

+        call status := CAS(tid, false, true);

+	par YieldLock();

+        goto A, B;

+

+    A: 

+        assume status;

+	return;

+

+    B:

+        assume !status;

+	goto L;

+}

+

+procedure {:yields} CAS(tid: X, prev: bool, next: bool) returns (status: bool);

+ensures {:atomic 0} |{ 

+A: goto B, C; 

+B: assume b == prev; b := next; status := true; lock := tid; return true; 

+C: status := false; return true; 

+}|;

+

+procedure {:yields} Release({:cnst "tid"} tid: X);

+ensures {:left 1} |{ A: assert lock == tid && tid != nil; b := false; lock := nil; return true; }|;

+

+procedure {:yields} {:stable} YieldLock()

+requires {:phase 1} InvLock(lock, b);

+ensures {:phase 1} InvLock(lock, b);

+{

+    yield;

+    assert {:phase 1} InvLock(lock, b);

+}

+

+function {:inline} InvLock(lock: X, b: bool) : bool

+{

+    lock != nil <==> b

+}

diff --git a/Test/og/multiset.bpl b/Test/og/multiset.bpl
index 9da8c125..d757362b 100644
--- a/Test/og/multiset.bpl
+++ b/Test/og/multiset.bpl
@@ -185,7 +185,7 @@ ensures {:atomic 2}  |{ var r:int;
 	{

 		result := false;

                 tidOut := tidTmp;

-                par YieldInv();

+                par Yield12();

 		return;

 	}

         par Yield1();

@@ -198,7 +198,7 @@ ensures {:atomic 2}  |{ var r:int;
 	call tidTmp := release(i, tidTmp);

 	result := true; 

         tidOut := tidTmp;

-        par YieldInv();

+        par Yield12();

 	return;

 }