diff options
Diffstat (limited to 'Test/civl/DeviceCache.bpl')
| -rw-r--r-- | Test/civl/DeviceCache.bpl | 210 |
1 files changed, 210 insertions, 0 deletions
diff --git a/Test/civl/DeviceCache.bpl b/Test/civl/DeviceCache.bpl new file mode 100644 index 00000000..f439b607 --- /dev/null +++ b/Test/civl/DeviceCache.bpl @@ -0,0 +1,210 @@ +// RUN: %boogie -noinfer -typeEncoding:m -useArrayTheory "%s" > "%t"
+// RUN: %diff "%s.expect" "%t"
+type X;
+function {:builtin "MapConst"} mapconstbool(bool): [X]bool;
+const nil: X;
+var {:layer 0,1} ghostLock: X;
+var {:layer 0,1} lock: X;
+var {:layer 0,1} currsize: int;
+var {:layer 0,1} newsize: int;
+
+function {:builtin "MapConst"} MapConstBool(bool) : [X]bool;
+function {:inline} {:linear "tid"} TidCollector(x: X) : [X]bool
+{
+ MapConstBool(false)[x := true]
+}
+function {:inline} {:linear "tid"} TidSetCollector(x: [X]bool) : [X]bool
+{
+ x
+}
+
+function {:inline} Inv(ghostLock: X, currsize: int, newsize: int) : (bool)
+{
+ 0 <= currsize && currsize <= newsize &&
+ (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;
+{
+ yield;
+ assert {:layer 1} Inv(ghostLock, currsize, newsize) && old(currsize) <= currsize;
+}
+
+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 {:layer 1} Inv(ghostLock, currsize, newsize) && tid != nil && ghostLock == tid && old(currsize) == currsize && old(newsize) == newsize;
+}
+
+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);
+{
+ var {:linear "tid"} tid: X;
+
+ yield;
+
+ call Init(xls);
+
+ yield;
+ assert {:layer 1} Inv(ghostLock, currsize, newsize);
+
+ while (*)
+ invariant {:layer 1} Inv(ghostLock, currsize, newsize);
+ {
+ par tid := Allocate() | Yield();
+ yield;
+ assert {:layer 1} Inv(ghostLock, currsize, newsize);
+ async call Thread(tid);
+ yield;
+ assert {:layer 1} Inv(ghostLock, currsize, newsize);
+ }
+ yield;
+}
+
+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;
+
+ havoc start, size;
+ assume (0 <= start && 0 <= size);
+ call bytesRead := Read(tid, start, 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;
+
+ par YieldToReadCache(tid);
+ bytesRead := size;
+ call acquire(tid);
+ call i := ReadCurrsize(tid);
+ call tmp := ReadNewsize(tid);
+ if (start + size <= i) {
+ call release(tid);
+ goto COPY_TO_BUFFER;
+ } else if (tmp > i) {
+ bytesRead := if (start <= i) then (i - start) else 0;
+ call release(tid);
+ goto COPY_TO_BUFFER;
+ } else {
+ call WriteNewsize(tid, start + size);
+ call release(tid);
+ goto READ_DEVICE;
+ }
+
+READ_DEVICE:
+ 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 YieldToReadCache(tid);
+ call ReadCache(tid, start, bytesRead);
+}
+
+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 {: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);
+ j := j + 1;
+ }
+ par YieldToWriteCache(tid);
+}
+
+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;
+
+ par YieldToReadCache(tid);
+
+ j := 0;
+ while(j < bytesRead)
+ invariant {:layer 1} 0 <= j;
+ invariant {:layer 1} bytesRead == 0 || start + bytesRead <= currsize;
+ invariant {:layer 1} Inv(ghostLock, currsize, newsize);
+ {
+ assert {:layer 1} start + j < currsize;
+ call ReadCacheEntry(tid, start + j);
+ j := j + 1;
+ par YieldToReadCache(tid);
+ }
+
+ par YieldToReadCache(tid);
+}
+
+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);
+ensures {:right} |{A: assert tid != nil; assert lock == tid || ghostLock == tid; val := currsize; return true; }|;
+
+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} {: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} {: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} {:layer 0,1} ReadCacheEntry({:linear "tid"} tid: X, index: int);
+ensures {:atomic} |{ A: assert 0 <= index && index < currsize; return true; }|;
+
+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} {:layer 0,1} acquire({:linear "tid"} tid: X);
+ensures {:right} |{ A: assert tid != nil; assume lock == nil; lock := tid; return true; }|;
+
+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; }|;
|