From 28e03877a9c41dc0556d17115ccd1647f9eddcf6 Mon Sep 17 00:00:00 2001 From: rustanleino Date: Mon, 19 Jul 2010 20:46:55 +0000 Subject: Chalice: Introduced '[[ S ]]' as a shorthand syntax for 'lock (this) { S }'. Think of the new brackets as atomicity brackets (see PetersonsAlgorithm.chalice) Chalice: Added Peterson's algorithm to test suite (safety properties only) VS 2010 integration: Updated Chalice and Dafny modes, added keyword highlighting for a new Boogie mode --- Chalice/examples/Answer | 3 ++ Chalice/examples/PetersonsAlgorithm.chalice | 79 +++++++++++++++++++++++++++++ Chalice/src/Parser.scala | 11 ++-- Chalice/test.bat | 3 +- 4 files changed, 92 insertions(+), 4 deletions(-) create mode 100644 Chalice/examples/PetersonsAlgorithm.chalice (limited to 'Chalice') diff --git a/Chalice/examples/Answer b/Chalice/examples/Answer index 5df00502..ab085a36 100644 --- a/Chalice/examples/Answer +++ b/Chalice/examples/Answer @@ -240,6 +240,9 @@ Boogie program verifier finished with 19 verified, 4 errors 65.5: The loop might lock/unlock more than the lockchange clause allows. Boogie program verifier finished with 14 verified, 3 errors +------ Running regression test PetersonsAlgorithm.chalice + +Boogie program verifier finished with 7 verified, 0 errors ------ Running regression test cell-defaults.chalice 96.5: The heap of the callee might not be strictly smaller than the heap of the caller. 102.5: The heap of the callee might not be strictly smaller than the heap of the caller. diff --git a/Chalice/examples/PetersonsAlgorithm.chalice b/Chalice/examples/PetersonsAlgorithm.chalice new file mode 100644 index 00000000..8760b04b --- /dev/null +++ b/Chalice/examples/PetersonsAlgorithm.chalice @@ -0,0 +1,79 @@ +class Peterson { + var x0: bool; + var x1: bool; + var turn: bool; + ghost var cs0: bool; + ghost var cs1: bool; + ghost var b0: bool; + ghost var b1: bool; + + invariant acc(x0,50) && acc(x1,50) && acc(turn); + invariant acc(cs0,50) && acc(cs1,50) && acc(b0,50) && acc(b1,50); + invariant cs0 ==> x0 && !b0 && (!x1 || !turn || b1); + invariant cs1 ==> x1 && !b1 && (!x0 || turn || b0); + + method Main() { + var p := new Peterson{ x0 := false, x1 := false, + cs0 := false, cs1 := false, b0 := false, b1 := false }; + share p; + fork p.Process0(); + fork p.Process1(); + // The purpose of the following loop is simply to prove mutual exclusion, that is, + // to prove that !(cs0 && cs1) follows from the monitor invariant. + while (true) + invariant rd(p.mu) && waitlevel << p.mu; + { + lock (p) { assert !(p.cs0 && p.cs1); } + } + } + + method Process0() + requires rd(mu) && waitlevel << mu; + requires acc(x0,50) && acc(cs0,50) && acc(b0,50) && !x0 && !cs0 && !b0; + { + while (true) + invariant rd(mu) && waitlevel << mu; + invariant acc(x0,50) && acc(cs0,50) && acc(b0,50) && !x0 && !cs0 && !b0; + { + [[ x0 := true; b0 := true; ]] + [[ turn := true; b0 := false; ]] + // await (!x1 || !turn) + var waiting := true; + while (waiting) + invariant rd(mu) && waitlevel << mu && acc(cs0,50); + invariant acc(x0,50) && acc(b0,50) && x0 && !b0; + invariant !waiting ==> cs0; + { + [[ if (!x1) { waiting := false; cs0 := true; } ]] + [[ if (!turn) { waiting := false; cs0 := true; } ]] + } + // critical section... + [[ cs0 := false; x0 := false; ]] + } + } + + method Process1() + requires rd(mu) && waitlevel << mu; + requires acc(x1,50) && acc(cs1,50) && acc(b1,50) && !x1 && !cs1 && !b1; + { + while (true) + invariant rd(mu) && waitlevel << mu; + invariant acc(x1,50) && acc(cs1,50) && acc(b1,50) && !x1 && !cs1 && !b1; + { + [[ x1 := true; b1 := true; ]] + [[ turn := false; b1 := false; ]] + // await (!x0 || turn) + var waiting := true; + while (waiting) + invariant rd(mu) && waitlevel << mu && acc(cs1,50); + invariant acc(x1,50) && acc(b1,50) && x1 && !b1; + invariant !waiting ==> cs1; + { + [[ if (!x0) { waiting := false; cs1 := true; } ]] + [[ if (turn) { waiting := false; cs1 := true; } ]] + } + // critical section... + [[ cs1 := false; x1 := false; ]] + } + } +} diff --git a/Chalice/src/Parser.scala b/Chalice/src/Parser.scala index 8a87d2f6..12a989d7 100644 --- a/Chalice/src/Parser.scala +++ b/Chalice/src/Parser.scala @@ -36,7 +36,7 @@ class Parser extends StandardTokenParsers { "seq", "nil", "result", "eval", "token", "wait", "signal") // todo: can we remove "nil"? - lexical.delimiters += ("(", ")", "{", "}", + lexical.delimiters += ("(", ")", "{", "}", "[[", "]]", "<==>", "==>", "&&", "||", "==", "!=", "<", "<=", ">=", ">", "<<", "+", "-", "*", "/", "%", "!", ".", "..", @@ -114,8 +114,11 @@ class Parser extends StandardTokenParsers { | "lockchange" ~> expressionList <~ Semi ^^ LockChange ) def blockStatement: Parser[List[Statement]] = { + "{" ~> blockStatementBody <~ "}" + } + def blockStatementBody: Parser[List[Statement]] = { val prev = currentLocalVariables - "{" ~> (statement*) <~ "}" ^^ { + (statement*) ^^ { case x => currentLocalVariables = prev; x } } @@ -125,7 +128,7 @@ class Parser extends StandardTokenParsers { // statements - def statement = + def statement: Parser[Statement] = positioned( "assert" ~> expression <~ Semi ^^ Assert | "assume" ~> expression <~ Semi ^^ Assume | blockStatement ^^ BlockStmt @@ -148,6 +151,8 @@ class Parser extends StandardTokenParsers { | "release" ~> expression <~ Semi ^^ Release | "lock" ~> "(" ~> expression ~ ")" ~ blockStatement ^^ { case e ~ _ ~ b => Lock(e, BlockStmt(b), false) } + | "[[" ~> blockStatementBody <~ "]]" ^^ { + case b => Lock(ExplicitThisExpr(), BlockStmt(b), false) } | "rd" ~> ( "lock" ~> "(" ~> expression ~ ")" ~ blockStatement ^^ { case e ~ _ ~ b => Lock(e, BlockStmt(b), true) } diff --git a/Chalice/test.bat b/Chalice/test.bat index f7c933aa..7432a145 100644 --- a/Chalice/test.bat +++ b/Chalice/test.bat @@ -10,7 +10,8 @@ REM to do: Leaks -checkLeaks for %%f in (cell counter dining-philosophers ForkJoin HandOverHand iterator iterator2 producer-consumer prog0 prog1 prog2 prog3 prog4 ImplicitLocals - RockBand swap OwickiGries ProdConsChannel LoopLockChange) do ( + RockBand swap OwickiGries ProdConsChannel LoopLockChange + PetersonsAlgorithm) do ( echo Testing %%f.chalice ... echo ------ Running regression test %%f.chalice >> Output %CHALICE% %* examples\%%f.chalice >> Output 2>&1 -- cgit v1.2.3