Chalice: New permission model that provides more abstraction and more flexibility. Details of the model can be found in the paper 'Fractional Permissions without the Fractions', FTfJP 2011 (see http://www.pm.inf.ethz.ch/publications/).

This changeset also fixes several bugs not directly related to the permissions model and improves the error handling. The following features have been added or enhanced:
- Error handling: If exceptions (e.g. about not supported features) are encountered, a user-friendly message is displayed
- Sequence axioms: There is an additional axiom for singleton lists, which is helpful in some cases
- Prelude: Chalice's prelude has been split into sections (e.g. one for permission-related stuff, one for sequence axioms, and so on), which are included on demand (less superfluous axioms, etc.)
Currently not working - but planned to be updated as well - are the following features:
- Stepwise refinements
- autoFold
- read locks
There is a performance issue with permission scaling (i.e., taking non-full versions of predicates that contain read-permissions). Details can be found in the following file: Chalice/tests/permission-model/scaling.chalice.

A list of fixed bugs (see http://boogie.codeplex.com/workitem/<workitem number> for details on the individual bugs)
- workitem 10200: Issue with the axiom of framing functions
- workitem 10197: The translation of old(waitlevel) resultet in Boogie error
- workitem 10196: Quantification over empty sequences
- workitem 10195: Contradiction when descending sequences are used
- workitem 10192: Invalid translation of old-construct in certain cases
- workitem 10190: Stack overflow when parsing large comment blocks
- workitem 10147: Duplicated method parameters and return values are not detected

1 files changed, 0 insertions, 79 deletions

diff --git a/Chalice/examples/PetersonsAlgorithm.chalice b/Chalice/examples/PetersonsAlgorithm.chalice
deleted file mode 100644
index 8760b04b..00000000
--- a/Chalice/examples/PetersonsAlgorithm.chalice
+++ /dev/null
@@ -1,79 +0,0 @@
-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; ]]

-    }

-  }

-}