== The Sequentially Consistent Subset of OpenMP ==
OpenMP programs that:
* Do not use non-sequentially consistent atomic directives;
* Do not rely on the accuracy of a false result from omp_test_lock and omp_test_nest_lock; and
* Correctly avoid data races as required in Section 1.4.1 on page 23 (OpenMP spec 5.0)

The relaxed consistency model is invisible for such programs, and any explicit flush operations in such programs are redundant.

== OpenMP Constructs ==

* `parallel`
 * `private(`list`)`
 * `firstprivate(list)`
 * `copyin(list)`
 * `shared(`list`)`
 * `default(none`|`shared)`
 * `num_threads(`n`)`
 * `reduction(op:list)`

* `sections`
 * `private(`list`)`
 * `firstprivate(list)`
 * `lastprivate(list)`
 * `reduction(op:list)`
 * `nowait`

* `section`

* `single`
 * `private(`list`)`
 * `firstprivate(list)`
 * `copyprivate(list)`
 * `nowait`
 
* `for`
 * `private(`list`)`
 * `firstprivate(list)`
 * `lastprivate(list)`
 * `reduction`
 * `schedule`
 * `collapse`
 * `nowait`

* `simd`
 * `safelen(n)`
 * `linear(n)`
 * `aligned(n)`
 * `private`
 * `lastprivate`
 * `reduction`
 * `collaplse`

* `for simd`
 * `safelen(n)`
 * `linear(n)`
 * `aligned(n)`
 * `private`
 * `lastprivate`
 * `reduction`
 * `collapse`
 * `firstprivate`
 * `nowait`
 * `schedule`

* `declare simd`
 * `simdlen(n)`
 * `linear`
 * `aligned(n)`
 * `uniform`
 * `inbranch`
 * `notinbranch`

* `barrier`

* `critical`
 * `[name]`

* `atomic`
 * `read | write | update | capture`
 * `seq_cst`

* `master`

== OpenMP Types ==
* `omp_lock_t`

== OpenMP Functions ==
* `omp_get_num_threads()`
* `omp_get_thread_num()`
* `omp_get_wtime()`

== OpenMP Functions ==
* `omp_init_lock`
* `omp_destroy_lock`
* `omp_set_lock`
* `omp_unset_lock`
* `omp_test_lock`

== Plan ==
* We are going to get rid of the current OMP2CIVL transformer and come up a new transformer that assumes given OpenMP programs are sequentially consistent
* We are gong to improve the current OmpSimplifier using pointer alias analysis
* Note that an atomic construct without `seq_cst` is outside of the  sequentially consistent subset of the language, we need a way to deal with that.

== Notes ==
* Currently, the simplifier is not aware of the cases that out-of-bound access on multiple dimensional arrays can raise data race.  For example, 
{{{
int a[10][5];
#pragma omp parallel for 
for (int i = 0; i < 5; i++)
  for (int j = 1; j < 10; j++)
    a[i][j] = a[i][j-1] // a[0][4] and a[1][-1] refer to the same element
}}}

The current simplifier will incorrectly sequentialize the example above without realizing the fact that this example is sequentializable if and only if no "logical" out-of-bound happens during the execution.
A fix for the simplifier could be sequentializing the example with inserted assertion for making sure that there is no "logical" out-of-bound error.

== Related ==
* [[wiki: StaticAnalysis| Static Analysis]]

== OpenMP Simplifier ==
* We improve the existing OpenMP simplifier with the informations provided by the [[wiki: StaticAnalysis| Static Analysis]].
* Example 1: (`DRB067-restrictpointer1-orig-no.c` from [https://github.com/LLNL/dataracebench/releases/tag/v1.2.0 DataRaceBench v1.2.0])
{{{
#include <stdlib.h>
typedef double real8;

void foo(real8 * restrict newSxx, real8 * restrict newSyy, int length)
{
  int i;

#pragma omp parallel for private (i) firstprivate (length)
  for (i = 0; i <= length - 1; i += 1) {
    newSxx[i] = 0.0;
    newSyy[i] = 0.0;
  }
}

int main()
{
  int length=10;
  real8* newSxx = malloc (length* sizeof (real8));
  real8* newSyy = malloc (length* sizeof (real8));

  foo(newSxx, newSyy, length);

  free (newSxx);
  free (newSyy);
  return 0;
}
}}}
  * The OpenMP simplifier analyzes the parallel region with points-to informations about the two pointer argument `newSxx` and `newSyy` from static analysis.
  * The OpenMP simplifier can determine that no data race will happen in the parallel region as long as no array out-of-bound error happens in it.
  * The OpenMP simplifier sequentializes the program which will be checked by CIVL.  Any possible array out-of-bound error will be caught by CIVL.

== Capture Read / Write at Runtime ==
* If the OpenMP Simplifier fails to sequentialize a program,  transform the OpenMP program to the following form for model checking:
{{{
$mem writes[nthreads], reads[nthreads];
$parfor (int tid:0..nthreads-1) {
  $write_set_push();
  $read_set_push();
  block1;
  // barrier
  writes[tid] = $write_set_pop();                                                                                                                
  reads[tid] = $read_set_pop();
  // check for dataraces (collective operation)                                                                            
  $write_set_push();
  $read_set_push();
  // barrier                                                                                                                  
  stmt2;
  // barrier
  writes[tid] = $write_set_pop();                                                                                                                
  reads[tid] = $read_set_pop();                                                                                                                 
  // check for dataraces (collective operation)
}
}}}
* Functions for managing `$mem` objects can be found in `mem.cvh`