Changes between Version 8 and Version 9 of ContractReduction

Timestamp:

07/02/14 15:48:15 (12 years ago)

Author:

zmanchun

Comment:

--

ContractReduction

@@ -19 +19 @@
 
 
+DEFAULT (when the `$depend` expression is absent): if no `$ample` expression is present, then the library enabler needs to calculate the ample set.
 
-I think the following can be done just using the ternary operator `?`:
-
-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, ....);
+void comm_deque($comm comm, ....)
+  $depend $access(void * obj);
+;
 }}}
 
 - 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);
+void strcpy(char *a, char *b)
+  $depend $accessRegion(a) || $writeRegion(b);
+;
 }}}
 
 - The following means that the current process itself can form the ample set.
 {{{
-$ample($false)
-int $comm_size($comm, ...);
+int $comm_size($comm, ...)
+  $depend $false;
+;
 }}}
 
 - The following means that if the argument `count` is equal to zero, then the current process forms the ample set, otherwise, any process that can reach the memory unit of object `comm` should be in the ample set.
 {{{
-[count = 0] $ample{$false} : $ample{$reach(comm)}
-void comm_deque($comm comm, int count ....);
+void comm_deque($comm comm, int count ....)
+  $depend count==0 ? $false : $access(comm);
+;
 }}}