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/lwswr (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 any ordering when placed between a write and a read. 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/lwswr000 |
SatAbs: 37.37sec Satabs-prefix-first: 75.72sec CBMC-WMM: 0.14sec CBMC-SC: 0.15sec CImpact: ERROR/TIMEOUT[8] 401.59sec Checkfence: 0.01sec ESBMC: 0.07sec Threader-monolithic: 0.19sec Threader-owicki-gries: 0.21sec Threader-rely-guarantee: 0.19sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT MMChecker (MM: sc): ERROR/TIMEOUT[1] 0.24sec |
Cycles
SatAbs: 3.64sec (x.09) Satabs-prefix-first: 4.49sec CBMC-WMM: 0.35sec CBMC-SC: 108.43sec CImpact: 3.37sec ESBMC: 0.13sec Threader-monolithic: ERROR/TIMEOUT[130] 638.60sec Threader-owicki-gries: ERROR/TIMEOUT[130] 613.37sec Threader-rely-guarantee: ERROR/TIMEOUT[130] 710.53sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT MMChecker (MM: csharp): ERROR/TIMEOUT[1] 0.23sec |
Cycles
SatAbs: ERROR/TIMEOUT[130] 787.83sec (x21.08) Satabs-prefix-first: ERROR/TIMEOUT[130] 693.47sec CBMC-WMM: 0.36sec CBMC-SC: 156.17sec CImpact: ERROR/TIMEOUT[8] 601.04sec Checkfence: 0.01sec ESBMC: 0.11sec Threader-monolithic: ERROR/TIMEOUT[130] 633.29sec Threader-owicki-gries: ERROR/TIMEOUT[130] 682.24sec Threader-rely-guarantee: ERROR/TIMEOUT[130] 640.16sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT MMChecker (MM: csharp): ERROR/TIMEOUT[1] 0.22sec |
Cycles
SatAbs: ERROR/TIMEOUT[130] 735.03sec (x19.66) Satabs-prefix-first: ERROR/TIMEOUT[130] 704.66sec CBMC-WMM: 0.35sec CBMC-SC: 14.39sec CImpact: ERROR/TIMEOUT[137] 319.22sec ESBMC: 0.13sec Threader-monolithic: ERROR/TIMEOUT[130] 743.04sec Threader-owicki-gries: ERROR/TIMEOUT[130] 730.78sec Threader-rely-guarantee: ERROR/TIMEOUT[130] 882.03sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT MMChecker (MM: csharp): ERROR/TIMEOUT[1] 0.39sec |
Cycles
SatAbs: ERROR/TIMEOUT[130] 811.29sec (x21.70) Satabs-prefix-first: ERROR/TIMEOUT[130] 860.37sec CBMC-WMM: 0.35sec CBMC-SC: 15.08sec CImpact: ERROR/TIMEOUT[8] 488.99sec ESBMC: 0.12sec Threader-monolithic: ERROR/TIMEOUT[130] 800.31sec Threader-owicki-gries: ERROR/TIMEOUT[130] 657.32sec Threader-rely-guarantee: ERROR/TIMEOUT[130] 665.27sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT MMChecker (MM: csharp): ERROR/TIMEOUT[1] 0.21sec |
Cycles
SatAbs: ERROR/TIMEOUT[130] 890.88sec (x23.83) Satabs-prefix-first: ERROR/TIMEOUT[130] 791.26sec CBMC-WMM: 0.36sec CBMC-SC: 150.95sec CImpact: ERROR/TIMEOUT[8] 551.04sec ESBMC: 0.14sec Threader-monolithic: ERROR/TIMEOUT[130] 897.46sec Threader-owicki-gries: ERROR/TIMEOUT[130] 897.50sec Threader-rely-guarantee: ERROR/TIMEOUT[130] 897.37sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT Blender: |
Cycles
SatAbs: ERROR/TIMEOUT[130] 1043.50sec (x27.92) Satabs-prefix-first: ERROR/TIMEOUT[130] 977.46sec CBMC-WMM: 0.39sec CBMC-SC: 143.00sec CImpact: ERROR/TIMEOUT[8] 579.46sec ESBMC: 0.15sec Threader-monolithic: ERROR/TIMEOUT[130] 897.60sec Threader-owicki-gries: ERROR/TIMEOUT[130] 897.61sec Threader-rely-guarantee: ERROR/TIMEOUT[130] 897.70sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT Blender: |
Cycles
SatAbs: ERROR/TIMEOUT[130] 1044.29sec (x27.94) Satabs-prefix-first: ERROR/TIMEOUT[130] 957.79sec CBMC-WMM: 0.34sec CBMC-SC: 138.51sec CImpact: ERROR/TIMEOUT[8] 549.59sec ESBMC: 0.12sec Threader-monolithic: ERROR/TIMEOUT[130] 897.73sec Threader-owicki-gries: ERROR/TIMEOUT[130] 897.35sec Threader-rely-guarantee: ERROR/TIMEOUT[130] 897.59sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT Blender: |
Cycles
SatAbs: ERROR/TIMEOUT[130] 1058.34sec (x28.32) Satabs-prefix-first: ERROR/TIMEOUT[130] 904.66sec CBMC-WMM: 0.43sec CBMC-SC: 130.87sec CImpact: ERROR/TIMEOUT[8] 586.89sec ESBMC: 0.16sec Threader-monolithic: ERROR/TIMEOUT[130] 897.29sec Threader-owicki-gries: ERROR/TIMEOUT[130] 896.88sec Threader-rely-guarantee: ERROR/TIMEOUT[130] 897.50sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT |
Cycles
SatAbs: ERROR/TIMEOUT[130] 1035.75sec (x27.71) Satabs-prefix-first: ERROR/TIMEOUT[130] 972.49sec CBMC-WMM: 0.39sec CBMC-SC: 141.49sec CImpact: ERROR/TIMEOUT[8] 590.46sec ESBMC: 0.13sec Threader-monolithic: ERROR/TIMEOUT[130] 897.54sec Threader-owicki-gries: ERROR/TIMEOUT[130] 897.51sec Threader-rely-guarantee: ERROR/TIMEOUT[130] 897.49sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT |
Cycles
SatAbs: ERROR/TIMEOUT[130] 1047.66sec (x28.03) Satabs-prefix-first: ERROR/TIMEOUT[130] 941.63sec CBMC-WMM: 0.39sec CBMC-SC: 136.30sec CImpact: ERROR/TIMEOUT[8] 601.53sec ESBMC: 0.11sec Threader-monolithic: ERROR/TIMEOUT[130] 896.89sec Threader-owicki-gries: ERROR/TIMEOUT[130] 896.97sec Threader-rely-guarantee: ERROR/TIMEOUT[130] 897.58sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT |
Cycles
SatAbs: 49.69sec (x1.32) Satabs-prefix-first: 79.37sec CBMC-WMM: 0.40sec CBMC-SC: 316.85sec CImpact: 4.43sec ESBMC: 0.17sec Threader-monolithic: ERROR/TIMEOUT[130] 897.43sec Threader-owicki-gries: ERROR/TIMEOUT[130] 897.13sec Threader-rely-guarantee: ERROR/TIMEOUT[130] 897.46sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT |
Cycles
SatAbs: 2.64sec (x.07) Satabs-prefix-first: 3.67sec CBMC-WMM: 0.38sec CBMC-SC: 32.23sec CImpact: ERROR/TIMEOUT[8] 531.93sec ESBMC: 0.11sec Threader-monolithic: ERROR/TIMEOUT[130] 897.56sec Threader-owicki-gries: ERROR/TIMEOUT[130] 897.44sec Threader-rely-guarantee: ERROR/TIMEOUT[130] 897.33sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT |
Cycles
SatAbs: 2.72sec (x.07) Satabs-prefix-first: 3.61sec CBMC-WMM: 0.36sec CBMC-SC: 32.42sec CImpact: ERROR/TIMEOUT[8] 464.61sec ESBMC: 0.10sec Threader-monolithic: ERROR/TIMEOUT[130] 896.90sec Threader-owicki-gries: ERROR/TIMEOUT[130] 897.35sec Threader-rely-guarantee: ERROR/TIMEOUT[130] 897.09sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT |
||||
ppc/lwswr001 |
SatAbs: 8.85sec Satabs-prefix-first: 20.45sec CBMC-WMM: 0.11sec CBMC-SC: 0.11sec CImpact: ERROR/TIMEOUT[8] 317.12sec Checkfence: 0.01sec ESBMC: 0.07sec Threader-monolithic: 0.17sec Threader-owicki-gries: 0.16sec Threader-rely-guarantee: 0.17sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT MMChecker (MM: sc): ERROR/TIMEOUT[1] 0.09sec |
Cycles
SatAbs: 17.41sec (x1.96) Satabs-prefix-first: 26.18sec CBMC-WMM: 0.22sec CBMC-SC: 41.94sec CImpact: 2.90sec ESBMC: 0.09sec Threader-monolithic: ERROR/TIMEOUT[130] 897.13sec Threader-owicki-gries: ERROR/TIMEOUT[130] 896.35sec Threader-rely-guarantee: ERROR/TIMEOUT[130] 897.12sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT MMChecker (MM: csharp): ERROR/TIMEOUT[1] 0.10sec |
Cycles
SatAbs: ERROR/TIMEOUT[130] 1016.27sec (x114.83) Satabs-prefix-first: ERROR/TIMEOUT[130] 977.46sec CBMC-WMM: 0.26sec CBMC-SC: 45.09sec CImpact: ERROR/TIMEOUT[8] 520.85sec Checkfence: 0.01sec ESBMC: 0.11sec Threader-monolithic: ERROR/TIMEOUT[130] 896.96sec Threader-owicki-gries: ERROR/TIMEOUT[130] 897.15sec Threader-rely-guarantee: ERROR/TIMEOUT[130] 897.17sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT MMChecker (MM: csharp): ERROR/TIMEOUT[1] 0.12sec |
Cycles
SatAbs: 16.33sec (x1.84) Satabs-prefix-first: 66.42sec CBMC-WMM: 0.21sec CBMC-SC: 2.06sec CImpact: ERROR/TIMEOUT[8] 330.97sec ESBMC: 0.09sec Threader-monolithic: ERROR/TIMEOUT[1] 331.83sec Threader-owicki-gries: ERROR/TIMEOUT[1] 328.57sec Threader-rely-guarantee: ERROR/TIMEOUT[1] 213.42sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT MMChecker (MM: csharp): ERROR/TIMEOUT[1] 0.09sec |
Cycles
SatAbs: 13.75sec (x1.55) Satabs-prefix-first: 60.95sec CBMC-WMM: 0.20sec CBMC-SC: 1.90sec CImpact: ERROR/TIMEOUT[8] 349.05sec ESBMC: 0.09sec Threader-monolithic: ERROR/TIMEOUT[1] 328.14sec Threader-owicki-gries: ERROR/TIMEOUT[1] 290.44sec Threader-rely-guarantee: ERROR/TIMEOUT[1] 233.57sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT MMChecker (MM: csharp): ERROR/TIMEOUT[1] 0.10sec |
Cycles
SatAbs: ERROR/TIMEOUT[130] 1008.59sec (x113.96) Satabs-prefix-first: ERROR/TIMEOUT[130] CBMC-WMM: 0.24sec CBMC-SC: 26.43sec CImpact: ERROR/TIMEOUT[8] 489.79sec ESBMC: 0.12sec Threader-monolithic: ERROR/TIMEOUT[130] 897.27sec Threader-owicki-gries: ERROR/TIMEOUT[130] 895.69sec Threader-rely-guarantee: ERROR/TIMEOUT[130] 897.40sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT Blender: |
Cycles
SatAbs: 14.10sec (x1.59) Satabs-prefix-first: 65.55sec CBMC-WMM: 0.19sec CBMC-SC: 2.01sec CImpact: ERROR/TIMEOUT[8] 421.40sec ESBMC: 0.09sec Threader-monolithic: ERROR/TIMEOUT[1] 271.65sec Threader-owicki-gries: ERROR/TIMEOUT[1] 269.04sec Threader-rely-guarantee: ERROR/TIMEOUT[1] 300.57sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT Blender: |
Cycles
SatAbs: 14.52sec (x1.64) Satabs-prefix-first: 66.61sec CBMC-WMM: 0.21sec CBMC-SC: 2.03sec CImpact: ERROR/TIMEOUT[8] 437.92sec ESBMC: 0.10sec Threader-monolithic: ERROR/TIMEOUT[1] 330.88sec Threader-owicki-gries: ERROR/TIMEOUT[1] 317.49sec Threader-rely-guarantee: ERROR/TIMEOUT[1] 221.44sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT Blender: |
Cycles
SatAbs: ERROR/TIMEOUT[130] 1027.34sec (x116.08) Satabs-prefix-first: ERROR/TIMEOUT[130] 972.48sec CBMC-WMM: 0.26sec CBMC-SC: 42.59sec CImpact: ERROR/TIMEOUT[8] 562.59sec ESBMC: 0.11sec Threader-monolithic: ERROR/TIMEOUT[130] 896.87sec Threader-owicki-gries: ERROR/TIMEOUT[130] 897.41sec Threader-rely-guarantee: ERROR/TIMEOUT[130] 897.20sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT |
Cycles
SatAbs: 13.65sec (x1.54) Satabs-prefix-first: 67.94sec CBMC-WMM: 0.26sec CBMC-SC: 2.27sec CImpact: ERROR/TIMEOUT[8] 426.55sec ESBMC: 0.10sec Threader-monolithic: ERROR/TIMEOUT[1] 318.55sec Threader-owicki-gries: ERROR/TIMEOUT[1] 257.77sec Threader-rely-guarantee: ERROR/TIMEOUT[1] 301.40sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT |
Cycles
SatAbs: 14.03sec (x1.58) Satabs-prefix-first: 65.08sec CBMC-WMM: 0.27sec CBMC-SC: 2.00sec CImpact: ERROR/TIMEOUT[8] 412.72sec ESBMC: 0.10sec Threader-monolithic: ERROR/TIMEOUT[1] 329.71sec Threader-owicki-gries: ERROR/TIMEOUT[1] 235.01sec Threader-rely-guarantee: ERROR/TIMEOUT[1] 306.93sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT |
Cycles
SatAbs: 24.81sec (x2.80) Satabs-prefix-first: 55.99sec CBMC-WMM: 0.24sec CBMC-SC: 54.97sec CImpact: 3.14sec ESBMC: 0.13sec Threader-monolithic: ERROR/TIMEOUT[130] 897.59sec Threader-owicki-gries: ERROR/TIMEOUT[130] 896.88sec Threader-rely-guarantee: ERROR/TIMEOUT[130] 897.42sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT |
Cycles
SatAbs: 15.14sec (x1.71) Satabs-prefix-first: 74.03sec CBMC-WMM: 0.28sec CBMC-SC: 2.09sec CImpact: ERROR/TIMEOUT[8] 348.21sec ESBMC: 0.10sec Threader-monolithic: ERROR/TIMEOUT[1] 234.30sec Threader-owicki-gries: ERROR/TIMEOUT[1] 273.09sec Threader-rely-guarantee: ERROR/TIMEOUT[1] 329.92sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT |
Cycles
SatAbs: 13.96sec (x1.57) Satabs-prefix-first: 64.92sec CBMC-WMM: 0.25sec CBMC-SC: 1.94sec CImpact: ERROR/TIMEOUT[8] 424.72sec ESBMC: 0.08sec Threader-monolithic: ERROR/TIMEOUT[1] 332.11sec Threader-owicki-gries: ERROR/TIMEOUT[1] 212.31sec Threader-rely-guarantee: ERROR/TIMEOUT[1] 329.55sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT |
||||
ppc/lwswr002 |
SatAbs: 2.81sec Satabs-prefix-first: 5.86sec CBMC-WMM: 0.06sec CBMC-SC: 0.06sec CImpact: 12.42sec Checkfence: 0.01sec ESBMC: 0.08sec Threader-monolithic: 0.15sec Threader-owicki-gries: 0.16sec Threader-rely-guarantee: 0.14sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT MMChecker (MM: sc): ERROR/TIMEOUT[1] 0.09sec |
Cycles
SatAbs: 21.56sec (x7.67) Satabs-prefix-first: 51.05sec CBMC-WMM: 0.14sec CBMC-SC: 10.58sec CImpact: 2.31sec ESBMC: 0.09sec Threader-monolithic: ERROR/TIMEOUT[130] 896.98sec Threader-owicki-gries: ERROR/TIMEOUT[130] 896.70sec Threader-rely-guarantee: ERROR/TIMEOUT[130] 896.80sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT MMChecker (MM: csharp): ERROR/TIMEOUT[1] 0.10sec |
Cycles
SatAbs: 18.60sec (x6.61) Satabs-prefix-first: 40.19sec CBMC-WMM: 0.13sec CBMC-SC: 16.39sec CImpact: 2.25sec Checkfence: 0.01sec ESBMC: 0.09sec Threader-monolithic: ERROR/TIMEOUT[130] 896.94sec Threader-owicki-gries: ERROR/TIMEOUT[130] 894.86sec Threader-rely-guarantee: ERROR/TIMEOUT[130] 896.31sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT MMChecker (MM: csharp): ERROR/TIMEOUT[1] 0.10sec |
Cycles
SatAbs: 14.40sec (x5.12) Satabs-prefix-first: 5.31sec CBMC-WMM: 0.16sec CBMC-SC: 2.17sec CImpact: 1.62sec ESBMC: 0.09sec Threader-monolithic: ERROR/TIMEOUT[1] 208.53sec Threader-owicki-gries: ERROR/TIMEOUT[1] 212.71sec Threader-rely-guarantee: ERROR/TIMEOUT[1] 234.54sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT MMChecker (MM: csharp): ERROR/TIMEOUT[1] 0.09sec |
Cycles
SatAbs: 7.86sec (x2.79) Satabs-prefix-first: 39.89sec CBMC-WMM: 0.15sec CBMC-SC: 1.13sec CImpact: 122.48sec ESBMC: 0.14sec Threader-monolithic: ERROR/TIMEOUT[1] 230.84sec Threader-owicki-gries: ERROR/TIMEOUT[1] 223.08sec Threader-rely-guarantee: ERROR/TIMEOUT[1] 188.70sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT MMChecker (MM: csharp): ERROR/TIMEOUT[1] 0.11sec |
Cycles
SatAbs: 20.69sec (x7.36) Satabs-prefix-first: 43.43sec CBMC-WMM: 0.14sec CBMC-SC: 16.63sec CImpact: 2.32sec ESBMC: 0.09sec Threader-monolithic: ERROR/TIMEOUT[130] 897.03sec Threader-owicki-gries: ERROR/TIMEOUT[130] 897.16sec Threader-rely-guarantee: ERROR/TIMEOUT[130] 896.82sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT Blender: |
Cycles
SatAbs: 12.80sec (x4.55) Satabs-prefix-first: 4.74sec CBMC-WMM: 0.13sec CBMC-SC: 1.88sec CImpact: 1.60sec ESBMC: 0.07sec Threader-monolithic: ERROR/TIMEOUT[1] 225.53sec Threader-owicki-gries: ERROR/TIMEOUT[1] 230.75sec Threader-rely-guarantee: ERROR/TIMEOUT[1] 229.42sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT Blender: |
Cycles
SatAbs: 7.03sec (x2.50) Satabs-prefix-first: 35.82sec CBMC-WMM: 0.14sec CBMC-SC: 1.06sec CImpact: 121.65sec ESBMC: 0.07sec Threader-monolithic: ERROR/TIMEOUT[1] 246.93sec Threader-owicki-gries: ERROR/TIMEOUT[1] 215.37sec Threader-rely-guarantee: ERROR/TIMEOUT[1] 170.88sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT Blender: |
Cycles
SatAbs: 18.64sec (x6.63) Satabs-prefix-first: 41.16sec CBMC-WMM: 0.15sec CBMC-SC: 16.30sec CImpact: 2.26sec ESBMC: 0.12sec Threader-monolithic: ERROR/TIMEOUT[130] 896.92sec Threader-owicki-gries: ERROR/TIMEOUT[130] 896.82sec Threader-rely-guarantee: ERROR/TIMEOUT[130] 897.06sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT |
Cycles
SatAbs: 13.16sec (x4.68) Satabs-prefix-first: 4.78sec CBMC-WMM: 0.18sec CBMC-SC: 1.98sec CImpact: 1.60sec ESBMC: 0.08sec Threader-monolithic: ERROR/TIMEOUT[1] 183.41sec Threader-owicki-gries: ERROR/TIMEOUT[1] 252.31sec Threader-rely-guarantee: ERROR/TIMEOUT[1] 252.27sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT |
Cycles
SatAbs: 6.49sec (x2.30) Satabs-prefix-first: 37.50sec CBMC-WMM: 0.17sec CBMC-SC: 1.05sec CImpact: 129.44sec ESBMC: 0.08sec Threader-monolithic: ERROR/TIMEOUT[1] 252.84sec Threader-owicki-gries: ERROR/TIMEOUT[1] 252.13sec Threader-rely-guarantee: ERROR/TIMEOUT[1] 251.27sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT |
Cycles
SatAbs: 19.78sec (x7.03) Satabs-prefix-first: 43.77sec CBMC-WMM: 0.17sec CBMC-SC: 15.23sec CImpact: 2.52sec ESBMC: 0.11sec Threader-monolithic: ERROR/TIMEOUT[130] 896.60sec Threader-owicki-gries: ERROR/TIMEOUT[130] 896.95sec Threader-rely-guarantee: ERROR/TIMEOUT[130] 897.01sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT |
Cycles
SatAbs: 11.75sec (x4.18) Satabs-prefix-first: 4.84sec CBMC-WMM: 0.12sec CBMC-SC: 1.34sec CImpact: 0.99sec ESBMC: 0.05sec Threader-monolithic: ERROR/TIMEOUT[1] 224.20sec Threader-owicki-gries: ERROR/TIMEOUT[1] 208.46sec Threader-rely-guarantee: ERROR/TIMEOUT[1] 212.49sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT |
Cycles
SatAbs: 7.22sec (x2.56) Satabs-prefix-first: 37.45sec CBMC-WMM: 0.16sec CBMC-SC: 1.08sec CImpact: 117.21sec ESBMC: 0.09sec Threader-monolithic: ERROR/TIMEOUT[1] 223.07sec Threader-owicki-gries: ERROR/TIMEOUT[1] 210.12sec Threader-rely-guarantee: ERROR/TIMEOUT[1] 229.02sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT |
||||
ppc/lwswr003 |
SatAbs: 49.95sec Satabs-prefix-first: 45.27sec CBMC-WMM: 0.10sec CBMC-SC: 0.10sec CImpact: ERROR/TIMEOUT[8] 317.01sec Checkfence: 0.01sec ESBMC: 0.08sec Threader-monolithic: 0.18sec Threader-owicki-gries: 0.18sec Threader-rely-guarantee: 0.17sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT MMChecker (MM: sc): ERROR/TIMEOUT[1] 0.09sec |
Cycles
SatAbs: 48.60sec (x.97) Satabs-prefix-first: 275.91sec CBMC-WMM: 0.25sec CBMC-SC: 62.31sec CImpact: ERROR/TIMEOUT[8] 387.72sec ESBMC: 0.14sec Threader-monolithic: ERROR/TIMEOUT[130] 897.24sec Threader-owicki-gries: ERROR/TIMEOUT[130] 897.29sec Threader-rely-guarantee: ERROR/TIMEOUT[130] 897.26sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT MMChecker (MM: csharp): ERROR/TIMEOUT[1] 0.10sec |
Cycles
SatAbs: 47.27sec (x.94) Satabs-prefix-first: 284.88sec CBMC-WMM: 0.27sec CBMC-SC: 40.28sec CImpact: ERROR/TIMEOUT[8] 423.83sec Checkfence: 0.01sec ESBMC: 0.12sec Threader-monolithic: ERROR/TIMEOUT[130] 897.05sec Threader-owicki-gries: ERROR/TIMEOUT[130] 896.87sec Threader-rely-guarantee: ERROR/TIMEOUT[130] 896.99sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT MMChecker (MM: csharp): ERROR/TIMEOUT[1] 0.09sec |
Cycles
SatAbs: 69.57sec (x1.39) Satabs-prefix-first: 114.36sec CBMC-WMM: 0.26sec CBMC-SC: 3.30sec CImpact: ERROR/TIMEOUT[8] 268.51sec ESBMC: 0.09sec Threader-monolithic: ERROR/TIMEOUT[1] 277.17sec Threader-owicki-gries: ERROR/TIMEOUT[1] 208.65sec Threader-rely-guarantee: ERROR/TIMEOUT[1] 215.66sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT MMChecker (MM: csharp): ERROR/TIMEOUT[1] 0.09sec |
Cycles
SatAbs: 128.81sec (x2.57) Satabs-prefix-first: 118.19sec CBMC-WMM: 0.22sec CBMC-SC: 1.18sec CImpact: ERROR/TIMEOUT[8] 373.83sec ESBMC: 0.07sec Threader-monolithic: ERROR/TIMEOUT[1] 263.53sec Threader-owicki-gries: ERROR/TIMEOUT[1] 297.34sec Threader-rely-guarantee: ERROR/TIMEOUT[1] 296.66sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT MMChecker (MM: csharp): ERROR/TIMEOUT[1] 0.10sec |
Cycles
SatAbs: 46.95sec (x.93) Satabs-prefix-first: 261.13sec CBMC-WMM: 0.25sec CBMC-SC: 61.11sec CImpact: ERROR/TIMEOUT[8] 571.60sec ESBMC: 0.14sec Threader-monolithic: ERROR/TIMEOUT[130] 897.19sec Threader-owicki-gries: ERROR/TIMEOUT[130] 897.13sec Threader-rely-guarantee: ERROR/TIMEOUT[130] 897.05sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT Blender: |
Cycles
SatAbs: 70.39sec (x1.40) Satabs-prefix-first: 117.35sec CBMC-WMM: 0.22sec CBMC-SC: 3.55sec CImpact: ERROR/TIMEOUT[8] 266.63sec ESBMC: 0.10sec Threader-monolithic: ERROR/TIMEOUT[1] 275.03sec Threader-owicki-gries: ERROR/TIMEOUT[1] 296.65sec Threader-rely-guarantee: ERROR/TIMEOUT[1] 297.45sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT Blender: |
Cycles
SatAbs: 129.17sec (x2.58) Satabs-prefix-first: 119.53sec CBMC-WMM: 0.25sec CBMC-SC: 1.19sec CImpact: ERROR/TIMEOUT[8] 371.77sec ESBMC: 0.07sec Threader-monolithic: ERROR/TIMEOUT[1] 295.69sec Threader-owicki-gries: ERROR/TIMEOUT[1] 293.18sec Threader-rely-guarantee: ERROR/TIMEOUT[1] 297.17sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT Blender: |
Cycles
SatAbs: 47.93sec (x.95) Satabs-prefix-first: 256.49sec CBMC-WMM: 0.33sec CBMC-SC: 65.45sec CImpact: ERROR/TIMEOUT[8] 401.88sec ESBMC: 0.13sec Threader-monolithic: ERROR/TIMEOUT[130] 897.11sec Threader-owicki-gries: ERROR/TIMEOUT[130] 897.44sec Threader-rely-guarantee: ERROR/TIMEOUT[130] 896.96sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT |
Cycles
SatAbs: 72.15sec (x1.44) Satabs-prefix-first: 118.95sec CBMC-WMM: 0.32sec CBMC-SC: 3.27sec CImpact: ERROR/TIMEOUT[8] 404.24sec ESBMC: 0.10sec Threader-monolithic: ERROR/TIMEOUT[1] 296.19sec Threader-owicki-gries: ERROR/TIMEOUT[1] 296.18sec Threader-rely-guarantee: ERROR/TIMEOUT[1] 297.13sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT |
Cycles
SatAbs: 131.61sec (x2.63) Satabs-prefix-first: 119.52sec CBMC-WMM: 0.31sec CBMC-SC: 1.19sec CImpact: ERROR/TIMEOUT[8] 376.50sec ESBMC: 0.09sec Threader-monolithic: ERROR/TIMEOUT[1] 297.24sec Threader-owicki-gries: ERROR/TIMEOUT[1] 273.29sec Threader-rely-guarantee: ERROR/TIMEOUT[1] 238.35sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT |
Cycles
SatAbs: 47.31sec (x.94) Satabs-prefix-first: 253.95sec CBMC-WMM: 0.29sec CBMC-SC: 60.71sec CImpact: ERROR/TIMEOUT[8] 494.30sec ESBMC: 0.14sec Threader-monolithic: ERROR/TIMEOUT[130] 897.12sec Threader-owicki-gries: ERROR/TIMEOUT[130] 897.27sec Threader-rely-guarantee: ERROR/TIMEOUT[130] 897.32sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT |
Cycles
SatAbs: 70.37sec (x1.40) Satabs-prefix-first: 116.17sec CBMC-WMM: 0.31sec CBMC-SC: 3.22sec CImpact: ERROR/TIMEOUT[8] 368.31sec ESBMC: 0.10sec Threader-monolithic: ERROR/TIMEOUT[1] 215.81sec Threader-owicki-gries: ERROR/TIMEOUT[1] 224.09sec Threader-rely-guarantee: ERROR/TIMEOUT[1] 224.55sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT |
Cycles
SatAbs: 132.40sec (x2.65) Satabs-prefix-first: 117.21sec CBMC-WMM: 0.32sec CBMC-SC: 1.21sec CImpact: ERROR/TIMEOUT[8] 331.97sec ESBMC: 0.10sec Threader-monolithic: ERROR/TIMEOUT[1] 293.71sec Threader-owicki-gries: ERROR/TIMEOUT[1] 197.45sec Threader-rely-guarantee: ERROR/TIMEOUT[1] 218.18sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT |