Contract Reduction Language

Given a process p that is at a state that a call to a system function f is enabled, if p is chosen in the ample set, then the following represents the set of processes other than p that have to be in the ample set as well:

$ample{ BOOLEAN EXPRESSION }

where BOOLEAN EXPRESSION is composed of the following functions over f's arguments.

• $reach(a, ...)

returns true iff the memory unit of the object a (and others if present) is reachable by a given process p'.

• $reach_from(a, ...)

returns true iff any of the memory units reachable from the object a (and others if present) is reachable by a given process p'.

• $write(a, ...)

returns true iff the memory unit of the object a (and others if present) is to be written now or in the future by a given process p'.

• $write_from(a, ...)

returns true iff any of the memory units reachable from the object a (and others if present) is to be written now or in the future by a given process p'.

• $ample{$true}

any process exists in the state should be in the ample set

• $ample{$false}

any process other than the current process ($self) need NOT be in the ample set.

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