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: ![]() Threader: ![]() ... |
Cycles SatAbs: ![]() 3.94sec (x6.56) ESBMC: ![]() Threader: ERROR/TIMEOUT[1] 491.99sec ... |
Cycles SatAbs: ![]() 2.43sec (x4.05) ESBMC: ![]() Threader: ERROR/TIMEOUT[1] 182.60sec ... |
![]() |
... |
ppc/podrr (tooling date Sun Jan 22 02:23:23 GMT 2012)
This family corresponds to litmus tests involving pairs showing that Power can reorder read-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/podrr000 |
SatAbs: ![]() 0.83sec Satabs-prefix-first: ![]() CBMC-WMM: ![]() CBMC-SC: ![]() CImpact: ![]() Checkfence: 0.01sec ESBMC: 0.07sec Threader-monolithic: ![]() Threader-owicki-gries: ![]() Threader-rely-guarantee: ![]() Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT MMChecker (MM: sc): ERROR/TIMEOUT[2] 0.01sec |
Cycles
SatAbs: ![]() 13.89sec (x16.73) Satabs-prefix-first: ![]() CBMC-WMM: ![]() CBMC-SC: ![]() CImpact: ![]() ESBMC: 0.11sec Threader-monolithic: ERROR/TIMEOUT[130] 896.47sec Threader-owicki-gries: ERROR/TIMEOUT[130] 897.05sec Threader-rely-guarantee: ERROR/TIMEOUT[130] 896.46sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT MMChecker (MM: csharp): ERROR/TIMEOUT[2] 0.00sec |
Cycles
SatAbs: ![]() 1.39sec (x1.67) Satabs-prefix-first: ![]() CBMC-WMM: ![]() CBMC-SC: ![]() CImpact: ![]() Checkfence: 0.01sec ESBMC: 0.09sec Threader-monolithic: ERROR/TIMEOUT[1] 0.10sec Threader-owicki-gries: ERROR/TIMEOUT[1] 0.10sec Threader-rely-guarantee: ERROR/TIMEOUT[1] 0.10sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT MMChecker (MM: csharp): ERROR/TIMEOUT[2] 0.00sec |
Cycles
SatAbs: ![]() 0.93sec (x1.12) Satabs-prefix-first: ![]() CBMC-WMM: ![]() CBMC-SC: ![]() CImpact: ![]() ESBMC: 0.10sec Threader-monolithic: ERROR/TIMEOUT[1] 0.10sec Threader-owicki-gries: ERROR/TIMEOUT[1] 0.10sec Threader-rely-guarantee: ERROR/TIMEOUT[1] 0.10sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT MMChecker (MM: csharp): ERROR/TIMEOUT[2] 0.00sec |
Cycles
SatAbs: ![]() 1.05sec (x1.26) Satabs-prefix-first: ![]() CBMC-WMM: ![]() CBMC-SC: ![]() CImpact: ![]() 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): ERROR/TIMEOUT[2] 0.00sec |
![]() |
Cycles
SatAbs: ![]() 0.81sec (x.97) Satabs-prefix-first: ![]() CBMC-WMM: ![]() CBMC-SC: ![]() CImpact: ![]() ESBMC: 0.09sec Threader-monolithic: ERROR/TIMEOUT[1] 0.10sec 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: ![]() 0.96sec (x1.15) Satabs-prefix-first: ![]() CBMC-WMM: ![]() CBMC-SC: ![]() CImpact: ![]() ESBMC: 0.09sec Threader-monolithic: ERROR/TIMEOUT[1] 0.10sec 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: ![]() 1.03sec (x1.24) Satabs-prefix-first: ![]() CBMC-WMM: ![]() CBMC-SC: ![]() CImpact: ![]() 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 Blender: ![]() |
![]() |
Cycles
SatAbs: ![]() 2.78sec (x3.34) Satabs-prefix-first: ![]() CBMC-WMM: ![]() CBMC-SC: ![]() CImpact: ![]() ESBMC: 0.09sec Threader-monolithic: ERROR/TIMEOUT[1] 374.68sec Threader-owicki-gries: ERROR/TIMEOUT[1] 368.84sec Threader-rely-guarantee: ERROR/TIMEOUT[1] 261.64sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT |
Cycles
SatAbs: ![]() 2.67sec (x3.21) Satabs-prefix-first: ![]() CBMC-WMM: ![]() CBMC-SC: ![]() CImpact: ![]() ESBMC: 0.10sec Threader-monolithic: ERROR/TIMEOUT[1] 370.42sec Threader-owicki-gries: ERROR/TIMEOUT[1] 374.77sec Threader-rely-guarantee: ERROR/TIMEOUT[1] 356.51sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT |
Cycles
SatAbs: ![]() 2.87sec (x3.45) Satabs-prefix-first: ![]() CBMC-WMM: ![]() CBMC-SC: ![]() CImpact: ![]() ESBMC: 0.10sec Threader-monolithic: ERROR/TIMEOUT[1] 376.89sec Threader-owicki-gries: ERROR/TIMEOUT[1] 375.24sec Threader-rely-guarantee: ERROR/TIMEOUT[1] 269.99sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT |
![]() |
Cycles
SatAbs: ![]() 3.14sec (x3.78) Satabs-prefix-first: ![]() CBMC-WMM: ![]() CBMC-SC: ![]() CImpact: ![]() ESBMC: 0.10sec Threader-monolithic: ERROR/TIMEOUT[1] 311.47sec Threader-owicki-gries: ERROR/TIMEOUT[1] 348.63sec Threader-rely-guarantee: ERROR/TIMEOUT[1] 361.46sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT |
Cycles
SatAbs: ![]() 4.14sec (x4.98) Satabs-prefix-first: ![]() CBMC-WMM: ![]() CBMC-SC: ![]() CImpact: ![]() ESBMC: 0.12sec Threader-monolithic: ERROR/TIMEOUT[1] 280.11sec Threader-owicki-gries: ERROR/TIMEOUT[1] 286.17sec Threader-rely-guarantee: ERROR/TIMEOUT[1] 345.68sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT |
Cycles
SatAbs: ![]() 2.96sec (x3.56) Satabs-prefix-first: ![]() CBMC-WMM: ![]() CBMC-SC: ![]() CImpact: ![]() ESBMC: 0.08sec Threader-monolithic: ERROR/TIMEOUT[1] 372.03sec Threader-owicki-gries: ERROR/TIMEOUT[1] 256.04sec Threader-rely-guarantee: ERROR/TIMEOUT[1] 376.84sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT |
![]() |
ppc/podrr001 |
SatAbs: ![]() 2.63sec Satabs-prefix-first: ![]() CBMC-WMM: ![]() CBMC-SC: ![]() CImpact: ERROR/TIMEOUT[8] 291.47sec Checkfence: 0.01sec ESBMC: 0.10sec Threader-monolithic: ![]() Threader-owicki-gries: ![]() Threader-rely-guarantee: ![]() Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT MMChecker (MM: sc): ERROR/TIMEOUT[2] 0.00sec |
Cycles
SatAbs: ![]() 58.03sec (x22.06) Satabs-prefix-first: ![]() CBMC-WMM: ![]() CBMC-SC: ![]() CImpact: ERROR/TIMEOUT[8] 317.39sec ESBMC: 0.11sec Threader-monolithic: ERROR/TIMEOUT[130] 897.16sec Threader-owicki-gries: ERROR/TIMEOUT[130] 897.16sec Threader-rely-guarantee: ERROR/TIMEOUT[130] 897.19sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT MMChecker (MM: csharp): ERROR/TIMEOUT[2] 0.01sec |
Cycles
SatAbs: ![]() 9.95sec (x3.78) Satabs-prefix-first: ![]() CBMC-WMM: ![]() CBMC-SC: ![]() CImpact: ERROR/TIMEOUT[8] 363.45sec Checkfence: 0.01sec ESBMC: 0.08sec Threader-monolithic: ERROR/TIMEOUT[1] 0.12sec Threader-owicki-gries: ERROR/TIMEOUT[1] 0.11sec Threader-rely-guarantee: ERROR/TIMEOUT[1] 0.09sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT MMChecker (MM: csharp): ERROR/TIMEOUT[2] 0.00sec |
Cycles
SatAbs: ![]() 12.50sec (x4.75) Satabs-prefix-first: ![]() CBMC-WMM: ![]() CBMC-SC: ![]() CImpact: ERROR/TIMEOUT[8] 323.49sec ESBMC: 0.09sec Threader-monolithic: ERROR/TIMEOUT[1] 0.12sec 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): ERROR/TIMEOUT[2] 0.00sec |
Cycles
SatAbs: ![]() 9.76sec (x3.71) Satabs-prefix-first: ![]() CBMC-WMM: ![]() CBMC-SC: ![]() CImpact: ERROR/TIMEOUT[8] 351.94sec ESBMC: 0.06sec Threader-monolithic: ERROR/TIMEOUT[1] 0.11sec Threader-owicki-gries: ERROR/TIMEOUT[1] 0.12sec Threader-rely-guarantee: ERROR/TIMEOUT[1] 0.10sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT MMChecker (MM: csharp): ERROR/TIMEOUT[2] 0.00sec |
![]() |
Cycles
SatAbs: ![]() 10.54sec (x4.00) Satabs-prefix-first: ![]() CBMC-WMM: ![]() CBMC-SC: ![]() CImpact: ERROR/TIMEOUT[8] 350.24sec ESBMC: 0.09sec Threader-monolithic: ERROR/TIMEOUT[1] 0.12sec Threader-owicki-gries: ERROR/TIMEOUT[1] 0.10sec Threader-rely-guarantee: ERROR/TIMEOUT[1] 0.10sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT Blender: ![]() |
Cycles
SatAbs: ![]() 9.61sec (x3.65) Satabs-prefix-first: ![]() CBMC-WMM: ![]() CBMC-SC: ![]() CImpact: ERROR/TIMEOUT[8] 307.19sec ESBMC: 0.08sec 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: ![]() 9.60sec (x3.65) Satabs-prefix-first: ![]() CBMC-WMM: ![]() CBMC-SC: ![]() CImpact: ERROR/TIMEOUT[8] 328.93sec ESBMC: 0.08sec Threader-monolithic: ERROR/TIMEOUT[1] 0.12sec Threader-owicki-gries: ERROR/TIMEOUT[1] 0.09sec Threader-rely-guarantee: ERROR/TIMEOUT[1] 0.11sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT Blender: ![]() |
![]() |
Cycles
SatAbs: ![]() 44.91sec (x17.07) Satabs-prefix-first: ![]() CBMC-WMM: ![]() CBMC-SC: ![]() CImpact: ERROR/TIMEOUT[8] 230.03sec ESBMC: 0.10sec Threader-monolithic: ERROR/TIMEOUT[1] 345.82sec Threader-owicki-gries: ERROR/TIMEOUT[1] 439.36sec Threader-rely-guarantee: ERROR/TIMEOUT[1] 331.22sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT |
Cycles
SatAbs: ![]() 45.43sec (x17.27) Satabs-prefix-first: ![]() CBMC-WMM: ![]() CBMC-SC: ![]() CImpact: ERROR/TIMEOUT[8] 298.33sec ESBMC: 0.11sec Threader-monolithic: ERROR/TIMEOUT[1] 416.07sec Threader-owicki-gries: ERROR/TIMEOUT[1] 315.05sec Threader-rely-guarantee: ERROR/TIMEOUT[1] 442.62sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT |
Cycles
SatAbs: ![]() 45.53sec (x17.31) Satabs-prefix-first: ![]() CBMC-WMM: ![]() CBMC-SC: ![]() CImpact: ERROR/TIMEOUT[8] 326.54sec ESBMC: 0.10sec Threader-monolithic: ERROR/TIMEOUT[1] 446.04sec Threader-owicki-gries: ERROR/TIMEOUT[1] 441.57sec Threader-rely-guarantee: ERROR/TIMEOUT[1] 376.73sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT |
![]() |
Cycles
SatAbs: ![]() 40.61sec (x15.44) Satabs-prefix-first: ![]() CBMC-WMM: ![]() CBMC-SC: ![]() CImpact: ERROR/TIMEOUT[8] 267.93sec ESBMC: 0.10sec Threader-monolithic: ERROR/TIMEOUT[1] 406.65sec Threader-owicki-gries: ERROR/TIMEOUT[1] 401.93sec Threader-rely-guarantee: ERROR/TIMEOUT[1] 405.68sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT |
Cycles
SatAbs: ![]() 39.76sec (x15.11) Satabs-prefix-first: ![]() CBMC-WMM: ![]() CBMC-SC: ![]() CImpact: ERROR/TIMEOUT[8] 346.85sec ESBMC: 0.09sec Threader-monolithic: ERROR/TIMEOUT[1] 423.76sec Threader-owicki-gries: ERROR/TIMEOUT[1] 448.03sec Threader-rely-guarantee: ERROR/TIMEOUT[1] 436.83sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT |
Cycles
SatAbs: ![]() 41.28sec (x15.69) Satabs-prefix-first: ![]() CBMC-WMM: ![]() CBMC-SC: ![]() CImpact: ERROR/TIMEOUT[8] 218.27sec ESBMC: 0.08sec Threader-monolithic: ERROR/TIMEOUT[1] 438.02sec Threader-owicki-gries: ERROR/TIMEOUT[1] 391.89sec Threader-rely-guarantee: ERROR/TIMEOUT[1] 396.38sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT |
![]() |
ppc/podrr002 |
SatAbs: ![]() 1.24sec Satabs-prefix-first: ![]() CBMC-WMM: ![]() CBMC-SC: ![]() CImpact: ERROR/TIMEOUT[8] 279.10sec Checkfence: 0.01sec ESBMC: 0.09sec Threader-monolithic: ![]() Threader-owicki-gries: ![]() Threader-rely-guarantee: ![]() Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT MMChecker (MM: sc): ERROR/TIMEOUT[2] 0.00sec |
Cycles
SatAbs: ![]() 104.14sec (x83.98) Satabs-prefix-first: ERROR/TIMEOUT[130] 920.12sec CBMC-WMM: ![]() CBMC-SC: ![]() CImpact: ERROR/TIMEOUT[8] 474.30sec ESBMC: 0.13sec Threader-monolithic: ERROR/TIMEOUT[130] 897.17sec Threader-owicki-gries: ERROR/TIMEOUT[130] 897.33sec Threader-rely-guarantee: ERROR/TIMEOUT[130] 897.49sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT MMChecker (MM: csharp): ERROR/TIMEOUT[2] 0.00sec |
Cycles
SatAbs: ![]() 6.52sec (x5.25) Satabs-prefix-first: ![]() CBMC-WMM: ![]() CBMC-SC: ![]() CImpact: ERROR/TIMEOUT[8] 315.28sec Checkfence: 0.01sec ESBMC: 0.09sec Threader-monolithic: ERROR/TIMEOUT[1] 0.12sec 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): ERROR/TIMEOUT[2] 0.00sec |
Cycles
SatAbs: ![]() 6.40sec (x5.16) Satabs-prefix-first: ![]() CBMC-WMM: ![]() CBMC-SC: ![]() CImpact: ERROR/TIMEOUT[8] 302.06sec ESBMC: 0.09sec Threader-monolithic: ERROR/TIMEOUT[1] 0.09sec Threader-owicki-gries: ERROR/TIMEOUT[1] 0.12sec Threader-rely-guarantee: ERROR/TIMEOUT[1] 0.12sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT MMChecker (MM: csharp): ERROR/TIMEOUT[2] 0.00sec |
Cycles
SatAbs: ![]() 7.44sec (x6.00) Satabs-prefix-first: ![]() CBMC-WMM: ![]() CBMC-SC: ![]() CImpact: ERROR/TIMEOUT[8] 339.00sec ESBMC: 0.08sec Threader-monolithic: ERROR/TIMEOUT[1] 0.11sec 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): ERROR/TIMEOUT[2] 0.00sec |
![]() |
Cycles
SatAbs: ![]() 6.17sec (x4.97) Satabs-prefix-first: ![]() CBMC-WMM: ![]() CBMC-SC: ![]() CImpact: ERROR/TIMEOUT[8] 300.53sec ESBMC: 0.09sec Threader-monolithic: ERROR/TIMEOUT[1] 0.11sec Threader-owicki-gries: ERROR/TIMEOUT[1] 0.12sec Threader-rely-guarantee: ERROR/TIMEOUT[1] 0.12sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT Blender: ![]() |
Cycles
SatAbs: ![]() 6.27sec (x5.05) Satabs-prefix-first: ![]() CBMC-WMM: ![]() CBMC-SC: ![]() CImpact: ERROR/TIMEOUT[8] 318.34sec ESBMC: 0.09sec Threader-monolithic: ERROR/TIMEOUT[1] 0.10sec Threader-owicki-gries: ERROR/TIMEOUT[1] 0.11sec Threader-rely-guarantee: ERROR/TIMEOUT[1] 0.10sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT Blender: ![]() |
Cycles
SatAbs: ![]() 6.82sec (x5.50) Satabs-prefix-first: ![]() CBMC-WMM: ![]() CBMC-SC: ![]() CImpact: ERROR/TIMEOUT[8] 338.19sec ESBMC: 0.08sec 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 Blender: ![]() |
![]() |
Cycles
SatAbs: ![]() 44.90sec (x36.20) Satabs-prefix-first: ![]() CBMC-WMM: ![]() CBMC-SC: ![]() CImpact: ERROR/TIMEOUT[8] 311.47sec ESBMC: 0.09sec Threader-monolithic: ERROR/TIMEOUT[1] 367.96sec Threader-owicki-gries: ERROR/TIMEOUT[1] 489.94sec Threader-rely-guarantee: ERROR/TIMEOUT[1] 417.22sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT |
Cycles
SatAbs: ![]() 48.93sec (x39.45) Satabs-prefix-first: ![]() CBMC-WMM: ![]() CBMC-SC: ![]() CImpact: ERROR/TIMEOUT[8] 345.66sec ESBMC: 0.08sec Threader-monolithic: ERROR/TIMEOUT[1] 488.51sec Threader-owicki-gries: ERROR/TIMEOUT[1] 490.59sec Threader-rely-guarantee: ERROR/TIMEOUT[1] 489.48sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT |
Cycles
SatAbs: ![]() 45.38sec (x36.59) Satabs-prefix-first: ![]() CBMC-WMM: ![]() CBMC-SC: ![]() CImpact: ERROR/TIMEOUT[8] 327.31sec ESBMC: 0.07sec Threader-monolithic: ERROR/TIMEOUT[1] 479.44sec Threader-owicki-gries: ERROR/TIMEOUT[1] 451.54sec Threader-rely-guarantee: ERROR/TIMEOUT[1] 366.75sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT |
![]() |
Cycles
SatAbs: ERROR/TIMEOUT[130] 1020.55sec (x823.02) Satabs-prefix-first: ERROR/TIMEOUT[130] 915.64sec CBMC-WMM: ![]() CBMC-SC: ![]() CImpact: ERROR/TIMEOUT[8] 358.93sec ESBMC: 0.12sec Threader-monolithic: ERROR/TIMEOUT[130] 897.65sec Threader-owicki-gries: ERROR/TIMEOUT[130] 897.53sec Threader-rely-guarantee: ERROR/TIMEOUT[130] 897.42sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT |
Cycles
SatAbs: ![]() 48.76sec (x39.32) Satabs-prefix-first: ![]() CBMC-WMM: ![]() CBMC-SC: ![]() CImpact: ERROR/TIMEOUT[8] 290.37sec ESBMC: 0.08sec Threader-monolithic: ERROR/TIMEOUT[1] 468.27sec Threader-owicki-gries: ERROR/TIMEOUT[1] 449.16sec Threader-rely-guarantee: ERROR/TIMEOUT[1] 472.40sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT |
Cycles
SatAbs: ![]() 50.79sec (x40.95) Satabs-prefix-first: ![]() CBMC-WMM: ![]() CBMC-SC: ![]() CImpact: ERROR/TIMEOUT[8] 326.15sec ESBMC: 0.10sec Threader-monolithic: ERROR/TIMEOUT[1] 489.90sec Threader-owicki-gries: ERROR/TIMEOUT[1] 492.77sec Threader-rely-guarantee: ERROR/TIMEOUT[1] 493.78sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT |
![]() |
ppc/podrr003 |
SatAbs: ![]() 3.98sec Satabs-prefix-first: ![]() CBMC-WMM: ![]() CBMC-SC: ![]() CImpact: ERROR/TIMEOUT[8] 298.02sec Checkfence: 0.01sec ESBMC: 0.06sec Threader-monolithic: ![]() Threader-owicki-gries: ![]() Threader-rely-guarantee: ![]() Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT MMChecker (MM: sc): ERROR/TIMEOUT[2] 0.00sec |
Cycles
SatAbs: ![]() 6.52sec (x1.63) Satabs-prefix-first: ![]() CBMC-WMM: ![]() CBMC-SC: ![]() CImpact: ERROR/TIMEOUT[8] 437.31sec ESBMC: 0.13sec Threader-monolithic: ERROR/TIMEOUT[130] 897.13sec Threader-owicki-gries: ERROR/TIMEOUT[130] 897.55sec Threader-rely-guarantee: ERROR/TIMEOUT[130] 896.99sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT MMChecker (MM: csharp): ERROR/TIMEOUT[2] 0.00sec |
Cycles
SatAbs: ![]() 10.95sec (x2.75) Satabs-prefix-first: ![]() CBMC-WMM: ![]() CBMC-SC: ![]() CImpact: ERROR/TIMEOUT[8] 371.52sec Checkfence: 0.01sec ESBMC: 0.07sec Threader-monolithic: ERROR/TIMEOUT[1] 0.12sec Threader-owicki-gries: ERROR/TIMEOUT[1] 0.11sec Threader-rely-guarantee: ERROR/TIMEOUT[1] 0.10sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT MMChecker (MM: csharp): ERROR/TIMEOUT[2] 0.00sec |
Cycles
SatAbs: ![]() 8.99sec (x2.25) Satabs-prefix-first: ![]() CBMC-WMM: ![]() CBMC-SC: ![]() CImpact: ERROR/TIMEOUT[8] 276.54sec ESBMC: 0.08sec Threader-monolithic: ERROR/TIMEOUT[1] 0.11sec Threader-owicki-gries: ERROR/TIMEOUT[1] 0.11sec Threader-rely-guarantee: ERROR/TIMEOUT[1] 0.10sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT MMChecker (MM: csharp): ERROR/TIMEOUT[2] 0.00sec |
Cycles
SatAbs: ![]() 7.52sec (x1.88) Satabs-prefix-first: ![]() CBMC-WMM: ![]() CBMC-SC: ![]() CImpact: ERROR/TIMEOUT[8] 357.00sec ESBMC: 0.09sec 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 MMChecker (MM: csharp): ERROR/TIMEOUT[2] 0.00sec |
![]() |
Cycles
SatAbs: ![]() 7.75sec (x1.94) Satabs-prefix-first: ![]() CBMC-WMM: ![]() CBMC-SC: ![]() CImpact: ERROR/TIMEOUT[8] 342.59sec ESBMC: 0.08sec Threader-monolithic: ERROR/TIMEOUT[1] 0.11sec Threader-owicki-gries: ERROR/TIMEOUT[1] 0.12sec Threader-rely-guarantee: ERROR/TIMEOUT[1] 0.11sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT Blender: ![]() |
Cycles
SatAbs: ![]() 7.50sec (x1.88) Satabs-prefix-first: ![]() CBMC-WMM: ![]() CBMC-SC: ![]() CImpact: ERROR/TIMEOUT[8] 271.82sec 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.10sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT Blender: ![]() |
Cycles
SatAbs: ![]() 7.62sec (x1.91) Satabs-prefix-first: ![]() CBMC-WMM: ![]() CBMC-SC: ![]() CImpact: ERROR/TIMEOUT[8] 343.70sec ESBMC: 0.10sec Threader-monolithic: ERROR/TIMEOUT[1] 0.11sec Threader-owicki-gries: ERROR/TIMEOUT[1] 0.12sec Threader-rely-guarantee: ERROR/TIMEOUT[1] 0.12sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT Blender: ![]() |
![]() |
Cycles
SatAbs: ![]() 109.07sec (x27.40) Satabs-prefix-first: ERROR/TIMEOUT[100] 626.15sec CBMC-WMM: ![]() CBMC-SC: ![]() CImpact: ERROR/TIMEOUT[8] 407.37sec ESBMC: 0.10sec Threader-monolithic: ERROR/TIMEOUT[130] 897.44sec Threader-owicki-gries: ERROR/TIMEOUT[130] 897.40sec Threader-rely-guarantee: ERROR/TIMEOUT[130] 897.21sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT |
Cycles
SatAbs: ![]() 110.75sec (x27.82) Satabs-prefix-first: ERROR/TIMEOUT[100] 536.66sec CBMC-WMM: ![]() CBMC-SC: ![]() CImpact: ERROR/TIMEOUT[8] 441.68sec ESBMC: 0.11sec Threader-monolithic: ERROR/TIMEOUT[130] 896.03sec Threader-owicki-gries: ERROR/TIMEOUT[130] 897.32sec Threader-rely-guarantee: ERROR/TIMEOUT[130] 897.48sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT |
Cycles
SatAbs: ![]() 114.18sec (x28.68) Satabs-prefix-first: ERROR/TIMEOUT[100] 668.71sec CBMC-WMM: ![]() CBMC-SC: ![]() CImpact: ERROR/TIMEOUT[8] 404.63sec ESBMC: 0.11sec Threader-monolithic: ERROR/TIMEOUT[130] 897.12sec Threader-owicki-gries: ERROR/TIMEOUT[130] 897.41sec Threader-rely-guarantee: ERROR/TIMEOUT[130] 897.65sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT |
![]() |
Cycles
SatAbs: ![]() 202.45sec (x50.86) Satabs-prefix-first: ERROR/TIMEOUT[130] 928.10sec CBMC-WMM: ![]() CBMC-SC: ![]() CImpact: ERROR/TIMEOUT[8] 328.69sec ESBMC: 0.09sec Threader-monolithic: ERROR/TIMEOUT[130] 897.36sec Threader-owicki-gries: ERROR/TIMEOUT[130] 897.34sec Threader-rely-guarantee: ERROR/TIMEOUT[130] 897.43sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT |
Cycles
SatAbs: ![]() 96.12sec (x24.15) Satabs-prefix-first: ERROR/TIMEOUT[130] 897.08sec CBMC-WMM: ![]() CBMC-SC: ![]() CImpact: ERROR/TIMEOUT[8] 358.27sec ESBMC: 0.11sec Threader-monolithic: ERROR/TIMEOUT[130] 897.49sec Threader-owicki-gries: ERROR/TIMEOUT[130] 897.53sec Threader-rely-guarantee: ERROR/TIMEOUT[130] 897.53sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT |
Cycles
SatAbs: ![]() 95.36sec (x23.95) Satabs-prefix-first: ERROR/TIMEOUT[130] 897.30sec CBMC-WMM: ![]() CBMC-SC: ![]() CImpact: ERROR/TIMEOUT[8] 254.84sec ESBMC: 0.10sec Threader-monolithic: ERROR/TIMEOUT[130] 897.40sec Threader-owicki-gries: ERROR/TIMEOUT[130] 895.72sec Threader-rely-guarantee: ERROR/TIMEOUT[130] 895.96sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT |
![]() |