This is a proposal to add some new constructs to CIVL-C. The goals are to make it easier to translate from source languages/APIs to CIVL-C and to enable optimizations in the model checker and possibly other static analysis tools.

New types

• $range : an ordered set of integers
• $domain(n) : an ordered set of n-tuples of integers; an "n-dimensional" domain. n is at least 1.
• $domain: union over all n>=1 of $domain(n). For each n, $domain(n) is a subtype of $domain. it is exactly the same as the array types in CIVL-C.

New functions dealing with the types above

// range consisting of lo, lo+step, lo+2*step, ...
// the sequence stops just before the first number
// greater than hi.
$range $range_regular(int lo, int hi, int step);

// domain which is the Cartesian products of the given ranges.
// this is a var-args function; the number of arguments determines
// the dimension of the domain returned.    The order is dictionary
// order.
$domain $domain_rectangular($range r1, ...);

// returns the dimension of the domain
int $domain_get_dim($domain d);

New statements

$for (i1, i2, ... : dom) S

i1, i2, ... are variables of integer type. These are called the "index variables". dom is an expression of type $domain. The number of index variables must equal the dimension of dom.

S is a statement.

Semantics: loop over all elements of the domain and execute S for each such element.

In the form above, the index variables must have been previously declared; alternatively, they can be declared inside the statement:

$for (int i1, i2, ... : dom) S

Next, a parallel version of above:

$parfor (i1, i2, ... : dom) S

Similar to $for, but instead of executing sequentially, a process (thread) is instantiated for each element of the domain and they all execute concurrently. There is an implicit barrier at the end of S and all the processes are waited on.

Example 1: OpenMP parallel construct

#pragma omp parallel {
  ...
}

=>

int nthreads = 1+$choose_int(THREADS_MAX);
$range thread_range = $range_regular(0, nthreads-1, 1);
$domain(1) thread_dom = $domain_rectangular(thread_range);
$parfor (int tid : thread_dom) {
  ...
}

Example 2: CUDA 3d grid

__kernel__ grid() {
  ...
}

grid<<<nx,ny,nz>>>();

=>

grid(int idx, int idy, int idz) {
  ...
}

$range grid_range_x = $range_regular(0, nx-1, 1);
$range grid_range_y = $range_regular(0, ny-1, 1);
$range grid_range_z = $range_regular(0, nz-1, 1);
$domain(3) block_dom = $domain_rectangular(grid_range_x,
  grid_range_y, grid_range_z);
$parfor (int idx, idy, idz : block_dom)  grid(idx, idy, idz);

Optimization

The purpose of the parfor construct is to enable possible optimization in CIVL. The model checker, for example, when control reaches the parfor loop, may try to determine that any two iterations are non-interfering, i.e., any atomic statement from one iteration will commute with any atomic statement from a different iteration. In this case, it will just execute the loop sequentially without creating any new threads.

Worksharing

We could take this further and provide in CIVL-C "worksharing" constructs similar to those in OpenMP. Would this be a good idea?