diff options
| author |  Unknown <qadeer@FAIZ-AHMED-FAIZ.redmond.corp.microsoft.com> | 2013-02-05 10:22:50 -0800 |
|---|---|---|
| committer | Unknown <qadeer@FAIZ-AHMED-FAIZ.redmond.corp.microsoft.com> | 2013-02-05 10:22:50 -0800 |
| commit | 56ea854550a4da87d5289932e305cedaf1b1b2cb (patch) | |
| tree | c0570721342f91d53c49bd288b69e9e3ecbbe73c /Test/og | |
| parent | 0ad7d270e9a989919d9291a86a018fe55349022b (diff) | |
Further bug fixes in OG
Added another sample
Diffstat (limited to 'Test/og')
| -rw-r--r-- | Test/og/DeviceCacheSimplified.bpl | 144 | ||||
| -rw-r--r-- | Test/og/runtest.bat | 2 |
2 files changed, 145 insertions, 1 deletions
diff --git a/Test/og/DeviceCacheSimplified.bpl b/Test/og/DeviceCacheSimplified.bpl new file mode 100644 index 00000000..00a02ffa --- /dev/null +++ b/Test/og/DeviceCacheSimplified.bpl @@ -0,0 +1,144 @@ +function {:inline} Inv1(currsize: int, newsize: int) : (bool)
+{
+ 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)
+requires tid' != nil;
+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 tid != nil;
+}
+
+procedure YieldWithGhostLock({:linear "tid"} tid': X) returns ({:linear "tid"} tid: X)
+requires tid' != nil;
+ensures tid == tid';
+requires Inv1(currsize, newsize);
+requires Inv2(ghostLock, currsize, newsize);
+requires ghostLock == tid';
+ensures Inv1(currsize, newsize);
+ensures Inv2(ghostLock, currsize, newsize);
+ensures ghostLock == tid;
+{
+ assume tid == tid';
+ assert {:yield} Inv1(currsize, newsize);
+ assert Inv2(ghostLock, currsize, newsize);
+ assert tid != nil;
+ assert ghostLock == tid;
+}
+
+var ghostLock: X;
+var lock: X;
+const nil: X;
+var currsize: int;
+var newsize: int;
+
+procedure acquire(tid: X);
+modifies lock;
+ensures old(lock) == nil && lock == tid;
+
+procedure release(tid: X);
+modifies lock;
+requires lock == tid;
+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);
+ensures 0 <= bytesread && bytesread <= size;
+{
+ var copyGhostLock: X;
+ var i, j, tmp : int;
+ var {:linear "tid"} tid: X;
+ assume tid == tid';
+
+ bytesread := size;
+ call acquire(tid);
+ i := currsize;
+ if (start + size <= i) {
+ call release(tid);
+ call tid := Yield(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);
+ goto COPY_TO_BUFFER;
+ } else {
+ newsize := start + size;
+ ghostLock := tid;
+ call release(tid);
+ call tid := YieldWithGhostLock(tid);
+ goto READ_DEVICE;
+ }
+
+READ_DEVICE:
+ while (i < start + size)
+ invariant Inv1(currsize, newsize);
+ invariant Inv2(ghostLock, currsize, newsize);
+ invariant ghostLock == tid;
+ invariant tid != nil;
+ {
+ assert ghostLock == tid;
+ call tid := YieldWithGhostLock(tid);
+ i := i + 1;
+ }
+ call acquire(tid);
+ tmp := newsize;
+ currsize := tmp;
+ ghostLock := nil;
+ call release(tid);
+ call tid := Yield(tid);
+
+COPY_TO_BUFFER:
+ j := 0;
+ while(j < bytesread)
+ invariant Inv1(currsize, newsize);
+ invariant Inv2(ghostLock, currsize, newsize);
+ invariant tid != nil;
+ {
+ call tid := Yield(tid);
+ j := j + 1;
+ }
+}
+
+procedure thread({:linear "tid"} tid': X)
+requires tid' != nil;
+requires Inv1(currsize, newsize);
+requires Inv2(ghostLock, currsize, newsize);
+{
+ var start, size, bytesread: int;
+ var {:linear "tid"} tid: X;
+
+ assume tid == tid';
+ havoc start, size;
+ assume (0 <= start && 0 <= size);
+ call bytesread := Read(tid, start, size);
+}
+
+procedure {:entrypoint} main()
+requires currsize == 0 && newsize == 0 && ghostLock == nil && lock == nil;
+{
+ var {:linear "tid"} tid: X;
+
+ while (*)
+ {
+ havoc tid;
+ assume tid != nil;
+ call {:async} thread(tid);
+ }
+}
\ No newline at end of file diff --git a/Test/og/runtest.bat b/Test/og/runtest.bat index 3ec39f7e..839ac09b 100644 --- a/Test/og/runtest.bat +++ b/Test/og/runtest.bat @@ -9,7 +9,7 @@ for %%f in (foo.bpl bar.bpl) do ( %BGEXE% %* /nologo /noinfer /doModSetAnalysis /OwickiGries:OwickiGriesDesugared.bpl %%f
)
-for %%f in (linear-set.bpl linear-set2.bpl FlanaganQadeer.bpl) do (
+for %%f in (linear-set.bpl linear-set2.bpl FlanaganQadeer.bpl DeviceCacheSimplified.bpl) do (
echo.
echo -------------------- %%f --------------------
%BGEXE% %* /nologo /noinfer /typeEncoding:m /useArrayTheory /doModSetAnalysis /OwickiGries:OwickiGriesDesugared.bpl %%f Maps.bpl
|