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

4 files changed, 92 insertions, 4 deletions

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