added introduced and ghost local variables

5 files changed, 220 insertions, 67 deletions

diff --git a/Test/civl/alloc.bpl b/Test/civl/alloc.bpl
new file mode 100644
index 00000000..33535b00
--- /dev/null
+++ b/Test/civl/alloc.bpl
@@ -0,0 +1,158 @@
+// RUN: %boogie -noinfer -useArrayTheory "%s" > "%t"
+// RUN: %diff "%s.expect" "%t"
+function {:builtin "MapConst"} MapConstBool(bool) : [int]bool;
+
+type lmap;
+function {:linear "mem"} dom(lmap): [int]bool;
+function map(lmap): [int]int;
+function cons([int]bool, [int]int) : lmap;
+axiom (forall x: [int]bool, y: [int]int :: {cons(x,y)} dom(cons(x, y)) == x && map(cons(x,y)) == y);
+
+function EmptyLmap(): (lmap);
+axiom (dom(EmptyLmap()) == MapConstBool(false));
+
+function Add(x: lmap, i: int, v: int): (lmap);
+axiom (forall x: lmap, i: int, v: int :: dom(Add(x, i, v)) == dom(x)[i:=true] && map(Add(x, i, v)) == map(x)[i := v]);
+
+function Remove(x: lmap, i: int): (lmap);
+axiom (forall x: lmap, i: int :: dom(Remove(x, i)) == dom(x)[i:=false] && map(Remove(x, i)) == map(x));
+
+procedure {:yields} {:layer 2} Main()
+requires {:layer 1} (forall x: int :: unallocated[x] ==> dom(pool)[x]);
+ensures {:layer 1} (forall x: int :: unallocated[x] ==> dom(pool)[x]);
+{
+   var {:layer 1} {:linear "mem"} l: lmap;
+   var i: int;
+   par Yield() | Dummy();
+   while (*)
+   invariant {:layer 1} (forall x: int :: unallocated[x] ==> dom(pool)[x]);
+   {
+      call  l, i := Alloc();
+      async call Thread(l, i);
+      par Yield() | Dummy();
+   }
+   par Yield() | Dummy();
+}
+
+procedure {:yields} {:layer 2} Thread({:layer 1} {:linear_in "mem"} local_in: lmap, i: int)
+requires {:layer 1} (forall x: int :: unallocated[x] ==> dom(pool)[x]);
+ensures {:layer 1} (forall x: int :: unallocated[x] ==> dom(pool)[x]);
+requires {:layer 1} dom(local_in)[i] && map(local_in)[i] == mem[i];
+requires {:layer 2} dom(local_in)[i];
+{
+    var y, o: int;
+    var {:layer 1} {:linear "mem"} local: lmap;
+    var {:layer 1} {:linear "mem"} l: lmap;
+
+    par YieldMem(local_in, i) | Dummy();
+    call local := Copy(local_in);
+    call local := Write(local, i, 42);
+    call o := Read(local, i);
+    assert {:layer 2} o == 42;
+    while (*)
+    invariant {:layer 1} (forall x: int :: unallocated[x] ==> dom(pool)[x]);
+    {
+        call l, y := Alloc();
+        call l := Write(l, y, 42);
+	call o := Read(l, y);
+	assert {:layer 2} o == 42;
+        call Free(l);
+	par Yield() | Dummy();
+    }
+    par Yield() | Dummy();
+}
+
+procedure {:pure} {:inline 1} Copy({:linear_in "mem"} l: lmap) returns ({:linear "mem"} l': lmap)
+{
+    l' := l;
+}
+
+procedure {:yields} {:layer 1,2} Alloc() returns ({:layer 1} {:linear "mem"} l: lmap, i: int)
+requires {:layer 1} (forall x: int :: unallocated[x] ==> dom(pool)[x]);
+ensures {:layer 1} (forall x: int :: unallocated[x] ==> dom(pool)[x]);
+ensures {:layer 1} dom(l)[i] && map(l)[i] == mem[i];
+ensures {:right} |{ A: assume dom(l)[i]; return true; }|;
+{
+    call Yield();
+    call i := PickAddr();
+    call l := AllocLinear(i);
+    call YieldMem(l, i);
+}
+
+procedure {:yields} {:layer 1,2} Free({:layer 1} {:linear_in "mem"} l: lmap)
+requires {:layer 1} (forall x: int :: unallocated[x] ==> dom(pool)[x]);
+ensures {:layer 1} (forall x: int :: unallocated[x] ==> dom(pool)[x]);
+ensures {:both} |{ A: return true; }|;
+{
+    call Yield();
+}
+
+procedure {:yields} {:layer 1,2} Read({:layer 1} {:linear "mem"} l: lmap, i: int) returns (o: int)
+requires {:layer 1} (forall x: int :: unallocated[x] ==> dom(pool)[x]);
+ensures {:layer 1} (forall x: int :: unallocated[x] ==> dom(pool)[x]);
+requires {:layer 1} dom(l)[i] && map(l)[i] == mem[i];
+ensures {:both} |{ A: assert dom(l)[i]; o := map(l)[i]; return true; }|;
+{
+    call YieldMem(l, i);
+    call o := ReadLow(i);
+    call YieldMem(l, i);
+}
+
+procedure {:yields} {:layer 1,2} Write({:layer 1} {:linear_in "mem"} l: lmap, i: int, o: int) returns ({:layer 1} {:linear "mem"} l': lmap)
+requires {:layer 1} (forall x: int :: unallocated[x] ==> dom(pool)[x]);
+ensures {:layer 1} (forall x: int :: unallocated[x] ==> dom(pool)[x]);
+requires {:layer 1} dom(l)[i] && map(l)[i] == mem[i];
+ensures {:layer 1} dom(l')[i] && map(l')[i] == mem[i];
+ensures {:both} |{ A: assert dom(l)[i]; l' := cons(dom(l), map(l)[i := o]); return true; }|;
+{
+    call YieldMem(l, i);
+    call WriteLow(i, o);
+    call l' := WriteLinear(l, i, o);
+    call YieldMem(l', i);
+}
+
+procedure {:layer 1} AllocLinear(i: int) returns ({:linear "mem"} l: lmap);
+modifies pool;
+requires dom(pool)[i];
+ensures pool == Remove(old(pool), i) && dom(l)[i] && map(l)[i] == mem[i];
+
+procedure {:layer 1} WriteLinear({:layer 1} {:linear_in "mem"} l: lmap, i: int, o: int) returns ({:layer 1} {:linear "mem"} l': lmap);
+requires dom(l)[i];
+ensures l' == cons(dom(l), map(l)[i := o]);
+
+procedure {:yields} {:layer 1} Yield()
+requires {:layer 1} (forall x: int :: unallocated[x] ==> dom(pool)[x]);
+ensures {:layer 1} (forall x: int :: unallocated[x] ==> dom(pool)[x]);
+{
+    yield;
+    assert {:layer 1} (forall x: int :: unallocated[x] ==> dom(pool)[x]);
+}
+
+procedure {:yields} {:layer 1} YieldMem({:layer 1} {:linear "mem"} l: lmap, i: int)
+requires {:layer 1} (forall x: int :: unallocated[x] ==> dom(pool)[x]);
+ensures {:layer 1} (forall x: int :: unallocated[x] ==> dom(pool)[x]);
+requires {:layer 1} dom(l)[i] && map(l)[i] == mem[i];
+ensures {:layer 1} dom(l)[i] && map(l)[i] == mem[i];
+{
+    yield;
+    assert {:layer 1} (forall x: int :: unallocated[x] ==> dom(pool)[x]);
+    assert {:layer 1} dom(l)[i] && map(l)[i] == mem[i];
+}
+
+procedure {:yields} {:layer 2} Dummy()
+{
+    yield;
+}
+
+var {:layer 1, 1} pool: lmap;
+var {:layer 0, 1} mem:[int]int;
+var {:layer 0, 1} unallocated:[int]bool;
+
+procedure {:yields} {:layer 0, 1} ReadLow(i: int) returns (o: int);
+ensures {:atomic} |{ A: o := mem[i]; return true; }|;
+
+procedure {:yields} {:layer 0, 1} WriteLow(i: int, o: int);
+ensures {:atomic} |{ A: mem[i] := o; return true; }|;
+
+procedure {:yields} {:layer 0, 1} PickAddr() returns (i: int);
+ensures {:atomic} |{ A: assume unallocated[i]; unallocated[i] := false; return true; }|;
\ No newline at end of file
diff --git a/Test/civl/alloc.bpl.expect b/Test/civl/alloc.bpl.expect
new file mode 100644
index 00000000..f08c6e00
--- /dev/null
+++ b/Test/civl/alloc.bpl.expect
@@ -0,0 +1,2 @@
+
+Boogie program verifier finished with 12 verified, 0 errors
diff --git a/Test/civl/ghost.bpl b/Test/civl/ghost.bpl
index 74d16acf..1468fa56 100644
--- a/Test/civl/ghost.bpl
+++ b/Test/civl/ghost.bpl
@@ -5,7 +5,7 @@ var {:layer 0} x: int;
 procedure {:yields} {:layer 0,1} Incr();
 ensures {:right} |{ A: x := x + 1; return true; }|;
 
-procedure ghost(y: int) returns (z: int)
+procedure {:pure} ghost(y: int) returns (z: int)
 requires y == 1;
 ensures z == 2;
 {
@@ -15,8 +15,7 @@ ensures z == 2;
 procedure {:yields} {:layer 1,2} Incr2() 
 ensures {:right} |{ A: x := x + 2; return true; }|;
 {
-  var {:ghost} a: int;
-  var {:ghost} b: int;
+  var {:layer 1} a: int;
 
   yield;
   call a := ghost(1);
@@ -25,7 +24,7 @@ ensures {:right} |{ A: x := x + 2; return true; }|;
   yield;
 }
 
-procedure ghost_0() returns (z: int)
+procedure {:layer 1} ghost_0() returns (z: int)
 ensures z == x;
 {
   z := x;
@@ -34,8 +33,8 @@ ensures z == x;
 procedure {:yields} {:layer 1,2} Incr2_0() 
 ensures {:right} |{ A: x := x + 2; return true; }|;
 {
-  var {:ghost} a: int;
-  var {:ghost} b: int;
+  var {:layer 1} a: int;
+  var {:layer 1} b: int;
 
   yield;
   call a := ghost_0();
diff --git a/Test/civl/lock-introduced.bpl b/Test/civl/lock-introduced.bpl
index fa0a3977..5403e5d4 100644
--- a/Test/civl/lock-introduced.bpl
+++ b/Test/civl/lock-introduced.bpl
@@ -67,6 +67,9 @@ ensures {:atomic} |{ A: assume !b; b := true; lock := tid; return true; }|;
     yield;
     L: 
         call status := CAS(false, true);
+        if (status) {
+	    call SetLock(tid);
+	}
 	yield;
         goto A, B;
 
@@ -85,9 +88,16 @@ ensures {:atomic} |{ A: b := false; lock := nil; return true; }|;
 {
     yield;
     call SET(false);
+    call SetLock(nil);
     yield;
 }
 
+procedure {:layer 1} {:inline 1} SetLock(v: X)
+modifies lock;
+{
+    lock := v;
+}
+
 procedure {:yields} {:layer 0,1} CAS(prev: bool, next: bool) returns (status: bool);
 ensures {:atomic} |{ 
 A: goto B, C; 
diff --git a/Test/civl/wsq.bpl b/Test/civl/wsq.bpl
index 17f53401..39dad919 100644
--- a/Test/civl/wsq.bpl
+++ b/Test/civl/wsq.bpl
@@ -89,13 +89,11 @@ ensures {:layer 3} {:expand} emptyInv(put_in_cs, take_in_cs, items,status,T);
 ensures {:atomic} |{ var i: int; A: assume status[i] == NOT_IN_Q; status[i] := IN_Q; return true; }|;
 {
    var t: int;
-   var {:ghost} oldH:int;
-   var {:ghost} oldT:int;
-   var {:ghost} oldStatusT:bool;
+   var {:ghost} {:layer 3} oldH:int;
+   var {:ghost} {:layer 3} oldT:int;
+   var {:ghost} {:layer 3} oldStatusT:bool;
    
-
-   oldH := H;
-   oldT := T;
+   call oldH, oldT := GhostRead();
    yield;
    assert {:layer 3} {:expand} queueInv(steal_in_cs,put_in_cs,take_in_cs,items, status, H, T-1) && tid == ptTid && !take_in_cs && !put_in_cs;
    assert {:layer 3} {:expand} {:expand} ideasInv(put_in_cs,items, status, H, T, take_in_cs, steal_in_cs, h_ss, t_ss);
@@ -104,8 +102,7 @@ ensures {:atomic} |{ var i: int; A: assume status[i] == NOT_IN_Q; status[i] := I
 
    call t := readT_put(tid);
 
-   oldH := H;
-   oldT := T;
+   call oldH, oldT := GhostRead();
    yield;
    assert {:layer 3} {:expand} queueInv(steal_in_cs,put_in_cs,take_in_cs,items, status, H, T-1) && tid == ptTid && !take_in_cs && put_in_cs;
    assert {:layer 3} {:expand} ideasInv(put_in_cs,items, status, H, T, take_in_cs, steal_in_cs, h_ss, t_ss);
@@ -115,9 +112,8 @@ ensures {:atomic} |{ var i: int; A: assume status[i] == NOT_IN_Q; status[i] := I
    
    call writeItems_put(tid,t, task);
 
-   oldH := H;
-   oldT := T;
-   oldStatusT := status[T];
+   call oldH, oldT := GhostRead();
+   call oldStatusT := GhostReadStatus();
    yield;
    assert {:layer 3} {:expand} queueInv(steal_in_cs,put_in_cs,take_in_cs,items, status, H, T) && t == T && tid == ptTid && !take_in_cs && put_in_cs;
    assert {:layer 3} {:expand} ideasInv(put_in_cs,items, status, H, T, take_in_cs, steal_in_cs, h_ss, t_ss);
@@ -128,8 +124,7 @@ ensures {:atomic} |{ var i: int; A: assume status[i] == NOT_IN_Q; status[i] := I
    
    call writeT_put(tid, t+1);
 
-   oldH := H;
-   oldT := T;
+   call oldH, oldT := GhostRead();
    yield;
    assert {:layer 3} {:expand} queueInv(steal_in_cs,put_in_cs,take_in_cs,items, status, H, T-1) && tid == ptTid && !take_in_cs && !put_in_cs;
    assert {:layer 3} {:expand} ideasInv(put_in_cs,items, status, H, T, take_in_cs, steal_in_cs, h_ss, t_ss);
@@ -147,11 +142,10 @@ ensures {:atomic} |{ var i: int; A: goto B,C; B: assume status[i] == IN_Q; statu
 {
    var h, t: int;
    var chk: bool;
-   var {:ghost} oldH:int;
-   var {:ghost} oldT:int;
+   var {:ghost} {:layer 3} oldH:int;
+   var {:ghost} {:layer 3} oldT:int;
 
-   oldH := H;
-   oldT := T;
+   call oldH, oldT := GhostRead();
    yield;
    assert {:layer 3} queueInv(steal_in_cs,put_in_cs,take_in_cs,items, status, H, T-1) && tid == ptTid && !take_in_cs && !put_in_cs;
    assert {:layer 3} ideasInv(put_in_cs,items, status, H, T, take_in_cs, steal_in_cs, h_ss, t_ss);
@@ -164,8 +158,7 @@ ensures {:atomic} |{ var i: int; A: goto B,C; B: assume status[i] == IN_Q; statu
    invariant {:layer 3} ideasInv(put_in_cs,items, status, H, T, take_in_cs, steal_in_cs, h_ss, t_ss);    
    {
 
-       oldH := H;
-       oldT := T;
+       call oldH, oldT := GhostRead();
        yield;
        assert {:layer 3} queueInv(steal_in_cs,put_in_cs,take_in_cs,items, status, H, T-1) && tid == ptTid && !take_in_cs && !put_in_cs;
     assert {:layer 3} ideasInv(put_in_cs,items, status, H, T, take_in_cs, steal_in_cs, h_ss, t_ss);
@@ -173,8 +166,7 @@ ensures {:atomic} |{ var i: int; A: goto B,C; B: assume status[i] == IN_Q; statu
     
        call t := readT_take_init(tid);
 
-       oldH := H;
-       oldT := T;
+       call oldH, oldT := GhostRead();
        yield;
        assert {:layer 3} queueInv(steal_in_cs,put_in_cs,take_in_cs,items, status, H, T-1) && tid == ptTid && !take_in_cs && !put_in_cs;
        assert {:layer 3} ideasInv(put_in_cs,items, status, H, T, take_in_cs, steal_in_cs, h_ss, t_ss);    
@@ -185,8 +177,7 @@ ensures {:atomic} |{ var i: int; A: goto B,C; B: assume status[i] == IN_Q; statu
        t := t-1;
        call writeT_take(tid, t);
 
-       oldH := H;
-       oldT := T;
+       call oldH, oldT := GhostRead();
        yield;
        assert {:layer 3} queueInv(steal_in_cs,put_in_cs,take_in_cs,items, status, H, T) && tid == ptTid && !take_in_cs && !put_in_cs && t_ss[tid] == t;
        assert {:layer 3} ideasInv(put_in_cs,items, status, H, T, take_in_cs, steal_in_cs, h_ss, t_ss);    
@@ -196,8 +187,7 @@ ensures {:atomic} |{ var i: int; A: goto B,C; B: assume status[i] == IN_Q; statu
     
        call h := readH_take(tid);
 
-       oldH := H;
-       oldT := T;
+       call oldH, oldT := GhostRead();
        yield;
        assert {:layer 3} queueInv(steal_in_cs,put_in_cs,take_in_cs,items, status, H, T) && tid == ptTid && take_in_cs  && !put_in_cs && h_ss[tid] == h && t_ss[tid] == t;  
        assert {:layer 3} {:expand} ideasInv(put_in_cs,items, status, H, T, take_in_cs, steal_in_cs, h_ss, t_ss);    
@@ -214,8 +204,7 @@ ensures {:atomic} |{ var i: int; A: goto B,C; B: assume status[i] == IN_Q; statu
            call writeT_take_abort(tid, h);
            task := EMPTY;
  
-           oldH := H;
-           oldT := T;
+           call oldH, oldT := GhostRead();
            yield;
         assert {:layer 3} h <= H;
            assert {:layer 3} queueInv(steal_in_cs,put_in_cs,take_in_cs,items, status, H, T-1) && tid == ptTid && !take_in_cs && !put_in_cs; 
@@ -227,8 +216,7 @@ ensures {:atomic} |{ var i: int; A: goto B,C; B: assume status[i] == IN_Q; statu
 
        call task, taskstatus := readItems(tid, t);
 
-       oldH := H;
-       oldT := T;
+       call oldH, oldT := GhostRead();
        yield;
     assert {:layer 3} H >= h;
        assert {:layer 3} queueInv(steal_in_cs,put_in_cs,take_in_cs,items, status, H, T) && tid == ptTid && take_in_cs && h_ss[tid] == h && t_ss[tid] == t;  
@@ -240,8 +228,7 @@ ensures {:atomic} |{ var i: int; A: goto B,C; B: assume status[i] == IN_Q; statu
        if(t>h) {
         call takeExitCS(tid);
 
-           oldH := H;
-           oldT := T;    
+           call oldH, oldT := GhostRead();    
            yield;
            assert {:layer 3} queueInv(steal_in_cs,put_in_cs,take_in_cs,items, status, H, T-1) && tid == ptTid && !take_in_cs && h_ss[tid] == h && t_ss[tid] == t;  
         assert {:layer 3} ideasInv(put_in_cs,items, status, H, T, take_in_cs, steal_in_cs, h_ss, t_ss);
@@ -250,8 +237,7 @@ ensures {:atomic} |{ var i: int; A: goto B,C; B: assume status[i] == IN_Q; statu
            return;
        }
 	   call writeT_take_eq(tid, h+1);
-	   oldH := H;
-       oldT := T;
+	   call oldH, oldT := GhostRead();
 	   
 	   yield;
 	   assert {:layer 3} queueInv(steal_in_cs,put_in_cs,take_in_cs,items, status, H, T-1) && tid == ptTid && h_ss[tid] == h && t_ss[tid] == t;
@@ -265,8 +251,7 @@ ensures {:atomic} |{ var i: int; A: goto B,C; B: assume status[i] == IN_Q; statu
        call chk := CAS_H_take(tid, h,h+1);
 
 
-       oldH := H;
-       oldT := T;    
+       call oldH, oldT := GhostRead();    
        yield;
 	assert {:layer 3} chk ==> (h+1 == oldH && h_ss[tid] == oldH -1 && task != EMPTY);
        assert {:layer 3} queueInv(steal_in_cs,put_in_cs,take_in_cs,items, status, H, T-1) && tid == ptTid && h_ss[tid] == h && t_ss[tid] == t;  
@@ -279,8 +264,7 @@ ensures {:atomic} |{ var i: int; A: goto B,C; B: assume status[i] == IN_Q; statu
 
        if(!chk) {
     
-          oldH := H;
-          oldT := T;    
+          call oldH, oldT := GhostRead();    
           yield;
           assert {:layer 3} queueInv(steal_in_cs,put_in_cs,take_in_cs,items, status, H, T-1) && tid == ptTid && h_ss[tid] == h && t_ss[tid] == t;  
          assert {:layer 3} ideasInv(put_in_cs,items, status, H, T, take_in_cs, steal_in_cs, h_ss, t_ss);
@@ -290,8 +274,7 @@ ensures {:atomic} |{ var i: int; A: goto B,C; B: assume status[i] == IN_Q; statu
           goto LOOP_ENTRY_1;
        }
 
-       oldH := H;
-       oldT := T;    
+       call oldH, oldT := GhostRead();    
        yield;
        assert {:layer 3} queueInv(steal_in_cs,put_in_cs,take_in_cs,items, status, H, T-1) && tid == ptTid && h_ss[tid] == h && t_ss[tid] == t;  
     assert {:layer 3} ideasInv(put_in_cs,items, status, H, T, take_in_cs, steal_in_cs, h_ss, t_ss);
@@ -301,8 +284,7 @@ ensures {:atomic} |{ var i: int; A: goto B,C; B: assume status[i] == IN_Q; statu
        return;
    }
    
-   oldH := H;
-   oldT := T;
+   call oldH, oldT := GhostRead();
    yield;
    assert {:layer 3} queueInv(steal_in_cs,put_in_cs,take_in_cs,items, status, H, T) && tid == ptTid && !put_in_cs;
    assert {:layer 3} ideasInv(put_in_cs,items, status, H, T, take_in_cs, steal_in_cs, h_ss, t_ss);
@@ -322,11 +304,10 @@ ensures {:atomic} |{ var i: int; A: goto B,C; B: assume status[i] == IN_Q; statu
 {
    var h, t: int;
    var chk: bool;
-   var {:ghost} oldH:int;
-   var {:ghost} oldT:int;
+   var {:ghost} {:layer 3} oldH:int;
+   var {:ghost} {:layer 3} oldT:int;
 
-   oldH := H;
-   oldT := T;
+   call oldH, oldT := GhostRead();
    yield;
    assert {:layer 3} stealerTid(tid);
    assert {:layer 3} queueInv(steal_in_cs,put_in_cs,take_in_cs,items, status, H, T-1);
@@ -341,8 +322,7 @@ ensures {:atomic} |{ var i: int; A: goto B,C; B: assume status[i] == IN_Q; statu
    invariant {:layer 3} ideasInv(put_in_cs,items, status, H, T, take_in_cs, steal_in_cs, h_ss, t_ss);
    invariant {:layer 3} !steal_in_cs[tid];
    {
-       oldH := H;
-       oldT := T;
+       call oldH, oldT := GhostRead();
        yield;
     assert {:layer 3} stealerTid(tid);
        assert {:layer 3} queueInv(steal_in_cs,put_in_cs,take_in_cs,items, status, H, T-1);
@@ -352,8 +332,7 @@ ensures {:atomic} |{ var i: int; A: goto B,C; B: assume status[i] == IN_Q; statu
     
        call h := readH_steal(tid);
 
-       oldH := H;
-       oldT := T;
+       call oldH, oldT := GhostRead();
        yield;
     assert {:layer 3} H >= h;
     assert {:layer 3} !steal_in_cs[tid];
@@ -365,8 +344,7 @@ ensures {:atomic} |{ var i: int; A: goto B,C; B: assume status[i] == IN_Q; statu
        call t := readT_steal(tid);
 
 
-       oldH := H;
-       oldT := T;
+       call oldH, oldT := GhostRead();
        yield;
     assert {:layer 3} steal_in_cs[tid];
     assert {:layer 3} stealerTid(tid) && H >= h && steal_in_cs[tid] && h_ss[tid] == h;
@@ -381,8 +359,7 @@ ensures {:atomic} |{ var i: int; A: goto B,C; B: assume status[i] == IN_Q; statu
            task := EMPTY;
         call stealExitCS(tid);
 
-           oldH := H;
-           oldT := T;
+        call oldH, oldT := GhostRead();
            yield;
         assert {:layer 3} !steal_in_cs[tid];
         assert {:layer 3} stealerTid(tid) && !steal_in_cs[tid] && h_ss[tid] == h;
@@ -395,8 +372,7 @@ ensures {:atomic} |{ var i: int; A: goto B,C; B: assume status[i] == IN_Q; statu
        call task, taskstatus := readItems(tid, h);
 
 
-       oldH := H;
-       oldT := T;
+    call oldH, oldT := GhostRead();
        yield;
     assert {:layer 3} stealerTid(tid) && steal_in_cs[tid] && h_ss[tid] == h;
        assert {:layer 3} queueInv(steal_in_cs,put_in_cs,take_in_cs,items, status, H, T-1);
@@ -408,8 +384,7 @@ ensures {:atomic} |{ var i: int; A: goto B,C; B: assume status[i] == IN_Q; statu
 
        call chk := CAS_H_steal(tid, h,h+1);
 
-       oldH := H;
-       oldT := T;
+       call oldH, oldT := GhostRead();
        yield;
     assert {:layer 3} h_ss[tid] == h;
     assert {:layer 3} chk ==> (h+1 == oldH && h_ss[tid] == h && task != EMPTY && taskstatus == IN_Q);
@@ -423,8 +398,7 @@ ensures {:atomic} |{ var i: int; A: goto B,C; B: assume status[i] == IN_Q; statu
           goto LOOP_ENTRY_2;
        }
 
-       oldH := H;
-       oldT := T;
+       call oldH, oldT := GhostRead();
        yield;
     assert {:layer 3} stealerTid(tid) && !steal_in_cs[tid];
        assert {:layer 3} queueInv(steal_in_cs,put_in_cs,take_in_cs,items, status, H, T-1);
@@ -433,14 +407,24 @@ ensures {:atomic} |{ var i: int; A: goto B,C; B: assume status[i] == IN_Q; statu
        return;
    }
    
-   oldH := H;
-   oldT := T;
+   call oldH, oldT := GhostRead();
    yield;
    assert {:layer 3} chk && task != EMPTY;
    assert {:layer 3} stealerTid(tid) && !steal_in_cs[tid];
    assert {:layer 3} oldH <= H;
 }
 
+procedure {:layer 3} {:inline 1} GhostRead() returns (oldH: int, oldT: int)
+{
+   oldH := H;
+   oldT := T;
+}
+
+procedure {:layer 3} {:inline 1} GhostReadStatus() returns (oldStatus: bool)
+{
+   oldStatus := status[T];
+}
+
 procedure {:yields}{:layer 0,3} readH_take({:linear "tid"} tid:Tid) returns (y: int);
 ensures {:atomic} |{A:  assert tid == ptTid;
                        y := H;