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/rfe (tooling date Sun Jan 22 02:23:23 GMT 2012)
This family corresponds to litmus tests showing that Power relaxes the atomicity of 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/rfe000 |
SatAbs: ![]() 1.62sec Satabs-prefix-first: ![]() CBMC-WMM: ![]() CBMC-SC: ![]() CImpact: ![]() 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: ![]() 6.29sec (x3.88) Satabs-prefix-first: ![]() CBMC-WMM: ![]() CBMC-SC: ![]() CImpact: ![]() ESBMC: 0.12sec Threader-monolithic: ERROR/TIMEOUT[130] 896.01sec Threader-owicki-gries: ERROR/TIMEOUT[130] 896.84sec Threader-rely-guarantee: ERROR/TIMEOUT[130] 896.71sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT MMChecker (MM: csharp): ERROR/TIMEOUT[2] 0.00sec |
Cycles
SatAbs: ![]() 0.63sec (x.38) Satabs-prefix-first: ![]() CBMC-WMM: ![]() CBMC-SC: ![]() CImpact: ![]() Checkfence: 0.01sec 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.12sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT MMChecker (MM: csharp): ERROR/TIMEOUT[2] 0.00sec |
Cycles
SatAbs: ![]() 0.56sec (x.34) Satabs-prefix-first: ![]() CBMC-WMM: ![]() CBMC-SC: ![]() CImpact: ![]() 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.10sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT MMChecker (MM: csharp): ERROR/TIMEOUT[2] 0.00sec |
Cycles
SatAbs: ![]() 0.66sec (x.40) Satabs-prefix-first: ![]() CBMC-WMM: ![]() CBMC-SC: ![]() CImpact: ![]() 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.10sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT MMChecker (MM: csharp): ERROR/TIMEOUT[2] 0.00sec |
(thin-air) ![]() |
Cycles
SatAbs: ![]() 0.59sec (x.36) Satabs-prefix-first: ![]() CBMC-WMM: ![]() CBMC-SC: ![]() CImpact: ![]() 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.12sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT Blender: ![]() |
Cycles
SatAbs: ![]() 0.62sec (x.38) Satabs-prefix-first: ![]() CBMC-WMM: ![]() CBMC-SC: ![]() CImpact: ![]() 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 Blender: ![]() |
Cycles
SatAbs: ![]() 0.70sec (x.43) Satabs-prefix-first: ![]() CBMC-WMM: ![]() CBMC-SC: ![]() CImpact: ![]() ESBMC: 0.09sec 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: ![]() |
(thin-air) ![]() |
Cycles
SatAbs: ![]() 0.55sec (x.33) Satabs-prefix-first: ![]() CBMC-WMM: ![]() CBMC-SC: ![]() CImpact: ![]() ESBMC: 0.07sec Threader-monolithic: ERROR/TIMEOUT[1] 0.11sec Threader-owicki-gries: ERROR/TIMEOUT[1] 0.09sec Threader-rely-guarantee: ERROR/TIMEOUT[1] 0.10sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT |
Cycles
SatAbs: ![]() 0.63sec (x.38) Satabs-prefix-first: ![]() CBMC-WMM: ![]() CBMC-SC: ![]() CImpact: ![]() ESBMC: 0.08sec Threader-monolithic: ERROR/TIMEOUT[1] 0.11sec Threader-owicki-gries: ERROR/TIMEOUT[1] 0.08sec Threader-rely-guarantee: ERROR/TIMEOUT[1] 0.12sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT |
Cycles
SatAbs: ![]() 0.60sec (x.37) Satabs-prefix-first: ![]() CBMC-WMM: ![]() CBMC-SC: ![]() CImpact: ![]() 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.11sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT |
(thin-air) ![]() |
Cycles
SatAbs: ![]() 0.66sec (x.40) 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.10sec Threader-rely-guarantee: ERROR/TIMEOUT[1] 0.12sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT |
Cycles
SatAbs: ![]() 0.68sec (x.41) Satabs-prefix-first: ![]() CBMC-WMM: ![]() CBMC-SC: ![]() CImpact: ![]() ESBMC: 0.09sec Threader-monolithic: ERROR/TIMEOUT[1] 0.12sec Threader-owicki-gries: ERROR/TIMEOUT[1] 0.09sec Threader-rely-guarantee: ERROR/TIMEOUT[1] 0.12sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT |
Cycles
SatAbs: ![]() 0.61sec (x.37) Satabs-prefix-first: ![]() CBMC-WMM: ![]() CBMC-SC: ![]() CImpact: ![]() ESBMC: 0.07sec 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 |
(thin-air) ![]() |
ppc/rfe001 |
SatAbs: ![]() 3.01sec Satabs-prefix-first: ![]() CBMC-WMM: ![]() CBMC-SC: ![]() CImpact: ERROR/TIMEOUT[8] 325.45sec 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: ![]() 19.48sec (x6.47) Satabs-prefix-first: ![]() CBMC-WMM: ![]() CBMC-SC: ![]() CImpact: ERROR/TIMEOUT[8] 427.32sec ESBMC: 0.12sec Threader-monolithic: ERROR/TIMEOUT[130] 897.04sec Threader-owicki-gries: ERROR/TIMEOUT[130] 897.17sec Threader-rely-guarantee: ERROR/TIMEOUT[130] 897.20sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT MMChecker (MM: csharp): ERROR/TIMEOUT[2] 0.00sec |
Cycles
SatAbs: ![]() 2.09sec (x.69) Satabs-prefix-first: ![]() CBMC-WMM: ![]() CBMC-SC: ![]() CImpact: ERROR/TIMEOUT[8] 384.46sec Checkfence: 0.01sec ESBMC: 0.09sec Threader-monolithic: ERROR/TIMEOUT[1] 0.09sec Threader-owicki-gries: ERROR/TIMEOUT[1] 0.13sec Threader-rely-guarantee: ERROR/TIMEOUT[1] 0.12sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT MMChecker (MM: csharp): ERROR/TIMEOUT[2] 0.01sec |
Cycles
SatAbs: ![]() 1.55sec (x.51) Satabs-prefix-first: ![]() CBMC-WMM: ![]() CBMC-SC: ![]() CImpact: ERROR/TIMEOUT[8] 331.33sec ESBMC: 0.11sec Threader-monolithic: ERROR/TIMEOUT[1] 0.14sec 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: ![]() 1.42sec (x.47) Satabs-prefix-first: ![]() CBMC-WMM: ![]() CBMC-SC: ![]() CImpact: ERROR/TIMEOUT[8] 305.33sec ESBMC: 0.11sec Threader-monolithic: ERROR/TIMEOUT[1] 0.13sec Threader-owicki-gries: ERROR/TIMEOUT[1] 0.12sec Threader-rely-guarantee: ERROR/TIMEOUT[1] 0.08sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT MMChecker (MM: csharp): ERROR/TIMEOUT[2] 0.00sec |
(thin-air) ![]() |
Cycles
SatAbs: ![]() 1.62sec (x.53) Satabs-prefix-first: ![]() CBMC-WMM: ![]() CBMC-SC: ![]() CImpact: ERROR/TIMEOUT[8] 330.25sec ESBMC: 0.08sec Threader-monolithic: ERROR/TIMEOUT[1] 0.12sec 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: ![]() 1.36sec (x.45) Satabs-prefix-first: ![]() CBMC-WMM: ![]() CBMC-SC: ![]() CImpact: ERROR/TIMEOUT[8] 331.03sec ESBMC: 0.10sec Threader-monolithic: ERROR/TIMEOUT[1] 0.10sec 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: ![]() 1.54sec (x.51) Satabs-prefix-first: ![]() CBMC-WMM: ![]() CBMC-SC: ![]() CImpact: ERROR/TIMEOUT[8] 346.15sec ESBMC: 0.09sec Threader-monolithic: ERROR/TIMEOUT[1] 0.12sec Threader-owicki-gries: ERROR/TIMEOUT[1] 0.12sec Threader-rely-guarantee: ERROR/TIMEOUT[1] 0.10sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT Blender: ![]() |
(thin-air) ![]() |
Cycles
SatAbs: ![]() 1.43sec (x.47) Satabs-prefix-first: ![]() CBMC-WMM: ![]() CBMC-SC: ![]() CImpact: ERROR/TIMEOUT[8] 244.54sec ESBMC: 0.09sec Threader-monolithic: ERROR/TIMEOUT[1] 0.10sec Threader-owicki-gries: ERROR/TIMEOUT[1] 0.08sec Threader-rely-guarantee: ERROR/TIMEOUT[1] 0.11sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT |
Cycles
SatAbs: ![]() 1.46sec (x.48) Satabs-prefix-first: ![]() CBMC-WMM: ![]() CBMC-SC: ![]() CImpact: ERROR/TIMEOUT[8] 353.79sec ESBMC: 0.08sec Threader-monolithic: ERROR/TIMEOUT[1] 0.12sec Threader-owicki-gries: ERROR/TIMEOUT[1] 0.12sec Threader-rely-guarantee: ERROR/TIMEOUT[1] 0.12sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT |
Cycles
SatAbs: ![]() 1.49sec (x.49) Satabs-prefix-first: ![]() CBMC-WMM: ![]() CBMC-SC: ![]() CImpact: ERROR/TIMEOUT[8] 349.38sec ESBMC: 0.09sec Threader-monolithic: ERROR/TIMEOUT[1] 0.12sec Threader-owicki-gries: ERROR/TIMEOUT[1] 0.14sec Threader-rely-guarantee: ERROR/TIMEOUT[1] 0.11sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT |
(thin-air) ![]() |
Cycles
SatAbs: ![]() 1.61sec (x.53) Satabs-prefix-first: ![]() CBMC-WMM: ![]() CBMC-SC: ![]() CImpact: ERROR/TIMEOUT[8] 352.09sec 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.12sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT |
Cycles
SatAbs: ![]() 1.52sec (x.50) Satabs-prefix-first: ![]() CBMC-WMM: ![]() CBMC-SC: ![]() CImpact: ERROR/TIMEOUT[8] 327.02sec 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 |
Cycles
SatAbs: ![]() 1.53sec (x.50) Satabs-prefix-first: ![]() CBMC-WMM: ![]() CBMC-SC: ![]() CImpact: ERROR/TIMEOUT[8] 340.77sec ESBMC: 0.08sec 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 |
(thin-air) ![]() |
ppc/rfe002 |
SatAbs: ![]() 7.92sec Satabs-prefix-first: ![]() CBMC-WMM: ![]() CBMC-SC: ![]() CImpact: ERROR/TIMEOUT[8] 306.56sec Checkfence: 0.01sec ESBMC: 0.08sec 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: ![]() 2.43sec (x.30) Satabs-prefix-first: ![]() CBMC-WMM: ![]() CBMC-SC: ![]() CImpact: ERROR/TIMEOUT[8] 396.62sec ESBMC: 0.10sec Threader-monolithic: ERROR/TIMEOUT[130] 896.90sec Threader-owicki-gries: ERROR/TIMEOUT[130] 897.47sec Threader-rely-guarantee: ERROR/TIMEOUT[130] 897.61sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT MMChecker (MM: csharp): ERROR/TIMEOUT[2] 0.01sec |
Cycles
SatAbs: ![]() 8.84sec (x1.11) Satabs-prefix-first: ![]() CBMC-WMM: ![]() CBMC-SC: ![]() CImpact: ERROR/TIMEOUT[8] 303.23sec Checkfence: 0.01sec 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.13sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT MMChecker (MM: csharp): ERROR/TIMEOUT[2] 0.00sec |
Cycles
SatAbs: ![]() 11.26sec (x1.42) Satabs-prefix-first: ![]() CBMC-WMM: ![]() CBMC-SC: ![]() CImpact: ERROR/TIMEOUT[8] 315.79sec 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 MMChecker (MM: csharp): ERROR/TIMEOUT[2] 0.01sec |
Cycles
SatAbs: ![]() 8.66sec (x1.09) Satabs-prefix-first: ![]() CBMC-WMM: ![]() CBMC-SC: ![]() CImpact: ERROR/TIMEOUT[8] 311.98sec 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 MMChecker (MM: csharp): ERROR/TIMEOUT[2] 0.01sec |
![]() |
Cycles
SatAbs: ![]() 8.42sec (x1.06) Satabs-prefix-first: ![]() CBMC-WMM: ![]() CBMC-SC: ![]() CImpact: ERROR/TIMEOUT[8] 267.85sec ESBMC: 0.09sec 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 Blender: ![]() |
Cycles
SatAbs: ![]() 9.01sec (x1.13) Satabs-prefix-first: ![]() CBMC-WMM: ![]() CBMC-SC: ![]() CImpact: ERROR/TIMEOUT[8] 276.60sec 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 Blender: ![]() |
Cycles
SatAbs: ![]() 9.20sec (x1.16) Satabs-prefix-first: ![]() CBMC-WMM: ![]() CBMC-SC: ![]() CImpact: ERROR/TIMEOUT[8] 321.26sec ESBMC: 0.07sec 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: ![]() 8.48sec (x1.07) Satabs-prefix-first: ![]() CBMC-WMM: ![]() CBMC-SC: ![]() CImpact: ERROR/TIMEOUT[8] 317.42sec 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.12sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT |
Cycles
SatAbs: ![]() 8.65sec (x1.09) Satabs-prefix-first: ![]() CBMC-WMM: ![]() CBMC-SC: ![]() CImpact: ERROR/TIMEOUT[8] 316.88sec 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 |
Cycles
SatAbs: ![]() 8.62sec (x1.08) Satabs-prefix-first: ![]() CBMC-WMM: ![]() CBMC-SC: ![]() CImpact: ERROR/TIMEOUT[8] 314.99sec ESBMC: 0.09sec Threader-monolithic: ERROR/TIMEOUT[1] 0.10sec Threader-owicki-gries: ERROR/TIMEOUT[1] 0.12sec Threader-rely-guarantee: ERROR/TIMEOUT[1] 0.10sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT |
![]() |
Cycles
SatAbs: ![]() 12.64sec (x1.59) Satabs-prefix-first: ![]() CBMC-WMM: ![]() CBMC-SC: ![]() CImpact: ![]() ESBMC: 0.12sec Threader-monolithic: ERROR/TIMEOUT[130] 896.58sec Threader-owicki-gries: ERROR/TIMEOUT[130] 896.74sec Threader-rely-guarantee: ERROR/TIMEOUT[130] 897.17sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT |
Cycles
SatAbs: ![]() 97.50sec (x12.31) Satabs-prefix-first: ![]() CBMC-WMM: ![]() CBMC-SC: ![]() CImpact: ERROR/TIMEOUT[8] 381.03sec ESBMC: 0.09sec Threader-monolithic: ERROR/TIMEOUT[130] 897.49sec Threader-owicki-gries: ERROR/TIMEOUT[130] 896.77sec Threader-rely-guarantee: ERROR/TIMEOUT[130] 897.22sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT |
Cycles
SatAbs: ![]() 98.83sec (x12.47) Satabs-prefix-first: ![]() CBMC-WMM: ![]() CBMC-SC: ![]() CImpact: ERROR/TIMEOUT[8] 371.11sec ESBMC: 0.09sec Threader-monolithic: ERROR/TIMEOUT[130] 896.55sec Threader-owicki-gries: ERROR/TIMEOUT[130] 897.41sec Threader-rely-guarantee: ERROR/TIMEOUT[130] 897.43sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT |
![]() |
ppc/rfe003 |
SatAbs: ![]() 10.12sec Satabs-prefix-first: ![]() CBMC-WMM: ![]() CBMC-SC: ![]() CImpact: ERROR/TIMEOUT[8] 223.51sec 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.08sec |
Cycles
SatAbs: ![]() 52.39sec (x5.17) Satabs-prefix-first: ![]() CBMC-WMM: ![]() CBMC-SC: ![]() CImpact: ERROR/TIMEOUT[8] 304.38sec ESBMC: 0.12sec Threader-monolithic: ERROR/TIMEOUT[130] 897.01sec Threader-owicki-gries: ERROR/TIMEOUT[130] 896.77sec Threader-rely-guarantee: ERROR/TIMEOUT[130] 896.93sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT MMChecker (MM: csharp): ERROR/TIMEOUT[2] 0.00sec |
Cycles
SatAbs: ![]() 10.14sec (x1.00) Satabs-prefix-first: ![]() CBMC-WMM: ![]() CBMC-SC: ![]() CImpact: ERROR/TIMEOUT[8] 309.70sec Checkfence: 0.01sec ESBMC: 0.08sec Threader-monolithic: ERROR/TIMEOUT[1] 0.10sec Threader-owicki-gries: ERROR/TIMEOUT[1] 0.10sec 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: ![]() 12.67sec (x1.25) Satabs-prefix-first: ![]() CBMC-WMM: ![]() CBMC-SC: ![]() CImpact: ERROR/TIMEOUT[8] 306.90sec 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.12sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT MMChecker (MM: csharp): ERROR/TIMEOUT[2] 0.00sec |
Cycles
SatAbs: ![]() 10.99sec (x1.08) Satabs-prefix-first: ![]() CBMC-WMM: ![]() CBMC-SC: ![]() CImpact: ERROR/TIMEOUT[8] 244.93sec ESBMC: 0.08sec 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): ERROR/TIMEOUT[2] 0.00sec |
![]() |
Cycles
SatAbs: ![]() 10.35sec (x1.02) Satabs-prefix-first: ![]() CBMC-WMM: ![]() CBMC-SC: ![]() CImpact: ERROR/TIMEOUT[8] 315.51sec ESBMC: 0.09sec Threader-monolithic: ERROR/TIMEOUT[1] 0.10sec Threader-owicki-gries: ERROR/TIMEOUT[1] 0.09sec Threader-rely-guarantee: ERROR/TIMEOUT[1] 0.12sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT Blender: ![]() |
Cycles
SatAbs: ![]() 10.43sec (x1.03) Satabs-prefix-first: ![]() CBMC-WMM: ![]() CBMC-SC: ![]() CImpact: ERROR/TIMEOUT[8] 208.22sec ESBMC: 0.10sec 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 Blender: ![]() |
Cycles
SatAbs: ![]() 10.43sec (x1.03) Satabs-prefix-first: ![]() CBMC-WMM: ![]() CBMC-SC: ![]() CImpact: ERROR/TIMEOUT[8] 315.20sec ESBMC: 0.08sec Threader-monolithic: ERROR/TIMEOUT[1] 0.10sec Threader-owicki-gries: ERROR/TIMEOUT[1] 0.13sec Threader-rely-guarantee: ERROR/TIMEOUT[1] 0.12sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT Blender: ![]() |
![]() |
Cycles
SatAbs: ![]() 9.79sec (x.96) Satabs-prefix-first: ![]() CBMC-WMM: ![]() CBMC-SC: ![]() CImpact: ERROR/TIMEOUT[8] 298.02sec ESBMC: 0.10sec 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 |
Cycles
SatAbs: ![]() 9.61sec (x.94) Satabs-prefix-first: ![]() CBMC-WMM: ![]() CBMC-SC: ![]() CImpact: ERROR/TIMEOUT[8] 329.00sec 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.12sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT |
Cycles
SatAbs: ![]() 11.81sec (x1.16) Satabs-prefix-first: ![]() CBMC-WMM: ![]() CBMC-SC: ![]() CImpact: ERROR/TIMEOUT[8] 304.46sec 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.12sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT |
![]() |
Cycles
SatAbs: ![]() 278.47sec (x27.51) Satabs-prefix-first: ![]() CBMC-WMM: ![]() CBMC-SC: ![]() CImpact: ![]() ESBMC: 0.17sec Threader-monolithic: ERROR/TIMEOUT[130] 885.31sec Threader-owicki-gries: ERROR/TIMEOUT[130] 895.08sec Threader-rely-guarantee: ERROR/TIMEOUT[130] 897.68sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT |
Cycles
SatAbs: ![]() 85.95sec (x8.49) Satabs-prefix-first: ![]() CBMC-WMM: ![]() CBMC-SC: ![]() CImpact: ERROR/TIMEOUT[8] 322.29sec ESBMC: 0.11sec Threader-monolithic: ERROR/TIMEOUT[1] 448.28sec Threader-owicki-gries: ERROR/TIMEOUT[1] 331.35sec Threader-rely-guarantee: ERROR/TIMEOUT[1] 357.14sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT |
Cycles
SatAbs: ![]() 85.73sec (x8.47) Satabs-prefix-first: ![]() CBMC-WMM: ![]() CBMC-SC: ![]() CImpact: ERROR/TIMEOUT[8] 354.92sec ESBMC: 0.10sec Threader-monolithic: ERROR/TIMEOUT[1] 418.04sec Threader-owicki-gries: ERROR/TIMEOUT[1] 380.51sec Threader-rely-guarantee: ERROR/TIMEOUT[1] 316.51sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT |
![]() |
ppc/rfe004 |
SatAbs: ![]() 26.21sec Satabs-prefix-first: ![]() CBMC-WMM: ![]() CBMC-SC: ![]() CImpact: ERROR/TIMEOUT[8] 293.13sec Checkfence: 0.01sec ESBMC: 0.08sec 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: ![]() 3.33sec (x.12) Satabs-prefix-first: ![]() CBMC-WMM: ![]() CBMC-SC: ![]() CImpact: ![]() ESBMC: 0.13sec Threader-monolithic: ERROR/TIMEOUT[130] 897.62sec Threader-owicki-gries: ERROR/TIMEOUT[130] 897.62sec Threader-rely-guarantee: ERROR/TIMEOUT[130] 897.66sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT MMChecker (MM: csharp): ERROR/TIMEOUT[2] 0.00sec |
Cycles
SatAbs: ![]() 34.29sec (x1.30) Satabs-prefix-first: ![]() CBMC-WMM: ![]() CBMC-SC: ![]() CImpact: ERROR/TIMEOUT[8] 241.67sec Checkfence: 0.01sec ESBMC: 0.08sec Threader-monolithic: ERROR/TIMEOUT[1] 0.12sec Threader-owicki-gries: ERROR/TIMEOUT[1] 0.10sec 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: ![]() 34.31sec (x1.30) Satabs-prefix-first: ![]() CBMC-WMM: ![]() CBMC-SC: ![]() CImpact: ERROR/TIMEOUT[8] 328.51sec ESBMC: 0.07sec Threader-monolithic: ERROR/TIMEOUT[1] 0.12sec Threader-owicki-gries: ERROR/TIMEOUT[1] 0.13sec Threader-rely-guarantee: ERROR/TIMEOUT[1] 0.13sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT MMChecker (MM: csharp): ERROR/TIMEOUT[2] 0.00sec |
Cycles
SatAbs: ![]() 34.77sec (x1.32) Satabs-prefix-first: ![]() CBMC-WMM: ![]() CBMC-SC: ![]() CImpact: ERROR/TIMEOUT[8] 331.95sec 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.09sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT MMChecker (MM: csharp): ERROR/TIMEOUT[2] 0.01sec |
![]() |
Cycles
SatAbs: ![]() 35.09sec (x1.33) Satabs-prefix-first: ![]() CBMC-WMM: ![]() CBMC-SC: ![]() CImpact: ERROR/TIMEOUT[8] 330.02sec ESBMC: 0.08sec Threader-monolithic: ERROR/TIMEOUT[1] 0.11sec Threader-owicki-gries: ERROR/TIMEOUT[1] 0.13sec Threader-rely-guarantee: ERROR/TIMEOUT[1] 0.13sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT Blender: ![]() |
Cycles
SatAbs: ![]() 35.30sec (x1.34) Satabs-prefix-first: ![]() CBMC-WMM: ![]() CBMC-SC: ![]() CImpact: ERROR/TIMEOUT[8] 255.81sec ESBMC: 0.05sec Threader-monolithic: ERROR/TIMEOUT[1] 0.12sec Threader-owicki-gries: ERROR/TIMEOUT[1] 0.13sec Threader-rely-guarantee: ERROR/TIMEOUT[1] 0.13sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT Blender: ![]() |
Cycles
SatAbs: ![]() 34.46sec (x1.31) Satabs-prefix-first: ![]() CBMC-WMM: ![]() CBMC-SC: ![]() CImpact: ERROR/TIMEOUT[8] 231.79sec ESBMC: 0.09sec Threader-monolithic: ERROR/TIMEOUT[1] 0.12sec Threader-owicki-gries: ERROR/TIMEOUT[1] 0.13sec Threader-rely-guarantee: ERROR/TIMEOUT[1] 0.10sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT Blender: ![]() |
![]() |
Cycles
SatAbs: ![]() 34.98sec (x1.33) Satabs-prefix-first: ![]() CBMC-WMM: ![]() CBMC-SC: ![]() CImpact: ERROR/TIMEOUT[8] 339.82sec ESBMC: 0.08sec Threader-monolithic: ERROR/TIMEOUT[1] 0.13sec Threader-owicki-gries: ERROR/TIMEOUT[1] 0.11sec Threader-rely-guarantee: ERROR/TIMEOUT[1] 0.13sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT |
Cycles
SatAbs: ![]() 33.49sec (x1.27) Satabs-prefix-first: ![]() CBMC-WMM: ![]() CBMC-SC: ![]() CImpact: ERROR/TIMEOUT[8] 342.27sec ESBMC: 0.10sec Threader-monolithic: ERROR/TIMEOUT[1] 0.13sec Threader-owicki-gries: ERROR/TIMEOUT[1] 0.13sec Threader-rely-guarantee: ERROR/TIMEOUT[1] 0.11sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT |
Cycles
SatAbs: ![]() 34.37sec (x1.31) Satabs-prefix-first: ![]() CBMC-WMM: ![]() CBMC-SC: ![]() CImpact: ERROR/TIMEOUT[8] 282.03sec ESBMC: 0.09sec Threader-monolithic: ERROR/TIMEOUT[1] 0.13sec Threader-owicki-gries: ERROR/TIMEOUT[1] 0.08sec Threader-rely-guarantee: ERROR/TIMEOUT[1] 0.12sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT |
![]() |
Cycles
SatAbs: ![]() 17.63sec (x.67) Satabs-prefix-first: ![]() CBMC-WMM: ![]() CBMC-SC: ![]() CImpact: ![]() ESBMC: 0.12sec Threader-monolithic: ERROR/TIMEOUT[130] 897.23sec Threader-owicki-gries: ERROR/TIMEOUT[130] 897.74sec Threader-rely-guarantee: ERROR/TIMEOUT[130] 897.82sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT |
Cycles
SatAbs: ![]() 3.11sec (x.11) Satabs-prefix-first: ![]() CBMC-WMM: ![]() CBMC-SC: ![]() CImpact: ERROR/TIMEOUT[8] 313.01sec ESBMC: 0.08sec Threader-monolithic: ERROR/TIMEOUT[130] 897.43sec Threader-owicki-gries: ERROR/TIMEOUT[130] 897.39sec Threader-rely-guarantee: ERROR/TIMEOUT[130] 897.27sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT |
Cycles
SatAbs: ![]() 50.61sec (x1.93) Satabs-prefix-first: ![]() CBMC-WMM: ![]() CBMC-SC: ![]() CImpact: ![]() ESBMC: 0.10sec Threader-monolithic: ERROR/TIMEOUT[130] 896.46sec Threader-owicki-gries: ERROR/TIMEOUT[130] 897.12sec Threader-rely-guarantee: ERROR/TIMEOUT[130] 897.47sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT |
![]() |
ppc/rfe005 |
SatAbs: ![]() 21.57sec Satabs-prefix-first: ![]() CBMC-WMM: ![]() CBMC-SC: ![]() CImpact: ERROR/TIMEOUT[8] 257.98sec 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: ![]() 21.20sec (x.98) Satabs-prefix-first: ![]() CBMC-WMM: ![]() CBMC-SC: ![]() CImpact: ![]() ESBMC: 0.10sec Threader-monolithic: ERROR/TIMEOUT[130] 896.59sec Threader-owicki-gries: ERROR/TIMEOUT[130] 897.56sec Threader-rely-guarantee: ERROR/TIMEOUT[130] 897.48sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT MMChecker (MM: csharp): ERROR/TIMEOUT[2] 0.00sec |
Cycles
SatAbs: ![]() 37.03sec (x1.71) Satabs-prefix-first: ![]() CBMC-WMM: ![]() CBMC-SC: ![]() CImpact: ERROR/TIMEOUT[8] 268.82sec Checkfence: 0.01sec ESBMC: 0.08sec Threader-monolithic: ERROR/TIMEOUT[1] 0.12sec Threader-owicki-gries: ERROR/TIMEOUT[1] 0.10sec Threader-rely-guarantee: ERROR/TIMEOUT[1] 0.08sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT MMChecker (MM: csharp): ERROR/TIMEOUT[2] 0.00sec |
Cycles
SatAbs: ![]() 38.70sec (x1.79) Satabs-prefix-first: ![]() CBMC-WMM: ![]() CBMC-SC: ![]() CImpact: ERROR/TIMEOUT[8] 313.23sec ESBMC: 0.09sec Threader-monolithic: ERROR/TIMEOUT[1] 0.13sec Threader-owicki-gries: ERROR/TIMEOUT[1] 0.12sec Threader-rely-guarantee: ERROR/TIMEOUT[1] 0.13sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT MMChecker (MM: csharp): ERROR/TIMEOUT[2] 0.00sec |
Cycles
SatAbs: ![]() 43.74sec (x2.02) Satabs-prefix-first: ![]() CBMC-WMM: ![]() CBMC-SC: ![]() CImpact: ERROR/TIMEOUT[8] 226.98sec ESBMC: 0.06sec Threader-monolithic: ERROR/TIMEOUT[1] 0.12sec 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: ![]() 38.35sec (x1.77) Satabs-prefix-first: ![]() CBMC-WMM: ![]() CBMC-SC: ![]() CImpact: ERROR/TIMEOUT[8] 313.25sec ESBMC: 0.09sec Threader-monolithic: ERROR/TIMEOUT[1] 0.13sec Threader-owicki-gries: ERROR/TIMEOUT[1] 0.12sec Threader-rely-guarantee: ERROR/TIMEOUT[1] 0.13sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT Blender: ![]() |
Cycles
SatAbs: ![]() 37.81sec (x1.75) Satabs-prefix-first: ![]() CBMC-WMM: ![]() CBMC-SC: ![]() CImpact: ERROR/TIMEOUT[8] 202.58sec ESBMC: 0.08sec Threader-monolithic: ERROR/TIMEOUT[1] 0.13sec 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: ![]() 39.33sec (x1.82) Satabs-prefix-first: ![]() CBMC-WMM: ![]() CBMC-SC: ![]() CImpact: ERROR/TIMEOUT[8] 284.62sec 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.11sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT Blender: ![]() |
![]() |
Cycles
SatAbs: ![]() 37.59sec (x1.74) Satabs-prefix-first: ![]() CBMC-WMM: ![]() CBMC-SC: ![]() CImpact: ERROR/TIMEOUT[8] 312.22sec ESBMC: 0.10sec Threader-monolithic: ERROR/TIMEOUT[1] 0.11sec Threader-owicki-gries: ERROR/TIMEOUT[1] 0.10sec Threader-rely-guarantee: ERROR/TIMEOUT[1] 0.10sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT |
Cycles
SatAbs: ![]() 40.54sec (x1.87) Satabs-prefix-first: ![]() CBMC-WMM: ![]() CBMC-SC: ![]() CImpact: ERROR/TIMEOUT[8] 311.09sec 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.13sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT |
Cycles
SatAbs: ![]() 38.91sec (x1.80) Satabs-prefix-first: ![]() CBMC-WMM: ![]() CBMC-SC: ![]() CImpact: ERROR/TIMEOUT[8] 311.59sec ESBMC: 0.06sec Threader-monolithic: ERROR/TIMEOUT[1] 0.13sec Threader-owicki-gries: ERROR/TIMEOUT[1] 0.13sec Threader-rely-guarantee: ERROR/TIMEOUT[1] 0.13sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT |
![]() |
Cycles
SatAbs: ERROR/TIMEOUT[130] Satabs-prefix-first: ![]() CBMC-WMM: ![]() CBMC-SC: ![]() CImpact: ![]() ESBMC: 0.14sec Threader-monolithic: ERROR/TIMEOUT[130] 897.09sec Threader-owicki-gries: ERROR/TIMEOUT[130] 895.63sec Threader-rely-guarantee: ERROR/TIMEOUT[130] 896.82sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT |
Cycles
SatAbs: ![]() 360.93sec (x16.73) Satabs-prefix-first: ![]() CBMC-WMM: ![]() CBMC-SC: ![]() CImpact: ERROR/TIMEOUT[8] 320.11sec ESBMC: 0.18sec Threader-monolithic: ERROR/TIMEOUT[1] 515.85sec Threader-owicki-gries: ERROR/TIMEOUT[1] 380.23sec Threader-rely-guarantee: ERROR/TIMEOUT[1] 531.64sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT |
Cycles
SatAbs: ![]() 337.21sec (x15.63) Satabs-prefix-first: ![]() CBMC-WMM: ![]() CBMC-SC: ![]() CImpact: ERROR/TIMEOUT[8] 394.91sec ESBMC: 0.08sec Threader-monolithic: ERROR/TIMEOUT[1] 502.42sec Threader-owicki-gries: ERROR/TIMEOUT[1] 464.44sec Threader-rely-guarantee: ERROR/TIMEOUT[1] 456.16sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT |
![]() |
ppc/rfe006 |
SatAbs: ![]() 21.59sec Satabs-prefix-first: ![]() CBMC-WMM: ![]() CBMC-SC: ![]() CImpact: ERROR/TIMEOUT[8] 360.00sec 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.00sec |
Cycles
SatAbs: ERROR/TIMEOUT[130] 1045.11sec (x48.40) Satabs-prefix-first: ![]() CBMC-WMM: ![]() CBMC-SC: ![]() CImpact: ERROR/TIMEOUT[8] 305.47sec ESBMC: 0.10sec Threader-monolithic: ERROR/TIMEOUT[130] 897.28sec Threader-owicki-gries: ERROR/TIMEOUT[130] 897.13sec Threader-rely-guarantee: ERROR/TIMEOUT[130] 897.11sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT MMChecker (MM: csharp): ERROR/TIMEOUT[2] 0.00sec |
Cycles
SatAbs: ![]() 66.43sec (x3.07) Satabs-prefix-first: ![]() CBMC-WMM: ![]() CBMC-SC: ![]() CImpact: ERROR/TIMEOUT[8] 283.43sec Checkfence: 0.01sec ESBMC: 0.08sec Threader-monolithic: ERROR/TIMEOUT[1] 0.13sec 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): ERROR/TIMEOUT[2] 0.00sec |
Cycles
SatAbs: ![]() 65.00sec (x3.01) Satabs-prefix-first: ![]() CBMC-WMM: ![]() CBMC-SC: ![]() CImpact: ERROR/TIMEOUT[8] 256.92sec ESBMC: 0.08sec Threader-monolithic: ERROR/TIMEOUT[1] 0.13sec Threader-owicki-gries: ERROR/TIMEOUT[1] 0.10sec Threader-rely-guarantee: ERROR/TIMEOUT[1] 0.13sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT MMChecker (MM: csharp): ERROR/TIMEOUT[2] 0.00sec |
Cycles
SatAbs: ![]() 61.17sec (x2.83) Satabs-prefix-first: ![]() CBMC-WMM: ![]() CBMC-SC: ![]() CImpact: ERROR/TIMEOUT[8] 262.63sec 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.13sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT MMChecker (MM: csharp): ERROR/TIMEOUT[2] 0.00sec |
![]() |
Cycles
SatAbs: ![]() 65.69sec (x3.04) Satabs-prefix-first: ![]() CBMC-WMM: ![]() CBMC-SC: ![]() CImpact: ERROR/TIMEOUT[8] 352.78sec ESBMC: 0.08sec Threader-monolithic: ERROR/TIMEOUT[1] 0.10sec Threader-owicki-gries: ERROR/TIMEOUT[1] 0.13sec Threader-rely-guarantee: ERROR/TIMEOUT[1] 0.13sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT Blender: ![]() |
Cycles
SatAbs: ![]() 67.28sec (x3.11) Satabs-prefix-first: ![]() CBMC-WMM: ![]() CBMC-SC: ![]() CImpact: ERROR/TIMEOUT[8] 331.38sec ESBMC: 0.09sec Threader-monolithic: ERROR/TIMEOUT[1] 0.12sec Threader-owicki-gries: ERROR/TIMEOUT[1] 0.09sec Threader-rely-guarantee: ERROR/TIMEOUT[1] 0.12sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT Blender: ![]() |
Cycles
SatAbs: ![]() 64.21sec (x2.97) Satabs-prefix-first: ![]() CBMC-WMM: ![]() CBMC-SC: ![]() CImpact: ERROR/TIMEOUT[8] 256.11sec ESBMC: 0.09sec Threader-monolithic: ERROR/TIMEOUT[1] 0.13sec 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: ![]() 63.61sec (x2.94) Satabs-prefix-first: ![]() CBMC-WMM: ![]() CBMC-SC: ![]() CImpact: ERROR/TIMEOUT[8] 334.41sec ESBMC: 0.08sec Threader-monolithic: ERROR/TIMEOUT[1] 0.12sec Threader-owicki-gries: ERROR/TIMEOUT[1] 0.10sec Threader-rely-guarantee: ERROR/TIMEOUT[1] 0.13sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT |
Cycles
SatAbs: ![]() 66.05sec (x3.05) Satabs-prefix-first: ![]() CBMC-WMM: ![]() CBMC-SC: ![]() CImpact: ERROR/TIMEOUT[8] 264.56sec ESBMC: 0.07sec Threader-monolithic: ERROR/TIMEOUT[1] 0.13sec Threader-owicki-gries: ERROR/TIMEOUT[1] 0.13sec Threader-rely-guarantee: ERROR/TIMEOUT[1] 0.13sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT |
Cycles
SatAbs: ![]() 65.92sec (x3.05) Satabs-prefix-first: ![]() CBMC-WMM: ![]() CBMC-SC: ![]() CImpact: ERROR/TIMEOUT[8] 279.53sec ESBMC: 0.09sec Threader-monolithic: ERROR/TIMEOUT[1] 0.13sec Threader-owicki-gries: ERROR/TIMEOUT[1] 0.13sec Threader-rely-guarantee: ERROR/TIMEOUT[1] 0.12sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT |
![]() |
Cycles
SatAbs: ERROR/TIMEOUT[130] 1161.75sec (x53.80) Satabs-prefix-first: ERROR/TIMEOUT[130] 1060.15sec CBMC-WMM: ![]() CBMC-SC: ![]() CImpact: ![]() ESBMC: 0.13sec Threader-monolithic: ERROR/TIMEOUT[130] 897.80sec Threader-owicki-gries: ERROR/TIMEOUT[130] 897.70sec Threader-rely-guarantee: ERROR/TIMEOUT[130] 897.80sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT |
Cycles
SatAbs: ![]() 629.20sec (x29.14) Satabs-prefix-first: ![]() CBMC-WMM: ![]() CBMC-SC: ![]() CImpact: ERROR/TIMEOUT[8] 403.93sec ESBMC: 0.09sec Threader-monolithic: ERROR/TIMEOUT[1] 383.18sec Threader-owicki-gries: ERROR/TIMEOUT[1] 408.71sec Threader-rely-guarantee: ERROR/TIMEOUT[1] 508.53sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT |
Cycles
SatAbs: ![]() 620.18sec (x28.72) Satabs-prefix-first: ![]() CBMC-WMM: ![]() CBMC-SC: ![]() CImpact: ERROR/TIMEOUT[8] 437.08sec ESBMC: 0.11sec Threader-monolithic: ERROR/TIMEOUT[1] 482.72sec Threader-owicki-gries: ERROR/TIMEOUT[1] 423.64sec Threader-rely-guarantee: ERROR/TIMEOUT[1] 435.49sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT |
![]() |