Changes between Version 11 and Version 12 of ContractReduction

Timestamp:

07/21/14 11:29:28 (12 years ago)

Author:

siegel

Comment:

--

ContractReduction

@@ -1 +1 @@
 == Contract Reduction Language  ==
+
+
+== `$memory` type ==
+
+The new built-in type `$memory` denotes a set of memory units.  The following expressions have type `$memory`:
+* a left-hand-side expression, when used in certain contexts, is automatically converted to `$memory`.  The contexts are: arguments to the built-in functions `$access`, `$read`, and `$write` described below, or occurrence in the list of an `$assigns` clause
+* `a[dom]`, where `a` is an expression of array type and `dom` is an expression of `$domain` type.   The dimension of the array must match the dimension of the domain.   This represents all memory units which are the cells in the array indexed by a tuple in `dom`.
+* `$region(ptr)`, where `ptr` is an expression with a pointer type.  This represents the set of all memory units reachable from `ptr`, including the memory unit pointed to by `ptr` itself.
+
+[[* `mem1+mem2`, where `mem1` and `mem2` are expressions of type `$memory`.  This is the union of the two sets.]]  Problem this is ambiguous with numeric +, as in x+y.
+
+== `$assigns` clause ==
+
+As in other contract specification language, this contract clause is used to specify a set of existing memory units.    The claim is that if an existing memory unit is not in the set, it will not be modified in the course of the function call.  The syntax is:
+{{{
+$assigns <memory-list>;
+}}}
+where `<memory-list>` is a comma-separated list of expressions of type `$memory`.
+
+Example:
+{{{
+$assigns x,a[i][j],$region(list->head),b[dom];
+}}}
+
 
 == `$depends` clause ==
 
-The following contractual clause may appear in a function contract in the same places that `$ensures` or `$requires` clauses can appear:
+This contractual clause specifies part of the dependence relation used in POR.
 {{{
 $depends e ;
@@ -9 +33 @@
 where `e` is an expression of boolean type.   For each process `p`, the `e` can be evaluated in the context of `p`.   If `e` evaluates to `true`, then `p` must be included in an ample set containing a call to this function. 
 
-The following boolean expressions may be used as constituents in the boolean expression `e`:
+The following built-in functions may be used as constituents in the boolean expression `e`:
 
-* `$reaches(void * obj)`
- * holds iff the memory unit pointed to by `obj` is reachable from `p`.  This means there is a path from the variables on the call stack of `p` to the memory unit, following array elements, struct members, and pointer dereferences, pointer arithmetic.
-* `$reachesRegion(void * obj)`
- * holds iff any of the memory units reachable from `obj` (including the object pointed to by `obj` itself) is reachable from`p`
-* `$writes(void * obj)`
- * holds iff the memory unit pointed to by `obj` is not only reachable from `p` but if it is possible that `p` (or a process spawned by `p`) could write to that memory unit at some point now or in the future.
-* `$writesRegion(void * obj)`
- * like above but true if any of the memory units in the reachable region specified by `obj` may be written to
+* `_Bool $access($memory mem)`
+ * holds if any memory unit in `mem` may be read or modified by `p` at some point now or in the future.
+* `_Bool $write($memory mem)`
+ * holds if any memory unit in `mem` may be modified by `p` at some point now or in the future.
+* `_Bool $read($memory mem)`
+ * holds if any memory unit in `mem` may be read by `p` at some point now or in the future.
 
-Default: if there is `$depends` clause present:
+Default: if there is no `$depends` clause present:
 * if the body of the function is not provided, i.e., the function is a system function, the verifier will assume that execution of the function may read and/or modify any memory unit that it can reach, and decide on the partial order reduction appropriately
 * if the body of the function is present, the statements comprising the body may be analyzed to further restrict the reduction.
@@ -28 +50 @@
 Both `$atomic` and `$atom` may be used as function specifiers.   They designate that any call to the function is to be treated atomically or atom-ly, respectively.
 
-== `$assigns` clause ==
-
-As in other contract specification language, this clause is used to specify a set of existing memory units.    The claim is that if an existing memory unit is not in the set, it will not be modified in the course of the function call.
-
-The argument following the `$assigns` token is a comma-separated list.  The elements of the list may be left-hand-side expressions, or an expression of the form
-{{{
-$region(ptr)
-}}}
-where `ptr` is expression which has a pointer type.  It denotes the set of all memory units reachable from that pointer, beginning with and including the memory unit pointer to by `ptr`.
-Example:
-{{{
-$assigns x,a[i][j],$region(list->head);
-}}}
-
 
 
@@ -48 +56 @@
 - 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.
 {{{
-void comm_deque($comm comm, ....)
-  $depend $access(void * obj);
+void comm_dequeue($comm comm, ....)
+  $depends $access(*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.
-{{{
-void strcpy(char *a, char *b)
-  $depend $accessRegion(a) || $writeRegion(b);
-;
-}}}
-
-- The following means that the current process itself can form the ample set.
-{{{
-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.
-{{{
-void comm_deque($comm comm, int count ....)
-  $depend count==0 ? $false : $access(comm);
-;
-}}}