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

files,language,blank,comment,code,"http://cloc.sourceforge.net v 1.62  T=0.01 s (181.4 files/s, 7438.3 lines/s)"
1,C,5,18,18
civl verify -ompLoopDecomp=ALL -inputTHREAD_MAX=3 -enablePrintf=false  dotProduct1.c
CIVL v0.16 of 2015-1-6 -- http://vsl.cis.udel.edu/civl

=================== Stats ===================
   validCalls          : 85
   proverCalls         : 3
   memory (bytes)      : 650117120
   time (s)            : 1.85
   maxProcs            : 1
   statesInstantiated  : 411
   statesSaved         : 76
   statesSeen          : 75
   statesMatched       : 0
   steps               : 121
   transitions         : 74

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

files,language,blank,comment,code,"http://cloc.sourceforge.net v 1.62  T=0.02 s (66.3 files/s, 3445.1 lines/s)"
1,C,12,11,29
civl verify -ompLoopDecomp=ALL -inputTHREAD_MAX=3 -enablePrintf=false  dotProduct_critical.c
CIVL v0.16 of 2015-1-6 -- 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.

Error 0 encountered at depth 2361:
CIVL execution error in p3(id=2) (kind: ASSERTION_VIOLATION, certainty: PROVEABLE)
Cannot prove assertion holds: $assert (otherTid<0)
  Path condition: (0 <= SIZEOF(dynamicType<235>)+-1) && (0 <= SIZEOF(dynamicType<243>)+-1) && (0 <= SIZEOF(dynamicType<248>)+-1) && (0 <= SIZEOF(dynamicType<253>)+-1) && (0 <= -1*X3+9) && (0 <= X3+-1)
  Assertion: false

at civl-omp.cvl:243.2-245.25 "$assert otherTid < 0 : ... otherTid".
State -1:137588
| Path condition
| | (0 <= SIZEOF(dynamicType<235>)+-1) && (0 <= SIZEOF(dynamicType<243>)+-1) && (0 <= SIZEOF(dynamicType<248>)+-1) && (0 <= SIZEOF(dynamicType<253>)+-1) && (0 <= -1*X3+9) && (0 <= X3+-1)
| Dynamic scopes
| | dyscope d0 (id=0, parent=NULL, static=0)
| | | variables
| | | | _atomic_lock_var = p3
| | | | _time_count_var = 0
| | | | CIVL_argc = X3
| | | | CIVL_argv = X4
| | | | THREAD_MAX = 3
| | | | _critical_noname = false
| | | | $omp_numThreads = 3
| | dyscope d3 (id=1, parent=d1, static=46)
| | | variables
| | | | _heap = 
| | | | | objects of malloc 0 at civl-omp.cvl:72.13-74 "result = ($omp_gteam)$malloc( ... )":
| | | | | | 0: (OMP_gteam[1])<OMP_gteam<d3,2,(boolean[2])<true,true>,(OMP_work_record[1][])<(OMP_work_record[2])<V4[0]<0:=3, 1:=0, 2:=true>,V4[1]<0:=3, 1:=0, 2:=false>>>,(pointer[0])>,&<d3>heap<4,0>[0]>>
| | | | | objects of malloc 2 at civl-omp.cvl:127.15-128.67 "result =\n    ($omp_gshared)$malloc ... )":
| | | | | | 0: (OMP_gshared[1])<OMP_gshared<2,(boolean[2])<false,false>,(pointer[2])<&<d18>heap<3,0>[0],&<d5432>heap<3,0>[0]>,&<d1>a>>
| | | | | | 1: (OMP_gshared[1])<OMP_gshared<2,(boolean[2])<false,false>,(pointer[2])<&<d18>heap<3,1>[0],&<d5432>heap<3,1>[0]>,&<d1>b>>
| | | | | | 2: (OMP_gshared[1])<OMP_gshared<2,(boolean[2])<false,false>,(pointer[2])<&<d18>heap<3,2>[0],&<d5432>heap<3,2>[0]>,&<d1>sum>>
| | | | | | 3: (OMP_gshared[1])<OMP_gshared<2,(boolean[2])<false,false>,(pointer[2])<&<d18>heap<3,3>[0],&<d5432>heap<3,3>[0]>,&<d1>tid>>
| | | | | | 4: (OMP_gshared[1])<OMP_gshared<2,(boolean[2])<false,false>,(pointer[2])<&<d18>heap<3,4>[0],&<d5432>heap<3,4>[0]>,&<d1>nthreads>>
| | | | | objects of malloc 4:
| | | | | | 0: (__gbarrier__[1])<__gbarrier__<2,(process[2])<p1,p3>,(boolean[2])<true,false>,1>>
| | | | _nthreads = 2
| | | | thread_range = $regular_range<0,1,1>
| | | | dom = $domain<1,0,inject(0,($regular_range[1])<$regular_range<0,1,1>>)>
| | | | gteam = &<d3>heap<0,0>[0]
| | | | a_gshared = &<d3>heap<2,0>[0]
| | | | b_gshared = &<d3>heap<2,1>[0]
| | | | sum_gshared = &<d3>heap<2,2>[0]
| | | | tid_gshared = &<d3>heap<2,3>[0]
| | | | nthreads_gshared = &<d3>heap<2,4>[0]
| | | | _dom_size0 = 2
| | | | _par_procs0 = (process[2])<p1,p3>
| | dyscope d1 (id=2, parent=d0, static=44)
| | | variables
| | | | _argv = (pointer[10])<&<d0>CIVL_argv[0][0],&<d0>CIVL_argv[1][0],&<d0>CIVL_argv[2][0],&<d0>CIVL_argv[3][0],&<d0>CIVL_argv[4][0],&<d0>CIVL_argv[5][0],&<d0>CIVL_argv[6][0],&<d0>CIVL_argv[7][0],&<d0>CIVL_argv[8][0],&<d0>CIVL_argv[9][0]>
| | | | argv = &<d1>_argv[0]
| | | | a = V0
| | | | b = V1
| | | | sum = 0
| | | | tid = NULL
| | | | nthreads = NULL
| | | | _anon_0 = NULL
| | dyscope d48 (id=3, parent=d31, static=93)
| | | variables
| | | | owner = 0
| | dyscope d31 (id=4, parent=d18, static=91)
| | | variables
| | | | tmpWrite0 = 0
| | dyscope d18 (id=5, parent=d17, static=90)
| | | variables
| | | | _heap = 
| | | | | objects of malloc 1 at civl-omp.cvl:96.12-71 "result = ($omp_team)$malloc( ... )":
| | | | | | 0: (OMP_team[1])<OMP_team<&<d3>heap<0,0>[0],d18,0,(pointer[5])<&<d18>heap<3,0>[0],&<d18>heap<3,1>[0],&<d18>heap<3,2>[0],&<d18>heap<3,3>[0],&<d18>heap<3,4>[0]>,&<d18>heap<5,0>[0]>>
| | | | | objects of malloc 3 at civl-omp.cvl:149.14-150.64 "result =\n    ($omp_shared)$malloc ... )":
| | | | | | 0: (OMP_shared[1])<OMP_shared<&<d3>heap<2,0>[0],0,&<d18>a_local,&<d18>a_status>>
| | | | | | 1: (OMP_shared[1])<OMP_shared<&<d3>heap<2,1>[0],0,&<d18>b_local,&<d18>b_status>>
| | | | | | 2: (OMP_shared[1])<OMP_shared<&<d3>heap<2,2>[0],0,&<d18>sum_local,&<d18>sum_status>>
| | | | | | 3: (OMP_shared[1])<OMP_shared<&<d3>heap<2,3>[0],0,&<d18>tid_local,&<d18>tid_status>>
| | | | | | 4: (OMP_shared[1])<OMP_shared<&<d3>heap<2,4>[0],0,&<d18>nthreads_local,&<d18>nthreads_status>>
| | | | | objects of malloc 5:
| | | | | | 0: (__barrier__[1])<__barrier__<0,&<d3>heap<4,0>[0]>>
| | | | team = &<d18>heap<1,0>[0]
| | | | a_local = (real[100])<0,1,2,3,4,5,6,7,8,9,10,11,12,13,14,15,16,17,18,19,20,21,22,23,24,25,26,27,28,29,30,31,32,33,34,35,36,37,38,39,40,41,42,43,44,45,46,47,48,49,50,51,52,53,54,55,56,57,58,59,60,61,62,63,64,65,66,67,68,69,70,71,72,73,74,75,76,77,78,79,80,81,82,83,84,85,86,87,88,89,90,91,92,93,94,95,96,97,98,99>
| | | | a_status = (int[100])<2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2>
| | | | b_local = (real[100])<0,1,2,3,4,5,6,7,8,9,10,11,12,13,14,15,16,17,18,19,20,21,22,23,24,25,26,27,28,29,30,31,32,33,34,35,36,37,38,39,40,41,42,43,44,45,46,47,48,49,50,51,52,53,54,55,56,57,58,59,60,61,62,63,64,65,66,67,68,69,70,71,72,73,74,75,76,77,78,79,80,81,82,83,84,85,86,87,88,89,90,91,92,93,94,95,96,97,98,99>
| | | | b_status = (int[100])<2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2>
| | | | sum_local = 0
| | | | sum_status = 1
| | | | tid_local = 0
| | | | tid_status = 2
| | | | nthreads_local = 2
| | | | nthreads_status = 2
| | | | a_shared = &<d18>heap<3,0>[0]
| | | | b_shared = &<d18>heap<3,1>[0]
| | | | sum_shared = &<d18>heap<3,2>[0]
| | | | tid_shared = &<d18>heap<3,3>[0]
| | | | nthreads_shared = &<d18>heap<3,4>[0]
| | | | localsum$omp_private = NULL
| | dyscope d17 (id=6, parent=d3, static=49)
| | | variables
| | | | _tid = 0
| | dyscope d1752 (id=7, parent=d0, static=38)
| | | variables
| | | | team = &<d18>heap<1,0>[0]
| | dyscope d1753 (id=8, parent=d0, static=22)
| | | variables
| | | | barrier = &<d18>heap<5,0>[0]
| | dyscope d5459 (id=9, parent=d5432, static=91)
| | | variables
| | | | tmpWrite0 = 1
| | dyscope d5432 (id=10, parent=d5431, static=90)
| | | variables
| | | | _heap = 
| | | | | objects of malloc 1 at civl-omp.cvl:96.12-71 "result = ($omp_team)$malloc( ... )":
| | | | | | 0: (OMP_team[1])<OMP_team<&<d3>heap<0,0>[0],d5432,1,(pointer[5])<&<d5432>heap<3,0>[0],&<d5432>heap<3,1>[0],&<d5432>heap<3,2>[0],&<d5432>heap<3,3>[0],&<d5432>heap<3,4>[0]>,&<d5432>heap<5,0>[0]>>
| | | | | objects of malloc 3 at civl-omp.cvl:149.14-150.64 "result =\n    ($omp_shared)$malloc ... )":
| | | | | | 0: (OMP_shared[1])<OMP_shared<&<d3>heap<2,0>[0],1,&<d5432>a_local,&<d5432>a_status>>
| | | | | | 1: (OMP_shared[1])<OMP_shared<&<d3>heap<2,1>[0],1,&<d5432>b_local,&<d5432>b_status>>
| | | | | | 2: (OMP_shared[1])<OMP_shared<&<d3>heap<2,2>[0],1,&<d5432>sum_local,&<d5432>sum_status>>
| | | | | | 3: (OMP_shared[1])<OMP_shared<&<d3>heap<2,3>[0],1,&<d5432>tid_local,&<d5432>tid_status>>
| | | | | | 4: (OMP_shared[1])<OMP_shared<&<d3>heap<2,4>[0],1,&<d5432>nthreads_local,&<d5432>nthreads_status>>
| | | | | objects of malloc 5:
| | | | | | 0: (__barrier__[1])<__barrier__<1,&<d3>heap<4,0>[0]>>
| | | | team = &<d5432>heap<1,0>[0]
| | | | a_local = V0
| | | | a_status = (int[100])<1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1>
| | | | b_local = V1
| | | | b_status = (int[100])<1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1>
| | | | sum_local = 0
| | | | sum_status = 1
| | | | tid_local = NULL
| | | | tid_status = 1
| | | | nthreads_local = NULL
| | | | nthreads_status = 1
| | | | a_shared = &<d5432>heap<3,0>[0]
| | | | b_shared = &<d5432>heap<3,1>[0]
| | | | sum_shared = &<d5432>heap<3,2>[0]
| | | | tid_shared = &<d5432>heap<3,3>[0]
| | | | nthreads_shared = &<d5432>heap<3,4>[0]
| | | | localsum$omp_private = NULL
| | dyscope d5431 (id=11, parent=d3, static=49)
| | | variables
| | | | _tid = 1
| | dyscope d7991 (id=12, parent=d5460, static=67)
| | | variables
| | | | otherTid = 0
| | | | _anon_5 = "Thread %d can't perform $omp_write because thread %d has written to the same variable and hasn't flushed yet.\n"
| | dyscope d5460 (id=13, parent=d0, static=35)
| | | variables
| | | | shared = &<d5432>heap<3,3>[0]
| | | | ref = &<d5432>tid_local
| | | | value = &<d5459>tmpWrite0
| | dyscope d7995 (id=14, parent=d7994, static=58)
| | | variables
| | | | other = &<d18>heap<3,3>[0]
| | | | segFault = true
| | dyscope d7994 (id=15, parent=d7993, static=57)
| | | variables
| | | | i = 0
| | dyscope d7993 (id=16, parent=d7992, static=56)
| | | variables
| | | | tid = 1
| | | | gshared = &<d3>heap<2,3>[0]
| | | | nthreads = 2
| | | | isIdentityRef = true
| | dyscope d7992 (id=17, parent=d0, static=33)
| | | variables
| | | | shared = &<d5432>heap<3,3>[0]
| | | | ref = &<d5432>tid_local
| Process states
| | process p0(id=0)
| | | call stack
| | | | Frame[function=_CIVL_system, location=24, OpenMPtoCIVLTransformer:0.-1-20 "$parfor(int _tid: ..." inserted by OpenMPtoCIVLTransformer.parallelPragmabefore op.h:22.1-10 "Operation" included from civlc.cvh:12.9-15 "<op.h>" included from omp.cvl:1.9-20 "<civlc.cvh>", dyscope=d3]
| | process p1(id=1)
| | | call stack
| | | | Frame[function=$barrier_call, location=38, concurrency.cvl:41.2-15 "$barrier_exit", dyscope=d1753]
| | | | Frame[function=$omp_barrier_and_flush, location=174, civl-omp.cvl:316.2-15 "$barrier_call", dyscope=d1752]
| | | | Frame[function=_par_proc0, location=273, OpenMPtoCIVLTransformer:0.-1-4 "team\n" inserted by OpenMPtoCIVLTransformer.barrierAndFlushCallbefore op.h:22.1-10 "Operation" included from civlc.cvh:12.9-15 "<op.h>" included from omp.cvl:1.9-20 "<civlc.cvh>", dyscope=d48]
| | process p3(id=2)
| | | call stack
| | | | Frame[function=$omp_write, location=138, civl-omp.cvl:243.2-9 "$assert", dyscope=d7991]
| | | | Frame[function=_par_proc0, location=257, OpenMPtoCIVLTransformer:0.-1-20 "tid_shared, &tid_l..." inserted by OpenMPtoCIVLTransformer.tid_sharedWriteCallbefore op.h:22.1-10 "Operation" included from civlc.cvh:12.9-15 "<op.h>" included from omp.cvl:1.9-20 "<civlc.cvh>", dyscope=d5459]

Logging new entry 0, writing trace to CIVLREP/dotProduct_critical_0.trace

Error bound exceeded: search terminated

=================== Stats ===================
   validCalls          : 42965
   proverCalls         : 10
   memory (bytes)      : 914882560
   time (s)            : 6.72
   maxProcs            : 3
   statesInstantiated  : 137589
   statesSaved         : 13783
   statesSeen          : 13752
   statesMatched       : 0
   steps               : 24427
   transitions         : 13751

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=3,NRA=8,NCA=8,NCB=8}

files,language,blank,comment,code,"http://cloc.sourceforge.net v 1.62  T=0.01 s (170.0 files/s, 13773.0 lines/s)"
1,C,7,19,55
civl verify -ompLoopDecomp=ALL -inputTHREAD_MAX=3 -enablePrintf=false  matProduct1.c
CIVL v0.16 of 2015-1-6 -- http://vsl.cis.udel.edu/civl

=================== Stats ===================
   validCalls          : 5188
   proverCalls         : 3
   memory (bytes)      : 650117120
   time (s)            : 2.23
   maxProcs            : 1
   statesInstantiated  : 9388
   statesSaved         : 1798
   statesSeen          : 1797
   statesMatched       : 0
   steps               : 2886
   transitions         : 1796

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

files,language,blank,comment,code,"http://cloc.sourceforge.net v 1.62  T=0.01 s (66.8 files/s, 20033.3 lines/s)"
1,C,44,106,150
civl verify -ompLoopDecomp=ALL -inputTHREAD_MAX=3 -enablePrintf=false  -DMATH_ELABORATE_ASSUMPTIONS heated_plate_openmp.c
CIVL v0.16 of 2015-1-6 -- http://vsl.cis.udel.edu/civl
18s: mem=1333Mb steps=80753 trans=70142 seen=69942 saved=70135 prove=12
33s: mem=1185Mb steps=165085 trans=142864 seen=142442 saved=142787 prove=12

=================== Stats ===================
   validCalls          : 567068
   proverCalls         : 12
   memory (bytes)      : 1205338112
   time (s)            : 35.48
   maxProcs            : 4
   statesInstantiated  : 1438162
   statesSaved         : 155151
   statesSeen          : 154790
   statesMatched       : 440
   steps               : 179235
   transitions         : 155229

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=3,M=10,N=10}

files,language,blank,comment,code,"http://cloc.sourceforge.net v 1.62  T=0.01 s (67.3 files/s, 6660.4 lines/s)"
1,C,20,36,43
civl verify -ompLoopDecomp=ALL -inputTHREAD_MAX=3 -enablePrintf=false  fig310-mxv-omp.c
CIVL v0.16 of 2015-1-6 -- http://vsl.cis.udel.edu/civl

=================== Stats ===================
   validCalls          : 2521
   proverCalls         : 5
   memory (bytes)      : 650117120
   time (s)            : 2.17
   maxProcs            : 1
   statesInstantiated  : 3605
   statesSaved         : 515
   statesSeen          : 511
   statesMatched       : 0
   steps               : 786
   transitions         : 510

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

files,language,blank,comment,code,"http://cloc.sourceforge.net v 1.62  T=0.01 s (69.3 files/s, 14477.7 lines/s)"
1,C,67,60,82
civl verify -ompLoopDecomp=ALL -inputTHREAD_MAX=3 -enablePrintf=false  quad_openmp.c
CIVL v0.16 of 2015-1-6 -- http://vsl.cis.udel.edu/civl

=================== Stats ===================
   validCalls          : 436
   proverCalls         : 5
   memory (bytes)      : 921174016
   time (s)            : 3.04
   maxProcs            : 1
   statesInstantiated  : 3216
   statesSaved         : 261
   statesSeen          : 259
   statesMatched       : 0
   steps               : 920
   transitions         : 258

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

files,language,blank,comment,code,"http://cloc.sourceforge.net v 1.62  T=0.01 s (68.8 files/s, 6054.0 lines/s)"
1,C,14,31,43
civl verify -ompLoopDecomp=ALL -inputTHREAD_MAX=3 -enablePrintf=false  pi.c
CIVL v0.16 of 2015-1-6 -- http://vsl.cis.udel.edu/civl

=================== Stats ===================
   validCalls          : 56835
   proverCalls         : 13
   memory (bytes)      : 1399324672
   time (s)            : 9.98
   maxProcs            : 4
   statesInstantiated  : 251850
   statesSaved         : 20841
   statesSeen          : 20785
   statesMatched       : 65
   steps               : 41151
   transitions         : 20849

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=3,M=5,N=5,EPSILON=0.1}

files,language,blank,comment,code,"http://cloc.sourceforge.net v 1.62  T=0.02 s (64.0 files/s, 19192.7 lines/s)"
1,C,44,106,150
civl verify -ompNoSimplify -ompLoopDecomp=ROUND_ROBIN -inputTHREAD_MAX=3 -enablePrintf=false  -DMATH_ELABORATE_ASSUMPTIONS heated_plate_openmp.c
CIVL v0.16 of 2015-1-6 -- http://vsl.cis.udel.edu/civl
19s: mem=1332Mb steps=132146 trans=65983 seen=65191 saved=65309 prove=16
34s: mem=1182Mb steps=315952 trans=135699 seen=133323 saved=133491 prove=16
49s: mem=963Mb steps=520337 trans=203833 seen=199556 saved=199752 prove=16
64s: mem=726Mb steps=709259 trans=273275 seen=267371 saved=267587 prove=16
79s: mem=557Mb steps=849231 trans=331384 seen=324409 saved=324674 prove=16
94s: mem=496Mb steps=967072 trans=367826 seen=359696 saved=359962 prove=16
109s: mem=474Mb steps=1083291 trans=403846 seen=394594 saved=394859 prove=16
124s: mem=560Mb steps=1205342 trans=441943 seen=431555 saved=431842 prove=16

=================== Stats ===================
   validCalls          : 1449767
   proverCalls         : 16
   memory (bytes)      : 579338240
   time (s)            : 128.43
   maxProcs            : 4
   statesInstantiated  : 6503538
   statesSaved         : 451329
   statesSeen          : 451022
   statesMatched       : 10753
   steps               : 1255764
   transitions         : 461774

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

files,language,blank,comment,code,"http://cloc.sourceforge.net v 1.62  T=0.01 s (68.4 files/s, 5469.7 lines/s)"
1,C,8,18,54
civl verify -ompLoopDecomp=ALL -inputTHREAD_MAX=3 -enablePrintf=false  omp_bug5.c
CIVL v0.16 of 2015-1-6 -- 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.

Error 0 encountered at depth 1101:
CIVL execution error in p3(id=2) (kind: ASSERTION_VIOLATION, certainty: PROVEABLE)
Cannot prove assertion holds: $assert (otherTid<0)
  Path condition: (0 <= SIZEOF(dynamicType<237>)+-1) && (0 <= SIZEOF(dynamicType<245>)+-1) && (0 <= SIZEOF(dynamicType<250>)+-1) && (0 <= SIZEOF(dynamicType<255>)+-1) && (0 <= -1*X3+9) && (0 <= X3+-1)
  Assertion: false

at civl-omp.cvl:243.2-245.25 "$assert otherTid < 0 : ... otherTid".
State -1:119141
| Path condition
| | (0 <= SIZEOF(dynamicType<237>)+-1) && (0 <= SIZEOF(dynamicType<245>)+-1) && (0 <= SIZEOF(dynamicType<250>)+-1) && (0 <= SIZEOF(dynamicType<255>)+-1) && (0 <= -1*X3+9) && (0 <= X3+-1)
| Dynamic scopes
| | dyscope d0 (id=0, parent=NULL, static=0)
| | | variables
| | | | _atomic_lock_var = p3
| | | | _time_count_var = 0
| | | | CIVL_argc = X3
| | | | CIVL_argv = X4
| | | | THREAD_MAX = 3
| | | | $omp_numThreads = 3
| | dyscope d5 (id=1, parent=d1, static=47)
| | | variables
| | | | _heap = 
| | | | | objects of malloc 0 at civl-omp.cvl:72.13-74 "result = ($omp_gteam)$malloc( ... )":
| | | | | | 0: (OMP_gteam[1])<OMP_gteam<d5,2,(boolean[2])<true,true>,(OMP_work_record[0][])>,(pointer[0])>,&<d5>heap<4,0>[0]>>
| | | | | objects of malloc 2 at civl-omp.cvl:127.15-128.67 "result =\n    ($omp_gshared)$malloc ... )":
| | | | | | 0: (OMP_gshared[1])<OMP_gshared<2,(boolean[2])<false,false>,(pointer[2])<&<d18>heap<3,0>[0],&<d1771>heap<3,0>[0]>,&<d1>a>>
| | | | | | 1: (OMP_gshared[1])<OMP_gshared<2,(boolean[2])<false,false>,(pointer[2])<&<d18>heap<3,1>[0],&<d1771>heap<3,1>[0]>,&<d1>b>>
| | | | | | 2: (OMP_gshared[1])<OMP_gshared<2,(boolean[2])<false,false>,(pointer[2])<&<d18>heap<3,2>[0],&<d1771>heap<3,2>[0]>,&<d1>nthreads>>
| | | | | | 3: (OMP_gshared[1])<OMP_gshared<2,(boolean[2])<false,false>,(pointer[2])<&<d18>heap<3,3>[0],&<d1771>heap<3,3>[0]>,&<d1>i>>
| | | | | objects of malloc 4:
| | | | | | 0: (__gbarrier__[1])<__gbarrier__<2,(process[2])<p1,p3>,(boolean[2])<false,false>,0>>
| | | | _nthreads = 2
| | | | thread_range = $regular_range<0,1,1>
| | | | dom = $domain<1,0,inject(0,($regular_range[1])<$regular_range<0,1,1>>)>
| | | | gteam = &<d5>heap<0,0>[0]
| | | | a_gshared = &<d5>heap<2,0>[0]
| | | | b_gshared = &<d5>heap<2,1>[0]
| | | | nthreads_gshared = &<d5>heap<2,2>[0]
| | | | i_gshared = &<d5>heap<2,3>[0]
| | | | _dom_size0 = 2
| | | | _par_procs0 = (process[2])<p1,p3>
| | dyscope d1 (id=2, parent=d0, static=45)
| | | variables
| | | | _argv = (pointer[10])<&<d0>CIVL_argv[0][0],&<d0>CIVL_argv[1][0],&<d0>CIVL_argv[2][0],&<d0>CIVL_argv[3][0],&<d0>CIVL_argv[4][0],&<d0>CIVL_argv[5][0],&<d0>CIVL_argv[6][0],&<d0>CIVL_argv[7][0],&<d0>CIVL_argv[8][0],&<d0>CIVL_argv[9][0]>
| | | | argv = &<d1>_argv[0]
| | | | nthreads = 2
| | | | i = NULL
| | | | a = V0
| | | | b = V1
| | | | locka = omp_lock_t<true>
| | | | lockb = omp_lock_t<true>
| | dyscope d130 (id=3, parent=d127, static=95)
| | | variables
| | | | i$omp = 0
| | | | __LiteralDomain_counter0__ = NULL
| | | | _anon_14 = "Thread %d initializing a[]\n"
| | | | _anon_15 = NULL
| | | | _anon_16 = NULL
| | | | _anon_17 = NULL
| | dyscope d127 (id=4, parent=d18, static=94)
| | | variables
| | | | my_secs = $domain<1,0,inject(0,($regular_range[1])<$regular_range<0,1,2>>)>
| | dyscope d18 (id=5, parent=d17, static=92)
| | | variables
| | | | _heap = 
| | | | | objects of malloc 1 at civl-omp.cvl:96.12-71 "result = ($omp_team)$malloc( ... )":
| | | | | | 0: (OMP_team[1])<OMP_team<&<d5>heap<0,0>[0],d18,0,(pointer[4])<&<d18>heap<3,0>[0],&<d18>heap<3,1>[0],&<d18>heap<3,2>[0],&<d18>heap<3,3>[0]>,&<d18>heap<5,0>[0]>>
| | | | | objects of malloc 3 at civl-omp.cvl:149.14-150.64 "result =\n    ($omp_shared)$malloc ... )":
| | | | | | 0: (OMP_shared[1])<OMP_shared<&<d5>heap<2,0>[0],0,&<d18>a_local,&<d18>a_status>>
| | | | | | 1: (OMP_shared[1])<OMP_shared<&<d5>heap<2,1>[0],0,&<d18>b_local,&<d18>b_status>>
| | | | | | 2: (OMP_shared[1])<OMP_shared<&<d5>heap<2,2>[0],0,&<d18>nthreads_local,&<d18>nthreads_status>>
| | | | | | 3: (OMP_shared[1])<OMP_shared<&<d5>heap<2,3>[0],0,&<d18>i_local,&<d18>i_status>>
| | | | | objects of malloc 5:
| | | | | | 0: (__barrier__[1])<__barrier__<0,&<d5>heap<4,0>[0]>>
| | | | team = &<d18>heap<1,0>[0]
| | | | a_local = (real[10])<0,283185307/20000000000,283185307/10000000000,849555921/20000000000,283185307/5000000000,283185307/4000000000,849555921/10000000000,1982297149/20000000000,283185307/2500000000,2548667763/20000000000>
| | | | a_status = (int[10])<2,2,2,2,2,2,2,2,2,2>
| | | | b_local = (real[10])<0,0,0,0,0,0,0,0,0,0>
| | | | b_status = (int[10])<0,0,0,0,0,0,0,0,0,0>
| | | | nthreads_local = 0
| | | | nthreads_status = 0
| | | | i_local = 10
| | | | i_status = 2
| | | | a_shared = &<d18>heap<3,0>[0]
| | | | b_shared = &<d18>heap<3,1>[0]
| | | | nthreads_shared = &<d18>heap<3,2>[0]
| | | | i_shared = &<d18>heap<3,3>[0]
| | | | tid$omp_private = 0
| | | | _anon_13 = "Thread %d starting...\n"
| | dyscope d17 (id=6, parent=d5, static=50)
| | | variables
| | | | _tid = 0
| | dyscope d377 (id=7, parent=d0, static=6)
| | | variables
| | | | slock = &<d1>lockb
| | | | team = &<d18>heap<1,0>[0]
| | dyscope d4251 (id=8, parent=d2897, static=100)
| | | variables
| | | | tmpWrite5 = 0
| | | | tmpRead4 = NULL
| | dyscope d2897 (id=9, parent=d1982, static=95)
| | | variables
| | | | i$omp = 1
| | | | __LiteralDomain_counter0__ = NULL
| | | | _anon_14 = NULL
| | | | _anon_15 = NULL
| | | | _anon_16 = "Thread %d initializing b[]\n"
| | | | _anon_17 = NULL
| | dyscope d1982 (id=10, parent=d1771, static=94)
| | | variables
| | | | my_secs = $domain<1,0,inject(0,($regular_range[1])<$regular_range<1,1,2>>)>
| | dyscope d1771 (id=11, parent=d1770, static=92)
| | | variables
| | | | _heap = 
| | | | | objects of malloc 1 at civl-omp.cvl:96.12-71 "result = ($omp_team)$malloc( ... )":
| | | | | | 0: (OMP_team[1])<OMP_team<&<d5>heap<0,0>[0],d1771,1,(pointer[4])<&<d1771>heap<3,0>[0],&<d1771>heap<3,1>[0],&<d1771>heap<3,2>[0],&<d1771>heap<3,3>[0]>,&<d1771>heap<5,0>[0]>>
| | | | | objects of malloc 3 at civl-omp.cvl:149.14-150.64 "result =\n    ($omp_shared)$malloc ... )":
| | | | | | 0: (OMP_shared[1])<OMP_shared<&<d5>heap<2,0>[0],1,&<d1771>a_local,&<d1771>a_status>>
| | | | | | 1: (OMP_shared[1])<OMP_shared<&<d5>heap<2,1>[0],1,&<d1771>b_local,&<d1771>b_status>>
| | | | | | 2: (OMP_shared[1])<OMP_shared<&<d5>heap<2,2>[0],1,&<d1771>nthreads_local,&<d1771>nthreads_status>>
| | | | | | 3: (OMP_shared[1])<OMP_shared<&<d5>heap<2,3>[0],1,&<d1771>i_local,&<d1771>i_status>>
| | | | | objects of malloc 5:
| | | | | | 0: (__barrier__[1])<__barrier__<1,&<d5>heap<4,0>[0]>>
| | | | team = &<d1771>heap<1,0>[0]
| | | | a_local = (real[10])<0,0,0,0,0,0,0,0,0,0>
| | | | a_status = (int[10])<0,0,0,0,0,0,0,0,0,0>
| | | | b_local = (real[10])<0,0,0,0,0,0,0,0,0,0>
| | | | b_status = (int[10])<0,0,0,0,0,0,0,0,0,0>
| | | | nthreads_local = 0
| | | | nthreads_status = 0
| | | | i_local = 0
| | | | i_status = 0
| | | | a_shared = &<d1771>heap<3,0>[0]
| | | | b_shared = &<d1771>heap<3,1>[0]
| | | | nthreads_shared = &<d1771>heap<3,2>[0]
| | | | i_shared = &<d1771>heap<3,3>[0]
| | | | tid$omp_private = 1
| | | | _anon_13 = "Thread %d starting...\n"
| | dyscope d1770 (id=12, parent=d5, static=50)
| | | variables
| | | | _tid = 1
| | dyscope d2998 (id=13, parent=d4252, static=68)
| | | variables
| | | | otherTid = 0
| | | | _anon_3 = "Thread %d can't perform $omp_write because thread %d has written to the same variable and hasn't flushed yet.\n"
| | dyscope d4252 (id=14, parent=d0, static=36)
| | | variables
| | | | shared = &<d1771>heap<3,3>[0]
| | | | ref = &<d1771>i_local
| | | | value = &<d4251>tmpWrite5
| | dyscope d8285 (id=15, parent=d2989, static=59)
| | | variables
| | | | other = &<d18>heap<3,3>[0]
| | | | segFault = true
| | dyscope d2989 (id=16, parent=d2988, static=58)
| | | variables
| | | | i = 0
| | dyscope d2988 (id=17, parent=d3011, static=57)
| | | variables
| | | | tid = 1
| | | | gshared = &<d5>heap<2,3>[0]
| | | | nthreads = 2
| | | | isIdentityRef = true
| | dyscope d3011 (id=18, parent=d0, static=34)
| | | variables
| | | | shared = &<d1771>heap<3,3>[0]
| | | | ref = &<d1771>i_local
| Process states
| | process p0(id=0)
| | | call stack
| | | | Frame[function=_CIVL_system, location=25, OpenMPtoCIVLTransformer:0.-1-20 "$parfor(int _tid: ..." inserted by OpenMPtoCIVLTransformer.parallelPragmabefore op.h:22.1-10 "Operation" included from civlc.cvh:12.9-15 "<op.h>" included from omp.cvl:1.9-20 "<civlc.cvh>", dyscope=d5]
| | process p1(id=1)
| | | call stack
| | | | Frame[function=$omp_set_lock, location=36, omp.cvl:27.2-9 "$atomic", dyscope=d377]
| | | | Frame[function=_par_proc0, location=297, omp_bug5.c:55.6-18 "omp_set_lock", dyscope=d130]
| | process p3(id=2)
| | | call stack
| | | | Frame[function=$omp_write, location=143, civl-omp.cvl:243.2-9 "$assert", dyscope=d2998]
| | | | Frame[function=_par_proc0, location=320, OpenMPtoCIVLTransformer:0.-1-20 "i_shared, &i_local..." inserted by OpenMPtoCIVLTransformer.i_sharedWriteCallbefore op.h:22.1-10 "Operation" included from civlc.cvh:12.9-15 "<op.h>" included from omp.cvl:1.9-20 "<civlc.cvh>", dyscope=d4251]

Logging new entry 0, writing trace to CIVLREP/omp_bug5_0.trace

Error bound exceeded: search terminated

=================== Stats ===================
   validCalls          : 31976
   proverCalls         : 10
   memory (bytes)      : 908591104
   time (s)            : 5.55
   maxProcs            : 3
   statesInstantiated  : 119142
   statesSaved         : 8671
   statesSeen          : 8645
   statesMatched       : 99
   steps               : 25883
   transitions         : 8743

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