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 expressions ==

Some new expressions will make it easy to create new ranges and domains using range and domain literals.

The range literal
{{{
lo..hi
}}}
where `lo` and `hi` are expressions of integer type, represents the same range as `$range_regular(lo, hi, 1)`.  The range literal
{{{
lo..hi#step
}}}
where all three identifiers signify expressions of integer type, represents the same range as `$range_regular(lo, hi, step)`.

The domain literal
{{{
{ r1, r2, ...}
}}}
where `r1`, `r2`, ..., are all expressions of range type, represents the domain `$domain_rectangular(r1, r2, ...)`.

== 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?