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/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: 4.16sec CBMC-WMM: 0.06sec CBMC-SC: 0.06sec CImpact: 2.41sec Checkfence: 0.01sec ESBMC: 0.09sec Threader-monolithic: 0.10sec Threader-owicki-gries: 0.12sec Threader-rely-guarantee: 0.14sec 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: 12.73sec CBMC-WMM: 0.10sec CBMC-SC: 5.95sec CImpact: 130.04sec 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: 1.54sec CBMC-WMM: 0.10sec CBMC-SC: 0.06sec CImpact: 95.15sec 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: 1.60sec CBMC-WMM: 0.10sec CBMC-SC: 0.06sec CImpact: 94.71sec 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: 1.53sec CBMC-WMM: 0.10sec CBMC-SC: 0.05sec CImpact: 94.85sec 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: 1.47sec CBMC-WMM: 0.07sec CBMC-SC: 0.05sec CImpact: 94.78sec 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: 1.48sec CBMC-WMM: 0.10sec CBMC-SC: 0.06sec CImpact: 94.62sec 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: 1.50sec CBMC-WMM: 0.10sec CBMC-SC: 0.05sec CImpact: 95.78sec 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: 1.50sec CBMC-WMM: 0.12sec CBMC-SC: 0.05sec CImpact: 95.75sec 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: 1.29sec CBMC-WMM: 0.11sec CBMC-SC: 0.05sec CImpact: 98.08sec 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: 1.55sec CBMC-WMM: 0.09sec CBMC-SC: 0.06sec CImpact: 96.27sec 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: 1.65sec CBMC-WMM: 0.12sec CBMC-SC: 0.05sec CImpact: 82.05sec 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: 1.57sec CBMC-WMM: 0.12sec CBMC-SC: 0.06sec CImpact: 104.04sec 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: 1.49sec CBMC-WMM: 0.12sec CBMC-SC: 0.06sec CImpact: 101.73sec 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: 16.81sec CBMC-WMM: 0.08sec CBMC-SC: 0.07sec CImpact: ERROR/TIMEOUT[8] 325.45sec Checkfence: 0.01sec ESBMC: 0.09sec Threader-monolithic: 0.14sec Threader-owicki-gries: 0.11sec Threader-rely-guarantee: 0.16sec 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: 52.63sec CBMC-WMM: 0.17sec CBMC-SC: 15.78sec 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: 7.29sec CBMC-WMM: 0.15sec CBMC-SC: 0.08sec 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: 6.50sec CBMC-WMM: 0.16sec CBMC-SC: 0.08sec 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: 6.28sec CBMC-WMM: 0.13sec CBMC-SC: 0.07sec 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: 6.50sec CBMC-WMM: 0.14sec CBMC-SC: 0.08sec 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: 6.48sec CBMC-WMM: 0.17sec CBMC-SC: 0.08sec 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: 6.53sec CBMC-WMM: 0.15sec CBMC-SC: 0.07sec 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: 6.67sec CBMC-WMM: 0.16sec CBMC-SC: 0.07sec 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: 6.05sec CBMC-WMM: 0.17sec CBMC-SC: 0.08sec 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: 6.23sec CBMC-WMM: 0.19sec CBMC-SC: 0.08sec 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: 5.98sec CBMC-WMM: 0.18sec CBMC-SC: 0.07sec 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: 6.26sec CBMC-WMM: 0.16sec CBMC-SC: 0.08sec 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: 6.15sec CBMC-WMM: 0.18sec CBMC-SC: 0.06sec 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: 21.24sec CBMC-WMM: 0.06sec CBMC-SC: 0.07sec CImpact: ERROR/TIMEOUT[8] 306.56sec Checkfence: 0.01sec ESBMC: 0.08sec Threader-monolithic: 0.14sec Threader-owicki-gries: 0.13sec Threader-rely-guarantee: 0.14sec 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: 1.75sec CBMC-WMM: 0.14sec CBMC-SC: 13.05sec 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: 5.17sec CBMC-WMM: 0.13sec CBMC-SC: 0.08sec 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: 6.44sec CBMC-WMM: 0.15sec CBMC-SC: 0.08sec 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: 5.20sec CBMC-WMM: 0.16sec CBMC-SC: 0.07sec 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: 5.11sec CBMC-WMM: 0.15sec CBMC-SC: 0.08sec 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: 5.43sec CBMC-WMM: 0.14sec CBMC-SC: 0.08sec 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: 5.09sec CBMC-WMM: 0.13sec CBMC-SC: 0.08sec 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: 5.30sec CBMC-WMM: 0.17sec CBMC-SC: 0.07sec 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: 4.99sec CBMC-WMM: 0.15sec CBMC-SC: 0.06sec 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: 4.73sec CBMC-WMM: 0.15sec CBMC-SC: 0.06sec 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: 14.19sec CBMC-WMM: 0.16sec CBMC-SC: 34.27sec CImpact: 0.02sec 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: 84.17sec CBMC-WMM: 0.18sec CBMC-SC: 3.91sec 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: 83.50sec CBMC-WMM: 0.17sec CBMC-SC: 3.56sec 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: 18.59sec CBMC-WMM: 0.07sec CBMC-SC: 0.08sec CImpact: ERROR/TIMEOUT[8] 223.51sec Checkfence: 0.01sec ESBMC: 0.09sec Threader-monolithic: 0.17sec Threader-owicki-gries: 0.16sec Threader-rely-guarantee: 0.11sec 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: 100.98sec CBMC-WMM: 0.15sec CBMC-SC: 17.32sec 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: 9.36sec CBMC-WMM: 0.13sec CBMC-SC: 0.07sec 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: 11.20sec CBMC-WMM: 0.15sec CBMC-SC: 0.09sec 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: 9.41sec CBMC-WMM: 0.15sec CBMC-SC: 0.08sec 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: 9.09sec CBMC-WMM: 0.14sec CBMC-SC: 0.07sec 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: 7.82sec CBMC-WMM: 0.14sec CBMC-SC: 0.08sec 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: 8.82sec CBMC-WMM: 0.16sec CBMC-SC: 0.08sec 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: 8.90sec CBMC-WMM: 0.17sec CBMC-SC: 0.08sec 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: 12.75sec CBMC-WMM: 0.18sec CBMC-SC: 0.08sec 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: 10.14sec CBMC-WMM: 0.21sec CBMC-SC: 0.12sec 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: 139.34sec CBMC-WMM: 0.14sec CBMC-SC: 12.71sec CImpact: 0.01sec 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: 33.13sec CBMC-WMM: 0.16sec CBMC-SC: 2.49sec 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: 33.64sec CBMC-WMM: 0.16sec CBMC-SC: 2.49sec 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: 44.30sec CBMC-WMM: 0.15sec CBMC-SC: 0.14sec CImpact: ERROR/TIMEOUT[8] 293.13sec Checkfence: 0.01sec ESBMC: 0.08sec Threader-monolithic: 0.15sec Threader-owicki-gries: 0.14sec Threader-rely-guarantee: 0.15sec 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: 2.99sec CBMC-WMM: 0.24sec CBMC-SC: 23.05sec CImpact: 0.84sec 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: 21.70sec CBMC-WMM: 0.23sec CBMC-SC: 0.12sec 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: 21.49sec CBMC-WMM: 0.23sec CBMC-SC: 0.12sec 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: 21.81sec CBMC-WMM: 0.26sec CBMC-SC: 0.12sec 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: 21.89sec CBMC-WMM: 0.22sec CBMC-SC: 0.11sec 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: 22.00sec CBMC-WMM: 0.23sec CBMC-SC: 0.09sec 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: 21.37sec CBMC-WMM: 0.23sec CBMC-SC: 0.12sec 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: 21.83sec CBMC-WMM: 0.26sec CBMC-SC: 0.12sec 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: 22.52sec CBMC-WMM: 0.28sec CBMC-SC: 0.12sec 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: 21.64sec CBMC-WMM: 0.27sec CBMC-SC: 0.10sec 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: 30.69sec CBMC-WMM: 0.22sec CBMC-SC: 65.13sec CImpact: 0.03sec 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: 3.72sec CBMC-WMM: 0.21sec CBMC-SC: 7.96sec 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: 12.36sec CBMC-WMM: 0.22sec CBMC-SC: 5.75sec CImpact: 0.02sec 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: 35.45sec CBMC-WMM: 0.18sec CBMC-SC: 0.15sec CImpact: ERROR/TIMEOUT[8] 257.98sec Checkfence: 0.01sec ESBMC: 0.09sec Threader-monolithic: 0.16sec Threader-owicki-gries: 0.16sec Threader-rely-guarantee: 0.16sec 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: 38.91sec CBMC-WMM: 0.24sec CBMC-SC: 20.53sec CImpact: 0.59sec 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: 58.17sec CBMC-WMM: 0.24sec CBMC-SC: 0.09sec 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: 57.83sec CBMC-WMM: 0.24sec CBMC-SC: 0.10sec 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: 64.15sec CBMC-WMM: 0.23sec CBMC-SC: 0.12sec 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: 57.92sec CBMC-WMM: 0.25sec CBMC-SC: 0.12sec 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: 55.66sec CBMC-WMM: 0.27sec CBMC-SC: 0.10sec 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: 59.20sec CBMC-WMM: 0.27sec CBMC-SC: 0.11sec 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: 58.21sec CBMC-WMM: 0.31sec CBMC-SC: 0.12sec 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: 62.82sec CBMC-WMM: 0.29sec CBMC-SC: 0.11sec 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: 58.63sec CBMC-WMM: 0.30sec CBMC-SC: 0.11sec 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: 206.88sec CBMC-WMM: 0.21sec CBMC-SC: 41.34sec CImpact: 0.02sec 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: 289.66sec CBMC-WMM: 0.22sec CBMC-SC: 3.76sec 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: 268.11sec CBMC-WMM: 0.23sec CBMC-SC: 3.57sec 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: 51.79sec CBMC-WMM: 0.14sec CBMC-SC: 0.15sec CImpact: ERROR/TIMEOUT[8] 360.00sec Checkfence: 0.01sec ESBMC: 0.07sec Threader-monolithic: 0.17sec Threader-owicki-gries: 0.17sec Threader-rely-guarantee: 0.17sec 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: 456.84sec CBMC-WMM: 0.23sec CBMC-SC: 30.88sec 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: 67.90sec CBMC-WMM: 0.24sec CBMC-SC: 0.13sec 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: 66.04sec CBMC-WMM: 0.25sec CBMC-SC: 0.09sec 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: 59.09sec CBMC-WMM: 0.23sec CBMC-SC: 0.12sec 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: 65.52sec CBMC-WMM: 0.24sec CBMC-SC: 0.13sec 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: 67.75sec CBMC-WMM: 0.23sec CBMC-SC: 0.11sec 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: 58.03sec CBMC-WMM: 0.22sec CBMC-SC: 0.12sec 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: 61.16sec CBMC-WMM: 0.25sec CBMC-SC: 0.14sec 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: 63.22sec CBMC-WMM: 0.27sec CBMC-SC: 0.12sec 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: 67.60sec CBMC-WMM: 0.29sec CBMC-SC: 0.11sec 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: 0.22sec CBMC-SC: 22.64sec CImpact: 0.02sec 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: 174.50sec CBMC-WMM: 0.21sec CBMC-SC: 4.45sec 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: 179.77sec CBMC-WMM: 0.21sec CBMC-SC: 4.69sec 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 |