How to read the tables?
Meaning of the model-checker's resultsModel-checker on the instrumented program | Observed state in Litmus | Picture |
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.
- In the first column, we can read the name of the original Litmus test (with a link to the file), and the expected violation cycle. The second column gathers the results of the model-checkers for SC. As we are interested in WMM bugs, the verification for SC should be .
- The three next columns concern TSO model. The last column tells which result we should get for this program under TSO, namely . We see in the third column that Satabs indeed finds the correct result when checking the instrumented program. ESBMC in this example is missing the counterexample. Threader is either returning an error, or killed by timeout (here, it is an error).
- Note that there are two columns for TSO results: in the first one, we instrument all the delays; in the second one, we instrument only one delay per cycle.
- We also experiment under PSO, RMO and Power, and with additional model-checkers: additional columns of results (and expected results) appear after TSO's columns.
Name | SC | TSO (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 ... |
... |
ppc/bclwsww (tooling date Sun Jan 22 02:23:23 GMT 2012)
This family corresponds to litmus tests involving pairs showing that Power's lwsync barrier cannot enforce a B-cumulative ordering when placed between two writes. Therefore they should answer Yes in litmus terms, or Verification Failed in verification terms as soon as the model is Power.
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) |
ppc/bclwsww000 |
SatAbs: 49.05sec Satabs-prefix-first: 54.45sec CBMC-WMM: 0.16sec CBMC-SC: 0.16sec CImpact: ERROR/TIMEOUT[8] 249.82sec Checkfence: 0.01sec ESBMC: 0.07sec Threader-monolithic: 0.18sec Threader-owicki-gries: 0.16sec Threader-rely-guarantee: 0.18sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT MMChecker (MM: sc): ERROR/TIMEOUT[1] 0.10sec |
Cycles
SatAbs: 3.70sec (x.07) Satabs-prefix-first: 5.17sec CBMC-WMM: 0.40sec CBMC-SC: 42.80sec CImpact: 0.02sec ESBMC: 0.12sec Threader-monolithic: ERROR/TIMEOUT[130] 897.55sec Threader-owicki-gries: ERROR/TIMEOUT[130] 897.59sec Threader-rely-guarantee: ERROR/TIMEOUT[130] 897.58sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT MMChecker (MM: csharp): ERROR/TIMEOUT[1] 0.10sec |
Cycles
SatAbs: 126.20sec (x2.57) Satabs-prefix-first: 77.33sec CBMC-WMM: 0.39sec CBMC-SC: 0.13sec CImpact: ERROR/TIMEOUT[8] 394.56sec Checkfence: 0.01sec ESBMC: 0.06sec Threader-monolithic: ERROR/TIMEOUT[1] 0.14sec Threader-owicki-gries: ERROR/TIMEOUT[1] 0.12sec Threader-rely-guarantee: ERROR/TIMEOUT[1] 0.14sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT MMChecker (MM: csharp): ERROR/TIMEOUT[1] 0.09sec |
Cycles
SatAbs: 131.71sec (x2.68) Satabs-prefix-first: 75.48sec CBMC-WMM: 0.40sec CBMC-SC: 0.12sec CImpact: ERROR/TIMEOUT[8] 332.72sec ESBMC: 0.07sec Threader-monolithic: ERROR/TIMEOUT[1] 0.15sec Threader-owicki-gries: ERROR/TIMEOUT[1] 0.15sec Threader-rely-guarantee: ERROR/TIMEOUT[1] 0.13sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT MMChecker (MM: csharp): ERROR/TIMEOUT[1] 0.10sec |
Cycles
SatAbs: 135.46sec (x2.76) Satabs-prefix-first: 84.86sec CBMC-WMM: 0.44sec CBMC-SC: 0.12sec CImpact: ERROR/TIMEOUT[8] 394.84sec ESBMC: 0.08sec Threader-monolithic: ERROR/TIMEOUT[1] 0.14sec Threader-owicki-gries: ERROR/TIMEOUT[1] 0.15sec Threader-rely-guarantee: ERROR/TIMEOUT[1] 0.15sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT MMChecker (MM: csharp): ERROR/TIMEOUT[1] 0.10sec |
Cycles
SatAbs: 129.68sec (x2.64) Satabs-prefix-first: 77.93sec CBMC-WMM: 0.42sec CBMC-SC: 0.12sec CImpact: ERROR/TIMEOUT[8] 342.17sec ESBMC: 0.07sec Threader-monolithic: ERROR/TIMEOUT[1] 0.15sec Threader-owicki-gries: ERROR/TIMEOUT[1] 0.14sec Threader-rely-guarantee: ERROR/TIMEOUT[1] 0.14sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT Blender: |
Cycles
SatAbs: 131.47sec (x2.68) Satabs-prefix-first: 88.34sec CBMC-WMM: 0.42sec CBMC-SC: 0.12sec CImpact: ERROR/TIMEOUT[8] 329.36sec ESBMC: 0.08sec Threader-monolithic: ERROR/TIMEOUT[1] 0.15sec Threader-owicki-gries: ERROR/TIMEOUT[1] 0.14sec Threader-rely-guarantee: ERROR/TIMEOUT[1] 0.13sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT Blender: |
Cycles
SatAbs: 129.47sec (x2.63) Satabs-prefix-first: 79.15sec CBMC-WMM: 0.41sec CBMC-SC: 0.13sec CImpact: ERROR/TIMEOUT[8] 399.87sec ESBMC: 0.08sec Threader-monolithic: ERROR/TIMEOUT[1] 0.13sec Threader-owicki-gries: ERROR/TIMEOUT[1] 0.15sec Threader-rely-guarantee: ERROR/TIMEOUT[1] 0.15sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT Blender: |
Cycles
SatAbs: 149.39sec (x3.04) Satabs-prefix-first: 77.51sec CBMC-WMM: 0.45sec CBMC-SC: 0.11sec CImpact: ERROR/TIMEOUT[8] 351.29sec ESBMC: 0.09sec Threader-monolithic: ERROR/TIMEOUT[1] 0.15sec Threader-owicki-gries: ERROR/TIMEOUT[1] 0.13sec Threader-rely-guarantee: ERROR/TIMEOUT[1] 0.14sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT |
Cycles
SatAbs: 132.35sec (x2.69) Satabs-prefix-first: 76.78sec CBMC-WMM: 0.44sec CBMC-SC: 0.13sec CImpact: ERROR/TIMEOUT[8] 346.87sec ESBMC: 0.07sec Threader-monolithic: ERROR/TIMEOUT[1] 0.13sec Threader-owicki-gries: ERROR/TIMEOUT[1] 0.12sec Threader-rely-guarantee: ERROR/TIMEOUT[1] 0.14sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT |
Cycles
SatAbs: 136.51sec (x2.78) Satabs-prefix-first: 82.97sec CBMC-WMM: 0.47sec CBMC-SC: 0.11sec CImpact: ERROR/TIMEOUT[8] 408.29sec ESBMC: 0.09sec Threader-monolithic: ERROR/TIMEOUT[1] 0.15sec Threader-owicki-gries: ERROR/TIMEOUT[1] 0.15sec Threader-rely-guarantee: ERROR/TIMEOUT[1] 0.14sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT |
Cycles
SatAbs: 50.64sec (x1.03) Satabs-prefix-first: 87.58sec CBMC-WMM: 0.30sec CBMC-SC: 295.32sec CImpact: 0.02sec ESBMC: 0.15sec Threader-monolithic: ERROR/TIMEOUT[130] 897.73sec Threader-owicki-gries: ERROR/TIMEOUT[130] 897.79sec Threader-rely-guarantee: ERROR/TIMEOUT[130] 897.78sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT |
Cycles
SatAbs: 3.37sec (x.06) Satabs-prefix-first: 7.45sec CBMC-WMM: 0.32sec CBMC-SC: 10.46sec CImpact: 0.01sec ESBMC: 0.10sec Threader-monolithic: ERROR/TIMEOUT[130] 897.34sec Threader-owicki-gries: ERROR/TIMEOUT[130] 896.88sec Threader-rely-guarantee: ERROR/TIMEOUT[130] 897.53sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT |
Cycles
SatAbs: 180.17sec (x3.67) Satabs-prefix-first: 11.72sec CBMC-WMM: 0.28sec CBMC-SC: 6.30sec CImpact: 0.02sec ESBMC: 0.11sec Threader-monolithic: ERROR/TIMEOUT[130] 897.12sec Threader-owicki-gries: ERROR/TIMEOUT[130] 897.45sec Threader-rely-guarantee: ERROR/TIMEOUT[130] 897.42sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT |