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 (a, ...).

• $reach(a, ...)

returns true iff the memory unit of the object a (or 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 (or others if present) is reachable by a given process p'.

• $write(a, ...)

returns true iff the memory unit of the object a (or 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 (or 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, ...);
  

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