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

...
  ...  

Borrowed C Programs

This family contains the bug found by Sebastian Burckhart and Madan Musuvathi with their Sober tool, presented in their CAV 2008 paper, and our own fix for it.

It should answer Yes in litmus terms, or Verification Failed in verification terms, starting from x86/TSO. Its fixed version should answer No in litmus terms, or Verification Successful in verification terms, regardless of the model.

All tools successfully check the code and its fix for SC, as expected. SatAbs fails to verify the buggy code on all models, as expected, and verifies its fix on all models, as expected. CImpact times out on every model for both the initial buggy code and its fix. ESBMC claims to verify the buggy code on all models, and successfully verifies its fix on all models. Threader aborts on both the initial code and its fix for all models (more precisely, the error message is "Fatal error: exception Failure("Error: nesting atomic blocks!")).

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)
sober.c
SatAbs:
0.36sec

CImpact: 2.54sec
ESBMC: 1.21sec
Threader: ERROR/TIMEOUT[1] 0.10sec
Poirot-Integer: 569.21875 s
Poirot-BitVector: ERROR/TIMEOUT
C code
Cycles
SatAbs:
1.55sec (x4.30)

CImpact: ERROR/TIMEOUT[8] 178.47sec
ESBMC: ERROR/TIMEOUT[130]
Threader: ERROR/TIMEOUT[1] 0.07sec
Poirot-Integer: ERROR/TIMEOUT
Poirot-BitVector: ERROR/TIMEOUT
Instrumented C code
Cycles
SatAbs:
1.06sec (x2.94)

CImpact: ERROR/TIMEOUT[8] 155.79sec
ESBMC: 858.55sec
Threader: ERROR/TIMEOUT[1] 0.09sec
Poirot-Integer: ERROR/TIMEOUT
Poirot-BitVector: ERROR/TIMEOUT
Instrumented C code
Cycles
SatAbs:
1.51sec (x4.19)

CImpact: ERROR/TIMEOUT[8] 179.77sec
ESBMC: ERROR/TIMEOUT[130]
Threader: ERROR/TIMEOUT[1] 0.08sec
Poirot-Integer: ERROR/TIMEOUT
Poirot-BitVector: ERROR/TIMEOUT
Instrumented C code
Cycles
SatAbs:
0.89sec (x2.47)

CImpact: ERROR/TIMEOUT[8] 155.26sec
ESBMC: 857.89sec
Threader: ERROR/TIMEOUT[1] 0.07sec
Poirot-Integer: ERROR/TIMEOUT
Poirot-BitVector: ERROR/TIMEOUT
Instrumented C code
Cycles
SatAbs:
1.47sec (x4.08)

CImpact: ERROR/TIMEOUT[8] 179.21sec
ESBMC: ERROR/TIMEOUT[130]
Threader: ERROR/TIMEOUT[1] 0.08sec
Poirot-Integer: ERROR/TIMEOUT
Poirot-BitVector: ERROR/TIMEOUT
Instrumented C code
Cycles
SatAbs:
0.94sec (x2.61)

CImpact: ERROR/TIMEOUT[8] 155.74sec
ESBMC: 859.29sec
Threader: ERROR/TIMEOUT[1] 0.08sec
Poirot-Integer: ERROR/TIMEOUT
Poirot-BitVector: ERROR/TIMEOUT
Instrumented C code
Cycles
SatAbs:
1.39sec (x3.86)

CImpact: ERROR/TIMEOUT[8] 198.63sec
ESBMC: ERROR/TIMEOUT[130]
Threader: ERROR/TIMEOUT[1] 0.07sec
Poirot-Integer: ERROR/TIMEOUT
Poirot-BitVector: ERROR/TIMEOUT
Instrumented C code
Cycles
SatAbs:
0.89sec (x2.47)

CImpact: ERROR/TIMEOUT[8] 153.62sec
ESBMC: 750.06sec
Threader: ERROR/TIMEOUT[1] 0.06sec
Poirot-Integer: ERROR/TIMEOUT
Poirot-BitVector: ERROR/TIMEOUT
Instrumented C code
sober-fixed.c
SatAbs:
0.33sec

CImpact: 2.56sec
ESBMC: 1.27sec
Threader: ERROR/TIMEOUT[1] 0.10sec
Poirot-Integer: 568.109375 s
Poirot-BitVector: ERROR/TIMEOUT
C code
Cycles
SatAbs:
2.54sec (x7.69)

CImpact: ERROR/TIMEOUT[8] 111.82sec
ESBMC: ERROR/TIMEOUT[130]
Threader: ERROR/TIMEOUT[1] 0.08sec
Poirot-Integer: 898.921875 s
Poirot-BitVector: ERROR/TIMEOUT
Instrumented C code
Cycles
SatAbs:
2.11sec (x6.39)

CImpact: ERROR/TIMEOUT[8] 109.23sec
ESBMC: ERROR/TIMEOUT[130]
Threader: ERROR/TIMEOUT[1] 0.07sec
Poirot-Integer: 897.84375 s
Poirot-BitVector: ERROR/TIMEOUT
Instrumented C code
Cycles
SatAbs:
1.91sec (x5.78)

CImpact: ERROR/TIMEOUT[8] 112.75sec
ESBMC: ERROR/TIMEOUT[130]
Threader: ERROR/TIMEOUT[1] 0.06sec
Poirot-Integer: 897.109375 s
Poirot-BitVector: ERROR/TIMEOUT
Instrumented C code
Cycles
SatAbs:
2.12sec (x6.42)

CImpact: ERROR/TIMEOUT[8] 112.77sec
ESBMC: ERROR/TIMEOUT[130]
Threader: ERROR/TIMEOUT[1] 0.08sec
Poirot-Integer: 898.390625 s
Poirot-BitVector: ERROR/TIMEOUT
Instrumented C code
Cycles
SatAbs:
2.92sec (x8.84)

CImpact: ERROR/TIMEOUT[8] 112.38sec
ESBMC: ERROR/TIMEOUT[130]
Threader: ERROR/TIMEOUT[1] 0.07sec
Poirot-Integer: 899.984375 s
Poirot-BitVector: ERROR/TIMEOUT
Instrumented C code
Cycles
SatAbs:
2.45sec (x7.42)

CImpact: ERROR/TIMEOUT[8] 111.62sec
ESBMC: ERROR/TIMEOUT[130]
Threader: ERROR/TIMEOUT[1] 0.09sec
Poirot-Integer: 897.921875 s
Poirot-BitVector: ERROR/TIMEOUT
Instrumented C code
Cycles
SatAbs:
2.17sec (x6.57)

CImpact: ERROR/TIMEOUT[8] 109.42sec
ESBMC: ERROR/TIMEOUT[130]
Threader: ERROR/TIMEOUT[1] 0.06sec
Poirot-Integer: 897.65625 s
Poirot-BitVector: ERROR/TIMEOUT
Instrumented C code
Cycles
SatAbs:
2.63sec (x7.96)

CImpact: ERROR/TIMEOUT[8] 111.98sec
ESBMC: ERROR/TIMEOUT[130]
Threader: ERROR/TIMEOUT[1] 0.06sec
Poirot-Integer: 898.078125 s
Poirot-BitVector: ERROR/TIMEOUT
Instrumented C code