summaryrefslogtreecommitdiff
path: root/Test
diff options
context:
space:
mode:
authorGravatar Shaz Qadeer <qadeer@microsoft.com>2016-02-09 21:35:24 -0800
committerGravatar Shaz Qadeer <qadeer@microsoft.com>2016-02-09 21:35:24 -0800
commit5fb565e439255ede7dc3653708af41678b6c1062 (patch)
treea91488b8ad92bc69718f2d5fda1d44082a3959de /Test
parent1e0f2b1ea7e9cbfd1c7923674c0ed4601263d09a (diff)
added an example
Diffstat (limited to 'Test')
-rw-r--r--Test/civl/funky.bpl133
-rw-r--r--Test/civl/funky.bpl.expect2
-rw-r--r--Test/civl/ticket.bpl5
3 files changed, 137 insertions, 3 deletions
diff --git a/Test/civl/funky.bpl b/Test/civl/funky.bpl
new file mode 100644
index 00000000..ad5bf271
--- /dev/null
+++ b/Test/civl/funky.bpl
@@ -0,0 +1,133 @@
+// RUN: %boogie -noinfer -typeEncoding:m -useArrayTheory "%s" > "%t"
+// RUN: %diff "%s.expect" "%t"
+type X;
+const nil: X;
+function {:builtin "MapConst"} MapConstBool(bool) : [X]bool;
+function {:inline} {:linear "tid"} TidCollector(x: X) : [X]bool
+{
+ MapConstBool(false)[x := true]
+}
+
+var {:layer 0, 3} A: X;
+var {:layer 0, 3} B: X;
+var {:layer 0, 3} counter: int;
+
+procedure {:yields} {:layer 0, 3} LockA({:linear "tid"} tid: X);
+ensures {:right} |{ A: assert tid != nil; assume A == nil; A := tid; return true; }|;
+
+procedure {:yields} {:layer 0, 1} IncrA({:linear "tid"} tid: X);
+ensures {:right} |{ A: assert tid != nil && A == tid; counter := counter + 1; return true; }|;
+
+procedure {:yields} {:layer 0, 1} DecrA({:linear "tid"} tid: X);
+ensures {:right} |{ A: assert tid != nil && A == tid; counter := counter - 1; return true; }|;
+
+procedure {:yields} {:layer 0, 3} UnlockA({:linear "tid"} tid: X);
+ensures {:left} |{ A: assert tid != nil && A == tid; A := nil; return true; }|;
+
+procedure {:yields} {:layer 0, 3} LockB({:linear "tid"} tid: X);
+ensures {:right} |{ A: assert tid != nil; assume B == nil; B := tid; return true; }|;
+
+procedure {:yields} {:layer 0, 2} IncrB({:linear "tid"} tid: X);
+ensures {:atomic} |{ A: assert tid != nil && B == tid; counter := counter + 1; return true; }|;
+
+procedure {:yields} {:layer 0, 1} DecrB({:linear "tid"} tid: X);
+ensures {:atomic} |{ A: assert tid != nil && B == tid; counter := counter - 1; return true; }|;
+
+procedure {:yields} {:layer 0, 3} UnlockB({:linear "tid"} tid: X);
+ensures {:left} |{ A: assert tid != nil && B == tid; B := nil; return true; }|;
+
+procedure {:yields} {:layer 0, 3} AssertA({:linear "tid"} tid: X);
+ensures {:atomic} |{ A: assert tid != nil && A == tid; assert counter >= -1; return true; }|;
+
+procedure {:yields} {:layer 0, 3} AssertB({:linear "tid"} tid: X);
+ensures {:atomic} |{ A: assert tid != nil && A == tid && B == tid; assert counter == 0; return true; }|;
+
+procedure {:pure} AllocTid() returns ({:linear "tid"} tid: X);
+ensures tid != nil;
+
+procedure {:yields} {:layer 1, 2} AbsDecrB({:linear "tid"} tid: X)
+ensures {:right} |{ A: assert tid != nil && B == tid && counter == 0; counter := counter - 1; return true; }|;
+{
+ yield;
+ call DecrB(tid);
+ yield;
+}
+
+procedure {:yields} {:layer 2, 3} AbsAssertA({:linear "tid"} tid: X)
+ensures {:both} |{ A: assert tid != nil && A == tid; assert counter >= -1; return true; }|;
+{
+ yield;
+ call AssertA(tid);
+ yield;
+}
+
+procedure {:yields} {:layer 2, 3} AbsAssertB({:linear "tid"} tid: X)
+ensures {:both} |{ A: assert tid != nil && A == tid && B == tid; assert counter == 0; return true; }|;
+{
+ yield;
+ call AssertB(tid);
+ yield;
+}
+
+procedure {:yields} {:layer 1} TA({:linear "tid"} tid: X)
+requires {:layer 1} tid != nil;
+{
+ yield;
+ call LockA(tid);
+ call IncrA(tid);
+ call DecrA(tid);
+ call UnlockA(tid);
+ yield;
+}
+
+procedure {:yields} {:layer 2, 3} TB({:linear "tid"} tid: X)
+ensures {:both} |{ A: assert tid != nil && counter == 0; return true; }|;
+{
+ yield;
+ call LockB(tid);
+ call AbsDecrB(tid);
+ call IncrB(tid);
+ call UnlockB(tid);
+ yield;
+}
+
+procedure {:yields} {:layer 3} AbsTB({:linear "tid"} tid: X)
+requires {:layer 3} tid != nil && counter == 0;
+{
+ yield;
+ assert {:layer 3} counter == 0;
+ call TB(tid);
+ yield;
+}
+
+procedure {:yields} {:layer 3} main({:linear "tid"} tid: X)
+requires {:layer 3} tid != nil && counter == 0;
+{
+ var {:linear "tid"} cid: X;
+
+ yield;
+ assert {:layer 3} counter == 0;
+ while (*)
+ invariant {:layer 3} counter == 0;
+ {
+ if (*) {
+ call cid := AllocTid();
+ async call TA(cid);
+ }
+ if (*) {
+ call cid := AllocTid();
+ async call AbsTB(cid);
+ }
+ yield;
+ assert {:layer 3} counter == 0;
+ call LockA(tid);
+ call AbsAssertA(tid);
+ call LockB(tid);
+ call AbsAssertB(tid);
+ call UnlockB(tid);
+ call UnlockA(tid);
+ yield;
+ assert {:layer 3} counter == 0;
+ }
+ yield;
+} \ No newline at end of file
diff --git a/Test/civl/funky.bpl.expect b/Test/civl/funky.bpl.expect
new file mode 100644
index 00000000..0a114594
--- /dev/null
+++ b/Test/civl/funky.bpl.expect
@@ -0,0 +1,2 @@
+
+Boogie program verifier finished with 75 verified, 0 errors
diff --git a/Test/civl/ticket.bpl b/Test/civl/ticket.bpl
index 9fc55646..df19aae4 100644
--- a/Test/civl/ticket.bpl
+++ b/Test/civl/ticket.bpl
@@ -6,7 +6,6 @@ axiom (forall x: int, y: int :: RightOpen(x)[y] <==> y < x);
axiom (forall x: int, y: int :: RightClosed(x)[y] <==> y <= x);
type X;
-function {:builtin "MapConst"} mapconstbool(bool): [X]bool;
const nil: X;
var {:layer 0,2} t: int;
var {:layer 0,2} s: int;
@@ -42,7 +41,7 @@ ensures {:layer 1} {:layer 2} xl != nil;
}
procedure {:yields} {:layer 2} main({:linear_in "tid"} xls':[X]bool)
-requires {:layer 2} xls' == mapconstbool(true);
+requires {:layer 2} xls' == MapConstBool(true);
{
var {:linear "tid"} tid: X;
var {:linear "tid"} xls: [X]bool;
@@ -132,7 +131,7 @@ ensures {:layer 1} Inv1(T,t);
}
procedure {:yields} {:layer 0,2} Init({:linear "tid"} xls:[X]bool);
-ensures {:atomic} |{ A: assert xls == mapconstbool(true); cs := nil; t := 0; s := 0; T := RightOpen(0); return true; }|;
+ensures {:atomic} |{ A: assert xls == MapConstBool(true); cs := nil; t := 0; s := 0; T := RightOpen(0); return true; }|;
procedure {:yields} {:layer 0,1} GetTicket({:linear "tid"} tid: X) returns (m: int);
ensures {:atomic} |{ A: m := t; t := t + 1; T[m] := true; return true; }|;