== 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, the dependency information will be obtained from Java code in the library enabler.  If the library enabler does not specify anything for this function, the default rules will be used, which are sound:
* 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, else
* if the body of the function is present, the statements comprising the body may be analyzed to further restrict the reduction.

== Ample set and the exact interpretation of $depends ==

Fix a state s, a process q, and a statement S.

Let T(s,S,q) denote the set of transitions specified by having q execute S from s.  We say this is a set because some statements S are nondeterministic, meaning they can generate multiple transitions. Note that T(s,S,q) includes all transitions specified by S, even those that are not enabled.

Suppose A(s,S,q) is a set of procs which satisfies the following:

In any execution departing from s, no transition dependent on a transition in T(s,S,q) can occur without a transition from a proc in A(s,S,q) occurring first.

Then define AMPLE as follows:
{{{
Function AMPLE(s:State, p:proc) : set of proc is
  let AmpleProcs = {p};
  let WorkSet = {p};
  // invariant: WorkSet is a subset of AmpleProcs
  while (WorkSet not empty) {
    choose q in WorkSet;
    WorkSet := WorkSet - {q};
    forall statements S emanating from current location of q in s:
      foreach r in A(s,S,q): if r is not in AmpleProcs, add r to AmpleProcs and to WorkSet
    end forall;
  }
  return AmpleProcs;
end Function AMPLE
}}}

Claim: for any process p, if AMPLE(s,p) contains a process with at least one enabled transition in s, then it defines an ample set, i.e., from any execution departing from s, no transition dependent
on a transition from a proc in AMPLE(s,p) can occur without a transition from a proc in AMPLE(s,p) occurring first.

Proof:  Let AMPLE=AMPLE(s,p).
Let

  (E)  t_1, t_2, ..., t_n, t

be any execution prefix starting from s for which t is dependent on a transition from a proc in AMPLE.

ASSUME that none of the t_i are from procs in AMPLE.

Say t is dependent on transition t0, and that t0 has statement S0 in process q0, and q0 is in AMPLE.

Throughout the entire execution prefix (E), q0 remains at the location it had in state s.  In particular, S0 emanates 
from the current location of q0 in s.

Since q0 is in AMPLE, that means from the algorithm that defines AMPLE that we must
have A(s,S0,q0) is a subset of AMPLE.

From the contract defining A, we know that no transition dependent on a transition in T(s,S0,q0) can occur without a transition
from a proc in A(s,S0,q0) occurring first.  Hence for some i, t_i is from a proc in A(s,S0,q0), and therefore t_i is in AMPLE.

We conclude that no transition dependent on a transition from a proc in AMPLE can occur without a transition from a proc
in AMPLE occurring first.  QED.


== 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.

== Guards ==

The following construct is used to specify a guard for a function.  The function may be a system or ordinary function.  It maybe used in conjunction with `$atom` or `$atomic`.
Grammatically, it is a contract clause, though it is not really part of the contract.  

{{{
$guard <bool-expr> ;
}}}

If missing, the default is to go the library enabler for the guard.  If the library enabler does not specify a guard, it defaults to `$true`.

==  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);
;
}}}