checkpoint

23 files changed, 500 insertions, 330 deletions

diff --git a/Test/linear/typecheck.bpl b/Test/linear/typecheck.bpl
index 187b3ff8..c8510909 100644
--- a/Test/linear/typecheck.bpl
+++ b/Test/linear/typecheck.bpl
@@ -20,7 +20,7 @@ procedure C()
 

 function f(X): X;

 

-procedure {:yields} D()

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

 {

     var {:linear "D"} a: X;

     var {:linear "D"} x: X;

@@ -58,7 +58,9 @@ procedure {:yields} D()
 

     call c, x := E(a, x);

 

+    yield;

     par a := F(a) | x := F(a);

+    yield;

 }

 

 procedure E({:linear "D"} a: X, {:linear "D"} b: X) returns ({:linear "D"} c: X, {:linear "D"} d: X)

@@ -66,9 +68,9 @@ procedure E({:linear "D"} a: X, {:linear "D"} b: X) returns ({:linear "D"} c: X,
     c := a;

 }

 

-procedure {:yields} {:stable} F({:linear "D"} a: X) returns ({:linear "D"} c: X);

+procedure {:yields} {:phase 0} F({:linear "D"} a: X) returns ({:linear "D"} c: X);

 

-var{:linear "x"} g:int;

+var {:linear "x"} g:int;

 

 procedure G(i:int) returns({:linear "x"} r:int)

 {

@@ -81,23 +83,29 @@ modifies g;
   g := r;

 }

 

-procedure {:yields} {:stable} I({:linear ""} x:int) returns({:linear ""} x':int)

+procedure {:yields} {:phase 0} I({:linear ""} x:int) returns({:linear ""} x':int)

 {

   x' := x;

 }

 

-procedure {:yields} {:stable} J()

+procedure {:yields} {:phase 0} J()

 {

 }

 

-procedure {:yields} P1({:linear ""} x:int) returns({:linear ""} x':int)

+procedure {:yields} {:phase 1} P1({:linear ""} x:int) returns({:linear ""} x':int)

 {

+  yield;

   par x' := I(x) | J();

+  yield;

   call x' := I(x');

+  yield;

 }

 

-procedure {:yields} P2({:linear ""} x:int) returns({:linear ""} x':int)

+procedure {:yields} {:phase 1} P2({:linear ""} x:int) returns({:linear ""} x':int)

 {

+  yield;

   call x' := I(x);

+  yield;

   par x' := I(x') | J();

+  yield;

 }

diff --git a/Test/og/DeviceCache.bpl b/Test/og/DeviceCache.bpl
index dd2968ee..0f6383ef 100644
--- a/Test/og/DeviceCache.bpl
+++ b/Test/og/DeviceCache.bpl
@@ -1,10 +1,10 @@
 type X;

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

 const nil: X;

-var {:qed} ghostLock: X;

-var {:qed} lock: X;

-var {:qed} currsize: int;

-var {:qed} newsize: int;

+var {:phase 1} ghostLock: X;

+var {:phase 1} lock: X;

+var {:phase 1} currsize: int;

+var {:phase 1} newsize: int;

 

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

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

@@ -22,14 +22,14 @@ function {:inline} Inv(ghostLock: X, currsize: int, newsize: int) : (bool)
     (ghostLock == nil <==> currsize == newsize)

 }

 

-procedure {:stable} {:yields} YieldToReadCache({:linear "tid"} tid': X) returns ({:linear "tid"} tid: X)

+procedure {:yields} {:phase 1} YieldToReadCache({:linear "tid"} tid': X) returns ({:linear "tid"} tid: X)

 requires {:phase 1} Inv(ghostLock, currsize, newsize) && tid' != nil;

 ensures {:phase 1} Inv(ghostLock, currsize, newsize) && tid != nil && tid == tid' && old(currsize) <= currsize;

 {

    tid := tid';

 }

 

-procedure {:stable} {:yields} YieldToWriteCache({:linear "tid"} tid': X) returns ({:linear "tid"} tid: X)

+procedure {:yields} {:phase 1} YieldToWriteCache({:linear "tid"} tid': X) returns ({:linear "tid"} tid: X)

 requires {:phase 1} Inv(ghostLock, currsize, newsize) && ghostLock == tid' && tid' != nil;

 ensures {:phase 1} Inv(ghostLock, currsize, newsize) && ghostLock == tid && tid != nil && tid == tid' && old(currsize) == currsize && old(newsize) == newsize;

 {

@@ -39,7 +39,7 @@ ensures {:phase 1} Inv(ghostLock, currsize, newsize) && ghostLock == tid && tid
 procedure Allocate({:linear "tid"} xls': [X]bool) returns ({:linear "tid"} xls: [X]bool, {:linear "tid"} xl: X);

 ensures {:phase 1} xl != nil;

 

-procedure {:entrypoint} {:yields} main({:linear "tid"} xls':[X]bool)

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

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

 {

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

@@ -56,11 +56,15 @@ requires {:phase 1} xls' == mapconstbool(true);
     invariant {:phase 1} Inv(ghostLock, currsize, newsize);

     {

         call xls, tid := Allocate(xls);

+	yield;

+    	assert {:phase 1} Inv(ghostLock, currsize, newsize);

         async call Thread(tid);

+	yield;

+    	assert {:phase 1} Inv(ghostLock, currsize, newsize);

     }

 }

 

-procedure {:yields} {:stable} Thread({:linear "tid"} tid': X)

+procedure {:yields} {:phase 1} Thread({:linear "tid"} tid': X)

 requires {:phase 1} tid' != nil;

 requires {:phase 1} Inv(ghostLock, currsize, newsize);

 {

@@ -73,7 +77,7 @@ requires {:phase 1} Inv(ghostLock, currsize, newsize);
     call bytesRead := Read(tid, start, size);

 }

 

-procedure {:yields} Read({:linear "tid"} tid': X, start : int, size : int) returns (bytesRead : int)

+procedure {:yields} {:phase 1} Read({:linear "tid"} tid': X, start : int, size : int) returns (bytesRead : int)

 requires {:phase 1} tid' != nil;

 requires {:phase 1} 0 <= start && 0 <= size;

 requires {:phase 1} Inv(ghostLock, currsize, newsize);

@@ -115,7 +119,7 @@ COPY_TO_BUFFER:
     call tid := ReadCache(tid, start, bytesRead);

 }

 

-procedure {:yields} WriteCache({:linear "tid"} tid': X, index: int) returns ({:linear "tid"} tid: X)

+procedure {:yields} {:phase 1} WriteCache({:linear "tid"} tid': X, index: int) returns ({:linear "tid"} tid: X)

 requires {:phase 1} Inv(ghostLock, currsize, newsize);

 requires {:phase 1} ghostLock == tid' && tid' != nil;

 ensures {:phase 1} tid == tid' && ghostLock == tid;

@@ -137,7 +141,7 @@ ensures {:phase 1} Inv(ghostLock, currsize, newsize) && old(currsize) == currsiz
     par tid := YieldToWriteCache(tid);

 }

 

-procedure {:yields} ReadCache({:linear "tid"} tid': X, start: int, bytesRead: int) returns ({:linear "tid"} tid: X)

+procedure {:yields} {:phase 1} ReadCache({:linear "tid"} tid': X, start: int, bytesRead: int) returns ({:linear "tid"} tid: X)

 requires {:phase 1} Inv(ghostLock, currsize, newsize);

 requires {:phase 1} tid' != nil;

 requires {:phase 1} 0 <= start && 0 <= bytesRead;

@@ -165,29 +169,29 @@ ensures {:phase 1} Inv(ghostLock, currsize, newsize);
     par tid := YieldToReadCache(tid);

 }

 

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

-ensures {:atomic 0} |{ A: assert xls' == mapconstbool(true); xls := xls'; currsize := 0; newsize := 0; lock := nil; ghostLock := nil; return true; }|;

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

+ensures {:atomic} |{ A: assert xls' == mapconstbool(true); xls := xls'; currsize := 0; newsize := 0; lock := nil; ghostLock := nil; return true; }|;

 

-procedure {:yields} ReadCurrsize({:linear "tid"} tid': X) returns ({:linear "tid"} tid: X, val: int);

-ensures {:right 0} |{A: assert tid' != nil; assert lock == tid' || ghostLock == tid'; tid := tid'; val := currsize; return true; }|;

+procedure {:yields} {:phase 0,1} ReadCurrsize({:linear "tid"} tid': X) returns ({:linear "tid"} tid: X, val: int);

+ensures {:right} |{A: assert tid' != nil; assert lock == tid' || ghostLock == tid'; tid := tid'; val := currsize; return true; }|;

 

-procedure {:yields} ReadNewsize({:linear "tid"} tid': X) returns ({:linear "tid"} tid: X, val: int);

-ensures {:right 0} |{A: assert tid' != nil; assert lock == tid' || ghostLock == tid'; tid := tid'; val := newsize; return true; }|;

+procedure {:yields} {:phase 0,1} ReadNewsize({:linear "tid"} tid': X) returns ({:linear "tid"} tid: X, val: int);

+ensures {:right} |{A: assert tid' != nil; assert lock == tid' || ghostLock == tid'; tid := tid'; val := newsize; return true; }|;

 

-procedure {:yields} WriteNewsize({:linear "tid"} tid': X, val: int) returns ({:linear "tid"} tid: X);

-ensures {:atomic 0} |{A: assert tid' != nil; assert lock == tid' && ghostLock == nil; tid := tid'; newsize := val; ghostLock := tid; return true; }|;

+procedure {:yields} {:phase 0,1} WriteNewsize({:linear "tid"} tid': X, val: int) returns ({:linear "tid"} tid: X);

+ensures {:atomic} |{A: assert tid' != nil; assert lock == tid' && ghostLock == nil; tid := tid'; newsize := val; ghostLock := tid; return true; }|;

 

-procedure {:yields} WriteCurrsize({:linear "tid"} tid': X, val: int) returns ({:linear "tid"} tid: X);

-ensures {:atomic 0} |{A: assert tid' != nil; assert lock == tid' && ghostLock == tid'; tid := tid'; currsize := val; ghostLock := nil; return true; }|;

+procedure {:yields} {:phase 0,1} WriteCurrsize({:linear "tid"} tid': X, val: int) returns ({:linear "tid"} tid: X);

+ensures {:atomic} |{A: assert tid' != nil; assert lock == tid' && ghostLock == tid'; tid := tid'; currsize := val; ghostLock := nil; return true; }|;

 

-procedure {:yields} ReadCacheEntry({:linear "tid"} tid': X, index: int) returns ({:linear "tid"} tid: X);

-ensures {:atomic 0} |{ A: assert 0 <= index && index < currsize; tid := tid'; return true; }|;

+procedure {:yields} {:phase 0,1} ReadCacheEntry({:linear "tid"} tid': X, index: int) returns ({:linear "tid"} tid: X);

+ensures {:atomic} |{ A: assert 0 <= index && index < currsize; tid := tid'; return true; }|;

 

-procedure {:yields} WriteCacheEntry({:linear "tid"} tid': X, index: int) returns ({:linear "tid"} tid: X);

-ensures {:right 0} |{ A: assert tid' != nil; assert currsize <= index && ghostLock == tid'; tid := tid'; return true; }|;

+procedure {:yields} {:phase 0,1} WriteCacheEntry({:linear "tid"} tid': X, index: int) returns ({:linear "tid"} tid: X);

+ensures {:right} |{ A: assert tid' != nil; assert currsize <= index && ghostLock == tid'; tid := tid'; return true; }|;

 

-procedure {:yields} acquire({:linear "tid"} tid': X) returns ({:linear "tid"} tid: X);

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

+procedure {:yields} {:phase 0,1} acquire({:linear "tid"} tid': X) returns ({:linear "tid"} tid: X);

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

 

-procedure {:yields} release({:linear "tid"} tid': X) returns ({:linear "tid"} tid: X);

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

+procedure {:yields} {:phase 0,1} release({:linear "tid"} tid': X) returns ({:linear "tid"} tid: X);

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

diff --git a/Test/og/FlanaganQadeer.bpl b/Test/og/FlanaganQadeer.bpl
index a263467c..e8df9515 100644
--- a/Test/og/FlanaganQadeer.bpl
+++ b/Test/og/FlanaganQadeer.bpl
@@ -1,7 +1,7 @@
 type X;

 const nil: X;

-var l: X;

-var x: int;

+var {:phase 1} l: X;

+var {:phase 1} x: int;

 

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

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

@@ -10,44 +10,55 @@ function {:inline} {:linear "tid"} TidCollector(x: X) : [X]bool
 }

 

 procedure Allocate() returns ({:linear "tid"} xls: X);

-ensures xls != nil;

+ensures {:phase 1} xls != nil;

 

-procedure {:entrypoint} {:yields} main()

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

 {

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

     var val: int;

 

     while (*) 

     {

+        yield;

         call tid := Allocate();

         havoc val;

         async call foo(tid, val);

+	yield;

     }

 }

+procedure {:yields} {:phase 0,1} Lock(tid: X);

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

 

-procedure {:yields} {:stable} foo({:linear "tid"} tid': X, val: int)

-requires tid' != nil;

+procedure {:yields} {:phase 0,1} Unlock();

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

+

+procedure {:yields} {:phase 0,1} Set(val: int);

+ensures {:atomic} |{A: x := val; return true; }|;

+

+procedure {:yields} {:phase 1} foo({:linear "tid"} tid': X, val: int)

+requires {:phase 1} tid' != nil;

 {

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

     tid := tid';

-    

-    assume l == nil;

-    l := tid;

+

+    yield;

+    call Lock(tid);    

     call tid := Yield(tid);

-    x := val;

+    call Set(val);

     call tid := Yield(tid);

-    assert x == val;

+    assert {:phase 1} x == val;

     call tid := Yield(tid);

-    l := nil;

+    call Unlock();

+    yield;

 }

 

-procedure {:yields} Yield({:linear "tid"} tid': X) returns ({:linear "tid"} tid: X)

-requires tid' != nil;

-ensures tid == tid';

-ensures old(l) == tid ==> old(l) == l && old(x) == x;

+procedure {:yields} {:phase 1} Yield({:linear "tid"} tid': X) returns ({:linear "tid"} tid: X)

+requires {:phase 1} tid' != nil;

+ensures {:phase 1} tid == tid';

+ensures {:phase 1} old(l) == tid ==> old(l) == l && old(x) == x;

 {

     tid := tid';

     yield;

-    assert tid != nil;

-    assert (old(l) == tid ==> old(l) == l && old(x) == x);

+    assert {:phase 1} tid != nil;

+    assert {:phase 1} (old(l) == tid ==> old(l) == l && old(x) == x);

 }
\ No newline at end of file
diff --git a/Test/og/akash.bpl b/Test/og/akash.bpl
index d31c20ee..90ccfebe 100644
--- a/Test/og/akash.bpl
+++ b/Test/og/akash.bpl
@@ -17,18 +17,24 @@ function {:inline} {:linear "2"} SetCollector2(x: [int]bool) : [int]bool
 }

 

 procedure Allocate() returns ({:linear "tid"} xls: int);

-ensures xls != 0;

+ensures {:phase 1} xls != 0;

 

 procedure Allocate_1() returns ({:linear "1"} xls: [int]bool);

-ensures xls == mapconstbool(true);

+ensures {:phase 1} xls == mapconstbool(true);

 

 procedure Allocate_2() returns ({:linear "2"} xls: [int]bool);

-ensures xls == mapconstbool(true);

+ensures {:phase 1} xls == mapconstbool(true);

 

-var g: int;

-var h: int;

+var {:phase 1} g: int;

+var {:phase 1} h: int;

 

-procedure {:yields} A({:linear "tid"} tid_in: int) returns ({:linear "tid"} tid_out: int) 

+procedure {:yields} {:phase 0,1} SetG(val:int);

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

+

+procedure {:yields} {:phase 0,1} SetH(val:int);

+ensures {:atomic} |{A: h := val; return true; }|;

+

+procedure {:yields} {:phase 1} A({:linear "tid"} tid_in: int) returns ({:linear "tid"} tid_out: int) 

 {

     var {:linear "1"} x: [int]bool;

     var {:linear "2"} y: [int]bool;

@@ -37,51 +43,62 @@ procedure {:yields} A({:linear "tid"} tid_in: int) returns ({:linear "tid"} tid_
     call x := Allocate_1();

     call y := Allocate_2();

 

-    g := 0;

     yield;

-    assert g == 0 && x == mapconstbool(true);    

+    call SetG(0);

+    yield;

+    assert {:phase 1} g == 0 && x == mapconstbool(true);    

 

     yield;

     call tid_child := Allocate();

     async call B(tid_child, x);

 

     yield;

-    h := 0;

+    call SetH(0);

 

     yield;

-    assert h == 0 && y == mapconstbool(true);    

+    assert {:phase 1} h == 0 && y == mapconstbool(true);    

 

     yield;

     call tid_child := Allocate();

     async call C(tid_child, y);

+

+    yield;

 }

 

-procedure {:yields} {:stable} B({:linear "tid"} tid_in: int, {:linear "1"} x_in: [int]bool) 

-requires x_in != mapconstbool(false);

+procedure {:yields} {:phase 1} B({:linear "tid"} tid_in: int, {:linear "1"} x_in: [int]bool) 

+requires {:phase 1} x_in != mapconstbool(false);

 {

     var {:linear "tid"} tid_out: int;

     var {:linear "1"} x: [int]bool;

     tid_out := tid_in;

     x := x_in;    

 

-    g := 1;

+    yield;

+

+    call SetG(1);

 

     yield;

 

-    g := 2;

+    call SetG(2);

+

+    yield;

 }

 

-procedure {:yields} {:stable} C({:linear "tid"} tid_in: int, {:linear "2"} y_in: [int]bool) 

-requires y_in != mapconstbool(false);

+procedure {:yields} {:phase 1} C({:linear "tid"} tid_in: int, {:linear "2"} y_in: [int]bool) 

+requires {:phase 1} y_in != mapconstbool(false);

 {

     var {:linear "tid"} tid_out: int;

     var {:linear "2"} y: [int]bool;

     tid_out := tid_in;

     y := y_in;    

 

-    h := 1;

+    yield;

+

+    call SetH(1);

 

     yield;

 

-    h := 2;

+    call SetH(2);

+

+    yield;

 }
\ No newline at end of file
diff --git a/Test/og/async.bpl b/Test/og/async.bpl
index 32f609bc..4ca43d30 100644
--- a/Test/og/async.bpl
+++ b/Test/og/async.bpl
@@ -1,8 +1,7 @@
-var x: int;

-var y: int;

+var {:phase 1} x: int;

+var {:phase 1} y: int;

 

-procedure {:entrypoint} {:yields} foo()

-modifies x, y; 

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

 {

   assume x == y;

   x := x + 1;

@@ -10,8 +9,8 @@ modifies x, y;
   y := y + 1;

 }

 

-procedure {:yields} {:stable} P()

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

 requires x != y;

 {

-  assert x != y;

+  assert {:phase 1} x != y;

 }
\ No newline at end of file
diff --git a/Test/og/bar.bpl b/Test/og/bar.bpl
index 920fc32c..22751d29 100644
--- a/Test/og/bar.bpl
+++ b/Test/og/bar.bpl
@@ -1,36 +1,55 @@
-var g:int;

+var {:phase 1} g:int;

 

-procedure {:yields} {:stable} PB()

-modifies g;

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

 {

-  g := g + 1;

+  yield;

+  call Incr();

+  yield;

 }

 

-procedure {:yields} PC()

-ensures g == old(g);

+procedure {:yields} {:phase 0,1} Incr();

+ensures {:atomic}

+|{A:

+  g := g + 1; return true;

+}|;

+

+procedure {:yields} {:phase 0,1} Set(v: int);

+ensures {:atomic}

+|{A:

+  g := v; return true;

+}|;

+

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

+ensures {:phase 1} g == old(g);

 {

   yield;

-  assert g == old(g);

+  assert {:phase 1} g == old(g);

 }

 

-procedure {:yields} {:stable} PE()

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

 {

   call PC();

 }

 

-procedure {:yields} {:stable} PD()

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

 {

-  g := 3;

+  yield;

+  call Set(3);

   call PC();

-  assert g == 3;

+  assert {:phase 1} g == 3;

 }

 

-procedure{:entrypoint} {:yields} Main2()

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

 {

+  yield;

   while (*)

   {

+    yield;

     async call PB();

+    yield;

     async call PE();

+    yield;

     async call PD();

+    yield;

   }

 }

diff --git a/Test/og/civl-paper.bpl b/Test/og/civl-paper.bpl
index 27c700f3..378bb8b5 100644
--- a/Test/og/civl-paper.bpl
+++ b/Test/og/civl-paper.bpl
@@ -13,31 +13,31 @@ 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;

+var {:phase 2} {: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} {:phase 1,2} TransferToGlobal({:cnst "tid"} tid: X, {:linear "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);

 

-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} {:phase 1,2} TransferFromGlobal({:cnst "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);

 

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

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

+procedure {:yields} {:phase 1} Load({:cnst "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} Store({:linear "mem"} l_in: lmap, a: int, v: int) returns ({:linear "mem"} l_out: lmap);

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

+procedure {:yields} {:phase 1} Store({:linear "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} P({:cnst "tid"} tid: X)

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

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

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

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

@@ -58,7 +58,7 @@ ensures {:phase 2} Inv(g);
     par Yield() | YieldLock();

 }

 

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

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

 requires {:phase 2} Inv(g);

 ensures {:phase 2} Inv(g);

 {

@@ -72,13 +72,13 @@ function {:inline} Inv(g: lmap) : bool
 }

 

 

-var {:qed 1} b: bool;

-var {:qed} lock: X;

+var {:phase 1} b: bool;

+var {:phase 2} lock: X;

 

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

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

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

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

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

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

 {

     var status: bool;

     var tmp: X;

@@ -100,8 +100,8 @@ ensures {:right 1} |{ A: assert tid != nil; assume lock == nil; lock := tid; ret
 	goto L;

 }

 

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

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

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

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

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

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

 {

@@ -110,19 +110,19 @@ ensures {:phase 1} InvLock(lock, b);
     par YieldLock();

 }

 

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

-ensures {:atomic 0,1} |{ 

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

+ensures {:atomic} |{ 

 A: goto B, C; 

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

 C: status := false; return true; 

 }|;

 

-procedure {:yields} CLEAR(tid: X, next: bool);

-ensures {:atomic 0,1} |{ 

+procedure {:yields} {:phase 0,1} CLEAR(tid: X, next: bool);

+ensures {:atomic} |{ 

 A: b := next; lock := nil; return true; 

 }|;

 

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

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

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

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

 {

diff --git a/Test/og/foo.bpl b/Test/og/foo.bpl
index 831d2b97..400f5a4e 100644
--- a/Test/og/foo.bpl
+++ b/Test/og/foo.bpl
@@ -1,37 +1,55 @@
-var g:int;

+var {:phase 1} g:int;

 

-procedure {:yields} {:stable} PB()

-modifies g;

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

 {

-  g := g + 1;

+  yield;

+  call Incr();

+  yield;

 }

 

-procedure {:yields} PC()

-ensures g == 3;

+procedure {:yields} {:phase 0,1} Incr();

+ensures {:atomic}

+|{A:

+  g := g + 1; return true;

+}|;

+

+procedure {:yields} {:phase 0,1} Set(v: int);

+ensures {:atomic}

+|{A:

+  g := v; return true;

+}|;

+

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

+ensures {:phase 1} g == 3;

 {

-  g := 3;

   yield;

-  assert g == 3;

+  call Set(3);

+  yield;

+  assert {:phase 1} g == 3;

 }

 

-procedure {:yields} {:stable} PE()

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

 {

   call PC();

 }

 

-procedure {:yields} {:stable} PD()

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

 {

   call PC();

-  assert g == 3;

-  yield;

+  assert {:phase 1} g == 3;

 }

 

-procedure {:entrypoint} {:yields} Main()

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

 {

+  yield;

   while (*)

   {

+    yield;

     async call PB();

+    yield;

     async call PE();

+    yield;

     async call PD();

+    yield;

   }

 }

diff --git a/Test/og/linear-set.bpl b/Test/og/linear-set.bpl
index ff3f5b1e..9effc04d 100644
--- a/Test/og/linear-set.bpl
+++ b/Test/og/linear-set.bpl
@@ -18,16 +18,26 @@ function {:inline} {:linear "x"} XCollector(xs: [X]bool) : [X]bool
   xs

 }

 

-var x: int;

-var l: [X]bool;

+var {:phase 1} x: int;

+var {:phase 1} l: [X]bool;

 

 procedure Split({:linear "x"} xls: [X]bool) returns ({:linear "x"} xls1: [X]bool, {:linear "x"} xls2: [X]bool);

 ensures xls == MapOr(xls1, xls2) && xls1 != None() && xls2 != None();

 

 procedure Allocate() returns ({:linear "tid"} xls: [X]bool);

 

-procedure {:entrypoint} {:yields} main({:linear "tid"} tidls': [X]bool, {:linear "x"} xls': [X]bool) 

-requires tidls' != None() && xls' == All();

+procedure {:yields} {:phase 0,1} Set(v: int);

+ensures {:atomic} |{A: x := v; return true; }|;

+

+procedure {:yields} {:phase 0,1} Lock(tidls: [X]bool);

+ensures {:atomic} |{A: assume l == None(); l := tidls; return true; }|;

+

+procedure {:yields} {:phase 0,1} Unlock();

+ensures {:atomic} |{A: l := None(); return true; }|;

+

+

+procedure {:yields} {:phase 1} main({:linear "tid"} tidls': [X]bool, {:linear "x"} xls': [X]bool) 

+requires {:phase 1} tidls' != None() && xls' == All();

 {

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

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

@@ -37,22 +47,25 @@ requires tidls' != None() && xls' == All();
 

     tidls := tidls';

     xls := xls';

-

-    x := 42;

     yield;

-    assert xls == All();

-    assert x == 42;

+    call Set(42);

+    yield;

+    assert {:phase 1} xls == All();

+    assert {:phase 1} x == 42;

     call xls1, xls2 := Split(xls);

     call lsChild := Allocate();

     assume (lsChild != None());

+    yield;

     async call thread(lsChild, xls1);

     call lsChild := Allocate();

     assume (lsChild != None());

+    yield;

     async call thread(lsChild, xls2);

+    yield;

 }

 

-procedure {:yields} {:stable} thread({:linear "tid"} tidls': [X]bool, {:linear "x"} xls': [X]bool)

-requires tidls' != None() && xls' != None();

+procedure {:yields} {:phase 1} thread({:linear "tid"} tidls': [X]bool, {:linear "x"} xls': [X]bool)

+requires {:phase 1} tidls' != None() && xls' != None();

 {

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

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

@@ -60,15 +73,15 @@ requires tidls' != None() && xls' != None();
     tidls := tidls';

     xls := xls';

 

-    assume l == None();

-    l := tidls;

     yield;

-    assert tidls != None() && xls != None();

-    x := 0;

+    call Lock(tidls);

+    yield;

+    assert {:phase 1} tidls != None() && xls != None();

+    call Set(0);

     yield;

-    assert tidls != None() && xls != None();

-    assert x == 0;

+    assert {:phase 1} tidls != None() && xls != None();

+    assert {:phase 1} x == 0;

+    assert {:phase 1} tidls != None() && xls != None();

+    call Unlock();

     yield;

-    assert tidls != None() && xls != None();

-    l := None();

 }

diff --git a/Test/og/linear-set2.bpl b/Test/og/linear-set2.bpl
index 04406609..36a8f9c7 100644
--- a/Test/og/linear-set2.bpl
+++ b/Test/og/linear-set2.bpl
@@ -18,8 +18,8 @@ function {:inline} {:linear "x"} XCollector(xs: [X]bool) : [X]bool
   xs

 }

 

-var x: int;

-var l: X;

+var {:phase 1} x: int;

+var {:phase 1} l: X;

 const nil: X;

 

 procedure Split({:linear "x"} xls: [X]bool) returns ({:linear "x"} xls1: [X]bool, {:linear "x"} xls2: [X]bool);

@@ -28,8 +28,17 @@ ensures xls == MapOr(xls1, xls2) && xls1 != None() && xls2 != None();
 procedure Allocate() returns ({:linear "tid"} xls: X);

 ensures xls != nil;

 

-procedure {:entrypoint}  {:yields} main({:linear "tid"} tidls': X, {:linear "x"} xls': [X]bool) 

-requires tidls' != nil && xls' == All();

+procedure {:yields} {:phase 0,1} Set(v: int);

+ensures {:atomic} |{A: x := v; return true; }|;

+

+procedure {:yields} {:phase 0,1} Lock(tidls: X);

+ensures {:atomic} |{A: assume l == nil; l := tidls; return true; }|;

+

+procedure {:yields} {:phase 0,1} Unlock();

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

+

+procedure {:yields} {:phase 1} main({:linear "tid"} tidls': X, {:linear "x"} xls': [X]bool) 

+requires {:phase 1} tidls' != nil && xls' == All();

 {

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

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

@@ -40,19 +49,23 @@ requires tidls' != nil && xls' == All();
     tidls := tidls';

     xls := xls';

 

-    x := 42;

     yield;

-    assert xls == All();

-    assert x == 42;

+    call Set(42);

+    yield;

+    assert {:phase 1} xls == All();

+    assert {:phase 1} x == 42;

     call xls1, xls2 := Split(xls);

     call lsChild := Allocate();

+    yield;

     async call thread(lsChild, xls1);

     call lsChild := Allocate();

+    yield;

     async call thread(lsChild, xls2);

+    yield;

 }

 

-procedure {:yields} {:stable} thread({:linear "tid"} tidls': X, {:linear "x"} xls': [X]bool)

-requires tidls' != nil && xls' != None();

+procedure {:yields} {:phase 1} thread({:linear "tid"} tidls': X, {:linear "x"} xls': [X]bool)

+requires {:phase 1} tidls' != nil && xls' != None();

 {

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

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

@@ -60,15 +73,16 @@ requires tidls' != nil && xls' != None();
     tidls := tidls';

     xls := xls';

 

-    assume l == nil;

-    l := tidls;

     yield;

-    assert tidls != nil && xls != None();

-    x := 0;

+    call Lock(tidls);

+    yield;

+    assert {:phase 1} tidls != nil && xls != None();

+    call Set(0);

+    yield;

+    assert {:phase 1} tidls != nil && xls != None();

+    assert {:phase 1} x == 0;

     yield;

-    assert tidls != nil && xls != None();

-    assert x == 0;

+    assert {:phase 1} tidls != nil && xls != None();

+    call Unlock();

     yield;

-    assert tidls != nil && xls != None();

-    l := nil;

 }

diff --git a/Test/og/lock.bpl b/Test/og/lock.bpl
index 92b803a4..4a6e002d 100644
--- a/Test/og/lock.bpl
+++ b/Test/og/lock.bpl
@@ -1,14 +1,18 @@
-var {:qed} b: bool;

+var {:phase 2} b: bool;

 

-procedure {:yields} {:entrypoint} main()

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

 {

     while (*)

     {

+        yield;

+

         async call Customer();

+

+        yield;

     }

 }

 

-procedure {:yields} {:stable} Customer()

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

 {

     while (*) 

     {

@@ -19,13 +23,15 @@ procedure {:yields} {:stable} Customer()
     	yield;

 

     	call Leave();

+

+        yield;

     }

 

     yield;

 }

 

-procedure {:yields} Enter() 

-ensures {:atomic 1} |{ A: assume !b; b := true; return true; }|;

+procedure {:yields} {:phase 1,2} Enter() 

+ensures {:atomic} |{ A: assume !b; b := true; return true; }|;

 {

     var status: bool;

     yield;

@@ -44,12 +50,12 @@ ensures {:atomic 1} |{ A: assume !b; b := true; return true; }|;
 	goto L;

 }

 

-procedure {:yields} CAS(prev: bool, next: bool) returns (status: bool);

-ensures {:atomic 0} |{ 

+procedure {:yields} {:phase 0,2} 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 0} |{ A: b := false; return true; }|;

+procedure {:yields} {:phase 0,2} Leave();

+ensures {:atomic} |{ A: b := false; return true; }|;

diff --git a/Test/og/lock2.bpl b/Test/og/lock2.bpl
index 307d55c8..b173ecd4 100644
--- a/Test/og/lock2.bpl
+++ b/Test/og/lock2.bpl
@@ -1,14 +1,18 @@
-var {:qed} b: int;

+var {:phase 2} b: int;

 

-procedure {:yields} {:entrypoint} main()

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

 {

     while (*)

     {

+        yield;

+

         async call Customer();

+

+        yield;

     }

 }

 

-procedure {:yields} {:stable} Customer()

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

 {

     while (*) 

     {

@@ -19,13 +23,15 @@ procedure {:yields} {:stable} Customer()
     	yield;

 

     	call Leave();

+

+        yield;

     }

 

     yield;

 }

 

-procedure {:yields} Enter() 

-ensures {:atomic 1} |{ A: assume b == 0; b := 1; return true; }|;

+procedure {:yields} {:phase 1,2} Enter() 

+ensures {:atomic} |{ A: assume b == 0; b := 1; return true; }|;

 {

     var _old, curr: int;

     while (true) { 

@@ -46,15 +52,15 @@ ensures {:atomic 1} |{ A: assume b == 0; b := 1; return true; }|;
     }

 }

 

-procedure {:yields} Read() returns (val: int);

-ensures {:atomic 0} |{ A: val := b; return true; }|;

+procedure {:yields} {:phase 0,2} Read() returns (val: int);

+ensures {:atomic} |{ A: val := b; return true; }|;

 

-procedure {:yields} CAS(prev: int, next: int) returns (_old: int);

-ensures {:atomic 0} |{ 

+procedure {:yields} {:phase 0,2} CAS(prev: int, next: int) returns (_old: int);

+ensures {:atomic} |{ 

 A: _old := b; goto B, C; 

 B: assume _old == prev; b := next; return true; 

 C: assume _old != prev; return true; 

 }|;

 

-procedure {:yields} Leave();

-ensures {:atomic 0} |{ A: b := 0; return true; }|;

+procedure {:yields} {:phase 0,2} Leave();

+ensures {:atomic} |{ A: b := 0; return true; }|;

diff --git a/Test/og/multiset.bpl b/Test/og/multiset.bpl
index 5bb056f3..3305b63f 100644
--- a/Test/og/multiset.bpl
+++ b/Test/og/multiset.bpl
@@ -4,10 +4,10 @@ const unique null : int;
 const unique nil: X;

 const unique done: X;

 

-var {:qed} elt : [int]int;

-var {:qed} valid : [int]bool;

-var {:qed} lock : [int]X;

-var {:qed} owner : [int]X;

+var elt : [int]int;

+var valid : [int]bool;

+var lock : [int]X;

+var owner : [int]X;

 const max : int;

 

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

@@ -18,8 +18,8 @@ function {:inline} {:linear "tid"} TidCollector(x: X) : [X]bool
 

 axiom (max > 0);

 

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

-ensures {:right 0} |{ A: 

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

+ensures {:right} |{ A: 

                       assert 0 <= i && i < max;

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

                       assume lock[i] == nil;

@@ -29,8 +29,8 @@ ensures {:right 0} |{ A:
                     }|;

 

 

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

-ensures {:left 0} |{ A: 

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

+ensures {:left} |{ A: 

                      assert 0 <= i && i < max;

                      assert lock[i] == tidIn;

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

@@ -40,8 +40,8 @@ ensures {:left 0} |{ A:
                     }|;

 

 

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

-ensures {:both 0,1} |{ A: 

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

+ensures {:both} |{ A: 

                      assert 0 <= j && j < max;

                      assert lock[j] == tidIn;

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

@@ -51,8 +51,8 @@ ensures {:both 0,1} |{ A:
                     }|;

 

 

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

-ensures {:both 0,1} |{ A: 

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

+ensures {:both} |{ A: 

                      assert x != null;

                      assert owner[j] == nil;

                      assert 0 <= j && j < max;

@@ -65,8 +65,8 @@ ensures {:both 0,1} |{ A:
                     }|;

 

 

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

-ensures {:left 0} |{ A: 

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

+ensures {:left} |{ A: 

                      assert owner[j] == tidIn;

                      assert 0 <= j && j < max;

                      assert lock[j] == tidIn;

@@ -78,8 +78,8 @@ ensures {:left 0} |{ A:
                      return true;

                     }|;

 

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

-ensures {:both 0} |{ A: 

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

+ensures {:both} |{ A: 

                      assert 0 <= j && j < max;

                      assert lock[j] == tidIn;

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

@@ -90,8 +90,8 @@ ensures {:both 0} |{ A:
                      return true;

                     }|;

 

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

-ensures {:both 0} |{ A: 

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

+ensures {:both} |{ A: 

                        assert 0 <= j && j < max;

                        assert lock[j] == tidIn;

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

@@ -100,10 +100,10 @@ ensures {:both 0} |{ A:
                        return true;

                     }|;

 

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

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

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

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

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

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

                           assert x != null; 

 			  goto B, C;

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

@@ -159,12 +159,12 @@ ensures {:right 1}  |{ A: assert tidIn != nil && tidIn != done;
 	return;

 }

 

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

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

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

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

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

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

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

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

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

                            assert x != null;

                            goto B, C;

@@ -204,7 +204,7 @@ ensures {:atomic 2}  |{ var r:int;
 	return;

 }

 

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

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

                                y : int, 

                                {:linear "tid"} tidIn: X) 

                                returns (result : bool, 

@@ -213,7 +213,7 @@ requires {:phase 1} Inv(valid, elt, owner);
 ensures {:phase 1} Inv(valid, elt, owner);

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

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

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

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

                         var ry:int;

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

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

@@ -285,12 +285,12 @@ ensures {:atomic 2}  |{ var rx:int;
 	return;

 }

 

-procedure {:yields} LookUp(x : int, {:linear "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"} tidIn: X, old_valid:[int]bool, old_elt:[int]int) returns (found : bool, {:linear "tid"} tidOut: X)

 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);

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

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

+ensures {:atomic}  |{ A: assert tidIn != nil && tidIn != 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));

@@ -335,14 +335,13 @@ ensures {:atomic 2}  |{ A: assert tidIn != nil && tidIn != done;
 	return;

 }

 

-procedure {:yields} {:stable} Yield1()

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

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

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

-ensures {:both 1} |{ A: return true; }|;

 {

 }

 

-procedure {:yields} {:stable} Yield12()

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

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

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

 {

@@ -355,7 +354,7 @@ function {:inline} Inv(valid: [int]bool, elt: [int]int, owner: [int]X): (bool)
    (forall i:int :: 0 <= i && i < max ==> (elt[i] == null <==> (!valid[i] && owner[i] == nil)))

 }

 

-procedure {:yields} {:stable} YieldLookUp(old_valid: [int]bool, old_elt: [int]int)

+procedure {:yields} {:phase 2} YieldLookUp(old_valid: [int]bool, old_elt: [int]int)

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

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

 {

diff --git a/Test/og/new1.bpl b/Test/og/new1.bpl
index 3ba0840d..6854e29c 100644
--- a/Test/og/new1.bpl
+++ b/Test/og/new1.bpl
@@ -1,6 +1,6 @@
 function {:builtin "MapConst"} mapconstbool(x:bool): [int]bool;

 

-var g:int;

+var {:phase 1} g:int;

 

 function {:inline} {:linear "Perm"} SetCollectorPerm(x: [int]bool) : [int]bool

 {

@@ -11,30 +11,37 @@ procedure Allocate_Perm({:linear "Perm"} Permissions: [int]bool) returns ({:line
 requires Permissions == mapconstbool(true);

 ensures xls == mapconstbool(true);

 

-procedure {:yields} {:stable} PB({:linear "Perm"} permVar_in:[int]bool)

-requires permVar_in[0] && g == 0;

+procedure {:yields} {:phase 1} PB({:linear "Perm"} permVar_in:[int]bool)

+requires {:phase 1} permVar_in[0] && g == 0;

 {

   var {:linear "Perm"} permVar_out: [int]bool;

   permVar_out := permVar_in;

 

   yield;

-  assert permVar_out[0];

-  assert g == 0;

+  assert {:phase 1} permVar_out[0];

+  assert {:phase 1} g == 0;

 

-  g := g + 1;

+  call IncrG();

 

   yield;

-  assert permVar_out[0];

-  assert g == 1;

+  assert {:phase 1} permVar_out[0];

+  assert {:phase 1} g == 1;

 }

 

-procedure{:entrypoint} {:yields} Main({:linear "Perm"} Permissions: [int]bool)

-requires Permissions == mapconstbool(true);

+procedure {:yields} {:phase 1} Main({:linear "Perm"} Permissions: [int]bool)

+requires {:phase 0,1} Permissions == mapconstbool(true);

 {

   var {:linear "Perm"} permVar_out: [int]bool;

 

   call permVar_out := Allocate_Perm(Permissions);

-

-  g := 0;

+  yield;

+  call SetG(0);

   async call PB(permVar_out);

+  yield;

 }

+

+procedure {:yields} {:phase 0,1} SetG(val:int);

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

+

+procedure {:yields} {:phase 0,1} IncrG();

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

diff --git a/Test/og/one.bpl b/Test/og/one.bpl
index 2a63d60d..1da2f116 100644
--- a/Test/og/one.bpl
+++ b/Test/og/one.bpl
@@ -1,4 +1,10 @@
-var x:int;

+var {:phase 1} x:int;

+

+procedure {:yields} {:phase 0,1} Set(v: int);

+ensures {:atomic}

+|{A:

+  x := v; return true;

+}|;

 

 procedure A()

 modifies x;

@@ -6,10 +12,11 @@ modifies x;
   x := x;

 }

 

-procedure {:yields} B()

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

 {

-  x := 5;

   yield;

-  assert x == 5;

+  call Set(5);

+  yield;

+  assert {:phase 1} x == 5;

 }

 

diff --git a/Test/og/parallel1.bpl b/Test/og/parallel1.bpl
index fc33d6cc..18050e09 100644
--- a/Test/og/parallel1.bpl
+++ b/Test/og/parallel1.bpl
@@ -1,27 +1,41 @@
-var g:int;

+var {:phase 1} g:int;

 

-procedure {:yields} {:stable} PB()

-modifies g;

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

 {

-  g := g + 1;

+  yield;

+  call Incr();

+  yield;

 }

 

-procedure {:yields} {:stable} PC()

-ensures g == 3;

+procedure {:yields} {:phase 0,1} Incr();

+ensures {:atomic}

+|{A:

+  g := g + 1; return true;

+}|;

+

+procedure {:yields} {:phase 0,1} Set(v: int);

+ensures {:atomic}

+|{A:

+  g := v; return true;

+}|;

+

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

+ensures {:phase 1} g == 3;

 {

-  g := 3;

   yield;

-  assert g == 3;

+  call Set(3);

+  yield;

+  assert {:phase 1} g == 3;

 }

 

-procedure {:yields} {:stable} PD()

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

 {

   call PC();

-  assert g == 3;

+  assert {:phase 1} g == 3;

   yield;

 }

 

-procedure {:entrypoint} {:yields} Main()

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

 {

   while (true)

   {

diff --git a/Test/og/parallel2.bpl b/Test/og/parallel2.bpl
index 07864511..4a3c1849 100644
--- a/Test/og/parallel2.bpl
+++ b/Test/og/parallel2.bpl
@@ -1,4 +1,4 @@
-var a:[int]int;

+var {:phase 1} a:[int]int;

 

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

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

@@ -8,7 +8,10 @@ function {:inline} {:linear "tid"} TidCollector(x: int) : [int]bool
 

 procedure Allocate() returns ({:linear "tid"} xls: int);

 

-procedure {:entrypoint} {:yields} main() 

+procedure {:yields} {:phase 0,1} Write(idx: int, val: int);

+ensures {:atomic} |{A: a[idx] := val; return true; }|;

+

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

 {

     var {:linear "tid"} i: int;

     var {:linear "tid"} j: int;

@@ -18,29 +21,31 @@ procedure {:entrypoint} {:yields} main()
     par i := u(i) | j := u(j);

 }

 

-procedure {:yields} {:stable} t({:linear "tid"} i': int) returns ({:linear "tid"} i: int)

+procedure {:yields} {:phase 1} t({:linear "tid"} i': int) returns ({:linear "tid"} i: int)

 {

     i := i';

 

-    a[i] := 42;

+    yield;

+    call Write(i, 42);

     call i := Yield(i);

-    assert a[i] == 42;

+    assert {:phase 1} a[i] == 42;

 }

 

-procedure {:yields} {:stable} u({:linear "tid"} i': int) returns ({:linear "tid"} i: int) 

+procedure {:yields} {:phase 1} u({:linear "tid"} i': int) returns ({:linear "tid"} i: int) 

 {

     i := i';

 

-    a[i] := 42;

     yield;

-    assert a[i] == 42;

+    call Write(i, 42);

+    yield;

+    assert {:phase 1} a[i] == 42;

 }

 

-procedure {:yields} Yield({:linear "tid"} i': int) returns ({:linear "tid"} i: int)

-ensures i == i';

-ensures old(a)[i] == a[i];

+procedure {:yields} {:phase 1} Yield({:linear "tid"} i': int) returns ({:linear "tid"} i: int)

+ensures {:phase 1} i == i';

+ensures {:phase 1} old(a)[i] == a[i];

 {

     i := i';

     yield;

-    assert old(a)[i] == a[i];

+    assert {:phase 1} old(a)[i] == a[i];

 }
\ No newline at end of file
diff --git a/Test/og/parallel4.bpl b/Test/og/parallel4.bpl
index 1069399f..2a2feb2d 100644
--- a/Test/og/parallel4.bpl
+++ b/Test/og/parallel4.bpl
@@ -1,4 +1,4 @@
-var a:int;

+var {:phase 1} a:int;

 

 procedure Allocate() returns ({:linear "tid"} xls: int);

 

@@ -8,7 +8,7 @@ function {:inline} {:linear "tid"} TidCollector(x: int) : [int]bool
   MapConstBool(false)[x := true]

 }

 

-procedure {:entrypoint} {:yields} main() 

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

 {

   var {:linear "tid"} i: int;

   var {:linear "tid"} j: int;

@@ -17,15 +17,19 @@ procedure {:entrypoint} {:yields} main()
   par i := t(i) | j := t(j);

 }

 

-procedure {:yields} {:stable} t({:linear "tid"} i': int) returns ({:linear "tid"} i: int)

+procedure {:yields} {:phase 1} t({:linear "tid"} i': int) returns ({:linear "tid"} i: int)

 {

   i := i';

   call Yield();

-  assert a == old(a);

-  a := a + 1;

+  assert {:phase 1} a == old(a);

+  call Incr();

+  yield;

 }

 

-procedure {:yields} Yield()

+procedure {:yields} {:phase 0,1} Incr();

+ensures {:atomic} |{A: a := a + 1; return true; }|;

+

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

 {

   yield;

 }

diff --git a/Test/og/parallel5.bpl b/Test/og/parallel5.bpl
index 01bbe74d..330b970d 100644
--- a/Test/og/parallel5.bpl
+++ b/Test/og/parallel5.bpl
@@ -1,4 +1,4 @@
-var a:[int]int;

+var {:phase 1} a:[int]int;

 

 procedure Allocate() returns ({:linear "tid"} xls: int);

 

@@ -8,7 +8,10 @@ function {:inline} {:linear "tid"} TidCollector(x: int) : [int]bool
   MapConstBool(false)[x := true]

 }

 

-procedure {:entrypoint} {:yields} main() 

+procedure {:yields} {:phase 0,1} Write(idx: int, val: int);

+ensures {:atomic} |{A: a[idx] := val; return true; }|;

+

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

 {

     var {:linear "tid"} i: int;

     var {:linear "tid"} j: int;

@@ -18,29 +21,31 @@ procedure {:entrypoint} {:yields} main()
     par i := u(i) | j := u(j);

 }

 

-procedure {:yields} {:stable} t({:linear "tid"} i': int) returns ({:linear "tid"} i: int)

+procedure {:yields} {:phase 1} t({:linear "tid"} i': int) returns ({:linear "tid"} i: int)

 {

     i := i';

 

-    a[i] := 42;

+    yield;

+    call Write(i, 42);

     call i := Yield(i);

-    assert a[i] == 42;

+    assert {:phase 1} a[i] == 42;

 }

 

-procedure {:yields} {:stable} u({:linear "tid"} i': int) returns ({:linear "tid"} i: int) 

+procedure {:yields} {:phase 1} u({:linear "tid"} i': int) returns ({:linear "tid"} i: int) 

 {

     i := i';

 

-    a[i] := 42;

     yield;

-    assert a[i] == 42;

+    call Write(i, 42);

+    yield;

+    assert {:phase 1} a[i] == 42;

 }

 

-procedure {:yields} {:stable} Yield({:linear "tid"} i': int) returns ({:linear "tid"} i: int)

-ensures i == i';

-ensures old(a)[i] == a[i];

+procedure {:yields} {:phase 1} Yield({:linear "tid"} i': int) returns ({:linear "tid"} i: int)

+ensures {:phase 1} i == i';

+ensures {:phase 1} old(a)[i] == a[i];

 {

     i := i';

     yield;

-    assert old(a)[i] == a[i];

+    assert {:phase 1} old(a)[i] == a[i];

 }
\ No newline at end of file
diff --git a/Test/og/perm.bpl b/Test/og/perm.bpl
index 8b77ce1b..6d07ca75 100644
--- a/Test/og/perm.bpl
+++ b/Test/og/perm.bpl
@@ -1,4 +1,4 @@
-var x: int;

+var {:phase 1} x: int;

 function {:builtin "MapConst"} ch_mapconstbool(x: bool) : [int]bool;

 

 function {:builtin "MapOr"} ch_mapunion(x: [int]bool, y: [int]bool) : [int]bool;

@@ -12,44 +12,44 @@ procedure Split({:linear "Perm"} xls: [int]bool) returns ({:linear "Perm"} xls1:
   ensures xls == ch_mapunion(xls1, xls2) && xls1 != ch_mapconstbool(false) && xls2 != ch_mapconstbool(false);

 

 

-procedure {:entrypoint} {:yields} mainE({:linear "Perm"} permVar_in: [int]bool)

-   free requires permVar_in == ch_mapconstbool(true);

-   free requires permVar_in[0];

-  modifies x;

+procedure {:yields} {:phase 1} mainE({:linear "Perm"} permVar_in: [int]bool)

+   free requires {:phase 1} permVar_in == ch_mapconstbool(true);

+   free requires {:phase 1} permVar_in[0];

+   free requires {:phase 1} x == 0;

 {

     var {:linear "Perm"} permVar_out: [int]bool;

     var {:linear "Perm"} permVarOut2: [int]bool;

 

     permVar_out := permVar_in;

 

-    assume x == 0;

-

     yield;

-    assert x == 0;

-    assert permVar_out[0];

-    assert permVar_out == ch_mapconstbool(true);

+    assert {:phase 1} x == 0;

+    assert {:phase 1} permVar_out[0];

+    assert {:phase 1} permVar_out == ch_mapconstbool(true);

 

     call permVar_out, permVarOut2 := Split(permVar_out);

     async call foo(permVarOut2);

+    yield;

 }

 

-procedure {:yields} {:stable} foo({:linear "Perm"} permVar_in: [int]bool) 

-  free requires permVar_in != ch_mapconstbool(false);

-  free requires permVar_in[1];

-  requires x == 0;

-  modifies x;

+procedure {:yields} {:phase 1} foo({:linear "Perm"} permVar_in: [int]bool) 

+  free requires {:phase 1} permVar_in != ch_mapconstbool(false);

+  free requires {:phase 1} permVar_in[1];

+  requires {:phase 1} x == 0;

 {

   var {:linear "Perm"} permVar_out: [int]bool;

   permVar_out := permVar_in;

   

   yield;

-  assert permVar_out[1];

-  assert x == 0;

+  assert {:phase 1} permVar_out[1];

+  assert {:phase 1} x == 0;

 

-  x := x + 1;

+  call Incr();

 

   yield;

-  assert permVar_out[1];

-  assert x == 1;

+  assert {:phase 1} permVar_out[1];

+  assert {:phase 1} x == 1;

 }

 

+procedure {:yields} {:phase 0,1} Incr();

+ensures {:atomic} |{A: x := x + 1; return true; }|;
\ No newline at end of file
diff --git a/Test/og/runtest.bat b/Test/og/runtest.bat
index 80f614ae..2a1d8ebb 100644
--- a/Test/og/runtest.bat
+++ b/Test/og/runtest.bat
@@ -9,7 +9,7 @@ for %%f in (foo.bpl bar.bpl one.bpl parallel1.bpl) do (
   %BGEXE% %* /nologo /noinfer %%f

 )

 

-for %%f in (linear-set.bpl linear-set2.bpl FlanaganQadeer.bpl DeviceCacheSimplified.bpl parallel2.bpl parallel4.bpl parallel5.bpl akash.bpl t1.bpl new1.bpl perm.bpl async.bpl DeviceCache.bpl ticket.bpl lock.bpl lock2.bpl multiset.bpl civl-paper.bpl) do (

+for %%f in (linear-set.bpl linear-set2.bpl FlanaganQadeer.bpl parallel2.bpl parallel4.bpl parallel5.bpl akash.bpl t1.bpl new1.bpl perm.bpl DeviceCache.bpl ticket.bpl lock.bpl lock2.bpl multiset.bpl civl-paper.bpl) do (

   echo.

   echo -------------------- %%f --------------------

   %BGEXE% %* /nologo /noinfer /typeEncoding:m /useArrayTheory %%f

diff --git a/Test/og/t1.bpl b/Test/og/t1.bpl
index 43758a91..c7e30dd9 100644
--- a/Test/og/t1.bpl
+++ b/Test/og/t1.bpl
@@ -17,18 +17,24 @@ function {:inline} {:linear "2"} SetCollector2(x: [int]bool) : [int]bool
 }

 

 procedure Allocate() returns ({:linear "tid"} xls: int);

-ensures xls != 0;

+ensures {:phase 1} xls != 0;

 

 procedure Allocate_1() returns ({:linear "1"} xls: [int]bool);

-ensures xls == mapconstbool(true);

+ensures {:phase 1} xls == mapconstbool(true);

 

 procedure Allocate_2() returns ({:linear "2"} xls: [int]bool);

-ensures xls == mapconstbool(true);

+ensures {:phase 1} xls == mapconstbool(true);

 

-var g: int;

-var h: int;

+var {:phase 1} g: int;

+var {:phase 1} h: int;

 

-procedure {:yields} A({:linear "tid"} tid_in: int) returns ({:linear "tid"} tid_out: int) 

+procedure {:yields} {:phase 0,1} SetG(val:int);

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

+

+procedure {:yields} {:phase 0,1} SetH(val:int);

+ensures {:atomic} |{A: h := val; return true; }|;

+

+procedure {:yields} {:phase 1} A({:linear "tid"} tid_in: int) returns ({:linear "tid"} tid_out: int) 

 {

     var {:linear "1"} x: [int]bool;

     var {:linear "2"} y: [int]bool;

@@ -37,48 +43,55 @@ procedure {:yields} A({:linear "tid"} tid_in: int) returns ({:linear "tid"} tid_
     call x := Allocate_1();

     call y := Allocate_2();

 

-    g := 0;

     yield;

-    assert x == mapconstbool(true);    

-    assert g == 0;    

+    call SetG(0);

+    yield;

+    assert {:phase 1} x == mapconstbool(true);    

+    assert {:phase 1} g == 0;    

 

     yield;

     call tid_child := Allocate();

     async call B(tid_child, x);

 

     yield;

-    assert x == mapconstbool(true);    

-    assert g == 0;

+    assert {:phase 1} x == mapconstbool(true);    

+    assert {:phase 1} g == 0;

 

     yield;

-    h := 0;

+    call SetH(0);

 

     yield;

-    assert h == 0 && y == mapconstbool(true);    

+    assert {:phase 1} h == 0 && y == mapconstbool(true);    

 

     yield;

     call tid_child := Allocate();

     async call C(tid_child, y);

+

+    yield;

 }

 

-procedure {:yields} {:stable} B({:linear "tid"} tid_in: int, {:linear "1"} x_in: [int]bool) 

-requires x_in != mapconstbool(false);

+procedure {:yields} {:phase 1} B({:linear "tid"} tid_in: int, {:linear "1"} x_in: [int]bool) 

+requires {:phase 1} x_in != mapconstbool(false);

 {

     var {:linear "tid"} tid_out: int;

     var {:linear "1"} x: [int]bool;

     tid_out := tid_in;

     x := x_in;    

 

-    g := 1;

+    yield;

+    call SetG(1);

+    yield;

 }

 

-procedure {:yields} {:stable} C({:linear "tid"} tid_in: int, {:linear "2"} y_in: [int]bool) 

-requires y_in != mapconstbool(false);

+procedure {:yields} {:phase 1} C({:linear "tid"} tid_in: int, {:linear "2"} y_in: [int]bool) 

+requires {:phase 1} y_in != mapconstbool(false);

 {

     var {:linear "tid"} tid_out: int;

     var {:linear "2"} y: [int]bool;

     tid_out := tid_in;

     y := y_in;   

 

-    h := 1;

+    yield;

+    call SetH(1);

+    yield;

 }

diff --git a/Test/og/ticket.bpl b/Test/og/ticket.bpl
index 953230e7..ea08dcb5 100644
--- a/Test/og/ticket.bpl
+++ b/Test/og/ticket.bpl
@@ -6,10 +6,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 {:qed} t: int;

-var {:qed} s: int;

-var {:qed} cs: X;

-var {:qed} T: [int]bool;

+var {:phase 3} t: int;

+var {:phase 3} s: int;

+var {:phase 3} cs: X;

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

 

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

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

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

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

 

-procedure {:yields} {:entrypoint} main({:linear "tid"} xls':[X]bool)

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

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

 {

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

@@ -50,12 +50,15 @@ requires {:phase 3} xls' == mapconstbool(true);
     invariant {:phase 1} Inv1(T, t);

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

     {

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

         call xls, tid := Allocate(xls);

         async call Customer(tid);

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

+

     }

 }

 

-procedure {:yields} {:stable} Customer({:linear "tid"} tid': X)

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

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

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

 requires {:phase 3} true;

@@ -75,12 +78,12 @@ requires {:phase 3} true;
     }

 }

 

-procedure {:yields} Enter({:linear "tid"} tid': X) returns ({:linear "tid"} tid: X)

+procedure {:yields} {:phase 2,3} Enter({:linear "tid"} tid': X) returns ({: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 2} |{ A: tid := tid'; havoc t, T; assume tid != nil && cs == nil; cs := tid; return true; }|;

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

 {

     var m: int;

 

@@ -92,10 +95,10 @@ ensures {:right 2} |{ A: tid := tid'; havoc t, T; assume tid != nil && cs == nil
     par Yield1() | Yield2();

 }

 

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

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

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

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

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

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

 {

     par Yield1();

     tid := tid';

@@ -103,33 +106,31 @@ ensures {:right 1,2} |{ A: tid := tid'; havoc m, t; assume !T[m]; T[m] := true;
     par Yield1();

 }

 

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

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

 {

 }

 

-procedure {:yields} {:stable} Yield2()

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

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

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

-ensures {:both 2} |{ A: return true; }|;

 {

 }

 

-procedure {:yields} {:stable} Yield1()

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

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

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

-ensures {:both 1} |{ A: return true; }|;

 {

 }

 

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

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

+procedure {:yields} {:phase 0,3} Init({:linear "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} GetTicket({:linear "tid"} tid': X) returns ({:linear "tid"} tid: X, m: int);

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

+procedure {:yields} {:phase 0,1} GetTicket({:linear "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} WaitAndEnter({:linear "tid"} tid': X, m:int) returns ({:linear "tid"} tid: X);

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

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

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

 

-procedure {:yields} Leave({:linear "tid"} tid': X) returns ({:linear "tid"} tid: X);

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

+procedure {:yields} {:phase 0,3} Leave({:linear "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; }|;