diff options
| author |  stefanheule <unknown> | 2011-07-01 11:40:18 +0200 |
|---|---|---|
| committer | stefanheule <unknown> | 2011-07-01 11:40:18 +0200 |
| commit | 29997a5dd73bfe92292caf1c26fea6b04082a7c9 (patch) | |
| tree | 075d85b62fe670d744384aabfc83b01199d36ca0 /Chalice/tests/permission-model/scaling.chalice | |
| parent | 9dfd07f5afe943abf40eaa7a9351ea92748b59ab (diff) | |
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
Diffstat (limited to 'Chalice/tests/permission-model/scaling.chalice')
| -rw-r--r-- | Chalice/tests/permission-model/scaling.chalice | 89 |
1 files changed, 89 insertions, 0 deletions
diff --git a/Chalice/tests/permission-model/scaling.chalice b/Chalice/tests/permission-model/scaling.chalice new file mode 100644 index 00000000..29930346 --- /dev/null +++ b/Chalice/tests/permission-model/scaling.chalice @@ -0,0 +1,89 @@ +/*
+
+Note: At the moment, there is a performance problem if permissions are scaled.
+If a predicate (such as read1 below) contains a read permission, and one takes
+read access to that predicate (as in method s1; rd(read1)), then this
+effectively means that the fractions corresponding to the two read permissions
+are multiplied. This introduces non-linear arithmetic in Boogie, which can be
+very hard and unpredicable for the theorem prover. For this reason, this test is
+taking a very long time to complete.
+
+-- Stefan Heule, June 2011
+
+*/
+
+class Cell {
+ var x: int;
+
+ // --- some predicates ---
+
+ predicate write1 { acc(x) } // full permission in a predicate
+ predicate write2 { acc(x,10) } // 10%
+ predicate read1 { rd(x) } // abstract read permission
+ predicate read2 { rd*(x) } // starred read permission
+ predicate read3 { rd(x,1) } // counting permission (1 epsilon)
+
+ // --- permission scaling ---
+
+ method s1()
+ requires rd(read1);
+ {
+ unfold rd(read1);
+ assert(rd*(x));
+ assert(rd(x)); // ERROR: should fail
+ }
+
+ method s2() // INCOMPLETNESS: postcondition should hold, but fails at the moment
+ requires rd(read1);
+ ensures rd(read1);
+ {
+ unfold rd(read1);
+ fold rd(read1);
+ }
+
+ method s3()
+ requires acc(x);
+ ensures rd(read1);
+ {
+ fold rd(read1);
+ assert(rd*(x));
+ assert(acc(x)); // ERROR: should fail
+ }
+
+ method s4() // ERROR: postcondition does not hold
+ requires acc(x);
+ ensures read1;
+ {
+ fold rd(read1);
+ }
+
+ method s5()
+ requires rd(read2);
+ {
+ unfold rd(read2);
+ assert(rd*(x));
+ assert(rd(x)); // ERROR: should fail
+ }
+
+ method s6()
+ requires acc(x);
+ ensures rd(read2);
+ {
+ fold rd(read2);
+ assert(rd*(x));
+ assert(acc(x)); // ERROR: should fail
+ }
+
+ method s7() // ERROR: postcondition does not hold
+ requires acc(x);
+ ensures read2;
+ {
+ fold rd(read2);
+ }
+
+ // --- helper functions ---
+
+ method void() requires rd(x); ensures rd(x); {}
+ method dispose() requires rd(x); {}
+
+}
|