Contract Reduction Language

The following contractual clause may appear in a function contract in the same places that $ensures or $requires clauses can appear:

$depends expr ;

where expr is an expression of type function-from-$proc-to-boolean. This expression will usually be specified as a lambda expression:

$depends $lambda($proc p) e ;

where e is a boolean expression, usually involving p.

The following boolean expressions may be used as constituents in the boolean expression e:

• $reach($proc p, void * obj)

returns true iff the memory unit pointed to by obj is reachable from process p. This means there is a path from the variables on the call stack of p to the memory unit, following following array elements, struct members, and pointer dereferences.

• $reach_rec($proc p, void * obj)

returns true iff any of the memory units reachable from the object pointed to by obj (including the object pointed to by obj itself) is reachable from process p'.

• $write($proc p, void * obj)

returns true 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.

• $write_rec($proc p, void * obj)

like above but true if any of the memory units in the reachable region specified by obj may be written to

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, ...);
  

• 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 ....);