Contract Reduction Language

ACSL function contract grammar with CIVL-C extension

The CIVL-C function contract extends ACSL function contract with the following elements:

• guards clause: specify the guard of a function, i.e., the specified predicate should hold in order to enable the execution of the function body
• depends clause: specify the dependency relation of the function, usually used for partial order reduction (POR) or other analysis
  • \calls(fun, arg0, arg1, ...): a set of actions that invokes the function with the specified arguments
  • \noact: empty set of actions
  • \anyact: any action sets
  • set of memory actions: \read(mu-list), \write(mu-list)
  • action set operations: + union, - complement, & intersect
• reads clause: specify memory locations read by the function, the syntax of which is similar to assigns clause
• additional parameter for allocates clause: specify the scope of the heap for allocation; if absent then the root scope is used
• wildcard term: ...

function-contract ::= requires-clause∗ terminates-clause? decreases-clause? guards-clause?
                      simple-clause∗  named-behavior∗ completeness-clause∗ 
requires-clause ::= requires pred ;
terminates-clause ::= terminates pred ;
decreases-clause  ::= decreases term (for id)? ;
guards-clause ::= guards pred ;
simple-clause ::= assigns-clause | ensures-clause 
                | allocation-clause | abrupt-clause-fn
                | reads-clause | depends-clause
assigns-clause ::= assigns tsets ;
tsets ::= location (, location) ∗
ensures-clause ::= ensures pred ;
allocation-clause ::= allocates tsets (, scope)? ; | frees tsets ;
reads-clause ::= reads tsets;
depends-clause := depends event (, event)*;
named-behavior ::= behavior id : behavior-body
behavior-body ::= assumes-clause∗ requires-clause∗ simple-clause∗
assumes-clause ::= assumes pred ;
completeness-clause ::= complete behaviors (id (, id)∗)? ;
                      | disjoint behaviors (id (, id)∗)? ;
term ::= \old ( term ) | \result | \nothing | ...
pred ::= \old ( pred )

tset ::= \empty
       | tset -> id 
       | tset . id * tset
       | & tset
       | tset [ tset ]
       | term? .. term?
       | \union ( tset (, tset)∗ )
       | \inter ( tset (, tset)∗ )
       | tset + tset
       | ( tset )
       | { tset | binders (; pred)? }
       | { term } term

literal ::= \true | \false | integer | real | string | character

bin-op ::= + | - | * | / | % | << | >>
         | == | != | <= | >= | > | <
         | && | || | ^^
         | & | | | --> | <--> | ^

unary-op ::= + | - | ! | ~ | * | & 

term ::= literal | id | unary-op term | term bin-op term | term [ term ]
       | { term \with [ term ] = term } 
       | term . id
       | {term \with.id =term }
       | term -> id
       | ( type-expr ) term
       | id ( term (, term)∗ )
       | (term)
       | term ? term : term
       | \let id = term ; term sizeof ( term )
       | sizeof ( C-type-name )
       | id : term 
       | string : term

$memory type

The new built-in type $memory denotes a set of memory units (aka., memory locations). 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 and reads 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/reads location (, location)* or assigns/reads \nothing

where location is a tset expressions of type $memory.

Example:

assigns x,a[i][j],\region(list->head),b[dom];

• absence of assigns/reads clause
  • for non-system functions, the function body is scanned to understand the memory locations assigned/read by it
  • for system functions, only memory locations reachable form the arguments shall be assigned/read

depends clause

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

depends action (, action)*

where action is an action represented as a boolean expression. For each process p, the action can be evaluated in the context of p. If action evaluates to true, then p must be included in an ample set containing a call to this function.

The grammar of event is defined as follows:

EventSetExpression
 ::= \read(MemorySetExpression)
 | \write(MemorySetExpression)
 | \calls(FunctionCallExpression)
 | \noact
 | \anyact
 | ‘(’ EventSetExpression ‘)’
 | EventSetExpression + EventSetExpression
 | EventSetExpression - EventSetExpression
 | EventSetExpression & EventSetExpression

The expression event hence defines a predicate d(s,p), where s ranges over states, and p over procs. The requirement is the following:

Let s be any state and p a proc such that a function call for this function is enabled in p. Then in any execution departing from s, no transition dependent on the execution of this function call can occur without a transition from p or a proc q satisfying d(s,q) occurring first.

The following built-in functions may be used as constituents in the boolean expression e:

• _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 statement S and a process q.

Let T(S,q) denote the set of transitions specified by having q execute S. We say this is a set because some statements S are nondeterministic, meaning they can generate multiple transitions. Note that T(S,q) is independent of the state. In particular, it must include all possible transitions that could be generated by S, even if not all of them are enabled in every state.

Now fix a state s and assume that the origin of S is the location of q in s.

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,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 with origin the 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

Note: AMPLE(s,p) is the smallest set containing p and satisfying:

if q is in AMPLE(s,p) then for all statements S with origin the location of q in s, A(s,S,q) is a subset of AMPLE(s,p).

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 of Claim

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. We aim to get a contradiction.

Say t is dependent on transition t0 in T(S0,q0), for some statement S0 and process q0 in AMPLE.

By assumption, throughout the entire execution prefix (E), q0 remains at the location it had in state s. In particular, the origin of S0 is the location of q0 in s.

Since q0 is in AMPLE, it follows from the algorithm that defines AMPLE that 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(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, contradicting the ASSUMPTION. QED.

Use of $depends

In the case where S is a function call, the depends clause in the function contract specifies the set A(s,S,p) as follows: first the depends clause specifies a predicate d(s,q) where s is a state and q is a proc. Then

A(s,S,p) = {p} U {q|d(s,q)}

Function specifiers

• $atomic_f: may be used to designate that any call to the function is to be treated atomically.
• $pure: specify that a function doesn't have any side effect. (is equivalent to assigns \nothing).

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 $atomic_f. Grammatically, it is a contract clause, though it is not really part of the contract.

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

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

• Barrier

/* Creates a new barrier object and returns a handle to it.
 * The barrier has the specified size.
 * The new object will be allocated in the given scope. */
/*@ requires scope <= $root;
  @ requires size >= 0;
  @ depends \nothing;
  @ guards true;
  @ assigns \nothing;
  @ */
$gbarrier $gbarrier_create($scope scope, int size);

/* Destroys the gbarrier */
/*@ requires barrier != \null; 
  @ guards true;
  @ depends \noact;
  @ assigns barrier;//barrier has pointer type, and is converted into $memory type automatically
  @ */
void $gbarrier_destroy($gbarrier barrier);

/* checks if the global barrier has a vacancy at the specified place */
/*@ requires place >= 0;
  @*/
bool $gbarrier_vacant($gbarrier barrier, int place);

/* returns the process reference that takes the given place of the global barrier */
$proc $gbarrier_process_at($gbarrier barrier, int place);

/* Creates a new local barrier object and returns a handle to it.
 * The new barrier will be affiliated with the specified global
 * barrier.   This local barrier handle will be used as an
 * argument in most barrier functions.  The place must be in
 * [0,size-1] and specifies the place in the global barrier
 * that will be occupied by the local barrier.  
 * Only one call to $barrier_create may occur for each barrier-place pair.
 * The new object will be allocated in the given scope. */
/*@ requires scope <= $root && gbarrier!=\null && place >= 0;
 *@ ensures $gbarrier_process_at(gbarrier, place)==$self;
 *@ depends \calls($barrier_create, $everything, gbarrier, place);
 *@ assigns \nothing;
 *@ behavior success:
 *@   assumes $gbarrier_vacant(gbarrier, place);
 *@   allocates \result, scope;
 *@ behavior failure:
 *@   assumes !$gbarrier_vacant(gbarrier, place);
 *@   allocates \nothing, scope;
 *@ complete behaviors;
 *@ disjoint behaviors;
 */
$barrier $barrier_create($scope scope, $gbarrier gbarrier, int place);

/* Destroys the barrier. */
/*@ requires barrier != \null ==> \freeable{Here}(barrier);
  @ assigns \nothing;
  @ frees barrier;
  @ ensures barrier !=null ==> \allocable{Here}{barrier}; // what does it mean by \allocable?
  @ // the above is actually copied from ACSL reference where there is an example of contracts for free().
  @ 
  @*/
void $barrier_destroy($barrier barrier);

/* Calls the barrier associated with this local barrier object.*/
/*@ depends \noact;
  @ assigns \nothing; // although the barrier records is updated but it gets cleaned up when the method returns
  @*/
void $barrier_call($barrier barrier);

• A simple C implementation of queue

struct cqueue_t{
  int data[];
  $proc owner;
};

/*@ depends \noact;  
  @ assigns \nothing;
  @ reads \nothing; 
  @*/
$atomic_f void create(cqueue* q)
{
  q = (cqueue*)$malloc($root, sizeof(cqueue));
  q->owner=$proc_null;
  $seq_init(&q->data, 0, NULL);
}

/*@ depends \read(q->owner), \write(q->owner);
  @ assigns q->owner;
*/
$atomic_f _Bool lock(cqueue* q)
{
  if(q->owner==$self)
    return $true;
  if(q->owner == $proc_null){
    q->owner=$self;
    return $true;
  }else
    return $false;
}

/*@ depends \calls(enqueue, q, ...), $calls(dequeue,q, ...);
  @ reads q->data;
  @ assigns \nothing;
  @*/
$pure $atomic_f int size(cqueue* q)
{
  return $seq_length(&q->data); 
}

/*@ reads q->owner;
  @ behavior success:
  @   assumes q->owner==$self;
  @   depends \access(q->owner);
  @   assigns q->owner;
  @ behavior failure:
  @   assumes q->owner!=$self;
  @   depends \nothing;
  @   assigns \nothing;
  @*/
$atomic_f _Bool unlock(cqueue* q)
{
  if(q->owner==$self)
  {
    q->owner=$proc_null;
    return $true;
  }
  return $false;
}

/*@ depends calls(enqueue,q, ...);
  @ assigns q->data;
  @*/
$atomic_f _Bool enqueue(cqueue* q, int v)
{
  $seq_append(&q->data, &v, 1);
}

/*@ depends calls(enqueue, q, ...);
  @ assigns q->data;
  @*/
$atomic_f _Bool dequeue(cqueue* q, int* res)
{
  $seq_remove(&q->data, $seq_length(&q->data)-1, res, 1);
}