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

This contractual clause specifies part of the dependence relation used in POR.

$depends e ;

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 built-in functions may be used as constituents in the boolean expression e:

• _Bool $access(<memory-list>)
  • holds if any memory unit in the list may be read or modified by p at some point now or in the future.
• _Bool $write(<memory-list>)
  • holds if any memory unit in the list may be modified by p at some point now or in the future.
• _Bool $read(<memory-list>)
  • holds if any memory unit in the list may be read by p at some point now or in the future.

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.

Function specifiers

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.

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.

  void comm_dequeue($comm comm, ....)
    $depends $access(*comm);
  ;