Changes between Initial Version and Version 1 of ConcurrencyExtensions

Timestamp:

06/04/14 11:09:21 (12 years ago)

Author:

siegel

Comment:

--

ConcurrencyExtensions

@@ +1 @@
+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);
+$domain(1) thread_dom = $domain_rectangular(thread_range);
+$parfor (int i : 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);
+$range grid_range_y = $range_regular(0, ny-1);
+$range grid_range_z = $range_regular(0, nz-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
+`parlor` 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.