How to read the tables?

Meaning of the model-checker's results
Model-checker on the instrumented programObserved state in LitmusPicture
VERIFICATION FAILED YES
VERIFICATION SUCCESSFUL NO



Reading the results in the experiments tables
The table below is an excerpt of former results we obtained for x86/podwr experiments.
NameSCTSO (all delay/cyc)TSO (1 delay/cyc)Expected (TSO)  ...  
x86/podwr000
Fre PodWR Fre PodWR
SatAbs:
0.60sec

ESBMC: 0.30sec

Threader: 7.92sec

...
Cycles
SatAbs:
3.94sec (x6.56)

ESBMC: 8.34sec

Threader: ERROR/TIMEOUT[1] 491.99sec

...
Cycles
SatAbs:
2.43sec (x4.05)

ESBMC: 7.58sec

Threader: ERROR/TIMEOUT[1] 182.60sec

...
  ...  

Real-life C programs

On the one hand, this family contains the PostgreSQL bug, the fix proposed by PostgreSQL developers and our own fix for it. It should answer Yes in litmus terms, or Verification Failed in verification terms, starting from RMO. The fix proposed by the developers is not enough, hence should answer Yes in litmus terms, or Verification Failed in verification terms, starting from RMO. Our fix should answer No in litmus terms and Verification Successful in verification terms, regardless of the model.

On the other hand, this family contains our experiments with RCU and Apache. It shows all the cycles (i.e. potential bugs) exhibited by RCU, and verifies Apache.

Apache

Name SC CAV'11 TSO (all delay/cyc) TSO (1 delay/cyc) TSO (opt delay/cyc) Expected (TSO) PSO (all delay/cyc) PSO (1 delay/cyc) PSO (opt delay/cyc) Expected (PSO) RMO (all delay/cyc) RMO (1 delay/cyc) RMO (opt delay/cyc) Expected (RMO) Power (all delay/cyc) Power (1 delay/cyc) Power (opt delay/cyc) Expected (Power)
gb_fdqueue_builtins.c
SatAbs: ERROR/TIMEOUT[1]
0.10sec

Satabs-prefix-first: ERROR/TIMEOUT[1] 0.11sec
CBMC-WMM: 0.18sec
CBMC-SC: 0.15sec
dump-c failed with exit code 134
Cycles
SatAbs: ERROR/TIMEOUT[1]
0.10sec (x1.00)

Satabs-prefix-first: ERROR/TIMEOUT[1] 0.12sec
CBMC-WMM: 0.17sec
CBMC-SC: 0.16sec
dump-c failed with exit code 134
Cycles
SatAbs: ERROR/TIMEOUT[1]
0.09sec (x.90)

Satabs-prefix-first: ERROR/TIMEOUT[1] 0.12sec
CBMC-WMM: 0.19sec
CBMC-SC: 0.15sec
dump-c failed with exit code 134
Cycles
SatAbs: ERROR/TIMEOUT[1]
0.11sec (x1.10)

Satabs-prefix-first: ERROR/TIMEOUT[1] 0.09sec
CBMC-WMM: 0.17sec
CBMC-SC: 0.16sec
dump-c failed with exit code 134
Cycles
SatAbs: ERROR/TIMEOUT[1]
0.09sec (x.90)

Satabs-prefix-first: ERROR/TIMEOUT[1] 0.09sec
CBMC-WMM: 0.18sec
CBMC-SC: 0.15sec
dump-c failed with exit code 134
UNKNOWN Cycles
SatAbs: ERROR/TIMEOUT[1]
0.09sec (x.90)

Satabs-prefix-first: ERROR/TIMEOUT[1] 0.11sec
CBMC-WMM: 0.18sec
CBMC-SC: 0.17sec
dump-c failed with exit code 134
Cycles
SatAbs: ERROR/TIMEOUT[1]
0.10sec (x1.00)

Satabs-prefix-first: ERROR/TIMEOUT[1] 0.12sec
CBMC-WMM: 0.16sec
CBMC-SC: 0.17sec
dump-c failed with exit code 134
Cycles
SatAbs: ERROR/TIMEOUT[1]
0.12sec (x1.20)

Satabs-prefix-first: ERROR/TIMEOUT[1] 0.10sec
CBMC-WMM: 0.16sec
CBMC-SC: 0.19sec
dump-c failed with exit code 134
UNKNOWN Cycles
SatAbs: ERROR/TIMEOUT[1]
0.11sec (x1.10)

Satabs-prefix-first: ERROR/TIMEOUT[1] 0.12sec
CBMC-WMM: 0.20sec
CBMC-SC: 0.17sec
dump-c failed with exit code 134
Cycles
SatAbs: ERROR/TIMEOUT[1]
0.11sec (x1.10)

Satabs-prefix-first: ERROR/TIMEOUT[1] 0.12sec
CBMC-WMM: 0.13sec
CBMC-SC: 0.15sec
dump-c failed with exit code 134
Cycles
SatAbs: ERROR/TIMEOUT[1]
0.11sec (x1.10)

Satabs-prefix-first: ERROR/TIMEOUT[1] 0.11sec
CBMC-WMM: 0.17sec
CBMC-SC: 0.16sec
dump-c failed with exit code 134
UNKNOWN Cycles
SatAbs: ERROR/TIMEOUT[1]
0.11sec (x1.10)

Satabs-prefix-first: ERROR/TIMEOUT[1] 0.12sec
CBMC-WMM: 0.18sec
CBMC-SC: 0.14sec
dump-c failed with exit code 134
Cycles
SatAbs: ERROR/TIMEOUT[1]
0.11sec (x1.10)

Satabs-prefix-first: ERROR/TIMEOUT[1] 0.10sec
CBMC-WMM: 0.18sec
CBMC-SC: 0.18sec
dump-c failed with exit code 134
Cycles
SatAbs: ERROR/TIMEOUT[1]
0.09sec (x.90)

Satabs-prefix-first: ERROR/TIMEOUT[1] 0.10sec
CBMC-WMM: 0.16sec
CBMC-SC: 0.15sec
dump-c failed with exit code 134
UNKNOWN
gb_fdqueue_builtins_ppc.c
SatAbs: ERROR/TIMEOUT[1]
0.12sec

Satabs-prefix-first: ERROR/TIMEOUT[1] 0.09sec
CBMC-WMM: 0.18sec
CBMC-SC: 0.16sec
dump-c failed with exit code 134
Cycles
SatAbs: ERROR/TIMEOUT[]


Satabs-prefix-first: ERROR/TIMEOUT[]
CBMC-WMM: 0.11sec
CBMC-SC: ERROR/TIMEOUT[]
dump-c failed with exit code 11
Cycles
SatAbs: ERROR/TIMEOUT[]


Satabs-prefix-first: ERROR/TIMEOUT[]
CBMC-WMM: 0.15sec
CBMC-SC: ERROR/TIMEOUT[]
dump-c failed with exit code 11
Cycles
SatAbs: ERROR/TIMEOUT[]


Satabs-prefix-first: ERROR/TIMEOUT[]
CBMC-WMM: 0.15sec
CBMC-SC: ERROR/TIMEOUT[]
dump-c failed with exit code 11
Cycles
SatAbs: ERROR/TIMEOUT[]


Satabs-prefix-first: ERROR/TIMEOUT[]
CBMC-WMM: 0.15sec
CBMC-SC: ERROR/TIMEOUT[]
dump-c failed with exit code 11
UNKNOWN Cycles
SatAbs: ERROR/TIMEOUT[]


Satabs-prefix-first: ERROR/TIMEOUT[]
CBMC-WMM: 0.14sec
CBMC-SC: ERROR/TIMEOUT[]
dump-c failed with exit code 11
Cycles
SatAbs: ERROR/TIMEOUT[]


Satabs-prefix-first: ERROR/TIMEOUT[]
CBMC-WMM: 0.15sec
CBMC-SC: ERROR/TIMEOUT[]
dump-c failed with exit code 11
Cycles
SatAbs: ERROR/TIMEOUT[]


Satabs-prefix-first: ERROR/TIMEOUT[]
CBMC-WMM: 0.15sec
CBMC-SC: ERROR/TIMEOUT[]
dump-c failed with exit code 11
UNKNOWN Cycles
SatAbs: ERROR/TIMEOUT[]


Satabs-prefix-first: ERROR/TIMEOUT[]
CBMC-WMM: 0.15sec
CBMC-SC: ERROR/TIMEOUT[]
dump-c failed with exit code 11
Cycles
SatAbs: ERROR/TIMEOUT[]


Satabs-prefix-first: ERROR/TIMEOUT[]
CBMC-WMM: 0.16sec
CBMC-SC: ERROR/TIMEOUT[]
dump-c failed with exit code 11
Cycles
SatAbs: ERROR/TIMEOUT[]


Satabs-prefix-first: ERROR/TIMEOUT[]
CBMC-WMM: 0.16sec
CBMC-SC: ERROR/TIMEOUT[]
dump-c failed with exit code 11
UNKNOWN Cycles
SatAbs: ERROR/TIMEOUT[]


Satabs-prefix-first: ERROR/TIMEOUT[]
CBMC-WMM: 0.14sec
CBMC-SC: ERROR/TIMEOUT[]
dump-c failed with exit code 11
Cycles
SatAbs: ERROR/TIMEOUT[]


Satabs-prefix-first: ERROR/TIMEOUT[]
CBMC-WMM: 0.13sec
CBMC-SC: ERROR/TIMEOUT[]
dump-c failed with exit code 11
Cycles
SatAbs: ERROR/TIMEOUT[]


Satabs-prefix-first: ERROR/TIMEOUT[]
CBMC-WMM: 0.13sec
CBMC-SC: ERROR/TIMEOUT[]
dump-c failed with exit code 11
UNKNOWN
gb_fdqueue_ia32.c
SatAbs: ERROR/TIMEOUT[1]
0.10sec

Satabs-prefix-first: ERROR/TIMEOUT[1] 0.08sec
CBMC-WMM: 0.15sec
CBMC-SC: 0.15sec
dump-c failed with exit code 134
Cycles
SatAbs: ERROR/TIMEOUT[1]
0.12sec (x1.20)

Satabs-prefix-first: ERROR/TIMEOUT[1] 0.09sec
CBMC-WMM: 0.18sec
CBMC-SC: 0.18sec
dump-c failed with exit code 134
Cycles
SatAbs: ERROR/TIMEOUT[1]
0.11sec (x1.10)

Satabs-prefix-first: ERROR/TIMEOUT[1] 0.10sec
CBMC-WMM: 0.15sec
CBMC-SC: 0.17sec
dump-c failed with exit code 134
Cycles
SatAbs: ERROR/TIMEOUT[1]
0.11sec (x1.10)

Satabs-prefix-first: ERROR/TIMEOUT[1] 0.10sec
CBMC-WMM: 0.15sec
CBMC-SC: 0.17sec
dump-c failed with exit code 134
Cycles
SatAbs: ERROR/TIMEOUT[1]
0.11sec (x1.10)

Satabs-prefix-first: ERROR/TIMEOUT[1] 0.11sec
CBMC-WMM: 0.17sec
CBMC-SC: 0.17sec
dump-c failed with exit code 134
UNKNOWN Cycles
SatAbs: ERROR/TIMEOUT[1]
0.09sec (x.90)

Satabs-prefix-first: ERROR/TIMEOUT[1] 0.11sec
CBMC-WMM: 0.17sec
CBMC-SC: 0.18sec
dump-c failed with exit code 134
Cycles
SatAbs: ERROR/TIMEOUT[1]
0.10sec (x1.00)

Satabs-prefix-first: ERROR/TIMEOUT[1] 0.11sec
CBMC-WMM: 0.14sec
CBMC-SC: 0.15sec
dump-c failed with exit code 134
Cycles
SatAbs: ERROR/TIMEOUT[1]
0.11sec (x1.10)

Satabs-prefix-first: ERROR/TIMEOUT[1] 0.12sec
CBMC-WMM: 0.14sec
CBMC-SC: 0.15sec
dump-c failed with exit code 134
UNKNOWN Cycles
SatAbs: ERROR/TIMEOUT[1]
0.11sec (x1.10)

Satabs-prefix-first: ERROR/TIMEOUT[1] 0.11sec
CBMC-WMM: 0.18sec
CBMC-SC: 0.18sec
dump-c failed with exit code 134
Cycles
SatAbs: ERROR/TIMEOUT[1]
0.09sec (x.90)

Satabs-prefix-first: ERROR/TIMEOUT[1] 0.11sec
CBMC-WMM: 0.16sec
CBMC-SC: 0.16sec
dump-c failed with exit code 134
Cycles
SatAbs: ERROR/TIMEOUT[1]
0.09sec (x.90)

Satabs-prefix-first: ERROR/TIMEOUT[1] 0.11sec
CBMC-WMM: 0.16sec
CBMC-SC: 0.18sec
dump-c failed with exit code 134
UNKNOWN Cycles
SatAbs: ERROR/TIMEOUT[1]
0.11sec (x1.10)

Satabs-prefix-first: ERROR/TIMEOUT[1] 0.11sec
CBMC-WMM: 0.16sec
CBMC-SC: 0.16sec
dump-c failed with exit code 134
Cycles
SatAbs: ERROR/TIMEOUT[1]
0.12sec (x1.20)

Satabs-prefix-first: ERROR/TIMEOUT[1] 0.12sec
CBMC-WMM: 0.17sec
CBMC-SC: 0.20sec
dump-c failed with exit code 134
Cycles
SatAbs: ERROR/TIMEOUT[1]
0.11sec (x1.10)

Satabs-prefix-first: ERROR/TIMEOUT[1] 0.11sec
CBMC-WMM: 0.18sec
CBMC-SC: 0.15sec
dump-c failed with exit code 134
UNKNOWN
gb_fdqueue_ppc.c
SatAbs: ERROR/TIMEOUT[1]
0.11sec

Satabs-prefix-first: ERROR/TIMEOUT[1] 0.11sec
CBMC-WMM: 0.15sec
CBMC-SC: 0.15sec
dump-c failed with exit code 134
Cycles
SatAbs: ERROR/TIMEOUT[1]
0.09sec (x.81)

Satabs-prefix-first: ERROR/TIMEOUT[1] 0.11sec
CBMC-WMM: 0.16sec
CBMC-SC: 0.18sec
dump-c failed with exit code 134
Cycles
SatAbs: ERROR/TIMEOUT[1]
0.08sec (x.72)

Satabs-prefix-first: ERROR/TIMEOUT[1] 0.09sec
CBMC-WMM: 0.18sec
CBMC-SC: 0.18sec
dump-c failed with exit code 134
Cycles
SatAbs: ERROR/TIMEOUT[1]
0.10sec (x.90)

Satabs-prefix-first: ERROR/TIMEOUT[1] 0.10sec
CBMC-WMM: 0.18sec
CBMC-SC: 0.14sec
dump-c failed with exit code 134
Cycles
SatAbs: ERROR/TIMEOUT[1]
0.13sec (x1.18)

Satabs-prefix-first: ERROR/TIMEOUT[1] 0.12sec
CBMC-WMM: 0.16sec
CBMC-SC: 0.15sec
dump-c failed with exit code 134
UNKNOWN Cycles
SatAbs: ERROR/TIMEOUT[1]
0.10sec (x.90)

Satabs-prefix-first: ERROR/TIMEOUT[1] 0.11sec
CBMC-WMM: 0.15sec
CBMC-SC: 0.15sec
dump-c failed with exit code 134
Cycles
SatAbs: ERROR/TIMEOUT[1]
0.11sec (x1.00)

Satabs-prefix-first: ERROR/TIMEOUT[1] 0.08sec
CBMC-WMM: 0.16sec
CBMC-SC: 0.17sec
dump-c failed with exit code 134
Cycles
SatAbs: ERROR/TIMEOUT[1]
0.09sec (x.81)

Satabs-prefix-first: ERROR/TIMEOUT[1] 0.09sec
CBMC-WMM: 0.19sec
CBMC-SC: 0.15sec
dump-c failed with exit code 134
UNKNOWN Cycles
SatAbs: ERROR/TIMEOUT[1]
0.11sec (x1.00)

Satabs-prefix-first: ERROR/TIMEOUT[1] 0.10sec
CBMC-WMM: 0.14sec
CBMC-SC: 0.18sec
dump-c failed with exit code 134
Cycles
SatAbs: ERROR/TIMEOUT[1]
0.12sec (x1.09)

Satabs-prefix-first: ERROR/TIMEOUT[1] 0.10sec
CBMC-WMM: 0.16sec
CBMC-SC: 0.18sec
dump-c failed with exit code 134
Cycles
SatAbs: ERROR/TIMEOUT[1]
0.11sec (x1.00)

Satabs-prefix-first: ERROR/TIMEOUT[1] 0.10sec
CBMC-WMM: 0.16sec
CBMC-SC: 0.16sec
dump-c failed with exit code 134
UNKNOWN Cycles
SatAbs: ERROR/TIMEOUT[1]
0.11sec (x1.00)

Satabs-prefix-first: ERROR/TIMEOUT[1] 0.12sec
CBMC-WMM: 0.16sec
CBMC-SC: 0.16sec
dump-c failed with exit code 134
Cycles
SatAbs: ERROR/TIMEOUT[1]
0.11sec (x1.00)

Satabs-prefix-first: ERROR/TIMEOUT[1] 0.11sec
CBMC-WMM: 0.16sec
CBMC-SC: 0.17sec
dump-c failed with exit code 134
Cycles
SatAbs: ERROR/TIMEOUT[1]
0.08sec (x.72)

Satabs-prefix-first: ERROR/TIMEOUT[1] 0.11sec
CBMC-WMM: 0.19sec
CBMC-SC: 0.17sec
dump-c failed with exit code 134
UNKNOWN

Pgsql

Name SC TSO (all delay/cyc) TSO (1 delay/cyc) Expected (TSO) PSO (all delay/cyc) PSO (1 delay/cyc) Expected (PSO) RMO (all delay/cyc) RMO (1 delay/cyc) Expected (RMO) Power (all delay/cyc) Power (1 delay/cyc) Expected (Power)
pgsql_two.c
SatAbs:
0.06sec

CImpact: ERROR/TIMEOUT[8] 34.48sec
ESBMC: 475.63sec
Threader: 0.83sec
Poirot-Integer: ERROR/TIMEOUT
Poirot-BitVector: ERROR/TIMEOUT
C code
Cycles
SatAbs:
0.44sec (x7.33)

CImpact: ERROR/TIMEOUT[8] 19.86sec
ESBMC: ERROR/TIMEOUT[130]
Threader: ERROR/TIMEOUT[1] 0.08sec
Poirot-Integer: ERROR/TIMEOUT
Poirot-BitVector: ERROR/TIMEOUT
Instrumented C code
Cycles
SatAbs:
0.42sec (x7.00)

CImpact: ERROR/TIMEOUT[8] 17.74sec
ESBMC: ERROR/TIMEOUT[130]
Threader: ERROR/TIMEOUT[1] 0.07sec
Poirot-Integer: ERROR/TIMEOUT
Poirot-BitVector: ERROR/TIMEOUT
Instrumented C code
Cycles
SatAbs: (spurious)
18.13sec (x302.16)

CImpact: ERROR/TIMEOUT[8] 46.06sec
ESBMC: ERROR/TIMEOUT[130]
Threader: ERROR/TIMEOUT[1] 1.24sec
Poirot-Integer: ERROR/TIMEOUT
Poirot-BitVector: ERROR/TIMEOUT
Instrumented C code
Cycles
SatAbs: (spurious)
16.60sec (x276.66)

CImpact: ERROR/TIMEOUT[8] 46.55sec
ESBMC: ERROR/TIMEOUT[130]
Threader: ERROR/TIMEOUT[1] 1.07sec
Poirot-Integer: ERROR/TIMEOUT
Poirot-BitVector: ERROR/TIMEOUT
Instrumented C code
Cycles
SatAbs:
23.70sec (x395.00)

CImpact: ERROR/TIMEOUT[8] 52.59sec
ESBMC: ERROR/TIMEOUT[130]
Threader: ERROR/TIMEOUT[1] 1.12sec
Poirot-Integer: ERROR/TIMEOUT
Poirot-BitVector: ERROR/TIMEOUT
Instrumented C code
Cycles
SatAbs:
25.07sec (x417.83)

CImpact: ERROR/TIMEOUT[8] 88.22sec
ESBMC: ERROR/TIMEOUT[130]
Threader: ERROR/TIMEOUT[1] 1.13sec
Poirot-Integer: ERROR/TIMEOUT
Poirot-BitVector: ERROR/TIMEOUT
Instrumented C code
Cycles
SatAbs:
27.27sec (x454.50)

CImpact: ERROR/TIMEOUT[8] 57.24sec
ESBMC: ERROR/TIMEOUT[130]
Threader: ERROR/TIMEOUT[1] 3.07sec
Poirot-Integer: ERROR/TIMEOUT
Poirot-BitVector: ERROR/TIMEOUT
Instrumented C code
Cycles
SatAbs:
27.15sec (x452.50)

CImpact: ERROR/TIMEOUT[8] 55.60sec
ESBMC: ERROR/TIMEOUT[130]
Threader: ERROR/TIMEOUT[1] 5.00sec
Poirot-Integer: ERROR/TIMEOUT
Poirot-BitVector: ERROR/TIMEOUT
Instrumented C code
pgsql_two-developer-fix.c
SatAbs:
0.06sec

CImpact: ERROR/TIMEOUT[8] 18.92sec
ESBMC: 259.44sec
Threader: 0.60sec
Poirot-Integer: ERROR/TIMEOUT
Poirot-BitVector: ERROR/TIMEOUT
C code
Cycles
SatAbs:
0.35sec (x5.83)

CImpact: ERROR/TIMEOUT[8] 17.60sec
ESBMC: ERROR/TIMEOUT[130]
Threader: ERROR/TIMEOUT[1] 0.07sec
Poirot-Integer: ERROR/TIMEOUT
Poirot-BitVector: ERROR/TIMEOUT
Instrumented C code
Cycles
SatAbs:
0.54sec (x9.00)

CImpact: ERROR/TIMEOUT[8] 17.17sec
ESBMC: ERROR/TIMEOUT[130]
Threader: ERROR/TIMEOUT[1] 0.09sec
Poirot-Integer: ERROR/TIMEOUT
Poirot-BitVector: ERROR/TIMEOUT
Instrumented C code
Cycles
SatAbs: (spurious)
8.84sec (x147.33)

CImpact: ERROR/TIMEOUT[8] 32.93sec
ESBMC: ERROR/TIMEOUT[130]
Threader: ERROR/TIMEOUT[1] 1.50sec
Poirot-Integer: ERROR/TIMEOUT
Poirot-BitVector: ERROR/TIMEOUT
Instrumented C code
Cycles
SatAbs: (spurious)
9.33sec (x155.50)

CImpact: ERROR/TIMEOUT[8] 35.93sec
ESBMC: ERROR/TIMEOUT[130]
Threader: ERROR/TIMEOUT[1] 1.77sec
Poirot-Integer: ERROR/TIMEOUT
Poirot-BitVector: ERROR/TIMEOUT
Instrumented C code
Cycles
SatAbs:
12.61sec (x210.16)

CImpact: ERROR/TIMEOUT[8] 48.05sec
ESBMC: ERROR/TIMEOUT[130]
Threader: ERROR/TIMEOUT[1] 1.13sec
Poirot-Integer: ERROR/TIMEOUT
Poirot-BitVector: ERROR/TIMEOUT
Instrumented C code
Cycles
SatAbs:
8.87sec (x147.83)

CImpact: ERROR/TIMEOUT[8] 27.62sec
ESBMC: ERROR/TIMEOUT[130]
Threader: ERROR/TIMEOUT[1] 1.60sec
Poirot-Integer: ERROR/TIMEOUT
Poirot-BitVector: ERROR/TIMEOUT
Instrumented C code
Cycles
SatAbs:
13.86sec (x231.00)

CImpact: ERROR/TIMEOUT[8] 38.36sec
ESBMC: ERROR/TIMEOUT[130]
Threader: ERROR/TIMEOUT[1] 2.98sec
Poirot-Integer: ERROR/TIMEOUT
Poirot-BitVector: ERROR/TIMEOUT
Instrumented C code
Cycles
SatAbs:
14.52sec (x242.00)

CImpact: ERROR/TIMEOUT[8] 50.41sec
ESBMC: ERROR/TIMEOUT[130]
Threader: ERROR/TIMEOUT[1] 3.51sec
Poirot-Integer: ERROR/TIMEOUT
Poirot-BitVector: ERROR/TIMEOUT
Instrumented C code
pgsql_two-fix.c
SatAbs:
0.09sec

CImpact: ERROR/TIMEOUT[8] 20.87sec
ESBMC: ERROR/TIMEOUT[134] 0.08sec
Threader: ERROR/TIMEOUT[1] 0.10sec
Poirot-Integer: 131.890625 s
Poirot-BitVector: ERROR/TIMEOUT
C code
Cycles
SatAbs:
115.82sec (x1286.88)

CImpact: ERROR/TIMEOUT[8] 31.67sec
ESBMC: 0.39sec
Threader: ERROR/TIMEOUT[1] 0.09sec
Poirot-Integer: ERROR/TIMEOUT
Poirot-BitVector: ERROR/TIMEOUT
Instrumented C code
Cycles
SatAbs:
116.43sec (x1293.66)

CImpact: ERROR/TIMEOUT[8] 31.73sec
ESBMC: 0.36sec
Threader: ERROR/TIMEOUT[1] 0.08sec
Poirot-Integer: ERROR/TIMEOUT
Poirot-BitVector: ERROR/TIMEOUT
Instrumented C code
Cycles
SatAbs:
151.42sec (x1682.44)

CImpact: ERROR/TIMEOUT[8] 33.13sec
ESBMC: 0.71sec
Threader: ERROR/TIMEOUT[1] 0.35sec
Poirot-Integer: ERROR/TIMEOUT
Poirot-BitVector: ERROR/TIMEOUT
Instrumented C code
Cycles
SatAbs:
151.98sec (x1688.66)

CImpact: ERROR/TIMEOUT[8] 33.02sec
ESBMC: 0.75sec
Threader: ERROR/TIMEOUT[1] 0.36sec
Poirot-Integer: ERROR/TIMEOUT
Poirot-BitVector: ERROR/TIMEOUT
Instrumented C code
Cycles
SatAbs:
265.46sec (x2949.55)

CImpact: ERROR/TIMEOUT[8] 34.45sec
ESBMC: 0.80sec
Threader: ERROR/TIMEOUT[1] 0.59sec
Poirot-Integer: ERROR/TIMEOUT
Poirot-BitVector: ERROR/TIMEOUT
Instrumented C code
Cycles
SatAbs: ERROR/TIMEOUT[130]


CImpact: ERROR/TIMEOUT[8] 38.34sec
ESBMC: ERROR/TIMEOUT[130]
Threader: ERROR/TIMEOUT[1] 0.34sec
Poirot-Integer: ERROR/TIMEOUT
Poirot-BitVector: ERROR/TIMEOUT
Instrumented C code
Cycles
SatAbs:
4.222sec

CImpact: ERROR/TIMEOUT[8] 49.63sec
ESBMC: 1.67sec
Threader: ERROR/TIMEOUT[1] 4.52sec
Poirot-Integer: ERROR/TIMEOUT
Poirot-BitVector: ERROR/TIMEOUT
Instrumented C code
Cycles
SatAbs: ERROR/TIMEOUT[100]
385.62sec (x4284.66)

CImpact: ERROR/TIMEOUT[8] 33.18sec
ESBMC: ERROR/TIMEOUT[134] 1.34sec
Threader: ERROR/TIMEOUT[1] 2.90sec
Poirot-Integer: ERROR/TIMEOUT
Poirot-BitVector: ERROR/TIMEOUT
Instrumented C code
pgsql_two-fix-lwsync.c
SatAbs:
0.20sec

Satabs-prefix-first: 0.26sec
CImpact: ERROR/TIMEOUT[8] 19.90sec
C code
Cycles
SatAbs:
0.19sec (x.95)

Satabs-prefix-first: 0.21sec
CImpact: ERROR/TIMEOUT[8] 18.44sec
Instrumented C code
Cycles
SatAbs:
0.17sec (x.85)

Satabs-prefix-first: 0.19sec
CImpact: ERROR/TIMEOUT[8] 18.66sec
Instrumented C code
UNKNOWN Cycles
SatAbs:
1.60sec (x8.00)

Satabs-prefix-first: 2.67sec
CImpact: ERROR/TIMEOUT[8] 27.93sec
Instrumented C code
Cycles
SatAbs:
0.86sec (x4.30)

Satabs-prefix-first: 1.08sec
CImpact: ERROR/TIMEOUT[8] 29.15sec
Instrumented C code
UNKNOWN Cycles
SatAbs:
2.21sec (x11.05)

Satabs-prefix-first: 2.90sec
CImpact: ERROR/TIMEOUT[8] 26.32sec
Instrumented C code
Cycles
SatAbs:
0.80sec (x4.00)

Satabs-prefix-first: 0.97sec
CImpact: ERROR/TIMEOUT[8] 23.65sec
Instrumented C code
UNKNOWN Cycles
SatAbs:
1.49sec (x7.45)

Satabs-prefix-first: 2.33sec
CImpact: ERROR/TIMEOUT[8] 24.71sec
Instrumented C code
Cycles
SatAbs:
0.85sec (x4.25)

Satabs-prefix-first: 1.27sec
CImpact: ERROR/TIMEOUT[8] 24.41sec
Instrumented C code
UNKNOWN

RCU

Name SC CAV'11 TSO (all delay/cyc) TSO (1 delay/cyc) TSO (opt delay/cyc) Expected (TSO) PSO (all delay/cyc) PSO (1 delay/cyc) PSO (opt delay/cyc) Expected (PSO) RMO (all delay/cyc) RMO (1 delay/cyc) RMO (opt delay/cyc) Expected (RMO) Power (all delay/cyc) Power (1 delay/cyc) Power (opt delay/cyc) Expected (Power)
gb_rcu_powerpc.c
SatAbs: ERROR/TIMEOUT[1]
4.86sec

Satabs-prefix-first: ERROR/TIMEOUT[1] 4.71sec
CBMC-WMM: 0.04sec
CBMC-SC: 0.02sec
dump-c failed with exit code 134
Cycles
SatAbs: ERROR/TIMEOUT[]


Satabs-prefix-first: ERROR/TIMEOUT[]
CBMC-WMM: 0.02sec
CBMC-SC: ERROR/TIMEOUT[]
dump-c failed with exit code 11
Cycles
SatAbs:
0.04sec (x0)

Satabs-prefix-first: 0.02sec
CBMC-WMM: 0.03sec
CBMC-SC: 0.03sec
dump-c failed with exit code 134
Cycles
SatAbs:
0.03sec (x0)

Satabs-prefix-first: 0.02sec
CBMC-WMM: 0.03sec
CBMC-SC: 0.04sec
dump-c failed with exit code 134
Cycles
SatAbs:
0.05sec (x.01)

Satabs-prefix-first: 0.03sec
CBMC-WMM: 0.02sec
CBMC-SC: 0.04sec
dump-c failed with exit code 134
UNKNOWN Cycles
SatAbs: ERROR/TIMEOUT[]


Satabs-prefix-first: ERROR/TIMEOUT[]
CBMC-WMM: 0.04sec
CBMC-SC: ERROR/TIMEOUT[]
dump-c failed with exit code 11
Cycles
SatAbs: ERROR/TIMEOUT[]


Satabs-prefix-first: ERROR/TIMEOUT[]
CBMC-WMM: 0.02sec
CBMC-SC: ERROR/TIMEOUT[]
dump-c failed with exit code 11
Cycles
SatAbs: ERROR/TIMEOUT[]


Satabs-prefix-first: ERROR/TIMEOUT[]
CBMC-WMM: 0.04sec
CBMC-SC: ERROR/TIMEOUT[]
dump-c failed with exit code 11
UNKNOWN Cycles
SatAbs:
0.05sec (x.01)

Satabs-prefix-first: 0.02sec
CBMC-WMM: 0.04sec
CBMC-SC: 0.04sec
dump-c failed with exit code 134
Cycles
SatAbs:
0.02sec (x0)

Satabs-prefix-first: 0.02sec
CBMC-WMM: 0.02sec
CBMC-SC: 0.02sec
dump-c failed with exit code 134
Cycles
SatAbs:
0.01sec (x0)

Satabs-prefix-first: 0.02sec
CBMC-WMM: 0.02sec
CBMC-SC: 0.03sec
dump-c failed with exit code 134
UNKNOWN Cycles
SatAbs: ERROR/TIMEOUT[]


Satabs-prefix-first: ERROR/TIMEOUT[]
CBMC-WMM: 0.03sec
CBMC-SC: ERROR/TIMEOUT[]
dump-c failed with exit code 11
Cycles
SatAbs:
0.06sec (x.01)

Satabs-prefix-first: 0.12sec
CBMC-WMM: 0.04sec
CBMC-SC: 1.08sec
dump-c failed with exit code 134
Cycles
SatAbs:
0.07sec (x.01)

Satabs-prefix-first: 0.07sec
CBMC-WMM: 0.04sec
CBMC-SC: 1.10sec
dump-c failed with exit code 134
UNKNOWN
gb_rcu_powerpc_nosync.c
SatAbs: ERROR/TIMEOUT[1]
4.35sec

Satabs-prefix-first: ERROR/TIMEOUT[1] 4.19sec
CBMC-WMM: 0.03sec
CBMC-SC: 0.04sec
dump-c failed with exit code 134
Cycles
SatAbs: ERROR/TIMEOUT[]


Satabs-prefix-first: ERROR/TIMEOUT[]
CBMC-WMM: 0.02sec
CBMC-SC: ERROR/TIMEOUT[]
dump-c failed with exit code 11
Cycles
SatAbs:
0.05sec (x.01)

Satabs-prefix-first: 0.03sec
CBMC-WMM: 0.04sec
CBMC-SC: 0.02sec
dump-c failed with exit code 134
Cycles
SatAbs:
0.06sec (x.01)

Satabs-prefix-first: 0.04sec
CBMC-WMM: 0.04sec
CBMC-SC: 0.03sec
dump-c failed with exit code 134
Cycles
SatAbs:
0.05sec (x.01)

Satabs-prefix-first: 0.04sec
CBMC-WMM: 0.04sec
CBMC-SC: 0.02sec
dump-c failed with exit code 134
UNKNOWN Cycles
SatAbs:
0.03sec (x0)

Satabs-prefix-first: 0.02sec
CBMC-WMM: 0.03sec
CBMC-SC: 0.02sec
dump-c failed with exit code 134
Cycles
SatAbs:
0.06sec (x.01)

Satabs-prefix-first: 0.01sec
CBMC-WMM: 0.04sec
CBMC-SC: 0.04sec
dump-c failed with exit code 134
Cycles
SatAbs:
0.03sec (x0)

Satabs-prefix-first: 0.01sec
CBMC-WMM: 0.04sec
CBMC-SC: 0.04sec
dump-c failed with exit code 134
UNKNOWN Cycles
SatAbs:
0.02sec (x0)

Satabs-prefix-first: 0.03sec
CBMC-WMM: 0.04sec
CBMC-SC: 0.03sec
dump-c failed with exit code 134
Cycles
SatAbs:
0.04sec (x0)

Satabs-prefix-first: 0.04sec
CBMC-WMM: 0.03sec
CBMC-SC: 0.03sec
dump-c failed with exit code 134
Cycles
SatAbs:
0.03sec (x0)

Satabs-prefix-first: 0.04sec
CBMC-WMM: 0.04sec
CBMC-SC: 0.04sec
dump-c failed with exit code 134
UNKNOWN Cycles
SatAbs:
0.12sec (x.02)

Satabs-prefix-first: 0.08sec
CBMC-WMM: 0.04sec
CBMC-SC: 1.67sec
dump-c failed with exit code 134
Cycles
SatAbs:
0.07sec (x.01)

Satabs-prefix-first: 0.11sec
CBMC-WMM: 0.03sec
CBMC-SC: 0.91sec
dump-c failed with exit code 134
Cycles
SatAbs:
0.07sec (x.01)

Satabs-prefix-first: 0.10sec
CBMC-WMM: 0.02sec
CBMC-SC: 0.88sec
dump-c failed with exit code 134
UNKNOWN
gb_rcu_x86.c
SatAbs: ERROR/TIMEOUT[1]
4.22sec

Satabs-prefix-first: ERROR/TIMEOUT[1] 4.08sec
CBMC-WMM: 0.03sec
CBMC-SC: 0.04sec
dump-c failed with exit code 134
Cycles
SatAbs: ERROR/TIMEOUT[]


Satabs-prefix-first: ERROR/TIMEOUT[]
CBMC-WMM: 0.03sec
CBMC-SC: ERROR/TIMEOUT[]
dump-c failed with exit code 11
Cycles
SatAbs:
0.04sec (x0)

Satabs-prefix-first: 0.05sec
CBMC-WMM: 0.03sec
CBMC-SC: 0.04sec
dump-c failed with exit code 134
Cycles
SatAbs:
0.05sec (x.01)

Satabs-prefix-first: 0.04sec
CBMC-WMM: 0.04sec
CBMC-SC: 0.04sec
dump-c failed with exit code 134
Cycles
SatAbs:
0.04sec (x0)

Satabs-prefix-first: 0.04sec
CBMC-WMM: 0.03sec
CBMC-SC: 0.04sec
dump-c failed with exit code 134
UNKNOWN Cycles
SatAbs:
0.05sec (x.01)

Satabs-prefix-first: 0.04sec
CBMC-WMM: 0.04sec
CBMC-SC: 0.04sec
dump-c failed with exit code 134
Cycles
SatAbs:
0.03sec (x0)

Satabs-prefix-first: 0.02sec
CBMC-WMM: 0.03sec
CBMC-SC: 0.03sec
dump-c failed with exit code 134
Cycles
SatAbs:
0.03sec (x0)

Satabs-prefix-first: 0.05sec
CBMC-WMM: 0.03sec
CBMC-SC: 0.03sec
dump-c failed with exit code 134
UNKNOWN Cycles
SatAbs:
0.04sec (x0)

Satabs-prefix-first: 0.05sec
CBMC-WMM: 0.04sec
CBMC-SC: 0.04sec
dump-c failed with exit code 134
Cycles
SatAbs:
0.04sec (x0)

Satabs-prefix-first: 0.05sec
CBMC-WMM: 0.04sec
CBMC-SC: 0.03sec
dump-c failed with exit code 134
Cycles
SatAbs:
0.01sec (x0)

Satabs-prefix-first: 0.05sec
CBMC-WMM: 0.02sec
CBMC-SC: 0.04sec
dump-c failed with exit code 134
UNKNOWN Cycles
SatAbs:
0.08sec (x.01)

Satabs-prefix-first: 0.10sec
CBMC-WMM: 0.03sec
CBMC-SC: 1.86sec
dump-c failed with exit code 134
Cycles
SatAbs:
0.08sec (x.01)

Satabs-prefix-first: 0.09sec
CBMC-WMM: 0.04sec
CBMC-SC: 0.88sec
dump-c failed with exit code 134
Cycles
SatAbs:
0.07sec (x.01)

Satabs-prefix-first: 0.12sec
CBMC-WMM: 0.04sec
CBMC-SC: 0.90sec
dump-c failed with exit code 134
UNKNOWN