NAME: dotProduct1.c
CITE: \cite{LLNL:OpenMP:URL}
TYPE: $\text{O}$
SCALE: \texttt{NT$\leq,N=8}

files,language,blank,comment,code,"http://cloc.sourceforge.net v 1.62  T=0.01 s (101.9 files/s, 4990.8 lines/s)"
1,C,7,18,24
civl verify -ompLoopDecomp=ALL -input_omp_thread_max=3 -enablePrintf=false  dotProduct1.c
CIVL v1.3+ of 2015-07-23 -- http://vsl.cis.udel.edu/civl

=== Command ===
civl verify -ompLoopDecomp=ALL -input_omp_thread_max=3 -enablePrintf=false dotProduct1.c 

=== Stats ===
   time (s)            : 2.23
   memory (bytes)      : 914882560
   max process count   : 1
   states              : 124
   states saved        : 48
   state matches       : 0
   transitions         : 123
   trace steps         : 46
   valid calls         : 32
   provers             : z3, cvc4, cvc3
   prover calls        : 3

=== Result ===
The standard properties hold for all executions.
NAME: dotProduct{\U}critical.c
CITE: \cite{PP2012:OpenMP:URL}
TYPE: $\text{O}$
SCALE: \texttt{NT$\leq,N=100}

files,language,blank,comment,code,"http://cloc.sourceforge.net v 1.62  T=0.01 s (101.0 files/s, 6159.0 lines/s)"
1,C,15,11,35
civl verify -ompLoopDecomp=ALL -input_omp_thread_max=3 -enablePrintf=false  dotProduct_critical.c
CIVL v1.3+ of 2015-07-23 -- http://vsl.cis.udel.edu/civl
Thread 1 can't perform $omp_write because thread 0 has written to the same variable and hasn't flushed yet.


Violation 0 encountered at depth 1646:
CIVL execution violation in p3(id=2) (kind: ASSERTION_VIOLATION, certainty: PROVEABLE)
at civl-omp.cvl:239.2-240.26 "$assert(otherTid < 0,  ... )":

Input variables:
_gen_argc=X0
_gen_argv=(CHAR[10][])X1
_omp_thread_max=3

Context: 0<=SIZEOF(struct OMP_gteam)+-1 && 0<=SIZEOF(struct OMP_team)+-1 && 0<=SIZEOF(struct OMP_gshared)+-1 && 0<=SIZEOF(struct OMP_shared)+-1 && 0<=-1*X0+9 && 0<=X0+-1

Assertion: $assert((otherTid<0), &((_anon_4)[0]), (*(shared)).1, otherTid)
-> 0<0
-> false

Call stacks:

process p0 (id=0):
  _gen_main at OpenMPtoCIVLTransformer:0.-1-20 "$parfor(int _omp_t..." inserted by OpenMPtoCIVLTransformer.parallelPragma before op.h:21.1-10 "Operation" included from civlc.cvh:11.9-15 "<op.h>" included from omp.cvl:1.9-20 "<civlc.cvh>" called from
  _CIVL_system at GeneralTransformer:0.-1-20 "_gen_argc, &_gen_a..." inserted by GeneralTransformer.new main function before dotProduct_critical.c:19.14-18 "argc"

process p1 (id=1):
  $barrier_call at concurrency.cvl:60.2-15 "$barrier_exit" called from
  $omp_barrier_and_flush at civl-omp.cvl:311.2-15 "$barrier_call" called from
  _par_proc0 at OpenMPtoCIVLTransformer:0.-1-9 "_omp_team\n" inserted by OpenMPtoCIVLTransformer.barrierAndFlushCall before op.h:21.1-10 "Operation" included from civlc.cvh:11.9-15 "<op.h>" included from omp.cvl:1.9-20 "<civlc.cvh>"

process p3 (id=2):
  $omp_write at civl-omp.cvl:239.2-9 "$assert" called from
  _par_proc0 at OpenMPtoCIVLTransformer:0.-1-20 "_omp_tid_shared, &..." inserted by OpenMPtoCIVLTransformer.tid_sharedWriteCall before op.h:21.1-10 "Operation" included from civlc.cvh:11.9-15 "<op.h>" included from omp.cvl:1.9-20 "<civlc.cvh>"

Logging new entry 0, writing trace to CIVLREP/dotProduct_critical_0.trace
Terminating search after finding 1 violation.

=== Command ===
civl verify -ompLoopDecomp=ALL -input_omp_thread_max=3 -enablePrintf=false dotProduct_critical.c 

=== Stats ===
   time (s)            : 5.58
   memory (bytes)      : 915931136
   max process count   : 3
   states              : 23656
   states saved        : 11613
   state matches       : 0
   transitions         : 23656
   trace steps         : 11581
   valid calls         : 28248
   provers             : z3, cvc4, cvc3
   prover calls        : 7

=== Result ===
The program MAY NOT be correct.  See CIVLREP/dotProduct_critical_log.txt
NAME: matProduct1.c
CITE: \cite{LLNL:OpenMP:URL}
TYPE: $\text{O}$
SCALE: \texttt{NT$\leq,NRA=8,NCA=8,NCB=8}

files,language,blank,comment,code,"http://cloc.sourceforge.net v 1.62  T=0.01 s (95.9 files/s, 8915.7 lines/s)"
1,C,8,19,66
civl verify -ompLoopDecomp=ALL -input_omp_thread_max=3 -enablePrintf=false  matProduct1.c
CIVL v1.3+ of 2015-07-23 -- http://vsl.cis.udel.edu/civl

=== Command ===
civl verify -ompLoopDecomp=ALL -input_omp_thread_max=3 -enablePrintf=false matProduct1.c 

=== Stats ===
   time (s)            : 2.41
   memory (bytes)      : 914882560
   max process count   : 1
   states              : 651
   states saved        : 380
   state matches       : 0
   transitions         : 650
   trace steps         : 378
   valid calls         : 471
   provers             : z3, cvc4, cvc3
   prover calls        : 3

=== Result ===
The standard properties hold for all executions.
NAME: heated{\U}plate{\U}openmp.c
CITE: \cite{Quinn:Book04}
TYPE: $\text{O}$
SCALE: \texttt{NT$\leq,M=5,N=5,EPSILON=0.1}

files,language,blank,comment,code,"http://cloc.sourceforge.net v 1.62  T=0.01 s (83.5 files/s, 25461.0 lines/s)"
1,C,44,101,160
civl verify -ompLoopDecomp=ALL -input_omp_thread_max=3 -enablePrintf=false  -DMATH_ELABORATE_ASSUMPTIONS heated_plate_openmp.c
CIVL v1.3+ of 2015-07-23 -- http://vsl.cis.udel.edu/civl
19s: mem=1327Mb trans=112109 traceSteps=82350 explored=111553 saved=82141 prove=7

=== Command ===
civl verify -ompLoopDecomp=ALL -input_omp_thread_max=3 -enablePrintf=false -DMATH_ELABORATE_ASSUMPTIONS heated_plate_openmp.c 

=== Stats ===
   time (s)            : 33.42
   memory (bytes)      : 1125646336
   max process count   : 4
   states              : 228034
   states saved        : 166567
   state matches       : 1294
   transitions         : 229308
   trace steps         : 167175
   valid calls         : 472742
   provers             : z3, cvc4, cvc3
   prover calls        : 7

=== Result ===
The standard properties hold for all executions.
NAME: fig3.10-mxv-omp.c
CITE: \cite{chapman-etal:2008:using-openmp}
TYPE: $\text{O}$
SCALE: \texttt{NT$\leq,M=10,N=10}

files,language,blank,comment,code,"http://cloc.sourceforge.net v 1.62  T=0.01 s (96.1 files/s, 10959.2 lines/s)"
1,C,21,31,62
civl verify -ompLoopDecomp=ALL -input_omp_thread_max=3 -enablePrintf=false  fig310-mxv-omp.c
CIVL v1.3+ of 2015-07-23 -- http://vsl.cis.udel.edu/civl

=== Command ===
civl verify -ompLoopDecomp=ALL -input_omp_thread_max=3 -enablePrintf=false fig310-mxv-omp.c 

=== Stats ===
   time (s)            : 2.44
   memory (bytes)      : 914882560
   max process count   : 1
   states              : 821
   states saved        : 263
   state matches       : 0
   transitions         : 820
   trace steps         : 258
   valid calls         : 2047
   provers             : z3, cvc4, cvc3
   prover calls        : 4

=== Result ===
The standard properties hold for all executions.
NAME: quad{\U}openmp.c
CITE: \cite{Burkardt:OpenMP:URL}
TYPE: $\text{O}$
SCALE: \texttt{NT$\leq,N=100}

files,language,blank,comment,code,"http://cloc.sourceforge.net v 1.62  T=0.01 s (88.8 files/s, 19355.2 lines/s)"
1,C,67,60,91
civl verify -ompLoopDecomp=ALL -input_omp_thread_max=3 -enablePrintf=false  quad_openmp.c
CIVL v1.3+ of 2015-07-23 -- http://vsl.cis.udel.edu/civl

=== Command ===
civl verify -ompLoopDecomp=ALL -input_omp_thread_max=3 -enablePrintf=false quad_openmp.c 

=== Stats ===
   time (s)            : 13.04
   memory (bytes)      : 1397751808
   max process count   : 1
   states              : 8138
   states saved        : 1058
   state matches       : 0
   transitions         : 8137
   trace steps         : 1055
   valid calls         : 2035
   provers             : z3, cvc4, cvc3
   prover calls        : 5

=== Result ===
The standard properties hold for all executions.
NAME: pi.c
CITE: \cite{PP2012:OpenMP:URL}
TYPE: $\text{O}$
SCALE: \texttt{NT$\leq,N=100}

files,language,blank,comment,code,"http://cloc.sourceforge.net v 1.62  T=0.01 s (94.5 files/s, 9355.5 lines/s)"
1,C,14,15,70
civl verify -ompLoopDecomp=ALL -input_omp_thread_max=3 -enablePrintf=false  pi.c
CIVL v1.3+ of 2015-07-23 -- http://vsl.cis.udel.edu/civl

=== Command ===
civl verify -ompLoopDecomp=ALL -input_omp_thread_max=3 -enablePrintf=false pi.c 

=== Stats ===
   time (s)            : 10.42
   memory (bytes)      : 1367343104
   max process count   : 4
   states              : 44004
   states saved        : 24217
   state matches       : 86
   transitions         : 44088
   trace steps         : 24243
   valid calls         : 54705
   provers             : z3, cvc4, cvc3
   prover calls        : 10

=== Result ===
The standard properties hold for all executions.
NAME: heated{\U}plate{\U}openmp.c
CITE: \cite{Quinn:Book04}
TYPE: $\text{O}^r$
SCALE: \texttt{NT$\leq,M=5,N=5,EPSILON=0.1}

files,language,blank,comment,code,"http://cloc.sourceforge.net v 1.62  T=0.01 s (90.2 files/s, 27514.6 lines/s)"
1,C,44,101,160
civl verify -ompNoSimplify -ompLoopDecomp=ROUND_ROBIN -input_omp_thread_max=3 -enablePrintf=false  -DMATH_ELABORATE_ASSUMPTIONS heated_plate_openmp.c
CIVL v1.3+ of 2015-07-23 -- http://vsl.cis.udel.edu/civl
19s: mem=1326Mb trans=176189 traceSteps=66872 explored=174888 saved=65715 prove=8
34s: mem=1042Mb trans=448955 traceSteps=138314 explored=445117 saved=134718 prove=8
49s: mem=770Mb trans=714567 traceSteps=206818 explored=708178 saved=200700 prove=8
65s: mem=549Mb trans=967960 traceSteps=276419 explored=959249 saved=268072 prove=8
80s: mem=509Mb trans=1235069 traceSteps=346228 explored=1223877 saved=335497 prove=8
95s: mem=563Mb trans=1508519 traceSteps=415751 explored=1494706 saved=402432 prove=8

=== Command ===
civl verify -ompNoSimplify -ompLoopDecomp=ROUND_ROBIN -input_omp_thread_max=3 -enablePrintf=false -DMATH_ELABORATE_ASSUMPTIONS heated_plate_openmp.c 

=== Stats ===
   time (s)            : 103.07
   memory (bytes)      : 607125504
   max process count   : 4
   states              : 1684918
   states saved        : 442754
   state matches       : 15607
   transitions         : 1700505
   trace steps         : 457774
   valid calls         : 1135138
   provers             : z3, cvc4, cvc3
   prover calls        : 8

=== Result ===
The standard properties hold for all executions.
NAME: omp{\U}bug5.c
CITE: \cite{LLNL:OpenMP:URL}
TYPE: $\text{O}$
SCALE: \texttt{NT$\leq,N=10}

files,language,blank,comment,code,"http://cloc.sourceforge.net v 1.62  T=0.01 s (94.0 files/s, 7521.6 lines/s)"
1,C,8,18,54
civl verify -ompLoopDecomp=ALL -input_omp_thread_max=3 -enablePrintf=false  omp_bug5.c
CIVL v1.3+ of 2015-07-23 -- http://vsl.cis.udel.edu/civl
Thread 1 can't perform $omp_write because thread 0 has written to the same variable and hasn't flushed yet.


Violation 0 encountered at depth 782:
CIVL execution violation in p3(id=2) (kind: ASSERTION_VIOLATION, certainty: PROVEABLE)
at civl-omp.cvl:239.2-240.26 "$assert(otherTid < 0,  ... )":

Input variables:
_gen_argc=X0
_gen_argv=(CHAR[10][])X1
_omp_thread_max=3

Context: 0<=SIZEOF(struct OMP_gteam)+-1 && 0<=SIZEOF(struct OMP_team)+-1 && 0<=SIZEOF(struct OMP_gshared)+-1 && 0<=SIZEOF(struct OMP_shared)+-1 && 0<=-1*X0+9 && 0<=X0+-1

Assertion: $assert((otherTid<0), &((_anon_3)[0]), (*(shared)).1, otherTid)
-> 0<0
-> false

Call stacks:

process p0 (id=0):
  _gen_main at OpenMPtoCIVLTransformer:0.-1-20 "$parfor(int _omp_t..." inserted by OpenMPtoCIVLTransformer.parallelPragma before op.h:21.1-10 "Operation" included from civlc.cvh:11.9-15 "<op.h>" included from omp.cvl:1.9-20 "<civlc.cvh>" called from
  _CIVL_system at GeneralTransformer:0.-1-20 "_gen_argc, &_gen_a..." inserted by GeneralTransformer.new main function before omp_bug5.c:23.14-18 "argc"

process p1 (id=1):
  $omp_write at civl-omp.cvl:236.2-9 "$atomic" called from
  _par_proc0 at OpenMPtoCIVLTransformer:0.-1-20 "_omp_a_shared, &_o..." inserted by OpenMPtoCIVLTransformer.a_sharedWriteCall before op.h:21.1-10 "Operation" included from civlc.cvh:11.9-15 "<op.h>" included from omp.cvl:1.9-20 "<civlc.cvh>"

process p3 (id=2):
  $omp_write at civl-omp.cvl:239.2-9 "$assert" called from
  _par_proc0 at OpenMPtoCIVLTransformer:0.-1-20 "_omp_i_shared, &_o..." inserted by OpenMPtoCIVLTransformer.i_sharedWriteCall before op.h:21.1-10 "Operation" included from civlc.cvh:11.9-15 "<op.h>" included from omp.cvl:1.9-20 "<civlc.cvh>"

Logging new entry 0, writing trace to CIVLREP/omp_bug5_0.trace
Terminating search after finding 1 violation.

=== Command ===
civl verify -ompLoopDecomp=ALL -input_omp_thread_max=3 -enablePrintf=false omp_bug5.c 

=== Stats ===
   time (s)            : 3.66
   memory (bytes)      : 915931136
   max process count   : 3
   states              : 2647
   states saved        : 1277
   state matches       : 5
   transitions         : 2652
   trace steps         : 1255
   valid calls         : 3035
   provers             : z3, cvc4, cvc3
   prover calls        : 7

=== Result ===
The program MAY NOT be correct.  See CIVLREP/omp_bug5_log.txt
