second checkpoint

1 files changed, 67 insertions, 71 deletions

diff --git a/Test/og/DeviceCache.bpl b/Test/og/DeviceCache.bpl
index 0f6383ef..23f36ae5 100644
--- a/Test/og/DeviceCache.bpl
+++ b/Test/og/DeviceCache.bpl
@@ -22,18 +22,20 @@ function {:inline} Inv(ghostLock: X, currsize: int, newsize: int) : (bool)
     (ghostLock == nil <==> currsize == newsize)

 }

 

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

+procedure {:yields} {:phase 1} YieldToReadCache({:cnst "tid"} tid: X)

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

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

 {

-   tid := tid';

+   yield;

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

 }

 

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

+procedure {:yields} {:phase 1} YieldToWriteCache({:cnst "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;

 {

-    tid := tid';

+    yield;

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

 }

 

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

@@ -47,7 +49,8 @@ requires {:phase 1} xls' == mapconstbool(true);
 

     yield;

 

-    call xls := Init(xls');

+    xls := xls';

+    call Init(xls);

     

     yield;

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

@@ -64,134 +67,127 @@ requires {:phase 1} xls' == mapconstbool(true);
     }

 }

 

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

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

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

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

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

 {

     var start, size, bytesRead: int;

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

 

-    tid := tid';

     havoc start, size;

     assume (0 <= start && 0 <= size);

     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;

+procedure {:yields} {:phase 1} Read({:cnst "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;

 {

     var i, tmp: int;

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

-    tid := tid';

 

-    par  tid := YieldToReadCache(tid);

+    par YieldToReadCache(tid);

     bytesRead := size;

-    call tid := acquire(tid);

-    call tid, i := ReadCurrsize(tid);

-    call tid, tmp := ReadNewsize(tid);

+    call acquire(tid);

+    call i := ReadCurrsize(tid);

+    call tmp := ReadNewsize(tid);

     if (start + size <= i) {

-        call tid := release(tid); 

+        call release(tid); 

     	goto COPY_TO_BUFFER;

     } else if (tmp > i) {

         bytesRead := if (start <= i) then (i - start) else 0;

-    	call tid := release(tid); 

+    	call release(tid); 

 	goto COPY_TO_BUFFER;

     } else {

-        call tid := WriteNewsize(tid, start + size);

-    	call tid := release(tid); 

+        call WriteNewsize(tid, start + size);

+    	call release(tid); 

 	goto READ_DEVICE;

     }

 

 READ_DEVICE:

-    par  tid := YieldToWriteCache(tid);

-    call tid := WriteCache(tid, start + size);

-    par  tid := YieldToWriteCache(tid);

-    call tid := acquire(tid);

-    call tid, tmp := ReadNewsize(tid);

-    call tid := WriteCurrsize(tid, tmp);

-    call tid := release(tid);

+    par YieldToWriteCache(tid);

+    call WriteCache(tid, start + size);

+    par YieldToWriteCache(tid);

+    call acquire(tid);

+    call tmp := ReadNewsize(tid);

+    call WriteCurrsize(tid, tmp);

+    call release(tid);

 

 COPY_TO_BUFFER:

-    par tid := YieldToReadCache(tid);

-    call tid := ReadCache(tid, start, bytesRead);

+    par YieldToReadCache(tid);

+    call ReadCache(tid, start, bytesRead);

 }

 

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

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

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

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

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

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

 {

     var j: int;

-    tid := tid';

 

-    par tid := YieldToWriteCache(tid);

-    call tid, j := ReadCurrsize(tid);

+    par YieldToWriteCache(tid);

+    call j := ReadCurrsize(tid);

     while (j < index)

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

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

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

     {

-        par tid := YieldToWriteCache(tid);

-        call tid := WriteCacheEntry(tid, j);

+        par YieldToWriteCache(tid);

+        call WriteCacheEntry(tid, j);

 	j := j + 1;

     }

-    par tid := YieldToWriteCache(tid);

+    par YieldToWriteCache(tid);

 }

 

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

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

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

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

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

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

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

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

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

 {

     var j: int;

-    tid := tid';

 

-    par tid := YieldToReadCache(tid);

+    par YieldToReadCache(tid);

 

     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) && tid == tid';

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

     {

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

-        call tid := ReadCacheEntry(tid, start + j);

+        call ReadCacheEntry(tid, start + j);

         j := j + 1;

-	par tid := YieldToReadCache(tid);

+	par YieldToReadCache(tid);

     }

 

-    par tid := YieldToReadCache(tid);

+    par YieldToReadCache(tid);

 }

 

-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} {:phase 0,1} Init({:cnst "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 ({: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} {:phase 0,1} ReadCurrsize({:cnst "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 ({: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} {:phase 0,1} ReadNewsize({:cnst "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) 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} {:phase 0,1} WriteNewsize({:cnst "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) 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} {:phase 0,1} WriteCurrsize({:cnst "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) returns ({:linear "tid"} tid: X);

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

+procedure {:yields} {:phase 0,1} ReadCacheEntry({:cnst "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) returns ({:linear "tid"} tid: X);

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

+procedure {:yields} {:phase 0,1} WriteCacheEntry({:cnst "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) returns ({:linear "tid"} tid: X);

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

+procedure {:yields} {:phase 0,1} acquire({:cnst "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) returns ({:linear "tid"} tid: X);

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

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

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