finished the sample

1 files changed, 37 insertions, 38 deletions

diff --git a/Test/og/DeviceCacheSimplified.bpl b/Test/og/DeviceCacheSimplified.bpl
index 00a02ffa..40a0ab1c 100644
--- a/Test/og/DeviceCacheSimplified.bpl
+++ b/Test/og/DeviceCacheSimplified.bpl
@@ -1,42 +1,40 @@
-function {:inline} Inv1(currsize: int, newsize: int) : (bool)

+function {:inline} Inv(ghostLock: X, currsize: int, newsize: int) : (bool)

 {

-    currsize <= newsize

+    currsize <= newsize && (ghostLock == nil <==> currsize == newsize)

 }

 

-function {:inline} Inv2(ghostLock: X, currsize: int, newsize: int) : (bool)

-{

-    ghostLock == nil <==> currsize == newsize

-}

-

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

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

 requires tid' != nil;

+requires Inv(ghostLock, currsize, newsize);

+ensures Inv(ghostLock, currsize, newsize);

+ensures old(currsize) <= currsize;

 ensures tid == tid';

-requires Inv1(currsize, newsize);

-requires Inv2(ghostLock, currsize, newsize);

-ensures Inv1(currsize, newsize);

-ensures Inv2(ghostLock, currsize, newsize);

 {

     assume tid == tid';

-    assert {:yield} Inv1(currsize, newsize);

-    assert Inv2(ghostLock, currsize, newsize);

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

+    assert old(currsize) <= currsize;

     assert tid != nil;

 }

 

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

+procedure YieldToUpdateCache({:linear "tid"} tid': X, i: int) returns ({:linear "tid"} tid: X)

 requires tid' != nil;

-ensures tid == tid';

-requires Inv1(currsize, newsize);

-requires Inv2(ghostLock, currsize, newsize);

+requires Inv(ghostLock, currsize, newsize);

 requires ghostLock == tid';

-ensures Inv1(currsize, newsize);

-ensures Inv2(ghostLock, currsize, newsize);

+requires currsize <= i;

+ensures Inv(ghostLock, currsize, newsize);

+ensures old(currsize) <= currsize;

+ensures tid == tid';

 ensures ghostLock == tid;

+ensures currsize <= i;

+ensures newsize == old(newsize);

 {

     assume tid == tid';

-    assert {:yield} Inv1(currsize, newsize);

-    assert Inv2(ghostLock, currsize, newsize);

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

+    assert old(currsize) <= currsize;

     assert tid != nil;

     assert ghostLock == tid;

+    assert currsize <= i;

+    assert newsize == old(newsize);

 }

 

 var ghostLock: X;

@@ -57,11 +55,10 @@ ensures lock == nil;
 procedure Read ({:linear "tid"} tid': X, start : int, size : int) returns (bytesread : int)

 requires tid' != nil;

 requires 0 <= start && 0 <= size;

-requires Inv1(currsize, newsize);

-requires Inv2(ghostLock, currsize, newsize);

+requires Inv(ghostLock, currsize, newsize);

 ensures 0 <= bytesread && bytesread <= size;

 {

-    var copyGhostLock: X;

+    var copy_currsize: int;

     var i, j, tmp : int;

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

     assume tid == tid';

@@ -71,30 +68,31 @@ ensures 0 <= bytesread && bytesread <= size;
     i := currsize;

     if (start + size <= i) {

         call release(tid); 

-	call tid := Yield(tid);

+	call tid := YieldToReadCache(tid);

 	goto COPY_TO_BUFFER;

     } else if (newsize > i) {

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

 	call release(tid); 

-	call tid := Yield(tid);

+	call tid := YieldToReadCache(tid);

 	goto COPY_TO_BUFFER;

     } else {

         newsize := start + size;

 	ghostLock := tid;

 	call release(tid); 

-	call tid := YieldWithGhostLock(tid);

+	call tid := YieldToUpdateCache(tid, i);

 	goto READ_DEVICE;

     }

 

 READ_DEVICE:

     while (i < start + size) 

-    invariant Inv1(currsize, newsize);

-    invariant Inv2(ghostLock, currsize, newsize); 

+    invariant Inv(ghostLock, currsize, newsize); 

     invariant ghostLock == tid;

     invariant tid != nil;

+    invariant currsize <= i;

+    invariant newsize == start + size;

     {

-        assert ghostLock == tid;

-        call tid := YieldWithGhostLock(tid);

+        call tid := YieldToUpdateCache(tid, i);

+	assert currsize <= i;

 	i := i + 1;

     }

     call acquire(tid);

@@ -102,24 +100,25 @@ READ_DEVICE:
     currsize := tmp;

     ghostLock := nil;

     call release(tid);

-    call tid := Yield(tid);

+    call tid := YieldToReadCache(tid);

 

 COPY_TO_BUFFER:

     j := 0;

     while(j < bytesread) 

-    invariant Inv1(currsize, newsize);

-    invariant Inv2(ghostLock, currsize, newsize); 

+    invariant 0 <= j;

+    invariant Inv(ghostLock, currsize, newsize); 

     invariant tid != nil;

+    invariant bytesread == 0 || start + bytesread <= currsize;

     {

-        call tid := Yield(tid);

+        call tid := YieldToReadCache(tid);

+	assert start + j < currsize;

         j := j + 1;

     }

 }

 

 procedure thread({:linear "tid"} tid': X)

 requires tid' != nil;

-requires Inv1(currsize, newsize);

-requires Inv2(ghostLock, currsize, newsize);

+requires Inv(ghostLock, currsize, newsize);

 {

     var start, size, bytesread: int;

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