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, 35 deletions

diff --git a/Chalice/examples/OwickiGries.chalice b/Chalice/examples/OwickiGries.chalice
deleted file mode 100644
index f466b58a..00000000
--- a/Chalice/examples/OwickiGries.chalice
+++ /dev/null
@@ -1,35 +0,0 @@
-class OwickiGries {

-  var counter: int

-  ghost var c0: int

-  ghost var c1: int

-  invariant acc(counter) && acc(c0,50) && acc(c1,50) && counter == c0 + c1

-

-  method Main() {

-    var og := new OwickiGries{ counter := 0, c0 := 0, c1 := 0 }

-    share og

-

-    fork tk0 := og.Worker(false)

-    fork tk1 := og.Worker(true)

-    join tk0; join tk1

-

-    acquire og; unshare og

-    assert og.counter == 2

-  }

-

-  method Worker(b: bool)

-    requires rd(mu) && waitlevel << mu

-    requires (!b ==> acc(c0,50)) && (b ==> acc(c1,50))

-    ensures rd(mu)

-    ensures !b ==> acc(c0,50) && c0 == old(c0) + 1

-    ensures b ==> acc(c1,50) && c1 == old(c1) + 1

-  {

-    lock (this) {

-      counter := counter + 1

-      if (!b) {

-        c0 := c0 + 1

-      } else {

-        c1 := c1 + 1

-      }

-    }

-  }

-}