deleted the free assume about gates after parallel calls

6 files changed, 201 insertions, 216 deletions

diff --git a/Source/Concurrency/OwickiGries.cs b/Source/Concurrency/OwickiGries.cs
index e5201809..23c8945b 100644
--- a/Source/Concurrency/OwickiGries.cs
+++ b/Source/Concurrency/OwickiGries.cs
@@ -945,13 +945,6 @@ namespace Microsoft.Boogie
                         ParCallCmd parCallCmd = cmd as ParCallCmd;

                         AddCallToYieldProc(parCallCmd.tok, newCmds, ogOldGlobalMap, domainNameToLocalVar);

                         DesugarParallelCallCmd(newCmds, parCallCmd);

-                        if (globalMods.Count > 0 && pc != null)

-                        {

-                            // assume pc || alpha(i, g);

-                            Expr assumeExpr = Expr.Or(Expr.Ident(pc), alpha);

-                            assumeExpr.Type = Type.Bool;

-                            newCmds.Add(new AssumeCmd(Token.NoToken, assumeExpr));

-                        }

                         HashSet<Variable> availableLinearVars = new HashSet<Variable>(AvailableLinearVars(parCallCmd));

                         linearTypeChecker.AddAvailableVars(parCallCmd, availableLinearVars);

                         Dictionary<string, Expr> domainNameToExpr = ComputeAvailableExprs(availableLinearVars, domainNameToInputVar);

diff --git a/Test/og/civl-paper.bpl b/Test/og/civl-paper.bpl
index eadf81e3..be519470 100644
--- a/Test/og/civl-paper.bpl
+++ b/Test/og/civl-paper.bpl
@@ -15,86 +15,123 @@ 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 {:phase 2} {:linear "mem"} g: lmap;

+var {:phase 3} {:linear "mem"} g: lmap;

+var {:phase 3} lock: X;

+var {:phase 1} b: bool;

 

 const p: int;

 

-procedure {:yields} {:phase 1,2} TransferToGlobal({:linear "tid"} tid: X, {:linear_in "mem"} l: lmap);

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

+procedure {:yields} {:phase 1} Yield1()

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

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

+{

+    yield;

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

+}

 

-procedure {:yields} {:phase 1,2} TransferFromGlobal({:linear "tid"} tid: X) returns ({:linear "mem"} l: lmap);

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

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

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

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

+{

+    lock != nil <==> b

+}

 

-procedure {:yields} {:phase 1} Load({:linear "mem"} l: lmap, a: int) returns (v: int);

-ensures {:both} |{ A: v := map(l)[a]; return true; }|;

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

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

+procedure {:yields} {:phase 2} Yield2()

+{

+    yield;

+}

 

-procedure {:yields} {:phase 1} Store({:linear_in "mem"} l_in: lmap, a: int, v: int) returns ({:linear "mem"} l_out: lmap);

-ensures {:both} |{ A: assume l_out == cons(dom(l_in), map(l_in)[a := v]); return true; }|;

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

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

+procedure {:yields} {:phase 3} Yield3()

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

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

+{

+    yield;

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

+}

 

-procedure {:yields} {:phase 2} P({:linear "tid"} tid: X)

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

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

+{

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

+}

+

+procedure {:yields} {:phase 3} P({:linear "tid"} tid: X)

+requires {:phase 1} tid != nil && InvLock(lock, b);

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

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

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

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

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

 {

     var t: int;

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

 

-    par Yield() | YieldLock();

-    call Acquire(tid);

-    call l := TransferFromGlobal(tid);

+    par Yield3() | Yield1();

+    call AcquireProtected(tid);

+    call l := TransferFromGlobalProtected(tid);

     call t := Load(l, p);

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

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

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

-    call TransferToGlobal(tid, l);

-    call Release(tid);

-    par Yield() | YieldLock();

+    call TransferToGlobalProtected(tid, l);

+    call ReleaseProtected(tid);

+    par Yield3() | Yield1();

 }

 

-procedure {:yields} {:phase 2} Yield()

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

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

+

+procedure {:yields} {:phase 2,3} TransferToGlobalProtected({:linear "tid"} tid: X, {:linear_in "mem"} l: lmap)

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

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

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

 {

-    yield;

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

+  par Yield1() | Yield2();

+  call TransferToGlobal(tid, l);

+  par Yield1() | Yield2();

 }

 

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

+procedure {:yields} {:phase 2,3} TransferFromGlobalProtected({:linear "tid"} tid: X) returns ({:linear "mem"} l: lmap)

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

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

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

 {

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

+  par Yield1() | Yield2();

+  call l := TransferFromGlobal(tid);

+  par Yield1() | Yield2();

 }

 

+procedure {:yields} {:phase 2,3} AcquireProtected({:linear "tid"} tid: X)

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

+requires {:phase 1} tid != nil && InvLock(lock, b);

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

+{

+  par Yield1() | Yield2();

+  call Acquire(tid);

+  par Yield1() | Yield2();

+}

 

-var {:phase 1} b: bool;

-var {:phase 2} lock: X;

+procedure {:yields} {:phase 2,3} ReleaseProtected({:linear "tid"} tid: X)

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

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

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

+{

+  par Yield1() | Yield2();

+  call Release(tid);

+  par Yield1() | Yield2();

+}

 

 procedure {:yields} {:phase 1,2} Acquire({:linear "tid"} tid: X)

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

+requires {:phase 1} tid != nil && InvLock(lock, b);

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

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

+ensures {:atomic} |{ A: assume lock == nil; lock := tid; return true; }|;

 {

     var status: bool;

     var tmp: X;

 

-    par YieldLock();

+    par Yield1();

     L: 

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

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

-	par YieldLock();

+	par Yield1();

         goto A, B;

 

     A: 

         assume status;

-	par YieldLock();	

+	par Yield1();	

 	return;

 

     B:

@@ -103,15 +140,27 @@ ensures {:right} |{ A: assert tid != nil; assume lock == nil; lock := tid; retur
 }

 

 procedure {:yields} {:phase 1,2} Release({:linear "tid"} tid: X)

-ensures {:left} |{ A: assert lock == tid && tid != nil; lock := nil; return true; }|;

+ensures {:atomic} |{ A: lock := nil; return true; }|;

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

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

 {

-    par YieldLock();

+    par Yield1();

     call CLEAR(tid, false);

-    par YieldLock();

+    par Yield1();

 }

 

+procedure {:yields} {:phase 0,2} TransferToGlobal({:linear "tid"} tid: X, {:linear_in "mem"} l: lmap);

+ensures {:atomic} |{ A: g := l; return true; }|;

+

+procedure {:yields} {:phase 0,2} TransferFromGlobal({:linear "tid"} tid: X) returns ({:linear "mem"} l: lmap);

+ensures {:atomic} |{ A: l := g; return true; }|;

+

+procedure {:yields} {:phase 0,3} Load({:linear "mem"} l: lmap, a: int) returns (v: int);

+ensures {:both} |{ A: v := map(l)[a]; return true; }|;

+

+procedure {:yields} {:phase 0,3} Store({:linear_in "mem"} l_in: lmap, a: int, v: int) returns ({:linear "mem"} l_out: lmap);

+ensures {:both} |{ A: assume l_out == cons(dom(l_in), map(l_in)[a := v]); return true; }|;

+

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

 ensures {:atomic} |{ 

 A: goto B, C; 

@@ -124,15 +173,3 @@ ensures {:atomic} |{
 A: b := next; lock := nil; return true; 

 }|;

 

-procedure {:yields} {:phase 1} 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/civl-paper.bpl.expect b/Test/og/civl-paper.bpl.expect
index ac38b46e..4bcd03fb 100644
--- a/Test/og/civl-paper.bpl.expect
+++ b/Test/og/civl-paper.bpl.expect
@@ -1,2 +1,2 @@
 

-Boogie program verifier finished with 23 verified, 0 errors

+Boogie program verifier finished with 35 verified, 0 errors

diff --git a/Test/og/multiset.bpl b/Test/og/multiset.bpl
index 8ee661c6..a522f304 100644
--- a/Test/og/multiset.bpl
+++ b/Test/og/multiset.bpl
@@ -20,92 +20,85 @@ function {:inline} {:linear "tid"} TidCollector(x: X) : [X]bool
 

 axiom (max > 0);

 

-procedure {:yields} {:phase 0} acquire(i : int, {:linear_in "tid"} tidIn: X) returns ({:linear "tid"} tidOut: X);

+procedure {:yields} {:phase 0} acquire(i : int, {:linear "tid"} tid: X);

 ensures {:right} |{ A: 

                       assert 0 <= i && i < max;

-                      assert tidIn != nil && tidIn != done;

+                      assert tid != nil && tid != done;

                       assume lock[i] == nil;

-                      tidOut := tidIn;

-	              lock[i] := tidOut;

+	              lock[i] := tid;

                       return true;

                     }|;

 

 

-procedure {:yields} {:phase 0} release(i : int, {:linear_in "tid"} tidIn: X) returns ({:linear "tid"} tidOut: X);

+procedure {:yields} {:phase 0} release(i : int, {:linear "tid"} tid: X);

 ensures {:left} |{ A: 

                      assert 0 <= i && i < max;

-                     assert lock[i] == tidIn;

-                     assert tidIn != nil && tidIn != done; 

-                     tidOut := tidIn;

+                     assert lock[i] == tid;

+                     assert tid != nil && tid != done; 

 	             lock[i] := nil;

                      return true;

                     }|;

 

 

-procedure {:yields} {:phase 0,1} getElt(j : int, {:linear_in "tid"} tidIn: X) returns ({:linear "tid"} tidOut: X, elt_j:int);

+procedure {:yields} {:phase 0,1} getElt(j : int, {:linear "tid"} tid: X) returns (elt_j:int);

 ensures {:both} |{ A: 

                      assert 0 <= j && j < max;

-                     assert lock[j] == tidIn;

-                     assert tidIn != nil && tidIn != done;

-                     tidOut := tidIn;

+                     assert lock[j] == tid;

+                     assert tid != nil && tid != done;

 	             elt_j := elt[j];

                      return true;

                     }|;

 

 

-procedure {:yields} {:phase 0,1} setElt(j : int, x : int, {:linear_in "tid"} tidIn: X) returns ({:linear "tid"} tidOut: X);

+procedure {:yields} {:phase 0,1} setElt(j : int, x : int, {:linear "tid"} tid: X);

 ensures {:both} |{ A: 

                      assert x != null;

                      assert owner[j] == nil;

                      assert 0 <= j && j < max;

-                     assert lock[j] == tidIn;

-                     assert tidIn != nil && tidIn != done;

-                     tidOut := tidIn;

+                     assert lock[j] == tid;

+                     assert tid != nil && tid != done;

 	             elt[j] := x;

-                     owner[j] := tidIn;

+                     owner[j] := tid;

                      return true;

                     }|;

 

 

-procedure {:yields} {:phase 0} setEltToNull(j : int, {:linear_in "tid"} tidIn: X) returns ({:linear "tid"} tidOut: X);

+procedure {:yields} {:phase 0} setEltToNull(j : int, {:linear "tid"} tid: X);

 ensures {:left} |{ A: 

-                     assert owner[j] == tidIn;

+                     assert owner[j] == tid;

                      assert 0 <= j && j < max;

-                     assert lock[j] == tidIn;

+                     assert lock[j] == tid;

                      assert !valid[j];

-                     assert tidIn != nil  && tidIn != done;

-                     tidOut := tidIn;

+                     assert tid != nil  && tid != done;

 	             elt[j] := null;

                      owner[j] := nil;

                      return true;

                     }|;

 

-procedure {:yields} {:phase 0} setValid(j : int, {:linear_in "tid"} tidIn: X) returns ({:linear "tid"} tidOut: X);

+procedure {:yields} {:phase 0} setValid(j : int, {:linear "tid"} tid: X);

 ensures {:both} |{ A: 

                      assert 0 <= j && j < max;

-                     assert lock[j] == tidIn;

-                     assert tidIn != nil && tidIn != done;

-                     assert owner[j] == tidIn;

-                     tidOut := tidIn;

+                     assert lock[j] == tid;

+                     assert tid != nil && tid != done;

+                     assert owner[j] == tid;

 	             valid[j] := true;

                      owner[j] := done;

                      return true;

                     }|;

 

-procedure {:yields} {:phase 0} isEltThereAndValid(j : int, x : int, {:linear_in "tid"} tidIn: X) returns ({:linear "tid"} tidOut: X, fnd:bool);

+procedure {:yields} {:phase 0} isEltThereAndValid(j : int, x : int, {:linear "tid"} tid: X) returns (fnd:bool);

 ensures {:both} |{ A: 

                        assert 0 <= j && j < max;

-                       assert lock[j] == tidIn;

-                       assert tidIn != nil && tidIn != done;

-                       tidOut := tidIn;

+                       assert lock[j] == tid;

+                       assert tid != nil && tid != done;

                        fnd := (elt[j] == x) && valid[j];

                        return true;

                     }|;

 

-procedure {:yields} {:phase 1} FindSlot(x : int, {:linear_in "tid"} tidIn: X) returns (r : int, {:linear "tid"} tidOut: X)

-requires {:phase 1} Inv(valid, elt, owner);

+procedure {:yields} {:phase 1} FindSlot(x : int, {:linear "tid"} tid: X) returns (r : int)

+requires {:phase 1} Inv(valid, elt, owner) && x != null && tid != nil && tid != done; 

 ensures {:phase 1} Inv(valid, elt, owner);

-ensures {:right}  |{ A: assert tidIn != nil && tidIn != done; 

+ensures {:right}  |{   A: assert tid != nil && tid != done; 

                           assert x != null; 

 			  goto B, C;

                        B: assume (0 <= r && r < max); 

@@ -113,112 +106,91 @@ ensures {:right}  |{ A: assert tidIn != nil && tidIn != done;
                                             assume owner[r] == nil;

 					    assume !valid[r];

                                             elt[r] := x; 

-                                            owner[r] := tidIn;

-                                            tidOut := tidIn; 

+                                            owner[r] := tid;

                                             return true;

-                       C: assume (r == -1); tidOut := tidIn; return true; 

+                       C: assume (r == -1); return true; 

                    }|;

 {

 	var j : int;

 	var elt_j : int;

-        var {:linear "tid"} tidTmp: X;

         

         par Yield1();

 

 	j := 0;

-        tidTmp := tidIn;

-

-	

 	while(j < max)

-        invariant {:phase 1} tidTmp != nil && tidTmp != done;

-        invariant {:phase 1} tidTmp == tidIn;

         invariant {:phase 1} Inv(valid, elt, owner);

 	invariant {:phase 1} 0 <= j;

 	{

-                call tidTmp := acquire(j, tidTmp);

-                call tidTmp, elt_j := getElt(j, tidTmp);

+                call acquire(j, tid);

+                call elt_j := getElt(j, tid);

 		if(elt_j == null)

 		{

-                        call tidTmp := setElt(j, x, tidTmp);

-			call tidTmp := release(j, tidTmp);

+                        call setElt(j, x, tid);

+			call release(j, tid);

 			r := j;

-                        tidOut := tidTmp;

 

                         par Yield1();

 			return;		

 		}

-		call tidTmp := release(j,tidTmp);

+		call release(j,tid);

 

                 par Yield1();

 

 		j := j + 1;	

 	}

 	r := -1;

-        tidOut := tidTmp;

 

         par Yield1();

 	return;

 }

 

-procedure {:yields} {:phase 2} Insert(x : int, {:linear_in "tid"} tidIn: X) returns (result : bool, {:linear "tid"} tidOut: X) 

-requires {:phase 1} Inv(valid, elt, owner);

-requires {:phase 2} Inv(valid, elt, owner);

+procedure {:yields} {:phase 2} Insert(x : int, {:linear "tid"} tid: X) returns (result : bool) 

+requires {:phase 1} Inv(valid, elt, owner) && x != null && tid != nil && tid != done; 

 ensures {:phase 1} Inv(valid, elt, owner);

-requires {:phase 2} Inv(valid, elt, owner);

+requires {:phase 2} Inv(valid, elt, owner) && x != null && tid != nil && tid != done; 

+ensures {:phase 2} Inv(valid, elt, owner);

 ensures {:atomic}  |{ var r:int;

-                        A: assert tidIn != nil && tidIn != done; 

-                           assert x != null;

-                           goto B, C;

+                        A: goto B, C;

                         B: assume (0 <= r && r < max); 

                            assume valid[r] == false; 

                            assume elt[r] == null; 

                            assume owner[r] == nil; 

                            elt[r] := x; valid[r] := true; owner[r] := done;

-                           tidOut := tidIn; result := true; return true;

-                        C: tidOut := tidIn; result := false; return true; 

+                           result := true; return true;

+                        C: result := false; return true; 

                       }|;

  {

         var i: int;

-        var {:linear "tid"} tidTmp: X;

         par Yield12();

-        tidTmp := tidIn;

-        call i, tidTmp := FindSlot(x, tidTmp);

+        call i := FindSlot(x, tid);

         

 	if(i == -1)

 	{

 		result := false;

-                tidOut := tidTmp;

                 par Yield12();

 		return;

 	}

         par Yield1();

         assert {:phase 1} i != -1;

         assert {:phase 2} i != -1;

-	call tidTmp := acquire(i, tidTmp);

+	call acquire(i, tid);

         assert {:phase 2} elt[i] == x;

 	assert {:phase 2}  valid[i] == false;

-        call tidTmp := setValid(i, tidTmp);   

-	call tidTmp := release(i, tidTmp);

+        call setValid(i, tid);   

+	call release(i, tid);

 	result := true; 

-        tidOut := tidTmp;

         par Yield12();

 	return;

 }

 

-procedure {:yields} {:phase 2} InsertPair(x : int, 

-                               y : int, 

-                               {:linear_in "tid"} tidIn: X) 

-                               returns (result : bool, 

-                                        {:linear "tid"} tidOut: X) 

-requires {:phase 1} Inv(valid, elt, owner);

+procedure {:yields} {:phase 2} InsertPair(x : int, y : int, {:linear "tid"} tid: X) returns (result : bool)

+requires {:phase 1} Inv(valid, elt, owner) && x != null && y != null && tid != nil && tid != done; 

 ensures {:phase 1} Inv(valid, elt, owner);

-requires {:phase 2} Inv(valid, elt, owner);

+requires {:phase 2} Inv(valid, elt, owner) && x != null && y != null && tid != nil && tid != done; 

 ensures {:phase 2} Inv(valid, elt, owner);

 ensures {:atomic}  |{ var rx:int;

                         var ry:int;

-                        A: assert tidIn != nil && tidIn != done; 

-                           assert x != null && y != null;

-                           goto B, C;

+                        A: goto B, C;

                         B: assume (0 <= rx && rx < max && 0 <= ry && ry < max && rx != ry); 

                            assume valid[rx] == false; 

                            assume valid[ry] == false; 

@@ -230,68 +202,60 @@ ensures {:atomic}  |{ var rx:int;
                            valid[ry] := true;

                            owner[rx] := done;

                            owner[ry] := done; 

-                           tidOut := tidIn; 

                            result := true; return true;

-                        C: tidOut := tidIn; 

-                           result := false; return true; 

+                        C: result := false; return true; 

                       }|;

  {

         var i : int; 

         var j : int;

-        var {:linear "tid"} tidTmp: X;

         par Yield12();

 

-        tidTmp := tidIn;

-

-        call i, tidTmp := FindSlot(x, tidTmp);

+        call i := FindSlot(x, tid);

         

 	if (i == -1)

 	{

 	 	result := false;

-                tidOut := tidTmp;

                 par Yield12();

 		return;

 	}

 

         par Yield1();

-        call j, tidTmp := FindSlot(y, tidTmp);

+        call j := FindSlot(y, tid);

         

 	if(j == -1)

 	{

                 par Yield1();

-                call tidTmp := acquire(i,tidTmp);  

-                call tidTmp := setEltToNull(i, tidTmp);

-                call tidTmp := release(i,tidTmp);  

+                call acquire(i,tid);  

+                call setEltToNull(i, tid);

+                call release(i,tid);  

 		result := false;

-                tidOut := tidTmp;

                 par Yield12();

 		return;

 	}

 

         par Yield1();

         assert {:phase 2} i != -1 && j != -1;

-	call tidTmp := acquire(i, tidTmp);

-	call tidTmp := acquire(j, tidTmp);

+	call acquire(i, tid);

+	call acquire(j, tid);

         assert {:phase 2} elt[i] == x;

         assert {:phase 2} elt[j] == y;

 	assert {:phase 2}  valid[i] == false;

 	assert {:phase 2}  valid[j] == false;

-        call tidTmp := setValid(i, tidTmp);   

-        call tidTmp := setValid(j, tidTmp);   

-	call tidTmp := release(j, tidTmp);

-	call tidTmp := release(i, tidTmp);

+        call setValid(i, tid);   

+        call setValid(j, tid);   

+	call release(j, tid);

+	call release(i, tid);

 	result := true; 

-        tidOut := tidTmp;

         par Yield12();

 	return;

 }

 

-procedure {:yields} {:phase 2} LookUp(x : int, {:linear_in "tid"} tidIn: X, old_valid:[int]bool, old_elt:[int]int) returns (found : bool, {:linear "tid"} tidOut: X)

+procedure {:yields} {:phase 2} LookUp(x : int, {:linear "tid"} tid: X, old_valid:[int]bool, old_elt:[int]int) returns (found : bool)

 requires {:phase 1} {:phase 2} old_valid == valid && old_elt == elt;

 requires {:phase 1} {:phase 2} Inv(valid, elt, owner);

-requires {:phase 1} {:phase 2} (tidIn != nil && tidIn != done);

+requires {:phase 1} {:phase 2} (tid != nil && tid != done);

 ensures {:phase 1} {:phase 2} Inv(valid, elt, owner);

-ensures {:atomic}  |{ A: assert tidIn != nil && tidIn != done; 

+ensures {:atomic}  |{ A: assert tid != nil && tid != done; 

                           assert x != null;

                           assume found ==> (exists ii:int :: 0 <= ii && ii < max && valid[ii] && elt[ii] == x);

 			  assume !found ==> (forall ii:int :: 0 <= ii && ii < max ==> !(old_valid[ii] && old_elt[ii] == x));

@@ -300,37 +264,31 @@ ensures {:atomic}  |{ A: assert tidIn != nil && tidIn != done;
 {

 	var j : int;

 	var isThere : bool;

-        var {:linear "tid"} tidTmp: X;

         

         par Yield12() | YieldLookUp(old_valid, old_elt);

 

 	j := 0;

-        tidTmp := tidIn;

 

 	while(j < max)

-        invariant {:phase 1} {:phase 2} tidTmp != nil && tidTmp != done;

-        invariant {:phase 1} {:phase 2} tidTmp == tidIn;

         invariant {:phase 1} {:phase 2} Inv(valid, elt, owner);

         invariant {:phase 1} {:phase 2} (forall ii:int :: 0 <= ii && ii < j ==> !(old_valid[ii] && old_elt[ii] == x));

 	invariant {:phase 1} {:phase 2} (forall ii:int :: 0 <= ii && ii < max && old_valid[ii] ==> valid[ii] && old_elt[ii] == elt[ii]);

 	invariant {:phase 1} {:phase 2} 0 <= j;

 	{

-                call tidTmp := acquire(j, tidTmp);

-                call tidTmp, isThere := isEltThereAndValid(j, x, tidTmp);

+                call acquire(j, tid);

+                call isThere := isEltThereAndValid(j, x, tid);

 		if(isThere)

 		{

-			 call tidTmp := release(j, tidTmp);

+			 call release(j, tid);

                          found := true; 

-                         tidOut := tidTmp;

                          par Yield12() | YieldLookUp(old_valid, old_elt);

 		 	 return;		

 		}

-		call tidTmp := release(j,tidTmp);

+		call release(j,tid);

                 par Yield12() | YieldLookUp(old_valid, old_elt);

 		j := j + 1;	

 	}

 	found := false;

-        tidOut := tidTmp;

 

         par Yield12() | YieldLookUp(old_valid, old_elt);

 	return;

diff --git a/Test/og/ticket.bpl b/Test/og/ticket.bpl
index 552a4007..9c1b7c9a 100644
--- a/Test/og/ticket.bpl
+++ b/Test/og/ticket.bpl
@@ -8,10 +8,10 @@ axiom (forall x: int, y: int :: RightClosed(x)[y] <==> y <= x);
 type X;

 function {:builtin "MapConst"} mapconstbool(bool): [X]bool;

 const nil: X;

-var {:phase 3} t: int;

-var {:phase 3} s: int;

-var {:phase 3} cs: X;

-var {:phase 3} T: [int]bool;

+var {:phase 2} t: int;

+var {:phase 2} s: int;

+var {:phase 2} cs: X;

+var {:phase 2} T: [int]bool;

 

 function {:builtin "MapConst"} MapConstBool(bool) : [X]bool;

 function {:inline} {:linear "tid"} TidCollector(x: X) : [X]bool

@@ -36,17 +36,18 @@ function {:inline} Inv2(tickets: [int]bool, ticket: int, lock: X): (bool)
 procedure Allocate({:linear_in "tid"} xls':[X]bool) returns ({:linear "tid"} xls: [X]bool, {:linear "tid"} xl: X);

 ensures {:phase 1} {:phase 2} xl != nil;

 

-procedure {:yields} {:phase 3} main({:linear_in "tid"} xls':[X]bool)

-requires {:phase 3} xls' == mapconstbool(true);

+procedure {:yields} {:phase 2} main({:linear_in "tid"} xls':[X]bool)

+requires {:phase 2} xls' == mapconstbool(true);

 {

     var {:linear "tid"} tid: X;

     var {:linear "tid"} xls: [X]bool;

 

     yield;

 

-    call xls := Init(xls');

+    call Init(xls');

+    xls := xls';

 

-    par Yield1() | Yield2() | Yield();

+    par Yield1() | Yield2();

 

     while (*)

     invariant {:phase 1} Inv1(T, t);

@@ -54,63 +55,59 @@ requires {:phase 3} xls' == mapconstbool(true);
     {

         call xls, tid := Allocate(xls);

         async call Customer(tid);

-    	par Yield1() | Yield2() | Yield();

+    	par Yield1() | Yield2();

     }

-    par Yield1() | Yield2() | Yield();

+    par Yield1() | Yield2();

 }

 

-procedure {:yields} {:phase 3} Customer({:linear_in "tid"} tid': X)

+procedure {:yields} {:phase 2} Customer({:linear_in "tid"} tid: X)

 requires {:phase 1} Inv1(T, t);

-requires {:phase 2} tid' != nil && Inv2(T, s, cs);

-requires {:phase 3} true;

+requires {:phase 2} tid != nil && Inv2(T, s, cs);

 {

-    var {:linear "tid"} tid: X;

-    tid := tid';

-    

-    par Yield1() | Yield2() | Yield();    

+    par Yield1() | Yield2();    

     while (*) 

     invariant {:phase 1} Inv1(T, t);

-    invariant {:phase 2} tid != nil && Inv2(T, s, cs);

+    invariant {:phase 2} Inv2(T, s, cs);

     {

-        call tid := Enter(tid);

+        call Enter(tid);

+        par Yield1() | Yield2() | YieldSpec(tid);

+    	call Leave(tid);

         par Yield1() | Yield2();

-    	call tid := Leave(tid);

-        par Yield1() | Yield2() | Yield();

     }

-    par Yield1() | Yield2() | Yield();

+    par Yield1() | Yield2();

 }

 

-procedure {:yields} {:phase 2,3} Enter({:linear_in "tid"} tid': X) returns ({:linear "tid"} tid: X)

+procedure {:yields} {:phase 2} Enter({:linear "tid"} tid: X)

 requires {:phase 1} Inv1(T, t);

 ensures {:phase 1} Inv1(T,t);

-requires {:phase 2} tid' != nil && Inv2(T, s, cs);

-ensures {:phase 2} tid != nil && Inv2(T, s, cs);

-ensures {:right} |{ A: tid := tid'; havoc t, T; assume tid != nil && cs == nil; cs := tid; return true; }|;

+requires {:phase 2} tid != nil && Inv2(T, s, cs);

+ensures {:phase 2} Inv2(T, s, cs) && cs == tid;

 {

     var m: int;

 

     par Yield1() | Yield2();

-    tid := tid';

-    call tid, m := GetTicketAbstract(tid);

+    call m := GetTicketAbstract(tid);

     par Yield1();

-    call tid := WaitAndEnter(tid, m);

-    par Yield1() | Yield2();

+    call WaitAndEnter(tid, m);

+    par Yield1() | Yield2() | YieldSpec(tid);

 }

 

-procedure {:yields} {:phase 1,2} GetTicketAbstract({:linear_in "tid"} tid': X) returns ({:linear "tid"} tid: X, m: int)

+procedure {:yields} {:phase 1,2} GetTicketAbstract({:linear "tid"} tid: X) returns (m: int)

 requires {:phase 1} Inv1(T, t);

 ensures {:phase 1} Inv1(T, t);

-ensures {:right} |{ A: tid := tid'; havoc m, t; assume !T[m]; T[m] := true; return true; }|;

+ensures {:right} |{ A: havoc m, t; assume !T[m]; T[m] := true; return true; }|;

 {

     par Yield1();

-    tid := tid';

-    call tid, m := GetTicket(tid);

+    call m := GetTicket(tid);

     par Yield1();

 }

 

-procedure {:yields} {:phase 3} Yield()

+procedure {:yields} {:phase 2} YieldSpec({:linear "tid"} tid: X)

+requires {:phase 2} tid != nil && cs == tid;

+ensures {:phase 2} cs == tid;

 {

     yield;

+    assert {:phase 2} tid != nil && cs == tid;

 }

 

 procedure {:yields} {:phase 2} Yield2()

@@ -129,15 +126,15 @@ ensures {:phase 1} Inv1(T,t);
     assert {:phase 1} Inv1(T,t);

 }

 

-procedure {:yields} {:phase 0,3} Init({:linear_in "tid"} xls':[X]bool) returns ({:linear "tid"} xls:[X]bool);

-ensures {:atomic} |{ A: assert xls' == mapconstbool(true); xls := xls'; cs := nil; t := 0; s := 0; T := RightOpen(0); return true; }|;

+procedure {:yields} {:phase 0,2} Init({:linear "tid"} xls:[X]bool);

+ensures {:atomic} |{ A: assert xls == mapconstbool(true); cs := nil; t := 0; s := 0; T := RightOpen(0); return true; }|;

 

-procedure {:yields} {:phase 0,1} GetTicket({:linear_in "tid"} tid': X) returns ({:linear "tid"} tid: X, m: int);

-ensures {:atomic} |{ A: tid := tid'; m := t; t := t + 1; T[m] := true; return true; }|;

+procedure {:yields} {:phase 0,1} GetTicket({:linear "tid"} tid: X) returns (m: int);

+ensures {:atomic} |{ A: m := t; t := t + 1; T[m] := true; return true; }|;

 

-procedure {:yields} {:phase 0,2} WaitAndEnter({:linear_in "tid"} tid': X, m:int) returns ({:linear "tid"} tid: X);

-ensures {:atomic} |{ A: tid := tid'; assume m <= s; cs := tid; return true; }|;

+procedure {:yields} {:phase 0,2} WaitAndEnter({:linear "tid"} tid: X, m:int);

+ensures {:atomic} |{ A: assume m <= s; cs := tid; return true; }|;

 

-procedure {:yields} {:phase 0,3} Leave({:linear_in "tid"} tid': X) returns ({:linear "tid"} tid: X);

-ensures {:atomic} |{ A: assert cs == tid'; assert tid' != nil; tid := tid'; s := s + 1; cs := nil; return true; }|;

+procedure {:yields} {:phase 0,2} Leave({:linear "tid"} tid: X);

+ensures {:atomic} |{ A: s := s + 1; cs := nil; return true; }|;

 

diff --git a/Test/og/ticket.bpl.expect b/Test/og/ticket.bpl.expect
index bc10e4e3..f7c1129d 100644
--- a/Test/og/ticket.bpl.expect
+++ b/Test/og/ticket.bpl.expect
@@ -1,2 +1,2 @@
 

-Boogie program verifier finished with 21 verified, 0 errors

+Boogie program verifier finished with 14 verified, 0 errors