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/podrw (tooling date Sun Jan 22 02:23:23 GMT 2012)
This family corresponds to litmus tests involving pairs showing that Power can reorder read-write 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/podrw000 |
SatAbs: 0.40sec Satabs-prefix-first: 0.52sec CBMC-WMM: 0.04sec CBMC-SC: 0.05sec CImpact: 1.26sec Checkfence: 0.01sec ESBMC: 0.05sec Threader-monolithic: 0.12sec Threader-owicki-gries: 0.13sec Threader-rely-guarantee: 0.11sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT MMChecker (MM: sc): 0.16sec |
Cycles
SatAbs: 1.61sec (x4.02) Satabs-prefix-first: 1.69sec CBMC-WMM: 0.09sec CBMC-SC: 8.41sec CImpact: 21.55sec ESBMC: 0.10sec Threader-monolithic: ERROR/TIMEOUT[130] 897.35sec Threader-owicki-gries: ERROR/TIMEOUT[130] 897.36sec Threader-rely-guarantee: ERROR/TIMEOUT[130] 897.32sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT MMChecker (MM: csharp): 0.17sec |
Cycles
SatAbs: 1.35sec (x3.37) Satabs-prefix-first: 1.60sec CBMC-WMM: 0.08sec CBMC-SC: 0.05sec CImpact: 75.75sec Checkfence: 0.00sec ESBMC: 0.05sec Threader-monolithic: ERROR/TIMEOUT[1] 0.10sec Threader-owicki-gries: ERROR/TIMEOUT[1] 0.10sec Threader-rely-guarantee: ERROR/TIMEOUT[1] 0.11sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT MMChecker (MM: csharp): 0.18sec |
Cycles
SatAbs: 1.23sec (x3.07) Satabs-prefix-first: 1.74sec CBMC-WMM: 0.07sec CBMC-SC: 0.05sec CImpact: 73.96sec ESBMC: 0.06sec Threader-monolithic: ERROR/TIMEOUT[1] 0.10sec Threader-owicki-gries: ERROR/TIMEOUT[1] 0.12sec Threader-rely-guarantee: ERROR/TIMEOUT[1] 0.11sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT MMChecker (MM: csharp): 0.24sec |
Cycles
SatAbs: 1.96sec (x4.90) Satabs-prefix-first: 2.93sec CBMC-WMM: 0.11sec CBMC-SC: 0.05sec CImpact: 53.19sec ESBMC: 0.08sec Threader-monolithic: ERROR/TIMEOUT[1] 0.10sec Threader-owicki-gries: ERROR/TIMEOUT[1] 0.11sec Threader-rely-guarantee: ERROR/TIMEOUT[1] 0.11sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT MMChecker (MM: csharp): 0.18sec |
Cycles
SatAbs: 1.05sec (x2.62) Satabs-prefix-first: 1.85sec CBMC-WMM: 0.10sec CBMC-SC: 0.05sec CImpact: 78.98sec ESBMC: 0.06sec Threader-monolithic: ERROR/TIMEOUT[1] 0.09sec Threader-owicki-gries: ERROR/TIMEOUT[1] 0.09sec Threader-rely-guarantee: ERROR/TIMEOUT[1] 0.07sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT Blender: |
Cycles
SatAbs: 1.27sec (x3.17) Satabs-prefix-first: 1.75sec CBMC-WMM: 0.10sec CBMC-SC: 0.05sec CImpact: 70.71sec ESBMC: 0.06sec Threader-monolithic: ERROR/TIMEOUT[1] 0.10sec Threader-owicki-gries: ERROR/TIMEOUT[1] 0.11sec Threader-rely-guarantee: ERROR/TIMEOUT[1] 0.09sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT Blender: |
Cycles
SatAbs: 1.08sec (x2.70) Satabs-prefix-first: 1.78sec CBMC-WMM: 0.09sec CBMC-SC: 0.05sec CImpact: 75.94sec ESBMC: 0.07sec Threader-monolithic: ERROR/TIMEOUT[1] 0.11sec Threader-owicki-gries: ERROR/TIMEOUT[1] 0.10sec Threader-rely-guarantee: ERROR/TIMEOUT[1] 0.12sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT Blender: |
Cycles
SatAbs: 12.55sec (x31.37) Satabs-prefix-first: 5.27sec CBMC-WMM: 0.11sec CBMC-SC: 0.64sec CImpact: 27.58sec ESBMC: 0.09sec Threader-monolithic: ERROR/TIMEOUT[1] 264.26sec Threader-owicki-gries: ERROR/TIMEOUT[1] 374.24sec Threader-rely-guarantee: ERROR/TIMEOUT[1] 290.41sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT |
Cycles
SatAbs: 12.16sec (x30.40) Satabs-prefix-first: 4.88sec CBMC-WMM: 0.09sec CBMC-SC: 0.63sec CImpact: 27.66sec ESBMC: 0.08sec Threader-monolithic: ERROR/TIMEOUT[1] 277.91sec Threader-owicki-gries: ERROR/TIMEOUT[1] 330.17sec Threader-rely-guarantee: ERROR/TIMEOUT[1] 275.19sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT |
Cycles
SatAbs: 12.75sec (x31.87) Satabs-prefix-first: 5.18sec CBMC-WMM: 0.10sec CBMC-SC: 0.57sec CImpact: 27.74sec ESBMC: 0.08sec Threader-monolithic: ERROR/TIMEOUT[1] 344.60sec Threader-owicki-gries: ERROR/TIMEOUT[1] 360.62sec Threader-rely-guarantee: ERROR/TIMEOUT[1] 375.99sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT |
Cycles
SatAbs: 72.58sec (x181.45) Satabs-prefix-first: 138.77sec CBMC-WMM: 0.10sec CBMC-SC: 1.91sec CImpact: 52.67sec ESBMC: 0.11sec Threader-monolithic: ERROR/TIMEOUT[130] 897.60sec Threader-owicki-gries: ERROR/TIMEOUT[130] 897.31sec Threader-rely-guarantee: ERROR/TIMEOUT[130] 897.47sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT |
Cycles
SatAbs: 10.42sec (x26.05) Satabs-prefix-first: 5.23sec CBMC-WMM: 0.11sec CBMC-SC: 0.81sec CImpact: 30.06sec ESBMC: 0.08sec Threader-monolithic: ERROR/TIMEOUT[1] 301.28sec Threader-owicki-gries: ERROR/TIMEOUT[1] 374.67sec Threader-rely-guarantee: ERROR/TIMEOUT[1] 375.62sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT |
Cycles
SatAbs: 10.67sec (x26.67) Satabs-prefix-first: 5.07sec CBMC-WMM: 0.10sec CBMC-SC: 0.78sec CImpact: 27.66sec ESBMC: 0.09sec Threader-monolithic: ERROR/TIMEOUT[1] 261.40sec Threader-owicki-gries: ERROR/TIMEOUT[1] 332.41sec Threader-rely-guarantee: ERROR/TIMEOUT[1] 313.42sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT |
||||
ppc/podrw001 |
SatAbs: 0.78sec Satabs-prefix-first: 0.70sec CBMC-WMM: 0.04sec CBMC-SC: 0.08sec CImpact: ERROR/TIMEOUT[8] 306.66sec Checkfence: 0.01sec ESBMC: 0.07sec Threader-monolithic: 0.16sec Threader-owicki-gries: 0.15sec Threader-rely-guarantee: 0.14sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT MMChecker (MM: sc): 0.36sec |
Cycles
SatAbs: 9.41sec (x12.06) Satabs-prefix-first: 17.77sec CBMC-WMM: 0.15sec CBMC-SC: 50.44sec CImpact: ERROR/TIMEOUT[8] 324.51sec ESBMC: 0.12sec Threader-monolithic: ERROR/TIMEOUT[130] 896.65sec Threader-owicki-gries: ERROR/TIMEOUT[130] 897.50sec Threader-rely-guarantee: ERROR/TIMEOUT[130] 897.01sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT MMChecker (MM: csharp): 0.49sec |
Cycles
SatAbs: 2.96sec (x3.79) Satabs-prefix-first: 4.78sec CBMC-WMM: 0.15sec CBMC-SC: 0.06sec CImpact: ERROR/TIMEOUT[8] 276.34sec Checkfence: 0.01sec ESBMC: 0.06sec Threader-monolithic: ERROR/TIMEOUT[1] 0.11sec Threader-owicki-gries: ERROR/TIMEOUT[1] 0.11sec Threader-rely-guarantee: ERROR/TIMEOUT[1] 0.12sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT MMChecker (MM: csharp): 0.48sec |
Cycles
SatAbs: 2.80sec (x3.58) Satabs-prefix-first: 4.65sec CBMC-WMM: 0.16sec CBMC-SC: 0.05sec CImpact: ERROR/TIMEOUT[8] 338.31sec ESBMC: 0.11sec Threader-monolithic: ERROR/TIMEOUT[1] 0.12sec Threader-owicki-gries: ERROR/TIMEOUT[1] 0.10sec Threader-rely-guarantee: ERROR/TIMEOUT[1] 0.11sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT MMChecker (MM: csharp): 0.49sec |
Cycles
SatAbs: 2.96sec (x3.79) Satabs-prefix-first: 4.84sec CBMC-WMM: 0.14sec CBMC-SC: 0.08sec CImpact: ERROR/TIMEOUT[8] 346.33sec ESBMC: 0.06sec Threader-monolithic: ERROR/TIMEOUT[1] 0.12sec Threader-owicki-gries: ERROR/TIMEOUT[1] 0.11sec Threader-rely-guarantee: ERROR/TIMEOUT[1] 0.12sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT MMChecker (MM: csharp): 0.49sec |
Cycles
SatAbs: 2.90sec (x3.71) Satabs-prefix-first: 4.34sec CBMC-WMM: 0.16sec CBMC-SC: 0.07sec CImpact: ERROR/TIMEOUT[8] 355.88sec ESBMC: 0.07sec Threader-monolithic: ERROR/TIMEOUT[1] 0.11sec Threader-owicki-gries: ERROR/TIMEOUT[1] 0.11sec Threader-rely-guarantee: ERROR/TIMEOUT[1] 0.11sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT Blender: |
Cycles
SatAbs: 3.07sec (x3.93) Satabs-prefix-first: 4.74sec CBMC-WMM: 0.14sec CBMC-SC: 0.07sec CImpact: ERROR/TIMEOUT[8] 347.96sec ESBMC: 0.06sec Threader-monolithic: ERROR/TIMEOUT[1] 0.12sec Threader-owicki-gries: ERROR/TIMEOUT[1] 0.10sec Threader-rely-guarantee: ERROR/TIMEOUT[1] 0.09sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT Blender: |
Cycles
SatAbs: 2.98sec (x3.82) Satabs-prefix-first: 4.65sec CBMC-WMM: 0.16sec CBMC-SC: 0.07sec CImpact: ERROR/TIMEOUT[8] 251.98sec ESBMC: 0.07sec Threader-monolithic: ERROR/TIMEOUT[1] 0.09sec Threader-owicki-gries: ERROR/TIMEOUT[1] 0.11sec Threader-rely-guarantee: ERROR/TIMEOUT[1] 0.11sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT Blender: |
Cycles
SatAbs: 25.76sec (x33.02) Satabs-prefix-first: 25.50sec CBMC-WMM: 0.14sec CBMC-SC: 0.77sec CImpact: ERROR/TIMEOUT[8] 327.91sec ESBMC: 0.09sec Threader-monolithic: ERROR/TIMEOUT[1] 344.01sec Threader-owicki-gries: ERROR/TIMEOUT[1] 442.39sec Threader-rely-guarantee: ERROR/TIMEOUT[1] 445.68sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT |
Cycles
SatAbs: 25.65sec (x32.88) Satabs-prefix-first: 24.78sec CBMC-WMM: 0.14sec CBMC-SC: 0.73sec CImpact: ERROR/TIMEOUT[8] 320.53sec ESBMC: 0.15sec Threader-monolithic: ERROR/TIMEOUT[1] 415.22sec Threader-owicki-gries: ERROR/TIMEOUT[1] 327.37sec Threader-rely-guarantee: ERROR/TIMEOUT[1] 396.55sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT |
Cycles
SatAbs: 26.68sec (x34.20) Satabs-prefix-first: 33.68sec CBMC-WMM: 0.22sec CBMC-SC: 1.23sec CImpact: ERROR/TIMEOUT[8] 240.69sec ESBMC: 0.08sec Threader-monolithic: ERROR/TIMEOUT[1] 398.35sec Threader-owicki-gries: ERROR/TIMEOUT[1] 358.41sec Threader-rely-guarantee: ERROR/TIMEOUT[1] 366.67sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT |
Cycles
SatAbs: 612.85sec (x785.70) Satabs-prefix-first: 910.46sec CBMC-WMM: 0.16sec CBMC-SC: 5.24sec CImpact: ERROR/TIMEOUT[8] 307.79sec ESBMC: 0.09sec Threader-monolithic: ERROR/TIMEOUT[130] 897.41sec Threader-owicki-gries: ERROR/TIMEOUT[130] 897.32sec Threader-rely-guarantee: ERROR/TIMEOUT[130] 897.42sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT |
Cycles
SatAbs: 37.50sec (x48.07) Satabs-prefix-first: 22.40sec CBMC-WMM: 0.16sec CBMC-SC: 1.15sec CImpact: ERROR/TIMEOUT[8] 271.30sec ESBMC: 0.10sec Threader-monolithic: ERROR/TIMEOUT[1] 344.34sec Threader-owicki-gries: ERROR/TIMEOUT[1] 328.33sec Threader-rely-guarantee: ERROR/TIMEOUT[1] 444.04sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT |
Cycles
SatAbs: 39.08sec (x50.10) Satabs-prefix-first: 22.86sec CBMC-WMM: 0.15sec CBMC-SC: 1.11sec CImpact: ERROR/TIMEOUT[8] 301.60sec ESBMC: 0.07sec Threader-monolithic: ERROR/TIMEOUT[1] 413.14sec Threader-owicki-gries: ERROR/TIMEOUT[1] 449.85sec Threader-rely-guarantee: ERROR/TIMEOUT[1] 374.38sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT |