Changes between Version 18 and Version 19 of Introduction

Timestamp:

12/31/18 14:43:09 (7 years ago)

Author:

siegel

Comment:

--

Introduction

@@ -602 +602 @@
 === Verifying C/OpenMP Programs ===
 
-CIVL uses an input variable `omp_thread_max` for verifying OpenMP programs.   It must be specified on the command line.  Upon entering an OpenMP parallel region, CIVL will nondeterministically choose an integer between 1 and `omp_thread_max`, and create a thread team consisting of that number of threads.   If `omp_thread_max` is not specified, then the program must explicitly specify the number of threads for each parallel region.
-
-By default, CIVL attempts to simplify and OpenMP program by replacing parallel code with sequential code when it can determine that the two are equivalent.  In the best case, this can remove all of the OpenMP, resulting in a sequential program.   The option `-ompNoSimplify` can be used to disable such simplification.   Another option, `-ompLoopDecomp=X` can be used to specify the loop decomposition strategy, where `X` is one `ALL` (the default), `ROUND_ROBIN`, or `RANDOM`.
+CIVL uses an input variable `omp_thread_max` for verifying OpenMP programs.   It must be specified on the command line, e.g.,
+
+{{{
+civl verify -input_omp_thread_max=3 sum_omp.c
+}}}
+
+Upon entering an OpenMP parallel region, CIVL will nondeterministically choose an integer between 1 and `omp_thread_max`, and create a thread team consisting of that number of threads.   If `omp_thread_max` is not specified, then the program must explicitly specify the number of threads for each parallel region.
+
+By default, CIVL attempts to simplify an OpenMP program by replacing parallel code with sequential code when it can determine that the two are equivalent.  In the best case, this can remove all of the OpenMP, resulting in a sequential program.   The option `-ompNoSimplify` can be used to disable such simplification.   Another option, `-ompLoopDecomp=X` can be used to specify the loop decomposition strategy, where `X` is one `ALL` (the default), `ROUND_ROBIN`, or `RANDOM`.
+
+A serious limitation in the current OpenMP transformation is that access to shared variables cannot take place through pointers.
 
 === Verifying CUDA-C Programs ===