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/podwr (tooling date Sun Jan 22 02:23:23 GMT 2012)
This family corresponds to litmus tests involving pairs showing that Power can reorder write-read pairs. 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/podwr000 |
SatAbs: 0.60sec Satabs-prefix-first: 0.61sec CBMC-WMM: 0.05sec CBMC-SC: 0.05sec CImpact: 0.54sec Checkfence: 0.01sec ESBMC: 0.04sec Threader-monolithic: 0.11sec Threader-owicki-gries: 0.12sec Threader-rely-guarantee: 0.12sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT MMChecker (MM: sc): 0.16sec |
Cycles
SatAbs: 10.99sec (x18.31) Satabs-prefix-first: 18.24sec CBMC-WMM: 0.08sec CBMC-SC: 5.44sec CImpact: 0.67sec ESBMC: 0.08sec Threader-monolithic: ERROR/TIMEOUT[130] 896.65sec Threader-owicki-gries: ERROR/TIMEOUT[130] 896.89sec Threader-rely-guarantee: ERROR/TIMEOUT[130] 896.54sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT MMChecker (MM: csharp): 0.19sec |
Cycles
SatAbs: 13.06sec (x21.76) Satabs-prefix-first: 24.67sec CBMC-WMM: 0.08sec CBMC-SC: 6.31sec CImpact: 0.69sec Checkfence: 0.01sec ESBMC: 0.11sec Threader-monolithic: ERROR/TIMEOUT[130] 897.14sec Threader-owicki-gries: ERROR/TIMEOUT[130] 897.17sec Threader-rely-guarantee: ERROR/TIMEOUT[130] 897.06sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT MMChecker (MM: csharp): 0.18sec |
Cycles
SatAbs: 2.60sec (x4.33) Satabs-prefix-first: 7.01sec CBMC-WMM: 0.07sec CBMC-SC: 0.85sec CImpact: 0.46sec ESBMC: 0.09sec Threader-monolithic: ERROR/TIMEOUT[1] 243.40sec Threader-owicki-gries: ERROR/TIMEOUT[1] 171.22sec Threader-rely-guarantee: ERROR/TIMEOUT[1] 205.56sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT MMChecker (MM: csharp): 0.19sec |
Cycles
SatAbs: 2.42sec (x4.03) Satabs-prefix-first: 6.64sec CBMC-WMM: 0.09sec CBMC-SC: 0.89sec CImpact: 0.52sec ESBMC: 0.07sec Threader-monolithic: ERROR/TIMEOUT[1] 162.46sec Threader-owicki-gries: ERROR/TIMEOUT[1] 184.47sec Threader-rely-guarantee: ERROR/TIMEOUT[1] 240.72sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT MMChecker (MM: csharp): 0.19sec |
Cycles
SatAbs: 11.19sec (x18.65) Satabs-prefix-first: 17.32sec CBMC-WMM: 0.08sec CBMC-SC: 5.58sec CImpact: 0.64sec ESBMC: 0.08sec Threader-monolithic: ERROR/TIMEOUT[130] 896.67sec Threader-owicki-gries: ERROR/TIMEOUT[130] 896.50sec Threader-rely-guarantee: ERROR/TIMEOUT[130] 896.18sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT Blender: |
Cycles
SatAbs: 2.67sec (x4.45) Satabs-prefix-first: 7.01sec CBMC-WMM: 0.08sec CBMC-SC: 0.85sec CImpact: 0.47sec ESBMC: 0.09sec Threader-monolithic: ERROR/TIMEOUT[1] 166.41sec Threader-owicki-gries: ERROR/TIMEOUT[1] 200.67sec Threader-rely-guarantee: ERROR/TIMEOUT[1] 241.95sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT Blender: |
Cycles
SatAbs: 2.79sec (x4.65) Satabs-prefix-first: 6.67sec CBMC-WMM: 0.08sec CBMC-SC: 0.88sec CImpact: 0.49sec ESBMC: 0.06sec Threader-monolithic: ERROR/TIMEOUT[1] 241.65sec Threader-owicki-gries: ERROR/TIMEOUT[1] 213.83sec Threader-rely-guarantee: ERROR/TIMEOUT[1] 228.67sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT Blender: |
Cycles
SatAbs: 11.23sec (x18.71) Satabs-prefix-first: 18.02sec CBMC-WMM: 0.09sec CBMC-SC: 5.74sec CImpact: 0.67sec ESBMC: 0.09sec Threader-monolithic: ERROR/TIMEOUT[130] 896.72sec Threader-owicki-gries: ERROR/TIMEOUT[130] 896.74sec Threader-rely-guarantee: ERROR/TIMEOUT[130] 896.63sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT |
Cycles
SatAbs: 2.69sec (x4.48) Satabs-prefix-first: 7.24sec CBMC-WMM: 0.07sec CBMC-SC: 0.82sec CImpact: 0.47sec ESBMC: 0.09sec Threader-monolithic: ERROR/TIMEOUT[1] 242.01sec Threader-owicki-gries: ERROR/TIMEOUT[1] 242.11sec Threader-rely-guarantee: ERROR/TIMEOUT[1] 241.71sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT |
Cycles
SatAbs: 2.48sec (x4.13) Satabs-prefix-first: 6.58sec CBMC-WMM: 0.09sec CBMC-SC: 0.80sec CImpact: 0.49sec ESBMC: 0.08sec Threader-monolithic: ERROR/TIMEOUT[1] 161.91sec Threader-owicki-gries: ERROR/TIMEOUT[1] 241.69sec Threader-rely-guarantee: ERROR/TIMEOUT[1] 199.67sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT |
Cycles
SatAbs: 11.37sec (x18.95) Satabs-prefix-first: 19.10sec CBMC-WMM: 0.09sec CBMC-SC: 5.78sec CImpact: 0.67sec ESBMC: 0.09sec Threader-monolithic: ERROR/TIMEOUT[130] 896.21sec Threader-owicki-gries: ERROR/TIMEOUT[130] 896.84sec Threader-rely-guarantee: ERROR/TIMEOUT[130] 896.90sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT |
Cycles
SatAbs: 2.45sec (x4.08) Satabs-prefix-first: 6.56sec CBMC-WMM: 0.08sec CBMC-SC: 0.84sec CImpact: 0.50sec ESBMC: 0.09sec Threader-monolithic: ERROR/TIMEOUT[1] 241.09sec Threader-owicki-gries: ERROR/TIMEOUT[1] 200.54sec Threader-rely-guarantee: ERROR/TIMEOUT[1] 222.26sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT |
Cycles
SatAbs: 2.39sec (x3.98) Satabs-prefix-first: 6.78sec CBMC-WMM: 0.08sec CBMC-SC: 0.84sec CImpact: 0.48sec ESBMC: 0.09sec Threader-monolithic: ERROR/TIMEOUT[1] 177.28sec Threader-owicki-gries: ERROR/TIMEOUT[1] 228.32sec Threader-rely-guarantee: ERROR/TIMEOUT[1] 207.11sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT |
||||
ppc/podwr001 |
SatAbs: 3.56sec Satabs-prefix-first: 1.47sec CBMC-WMM: 0.11sec CBMC-SC: 0.09sec CImpact: ERROR/TIMEOUT[8] 303.79sec Checkfence: 0.01sec ESBMC: 0.05sec Threader-monolithic: 0.14sec Threader-owicki-gries: 0.16sec Threader-rely-guarantee: 0.14sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT MMChecker (MM: sc): 0.30sec |
Cycles
SatAbs: 30.46sec (x8.55) Satabs-prefix-first: 71.28sec CBMC-WMM: 0.11sec CBMC-SC: 13.56sec CImpact: ERROR/TIMEOUT[8] 436.27sec ESBMC: 0.10sec Threader-monolithic: ERROR/TIMEOUT[130] 897.43sec Threader-owicki-gries: ERROR/TIMEOUT[130] 897.13sec Threader-rely-guarantee: ERROR/TIMEOUT[130] 897.24sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT MMChecker (MM: csharp): 1.49sec |
Cycles
SatAbs: 31.96sec (x8.97) Satabs-prefix-first: 73.46sec CBMC-WMM: 0.12sec CBMC-SC: 12.40sec CImpact: ERROR/TIMEOUT[8] 451.65sec Checkfence: 0.01sec ESBMC: 0.12sec Threader-monolithic: ERROR/TIMEOUT[130] 896.88sec Threader-owicki-gries: ERROR/TIMEOUT[130] 897.03sec Threader-rely-guarantee: ERROR/TIMEOUT[130] 896.80sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT MMChecker (MM: csharp): 1.49sec |
Cycles
SatAbs: 9.33sec (x2.62) Satabs-prefix-first: 20.12sec CBMC-WMM: 0.12sec CBMC-SC: 1.18sec CImpact: ERROR/TIMEOUT[8] 364.15sec ESBMC: 0.09sec Threader-monolithic: ERROR/TIMEOUT[1] 253.10sec Threader-owicki-gries: ERROR/TIMEOUT[1] 239.82sec Threader-rely-guarantee: ERROR/TIMEOUT[1] 203.87sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT MMChecker (MM: csharp): 1.60sec |
Cycles
SatAbs: 9.83sec (x2.76) Satabs-prefix-first: 21.97sec CBMC-WMM: 0.15sec CBMC-SC: 1.26sec CImpact: ERROR/TIMEOUT[8] 308.80sec ESBMC: 0.08sec Threader-monolithic: ERROR/TIMEOUT[1] 242.03sec Threader-owicki-gries: ERROR/TIMEOUT[1] 205.67sec Threader-rely-guarantee: ERROR/TIMEOUT[1] 193.04sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT MMChecker (MM: csharp): 1.51sec |
Cycles
SatAbs: 31.73sec (x8.91) Satabs-prefix-first: 73.80sec CBMC-WMM: 0.13sec CBMC-SC: 13.66sec CImpact: ERROR/TIMEOUT[8] 318.35sec ESBMC: 0.12sec Threader-monolithic: ERROR/TIMEOUT[130] 896.82sec Threader-owicki-gries: ERROR/TIMEOUT[130] 896.83sec Threader-rely-guarantee: ERROR/TIMEOUT[130] 896.95sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT Blender: |
Cycles
SatAbs: 10.64sec (x2.98) Satabs-prefix-first: 23.02sec CBMC-WMM: 0.14sec CBMC-SC: 1.19sec CImpact: ERROR/TIMEOUT[8] 262.96sec ESBMC: 0.08sec Threader-monolithic: ERROR/TIMEOUT[1] 258.91sec Threader-owicki-gries: ERROR/TIMEOUT[1] 239.55sec Threader-rely-guarantee: ERROR/TIMEOUT[1] 229.01sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT Blender: |
Cycles
SatAbs: 11.72sec (x3.29) Satabs-prefix-first: 24.00sec CBMC-WMM: 0.13sec CBMC-SC: 1.27sec CImpact: ERROR/TIMEOUT[8] 342.65sec ESBMC: 0.08sec Threader-monolithic: ERROR/TIMEOUT[1] 206.88sec Threader-owicki-gries: ERROR/TIMEOUT[1] 203.96sec Threader-rely-guarantee: ERROR/TIMEOUT[1] 201.01sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT Blender: |
Cycles
SatAbs: 35.40sec (x9.94) Satabs-prefix-first: 81.16sec CBMC-WMM: 0.18sec CBMC-SC: 14.97sec CImpact: ERROR/TIMEOUT[8] 396.36sec ESBMC: 0.13sec Threader-monolithic: ERROR/TIMEOUT[130] 896.62sec Threader-owicki-gries: ERROR/TIMEOUT[130] 896.99sec Threader-rely-guarantee: ERROR/TIMEOUT[130] 896.98sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT |
Cycles
SatAbs: 9.45sec (x2.65) Satabs-prefix-first: 26.17sec CBMC-WMM: 0.16sec CBMC-SC: 1.24sec CImpact: ERROR/TIMEOUT[8] 233.07sec ESBMC: 0.08sec Threader-monolithic: ERROR/TIMEOUT[1] 261.12sec Threader-owicki-gries: ERROR/TIMEOUT[1] 260.58sec Threader-rely-guarantee: ERROR/TIMEOUT[1] 228.20sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT |
Cycles
SatAbs: 10.02sec (x2.81) Satabs-prefix-first: 21.59sec CBMC-WMM: 0.15sec CBMC-SC: 1.20sec CImpact: ERROR/TIMEOUT[8] 251.37sec ESBMC: 0.08sec Threader-monolithic: ERROR/TIMEOUT[1] 243.34sec Threader-owicki-gries: ERROR/TIMEOUT[1] 264.28sec Threader-rely-guarantee: ERROR/TIMEOUT[1] 180.03sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT |
Cycles
SatAbs: 31.59sec (x8.87) Satabs-prefix-first: 74.59sec CBMC-WMM: 0.15sec CBMC-SC: 13.94sec CImpact: ERROR/TIMEOUT[8] 464.28sec ESBMC: 0.10sec Threader-monolithic: ERROR/TIMEOUT[130] 897.10sec Threader-owicki-gries: ERROR/TIMEOUT[130] 896.87sec Threader-rely-guarantee: ERROR/TIMEOUT[130] 896.20sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT |
Cycles
SatAbs: 9.77sec (x2.74) Satabs-prefix-first: 20.92sec CBMC-WMM: 0.15sec CBMC-SC: 1.16sec CImpact: ERROR/TIMEOUT[8] 378.97sec ESBMC: 0.09sec Threader-monolithic: ERROR/TIMEOUT[1] 257.07sec Threader-owicki-gries: ERROR/TIMEOUT[1] 263.28sec Threader-rely-guarantee: ERROR/TIMEOUT[1] 263.17sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT |
Cycles
SatAbs: 9.45sec (x2.65) Satabs-prefix-first: 19.35sec CBMC-WMM: 0.12sec CBMC-SC: 1.17sec CImpact: ERROR/TIMEOUT[8] 339.73sec ESBMC: 0.09sec Threader-monolithic: ERROR/TIMEOUT[1] 254.78sec Threader-owicki-gries: ERROR/TIMEOUT[1] 212.20sec Threader-rely-guarantee: ERROR/TIMEOUT[1] 263.27sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT |