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/lwdwr (tooling date Sun Jan 22 02:23:23 GMT 2012)
This family corresponds to litmus tests involving pairs showing that Power's lwsync barrier cannot enforce any ordering when placed between a write and a read. Therefore they should answer Yes in litmus terms, or Verification Failed in verification terms as soon as the model is Power.
Name | SC | CAV'11 | TSO (all delay/cyc) | TSO (1 delay/cyc) | TSO (opt delay/cyc) | Expected (TSO) | PSO (all delay/cyc) | PSO (1 delay/cyc) | PSO (opt delay/cyc) | Expected (PSO) | RMO (all delay/cyc) | RMO (1 delay/cyc) | RMO (opt delay/cyc) | Expected (RMO) | Power (all delay/cyc) | Power (1 delay/cyc) | Power (opt delay/cyc) | Expected (Power) |
ppc/lwdwr000 |
SatAbs: 1.98sec Satabs-prefix-first: 1.11sec CBMC-WMM: 0.10sec CBMC-SC: 0.07sec CImpact: ERROR/TIMEOUT[8] 312.61sec Checkfence: 0.01sec ESBMC: 0.08sec Threader-monolithic: 0.20sec Threader-owicki-gries: 0.16sec Threader-rely-guarantee: 0.19sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT MMChecker (MM: sc): ERROR/TIMEOUT[2] 0.00sec |
Cycles
SatAbs: 4.54sec (x2.29) Satabs-prefix-first: 7.09sec CBMC-WMM: 0.16sec CBMC-SC: 18.32sec CImpact: 1.42sec ESBMC: 0.14sec Threader-monolithic: ERROR/TIMEOUT[130] 897.14sec Threader-owicki-gries: ERROR/TIMEOUT[130] 897.37sec Threader-rely-guarantee: ERROR/TIMEOUT[130] 896.82sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT MMChecker (MM: csharp): ERROR/TIMEOUT[2] 0.00sec |
Cycles
SatAbs: 19.30sec (x9.74) Satabs-prefix-first: 12.20sec CBMC-WMM: 0.19sec CBMC-SC: 1.10sec CImpact: ERROR/TIMEOUT[8] 384.29sec Checkfence: 0.01sec ESBMC: 0.11sec Threader-monolithic: ERROR/TIMEOUT[130] 896.51sec Threader-owicki-gries: ERROR/TIMEOUT[130] 896.61sec Threader-rely-guarantee: ERROR/TIMEOUT[130] 896.96sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT MMChecker (MM: csharp): ERROR/TIMEOUT[2] 0.00sec |
Cycles
SatAbs: 21.29sec (x10.75) Satabs-prefix-first: 12.55sec CBMC-WMM: 0.18sec CBMC-SC: 1.05sec CImpact: ERROR/TIMEOUT[8] 358.96sec ESBMC: 0.11sec Threader-monolithic: ERROR/TIMEOUT[130] 892.70sec Threader-owicki-gries: ERROR/TIMEOUT[130] 895.21sec Threader-rely-guarantee: ERROR/TIMEOUT[130] 894.98sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT MMChecker (MM: csharp): ERROR/TIMEOUT[2] 0.00sec |
Cycles
SatAbs: 18.89sec (x9.54) Satabs-prefix-first: 12.86sec CBMC-WMM: 0.16sec CBMC-SC: 1.47sec CImpact: ERROR/TIMEOUT[8] 369.72sec ESBMC: 0.08sec Threader-monolithic: ERROR/TIMEOUT[130] 896.47sec Threader-owicki-gries: ERROR/TIMEOUT[130] 897.10sec Threader-rely-guarantee: ERROR/TIMEOUT[130] 896.89sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT MMChecker (MM: csharp): ERROR/TIMEOUT[2] 0.00sec |
Cycles
SatAbs: 19.58sec (x9.88) Satabs-prefix-first: 12.84sec CBMC-WMM: 0.17sec CBMC-SC: 1.02sec CImpact: ERROR/TIMEOUT[8] 372.94sec ESBMC: 0.09sec Threader-monolithic: ERROR/TIMEOUT[130] 868.16sec Threader-owicki-gries: ERROR/TIMEOUT[130] 895.82sec Threader-rely-guarantee: ERROR/TIMEOUT[130] 897.10sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT Blender: |
Cycles
SatAbs: 19.14sec (x9.66) Satabs-prefix-first: 12.01sec CBMC-WMM: 0.17sec CBMC-SC: 1.06sec CImpact: ERROR/TIMEOUT[8] 362.37sec ESBMC: 0.11sec Threader-monolithic: ERROR/TIMEOUT[130] 895.41sec Threader-owicki-gries: ERROR/TIMEOUT[130] 895.89sec Threader-rely-guarantee: ERROR/TIMEOUT[130] 896.84sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT Blender: |
Cycles
SatAbs: 18.62sec (x9.40) Satabs-prefix-first: 10.63sec CBMC-WMM: 0.17sec CBMC-SC: 0.99sec CImpact: ERROR/TIMEOUT[8] 356.18sec ESBMC: 0.10sec Threader-monolithic: ERROR/TIMEOUT[130] 894.64sec Threader-owicki-gries: ERROR/TIMEOUT[130] 897.04sec Threader-rely-guarantee: ERROR/TIMEOUT[130] 896.47sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT Blender: |
Cycles
SatAbs: 18.23sec (x9.20) Satabs-prefix-first: 11.69sec CBMC-WMM: 0.16sec CBMC-SC: 1.01sec CImpact: ERROR/TIMEOUT[8] 372.96sec ESBMC: 0.08sec Threader-monolithic: ERROR/TIMEOUT[130] 896.29sec Threader-owicki-gries: ERROR/TIMEOUT[130] 897.21sec Threader-rely-guarantee: ERROR/TIMEOUT[130] 897.51sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT |
Cycles
SatAbs: 19.04sec (x9.61) Satabs-prefix-first: 12.42sec CBMC-WMM: 0.16sec CBMC-SC: 0.90sec CImpact: ERROR/TIMEOUT[8] 284.48sec ESBMC: 0.11sec Threader-monolithic: ERROR/TIMEOUT[130] 896.56sec Threader-owicki-gries: ERROR/TIMEOUT[130] 897.31sec Threader-rely-guarantee: ERROR/TIMEOUT[130] 896.38sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT |
Cycles
SatAbs: 18.04sec (x9.11) Satabs-prefix-first: 15.40sec CBMC-WMM: 0.25sec CBMC-SC: 1.59sec CImpact: ERROR/TIMEOUT[8] 301.00sec ESBMC: 0.10sec Threader-monolithic: ERROR/TIMEOUT[130] 897.43sec Threader-owicki-gries: ERROR/TIMEOUT[130] 896.80sec Threader-rely-guarantee: ERROR/TIMEOUT[130] 897.27sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT |
Cycles
SatAbs: 18.11sec (x9.14) Satabs-prefix-first: 11.67sec CBMC-WMM: 0.19sec CBMC-SC: 1.00sec CImpact: ERROR/TIMEOUT[8] 311.91sec ESBMC: 0.10sec Threader-monolithic: ERROR/TIMEOUT[130] 897.43sec Threader-owicki-gries: ERROR/TIMEOUT[130] 897.42sec Threader-rely-guarantee: ERROR/TIMEOUT[130] 897.26sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT |
Cycles
SatAbs: 19.87sec (x10.03) Satabs-prefix-first: 13.27sec CBMC-WMM: 0.20sec CBMC-SC: 0.98sec CImpact: ERROR/TIMEOUT[8] 365.14sec ESBMC: 0.10sec Threader-monolithic: ERROR/TIMEOUT[130] 896.68sec Threader-owicki-gries: ERROR/TIMEOUT[130] 896.88sec Threader-rely-guarantee: ERROR/TIMEOUT[130] 897.31sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT |
Cycles
SatAbs: 19.83sec (x10.01) Satabs-prefix-first: 12.06sec CBMC-WMM: 0.22sec CBMC-SC: 0.94sec CImpact: ERROR/TIMEOUT[8] 384.71sec ESBMC: 0.09sec Threader-monolithic: ERROR/TIMEOUT[130] 896.83sec Threader-owicki-gries: ERROR/TIMEOUT[130] 897.27sec Threader-rely-guarantee: ERROR/TIMEOUT[130] 897.20sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT |
||||
ppc/lwdwr001 |
SatAbs: 2.09sec Satabs-prefix-first: 0.95sec CBMC-WMM: 0.10sec CBMC-SC: 0.09sec CImpact: ERROR/TIMEOUT[8] 309.40sec Checkfence: 0.01sec ESBMC: 0.08sec Threader-monolithic: 0.14sec Threader-owicki-gries: 0.16sec Threader-rely-guarantee: 0.15sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT MMChecker (MM: sc): ERROR/TIMEOUT[2] 0.00sec |
Cycles
SatAbs: 4.62sec (x2.21) Satabs-prefix-first: 6.01sec CBMC-WMM: 0.18sec CBMC-SC: 14.45sec CImpact: 1.34sec ESBMC: 0.11sec Threader-monolithic: ERROR/TIMEOUT[130] 897.24sec Threader-owicki-gries: ERROR/TIMEOUT[130] 897.31sec Threader-rely-guarantee: ERROR/TIMEOUT[130] 897.21sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT MMChecker (MM: csharp): ERROR/TIMEOUT[2] 0.00sec |
Cycles
SatAbs: 28.95sec (x13.85) Satabs-prefix-first: 10.83sec CBMC-WMM: 0.14sec CBMC-SC: 0.91sec CImpact: ERROR/TIMEOUT[8] 351.98sec Checkfence: 0.01sec ESBMC: 0.07sec Threader-monolithic: ERROR/TIMEOUT[130] 896.49sec Threader-owicki-gries: ERROR/TIMEOUT[130] 896.62sec Threader-rely-guarantee: ERROR/TIMEOUT[130] 897.25sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT MMChecker (MM: csharp): ERROR/TIMEOUT[2] 0.00sec |
Cycles
SatAbs: 26.47sec (x12.66) Satabs-prefix-first: 11.72sec CBMC-WMM: 0.19sec CBMC-SC: 0.92sec CImpact: ERROR/TIMEOUT[8] 355.09sec ESBMC: 0.09sec Threader-monolithic: ERROR/TIMEOUT[130] 897.16sec Threader-owicki-gries: ERROR/TIMEOUT[130] 897.28sec Threader-rely-guarantee: ERROR/TIMEOUT[130] 897.15sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT MMChecker (MM: csharp): ERROR/TIMEOUT[2] 0.00sec |
Cycles
SatAbs: 28.45sec (x13.61) Satabs-prefix-first: 10.39sec CBMC-WMM: 0.16sec CBMC-SC: 0.96sec CImpact: ERROR/TIMEOUT[8] 350.28sec ESBMC: 0.09sec Threader-monolithic: ERROR/TIMEOUT[130] 897.43sec Threader-owicki-gries: ERROR/TIMEOUT[130] 897.19sec Threader-rely-guarantee: ERROR/TIMEOUT[130] 897.14sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT MMChecker (MM: csharp): ERROR/TIMEOUT[2] 0.00sec |
Cycles
SatAbs: 27.50sec (x13.15) Satabs-prefix-first: 10.46sec CBMC-WMM: 0.14sec CBMC-SC: 0.86sec CImpact: ERROR/TIMEOUT[8] 347.64sec ESBMC: 0.14sec Threader-monolithic: ERROR/TIMEOUT[130] 897.20sec Threader-owicki-gries: ERROR/TIMEOUT[130] 897.41sec Threader-rely-guarantee: ERROR/TIMEOUT[130] 896.91sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT Blender: |
Cycles
SatAbs: 27.87sec (x13.33) Satabs-prefix-first: 10.73sec CBMC-WMM: 0.15sec CBMC-SC: 0.95sec CImpact: ERROR/TIMEOUT[8] 355.92sec ESBMC: 0.08sec Threader-monolithic: ERROR/TIMEOUT[130] 897.36sec Threader-owicki-gries: ERROR/TIMEOUT[130] 897.32sec Threader-rely-guarantee: ERROR/TIMEOUT[130] 897.37sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT Blender: |
Cycles
SatAbs: 28.88sec (x13.81) Satabs-prefix-first: 11.08sec CBMC-WMM: 0.17sec CBMC-SC: 0.87sec CImpact: ERROR/TIMEOUT[8] 357.39sec ESBMC: 0.09sec Threader-monolithic: ERROR/TIMEOUT[130] 897.45sec Threader-owicki-gries: ERROR/TIMEOUT[130] 897.39sec Threader-rely-guarantee: ERROR/TIMEOUT[130] 897.17sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT Blender: |
Cycles
SatAbs: 27.30sec (x13.06) Satabs-prefix-first: 10.41sec CBMC-WMM: 0.16sec CBMC-SC: 0.93sec CImpact: ERROR/TIMEOUT[8] 231.93sec ESBMC: 0.08sec Threader-monolithic: ERROR/TIMEOUT[130] 897.17sec Threader-owicki-gries: ERROR/TIMEOUT[130] 897.42sec Threader-rely-guarantee: ERROR/TIMEOUT[130] 896.75sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT |
Cycles
SatAbs: 27.67sec (x13.23) Satabs-prefix-first: 10.51sec CBMC-WMM: 0.18sec CBMC-SC: 0.89sec CImpact: ERROR/TIMEOUT[8] 309.99sec ESBMC: 0.11sec Threader-monolithic: ERROR/TIMEOUT[130] 897.31sec Threader-owicki-gries: ERROR/TIMEOUT[130] 896.89sec Threader-rely-guarantee: ERROR/TIMEOUT[130] 896.71sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT |
Cycles
SatAbs: 27.61sec (x13.21) Satabs-prefix-first: 11.39sec CBMC-WMM: 0.19sec CBMC-SC: 1.00sec CImpact: ERROR/TIMEOUT[8] 347.68sec ESBMC: 0.12sec Threader-monolithic: ERROR/TIMEOUT[130] 897.12sec Threader-owicki-gries: ERROR/TIMEOUT[130] 897.48sec Threader-rely-guarantee: ERROR/TIMEOUT[130] 897.17sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT |
Cycles
SatAbs: 42.73sec (x20.44) Satabs-prefix-first: 157.66sec CBMC-WMM: 0.18sec CBMC-SC: 28.59sec CImpact: ERROR/TIMEOUT[8] 407.60sec ESBMC: 0.12sec Threader-monolithic: ERROR/TIMEOUT[130] 897.68sec Threader-owicki-gries: ERROR/TIMEOUT[130] 897.18sec Threader-rely-guarantee: ERROR/TIMEOUT[130] 896.86sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT |
Cycles
SatAbs: 28.68sec (x13.72) Satabs-prefix-first: 10.76sec CBMC-WMM: 0.17sec CBMC-SC: 0.90sec CImpact: ERROR/TIMEOUT[8] 341.85sec ESBMC: 0.10sec Threader-monolithic: ERROR/TIMEOUT[130] 896.39sec Threader-owicki-gries: ERROR/TIMEOUT[130] 897.35sec Threader-rely-guarantee: ERROR/TIMEOUT[130] 897.29sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT |
Cycles
SatAbs: 30.45sec (x14.56) Satabs-prefix-first: 11.71sec CBMC-WMM: 0.19sec CBMC-SC: 0.90sec CImpact: ERROR/TIMEOUT[8] 363.91sec ESBMC: 0.09sec Threader-monolithic: ERROR/TIMEOUT[130] 896.60sec Threader-owicki-gries: ERROR/TIMEOUT[130] 897.32sec Threader-rely-guarantee: ERROR/TIMEOUT[130] 896.98sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT |
||||
ppc/lwdwr002 |
SatAbs: 0.42sec Satabs-prefix-first: 0.46sec CBMC-WMM: 0.05sec CBMC-SC: 0.05sec CImpact: 1.23sec Checkfence: 0.01sec ESBMC: 0.09sec Threader-monolithic: 0.11sec Threader-owicki-gries: 0.13sec Threader-rely-guarantee: 0.13sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT MMChecker (MM: sc): ERROR/TIMEOUT[2] 0.00sec |
Cycles
SatAbs: 2.35sec (x5.59) Satabs-prefix-first: 3.27sec CBMC-WMM: 0.10sec CBMC-SC: 9.37sec CImpact: 0.95sec ESBMC: 0.11sec Threader-monolithic: ERROR/TIMEOUT[130] 897.48sec Threader-owicki-gries: ERROR/TIMEOUT[130] 897.23sec Threader-rely-guarantee: ERROR/TIMEOUT[130] 897.29sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT MMChecker (MM: csharp): ERROR/TIMEOUT[2] 0.00sec |
Cycles
SatAbs: 4.62sec (x11.00) Satabs-prefix-first: 4.35sec CBMC-WMM: 0.09sec CBMC-SC: 0.62sec CImpact: 36.87sec Checkfence: 0.01sec ESBMC: 0.09sec Threader-monolithic: ERROR/TIMEOUT[130] 897.25sec Threader-owicki-gries: ERROR/TIMEOUT[130] 897.34sec Threader-rely-guarantee: ERROR/TIMEOUT[130] 897.14sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT MMChecker (MM: csharp): ERROR/TIMEOUT[2] 0.00sec |
Cycles
SatAbs: 5.55sec (x13.21) Satabs-prefix-first: 4.62sec CBMC-WMM: 0.10sec CBMC-SC: 0.61sec CImpact: 34.73sec ESBMC: 0.10sec Threader-monolithic: ERROR/TIMEOUT[130] 897.30sec Threader-owicki-gries: ERROR/TIMEOUT[130] 897.37sec Threader-rely-guarantee: ERROR/TIMEOUT[130] 897.31sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT MMChecker (MM: csharp): ERROR/TIMEOUT[2] 0.00sec |
Cycles
SatAbs: 4.73sec (x11.26) Satabs-prefix-first: 4.61sec CBMC-WMM: 0.10sec CBMC-SC: 0.60sec CImpact: 39.41sec ESBMC: 0.10sec Threader-monolithic: ERROR/TIMEOUT[130] 897.27sec Threader-owicki-gries: ERROR/TIMEOUT[130] 897.20sec Threader-rely-guarantee: ERROR/TIMEOUT[130] 897.32sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT MMChecker (MM: csharp): ERROR/TIMEOUT[2] 0.00sec |
Cycles
SatAbs: 4.58sec (x10.90) Satabs-prefix-first: 4.52sec CBMC-WMM: 0.11sec CBMC-SC: 0.62sec CImpact: 36.74sec ESBMC: 0.08sec Threader-monolithic: ERROR/TIMEOUT[130] 897.46sec Threader-owicki-gries: ERROR/TIMEOUT[130] 897.51sec Threader-rely-guarantee: ERROR/TIMEOUT[130] 897.44sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT Blender: |
Cycles
SatAbs: 4.41sec (x10.50) Satabs-prefix-first: 4.31sec CBMC-WMM: 0.11sec CBMC-SC: 0.64sec CImpact: 35.77sec ESBMC: 0.09sec Threader-monolithic: ERROR/TIMEOUT[130] 896.84sec Threader-owicki-gries: ERROR/TIMEOUT[130] 897.28sec Threader-rely-guarantee: ERROR/TIMEOUT[130] 896.86sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT Blender: |
Cycles
SatAbs: 4.89sec (x11.64) Satabs-prefix-first: 4.71sec CBMC-WMM: 0.09sec CBMC-SC: 0.80sec CImpact: 37.73sec ESBMC: 0.07sec Threader-monolithic: ERROR/TIMEOUT[130] 897.38sec Threader-owicki-gries: ERROR/TIMEOUT[130] 897.24sec Threader-rely-guarantee: ERROR/TIMEOUT[130] 897.18sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT Blender: |
Cycles
SatAbs: 4.44sec (x10.57) Satabs-prefix-first: 5.25sec CBMC-WMM: 0.12sec CBMC-SC: 0.62sec CImpact: 37.36sec ESBMC: 0.09sec Threader-monolithic: ERROR/TIMEOUT[130] 897.03sec Threader-owicki-gries: ERROR/TIMEOUT[130] 897.11sec Threader-rely-guarantee: ERROR/TIMEOUT[130] 897.40sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT |
Cycles
SatAbs: 4.46sec (x10.61) Satabs-prefix-first: 6.13sec CBMC-WMM: 0.12sec CBMC-SC: 0.72sec CImpact: 36.40sec ESBMC: 0.10sec Threader-monolithic: ERROR/TIMEOUT[130] 897.19sec Threader-owicki-gries: ERROR/TIMEOUT[130] 896.96sec Threader-rely-guarantee: ERROR/TIMEOUT[130] 897.31sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT |
Cycles
SatAbs: 4.55sec (x10.83) Satabs-prefix-first: 4.22sec CBMC-WMM: 0.10sec CBMC-SC: 0.61sec CImpact: 37.10sec ESBMC: 0.08sec Threader-monolithic: ERROR/TIMEOUT[130] 897.28sec Threader-owicki-gries: ERROR/TIMEOUT[130] 897.42sec Threader-rely-guarantee: ERROR/TIMEOUT[130] 896.88sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT |
Cycles
SatAbs: 4.58sec (x10.90) Satabs-prefix-first: 4.24sec CBMC-WMM: 0.10sec CBMC-SC: 0.75sec CImpact: 36.51sec ESBMC: 0.10sec Threader-monolithic: ERROR/TIMEOUT[130] 897.16sec Threader-owicki-gries: ERROR/TIMEOUT[130] 897.38sec Threader-rely-guarantee: ERROR/TIMEOUT[130] 897.14sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT |
Cycles
SatAbs: 4.25sec (x10.11) Satabs-prefix-first: 4.05sec CBMC-WMM: 0.11sec CBMC-SC: 0.57sec CImpact: 36.87sec ESBMC: 0.09sec Threader-monolithic: ERROR/TIMEOUT[130] 897.15sec Threader-owicki-gries: ERROR/TIMEOUT[130] 897.31sec Threader-rely-guarantee: ERROR/TIMEOUT[130] 897.24sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT |
Cycles
SatAbs: 4.39sec (x10.45) Satabs-prefix-first: 4.26sec CBMC-WMM: 0.11sec CBMC-SC: 0.59sec CImpact: 36.52sec ESBMC: 0.10sec Threader-monolithic: ERROR/TIMEOUT[130] 897.17sec Threader-owicki-gries: ERROR/TIMEOUT[130] 896.58sec Threader-rely-guarantee: ERROR/TIMEOUT[130] 897.46sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT |
||||
ppc/lwdwr003 |
SatAbs: 2.67sec Satabs-prefix-first: 1.10sec CBMC-WMM: 0.10sec CBMC-SC: 0.09sec CImpact: ERROR/TIMEOUT[8] 248.61sec Checkfence: 0.01sec ESBMC: 0.08sec Threader-monolithic: 0.13sec 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: 14.15sec (x5.29) Satabs-prefix-first: 15.67sec CBMC-WMM: 0.18sec CBMC-SC: 15.05sec CImpact: 1.14sec ESBMC: 0.10sec Threader-monolithic: ERROR/TIMEOUT[130] 897.40sec Threader-owicki-gries: ERROR/TIMEOUT[130] 896.80sec Threader-rely-guarantee: ERROR/TIMEOUT[130] 897.31sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT MMChecker (MM: csharp): ERROR/TIMEOUT[2] 0.00sec |
Cycles
SatAbs: 26.86sec (x10.05) Satabs-prefix-first: 38.34sec CBMC-WMM: 0.16sec CBMC-SC: 12.69sec CImpact: ERROR/TIMEOUT[8] 394.49sec Checkfence: 0.00sec ESBMC: 0.12sec Threader-monolithic: ERROR/TIMEOUT[130] 897.57sec Threader-owicki-gries: ERROR/TIMEOUT[130] 897.43sec Threader-rely-guarantee: ERROR/TIMEOUT[130] 897.02sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT MMChecker (MM: csharp): ERROR/TIMEOUT[2] 0.00sec |
Cycles
SatAbs: 21.52sec (x8.05) Satabs-prefix-first: 12.63sec CBMC-WMM: 0.16sec CBMC-SC: 1.54sec CImpact: ERROR/TIMEOUT[8] 350.29sec ESBMC: 0.09sec Threader-monolithic: ERROR/TIMEOUT[1] 265.30sec Threader-owicki-gries: ERROR/TIMEOUT[1] 261.60sec Threader-rely-guarantee: ERROR/TIMEOUT[1] 230.26sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT MMChecker (MM: csharp): ERROR/TIMEOUT[2] 0.01sec |
Cycles
SatAbs: 13.46sec (x5.04) Satabs-prefix-first: 20.99sec CBMC-WMM: 0.16sec CBMC-SC: 0.65sec CImpact: ERROR/TIMEOUT[8] 295.06sec ESBMC: 0.08sec Threader-monolithic: ERROR/TIMEOUT[130] 897.41sec Threader-owicki-gries: ERROR/TIMEOUT[130] 897.42sec Threader-rely-guarantee: ERROR/TIMEOUT[130] 895.59sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT MMChecker (MM: csharp): ERROR/TIMEOUT[2] 0.00sec |
Cycles
SatAbs: 26.33sec (x9.86) Satabs-prefix-first: 31.40sec CBMC-WMM: 0.15sec CBMC-SC: 12.20sec CImpact: ERROR/TIMEOUT[8] 288.49sec ESBMC: 0.10sec Threader-monolithic: ERROR/TIMEOUT[130] 897.51sec Threader-owicki-gries: ERROR/TIMEOUT[130] 897.29sec Threader-rely-guarantee: ERROR/TIMEOUT[130] 897.29sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT Blender: |
Cycles
SatAbs: 25.70sec (x9.62) Satabs-prefix-first: 15.27sec CBMC-WMM: 0.17sec CBMC-SC: 1.98sec CImpact: ERROR/TIMEOUT[8] 371.52sec ESBMC: 0.11sec Threader-monolithic: ERROR/TIMEOUT[1] 263.20sec Threader-owicki-gries: ERROR/TIMEOUT[1] 175.98sec Threader-rely-guarantee: ERROR/TIMEOUT[1] 230.08sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT Blender: |
Cycles
SatAbs: 14.99sec (x5.61) Satabs-prefix-first: 21.61sec CBMC-WMM: 0.16sec CBMC-SC: 0.68sec CImpact: ERROR/TIMEOUT[8] 337.02sec ESBMC: 0.10sec Threader-monolithic: ERROR/TIMEOUT[130] 897.06sec Threader-owicki-gries: ERROR/TIMEOUT[130] 896.15sec Threader-rely-guarantee: ERROR/TIMEOUT[130] 897.31sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT Blender: |
Cycles
SatAbs: 26.82sec (x10.04) Satabs-prefix-first: 34.18sec CBMC-WMM: 0.17sec CBMC-SC: 12.73sec CImpact: ERROR/TIMEOUT[8] 302.85sec ESBMC: 0.09sec Threader-monolithic: ERROR/TIMEOUT[130] 896.82sec Threader-owicki-gries: ERROR/TIMEOUT[130] 896.94sec Threader-rely-guarantee: ERROR/TIMEOUT[130] 897.30sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT |
Cycles
SatAbs: 28.24sec (x10.57) Satabs-prefix-first: 16.59sec CBMC-WMM: 0.19sec CBMC-SC: 1.87sec CImpact: ERROR/TIMEOUT[8] 354.23sec ESBMC: 0.09sec Threader-monolithic: ERROR/TIMEOUT[1] 222.42sec Threader-owicki-gries: ERROR/TIMEOUT[1] 222.40sec Threader-rely-guarantee: ERROR/TIMEOUT[1] 230.53sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT |
Cycles
SatAbs: 15.97sec (x5.98) Satabs-prefix-first: 23.95sec CBMC-WMM: 0.18sec CBMC-SC: 0.71sec CImpact: ERROR/TIMEOUT[8] 342.78sec ESBMC: 0.09sec Threader-monolithic: ERROR/TIMEOUT[130] 896.54sec Threader-owicki-gries: ERROR/TIMEOUT[130] 896.83sec Threader-rely-guarantee: ERROR/TIMEOUT[130] 897.26sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT |
Cycles
SatAbs: 28.76sec (x10.77) Satabs-prefix-first: 37.14sec CBMC-WMM: 0.20sec CBMC-SC: 12.77sec CImpact: ERROR/TIMEOUT[8] 333.58sec ESBMC: 0.12sec Threader-monolithic: ERROR/TIMEOUT[130] 897.42sec Threader-owicki-gries: ERROR/TIMEOUT[130] 897.51sec Threader-rely-guarantee: ERROR/TIMEOUT[130] 897.56sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT |
Cycles
SatAbs: 22.54sec (x8.44) Satabs-prefix-first: 13.56sec CBMC-WMM: 0.16sec CBMC-SC: 1.63sec CImpact: ERROR/TIMEOUT[8] 352.77sec ESBMC: 0.13sec Threader-monolithic: ERROR/TIMEOUT[1] 259.01sec Threader-owicki-gries: ERROR/TIMEOUT[1] 197.52sec Threader-rely-guarantee: ERROR/TIMEOUT[1] 246.56sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT |
Cycles
SatAbs: 15.31sec (x5.73) Satabs-prefix-first: 22.50sec CBMC-WMM: 0.17sec CBMC-SC: 0.72sec CImpact: ERROR/TIMEOUT[8] 295.67sec ESBMC: 0.10sec Threader-monolithic: ERROR/TIMEOUT[130] 897.30sec Threader-owicki-gries: ERROR/TIMEOUT[130] 897.41sec Threader-rely-guarantee: ERROR/TIMEOUT[130] 897.14sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT |
||||
ppc/lwdwr004 |
SatAbs: 3.39sec Satabs-prefix-first: 1.19sec CBMC-WMM: 0.10sec CBMC-SC: 0.09sec CImpact: ERROR/TIMEOUT[8] 305.46sec Checkfence: 0.01sec ESBMC: 0.08sec Threader-monolithic: 0.15sec Threader-owicki-gries: 0.13sec Threader-rely-guarantee: 0.15sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT MMChecker (MM: sc): ERROR/TIMEOUT[2] 0.00sec |
Cycles
SatAbs: 16.00sec (x4.71) Satabs-prefix-first: 19.41sec CBMC-WMM: 0.16sec CBMC-SC: 37.48sec CImpact: 1.10sec ESBMC: 0.13sec Threader-monolithic: ERROR/TIMEOUT[130] 897.44sec Threader-owicki-gries: ERROR/TIMEOUT[130] 897.54sec Threader-rely-guarantee: ERROR/TIMEOUT[130] 897.19sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT MMChecker (MM: csharp): ERROR/TIMEOUT[2] 0.00sec |
Cycles
SatAbs: 34.36sec (x10.13) Satabs-prefix-first: 15.17sec CBMC-WMM: 0.17sec CBMC-SC: 0.66sec CImpact: ERROR/TIMEOUT[8] 331.04sec Checkfence: 0.01sec ESBMC: 0.07sec Threader-monolithic: ERROR/TIMEOUT[130] 897.44sec Threader-owicki-gries: ERROR/TIMEOUT[130] 897.13sec Threader-rely-guarantee: ERROR/TIMEOUT[130] 897.26sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT MMChecker (MM: csharp): ERROR/TIMEOUT[2] 0.00sec |
Cycles
SatAbs: 29.17sec (x8.60) Satabs-prefix-first: 14.44sec CBMC-WMM: 0.15sec CBMC-SC: 0.63sec CImpact: ERROR/TIMEOUT[8] 317.34sec ESBMC: 0.09sec Threader-monolithic: ERROR/TIMEOUT[130] 897.29sec Threader-owicki-gries: ERROR/TIMEOUT[130] 897.05sec Threader-rely-guarantee: ERROR/TIMEOUT[130] 897.01sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT MMChecker (MM: csharp): ERROR/TIMEOUT[2] 0.00sec |
Cycles
SatAbs: 29.43sec (x8.68) Satabs-prefix-first: 13.64sec CBMC-WMM: 0.15sec CBMC-SC: 0.66sec CImpact: ERROR/TIMEOUT[8] 324.61sec ESBMC: 0.10sec Threader-monolithic: ERROR/TIMEOUT[130] 897.44sec Threader-owicki-gries: ERROR/TIMEOUT[130] 897.41sec Threader-rely-guarantee: ERROR/TIMEOUT[130] 897.40sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT MMChecker (MM: csharp): ERROR/TIMEOUT[2] 0.00sec |
Cycles
SatAbs: 30.07sec (x8.87) Satabs-prefix-first: 14.96sec CBMC-WMM: 0.18sec CBMC-SC: 0.64sec CImpact: ERROR/TIMEOUT[8] 295.45sec ESBMC: 0.10sec Threader-monolithic: ERROR/TIMEOUT[130] 897.29sec Threader-owicki-gries: ERROR/TIMEOUT[130] 897.27sec Threader-rely-guarantee: ERROR/TIMEOUT[130] 889.92sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT Blender: |
Cycles
SatAbs: 32.76sec (x9.66) Satabs-prefix-first: 17.64sec CBMC-WMM: 0.26sec CBMC-SC: 0.46sec CImpact: ERROR/TIMEOUT[8] 352.80sec ESBMC: 0.11sec Threader-monolithic: ERROR/TIMEOUT[130] 896.77sec Threader-owicki-gries: ERROR/TIMEOUT[130] 897.39sec Threader-rely-guarantee: ERROR/TIMEOUT[130] 897.36sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT Blender: |
Cycles
SatAbs: 30.91sec (x9.11) Satabs-prefix-first: 14.60sec CBMC-WMM: 0.16sec CBMC-SC: 0.61sec CImpact: ERROR/TIMEOUT[8] 248.24sec ESBMC: 0.08sec Threader-monolithic: ERROR/TIMEOUT[130] 897.35sec Threader-owicki-gries: ERROR/TIMEOUT[130] 897.31sec Threader-rely-guarantee: ERROR/TIMEOUT[130] 897.16sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT Blender: |
Cycles
SatAbs: 29.41sec (x8.67) Satabs-prefix-first: 13.59sec CBMC-WMM: 0.17sec CBMC-SC: 0.61sec CImpact: ERROR/TIMEOUT[8] 336.21sec ESBMC: 0.10sec Threader-monolithic: ERROR/TIMEOUT[130] 897.50sec Threader-owicki-gries: ERROR/TIMEOUT[130] 897.00sec Threader-rely-guarantee: ERROR/TIMEOUT[130] 897.02sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT |
Cycles
SatAbs: 28.82sec (x8.50) Satabs-prefix-first: 13.61sec CBMC-WMM: 0.18sec CBMC-SC: 0.66sec CImpact: ERROR/TIMEOUT[8] 286.55sec ESBMC: 0.11sec Threader-monolithic: ERROR/TIMEOUT[130] 897.13sec Threader-owicki-gries: ERROR/TIMEOUT[130] 897.28sec Threader-rely-guarantee: ERROR/TIMEOUT[130] 897.42sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT |
Cycles
SatAbs: 32.89sec (x9.70) Satabs-prefix-first: 14.87sec CBMC-WMM: 0.16sec CBMC-SC: 0.63sec CImpact: ERROR/TIMEOUT[8] 313.90sec ESBMC: 0.07sec Threader-monolithic: ERROR/TIMEOUT[130] 897.45sec Threader-owicki-gries: ERROR/TIMEOUT[130] 897.45sec Threader-rely-guarantee: ERROR/TIMEOUT[130] 897.44sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT |
Cycles
SatAbs: 29.59sec (x8.72) Satabs-prefix-first: 13.85sec CBMC-WMM: 0.16sec CBMC-SC: 0.63sec CImpact: ERROR/TIMEOUT[8] 339.05sec ESBMC: 0.09sec Threader-monolithic: ERROR/TIMEOUT[130] 897.35sec Threader-owicki-gries: ERROR/TIMEOUT[130] 897.33sec Threader-rely-guarantee: ERROR/TIMEOUT[130] 897.41sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT |
Cycles
SatAbs: 29.60sec (x8.73) Satabs-prefix-first: 13.85sec CBMC-WMM: 0.19sec CBMC-SC: 0.66sec CImpact: ERROR/TIMEOUT[8] 354.56sec ESBMC: 0.09sec Threader-monolithic: ERROR/TIMEOUT[130] 897.38sec Threader-owicki-gries: ERROR/TIMEOUT[130] 896.80sec Threader-rely-guarantee: ERROR/TIMEOUT[130] 897.01sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT |
Cycles
SatAbs: 29.85sec (x8.80) Satabs-prefix-first: 13.64sec CBMC-WMM: 0.16sec CBMC-SC: 0.61sec CImpact: ERROR/TIMEOUT[8] 337.76sec ESBMC: 0.10sec Threader-monolithic: ERROR/TIMEOUT[130] 897.42sec Threader-owicki-gries: ERROR/TIMEOUT[130] 897.44sec Threader-rely-guarantee: ERROR/TIMEOUT[130] 897.22sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT |
||||
ppc/lwdwr005 |
SatAbs: 1.30sec Satabs-prefix-first: 1.72sec CBMC-WMM: 0.10sec CBMC-SC: 0.10sec CImpact: ERROR/TIMEOUT[8] 307.06sec Checkfence: 0.01sec ESBMC: 0.10sec Threader-monolithic: 0.15sec Threader-owicki-gries: 0.15sec Threader-rely-guarantee: 0.15sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT MMChecker (MM: sc): ERROR/TIMEOUT[2] 0.00sec |
Cycles
SatAbs: 4.65sec (x3.57) Satabs-prefix-first: 8.06sec CBMC-WMM: 0.18sec CBMC-SC: 144.12sec CImpact: 1.17sec ESBMC: 0.13sec Threader-monolithic: ERROR/TIMEOUT[130] 897.58sec Threader-owicki-gries: ERROR/TIMEOUT[130] 897.06sec Threader-rely-guarantee: ERROR/TIMEOUT[130] 897.17sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT MMChecker (MM: csharp): ERROR/TIMEOUT[2] 0.00sec |
Cycles
SatAbs: 10.89sec (x8.37) Satabs-prefix-first: 29.33sec CBMC-WMM: 0.17sec CBMC-SC: 0.87sec CImpact: ERROR/TIMEOUT[8] 347.12sec Checkfence: 0.01sec ESBMC: 0.08sec Threader-monolithic: ERROR/TIMEOUT[130] 897.02sec Threader-owicki-gries: ERROR/TIMEOUT[130] 895.40sec Threader-rely-guarantee: ERROR/TIMEOUT[130] 897.04sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT MMChecker (MM: csharp): ERROR/TIMEOUT[2] 0.00sec |
Cycles
SatAbs: 10.78sec (x8.29) Satabs-prefix-first: 30.10sec CBMC-WMM: 0.18sec CBMC-SC: 0.90sec CImpact: ERROR/TIMEOUT[8] 294.64sec ESBMC: 0.09sec Threader-monolithic: ERROR/TIMEOUT[130] 897.32sec Threader-owicki-gries: ERROR/TIMEOUT[130] 897.42sec Threader-rely-guarantee: ERROR/TIMEOUT[130] 897.26sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT MMChecker (MM: csharp): ERROR/TIMEOUT[2] 0.00sec |
Cycles
SatAbs: 10.36sec (x7.96) Satabs-prefix-first: 27.33sec CBMC-WMM: 0.16sec CBMC-SC: 0.83sec CImpact: ERROR/TIMEOUT[8] 236.37sec ESBMC: 0.10sec Threader-monolithic: ERROR/TIMEOUT[130] 897.49sec Threader-owicki-gries: ERROR/TIMEOUT[130] 896.81sec Threader-rely-guarantee: ERROR/TIMEOUT[130] 897.02sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT MMChecker (MM: csharp): ERROR/TIMEOUT[2] 0.00sec |
Cycles
SatAbs: 10.89sec (x8.37) Satabs-prefix-first: 27.69sec CBMC-WMM: 0.17sec CBMC-SC: 0.91sec CImpact: ERROR/TIMEOUT[8] 311.70sec ESBMC: 0.11sec Threader-monolithic: ERROR/TIMEOUT[130] 897.26sec Threader-owicki-gries: ERROR/TIMEOUT[130] 897.39sec Threader-rely-guarantee: ERROR/TIMEOUT[130] 897.32sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT Blender: |
Cycles
SatAbs: 11.46sec (x8.81) Satabs-prefix-first: 26.91sec CBMC-WMM: 0.12sec CBMC-SC: 0.92sec CImpact: ERROR/TIMEOUT[8] 329.64sec ESBMC: 0.10sec Threader-monolithic: ERROR/TIMEOUT[130] 897.29sec Threader-owicki-gries: ERROR/TIMEOUT[130] 897.29sec Threader-rely-guarantee: ERROR/TIMEOUT[130] 897.35sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT Blender: |
Cycles
SatAbs: 13.40sec (x10.30) Satabs-prefix-first: 32.93sec CBMC-WMM: 0.17sec CBMC-SC: 0.89sec CImpact: ERROR/TIMEOUT[8] 367.85sec ESBMC: 0.07sec Threader-monolithic: ERROR/TIMEOUT[130] 896.64sec Threader-owicki-gries: ERROR/TIMEOUT[130] 896.80sec Threader-rely-guarantee: ERROR/TIMEOUT[130] 897.38sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT Blender: |
Cycles
SatAbs: 10.86sec (x8.35) Satabs-prefix-first: 28.39sec CBMC-WMM: 0.19sec CBMC-SC: 0.90sec CImpact: ERROR/TIMEOUT[8] 291.90sec ESBMC: 0.09sec Threader-monolithic: ERROR/TIMEOUT[130] 897.31sec Threader-owicki-gries: ERROR/TIMEOUT[130] 897.03sec Threader-rely-guarantee: ERROR/TIMEOUT[130] 897.30sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT |
Cycles
SatAbs: 10.34sec (x7.95) Satabs-prefix-first: 26.02sec CBMC-WMM: 0.16sec CBMC-SC: 0.84sec CImpact: ERROR/TIMEOUT[8] 344.27sec ESBMC: 0.10sec Threader-monolithic: ERROR/TIMEOUT[130] 897.48sec Threader-owicki-gries: ERROR/TIMEOUT[130] 897.30sec Threader-rely-guarantee: ERROR/TIMEOUT[130] 897.31sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT |
Cycles
SatAbs: 9.84sec (x7.56) Satabs-prefix-first: 29.96sec CBMC-WMM: 0.18sec CBMC-SC: 1.03sec CImpact: ERROR/TIMEOUT[8] 354.65sec ESBMC: 0.08sec Threader-monolithic: ERROR/TIMEOUT[130] 897.34sec Threader-owicki-gries: ERROR/TIMEOUT[130] 897.45sec Threader-rely-guarantee: ERROR/TIMEOUT[130] 897.42sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT |
Cycles
SatAbs: 23.40sec (x18.00) Satabs-prefix-first: 58.44sec CBMC-WMM: 0.19sec CBMC-SC: 272.50sec CImpact: 1.46sec ESBMC: 0.12sec Threader-monolithic: ERROR/TIMEOUT[130] 897.67sec Threader-owicki-gries: ERROR/TIMEOUT[130] 897.56sec Threader-rely-guarantee: ERROR/TIMEOUT[130] 897.75sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT |
Cycles
SatAbs: 9.84sec (x7.56) Satabs-prefix-first: 26.66sec CBMC-WMM: 0.19sec CBMC-SC: 0.85sec CImpact: ERROR/TIMEOUT[8] 336.43sec ESBMC: 0.09sec Threader-monolithic: ERROR/TIMEOUT[130] 897.25sec Threader-owicki-gries: ERROR/TIMEOUT[130] 896.13sec Threader-rely-guarantee: ERROR/TIMEOUT[130] 897.15sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT |
Cycles
SatAbs: 11.90sec (x9.15) Satabs-prefix-first: 29.19sec CBMC-WMM: 0.19sec CBMC-SC: 0.88sec CImpact: ERROR/TIMEOUT[8] 366.10sec ESBMC: 0.08sec Threader-monolithic: ERROR/TIMEOUT[130] 897.40sec Threader-owicki-gries: ERROR/TIMEOUT[130] 897.28sec Threader-rely-guarantee: ERROR/TIMEOUT[130] 897.21sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT |
||||
ppc/lwdwr006 |
SatAbs: 2.47sec Satabs-prefix-first: 1.40sec CBMC-WMM: 0.09sec CBMC-SC: 0.08sec CImpact: ERROR/TIMEOUT[8] 275.36sec Checkfence: 0.01sec ESBMC: 0.10sec Threader-monolithic: 0.16sec 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: 3.44sec (x1.39) Satabs-prefix-first: 3.04sec CBMC-WMM: 0.17sec CBMC-SC: 37.92sec CImpact: 1.37sec ESBMC: 0.11sec Threader-monolithic: ERROR/TIMEOUT[130] 896.72sec Threader-owicki-gries: ERROR/TIMEOUT[130] 897.53sec 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: 29.90sec (x12.10) Satabs-prefix-first: 16.06sec CBMC-WMM: 0.18sec CBMC-SC: 0.78sec CImpact: ERROR/TIMEOUT[8] 342.67sec Checkfence: 0.01sec ESBMC: 0.09sec Threader-monolithic: ERROR/TIMEOUT[130] 897.24sec Threader-owicki-gries: ERROR/TIMEOUT[130] 897.26sec Threader-rely-guarantee: ERROR/TIMEOUT[130] 897.44sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT MMChecker (MM: csharp): ERROR/TIMEOUT[2] 0.00sec |
Cycles
SatAbs: 28.95sec (x11.72) Satabs-prefix-first: 10.16sec CBMC-WMM: 0.19sec CBMC-SC: 0.79sec CImpact: ERROR/TIMEOUT[8] 379.48sec ESBMC: 0.11sec Threader-monolithic: ERROR/TIMEOUT[130] 897.49sec Threader-owicki-gries: ERROR/TIMEOUT[130] 895.61sec Threader-rely-guarantee: ERROR/TIMEOUT[130] 897.30sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT MMChecker (MM: csharp): ERROR/TIMEOUT[2] 0.00sec |
Cycles
SatAbs: 31.09sec (x12.58) Satabs-prefix-first: 10.46sec CBMC-WMM: 0.17sec CBMC-SC: 0.80sec CImpact: ERROR/TIMEOUT[8] 363.82sec ESBMC: 0.11sec Threader-monolithic: ERROR/TIMEOUT[130] 896.67sec Threader-owicki-gries: ERROR/TIMEOUT[130] 897.35sec 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: 29.78sec (x12.05) Satabs-prefix-first: 11.52sec CBMC-WMM: 0.17sec CBMC-SC: 0.82sec CImpact: ERROR/TIMEOUT[8] 338.90sec ESBMC: 0.10sec Threader-monolithic: ERROR/TIMEOUT[130] 897.33sec Threader-owicki-gries: ERROR/TIMEOUT[130] 897.27sec Threader-rely-guarantee: ERROR/TIMEOUT[130] 897.31sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT Blender: |
Cycles
SatAbs: 28.30sec (x11.45) Satabs-prefix-first: 10.24sec CBMC-WMM: 0.16sec CBMC-SC: 0.73sec CImpact: ERROR/TIMEOUT[8] 363.50sec ESBMC: 0.14sec Threader-monolithic: ERROR/TIMEOUT[130] 897.20sec Threader-owicki-gries: ERROR/TIMEOUT[130] 897.27sec Threader-rely-guarantee: ERROR/TIMEOUT[130] 897.41sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT Blender: |
Cycles
SatAbs: 28.60sec (x11.57) Satabs-prefix-first: 10.84sec CBMC-WMM: 0.16sec CBMC-SC: 0.77sec CImpact: ERROR/TIMEOUT[8] 327.02sec ESBMC: 0.10sec Threader-monolithic: ERROR/TIMEOUT[130] 896.62sec Threader-owicki-gries: ERROR/TIMEOUT[130] 896.45sec Threader-rely-guarantee: ERROR/TIMEOUT[130] 897.34sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT Blender: |
Cycles
SatAbs: 29.38sec (x11.89) Satabs-prefix-first: 11.33sec CBMC-WMM: 0.18sec CBMC-SC: 0.79sec CImpact: ERROR/TIMEOUT[8] 354.12sec ESBMC: 0.08sec Threader-monolithic: ERROR/TIMEOUT[130] 897.34sec Threader-owicki-gries: ERROR/TIMEOUT[130] 897.30sec Threader-rely-guarantee: ERROR/TIMEOUT[130] 896.85sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT |
Cycles
SatAbs: 31.17sec (x12.61) Satabs-prefix-first: 11.78sec CBMC-WMM: 0.16sec CBMC-SC: 0.60sec CImpact: ERROR/TIMEOUT[8] 348.68sec ESBMC: 0.11sec Threader-monolithic: ERROR/TIMEOUT[130] 897.23sec Threader-owicki-gries: ERROR/TIMEOUT[130] 896.12sec Threader-rely-guarantee: ERROR/TIMEOUT[130] 896.12sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT |
Cycles
SatAbs: 31.82sec (x12.88) Satabs-prefix-first: 13.44sec CBMC-WMM: 0.22sec CBMC-SC: 0.58sec CImpact: ERROR/TIMEOUT[8] 374.02sec ESBMC: 0.10sec Threader-monolithic: ERROR/TIMEOUT[130] 896.84sec Threader-owicki-gries: ERROR/TIMEOUT[130] 897.00sec Threader-rely-guarantee: ERROR/TIMEOUT[130] 897.04sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT |
Cycles
SatAbs: 7.63sec (x3.08) Satabs-prefix-first: 3.03sec CBMC-WMM: 0.21sec CBMC-SC: 4.43sec CImpact: 0.67sec ESBMC: 0.09sec Threader-monolithic: ERROR/TIMEOUT[130] 895.92sec Threader-owicki-gries: ERROR/TIMEOUT[130] 897.30sec Threader-rely-guarantee: ERROR/TIMEOUT[130] 896.87sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT |
Cycles
SatAbs: 28.66sec (x11.60) Satabs-prefix-first: 11.29sec CBMC-WMM: 0.19sec CBMC-SC: 0.86sec CImpact: ERROR/TIMEOUT[8] 361.54sec ESBMC: 0.11sec Threader-monolithic: ERROR/TIMEOUT[130] 896.61sec Threader-owicki-gries: ERROR/TIMEOUT[130] 897.39sec Threader-rely-guarantee: ERROR/TIMEOUT[130] 896.98sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT |
Cycles
SatAbs: 30.42sec (x12.31) Satabs-prefix-first: 12.02sec CBMC-WMM: 0.18sec CBMC-SC: 0.82sec CImpact: ERROR/TIMEOUT[8] 271.72sec ESBMC: 0.10sec Threader-monolithic: ERROR/TIMEOUT[130] 897.02sec Threader-owicki-gries: ERROR/TIMEOUT[130] 897.17sec Threader-rely-guarantee: ERROR/TIMEOUT[130] 897.48sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT |
||||
ppc/lwdwr007 |
SatAbs: 2.70sec Satabs-prefix-first: 1.13sec CBMC-WMM: 0.08sec CBMC-SC: 0.07sec CImpact: ERROR/TIMEOUT[8] 312.50sec Checkfence: 0.01sec ESBMC: 0.08sec Threader-monolithic: 0.16sec Threader-owicki-gries: 0.13sec Threader-rely-guarantee: 0.16sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT MMChecker (MM: sc): ERROR/TIMEOUT[2] 0.00sec |
Cycles
SatAbs: 2.95sec (x1.09) Satabs-prefix-first: 2.78sec CBMC-WMM: 0.16sec CBMC-SC: 23.32sec CImpact: 1.17sec ESBMC: 0.09sec Threader-monolithic: ERROR/TIMEOUT[130] 897.45sec Threader-owicki-gries: ERROR/TIMEOUT[130] 897.52sec Threader-rely-guarantee: ERROR/TIMEOUT[130] 897.26sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT MMChecker (MM: csharp): ERROR/TIMEOUT[2] 0.00sec |
Cycles
SatAbs: 23.91sec (x8.85) Satabs-prefix-first: 11.11sec CBMC-WMM: 0.18sec CBMC-SC: 0.81sec CImpact: ERROR/TIMEOUT[8] 271.57sec Checkfence: 0.01sec ESBMC: 0.09sec Threader-monolithic: ERROR/TIMEOUT[130] 897.41sec Threader-owicki-gries: ERROR/TIMEOUT[130] 897.03sec Threader-rely-guarantee: ERROR/TIMEOUT[130] 897.04sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT MMChecker (MM: csharp): ERROR/TIMEOUT[2] 0.00sec |
Cycles
SatAbs: 24.76sec (x9.17) Satabs-prefix-first: 10.24sec CBMC-WMM: 0.15sec CBMC-SC: 0.84sec CImpact: ERROR/TIMEOUT[8] 348.93sec ESBMC: 0.06sec Threader-monolithic: ERROR/TIMEOUT[130] 897.14sec Threader-owicki-gries: ERROR/TIMEOUT[130] 897.48sec Threader-rely-guarantee: ERROR/TIMEOUT[130] 897.15sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT MMChecker (MM: csharp): ERROR/TIMEOUT[2] 0.00sec |
Cycles
SatAbs: 23.52sec (x8.71) Satabs-prefix-first: 10.69sec CBMC-WMM: 0.19sec CBMC-SC: 0.84sec CImpact: ERROR/TIMEOUT[8] 325.63sec ESBMC: 0.11sec Threader-monolithic: ERROR/TIMEOUT[130] 897.27sec Threader-owicki-gries: ERROR/TIMEOUT[130] 896.88sec Threader-rely-guarantee: ERROR/TIMEOUT[130] 897.08sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT MMChecker (MM: csharp): ERROR/TIMEOUT[2] 0.00sec |
Cycles
SatAbs: 25.04sec (x9.27) Satabs-prefix-first: 11.50sec CBMC-WMM: 0.18sec CBMC-SC: 0.84sec CImpact: ERROR/TIMEOUT[8] 236.53sec ESBMC: 0.09sec Threader-monolithic: ERROR/TIMEOUT[130] 897.40sec Threader-owicki-gries: ERROR/TIMEOUT[130] 897.23sec Threader-rely-guarantee: ERROR/TIMEOUT[130] 896.79sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT Blender: |
Cycles
SatAbs: 23.47sec (x8.69) Satabs-prefix-first: 11.53sec CBMC-WMM: 0.19sec CBMC-SC: 0.85sec CImpact: ERROR/TIMEOUT[8] 305.62sec ESBMC: 0.09sec Threader-monolithic: ERROR/TIMEOUT[130] 897.09sec Threader-owicki-gries: ERROR/TIMEOUT[130] 895.65sec Threader-rely-guarantee: ERROR/TIMEOUT[130] 896.37sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT Blender: |
Cycles
SatAbs: 23.62sec (x8.74) Satabs-prefix-first: 9.66sec CBMC-WMM: 0.16sec CBMC-SC: 0.82sec CImpact: ERROR/TIMEOUT[8] 288.78sec ESBMC: 0.08sec Threader-monolithic: ERROR/TIMEOUT[130] 897.04sec Threader-owicki-gries: ERROR/TIMEOUT[130] 896.64sec Threader-rely-guarantee: ERROR/TIMEOUT[130] 896.00sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT Blender: |
Cycles
SatAbs: 30.09sec (x11.14) Satabs-prefix-first: 14.59sec CBMC-WMM: 0.16sec CBMC-SC: 0.69sec CImpact: ERROR/TIMEOUT[8] 356.65sec ESBMC: 0.10sec Threader-monolithic: ERROR/TIMEOUT[130] 897.11sec Threader-owicki-gries: ERROR/TIMEOUT[130] 897.13sec Threader-rely-guarantee: ERROR/TIMEOUT[130] 897.34sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT |
Cycles
SatAbs: 24.39sec (x9.03) Satabs-prefix-first: 10.78sec CBMC-WMM: 0.19sec CBMC-SC: 0.84sec CImpact: ERROR/TIMEOUT[8] 301.10sec ESBMC: 0.11sec Threader-monolithic: ERROR/TIMEOUT[130] 897.31sec Threader-owicki-gries: ERROR/TIMEOUT[130] 897.14sec Threader-rely-guarantee: ERROR/TIMEOUT[130] 897.50sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT |
Cycles
SatAbs: 29.10sec (x10.77) Satabs-prefix-first: 14.17sec CBMC-WMM: 0.20sec CBMC-SC: 0.83sec CImpact: ERROR/TIMEOUT[8] 348.32sec ESBMC: 0.08sec Threader-monolithic: ERROR/TIMEOUT[130] 897.28sec Threader-owicki-gries: ERROR/TIMEOUT[130] 897.46sec Threader-rely-guarantee: ERROR/TIMEOUT[130] 897.40sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT |
Cycles
SatAbs: 15.49sec (x5.73) Satabs-prefix-first: 8.79sec CBMC-WMM: 0.17sec CBMC-SC: 21.23sec CImpact: 1.06sec ESBMC: 0.11sec Threader-monolithic: ERROR/TIMEOUT[130] 897.66sec Threader-owicki-gries: ERROR/TIMEOUT[130] 897.66sec Threader-rely-guarantee: ERROR/TIMEOUT[130] 897.70sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT |
Cycles
SatAbs: 24.68sec (x9.14) Satabs-prefix-first: 11.47sec CBMC-WMM: 0.19sec CBMC-SC: 0.86sec CImpact: ERROR/TIMEOUT[8] 329.90sec ESBMC: 0.11sec Threader-monolithic: ERROR/TIMEOUT[130] 897.48sec Threader-owicki-gries: ERROR/TIMEOUT[130] 897.32sec Threader-rely-guarantee: ERROR/TIMEOUT[130] 897.26sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT |
Cycles
SatAbs: 26.48sec (x9.80) Satabs-prefix-first: 11.19sec CBMC-WMM: 0.22sec CBMC-SC: 1.10sec CImpact: ERROR/TIMEOUT[8] 327.12sec ESBMC: 0.11sec Threader-monolithic: ERROR/TIMEOUT[130] 897.32sec Threader-owicki-gries: ERROR/TIMEOUT[130] 897.35sec Threader-rely-guarantee: ERROR/TIMEOUT[130] 897.28sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT |
||||
ppc/lwdwr008 |
SatAbs: 0.45sec Satabs-prefix-first: 0.37sec CBMC-WMM: 0.05sec CBMC-SC: 0.04sec CImpact: 1.17sec Checkfence: 0.01sec ESBMC: 0.08sec Threader-monolithic: 0.12sec Threader-owicki-gries: 0.13sec Threader-rely-guarantee: 0.12sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT MMChecker (MM: sc): ERROR/TIMEOUT[2] 0.00sec |
Cycles
SatAbs: 1.67sec (x3.71) Satabs-prefix-first: 1.43sec CBMC-WMM: 0.11sec CBMC-SC: 6.74sec CImpact: 0.85sec ESBMC: 0.11sec Threader-monolithic: ERROR/TIMEOUT[130] 897.36sec Threader-owicki-gries: ERROR/TIMEOUT[130] 897.36sec Threader-rely-guarantee: ERROR/TIMEOUT[130] 897.25sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT MMChecker (MM: csharp): ERROR/TIMEOUT[2] 0.00sec |
Cycles
SatAbs: 4.32sec (x9.60) Satabs-prefix-first: 4.33sec CBMC-WMM: 0.09sec CBMC-SC: 0.65sec CImpact: 13.83sec Checkfence: 0.01sec ESBMC: 0.08sec Threader-monolithic: ERROR/TIMEOUT[130] 897.18sec Threader-owicki-gries: ERROR/TIMEOUT[130] 896.91sec Threader-rely-guarantee: ERROR/TIMEOUT[130] 897.35sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT MMChecker (MM: csharp): ERROR/TIMEOUT[2] 0.00sec |
Cycles
SatAbs: 4.86sec (x10.80) Satabs-prefix-first: 4.71sec CBMC-WMM: 0.10sec CBMC-SC: 0.71sec CImpact: 12.80sec ESBMC: 0.08sec Threader-monolithic: ERROR/TIMEOUT[130] 897.28sec Threader-owicki-gries: ERROR/TIMEOUT[130] 897.09sec Threader-rely-guarantee: ERROR/TIMEOUT[130] 897.30sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT MMChecker (MM: csharp): ERROR/TIMEOUT[2] 0.00sec |
Cycles
SatAbs: 4.54sec (x10.08) Satabs-prefix-first: 4.34sec CBMC-WMM: 0.11sec CBMC-SC: 0.68sec CImpact: 16.19sec ESBMC: 0.11sec Threader-monolithic: ERROR/TIMEOUT[130] 897.30sec Threader-owicki-gries: ERROR/TIMEOUT[130] 897.48sec Threader-rely-guarantee: ERROR/TIMEOUT[130] 897.47sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT MMChecker (MM: csharp): ERROR/TIMEOUT[2] 0.00sec |
Cycles
SatAbs: 4.57sec (x10.15) Satabs-prefix-first: 4.65sec CBMC-WMM: 0.10sec CBMC-SC: 0.74sec CImpact: 15.82sec ESBMC: 0.07sec Threader-monolithic: ERROR/TIMEOUT[130] 897.53sec Threader-owicki-gries: ERROR/TIMEOUT[130] 897.28sec Threader-rely-guarantee: ERROR/TIMEOUT[130] 897.61sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT Blender: |
Cycles
SatAbs: 4.81sec (x10.68) Satabs-prefix-first: 4.44sec CBMC-WMM: 0.08sec CBMC-SC: 0.51sec CImpact: 9.96sec ESBMC: 0.13sec Threader-monolithic: ERROR/TIMEOUT[130] 897.13sec Threader-owicki-gries: ERROR/TIMEOUT[130] 896.93sec Threader-rely-guarantee: ERROR/TIMEOUT[130] 897.10sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT Blender: |
Cycles
SatAbs: 4.68sec (x10.40) Satabs-prefix-first: 4.45sec CBMC-WMM: 0.09sec CBMC-SC: 0.71sec CImpact: 15.17sec ESBMC: 0.10sec Threader-monolithic: ERROR/TIMEOUT[130] 897.37sec Threader-owicki-gries: ERROR/TIMEOUT[130] 896.41sec Threader-rely-guarantee: ERROR/TIMEOUT[130] 897.22sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT Blender: |
Cycles
SatAbs: 4.54sec (x10.08) Satabs-prefix-first: 4.43sec CBMC-WMM: 0.11sec CBMC-SC: 0.75sec CImpact: 13.66sec ESBMC: 0.09sec Threader-monolithic: ERROR/TIMEOUT[130] 896.28sec Threader-owicki-gries: ERROR/TIMEOUT[130] 896.86sec Threader-rely-guarantee: ERROR/TIMEOUT[130] 896.52sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT |
Cycles
SatAbs: 4.55sec (x10.11) Satabs-prefix-first: 4.86sec CBMC-WMM: 0.13sec CBMC-SC: 0.78sec CImpact: 16.42sec ESBMC: 0.06sec Threader-monolithic: ERROR/TIMEOUT[130] 895.43sec Threader-owicki-gries: ERROR/TIMEOUT[130] 895.66sec Threader-rely-guarantee: ERROR/TIMEOUT[130] 896.58sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT |
Cycles
SatAbs: 4.44sec (x9.86) Satabs-prefix-first: 4.50sec CBMC-WMM: 0.11sec CBMC-SC: 0.70sec CImpact: 13.77sec ESBMC: 0.11sec Threader-monolithic: ERROR/TIMEOUT[130] 896.51sec Threader-owicki-gries: ERROR/TIMEOUT[130] 896.84sec Threader-rely-guarantee: ERROR/TIMEOUT[130] 895.05sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT |
Cycles
SatAbs: 1.52sec (x3.37) Satabs-prefix-first: 1.62sec CBMC-WMM: 0.09sec CBMC-SC: 4.01sec CImpact: 0.53sec ESBMC: 0.10sec Threader-monolithic: ERROR/TIMEOUT[130] 894.90sec Threader-owicki-gries: ERROR/TIMEOUT[130] 896.86sec Threader-rely-guarantee: ERROR/TIMEOUT[130] 897.29sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT |
Cycles
SatAbs: 4.62sec (x10.26) Satabs-prefix-first: 4.62sec CBMC-WMM: 0.11sec CBMC-SC: 0.74sec CImpact: 15.61sec ESBMC: 0.11sec Threader-monolithic: ERROR/TIMEOUT[130] 895.90sec Threader-owicki-gries: ERROR/TIMEOUT[130] 896.64sec Threader-rely-guarantee: ERROR/TIMEOUT[130] 896.48sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT |
Cycles
SatAbs: 4.31sec (x9.57) Satabs-prefix-first: 4.66sec CBMC-WMM: 0.10sec CBMC-SC: 0.75sec CImpact: 15.76sec ESBMC: 0.09sec Threader-monolithic: ERROR/TIMEOUT[130] 897.24sec Threader-owicki-gries: ERROR/TIMEOUT[130] 897.14sec Threader-rely-guarantee: ERROR/TIMEOUT[130] 897.09sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT |
||||
ppc/lwdwr009 |
SatAbs: 3.00sec Satabs-prefix-first: 1.16sec CBMC-WMM: 0.11sec CBMC-SC: 0.10sec CImpact: ERROR/TIMEOUT[8] 215.87sec Checkfence: 0.01sec ESBMC: 0.09sec Threader-monolithic: 0.13sec Threader-owicki-gries: 0.13sec Threader-rely-guarantee: 0.13sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT MMChecker (MM: sc): ERROR/TIMEOUT[2] 0.00sec |
Cycles
SatAbs: 12.18sec (x4.06) Satabs-prefix-first: 9.76sec CBMC-WMM: 0.18sec CBMC-SC: 19.02sec CImpact: 0.97sec ESBMC: 0.12sec Threader-monolithic: ERROR/TIMEOUT[130] 897.28sec Threader-owicki-gries: ERROR/TIMEOUT[130] 897.08sec Threader-rely-guarantee: ERROR/TIMEOUT[130] 897.34sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT MMChecker (MM: csharp): ERROR/TIMEOUT[2] 0.02sec |
Cycles
SatAbs: 27.49sec (x9.16) Satabs-prefix-first: 23.30sec CBMC-WMM: 0.17sec CBMC-SC: 6.56sec CImpact: ERROR/TIMEOUT[8] 377.43sec Checkfence: 0.01sec ESBMC: 0.11sec Threader-monolithic: ERROR/TIMEOUT[130] 897.11sec Threader-owicki-gries: ERROR/TIMEOUT[130] 896.68sec Threader-rely-guarantee: ERROR/TIMEOUT[130] 897.26sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT MMChecker (MM: csharp): ERROR/TIMEOUT[2] 0.00sec |
Cycles
SatAbs: 29.00sec (x9.66) Satabs-prefix-first: 11.99sec CBMC-WMM: 0.18sec CBMC-SC: 1.16sec CImpact: ERROR/TIMEOUT[8] 318.05sec ESBMC: 0.11sec Threader-monolithic: ERROR/TIMEOUT[1] 265.37sec Threader-owicki-gries: ERROR/TIMEOUT[1] 220.17sec Threader-rely-guarantee: ERROR/TIMEOUT[1] 213.06sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT MMChecker (MM: csharp): ERROR/TIMEOUT[2] 0.00sec |
Cycles
SatAbs: 21.64sec (x7.21) Satabs-prefix-first: 22.67sec CBMC-WMM: 0.18sec CBMC-SC: 1.02sec CImpact: ERROR/TIMEOUT[8] 222.69sec ESBMC: 0.09sec Threader-monolithic: ERROR/TIMEOUT[130] 896.95sec Threader-owicki-gries: ERROR/TIMEOUT[130] 897.24sec Threader-rely-guarantee: ERROR/TIMEOUT[130] 896.91sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT MMChecker (MM: csharp): ERROR/TIMEOUT[2] 0.00sec |
Cycles
SatAbs: 25.28sec (x8.42) Satabs-prefix-first: 23.75sec CBMC-WMM: 0.21sec CBMC-SC: 7.81sec CImpact: ERROR/TIMEOUT[8] 276.42sec ESBMC: 0.11sec Threader-monolithic: ERROR/TIMEOUT[130] 897.36sec Threader-owicki-gries: ERROR/TIMEOUT[130] 897.26sec Threader-rely-guarantee: ERROR/TIMEOUT[130] 897.27sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT Blender: |
Cycles
SatAbs: 26.18sec (x8.72) Satabs-prefix-first: 11.55sec CBMC-WMM: 0.17sec CBMC-SC: 1.09sec CImpact: ERROR/TIMEOUT[8] 332.10sec ESBMC: 0.10sec Threader-monolithic: ERROR/TIMEOUT[1] 218.43sec Threader-owicki-gries: ERROR/TIMEOUT[1] 216.83sec Threader-rely-guarantee: ERROR/TIMEOUT[1] 217.01sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT Blender: |
Cycles
SatAbs: 20.96sec (x6.98) Satabs-prefix-first: 21.34sec CBMC-WMM: 0.18sec CBMC-SC: 0.97sec CImpact: ERROR/TIMEOUT[8] 258.77sec ESBMC: 0.09sec Threader-monolithic: ERROR/TIMEOUT[130] 896.96sec Threader-owicki-gries: ERROR/TIMEOUT[130] 897.27sec Threader-rely-guarantee: ERROR/TIMEOUT[130] 897.34sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT Blender: |
Cycles
SatAbs: 26.72sec (x8.90) Satabs-prefix-first: 23.18sec CBMC-WMM: 0.19sec CBMC-SC: 7.80sec CImpact: ERROR/TIMEOUT[8] 401.28sec ESBMC: 0.12sec Threader-monolithic: ERROR/TIMEOUT[130] 897.17sec Threader-owicki-gries: ERROR/TIMEOUT[130] 897.40sec Threader-rely-guarantee: ERROR/TIMEOUT[130] 897.09sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT |
Cycles
SatAbs: 26.26sec (x8.75) Satabs-prefix-first: 11.88sec CBMC-WMM: 0.20sec CBMC-SC: 1.21sec CImpact: ERROR/TIMEOUT[8] 323.29sec ESBMC: 0.07sec Threader-monolithic: ERROR/TIMEOUT[1] 179.36sec Threader-owicki-gries: ERROR/TIMEOUT[1] 266.98sec Threader-rely-guarantee: ERROR/TIMEOUT[1] 270.92sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT |
Cycles
SatAbs: 21.28sec (x7.09) Satabs-prefix-first: 22.23sec CBMC-WMM: 0.19sec CBMC-SC: 0.97sec CImpact: ERROR/TIMEOUT[8] 349.40sec ESBMC: 0.10sec Threader-monolithic: ERROR/TIMEOUT[130] 897.23sec Threader-owicki-gries: ERROR/TIMEOUT[130] 897.01sec Threader-rely-guarantee: ERROR/TIMEOUT[130] 896.48sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT |
Cycles
SatAbs: 7.58sec (x2.52) Satabs-prefix-first: 5.62sec CBMC-WMM: 0.19sec CBMC-SC: 7.71sec CImpact: 0.96sec ESBMC: 0.10sec Threader-monolithic: ERROR/TIMEOUT[130] 897.35sec Threader-owicki-gries: ERROR/TIMEOUT[130] 895.87sec Threader-rely-guarantee: ERROR/TIMEOUT[130] 897.31sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT |
Cycles
SatAbs: 30.87sec (x10.29) Satabs-prefix-first: 16.64sec CBMC-WMM: 0.20sec CBMC-SC: 1.52sec CImpact: ERROR/TIMEOUT[8] 319.58sec ESBMC: 0.08sec Threader-monolithic: ERROR/TIMEOUT[1] 186.52sec Threader-owicki-gries: ERROR/TIMEOUT[1] 210.08sec Threader-rely-guarantee: ERROR/TIMEOUT[1] 173.63sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT |
Cycles
SatAbs: 20.77sec (x6.92) Satabs-prefix-first: 21.55sec CBMC-WMM: 0.17sec CBMC-SC: 0.96sec CImpact: ERROR/TIMEOUT[8] 338.24sec ESBMC: 0.09sec Threader-monolithic: ERROR/TIMEOUT[130] 897.16sec Threader-owicki-gries: ERROR/TIMEOUT[130] 897.36sec Threader-rely-guarantee: ERROR/TIMEOUT[130] 895.79sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT |
||||
ppc/lwdwr010 |
SatAbs: 2.37sec Satabs-prefix-first: 0.88sec CBMC-WMM: 0.07sec CBMC-SC: 0.07sec CImpact: ERROR/TIMEOUT[8] 231.13sec Checkfence: 0.01sec ESBMC: 0.09sec Threader-monolithic: 0.14sec Threader-owicki-gries: 0.13sec Threader-rely-guarantee: 0.13sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT MMChecker (MM: sc): ERROR/TIMEOUT[2] 0.00sec |
Cycles
SatAbs: 11.45sec (x4.83) Satabs-prefix-first: 9.51sec CBMC-WMM: 0.16sec CBMC-SC: 23.04sec CImpact: 1.10sec ESBMC: 0.11sec Threader-monolithic: ERROR/TIMEOUT[130] 895.89sec Threader-owicki-gries: ERROR/TIMEOUT[130] 896.45sec Threader-rely-guarantee: ERROR/TIMEOUT[130] 897.35sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT MMChecker (MM: csharp): ERROR/TIMEOUT[2] 0.00sec |
Cycles
SatAbs: 11.64sec (x4.91) Satabs-prefix-first: 19.99sec CBMC-WMM: 0.16sec CBMC-SC: 0.65sec CImpact: ERROR/TIMEOUT[8] 293.51sec Checkfence: 0.01sec ESBMC: 0.08sec Threader-monolithic: ERROR/TIMEOUT[130] 897.42sec Threader-owicki-gries: ERROR/TIMEOUT[130] 897.28sec Threader-rely-guarantee: ERROR/TIMEOUT[130] 897.24sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT MMChecker (MM: csharp): ERROR/TIMEOUT[2] 0.00sec |
Cycles
SatAbs: 14.74sec (x6.21) Satabs-prefix-first: 22.08sec CBMC-WMM: 0.18sec CBMC-SC: 0.70sec CImpact: ERROR/TIMEOUT[8] 289.80sec ESBMC: 0.21sec Threader-monolithic: ERROR/TIMEOUT[130] 895.55sec Threader-owicki-gries: ERROR/TIMEOUT[130] 895.38sec Threader-rely-guarantee: ERROR/TIMEOUT[130] 895.98sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT MMChecker (MM: csharp): ERROR/TIMEOUT[2] 0.01sec |
Cycles
SatAbs: 17.59sec (x7.42) Satabs-prefix-first: 22.60sec CBMC-WMM: 0.17sec CBMC-SC: 0.75sec CImpact: ERROR/TIMEOUT[8] 221.82sec ESBMC: 0.08sec Threader-monolithic: ERROR/TIMEOUT[130] 897.27sec Threader-owicki-gries: ERROR/TIMEOUT[130] 897.12sec 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: 10.63sec (x4.48) Satabs-prefix-first: 15.85sec CBMC-WMM: 0.11sec CBMC-SC: 0.46sec CImpact: ERROR/TIMEOUT[8] 212.77sec ESBMC: 0.06sec Threader-monolithic: ERROR/TIMEOUT[130] 897.36sec Threader-owicki-gries: ERROR/TIMEOUT[130] 896.81sec Threader-rely-guarantee: ERROR/TIMEOUT[130] 897.06sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT Blender: |
Cycles
SatAbs: 13.33sec (x5.62) Satabs-prefix-first: 19.08sec CBMC-WMM: 0.11sec CBMC-SC: 0.45sec CImpact: ERROR/TIMEOUT[8] 220.72sec ESBMC: 0.12sec Threader-monolithic: ERROR/TIMEOUT[130] 897.32sec Threader-owicki-gries: ERROR/TIMEOUT[130] 897.36sec Threader-rely-guarantee: ERROR/TIMEOUT[130] 897.44sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT Blender: |
Cycles
SatAbs: 11.24sec (x4.74) Satabs-prefix-first: 19.70sec CBMC-WMM: 0.11sec CBMC-SC: 0.49sec CImpact: ERROR/TIMEOUT[8] 214.78sec ESBMC: 0.06sec Threader-monolithic: ERROR/TIMEOUT[130] 897.41sec Threader-owicki-gries: ERROR/TIMEOUT[130] 897.14sec Threader-rely-guarantee: ERROR/TIMEOUT[130] 897.58sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT Blender: |
Cycles
SatAbs: 10.18sec (x4.29) Satabs-prefix-first: 14.84sec CBMC-WMM: 0.11sec CBMC-SC: 0.43sec CImpact: ERROR/TIMEOUT[8] 214.87sec ESBMC: 0.04sec Threader-monolithic: ERROR/TIMEOUT[130] 897.49sec Threader-owicki-gries: ERROR/TIMEOUT[130] 897.52sec Threader-rely-guarantee: ERROR/TIMEOUT[130] 897.29sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT |
Cycles
SatAbs: 14.31sec (x6.03) Satabs-prefix-first: 19.52sec CBMC-WMM: 0.11sec CBMC-SC: 0.48sec CImpact: ERROR/TIMEOUT[8] 215.72sec ESBMC: 0.07sec Threader-monolithic: ERROR/TIMEOUT[130] 897.32sec Threader-owicki-gries: ERROR/TIMEOUT[130] 897.52sec Threader-rely-guarantee: ERROR/TIMEOUT[130] 897.42sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT |
Cycles
SatAbs: 11.70sec (x4.93) Satabs-prefix-first: 19.19sec CBMC-WMM: 0.10sec CBMC-SC: 0.54sec CImpact: ERROR/TIMEOUT[8] 213.24sec ESBMC: 0.06sec Threader-monolithic: ERROR/TIMEOUT[130] 897.49sec Threader-owicki-gries: ERROR/TIMEOUT[130] 897.44sec Threader-rely-guarantee: ERROR/TIMEOUT[130] 897.42sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT |
Cycles
SatAbs: 3.18sec (x1.34) Satabs-prefix-first: 2.29sec CBMC-WMM: 0.12sec CBMC-SC: 2.80sec CImpact: 0.41sec ESBMC: 0.07sec Threader-monolithic: ERROR/TIMEOUT[130] 897.49sec Threader-owicki-gries: ERROR/TIMEOUT[130] 896.68sec Threader-rely-guarantee: ERROR/TIMEOUT[130] 895.18sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT |
Cycles
SatAbs: 12.21sec (x5.15) Satabs-prefix-first: 16.50sec CBMC-WMM: 0.16sec CBMC-SC: 0.45sec CImpact: ERROR/TIMEOUT[8] 215.75sec ESBMC: 0.06sec Threader-monolithic: ERROR/TIMEOUT[130] 895.69sec Threader-owicki-gries: ERROR/TIMEOUT[130] 897.27sec Threader-rely-guarantee: ERROR/TIMEOUT[130] 897.04sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT |
Cycles
SatAbs: 15.12sec (x6.37) Satabs-prefix-first: 21.90sec CBMC-WMM: 0.18sec CBMC-SC: 0.70sec CImpact: ERROR/TIMEOUT[8] 256.83sec ESBMC: 0.07sec Threader-monolithic: ERROR/TIMEOUT[130] 897.27sec Threader-owicki-gries: ERROR/TIMEOUT[130] 897.11sec Threader-rely-guarantee: ERROR/TIMEOUT[130] 897.36sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT |
||||
ppc/lwdwr011 |
SatAbs: 1.24sec Satabs-prefix-first: 2.63sec CBMC-WMM: 0.10sec CBMC-SC: 0.11sec CImpact: ERROR/TIMEOUT[8] 273.48sec Checkfence: 0.01sec ESBMC: 0.10sec Threader-monolithic: 0.14sec Threader-owicki-gries: 0.15sec Threader-rely-guarantee: 0.14sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT MMChecker (MM: sc): ERROR/TIMEOUT[2] 0.00sec |
Cycles
SatAbs: 4.54sec (x3.66) Satabs-prefix-first: 8.04sec CBMC-WMM: 0.15sec CBMC-SC: 68.19sec CImpact: 1.11sec ESBMC: 0.11sec Threader-monolithic: ERROR/TIMEOUT[130] 897.34sec Threader-owicki-gries: ERROR/TIMEOUT[130] 897.16sec Threader-rely-guarantee: ERROR/TIMEOUT[130] 896.03sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT MMChecker (MM: csharp): ERROR/TIMEOUT[2] 0.00sec |
Cycles
SatAbs: 10.84sec (x8.74) Satabs-prefix-first: 27.38sec CBMC-WMM: 0.17sec CBMC-SC: 0.79sec CImpact: ERROR/TIMEOUT[8] 242.61sec Checkfence: 0.01sec ESBMC: 0.07sec Threader-monolithic: ERROR/TIMEOUT[130] 897.29sec Threader-owicki-gries: ERROR/TIMEOUT[130] 896.85sec 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: 10.26sec (x8.27) Satabs-prefix-first: 27.28sec CBMC-WMM: 0.16sec CBMC-SC: 0.87sec CImpact: ERROR/TIMEOUT[8] 216.72sec ESBMC: 0.10sec Threader-monolithic: ERROR/TIMEOUT[130] 897.35sec Threader-owicki-gries: ERROR/TIMEOUT[130] 897.57sec Threader-rely-guarantee: ERROR/TIMEOUT[130] 896.91sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT MMChecker (MM: csharp): ERROR/TIMEOUT[2] 0.01sec |
Cycles
SatAbs: 10.59sec (x8.54) Satabs-prefix-first: 27.29sec CBMC-WMM: 0.17sec CBMC-SC: 0.84sec CImpact: ERROR/TIMEOUT[8] 344.90sec ESBMC: 0.09sec Threader-monolithic: ERROR/TIMEOUT[130] 897.24sec Threader-owicki-gries: ERROR/TIMEOUT[130] 897.45sec Threader-rely-guarantee: ERROR/TIMEOUT[130] 897.23sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT MMChecker (MM: csharp): ERROR/TIMEOUT[2] 0.00sec |
Cycles
SatAbs: 10.44sec (x8.41) Satabs-prefix-first: 27.17sec CBMC-WMM: 0.18sec CBMC-SC: 0.82sec CImpact: ERROR/TIMEOUT[8] 239.56sec ESBMC: 0.09sec Threader-monolithic: ERROR/TIMEOUT[130] 897.26sec Threader-owicki-gries: ERROR/TIMEOUT[130] 897.25sec Threader-rely-guarantee: ERROR/TIMEOUT[130] 896.77sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT Blender: |
Cycles
SatAbs: 10.26sec (x8.27) Satabs-prefix-first: 27.81sec CBMC-WMM: 0.16sec CBMC-SC: 0.91sec CImpact: ERROR/TIMEOUT[8] 306.55sec ESBMC: 0.06sec Threader-monolithic: ERROR/TIMEOUT[130] 897.46sec Threader-owicki-gries: ERROR/TIMEOUT[130] 896.15sec Threader-rely-guarantee: ERROR/TIMEOUT[130] 897.39sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT Blender: |
Cycles
SatAbs: 9.74sec (x7.85) Satabs-prefix-first: 26.53sec CBMC-WMM: 0.14sec CBMC-SC: 0.79sec CImpact: ERROR/TIMEOUT[8] 274.61sec ESBMC: 0.11sec Threader-monolithic: ERROR/TIMEOUT[130] 896.90sec Threader-owicki-gries: ERROR/TIMEOUT[130] 896.87sec Threader-rely-guarantee: ERROR/TIMEOUT[130] 897.25sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT Blender: |
Cycles
SatAbs: 11.04sec (x8.90) Satabs-prefix-first: 23.15sec CBMC-WMM: 0.19sec CBMC-SC: 0.85sec CImpact: ERROR/TIMEOUT[8] 329.49sec ESBMC: 0.09sec Threader-monolithic: ERROR/TIMEOUT[130] 896.36sec Threader-owicki-gries: ERROR/TIMEOUT[130] 896.56sec Threader-rely-guarantee: ERROR/TIMEOUT[130] 895.20sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT |
Cycles
SatAbs: 11.99sec (x9.66) Satabs-prefix-first: 31.31sec CBMC-WMM: 0.20sec CBMC-SC: 0.96sec CImpact: ERROR/TIMEOUT[8] 308.85sec ESBMC: 0.09sec Threader-monolithic: ERROR/TIMEOUT[130] 896.62sec Threader-owicki-gries: ERROR/TIMEOUT[130] 896.06sec Threader-rely-guarantee: ERROR/TIMEOUT[130] 896.76sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT |
Cycles
SatAbs: 10.55sec (x8.50) Satabs-prefix-first: 27.83sec CBMC-WMM: 0.20sec CBMC-SC: 0.87sec CImpact: ERROR/TIMEOUT[8] 346.52sec ESBMC: 0.08sec Threader-monolithic: ERROR/TIMEOUT[130] 896.76sec Threader-owicki-gries: ERROR/TIMEOUT[130] 895.01sec Threader-rely-guarantee: ERROR/TIMEOUT[130] 896.30sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT |
Cycles
SatAbs: 33.32sec (x26.87) Satabs-prefix-first: 55.12sec CBMC-WMM: 0.20sec CBMC-SC: 146.74sec CImpact: 1.62sec ESBMC: 0.13sec Threader-monolithic: ERROR/TIMEOUT[130] 897.24sec Threader-owicki-gries: ERROR/TIMEOUT[130] 897.48sec Threader-rely-guarantee: ERROR/TIMEOUT[130] 897.46sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT |
Cycles
SatAbs: 11.31sec (x9.12) Satabs-prefix-first: 28.79sec CBMC-WMM: 0.17sec CBMC-SC: 0.87sec CImpact: ERROR/TIMEOUT[8] 336.51sec ESBMC: 0.06sec Threader-monolithic: ERROR/TIMEOUT[130] 897.09sec Threader-owicki-gries: ERROR/TIMEOUT[130] 897.12sec Threader-rely-guarantee: ERROR/TIMEOUT[130] 897.04sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT |
Cycles
SatAbs: 10.50sec (x8.46) Satabs-prefix-first: 27.81sec CBMC-WMM: 0.20sec CBMC-SC: 0.91sec CImpact: ERROR/TIMEOUT[8] 335.53sec ESBMC: 0.10sec Threader-monolithic: ERROR/TIMEOUT[130] 896.62sec Threader-owicki-gries: ERROR/TIMEOUT[130] 896.64sec Threader-rely-guarantee: ERROR/TIMEOUT[130] 897.20sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT |
||||
ppc/lwdwr012 |
SatAbs: 0.71sec Satabs-prefix-first: 0.75sec CBMC-WMM: 0.05sec CBMC-SC: 0.06sec CImpact: 0.55sec Checkfence: 0.01sec ESBMC: 0.08sec Threader-monolithic: 0.13sec Threader-owicki-gries: 0.13sec Threader-rely-guarantee: 0.11sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT MMChecker (MM: sc): ERROR/TIMEOUT[2] 0.01sec |
Cycles
SatAbs: 12.09sec (x17.02) Satabs-prefix-first: 22.28sec CBMC-WMM: 0.09sec CBMC-SC: 5.10sec CImpact: 0.59sec ESBMC: 0.11sec Threader-monolithic: ERROR/TIMEOUT[130] 896.59sec Threader-owicki-gries: ERROR/TIMEOUT[130] 896.43sec Threader-rely-guarantee: ERROR/TIMEOUT[130] 895.78sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT MMChecker (MM: csharp): ERROR/TIMEOUT[2] 0.00sec |
Cycles
SatAbs: 12.36sec (x17.40) Satabs-prefix-first: 21.44sec CBMC-WMM: 0.11sec CBMC-SC: 5.96sec CImpact: 0.68sec Checkfence: 0.01sec ESBMC: 0.12sec Threader-monolithic: ERROR/TIMEOUT[130] 896.86sec Threader-owicki-gries: ERROR/TIMEOUT[130] 896.80sec Threader-rely-guarantee: ERROR/TIMEOUT[130] 896.77sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT MMChecker (MM: csharp): ERROR/TIMEOUT[2] 0.01sec |
Cycles
SatAbs: 2.96sec (x4.16) Satabs-prefix-first: 6.94sec CBMC-WMM: 0.09sec CBMC-SC: 0.92sec CImpact: 0.49sec ESBMC: 0.13sec Threader-monolithic: ERROR/TIMEOUT[1] 210.72sec Threader-owicki-gries: ERROR/TIMEOUT[1] 203.75sec Threader-rely-guarantee: ERROR/TIMEOUT[1] 179.67sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT MMChecker (MM: csharp): ERROR/TIMEOUT[2] 0.00sec |
Cycles
SatAbs: 2.78sec (x3.91) Satabs-prefix-first: 9.32sec CBMC-WMM: 0.13sec CBMC-SC: 1.01sec CImpact: 0.47sec ESBMC: 0.11sec Threader-monolithic: ERROR/TIMEOUT[1] 161.17sec Threader-owicki-gries: ERROR/TIMEOUT[1] 186.31sec Threader-rely-guarantee: ERROR/TIMEOUT[1] 219.30sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT MMChecker (MM: csharp): ERROR/TIMEOUT[2] 0.00sec |
Cycles
SatAbs: 13.03sec (x18.35) Satabs-prefix-first: 21.82sec CBMC-WMM: 0.10sec CBMC-SC: 6.29sec CImpact: 0.67sec ESBMC: 0.10sec Threader-monolithic: ERROR/TIMEOUT[130] 896.84sec Threader-owicki-gries: ERROR/TIMEOUT[130] 896.31sec Threader-rely-guarantee: ERROR/TIMEOUT[130] 896.62sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT Blender: |
Cycles
SatAbs: 2.90sec (x4.08) Satabs-prefix-first: 7.61sec CBMC-WMM: 0.10sec CBMC-SC: 0.79sec CImpact: 0.52sec ESBMC: 0.08sec Threader-monolithic: ERROR/TIMEOUT[1] 199.90sec Threader-owicki-gries: ERROR/TIMEOUT[1] 213.90sec Threader-rely-guarantee: ERROR/TIMEOUT[1] 210.52sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT Blender: |
Cycles
SatAbs: 2.01sec (x2.83) Satabs-prefix-first: 8.51sec CBMC-WMM: 0.09sec CBMC-SC: 0.42sec CImpact: 3.67sec ESBMC: 0.10sec Threader-monolithic: ERROR/TIMEOUT[1] 205.77sec Threader-owicki-gries: ERROR/TIMEOUT[1] 214.74sec Threader-rely-guarantee: ERROR/TIMEOUT[1] 236.51sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT Blender: |
Cycles
SatAbs: 12.97sec (x18.26) Satabs-prefix-first: 22.03sec CBMC-WMM: 0.11sec CBMC-SC: 5.28sec CImpact: 0.68sec ESBMC: 0.11sec Threader-monolithic: ERROR/TIMEOUT[130] 896.71sec Threader-owicki-gries: ERROR/TIMEOUT[130] 896.14sec Threader-rely-guarantee: ERROR/TIMEOUT[130] 897.03sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT |
Cycles
SatAbs: 2.74sec (x3.85) Satabs-prefix-first: 6.72sec CBMC-WMM: 0.11sec CBMC-SC: 0.88sec CImpact: 0.45sec ESBMC: 0.10sec Threader-monolithic: ERROR/TIMEOUT[1] 209.10sec Threader-owicki-gries: ERROR/TIMEOUT[1] 176.67sec Threader-rely-guarantee: ERROR/TIMEOUT[1] 199.73sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT |
Cycles
SatAbs: 1.73sec (x2.43) Satabs-prefix-first: 8.45sec CBMC-WMM: 0.10sec CBMC-SC: 0.47sec CImpact: 3.59sec ESBMC: 0.11sec Threader-monolithic: ERROR/TIMEOUT[1] 237.28sec Threader-owicki-gries: ERROR/TIMEOUT[1] 236.57sec Threader-rely-guarantee: ERROR/TIMEOUT[1] 237.70sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT |
Cycles
SatAbs: 12.52sec (x17.63) Satabs-prefix-first: 20.76sec CBMC-WMM: 0.12sec CBMC-SC: 5.82sec CImpact: 0.69sec ESBMC: 0.11sec Threader-monolithic: ERROR/TIMEOUT[130] 896.45sec Threader-owicki-gries: ERROR/TIMEOUT[130] 895.33sec Threader-rely-guarantee: ERROR/TIMEOUT[130] 896.57sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT |
Cycles
SatAbs: 2.88sec (x4.05) Satabs-prefix-first: 7.32sec CBMC-WMM: 0.12sec CBMC-SC: 0.82sec CImpact: 0.51sec ESBMC: 0.09sec Threader-monolithic: ERROR/TIMEOUT[1] 181.15sec Threader-owicki-gries: ERROR/TIMEOUT[1] 192.75sec Threader-rely-guarantee: ERROR/TIMEOUT[1] 176.87sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT |
Cycles
SatAbs: 1.83sec (x2.57) Satabs-prefix-first: 9.69sec CBMC-WMM: 0.11sec CBMC-SC: 0.40sec CImpact: 3.65sec ESBMC: 0.09sec Threader-monolithic: ERROR/TIMEOUT[1] 182.18sec Threader-owicki-gries: ERROR/TIMEOUT[1] 171.36sec Threader-rely-guarantee: ERROR/TIMEOUT[1] 187.33sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT |
||||
ppc/lwdwr013 |
SatAbs: 4.14sec Satabs-prefix-first: 1.60sec CBMC-WMM: 0.07sec CBMC-SC: 0.08sec CImpact: ERROR/TIMEOUT[8] 288.11sec Checkfence: 0.00sec ESBMC: 0.09sec Threader-monolithic: 0.16sec Threader-owicki-gries: 0.15sec Threader-rely-guarantee: 0.16sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT MMChecker (MM: sc): ERROR/TIMEOUT[2] 0.01sec |
Cycles
SatAbs: 35.84sec (x8.65) Satabs-prefix-first: 79.48sec CBMC-WMM: 0.15sec CBMC-SC: 13.27sec CImpact: ERROR/TIMEOUT[8] 312.19sec ESBMC: 0.11sec Threader-monolithic: ERROR/TIMEOUT[130] 896.64sec Threader-owicki-gries: ERROR/TIMEOUT[130] 896.25sec Threader-rely-guarantee: ERROR/TIMEOUT[130] 895.83sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT MMChecker (MM: csharp): ERROR/TIMEOUT[2] 0.00sec |
Cycles
SatAbs: 31.33sec (x7.56) Satabs-prefix-first: 72.21sec CBMC-WMM: 0.16sec CBMC-SC: 10.02sec CImpact: ERROR/TIMEOUT[8] 346.69sec Checkfence: 0.01sec ESBMC: 0.10sec Threader-monolithic: ERROR/TIMEOUT[130] 897.18sec Threader-owicki-gries: ERROR/TIMEOUT[130] 896.96sec Threader-rely-guarantee: ERROR/TIMEOUT[130] 896.72sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT MMChecker (MM: csharp): ERROR/TIMEOUT[2] 0.00sec |
Cycles
SatAbs: 7.76sec (x1.87) Satabs-prefix-first: 17.32sec CBMC-WMM: 0.12sec CBMC-SC: 0.76sec CImpact: ERROR/TIMEOUT[8] 220.85sec ESBMC: 0.06sec Threader-monolithic: ERROR/TIMEOUT[1] 175.46sec Threader-owicki-gries: ERROR/TIMEOUT[1] 171.11sec Threader-rely-guarantee: ERROR/TIMEOUT[1] 170.86sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT MMChecker (MM: csharp): ERROR/TIMEOUT[2] 0.00sec |
Cycles
SatAbs: 8.55sec (x2.06) Satabs-prefix-first: 17.97sec CBMC-WMM: 0.12sec CBMC-SC: 0.72sec CImpact: ERROR/TIMEOUT[8] 228.82sec ESBMC: 0.10sec Threader-monolithic: ERROR/TIMEOUT[1] 175.48sec Threader-owicki-gries: ERROR/TIMEOUT[1] 170.52sec Threader-rely-guarantee: ERROR/TIMEOUT[1] 170.34sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT MMChecker (MM: csharp): ERROR/TIMEOUT[2] 0.01sec |
Cycles
SatAbs: 21.72sec (x5.24) Satabs-prefix-first: 55.66sec CBMC-WMM: 0.09sec CBMC-SC: 8.28sec CImpact: ERROR/TIMEOUT[8] 283.62sec ESBMC: 0.09sec Threader-monolithic: ERROR/TIMEOUT[130] 897.18sec Threader-owicki-gries: ERROR/TIMEOUT[130] 896.83sec Threader-rely-guarantee: ERROR/TIMEOUT[130] 896.86sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT Blender: |
Cycles
SatAbs: 10.31sec (x2.49) Satabs-prefix-first: 20.22sec CBMC-WMM: 0.12sec CBMC-SC: 0.74sec CImpact: ERROR/TIMEOUT[8] 264.01sec ESBMC: 0.11sec Threader-monolithic: ERROR/TIMEOUT[1] 185.73sec Threader-owicki-gries: ERROR/TIMEOUT[1] 174.48sec Threader-rely-guarantee: ERROR/TIMEOUT[1] 170.03sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT Blender: |
Cycles
SatAbs: 15.36sec (x3.71) Satabs-prefix-first: 16.22sec CBMC-WMM: 0.11sec CBMC-SC: 0.58sec CImpact: ERROR/TIMEOUT[8] 214.89sec ESBMC: 0.06sec Threader-monolithic: ERROR/TIMEOUT[1] 170.23sec Threader-owicki-gries: ERROR/TIMEOUT[1] 169.11sec Threader-rely-guarantee: ERROR/TIMEOUT[1] 169.85sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT Blender: |
Cycles
SatAbs: 31.66sec (x7.64) Satabs-prefix-first: 73.73sec CBMC-WMM: 0.12sec CBMC-SC: 8.18sec CImpact: ERROR/TIMEOUT[8] 282.02sec ESBMC: 0.09sec Threader-monolithic: ERROR/TIMEOUT[130] 896.30sec Threader-owicki-gries: ERROR/TIMEOUT[130] 896.83sec Threader-rely-guarantee: ERROR/TIMEOUT[130] 897.13sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT |
Cycles
SatAbs: 7.07sec (x1.70) Satabs-prefix-first: 17.73sec CBMC-WMM: 0.10sec CBMC-SC: 0.75sec CImpact: ERROR/TIMEOUT[8] 222.09sec ESBMC: 0.07sec Threader-monolithic: ERROR/TIMEOUT[1] 172.78sec Threader-owicki-gries: ERROR/TIMEOUT[1] 170.41sec Threader-rely-guarantee: ERROR/TIMEOUT[1] 170.90sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT |
Cycles
SatAbs: 14.60sec (x3.52) Satabs-prefix-first: 16.09sec CBMC-WMM: 0.12sec CBMC-SC: 0.59sec CImpact: ERROR/TIMEOUT[8] 217.77sec ESBMC: 0.05sec Threader-monolithic: ERROR/TIMEOUT[1] 170.19sec Threader-owicki-gries: ERROR/TIMEOUT[1] 171.07sec Threader-rely-guarantee: ERROR/TIMEOUT[1] 170.93sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT |
Cycles
SatAbs: 32.04sec (x7.73) Satabs-prefix-first: 73.16sec CBMC-WMM: 0.14sec CBMC-SC: 8.32sec CImpact: ERROR/TIMEOUT[8] 283.29sec ESBMC: 0.09sec Threader-monolithic: ERROR/TIMEOUT[130] 895.48sec Threader-owicki-gries: ERROR/TIMEOUT[130] 896.33sec Threader-rely-guarantee: ERROR/TIMEOUT[130] 896.89sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT |
Cycles
SatAbs: 12.64sec (x3.05) Satabs-prefix-first: 24.75sec CBMC-WMM: 0.12sec CBMC-SC: 0.86sec CImpact: ERROR/TIMEOUT[8] 238.50sec ESBMC: 0.08sec Threader-monolithic: ERROR/TIMEOUT[1] 185.60sec Threader-owicki-gries: ERROR/TIMEOUT[1] 170.68sec Threader-rely-guarantee: ERROR/TIMEOUT[1] 170.51sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT |
Cycles
SatAbs: 11.79sec (x2.84) Satabs-prefix-first: 13.08sec CBMC-WMM: 0.13sec CBMC-SC: 0.55sec CImpact: ERROR/TIMEOUT[8] 215.91sec ESBMC: 0.07sec Threader-monolithic: ERROR/TIMEOUT[1] 171.42sec Threader-owicki-gries: ERROR/TIMEOUT[1] 173.26sec Threader-rely-guarantee: ERROR/TIMEOUT[1] 172.12sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT |
||||
ppc/lwdwr014 |
SatAbs: 2.93sec Satabs-prefix-first: 1.09sec CBMC-WMM: 0.07sec CBMC-SC: 0.06sec CImpact: ERROR/TIMEOUT[8] 199.00sec Checkfence: 0.01sec ESBMC: 0.06sec Threader-monolithic: 0.11sec Threader-owicki-gries: 0.11sec Threader-rely-guarantee: 0.10sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT MMChecker (MM: sc): ERROR/TIMEOUT[2] 0.00sec |
Cycles
SatAbs: 33.68sec (x11.49) Satabs-prefix-first: 51.26sec CBMC-WMM: 0.10sec CBMC-SC: 13.86sec CImpact: ERROR/TIMEOUT[8] 284.80sec ESBMC: 0.07sec Threader-monolithic: ERROR/TIMEOUT[130] 897.13sec Threader-owicki-gries: ERROR/TIMEOUT[130] 897.09sec Threader-rely-guarantee: ERROR/TIMEOUT[130] 897.18sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT MMChecker (MM: csharp): ERROR/TIMEOUT[2] 0.01sec |
Cycles
SatAbs: 15.93sec (x5.43) Satabs-prefix-first: 28.60sec CBMC-WMM: 0.12sec CBMC-SC: 4.51sec CImpact: ERROR/TIMEOUT[8] 245.47sec Checkfence: 0.01sec ESBMC: 0.08sec Threader-monolithic: ERROR/TIMEOUT[130] 896.17sec Threader-owicki-gries: ERROR/TIMEOUT[130] 896.82sec Threader-rely-guarantee: ERROR/TIMEOUT[130] 896.81sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT MMChecker (MM: csharp): ERROR/TIMEOUT[2] 0.00sec |
Cycles
SatAbs: 5.56sec (x1.89) Satabs-prefix-first: 17.79sec CBMC-WMM: 0.12sec CBMC-SC: 0.69sec CImpact: ERROR/TIMEOUT[8] 216.85sec ESBMC: 0.07sec Threader-monolithic: ERROR/TIMEOUT[1] 170.37sec Threader-owicki-gries: ERROR/TIMEOUT[1] 173.25sec Threader-rely-guarantee: ERROR/TIMEOUT[1] 170.49sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT MMChecker (MM: csharp): ERROR/TIMEOUT[2] 0.00sec |
Cycles
SatAbs: 5.66sec (x1.93) Satabs-prefix-first: 17.93sec CBMC-WMM: 0.11sec CBMC-SC: 0.69sec CImpact: ERROR/TIMEOUT[8] 212.90sec ESBMC: 0.08sec Threader-monolithic: ERROR/TIMEOUT[1] 170.46sec Threader-owicki-gries: ERROR/TIMEOUT[1] 170.11sec Threader-rely-guarantee: ERROR/TIMEOUT[1] 170.30sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT MMChecker (MM: csharp): ERROR/TIMEOUT[2] 0.00sec |
Cycles
SatAbs: 15.73sec (x5.36) Satabs-prefix-first: 26.11sec CBMC-WMM: 0.09sec CBMC-SC: 4.53sec CImpact: ERROR/TIMEOUT[8] 242.57sec ESBMC: 0.06sec Threader-monolithic: ERROR/TIMEOUT[130] 896.89sec Threader-owicki-gries: ERROR/TIMEOUT[130] 896.87sec Threader-rely-guarantee: ERROR/TIMEOUT[130] 896.81sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT Blender: |
Cycles
SatAbs: 5.76sec (x1.96) Satabs-prefix-first: 25.98sec CBMC-WMM: 0.12sec CBMC-SC: 0.72sec CImpact: ERROR/TIMEOUT[8] 228.19sec ESBMC: 0.07sec Threader-monolithic: ERROR/TIMEOUT[1] 175.35sec Threader-owicki-gries: ERROR/TIMEOUT[1] 177.02sec Threader-rely-guarantee: ERROR/TIMEOUT[1] 171.82sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT Blender: |
Cycles
SatAbs: 13.91sec (x4.74) Satabs-prefix-first: 13.97sec CBMC-WMM: 0.12sec CBMC-SC: 0.61sec CImpact: ERROR/TIMEOUT[8] 226.86sec ESBMC: 0.08sec Threader-monolithic: ERROR/TIMEOUT[1] 179.38sec Threader-owicki-gries: ERROR/TIMEOUT[1] 177.50sec Threader-rely-guarantee: ERROR/TIMEOUT[1] 169.53sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT Blender: |
Cycles
SatAbs: 16.07sec (x5.48) Satabs-prefix-first: 26.15sec CBMC-WMM: 0.11sec CBMC-SC: 4.53sec CImpact: ERROR/TIMEOUT[8] 242.66sec ESBMC: 0.07sec Threader-monolithic: ERROR/TIMEOUT[130] 896.77sec Threader-owicki-gries: ERROR/TIMEOUT[130] 896.74sec Threader-rely-guarantee: ERROR/TIMEOUT[130] 896.62sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT |
Cycles
SatAbs: 5.92sec (x2.02) Satabs-prefix-first: 18.36sec CBMC-WMM: 0.13sec CBMC-SC: 0.70sec CImpact: ERROR/TIMEOUT[8] 218.35sec ESBMC: 0.06sec Threader-monolithic: ERROR/TIMEOUT[1] 171.42sec Threader-owicki-gries: ERROR/TIMEOUT[1] 172.38sec Threader-rely-guarantee: ERROR/TIMEOUT[1] 171.12sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT |
Cycles
SatAbs: 12.05sec (x4.11) Satabs-prefix-first: 11.40sec CBMC-WMM: 0.12sec CBMC-SC: 0.59sec CImpact: ERROR/TIMEOUT[8] 218.40sec ESBMC: 0.07sec Threader-monolithic: ERROR/TIMEOUT[1] 170.83sec Threader-owicki-gries: ERROR/TIMEOUT[1] 170.28sec Threader-rely-guarantee: ERROR/TIMEOUT[1] 170.58sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT |
Cycles
SatAbs: 16.35sec (x5.58) Satabs-prefix-first: 24.15sec CBMC-WMM: 0.13sec CBMC-SC: 4.49sec CImpact: ERROR/TIMEOUT[8] 244.81sec ESBMC: 0.07sec Threader-monolithic: ERROR/TIMEOUT[130] 896.84sec Threader-owicki-gries: ERROR/TIMEOUT[130] 896.84sec Threader-rely-guarantee: ERROR/TIMEOUT[130] 896.72sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT |
Cycles
SatAbs: 5.65sec (x1.92) Satabs-prefix-first: 17.96sec CBMC-WMM: 0.13sec CBMC-SC: 0.67sec CImpact: ERROR/TIMEOUT[8] 213.46sec ESBMC: 0.07sec Threader-monolithic: ERROR/TIMEOUT[1] 170.86sec Threader-owicki-gries: ERROR/TIMEOUT[1] 170.86sec Threader-rely-guarantee: ERROR/TIMEOUT[1] 173.58sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT |
Cycles
SatAbs: 17.74sec (x6.05) Satabs-prefix-first: 16.16sec CBMC-WMM: 0.13sec CBMC-SC: 0.95sec CImpact: ERROR/TIMEOUT[8] 230.87sec ESBMC: 0.07sec Threader-monolithic: ERROR/TIMEOUT[1] 170.35sec Threader-owicki-gries: ERROR/TIMEOUT[1] 170.43sec Threader-rely-guarantee: ERROR/TIMEOUT[1] 170.43sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT |
||||
ppc/lwdwr015 |
SatAbs: 2.78sec Satabs-prefix-first: 2.30sec CBMC-WMM: 0.05sec CBMC-SC: 0.07sec CImpact: ERROR/TIMEOUT[8] 205.31sec Checkfence: 0.00sec ESBMC: 0.05sec Threader-monolithic: 0.11sec Threader-owicki-gries: 0.11sec Threader-rely-guarantee: 0.10sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT MMChecker (MM: sc): ERROR/TIMEOUT[2] 0.00sec |
Cycles
SatAbs: 9.47sec (x3.40) Satabs-prefix-first: 5.04sec CBMC-WMM: 0.11sec CBMC-SC: 49.14sec CImpact: ERROR/TIMEOUT[8] 292.31sec ESBMC: 0.10sec Threader-monolithic: ERROR/TIMEOUT[130] 897.35sec Threader-owicki-gries: ERROR/TIMEOUT[130] 897.30sec Threader-rely-guarantee: ERROR/TIMEOUT[130] 897.54sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT MMChecker (MM: csharp): ERROR/TIMEOUT[2] 0.00sec |
Cycles
SatAbs: 386.42sec (x139.00) Satabs-prefix-first: ERROR/TIMEOUT[130] 907.76sec CBMC-WMM: 0.10sec CBMC-SC: 38.64sec CImpact: ERROR/TIMEOUT[8] 296.90sec Checkfence: 0.01sec ESBMC: 0.07sec Threader-monolithic: ERROR/TIMEOUT[130] 897.27sec Threader-owicki-gries: ERROR/TIMEOUT[130] 897.47sec Threader-rely-guarantee: ERROR/TIMEOUT[130] 897.40sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT MMChecker (MM: csharp): ERROR/TIMEOUT[2] 0.00sec |
Cycles
SatAbs: 334.06sec (x120.16) Satabs-prefix-first: ERROR/TIMEOUT[130] 903.53sec CBMC-WMM: 0.12sec CBMC-SC: 3.98sec CImpact: ERROR/TIMEOUT[8] 262.88sec ESBMC: 0.09sec Threader-monolithic: ERROR/TIMEOUT[130] 897.46sec Threader-owicki-gries: ERROR/TIMEOUT[130] 897.38sec 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: 5.68sec (x2.04) Satabs-prefix-first: 16.06sec CBMC-WMM: 0.22sec CBMC-SC: 0.74sec CImpact: ERROR/TIMEOUT[8] 293.36sec ESBMC: 0.07sec Threader-monolithic: ERROR/TIMEOUT[1] 176.03sec Threader-owicki-gries: ERROR/TIMEOUT[1] 176.23sec Threader-rely-guarantee: ERROR/TIMEOUT[1] 177.82sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT MMChecker (MM: csharp): ERROR/TIMEOUT[2] 0.00sec |
Cycles
SatAbs: 396.81sec (x142.73) Satabs-prefix-first: ERROR/TIMEOUT[130] 908.21sec CBMC-WMM: 0.12sec CBMC-SC: 37.99sec CImpact: ERROR/TIMEOUT[8] 293.49sec ESBMC: 0.12sec Threader-monolithic: ERROR/TIMEOUT[130] 897.55sec Threader-owicki-gries: ERROR/TIMEOUT[130] 897.35sec Threader-rely-guarantee: ERROR/TIMEOUT[130] 897.34sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT Blender: |
Cycles
SatAbs: 336.28sec (x120.96) Satabs-prefix-first: ERROR/TIMEOUT[130] 903.44sec CBMC-WMM: 0.12sec CBMC-SC: 4.00sec CImpact: ERROR/TIMEOUT[8] 268.46sec ESBMC: 0.06sec Threader-monolithic: ERROR/TIMEOUT[130] 897.46sec Threader-owicki-gries: ERROR/TIMEOUT[130] 897.38sec Threader-rely-guarantee: ERROR/TIMEOUT[130] 897.46sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT Blender: |
Cycles
SatAbs: 4.69sec (x1.68) Satabs-prefix-first: 10.75sec CBMC-WMM: 0.12sec CBMC-SC: 0.48sec CImpact: ERROR/TIMEOUT[8] 281.09sec ESBMC: 0.06sec Threader-monolithic: ERROR/TIMEOUT[1] 174.08sec Threader-owicki-gries: ERROR/TIMEOUT[1] 173.27sec Threader-rely-guarantee: ERROR/TIMEOUT[1] 174.78sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT Blender: |
Cycles
SatAbs: 387.65sec (x139.44) Satabs-prefix-first: ERROR/TIMEOUT[130] 907.30sec CBMC-WMM: 0.12sec CBMC-SC: 38.01sec CImpact: ERROR/TIMEOUT[8] 291.90sec ESBMC: 0.07sec Threader-monolithic: ERROR/TIMEOUT[130] 897.13sec Threader-owicki-gries: ERROR/TIMEOUT[130] 897.35sec Threader-rely-guarantee: ERROR/TIMEOUT[130] 897.35sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT |
Cycles
SatAbs: 331.86sec (x119.37) Satabs-prefix-first: ERROR/TIMEOUT[130] 903.04sec CBMC-WMM: 0.23sec CBMC-SC: 4.10sec CImpact: ERROR/TIMEOUT[8] 261.98sec ESBMC: 0.07sec Threader-monolithic: ERROR/TIMEOUT[130] 897.53sec Threader-owicki-gries: ERROR/TIMEOUT[130] 897.39sec Threader-rely-guarantee: ERROR/TIMEOUT[130] 897.40sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT |
Cycles
SatAbs: 4.39sec (x1.57) Satabs-prefix-first: 11.02sec CBMC-WMM: 0.12sec CBMC-SC: 0.49sec CImpact: ERROR/TIMEOUT[8] 260.20sec ESBMC: 0.08sec Threader-monolithic: ERROR/TIMEOUT[1] 179.04sec Threader-owicki-gries: ERROR/TIMEOUT[1] 173.49sec Threader-rely-guarantee: ERROR/TIMEOUT[1] 173.95sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT |
Cycles
SatAbs: 63.02sec (x22.66) Satabs-prefix-first: 98.06sec CBMC-WMM: 0.11sec CBMC-SC: 114.49sec CImpact: ERROR/TIMEOUT[8] 363.48sec ESBMC: 0.10sec Threader-monolithic: ERROR/TIMEOUT[130] 897.63sec Threader-owicki-gries: ERROR/TIMEOUT[130] 897.43sec Threader-rely-guarantee: ERROR/TIMEOUT[130] 897.57sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT |
Cycles
SatAbs: 348.99sec (x125.53) Satabs-prefix-first: ERROR/TIMEOUT[130] 904.27sec CBMC-WMM: 0.11sec CBMC-SC: 4.11sec CImpact: ERROR/TIMEOUT[8] 266.40sec ESBMC: 0.08sec Threader-monolithic: ERROR/TIMEOUT[130] 897.51sec Threader-owicki-gries: ERROR/TIMEOUT[130] 897.28sec Threader-rely-guarantee: ERROR/TIMEOUT[130] 897.45sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT |
Cycles
SatAbs: 4.30sec (x1.54) Satabs-prefix-first: 10.79sec CBMC-WMM: 0.10sec CBMC-SC: 0.47sec CImpact: ERROR/TIMEOUT[8] 254.33sec ESBMC: 0.06sec Threader-monolithic: ERROR/TIMEOUT[1] 174.57sec Threader-owicki-gries: ERROR/TIMEOUT[1] 173.20sec Threader-rely-guarantee: ERROR/TIMEOUT[1] 173.24sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT |
||||
ppc/lwdwr016 |
SatAbs: 2.84sec Satabs-prefix-first: 0.91sec CBMC-WMM: 0.06sec CBMC-SC: 0.07sec CImpact: ERROR/TIMEOUT[8] 226.91sec Checkfence: 0.01sec ESBMC: 0.07sec Threader-monolithic: 0.10sec Threader-owicki-gries: 0.10sec Threader-rely-guarantee: 0.09sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT MMChecker (MM: sc): ERROR/TIMEOUT[2] 0.00sec |
Cycles
SatAbs: 3.01sec (x1.05) Satabs-prefix-first: 3.57sec CBMC-WMM: 0.11sec CBMC-SC: 18.76sec CImpact: ERROR/TIMEOUT[8] 325.57sec ESBMC: 0.08sec Threader-monolithic: ERROR/TIMEOUT[130] 897.50sec Threader-owicki-gries: ERROR/TIMEOUT[130] 897.53sec Threader-rely-guarantee: ERROR/TIMEOUT[130] 897.65sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT MMChecker (MM: csharp): ERROR/TIMEOUT[2] 0.00sec |
Cycles
SatAbs: 6.10sec (x2.14) Satabs-prefix-first: 12.74sec CBMC-WMM: 0.12sec CBMC-SC: 0.59sec CImpact: ERROR/TIMEOUT[8] 240.56sec Checkfence: 0.01sec ESBMC: 0.06sec Threader-monolithic: ERROR/TIMEOUT[1] 171.28sec Threader-owicki-gries: ERROR/TIMEOUT[1] 171.68sec Threader-rely-guarantee: ERROR/TIMEOUT[1] 169.71sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT MMChecker (MM: csharp): ERROR/TIMEOUT[2] 0.00sec |
Cycles
SatAbs: 6.28sec (x2.21) Satabs-prefix-first: 12.85sec CBMC-WMM: 0.10sec CBMC-SC: 0.59sec CImpact: ERROR/TIMEOUT[8] 218.97sec ESBMC: 0.07sec Threader-monolithic: ERROR/TIMEOUT[1] 171.18sec Threader-owicki-gries: ERROR/TIMEOUT[1] 171.05sec Threader-rely-guarantee: ERROR/TIMEOUT[1] 170.82sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT MMChecker (MM: csharp): ERROR/TIMEOUT[2] 0.00sec |
Cycles
SatAbs: 6.33sec (x2.22) Satabs-prefix-first: 13.21sec CBMC-WMM: 0.12sec CBMC-SC: 0.58sec CImpact: ERROR/TIMEOUT[8] 217.71sec ESBMC: 0.07sec Threader-monolithic: ERROR/TIMEOUT[1] 170.98sec Threader-owicki-gries: ERROR/TIMEOUT[1] 170.48sec Threader-rely-guarantee: ERROR/TIMEOUT[1] 170.11sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT MMChecker (MM: csharp): ERROR/TIMEOUT[2] 0.00sec |
Cycles
SatAbs: 6.00sec (x2.11) Satabs-prefix-first: 12.82sec CBMC-WMM: 0.12sec CBMC-SC: 0.61sec CImpact: ERROR/TIMEOUT[8] 220.37sec ESBMC: 0.07sec Threader-monolithic: ERROR/TIMEOUT[1] 171.83sec Threader-owicki-gries: ERROR/TIMEOUT[1] 169.26sec Threader-rely-guarantee: ERROR/TIMEOUT[1] 171.01sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT Blender: |
Cycles
SatAbs: 6.18sec (x2.17) Satabs-prefix-first: 12.66sec CBMC-WMM: 0.12sec CBMC-SC: 0.63sec CImpact: ERROR/TIMEOUT[8] 218.30sec ESBMC: 0.08sec Threader-monolithic: ERROR/TIMEOUT[1] 170.58sec Threader-owicki-gries: ERROR/TIMEOUT[1] 170.59sec Threader-rely-guarantee: ERROR/TIMEOUT[1] 169.88sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT Blender: |
Cycles
SatAbs: 5.68sec (x2.00) Satabs-prefix-first: 12.49sec CBMC-WMM: 0.12sec CBMC-SC: 0.62sec CImpact: ERROR/TIMEOUT[8] 220.51sec ESBMC: 0.07sec Threader-monolithic: ERROR/TIMEOUT[1] 170.73sec Threader-owicki-gries: ERROR/TIMEOUT[1] 170.79sec Threader-rely-guarantee: ERROR/TIMEOUT[1] 171.91sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT Blender: |
Cycles
SatAbs: 7.89sec (x2.77) Satabs-prefix-first: 15.65sec CBMC-WMM: 0.12sec CBMC-SC: 0.62sec CImpact: ERROR/TIMEOUT[8] 218.91sec ESBMC: 0.07sec Threader-monolithic: ERROR/TIMEOUT[1] 170.76sec Threader-owicki-gries: ERROR/TIMEOUT[1] 178.57sec Threader-rely-guarantee: ERROR/TIMEOUT[1] 169.64sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT |
Cycles
SatAbs: 7.79sec (x2.74) Satabs-prefix-first: 15.58sec CBMC-WMM: 0.11sec CBMC-SC: 0.60sec CImpact: ERROR/TIMEOUT[8] 217.27sec ESBMC: 0.07sec Threader-monolithic: ERROR/TIMEOUT[1] 170.08sec Threader-owicki-gries: ERROR/TIMEOUT[1] 173.77sec Threader-rely-guarantee: ERROR/TIMEOUT[1] 170.37sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT |
Cycles
SatAbs: 8.17sec (x2.87) Satabs-prefix-first: 16.10sec CBMC-WMM: 0.13sec CBMC-SC: 0.63sec CImpact: ERROR/TIMEOUT[8] 218.90sec ESBMC: 0.08sec Threader-monolithic: ERROR/TIMEOUT[1] 171.54sec Threader-owicki-gries: ERROR/TIMEOUT[1] 172.96sec Threader-rely-guarantee: ERROR/TIMEOUT[1] 170.22sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT |
Cycles
SatAbs: 7.92sec (x2.78) Satabs-prefix-first: 15.69sec CBMC-WMM: 0.12sec CBMC-SC: 0.60sec CImpact: ERROR/TIMEOUT[8] 216.40sec ESBMC: 0.07sec Threader-monolithic: ERROR/TIMEOUT[1] 169.31sec Threader-owicki-gries: ERROR/TIMEOUT[1] 170.45sec Threader-rely-guarantee: ERROR/TIMEOUT[1] 172.76sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT |
Cycles
SatAbs: 7.93sec (x2.79) Satabs-prefix-first: 15.99sec CBMC-WMM: 0.11sec CBMC-SC: 0.62sec CImpact: ERROR/TIMEOUT[8] 217.28sec ESBMC: 0.06sec Threader-monolithic: ERROR/TIMEOUT[1] 170.51sec Threader-owicki-gries: ERROR/TIMEOUT[1] 169.40sec Threader-rely-guarantee: ERROR/TIMEOUT[1] 170.11sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT |
Cycles
SatAbs: 7.86sec (x2.76) Satabs-prefix-first: 15.87sec CBMC-WMM: 0.13sec CBMC-SC: 0.60sec CImpact: ERROR/TIMEOUT[8] 218.42sec ESBMC: 0.07sec Threader-monolithic: ERROR/TIMEOUT[1] 170.74sec Threader-owicki-gries: ERROR/TIMEOUT[1] 170.58sec Threader-rely-guarantee: ERROR/TIMEOUT[1] 170.03sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT |
||||
ppc/lwdwr017 |
SatAbs: 4.01sec Satabs-prefix-first: 1.36sec CBMC-WMM: 0.07sec CBMC-SC: 0.07sec CImpact: ERROR/TIMEOUT[8] 202.23sec Checkfence: 0.00sec ESBMC: 0.07sec Threader-monolithic: 0.11sec Threader-owicki-gries: 0.11sec Threader-rely-guarantee: 0.08sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT MMChecker (MM: sc): ERROR/TIMEOUT[2] 0.00sec |
Cycles
SatAbs: 4.21sec (x1.04) Satabs-prefix-first: 4.98sec CBMC-WMM: 0.12sec CBMC-SC: 22.76sec CImpact: ERROR/TIMEOUT[8] 303.41sec ESBMC: 0.07sec Threader-monolithic: ERROR/TIMEOUT[130] 897.44sec Threader-owicki-gries: ERROR/TIMEOUT[130] 897.48sec Threader-rely-guarantee: ERROR/TIMEOUT[130] 897.55sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT MMChecker (MM: csharp): ERROR/TIMEOUT[2] 0.01sec |
Cycles
SatAbs: 7.74sec (x1.93) Satabs-prefix-first: 8.76sec CBMC-WMM: 0.09sec CBMC-SC: 0.35sec CImpact: ERROR/TIMEOUT[8] 274.35sec Checkfence: 0.01sec ESBMC: 0.15sec Threader-monolithic: ERROR/TIMEOUT[1] 173.90sec Threader-owicki-gries: ERROR/TIMEOUT[1] 170.49sec Threader-rely-guarantee: ERROR/TIMEOUT[1] 171.92sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT MMChecker (MM: csharp): ERROR/TIMEOUT[2] 0.01sec |
Cycles
SatAbs: 7.17sec (x1.78) Satabs-prefix-first: 8.11sec CBMC-WMM: 0.10sec CBMC-SC: 0.33sec CImpact: ERROR/TIMEOUT[8] 215.81sec ESBMC: 0.05sec Threader-monolithic: ERROR/TIMEOUT[1] 172.92sec Threader-owicki-gries: ERROR/TIMEOUT[1] 170.72sec Threader-rely-guarantee: ERROR/TIMEOUT[1] 170.67sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT MMChecker (MM: csharp): ERROR/TIMEOUT[2] 0.01sec |
Cycles
SatAbs: 6.86sec (x1.71) Satabs-prefix-first: 7.92sec CBMC-WMM: 0.10sec CBMC-SC: 0.39sec CImpact: ERROR/TIMEOUT[8] 215.92sec ESBMC: 0.08sec Threader-monolithic: ERROR/TIMEOUT[1] 171.36sec Threader-owicki-gries: ERROR/TIMEOUT[1] 170.92sec Threader-rely-guarantee: ERROR/TIMEOUT[1] 170.91sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT MMChecker (MM: csharp): ERROR/TIMEOUT[2] 0.03sec |
Cycles
SatAbs: 7.06sec (x1.76) Satabs-prefix-first: 8.26sec CBMC-WMM: 0.10sec CBMC-SC: 0.39sec CImpact: ERROR/TIMEOUT[8] 215.87sec ESBMC: 0.09sec Threader-monolithic: ERROR/TIMEOUT[1] 172.32sec Threader-owicki-gries: ERROR/TIMEOUT[1] 173.71sec Threader-rely-guarantee: ERROR/TIMEOUT[1] 170.48sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT Blender: |
Cycles
SatAbs: 7.35sec (x1.83) Satabs-prefix-first: 8.18sec CBMC-WMM: 0.10sec CBMC-SC: 0.37sec CImpact: ERROR/TIMEOUT[8] 215.71sec ESBMC: 0.07sec Threader-monolithic: ERROR/TIMEOUT[1] 170.36sec Threader-owicki-gries: ERROR/TIMEOUT[1] 175.85sec Threader-rely-guarantee: ERROR/TIMEOUT[1] 170.12sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT Blender: |
Cycles
SatAbs: 8.59sec (x2.14) Satabs-prefix-first: 9.92sec CBMC-WMM: 0.11sec CBMC-SC: 0.37sec CImpact: ERROR/TIMEOUT[8] 215.68sec ESBMC: 0.06sec Threader-monolithic: ERROR/TIMEOUT[1] 170.13sec Threader-owicki-gries: ERROR/TIMEOUT[1] 179.22sec Threader-rely-guarantee: ERROR/TIMEOUT[1] 169.95sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT Blender: |
Cycles
SatAbs: 8.49sec (x2.11) Satabs-prefix-first: 9.93sec CBMC-WMM: 0.13sec CBMC-SC: 0.37sec CImpact: ERROR/TIMEOUT[8] 220.87sec ESBMC: 0.08sec Threader-monolithic: ERROR/TIMEOUT[1] 182.22sec Threader-owicki-gries: ERROR/TIMEOUT[1] 171.06sec Threader-rely-guarantee: ERROR/TIMEOUT[1] 196.08sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT |
Cycles
SatAbs: 10.21sec (x2.54) Satabs-prefix-first: 12.30sec CBMC-WMM: 0.24sec CBMC-SC: 0.41sec CImpact: ERROR/TIMEOUT[8] 234.36sec ESBMC: 0.08sec Threader-monolithic: ERROR/TIMEOUT[1] 173.34sec Threader-owicki-gries: ERROR/TIMEOUT[1] 172.00sec Threader-rely-guarantee: ERROR/TIMEOUT[1] 177.41sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT |
Cycles
SatAbs: 7.52sec (x1.87) Satabs-prefix-first: 14.20sec CBMC-WMM: 0.18sec CBMC-SC: 0.68sec CImpact: ERROR/TIMEOUT[8] 234.27sec ESBMC: 0.08sec Threader-monolithic: ERROR/TIMEOUT[1] 171.44sec Threader-owicki-gries: ERROR/TIMEOUT[1] 172.97sec Threader-rely-guarantee: ERROR/TIMEOUT[1] 182.10sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT |
Cycles
SatAbs: 71.70sec (x17.88) Satabs-prefix-first: 66.34sec CBMC-WMM: 0.14sec CBMC-SC: 8.65sec CImpact: ERROR/TIMEOUT[8] 283.31sec ESBMC: 0.07sec Threader-monolithic: ERROR/TIMEOUT[130] 897.62sec Threader-owicki-gries: ERROR/TIMEOUT[130] 897.60sec Threader-rely-guarantee: ERROR/TIMEOUT[130] 897.43sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT |
Cycles
SatAbs: 7.07sec (x1.76) Satabs-prefix-first: 8.02sec CBMC-WMM: 0.12sec CBMC-SC: 0.39sec CImpact: ERROR/TIMEOUT[8] 226.55sec ESBMC: 0.07sec Threader-monolithic: ERROR/TIMEOUT[1] 171.35sec Threader-owicki-gries: ERROR/TIMEOUT[1] 173.43sec Threader-rely-guarantee: ERROR/TIMEOUT[1] 171.24sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT |
Cycles
SatAbs: 8.60sec (x2.14) Satabs-prefix-first: 9.51sec CBMC-WMM: 0.13sec CBMC-SC: 0.39sec CImpact: ERROR/TIMEOUT[8] 225.99sec ESBMC: 0.07sec Threader-monolithic: ERROR/TIMEOUT[1] 170.75sec Threader-owicki-gries: ERROR/TIMEOUT[1] 170.71sec Threader-rely-guarantee: ERROR/TIMEOUT[1] 177.89sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT |
||||
ppc/lwdwr018 |
SatAbs: 0.59sec Satabs-prefix-first: 0.72sec CBMC-WMM: 0.04sec CBMC-SC: 0.04sec CImpact: 0.30sec Checkfence: 0.00sec ESBMC: 0.06sec Threader-monolithic: 0.10sec Threader-owicki-gries: 0.09sec Threader-rely-guarantee: 0.08sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT MMChecker (MM: sc): ERROR/TIMEOUT[2] 0.00sec |
Cycles
SatAbs: 11.39sec (x19.30) Satabs-prefix-first: 18.22sec CBMC-WMM: 0.06sec CBMC-SC: 5.32sec CImpact: 4.44sec ESBMC: 0.08sec Threader-monolithic: ERROR/TIMEOUT[130] 896.28sec Threader-owicki-gries: ERROR/TIMEOUT[130] 896.64sec Threader-rely-guarantee: ERROR/TIMEOUT[130] 896.63sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT MMChecker (MM: csharp): ERROR/TIMEOUT[2] 0.00sec |
Cycles
SatAbs: 1.55sec (x2.62) Satabs-prefix-first: 6.09sec CBMC-WMM: 0.08sec CBMC-SC: 0.33sec CImpact: 6.85sec Checkfence: 0.01sec ESBMC: 0.05sec Threader-monolithic: ERROR/TIMEOUT[1] 157.09sec Threader-owicki-gries: ERROR/TIMEOUT[1] 159.97sec Threader-rely-guarantee: ERROR/TIMEOUT[1] 156.41sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT MMChecker (MM: csharp): ERROR/TIMEOUT[2] 0.00sec |
Cycles
SatAbs: 1.50sec (x2.54) Satabs-prefix-first: 6.44sec CBMC-WMM: 0.07sec CBMC-SC: 0.32sec CImpact: 6.79sec ESBMC: 0.08sec Threader-monolithic: ERROR/TIMEOUT[1] 155.85sec Threader-owicki-gries: ERROR/TIMEOUT[1] 159.81sec Threader-rely-guarantee: ERROR/TIMEOUT[1] 156.64sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT MMChecker (MM: csharp): ERROR/TIMEOUT[2] 0.00sec |
Cycles
SatAbs: 1.31sec (x2.22) Satabs-prefix-first: 5.83sec CBMC-WMM: 0.07sec CBMC-SC: 0.33sec CImpact: 6.68sec ESBMC: 0.04sec Threader-monolithic: ERROR/TIMEOUT[1] 156.44sec Threader-owicki-gries: ERROR/TIMEOUT[1] 156.63sec Threader-rely-guarantee: ERROR/TIMEOUT[1] 155.64sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT MMChecker (MM: csharp): ERROR/TIMEOUT[2] 0.00sec |
Cycles
SatAbs: 1.95sec (x3.30) Satabs-prefix-first: 7.93sec CBMC-WMM: 0.06sec CBMC-SC: 0.32sec CImpact: 6.73sec ESBMC: 0.06sec Threader-monolithic: ERROR/TIMEOUT[1] 162.98sec Threader-owicki-gries: ERROR/TIMEOUT[1] 156.92sec Threader-rely-guarantee: ERROR/TIMEOUT[1] 155.69sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT Blender: |
Cycles
SatAbs: 1.77sec (x3.00) Satabs-prefix-first: 7.88sec CBMC-WMM: 0.07sec CBMC-SC: 0.31sec CImpact: 6.72sec ESBMC: 0.07sec Threader-monolithic: ERROR/TIMEOUT[1] 156.53sec Threader-owicki-gries: ERROR/TIMEOUT[1] 156.04sec Threader-rely-guarantee: ERROR/TIMEOUT[1] 157.50sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT Blender: |
Cycles
SatAbs: 2.07sec (x3.50) Satabs-prefix-first: 7.72sec CBMC-WMM: 0.07sec CBMC-SC: 0.34sec CImpact: 6.79sec ESBMC: 0.07sec Threader-monolithic: ERROR/TIMEOUT[1] 156.10sec Threader-owicki-gries: ERROR/TIMEOUT[1] 156.54sec Threader-rely-guarantee: ERROR/TIMEOUT[1] 155.45sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT Blender: |
Cycles
SatAbs: 2.00sec (x3.38) Satabs-prefix-first: 8.05sec CBMC-WMM: 0.08sec CBMC-SC: 0.32sec CImpact: 6.85sec ESBMC: 0.07sec Threader-monolithic: ERROR/TIMEOUT[1] 159.03sec Threader-owicki-gries: ERROR/TIMEOUT[1] 156.60sec Threader-rely-guarantee: ERROR/TIMEOUT[1] 157.74sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT |
Cycles
SatAbs: 2.91sec (x4.93) Satabs-prefix-first: 10.17sec CBMC-WMM: 0.12sec CBMC-SC: 0.32sec CImpact: 6.90sec ESBMC: 0.06sec Threader-monolithic: ERROR/TIMEOUT[1] 156.15sec Threader-owicki-gries: ERROR/TIMEOUT[1] 156.62sec Threader-rely-guarantee: ERROR/TIMEOUT[1] 157.43sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT |
Cycles
SatAbs: 1.51sec (x2.55) Satabs-prefix-first: 6.84sec CBMC-WMM: 0.08sec CBMC-SC: 0.33sec CImpact: 6.77sec ESBMC: 0.07sec Threader-monolithic: ERROR/TIMEOUT[1] 156.32sec Threader-owicki-gries: ERROR/TIMEOUT[1] 156.95sec Threader-rely-guarantee: ERROR/TIMEOUT[1] 155.90sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT |
Cycles
SatAbs: 1.48sec (x2.50) Satabs-prefix-first: 6.29sec CBMC-WMM: 0.08sec CBMC-SC: 0.35sec CImpact: 6.85sec ESBMC: 0.06sec Threader-monolithic: ERROR/TIMEOUT[1] 156.50sec Threader-owicki-gries: ERROR/TIMEOUT[1] 156.08sec Threader-rely-guarantee: ERROR/TIMEOUT[1] 156.16sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT |
Cycles
SatAbs: 1.38sec (x2.33) Satabs-prefix-first: 6.34sec CBMC-WMM: 0.08sec CBMC-SC: 0.33sec CImpact: 6.72sec ESBMC: 0.05sec Threader-monolithic: ERROR/TIMEOUT[1] 155.85sec Threader-owicki-gries: ERROR/TIMEOUT[1] 155.44sec Threader-rely-guarantee: ERROR/TIMEOUT[1] 156.34sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT |
Cycles
SatAbs: 1.59sec (x2.69) Satabs-prefix-first: 6.45sec CBMC-WMM: 0.07sec CBMC-SC: 0.34sec CImpact: 6.74sec ESBMC: 0.05sec Threader-monolithic: ERROR/TIMEOUT[1] 156.41sec Threader-owicki-gries: ERROR/TIMEOUT[1] 159.55sec Threader-rely-guarantee: ERROR/TIMEOUT[1] 165.57sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT |
||||
ppc/lwdwr019 |
SatAbs: 4.13sec Satabs-prefix-first: 1.53sec CBMC-WMM: 0.07sec CBMC-SC: 0.05sec CImpact: ERROR/TIMEOUT[8] 200.68sec Checkfence: 0.01sec ESBMC: 0.06sec Threader-monolithic: 0.09sec Threader-owicki-gries: 0.10sec Threader-rely-guarantee: 0.08sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT MMChecker (MM: sc): ERROR/TIMEOUT[2] 0.00sec |
Cycles
SatAbs: 59.03sec (x14.29) Satabs-prefix-first: 72.27sec CBMC-WMM: 0.12sec CBMC-SC: 14.54sec CImpact: ERROR/TIMEOUT[8] 292.90sec ESBMC: 0.09sec Threader-monolithic: ERROR/TIMEOUT[130] 897.21sec Threader-owicki-gries: ERROR/TIMEOUT[130] 897.23sec 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: 12.74sec (x3.08) Satabs-prefix-first: 12.31sec CBMC-WMM: 0.11sec CBMC-SC: 0.46sec CImpact: ERROR/TIMEOUT[8] 215.54sec Checkfence: 0.01sec ESBMC: 0.07sec Threader-monolithic: ERROR/TIMEOUT[1] 170.32sec Threader-owicki-gries: ERROR/TIMEOUT[1] 170.88sec Threader-rely-guarantee: ERROR/TIMEOUT[1] 170.17sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT MMChecker (MM: csharp): ERROR/TIMEOUT[2] 0.00sec |
Cycles
SatAbs: 12.92sec (x3.12) Satabs-prefix-first: 12.18sec CBMC-WMM: 0.12sec CBMC-SC: 0.45sec CImpact: ERROR/TIMEOUT[8] 215.69sec ESBMC: 0.07sec Threader-monolithic: ERROR/TIMEOUT[1] 170.77sec Threader-owicki-gries: ERROR/TIMEOUT[1] 170.04sec Threader-rely-guarantee: ERROR/TIMEOUT[1] 170.61sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT MMChecker (MM: csharp): ERROR/TIMEOUT[2] 0.01sec |
Cycles
SatAbs: 12.58sec (x3.04) Satabs-prefix-first: 12.76sec CBMC-WMM: 0.12sec CBMC-SC: 0.47sec CImpact: ERROR/TIMEOUT[8] 215.33sec ESBMC: 0.06sec Threader-monolithic: ERROR/TIMEOUT[1] 170.60sec Threader-owicki-gries: ERROR/TIMEOUT[1] 169.80sec Threader-rely-guarantee: ERROR/TIMEOUT[1] 185.57sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT MMChecker (MM: csharp): ERROR/TIMEOUT[2] 0.01sec |
Cycles
SatAbs: 12.28sec (x2.97) Satabs-prefix-first: 13.07sec CBMC-WMM: 0.11sec CBMC-SC: 0.47sec CImpact: ERROR/TIMEOUT[8] 214.69sec ESBMC: 0.06sec Threader-monolithic: ERROR/TIMEOUT[1] 174.76sec Threader-owicki-gries: ERROR/TIMEOUT[1] 170.96sec Threader-rely-guarantee: ERROR/TIMEOUT[1] 171.37sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT Blender: |
Cycles
SatAbs: 12.75sec (x3.08) Satabs-prefix-first: 12.75sec CBMC-WMM: 0.10sec CBMC-SC: 0.48sec CImpact: ERROR/TIMEOUT[8] 217.33sec ESBMC: 0.05sec Threader-monolithic: ERROR/TIMEOUT[1] 170.90sec Threader-owicki-gries: ERROR/TIMEOUT[1] 183.04sec Threader-rely-guarantee: ERROR/TIMEOUT[1] 170.32sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT Blender: |
Cycles
SatAbs: 13.20sec (x3.19) Satabs-prefix-first: 12.86sec CBMC-WMM: 0.11sec CBMC-SC: 0.48sec CImpact: ERROR/TIMEOUT[8] 214.56sec ESBMC: 0.07sec Threader-monolithic: ERROR/TIMEOUT[1] 171.02sec Threader-owicki-gries: ERROR/TIMEOUT[1] 170.41sec Threader-rely-guarantee: ERROR/TIMEOUT[1] 170.17sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT Blender: |
Cycles
SatAbs: 12.93sec (x3.13) Satabs-prefix-first: 13.28sec CBMC-WMM: 0.11sec CBMC-SC: 0.49sec CImpact: ERROR/TIMEOUT[8] 217.85sec ESBMC: 0.05sec Threader-monolithic: ERROR/TIMEOUT[1] 171.13sec Threader-owicki-gries: ERROR/TIMEOUT[1] 171.18sec Threader-rely-guarantee: ERROR/TIMEOUT[1] 170.28sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT |
Cycles
SatAbs: 13.35sec (x3.23) Satabs-prefix-first: 13.27sec CBMC-WMM: 0.12sec CBMC-SC: 0.48sec CImpact: ERROR/TIMEOUT[8] 215.71sec ESBMC: 0.05sec Threader-monolithic: ERROR/TIMEOUT[1] 170.53sec Threader-owicki-gries: ERROR/TIMEOUT[1] 171.27sec Threader-rely-guarantee: ERROR/TIMEOUT[1] 171.79sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT |
Cycles
SatAbs: 13.68sec (x3.31) Satabs-prefix-first: 14.00sec CBMC-WMM: 0.12sec CBMC-SC: 0.47sec CImpact: ERROR/TIMEOUT[8] 243.63sec ESBMC: 0.06sec Threader-monolithic: ERROR/TIMEOUT[1] 170.44sec Threader-owicki-gries: ERROR/TIMEOUT[1] 176.92sec Threader-rely-guarantee: ERROR/TIMEOUT[1] 171.10sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT |
Cycles
SatAbs: 12.88sec (x3.11) Satabs-prefix-first: 12.75sec CBMC-WMM: 0.12sec CBMC-SC: 0.48sec CImpact: ERROR/TIMEOUT[8] 214.66sec ESBMC: 0.07sec Threader-monolithic: ERROR/TIMEOUT[1] 170.44sec Threader-owicki-gries: ERROR/TIMEOUT[1] 170.66sec Threader-rely-guarantee: ERROR/TIMEOUT[1] 172.27sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT |
Cycles
SatAbs: 12.99sec (x3.14) Satabs-prefix-first: 13.07sec CBMC-WMM: 0.11sec CBMC-SC: 0.47sec CImpact: ERROR/TIMEOUT[8] 215.44sec ESBMC: 0.07sec Threader-monolithic: ERROR/TIMEOUT[1] 170.48sec Threader-owicki-gries: ERROR/TIMEOUT[1] 171.86sec Threader-rely-guarantee: ERROR/TIMEOUT[1] 170.76sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT |
Cycles
SatAbs: 12.48sec (x3.02) Satabs-prefix-first: 12.82sec CBMC-WMM: 0.13sec CBMC-SC: 0.48sec CImpact: ERROR/TIMEOUT[8] 243.17sec ESBMC: 0.10sec Threader-monolithic: ERROR/TIMEOUT[1] 183.38sec Threader-owicki-gries: ERROR/TIMEOUT[1] 185.12sec Threader-rely-guarantee: ERROR/TIMEOUT[1] 178.07sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT |
||||
ppc/lwdwr020 |
SatAbs: 3.61sec Satabs-prefix-first: 3.90sec CBMC-WMM: 0.06sec CBMC-SC: 0.06sec CImpact: ERROR/TIMEOUT[8] 237.16sec Checkfence: 0.01sec ESBMC: 0.07sec Threader-monolithic: 0.10sec Threader-owicki-gries: 0.11sec Threader-rely-guarantee: 0.10sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT MMChecker (MM: sc): ERROR/TIMEOUT[2] 0.00sec |
Cycles
SatAbs: 11.71sec (x3.24) Satabs-prefix-first: 6.05sec CBMC-WMM: 0.11sec CBMC-SC: 89.06sec CImpact: ERROR/TIMEOUT[8] 307.34sec ESBMC: 0.09sec Threader-monolithic: ERROR/TIMEOUT[130] 897.39sec Threader-owicki-gries: ERROR/TIMEOUT[130] 897.33sec Threader-rely-guarantee: ERROR/TIMEOUT[130] 896.80sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT MMChecker (MM: csharp): ERROR/TIMEOUT[2] 0.00sec |
Cycles
SatAbs: 6.24sec (x1.72) Satabs-prefix-first: 16.06sec CBMC-WMM: 0.10sec CBMC-SC: 0.46sec CImpact: ERROR/TIMEOUT[8] 256.31sec Checkfence: 0.01sec ESBMC: 0.06sec Threader-monolithic: ERROR/TIMEOUT[1] 175.16sec Threader-owicki-gries: ERROR/TIMEOUT[1] 174.11sec Threader-rely-guarantee: ERROR/TIMEOUT[1] 177.47sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT MMChecker (MM: csharp): ERROR/TIMEOUT[2] 0.00sec |
Cycles
SatAbs: 5.41sec (x1.49) Satabs-prefix-first: 13.46sec CBMC-WMM: 0.12sec CBMC-SC: 0.43sec CImpact: ERROR/TIMEOUT[8] 256.54sec ESBMC: 0.06sec Threader-monolithic: ERROR/TIMEOUT[1] 173.57sec Threader-owicki-gries: ERROR/TIMEOUT[1] 172.94sec Threader-rely-guarantee: ERROR/TIMEOUT[1] 176.81sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT MMChecker (MM: csharp): ERROR/TIMEOUT[2] 0.00sec |
Cycles
SatAbs: 6.04sec (x1.67) Satabs-prefix-first: 14.32sec CBMC-WMM: 0.12sec CBMC-SC: 0.45sec CImpact: ERROR/TIMEOUT[8] 256.13sec ESBMC: 0.07sec Threader-monolithic: ERROR/TIMEOUT[1] 174.62sec Threader-owicki-gries: ERROR/TIMEOUT[1] 174.22sec Threader-rely-guarantee: ERROR/TIMEOUT[1] 176.07sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT MMChecker (MM: csharp): ERROR/TIMEOUT[2] 0.00sec |
Cycles
SatAbs: 4.45sec (x1.23) Satabs-prefix-first: 11.60sec CBMC-WMM: 0.12sec CBMC-SC: 0.44sec CImpact: ERROR/TIMEOUT[8] 258.61sec ESBMC: 0.08sec Threader-monolithic: ERROR/TIMEOUT[1] 173.26sec Threader-owicki-gries: ERROR/TIMEOUT[1] 174.27sec Threader-rely-guarantee: ERROR/TIMEOUT[1] 173.88sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT Blender: |
Cycles
SatAbs: 4.51sec (x1.24) Satabs-prefix-first: 13.05sec CBMC-WMM: 0.11sec CBMC-SC: 0.45sec CImpact: ERROR/TIMEOUT[8] 252.67sec ESBMC: 0.08sec Threader-monolithic: ERROR/TIMEOUT[1] 173.51sec Threader-owicki-gries: ERROR/TIMEOUT[1] 172.84sec Threader-rely-guarantee: ERROR/TIMEOUT[1] 173.23sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT Blender: |
Cycles
SatAbs: 5.02sec (x1.39) Satabs-prefix-first: 12.86sec CBMC-WMM: 0.12sec CBMC-SC: 0.45sec CImpact: ERROR/TIMEOUT[8] 257.93sec ESBMC: 0.08sec Threader-monolithic: ERROR/TIMEOUT[1] 172.68sec Threader-owicki-gries: ERROR/TIMEOUT[1] 174.38sec Threader-rely-guarantee: ERROR/TIMEOUT[1] 174.11sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT Blender: |
Cycles
SatAbs: 5.20sec (x1.44) Satabs-prefix-first: 13.63sec CBMC-WMM: 0.11sec CBMC-SC: 0.44sec CImpact: ERROR/TIMEOUT[8] 256.39sec ESBMC: 0.07sec Threader-monolithic: ERROR/TIMEOUT[1] 173.34sec Threader-owicki-gries: ERROR/TIMEOUT[1] 173.47sec Threader-rely-guarantee: ERROR/TIMEOUT[1] 173.79sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT |
Cycles
SatAbs: 6.57sec (x1.81) Satabs-prefix-first: 17.04sec CBMC-WMM: 0.16sec CBMC-SC: 0.47sec CImpact: ERROR/TIMEOUT[8] 256.80sec ESBMC: 0.07sec Threader-monolithic: ERROR/TIMEOUT[1] 173.82sec Threader-owicki-gries: ERROR/TIMEOUT[1] 174.25sec Threader-rely-guarantee: ERROR/TIMEOUT[1] 176.08sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT |
Cycles
SatAbs: 4.50sec (x1.24) Satabs-prefix-first: 11.17sec CBMC-WMM: 0.12sec CBMC-SC: 0.45sec CImpact: ERROR/TIMEOUT[8] 275.81sec ESBMC: 0.10sec Threader-monolithic: ERROR/TIMEOUT[1] 184.72sec Threader-owicki-gries: ERROR/TIMEOUT[1] 173.87sec Threader-rely-guarantee: ERROR/TIMEOUT[1] 173.40sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT |
Cycles
SatAbs: 79.37sec (x21.98) Satabs-prefix-first: 103.92sec CBMC-WMM: 0.11sec CBMC-SC: 225.28sec CImpact: ERROR/TIMEOUT[8] 332.30sec ESBMC: 0.10sec Threader-monolithic: ERROR/TIMEOUT[130] 897.53sec Threader-owicki-gries: ERROR/TIMEOUT[130] 897.64sec Threader-rely-guarantee: ERROR/TIMEOUT[130] 897.57sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT |
Cycles
SatAbs: 4.35sec (x1.20) Satabs-prefix-first: 11.58sec CBMC-WMM: 0.14sec CBMC-SC: 0.45sec CImpact: ERROR/TIMEOUT[8] 261.93sec ESBMC: 0.07sec Threader-monolithic: ERROR/TIMEOUT[1] 174.05sec Threader-owicki-gries: ERROR/TIMEOUT[1] 173.49sec Threader-rely-guarantee: ERROR/TIMEOUT[1] 173.65sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT |
Cycles
SatAbs: 4.54sec (x1.25) Satabs-prefix-first: 11.41sec CBMC-WMM: 0.14sec CBMC-SC: 0.43sec CImpact: ERROR/TIMEOUT[8] 255.54sec ESBMC: 0.08sec Threader-monolithic: ERROR/TIMEOUT[1] 172.59sec Threader-owicki-gries: ERROR/TIMEOUT[1] 173.16sec Threader-rely-guarantee: ERROR/TIMEOUT[1] 175.01sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT |
||||
ppc/lwdwr021 |
SatAbs: 2.50sec Satabs-prefix-first: 3.54sec CBMC-WMM: 0.08sec CBMC-SC: 0.07sec CImpact: ERROR/TIMEOUT[8] 204.21sec Checkfence: 0.01sec ESBMC: 0.07sec Threader-monolithic: 0.11sec Threader-owicki-gries: 0.11sec Threader-rely-guarantee: 0.11sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT MMChecker (MM: sc): ERROR/TIMEOUT[2] 0.00sec |
Cycles
SatAbs: 18.85sec (x7.54) Satabs-prefix-first: 58.82sec CBMC-WMM: 0.11sec CBMC-SC: 30.37sec CImpact: 6.67sec ESBMC: 0.09sec Threader-monolithic: ERROR/TIMEOUT[130] 897.42sec Threader-owicki-gries: ERROR/TIMEOUT[130] 897.40sec Threader-rely-guarantee: ERROR/TIMEOUT[130] 897.27sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT MMChecker (MM: csharp): ERROR/TIMEOUT[2] 0.00sec |
Cycles
SatAbs: 206.40sec (x82.56) Satabs-prefix-first: 541.02sec CBMC-WMM: 0.10sec CBMC-SC: 4.49sec CImpact: ERROR/TIMEOUT[8] 245.24sec Checkfence: 0.01sec ESBMC: 0.08sec Threader-monolithic: ERROR/TIMEOUT[130] 897.25sec Threader-owicki-gries: ERROR/TIMEOUT[130] 897.44sec Threader-rely-guarantee: ERROR/TIMEOUT[130] 897.31sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT MMChecker (MM: csharp): ERROR/TIMEOUT[2] 0.00sec |
Cycles
SatAbs: 197.79sec (x79.11) Satabs-prefix-first: 507.41sec CBMC-WMM: 0.12sec CBMC-SC: 4.46sec CImpact: ERROR/TIMEOUT[8] 242.50sec ESBMC: 0.08sec Threader-monolithic: ERROR/TIMEOUT[130] 897.34sec Threader-owicki-gries: ERROR/TIMEOUT[130] 897.29sec Threader-rely-guarantee: ERROR/TIMEOUT[130] 897.44sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT MMChecker (MM: csharp): ERROR/TIMEOUT[2] 0.00sec |
Cycles
SatAbs: 198.97sec (x79.58) Satabs-prefix-first: 502.04sec CBMC-WMM: 0.12sec CBMC-SC: 4.47sec CImpact: ERROR/TIMEOUT[8] 242.10sec ESBMC: 0.06sec Threader-monolithic: ERROR/TIMEOUT[130] 897.42sec Threader-owicki-gries: ERROR/TIMEOUT[130] 897.34sec Threader-rely-guarantee: ERROR/TIMEOUT[130] 897.46sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT MMChecker (MM: csharp): ERROR/TIMEOUT[2] 0.00sec |
Cycles
SatAbs: 198.80sec (x79.52) Satabs-prefix-first: 503.75sec CBMC-WMM: 0.12sec CBMC-SC: 4.48sec CImpact: ERROR/TIMEOUT[8] 243.17sec ESBMC: 0.08sec Threader-monolithic: ERROR/TIMEOUT[130] 897.42sec Threader-owicki-gries: ERROR/TIMEOUT[130] 897.36sec Threader-rely-guarantee: ERROR/TIMEOUT[130] 897.37sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT Blender: |
Cycles
SatAbs: 197.85sec (x79.14) Satabs-prefix-first: 502.90sec CBMC-WMM: 0.12sec CBMC-SC: 4.43sec CImpact: ERROR/TIMEOUT[8] 242.03sec ESBMC: 0.07sec Threader-monolithic: ERROR/TIMEOUT[130] 897.27sec Threader-owicki-gries: ERROR/TIMEOUT[130] 897.43sec Threader-rely-guarantee: ERROR/TIMEOUT[130] 897.49sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT Blender: |
Cycles
SatAbs: 200.38sec (x80.15) Satabs-prefix-first: 512.50sec CBMC-WMM: 0.08sec CBMC-SC: 4.45sec CImpact: ERROR/TIMEOUT[8] 243.42sec ESBMC: 0.06sec Threader-monolithic: ERROR/TIMEOUT[130] 897.38sec Threader-owicki-gries: ERROR/TIMEOUT[130] 895.55sec Threader-rely-guarantee: ERROR/TIMEOUT[130] 897.44sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT Blender: |
Cycles
SatAbs: 213.75sec (x85.50) Satabs-prefix-first: 514.94sec CBMC-WMM: 0.12sec CBMC-SC: 4.49sec CImpact: ERROR/TIMEOUT[8] 246.55sec ESBMC: 0.05sec Threader-monolithic: ERROR/TIMEOUT[130] 897.42sec Threader-owicki-gries: ERROR/TIMEOUT[130] 897.49sec Threader-rely-guarantee: ERROR/TIMEOUT[130] 897.29sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT |
Cycles
SatAbs: 201.43sec (x80.57) Satabs-prefix-first: 508.33sec CBMC-WMM: 0.11sec CBMC-SC: 4.47sec CImpact: ERROR/TIMEOUT[8] 242.60sec ESBMC: 0.06sec Threader-monolithic: ERROR/TIMEOUT[130] 897.22sec Threader-owicki-gries: ERROR/TIMEOUT[130] 897.23sec Threader-rely-guarantee: ERROR/TIMEOUT[130] 897.48sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT |
Cycles
SatAbs: 200.52sec (x80.20) Satabs-prefix-first: 505.86sec CBMC-WMM: 0.13sec CBMC-SC: 4.54sec CImpact: ERROR/TIMEOUT[8] 244.56sec ESBMC: 0.08sec Threader-monolithic: ERROR/TIMEOUT[130] 897.34sec Threader-owicki-gries: ERROR/TIMEOUT[130] 897.43sec Threader-rely-guarantee: ERROR/TIMEOUT[130] 897.45sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT |
Cycles
SatAbs: 23.92sec (x9.56) Satabs-prefix-first: 18.96sec CBMC-WMM: 0.13sec CBMC-SC: 42.62sec CImpact: 5.09sec ESBMC: 0.07sec Threader-monolithic: ERROR/TIMEOUT[130] 897.37sec Threader-owicki-gries: ERROR/TIMEOUT[130] 897.23sec Threader-rely-guarantee: ERROR/TIMEOUT[130] 896.19sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT |
Cycles
SatAbs: 251.84sec (x100.73) Satabs-prefix-first: 644.15sec CBMC-WMM: 0.20sec CBMC-SC: 6.86sec CImpact: ERROR/TIMEOUT[8] 296.93sec ESBMC: 0.12sec Threader-monolithic: ERROR/TIMEOUT[130] 897.22sec Threader-owicki-gries: ERROR/TIMEOUT[130] 897.19sec Threader-rely-guarantee: ERROR/TIMEOUT[130] 897.33sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT |
Cycles
SatAbs: 197.47sec (x78.98) Satabs-prefix-first: 509.17sec CBMC-WMM: 0.12sec CBMC-SC: 4.42sec CImpact: ERROR/TIMEOUT[8] 243.11sec ESBMC: 0.08sec Threader-monolithic: ERROR/TIMEOUT[130] 897.38sec Threader-owicki-gries: ERROR/TIMEOUT[130] 897.27sec Threader-rely-guarantee: ERROR/TIMEOUT[130] 897.17sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT |