Changes between Initial Version and Version 1 of ContractReduction

Timestamp:

06/29/14 23:19:32 (12 years ago)

Author:

zmanchun

Comment:

--

ContractReduction

@@ +1 @@
+== Contract Reduction Language  ==
+
+Given a process `p` that is at a state that a call to a system function `f` is enabled,
+if `p` is chosen in the ample set, then the following represents the set of processes other than
+`p` that have to be in the ample set as well:
+
+`$ample{ BOOLEAN EXPRESSION }`
+
+    where `BOOLEAN EXPRESSION` is composed of the following functions over `f`'s arguments.
+
+- `$reach(a, ...)`
+    returns true iff the memory unit of the object `a` (and others if present) is reachable by a given process `p'`.
+
+- `$reach_from(a, ...)`
+    returns true iff any of the memory units reachable from the object `a` (and others if present) is reachable by a given process `p'`.
+
+- `$write(a, ...)`
+    returns true iff the memory unit of the object `a` (and others if present) is to be written now or in the future by a given process `p'`.
+
+- `$write_from(a, ...)`
+    returns true iff any of the memory units reachable from the object `a` (and others if present) is to be written now or in the future by a given process `p'`.
+
+- `$ample{$true}`
+    any process exists in the state should be in the ample set
+
+- `$ample{$false}`
+    any process other than the current process (`$self`) need NOT be in the ample set.
+
+Conditional amples set: `[COND] $ample{EXPR1} : $ample(EXPR2)`
+    if `COND` is satisfied then processes satisfying `EXPR1` should be in the ample set;
+    otherwise, `EXPR2` is considered.
+
+Absent ample set (DEFAULT case): if no `$ample` expression is present, then the library enabler needs to calculate the ample set.
+
+   
+Examples:
+- The following means that any process that can reach the memory unit of `comm` should be in the ample set if the current process (`$self`) is to be chosen in the ample set.
+{{{
+$ample{$reach(comm)}
+void comm_deque($comm comm, ....);
+}}}
+
+- The following means that any process that can reach any of the memory units reachable from `a` or write any of the memory units reachable from `a` now or in the future should be in the ample set if the current process (`$self`) is to be chosen in the ample set.
+{{{
+$ample{$reach_from(a) || $write_from(b)}
+void strcpy(char *a, char *b);
+}}}
+
+- The following means that the current process itself can form the ample set.
+{{{
+$ample($false)
+int $comm_size($comm, ...);
+}}}