renamed :phase to :layer

1 files changed, 53 insertions, 53 deletions

diff --git a/Test/og/DeviceCache.bpl b/Test/og/DeviceCache.bpl
index ad75f1f9..b74b52c5 100644
--- a/Test/og/DeviceCache.bpl
+++ b/Test/og/DeviceCache.bpl
@@ -3,10 +3,10 @@
 type X;

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

 const nil: X;

-var {:phase 1} ghostLock: X;

-var {:phase 1} lock: X;

-var {:phase 1} currsize: int;

-var {:phase 1} newsize: int;

+var {:layer 1} ghostLock: X;

+var {:layer 1} lock: X;

+var {:layer 1} currsize: int;

+var {:layer 1} newsize: int;

 

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

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

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

 }

 

-procedure {:yields} {:phase 1} YieldToReadCache({:linear "tid"} tid: X)

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

-ensures {:phase 1} Inv(ghostLock, currsize, newsize) && old(currsize) <= currsize;

+procedure {:yields} {:layer 1} YieldToReadCache({:linear "tid"} tid: X)

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

+ensures {:layer 1} Inv(ghostLock, currsize, newsize) && old(currsize) <= currsize;

 {

    yield;

-   assert {:phase 1} Inv(ghostLock, currsize, newsize) && old(currsize) <= currsize;

+   assert {:layer 1} Inv(ghostLock, currsize, newsize) && old(currsize) <= currsize;

 }

 

-procedure {:yields} {:phase 1} YieldToWriteCache({:linear "tid"} tid: X)

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

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

+procedure {:yields} {:layer 1} YieldToWriteCache({:linear "tid"} tid: X)

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

+ensures {:layer 1} Inv(ghostLock, currsize, newsize) && ghostLock == tid && old(currsize) == currsize && old(newsize) == newsize;

 {

     yield;

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

+    assert {:layer 1} Inv(ghostLock, currsize, newsize) && tid != nil && ghostLock == tid && old(currsize) == currsize && old(newsize) == newsize;

 }

 

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

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

+ensures {:layer 1} xl != nil;

 

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

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

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

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

 {

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

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

@@ -55,24 +55,24 @@ requires {:phase 1} xls' == mapconstbool(true);
     call Init(xls);

     

     yield;

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

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

 

     while (*)

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

+    invariant {:layer 1} Inv(ghostLock, currsize, newsize);

     {

         call xls, tid := Allocate(xls);

 	yield;

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

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

         async call Thread(tid);

 	yield;

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

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

     }

     yield;

 }

 

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

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

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

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

+requires {:layer 1} tid != nil;

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

 {

     var start, size, bytesRead: int;

 

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

 }

 

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

-ensures {:phase 1} 0 <= bytesRead && bytesRead <= size;

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

+requires {:layer 1} tid != nil;

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

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

+ensures {:layer 1} 0 <= bytesRead && bytesRead <= size;

 {

     var i, tmp: int;

 

@@ -121,19 +121,19 @@ COPY_TO_BUFFER:
     call ReadCache(tid, start, bytesRead);

 }

 

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

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

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

-ensures {:phase 1} ghostLock == tid;

-ensures {:phase 1} Inv(ghostLock, currsize, newsize) && old(currsize) == currsize && old(newsize) == newsize;

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

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

+requires {:layer 1} ghostLock == tid && tid != nil;

+ensures {:layer 1} ghostLock == tid;

+ensures {:layer 1} Inv(ghostLock, currsize, newsize) && old(currsize) == currsize && old(newsize) == newsize;

 {

     var j: int;

 

     par YieldToWriteCache(tid);

     call j := ReadCurrsize(tid);

     while (j < index)

-    invariant {:phase 1} ghostLock == tid && currsize <= j && tid == tid;

-    invariant {:phase 1} Inv(ghostLock, currsize, newsize) && old(currsize) == currsize && old(newsize) == newsize;

+    invariant {:layer 1} ghostLock == tid && currsize <= j && tid == tid;

+    invariant {:layer 1} Inv(ghostLock, currsize, newsize) && old(currsize) == currsize && old(newsize) == newsize;

     {

         par YieldToWriteCache(tid);

         call WriteCacheEntry(tid, j);

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

 }

 

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

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

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

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

-requires {:phase 1} (bytesRead == 0 || start + bytesRead <= currsize);

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

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

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

+requires {:layer 1} tid != nil;

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

+requires {:layer 1} (bytesRead == 0 || start + bytesRead <= currsize);

+ensures {:layer 1} Inv(ghostLock, currsize, newsize);

 {

     var j: int;

 

@@ -155,11 +155,11 @@ ensures {:phase 1} Inv(ghostLock, currsize, newsize);
 

     j := 0;

     while(j < bytesRead)

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

-    invariant {:phase 1} bytesRead == 0 || start + bytesRead <= currsize; 

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

+    invariant {:layer 1} 0 <= j;

+    invariant {:layer 1} bytesRead == 0 || start + bytesRead <= currsize; 

+    invariant {:layer 1} Inv(ghostLock, currsize, newsize);

     {

-	assert {:phase 1} start + j < currsize;

+	assert {:layer 1} start + j < currsize;

         call ReadCacheEntry(tid, start + j);

         j := j + 1;

 	par YieldToReadCache(tid);

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

 }

 

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

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

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

 

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

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

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

 

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

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

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

 

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

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

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

 

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

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

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

 

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

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

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

 

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

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

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

 

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

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

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

 

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

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

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