summaryrefslogtreecommitdiff
path: root/Test/og/DeviceCache.bpl
diff options
context:
space:
mode:
Diffstat (limited to 'Test/og/DeviceCache.bpl')
-rw-r--r--Test/og/DeviceCache.bpl28
1 files changed, 21 insertions, 7 deletions
diff --git a/Test/og/DeviceCache.bpl b/Test/og/DeviceCache.bpl
index 703456ef..f439b607 100644
--- a/Test/og/DeviceCache.bpl
+++ b/Test/og/DeviceCache.bpl
@@ -24,6 +24,14 @@ function {:inline} Inv(ghostLock: X, currsize: int, newsize: int) : (bool)
(ghostLock == nil <==> currsize == newsize)
}
+procedure {:yields} {:layer 1} Yield()
+requires {:layer 1} Inv(ghostLock, currsize, newsize);
+ensures {:layer 1} Inv(ghostLock, currsize, newsize);
+{
+ yield;
+ assert {:layer 1} Inv(ghostLock, currsize, newsize);
+}
+
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;
@@ -40,18 +48,21 @@ ensures {:layer 1} Inv(ghostLock, currsize, newsize) && ghostLock == tid && old(
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);
+procedure {:yields} {:layer 1} Allocate() returns ({:linear "tid"} xl: X)
ensures {:layer 1} xl != nil;
+{
+ yield;
+ call xl := AllocateLow();
+ yield;
+}
-procedure {:yields} {:layer 1} main({:linear_in "tid"} xls':[X]bool)
-requires {:layer 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;
yield;
- xls := xls';
call Init(xls);
yield;
@@ -60,7 +71,7 @@ requires {:layer 1} xls' == mapconstbool(true);
while (*)
invariant {:layer 1} Inv(ghostLock, currsize, newsize);
{
- call xls, tid := Allocate(xls);
+ par tid := Allocate() | Yield();
yield;
assert {:layer 1} Inv(ghostLock, currsize, newsize);
async call Thread(tid);
@@ -168,7 +179,7 @@ ensures {:layer 1} Inv(ghostLock, currsize, newsize);
par YieldToReadCache(tid);
}
-procedure {:yields} {:layer 0,1} Init({:linear "tid"} xls:[X]bool);
+procedure {:yields} {:layer 0,1} Init({:linear_in "tid"} xls:[X]bool);
ensures {:atomic} |{ A: assert xls == mapconstbool(true); currsize := 0; newsize := 0; lock := nil; ghostLock := nil; return true; }|;
procedure {:yields} {:layer 0,1} ReadCurrsize({:linear "tid"} tid: X) returns (val: int);
@@ -194,3 +205,6 @@ ensures {:right} |{ A: assert tid != nil; assume lock == nil; lock := tid; retur
procedure {:yields} {:layer 0,1} release({:linear "tid"} tid: X);
ensures {:left} |{ A: assert tid != nil; assert lock == tid; lock := nil; return true; }|;
+
+procedure {:yields} {:layer 0,1} AllocateLow() returns ({:linear "tid"} tid: X);
+ensures {:atomic} |{ A: assume tid != nil; return true; }|;