From 5fb565e439255ede7dc3653708af41678b6c1062 Mon Sep 17 00:00:00 2001 From: Shaz Qadeer Date: Tue, 9 Feb 2016 21:35:24 -0800 Subject: added an example --- Test/civl/funky.bpl | 133 +++++++++++++++++++++++++++++++++++++++++++++ Test/civl/funky.bpl.expect | 2 + Test/civl/ticket.bpl | 5 +- 3 files changed, 137 insertions(+), 3 deletions(-) create mode 100644 Test/civl/funky.bpl create mode 100644 Test/civl/funky.bpl.expect 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; }|; -- cgit v1.2.3