NAME: bug4.c
CITE: \cite{LLNL:Pthreads:URL}
TYPE: $\text{P}$
SCALE: {\texttt{NT=3}}

files,language,blank,comment,code,"http://cloc.sourceforge.net v 1.62  T=0.01 s (165.6 files/s, 19708.7 lines/s)"
1,C,12,30,77
civl verify -enablePrintf=false bug4.c
CIVL v0.16 of 2015-1-6 -- http://vsl.cis.udel.edu/civl
Error 0 encountered at depth 250:
CIVL execution error in  (kind: DEADLOCK, certainty: PROVEABLE)
A deadlock is possible:
  Path condition: (0 <= -1*X3+9) && (0 <= X3+-1)
  Enabling predicate: false
ProcessState 0: at location 83, pthread.cvl:742.2-7 "$wait"
  Enabling predicate: false
ProcessState 1: at location 140, pthread.cvl:978.21-22 ";"
  Enabling predicate: false
ProcessState 2: terminated
ProcessState 3: terminated
at pthread.cvl:742.2-7 "$wait".
State 2120
| Path condition
| | (0 <= -1*X3+9) && (0 <= X3+-1)
| Dynamic scopes
| | dyscope d0 (id=0, parent=NULL, static=0)
| | | variables
| | | | _heap = 
| | | | | objects of malloc 0:
| | | | | | 0: (_pthread_gpool_t[1])<_pthread_gpool_t<(pointer[3])<&<d1>threads[0],&<d1>threads[1],&<d1>threads[2]>>>
| | | | _time_count_var = 0
| | | | CIVL_argc = X3
| | | | CIVL_argv = X4
| | | | value_ptr_value = NULL
| | | | $pthread_gpool = &<d0>heap<0,0>[0]
| | | | count = 6
| | | | finalresult = 4*(SIN(1)*TAN(1))+2*(SIN(1)*TAN(2))+6*(SIN(1)*TAN(0))+4*(SIN(2)*TAN(1))+2*(SIN(2)*TAN(2))+6*(SIN(2)*TAN(0))+4*(SIN(3)*TAN(1))+2*(SIN(3)*TAN(2))+6*(SIN(3)*TAN(0))+4*(SIN(4)*TAN(1))+2*(SIN(4)*TAN(2))+6*(SIN(4)*TAN(0))+4*(SIN(0)*TAN(1))+2*(SIN(0)*TAN(2))+6*(SIN(0)*TAN(0))
| | | | count_mutex = pthread_mutex_t<1,$proc_null,0,0,pthread_mutexattr_t<0,0,0,0,0>>
| | | | count_condvar = pthread_cond_t<1,false>
| | dyscope d1 (id=1, parent=d0, static=32)
| | | 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]
| | | | t1 = 1
| | | | t2 = 2
| | | | t3 = 3
| | | | i = 0
| | | | threads = (pthread_t[3])<pthread_t<p1,V0<0:=0, 2:=0>,false>,pthread_t<p2,V0<0:=0, 2:=0>,true>,pthread_t<p3,V0<0:=0, 2:=0>,true>>
| | | | attr = V0<0:=0, 2:=0>
| | | | _anon_0 = NULL
| | dyscope d16 (id=2, parent=d0, static=19)
| | | variables
| | | | thread = pthread_t<p1,V0<0:=0, 2:=0>,false>
| | | | value_ptr = NULL
| | | | _anon_1 = NULL
| | dyscope d17 (id=3, parent=d9, static=47)
| | | variables
| | | | tid = 1
| | | | myresult = 0
| | | | _anon_5 = "sub1: thread=%ld going into wait. count=%d\n"
| | | | _anon_6 = NULL
| | | | _anon_7 = NULL
| | | | _anon_8 = NULL
| | dyscope d9 (id=4, parent=d8, static=46)
| | | variables
| | | | _heap = 
| | | | | objects of malloc 1:
| | | | | | 0: (_pthread_pool_t[1])<_pthread_pool_t<&<d0>heap<0,0>[0],p1,&<d1>threads[0]>>
| | | | $pthread_pool = &<d9>heap<1,0>[0]
| | dyscope d8 (id=5, parent=d0, static=30)
| | | variables
| | | | t = 1
| | dyscope d73 (id=6, parent=d0, static=24)
| | | variables
| | | | cond = &<d0>count_condvar
| | | | mutex = &<d0>count_mutex
| | | | $pthread_pool = &<d9>heap<1,0>[0]
| Process states
| | process p0(id=0)
| | | call stack
| | | | Frame[function=pthread_join, location=83, pthread.cvl:742.2-7 "$wait", dyscope=d16]
| | | | Frame[function=_CIVL_system, location=34, bug4.c:107.4-16 "pthread_join", dyscope=d1]
| | process p1(id=1)
| | | call stack
| | | | Frame[function=_pthread_cond_wait, location=140, pthread.cvl:978.21-22 ";", dyscope=d73]
| | | | Frame[function=sub1, location=159, bug4.c:46.2-19 "pthread_cond_wait", dyscope=d17]
| | process p2(id=2)
| | | call stack
| | process p3(id=3)
| | | call stack

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

Error bound exceeded: search terminated

=================== Stats ===================
   validCalls          : 12859
   proverCalls         : 3
   memory (bytes)      : 920649728
   time (s)            : 3.61
   maxProcs            : 4
   statesInstantiated  : 29070
   statesSaved         : 2121
   statesSeen          : 2120
   statesMatched       : 271
   steps               : 5011
   transitions         : 2390

The program MAY NOT be correct.  See CIVLREP/bug4_log.txt
NAME: queue{\U}ok{\U}longest{\U}true.c
CITE: \cite{svcomp:2015} 
TYPE: $\text{P}$
SCALE: {\texttt{SIZE=800}}

files,language,blank,comment,code,"http://cloc.sourceforge.net v 1.62  T=0.01 s (139.8 files/s, 21249.7 lines/s)"
1,C,26,0,126
civl verify -enablePrintf=false -svcomp -inputSIZE=800 -inputEMPTY=-1 -inputFULL=-2 queue_ok_longest_true.c
CIVL v0.16 of 2015-1-6 -- http://vsl.cis.udel.edu/civl
17s: mem=801Mb steps=47161 trans=37796 seen=35682 saved=35682 prove=0
32s: mem=681Mb steps=119721 trans=86005 seen=78206 saved=78206 prove=0

=================== Stats ===================
   validCalls          : 226787
   proverCalls         : 0
   memory (bytes)      : 619184128
   time (s)            : 42.17
   maxProcs            : 3
   statesInstantiated  : 1001897
   statesSaved         : 104324
   statesSeen          : 104324
   statesMatched       : 11243
   steps               : 158247
   transitions         : 115566

The standard properties hold for all executions.
NAME: read{\U}write{\U}lock{\U}false.c
CITE: \cite{svcomp:2015} 
TYPE: $\text{P}$
SCALE: {\texttt{NT=4}}

files,language,blank,comment,code,"http://cloc.sourceforge.net v 1.62  T=0.01 s (74.2 files/s, 4006.5 lines/s)"
1,C,9,7,38
civl verify -enablePrintf=false -svcomp read_write_lock_false.c
CIVL v0.16 of 2015-1-6 -- http://vsl.cis.udel.edu/civl
Error 0 encountered at depth 63:
CIVL execution error in p2(id=1) (kind: ASSERTION_VIOLATION, certainty: PROVEABLE)
Cannot prove assertion holds: $assert false
  Path condition: true
  Assertion: false

at PthreadToCIVLTransformer:0.-1-15 "$assert $false;\n" inserted by PthreadToCIVLTransformer.assertionbefore read_write_lock_false.c:43.0-3 "int".
State -1:95728
| Path condition
| | true
| Dynamic scopes
| | dyscope d0 (id=0, parent=NULL, static=0)
| | | variables
| | | | _heap = 
| | | | | objects of malloc 0:
| | | | | | 0: (_pthread_gpool_t[1])<_pthread_gpool_t<(pointer[4])<&<d1>t1,&<d1>t2,&<d1>t3,&<d1>t4>>>
| | | | _time_count_var = 0
| | | | value_ptr_value = NULL
| | | | $pthread_gpool = &<d0>heap<0,0>[0]
| | | | w = 0
| | | | r = 0
| | | | x = 3
| | | | y = 0
| | dyscope d1 (id=1, parent=d0, static=18)
| | | variables
| | | | t1 = pthread_t<UNDEFINED,pthread_attr_t<0,0,0,0>,true>
| | | | t2 = pthread_t<UNDEFINED,pthread_attr_t<0,0,0,0>,true>
| | | | t3 = pthread_t<UNDEFINED,pthread_attr_t<0,0,0,0>,true>
| | | | t4 = pthread_t<p2,pthread_attr_t<0,0,0,0>,false>
| | dyscope d14 (id=2, parent=d0, static=11)
| | | variables
| | | | thread = pthread_t<p2,pthread_attr_t<0,0,0,0>,false>
| | | | value_ptr = NULL
| | | | _anon_0 = NULL
| | dyscope d16 (id=3, parent=d13, static=24)
| | | variables
| | | | l = 0
| | dyscope d13 (id=4, parent=d6, static=23)
| | | variables
| | | | _heap = 
| | | | | objects of malloc 1:
| | | | | | 0: (_pthread_pool_t[1])<_pthread_pool_t<&<d0>heap<0,0>[0],p2,&<d1>t4>>
| | | | $pthread_pool = &<d13>heap<1,0>[0]
| | dyscope d6 (id=5, parent=d0, static=17)
| | | variables
| | | | arg = NULL
| Process states
| | process p0(id=0)
| | | call stack
| | | | Frame[function=pthread_join, location=37, pthread.cvl:742.2-7 "$wait", dyscope=d14]
| | | | Frame[function=_CIVL_system, location=17, read_write_lock_false.c:52.2-14 "pthread_join", dyscope=d1]
| | process p2(id=1)
| | | call stack
| | | | Frame[function=reader, location=75, PthreadToCIVLTransformer:0.-1-15 "$assert $false;\n" inserted by PthreadToCIVLTransformer.assertionbefore read_write_lock_false.c:43.0-3 "int", dyscope=d16]

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

Error bound exceeded: search terminated

=================== Stats ===================
   validCalls          : 12208
   proverCalls         : 0
   memory (bytes)      : 514850816
   time (s)            : 2.66
   maxProcs            : 5
   statesInstantiated  : 95729
   statesSaved         : 7320
   statesSeen          : 7320
   statesMatched       : 2548
   steps               : 13937
   transitions         : 9867

The program MAY NOT be correct.  See CIVLREP/read_write_lock_false_log.txt
NAME: sync01{\U}true.c
CITE: \cite{svcomp:2015} 
TYPE: $\text{P}$
SCALE: {\texttt{NT=2}}

files,language,blank,comment,code,"http://cloc.sourceforge.net v 1.62  T=0.01 s (152.8 files/s, 10236.7 lines/s)"
1,C,24,1,42
civl verify -enablePrintf=false -svcomp sync01_true.c
CIVL v0.16 of 2015-1-6 -- http://vsl.cis.udel.edu/civl

=================== Stats ===================
   validCalls          : 855
   proverCalls         : 0
   memory (bytes)      : 514850816
   time (s)            : 1.38
   maxProcs            : 3
   statesInstantiated  : 2540
   statesSaved         : 247
   statesSeen          : 247
   statesMatched       : 25
   steps               : 449
   transitions         : 271

The standard properties hold for all executions.
NAME: 03{\U}incdec{\U}true.c
CITE: \cite{svcomp:2015} 
TYPE: $\text{P}$
SCALE: {\texttt{NT=3}}

files,language,blank,comment,code,"http://cloc.sourceforge.net v 1.62  T=0.01 s (72.9 files/s, 5835.1 lines/s)"
1,C,22,3,55
civl verify -enablePrintf=false -svcomp -procBound=3 03_incdec_true.c	
CIVL v0.16 of 2015-1-6 -- http://vsl.cis.udel.edu/civl

=================== Stats ===================
   validCalls          : 261
   proverCalls         : 3
   memory (bytes)      : 514850816
   time (s)            : 1.3
   maxProcs            : 3
   statesInstantiated  : 3518
   statesSaved         : 275
   statesSeen          : 273
   statesMatched       : 38
   steps               : 662
   transitions         : 310

The standard properties hold for all executions.
