How to read the tables?
Meaning of the model-checker's resultsModel-checker on the instrumented program | Observed state in Litmus | Picture |
VERIFICATION FAILED | YES | ![]() |
VERIFICATION SUCCESSFUL | NO | ![]() |
Reading the results in the experiments tables
The table below is an excerpt of former results we obtained for x86/podwr experiments.
- In the first column, we can read the name of the original Litmus test (with a link to the file), and the expected violation cycle. The second column gathers the results of the model-checkers for SC. As we are interested in WMM bugs, the verification for SC should be
.
- The three next columns concern TSO model. The last column tells which result we should get for this program under TSO, namely
. We see in the third column that Satabs indeed finds the correct result when checking the instrumented program. ESBMC in this example is missing the counterexample. Threader is either returning an error, or killed by timeout (here, it is an error).
- Note that there are two columns for TSO results: in the first one, we instrument all the delays; in the second one, we instrument only one delay per cycle.
- We also experiment under PSO, RMO and Power, and with additional model-checkers: additional columns of results (and expected results) appear after TSO's columns.
Name | SC | TSO (all delay/cyc) | TSO (1 delay/cyc) | Expected (TSO) | ... |
x86/podwr000 Fre PodWR Fre PodWR |
SatAbs: ![]() 0.60sec ESBMC: ![]() Threader: ![]() ... |
Cycles SatAbs: ![]() 3.94sec (x6.56) ESBMC: ![]() Threader: ERROR/TIMEOUT[1] 491.99sec ... |
Cycles SatAbs: ![]() 2.43sec (x4.05) ESBMC: ![]() Threader: ERROR/TIMEOUT[1] 182.60sec ... |
![]() |
... |
ppc/bclwdww (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 a B-cumulative ordering when placed between two writes. Therefore they should answer Yes in litmus terms, or Verification Failed in verification terms as soon as the model is Power.
Name | SC | CAV'11 | TSO (all delay/cyc) | TSO (1 delay/cyc) | TSO (opt delay/cyc) | Expected (TSO) | PSO (all delay/cyc) | PSO (1 delay/cyc) | PSO (opt delay/cyc) | Expected (PSO) | RMO (all delay/cyc) | RMO (1 delay/cyc) | RMO (opt delay/cyc) | Expected (RMO) | Power (all delay/cyc) | Power (1 delay/cyc) | Power (opt delay/cyc) | Expected (Power) |
ppc/bclwdww000 |
SatAbs: ![]() 1.81sec Satabs-prefix-first: ![]() CBMC-WMM: ![]() CBMC-SC: ![]() CImpact: ![]() Checkfence: 0.01sec ESBMC: ![]() Threader-monolithic: ![]() Threader-owicki-gries: ![]() Threader-rely-guarantee: ![]() Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT MMChecker (MM: sc): ERROR/TIMEOUT[1] 0.09sec |
Cycles
SatAbs: ![]() 6.86sec (x3.79) Satabs-prefix-first: ![]() CBMC-WMM: ![]() CBMC-SC: ![]() CImpact: ![]() ESBMC: ![]() Threader-monolithic: ERROR/TIMEOUT[130] 897.17sec Threader-owicki-gries: ERROR/TIMEOUT[130] 897.07sec Threader-rely-guarantee: ERROR/TIMEOUT[130] 897.56sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT MMChecker (MM: csharp): ERROR/TIMEOUT[1] 0.10sec |
Cycles
SatAbs: ![]() 1.01sec (x.55) Satabs-prefix-first: ![]() CBMC-WMM: ![]() CBMC-SC: ![]() CImpact: ![]() Checkfence: 0.01sec ESBMC: ![]() Threader-monolithic: ERROR/TIMEOUT[1] 0.11sec Threader-owicki-gries: ERROR/TIMEOUT[1] 0.11sec Threader-rely-guarantee: ERROR/TIMEOUT[1] 0.11sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT MMChecker (MM: csharp): ERROR/TIMEOUT[1] 0.09sec |
Cycles
SatAbs: ![]() 1.14sec (x.62) Satabs-prefix-first: ![]() CBMC-WMM: ![]() CBMC-SC: ![]() CImpact: ![]() ESBMC: ![]() Threader-monolithic: ERROR/TIMEOUT[1] 0.07sec Threader-owicki-gries: ERROR/TIMEOUT[1] 0.11sec Threader-rely-guarantee: ERROR/TIMEOUT[1] 0.11sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT MMChecker (MM: csharp): ERROR/TIMEOUT[1] 0.09sec |
Cycles
SatAbs: ![]() 1.17sec (x.64) Satabs-prefix-first: ![]() CBMC-WMM: ![]() CBMC-SC: ![]() CImpact: ![]() ESBMC: ![]() Threader-monolithic: ERROR/TIMEOUT[1] 0.11sec Threader-owicki-gries: ERROR/TIMEOUT[1] 0.12sec Threader-rely-guarantee: ERROR/TIMEOUT[1] 0.07sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT MMChecker (MM: csharp): ERROR/TIMEOUT[1] 0.10sec |
![]() |
Cycles
SatAbs: ![]() 1.12sec (x.61) Satabs-prefix-first: ![]() CBMC-WMM: ![]() CBMC-SC: ![]() CImpact: ![]() ESBMC: ![]() Threader-monolithic: ERROR/TIMEOUT[1] 0.12sec Threader-owicki-gries: ERROR/TIMEOUT[1] 0.10sec Threader-rely-guarantee: ERROR/TIMEOUT[1] 0.10sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT Blender: ![]() |
Cycles
SatAbs: ![]() 1.08sec (x.59) Satabs-prefix-first: ![]() CBMC-WMM: ![]() CBMC-SC: ![]() CImpact: ![]() ESBMC: ![]() Threader-monolithic: ERROR/TIMEOUT[1] 0.08sec Threader-owicki-gries: ERROR/TIMEOUT[1] 0.09sec Threader-rely-guarantee: ERROR/TIMEOUT[1] 0.11sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT Blender: ![]() |
Cycles
SatAbs: ![]() 1.14sec (x.62) Satabs-prefix-first: ![]() CBMC-WMM: ![]() CBMC-SC: ![]() CImpact: ![]() ESBMC: ![]() Threader-monolithic: ERROR/TIMEOUT[1] 0.11sec Threader-owicki-gries: ERROR/TIMEOUT[1] 0.11sec Threader-rely-guarantee: ERROR/TIMEOUT[1] 0.11sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT Blender: ![]() |
![]() |
Cycles
SatAbs: ![]() 0.93sec (x.51) Satabs-prefix-first: ![]() CBMC-WMM: ![]() CBMC-SC: ![]() CImpact: ![]() ESBMC: ![]() Threader-monolithic: ERROR/TIMEOUT[1] 0.09sec Threader-owicki-gries: ERROR/TIMEOUT[1] 0.07sec Threader-rely-guarantee: ERROR/TIMEOUT[1] 0.10sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT |
Cycles
SatAbs: ![]() 1.16sec (x.64) Satabs-prefix-first: ![]() CBMC-WMM: ![]() CBMC-SC: ![]() CImpact: ![]() ESBMC: ![]() Threader-monolithic: ERROR/TIMEOUT[1] 0.09sec Threader-owicki-gries: ERROR/TIMEOUT[1] 0.10sec Threader-rely-guarantee: ERROR/TIMEOUT[1] 0.11sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT |
Cycles
SatAbs: ![]() 1.11sec (x.61) Satabs-prefix-first: ![]() CBMC-WMM: ![]() CBMC-SC: ![]() CImpact: ![]() ESBMC: ![]() Threader-monolithic: ERROR/TIMEOUT[1] 0.11sec Threader-owicki-gries: ERROR/TIMEOUT[1] 0.11sec Threader-rely-guarantee: ERROR/TIMEOUT[1] 0.11sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT |
![]() |
Cycles
SatAbs: ![]() 86.10sec (x47.56) Satabs-prefix-first: ![]() CBMC-WMM: ![]() CBMC-SC: ![]() CImpact: ![]() ESBMC: ![]() Threader-monolithic: ERROR/TIMEOUT[130] 897.29sec Threader-owicki-gries: ERROR/TIMEOUT[130] 897.75sec Threader-rely-guarantee: ERROR/TIMEOUT[130] 897.42sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT |
Cycles
SatAbs: ![]() 7.70sec (x4.25) Satabs-prefix-first: ![]() CBMC-WMM: ![]() CBMC-SC: ![]() CImpact: ![]() ESBMC: ![]() Threader-monolithic: ERROR/TIMEOUT[1] 375.89sec Threader-owicki-gries: ERROR/TIMEOUT[1] 334.47sec Threader-rely-guarantee: ERROR/TIMEOUT[1] 377.54sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT |
Cycles
SatAbs: ![]() 7.47sec (x4.12) Satabs-prefix-first: ![]() CBMC-WMM: ![]() CBMC-SC: ![]() CImpact: ![]() ESBMC: ![]() Threader-monolithic: ERROR/TIMEOUT[1] 377.03sec Threader-owicki-gries: ERROR/TIMEOUT[1] 289.45sec Threader-rely-guarantee: ERROR/TIMEOUT[1] 312.52sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT |
![]() |
ppc/bclwdww001 |
SatAbs: ![]() 4.69sec Satabs-prefix-first: ![]() CBMC-WMM: ![]() CBMC-SC: ![]() CImpact: ERROR/TIMEOUT[8] 291.18sec Checkfence: 0.01sec ESBMC: ![]() Threader-monolithic: ![]() Threader-owicki-gries: ![]() Threader-rely-guarantee: ![]() Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT MMChecker (MM: sc): ERROR/TIMEOUT[1] 0.10sec |
Cycles
SatAbs: ![]() 5.05sec (x1.07) Satabs-prefix-first: ![]() CBMC-WMM: ![]() CBMC-SC: ![]() CImpact: ![]() ESBMC: ![]() Threader-monolithic: ERROR/TIMEOUT[130] 897.67sec Threader-owicki-gries: ERROR/TIMEOUT[130] 897.67sec Threader-rely-guarantee: ERROR/TIMEOUT[130] 897.44sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT MMChecker (MM: csharp): ERROR/TIMEOUT[1] 0.10sec |
Cycles
SatAbs: ![]() 3.28sec (x.69) Satabs-prefix-first: ![]() CBMC-WMM: ![]() CBMC-SC: ![]() CImpact: ERROR/TIMEOUT[8] 264.60sec Checkfence: 0.01sec ESBMC: ![]() Threader-monolithic: ERROR/TIMEOUT[1] 0.10sec Threader-owicki-gries: ERROR/TIMEOUT[1] 0.11sec Threader-rely-guarantee: ERROR/TIMEOUT[1] 0.10sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT MMChecker (MM: csharp): ERROR/TIMEOUT[1] 0.11sec |
Cycles
SatAbs: ![]() 4.37sec (x.93) Satabs-prefix-first: ![]() CBMC-WMM: ![]() CBMC-SC: ![]() CImpact: ERROR/TIMEOUT[8] 327.95sec ESBMC: ![]() Threader-monolithic: ERROR/TIMEOUT[1] 0.10sec Threader-owicki-gries: ERROR/TIMEOUT[1] 0.12sec Threader-rely-guarantee: ERROR/TIMEOUT[1] 0.13sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT MMChecker (MM: csharp): ERROR/TIMEOUT[1] 0.09sec |
Cycles
SatAbs: ![]() 3.29sec (x.70) Satabs-prefix-first: ![]() CBMC-WMM: ![]() CBMC-SC: ![]() CImpact: ERROR/TIMEOUT[8] 283.94sec ESBMC: ![]() Threader-monolithic: ERROR/TIMEOUT[1] 0.12sec Threader-owicki-gries: ERROR/TIMEOUT[1] 0.11sec Threader-rely-guarantee: ERROR/TIMEOUT[1] 0.13sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT MMChecker (MM: csharp): ERROR/TIMEOUT[1] 0.10sec |
![]() |
Cycles
SatAbs: ![]() 3.46sec (x.73) Satabs-prefix-first: ![]() CBMC-WMM: ![]() CBMC-SC: ![]() CImpact: ERROR/TIMEOUT[8] 321.06sec ESBMC: ![]() Threader-monolithic: ERROR/TIMEOUT[1] 0.12sec Threader-owicki-gries: ERROR/TIMEOUT[1] 0.10sec Threader-rely-guarantee: ERROR/TIMEOUT[1] 0.11sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT Blender: ![]() |
Cycles
SatAbs: ![]() 2.96sec (x.63) Satabs-prefix-first: ![]() CBMC-WMM: ![]() CBMC-SC: ![]() CImpact: ERROR/TIMEOUT[8] 325.97sec ESBMC: ![]() Threader-monolithic: ERROR/TIMEOUT[1] 0.11sec Threader-owicki-gries: ERROR/TIMEOUT[1] 0.11sec Threader-rely-guarantee: ERROR/TIMEOUT[1] 0.10sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT Blender: ![]() |
Cycles
SatAbs: ![]() 3.35sec (x.71) Satabs-prefix-first: ![]() CBMC-WMM: ![]() CBMC-SC: ![]() CImpact: ERROR/TIMEOUT[8] 305.36sec ESBMC: ![]() Threader-monolithic: ERROR/TIMEOUT[1] 0.09sec Threader-owicki-gries: ERROR/TIMEOUT[1] 0.09sec Threader-rely-guarantee: ERROR/TIMEOUT[1] 0.12sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT Blender: ![]() |
![]() |
Cycles
SatAbs: ![]() 2.98sec (x.63) Satabs-prefix-first: ![]() CBMC-WMM: ![]() CBMC-SC: ![]() CImpact: ERROR/TIMEOUT[8] 313.40sec ESBMC: ![]() Threader-monolithic: ERROR/TIMEOUT[1] 0.11sec Threader-owicki-gries: ERROR/TIMEOUT[1] 0.08sec Threader-rely-guarantee: ERROR/TIMEOUT[1] 0.11sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT |
Cycles
SatAbs: ![]() 3.26sec (x.69) Satabs-prefix-first: ![]() CBMC-WMM: ![]() CBMC-SC: ![]() CImpact: ERROR/TIMEOUT[8] 343.03sec ESBMC: ![]() Threader-monolithic: ERROR/TIMEOUT[1] 0.10sec Threader-owicki-gries: ERROR/TIMEOUT[1] 0.11sec Threader-rely-guarantee: ERROR/TIMEOUT[1] 0.09sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT |
Cycles
SatAbs: ![]() 3.17sec (x.67) Satabs-prefix-first: ![]() CBMC-WMM: ![]() CBMC-SC: ![]() CImpact: ERROR/TIMEOUT[8] 330.63sec ESBMC: ![]() Threader-monolithic: ERROR/TIMEOUT[1] 0.12sec Threader-owicki-gries: ERROR/TIMEOUT[1] 0.11sec Threader-rely-guarantee: ERROR/TIMEOUT[1] 0.12sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT |
![]() |
Cycles
SatAbs: ERROR/TIMEOUT[130] 1127.12sec (x240.32) Satabs-prefix-first: ![]() CBMC-WMM: ![]() CBMC-SC: ![]() CImpact: ![]() ESBMC: ![]() Threader-monolithic: ERROR/TIMEOUT[130] 897.42sec Threader-owicki-gries: ERROR/TIMEOUT[130] 897.65sec Threader-rely-guarantee: ERROR/TIMEOUT[130] 897.65sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT |
Cycles
SatAbs: ![]() 48.62sec (x10.36) Satabs-prefix-first: ![]() CBMC-WMM: ![]() CBMC-SC: ![]() CImpact: ![]() ESBMC: ![]() Threader-monolithic: ERROR/TIMEOUT[1] 410.30sec Threader-owicki-gries: ERROR/TIMEOUT[1] 408.43sec Threader-rely-guarantee: ERROR/TIMEOUT[1] 309.90sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT |
Cycles
SatAbs: ![]() 46.44sec (x9.90) Satabs-prefix-first: ![]() CBMC-WMM: ![]() CBMC-SC: ![]() CImpact: ![]() ESBMC: ![]() Threader-monolithic: ERROR/TIMEOUT[1] 366.21sec Threader-owicki-gries: ERROR/TIMEOUT[1] 395.13sec Threader-rely-guarantee: ERROR/TIMEOUT[1] 365.01sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT |
![]() |
ppc/bclwdww002 |
SatAbs: ![]() 0.73sec Satabs-prefix-first: ![]() CBMC-WMM: ![]() CBMC-SC: ![]() CImpact: ERROR/TIMEOUT[8] 279.06sec Checkfence: 0.01sec ESBMC: ![]() Threader-monolithic: ![]() Threader-owicki-gries: ![]() Threader-rely-guarantee: ![]() Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT MMChecker (MM: sc): ![]() |
Cycles
SatAbs: ![]() 5.12sec (x7.01) Satabs-prefix-first: ![]() CBMC-WMM: ![]() CBMC-SC: ![]() CImpact: ![]() ESBMC: ![]() Threader-monolithic: ERROR/TIMEOUT[130] 897.27sec Threader-owicki-gries: ERROR/TIMEOUT[130] 897.54sec Threader-rely-guarantee: ERROR/TIMEOUT[130] 897.60sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT MMChecker (MM: csharp): ![]() |
Cycles
SatAbs: ![]() 4.33sec (x5.93) Satabs-prefix-first: ![]() CBMC-WMM: ![]() CBMC-SC: ![]() CImpact: ERROR/TIMEOUT[8] 236.11sec Checkfence: 0.01sec ESBMC: ![]() Threader-monolithic: ERROR/TIMEOUT[1] 0.09sec Threader-owicki-gries: ERROR/TIMEOUT[1] 0.12sec Threader-rely-guarantee: ERROR/TIMEOUT[1] 0.11sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT MMChecker (MM: csharp): ![]() |
Cycles
SatAbs: ![]() 4.79sec (x6.56) Satabs-prefix-first: ![]() CBMC-WMM: ![]() CBMC-SC: ![]() CImpact: ERROR/TIMEOUT[8] 278.71sec ESBMC: ![]() Threader-monolithic: ERROR/TIMEOUT[1] 0.12sec Threader-owicki-gries: ERROR/TIMEOUT[1] 0.12sec Threader-rely-guarantee: ERROR/TIMEOUT[1] 0.11sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT MMChecker (MM: csharp): ![]() |
Cycles
SatAbs: ![]() 4.31sec (x5.90) Satabs-prefix-first: ![]() CBMC-WMM: ![]() CBMC-SC: ![]() CImpact: ERROR/TIMEOUT[8] 316.25sec ESBMC: ![]() Threader-monolithic: ERROR/TIMEOUT[1] 0.10sec Threader-owicki-gries: ERROR/TIMEOUT[1] 0.10sec Threader-rely-guarantee: ERROR/TIMEOUT[1] 0.11sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT MMChecker (MM: csharp): ![]() |
![]() |
Cycles
SatAbs: ![]() 4.44sec (x6.08) Satabs-prefix-first: ![]() CBMC-WMM: ![]() CBMC-SC: ![]() CImpact: ERROR/TIMEOUT[8] 238.61sec ESBMC: ![]() Threader-monolithic: ERROR/TIMEOUT[1] 0.10sec Threader-owicki-gries: ERROR/TIMEOUT[1] 0.11sec Threader-rely-guarantee: ERROR/TIMEOUT[1] 0.11sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT Blender: ![]() |
Cycles
SatAbs: ![]() 4.31sec (x5.90) Satabs-prefix-first: ![]() CBMC-WMM: ![]() CBMC-SC: ![]() CImpact: ERROR/TIMEOUT[8] 252.23sec ESBMC: ![]() Threader-monolithic: ERROR/TIMEOUT[1] 0.09sec Threader-owicki-gries: ERROR/TIMEOUT[1] 0.12sec Threader-rely-guarantee: ERROR/TIMEOUT[1] 0.11sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT Blender: ![]() |
Cycles
SatAbs: ![]() 4.14sec (x5.67) Satabs-prefix-first: ![]() CBMC-WMM: ![]() CBMC-SC: ![]() CImpact: ERROR/TIMEOUT[8] 240.29sec ESBMC: ![]() Threader-monolithic: ERROR/TIMEOUT[1] 0.12sec Threader-owicki-gries: ERROR/TIMEOUT[1] 0.11sec Threader-rely-guarantee: ERROR/TIMEOUT[1] 0.09sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT Blender: ![]() |
![]() |
Cycles
SatAbs: ![]() 4.27sec (x5.84) Satabs-prefix-first: ![]() CBMC-WMM: ![]() CBMC-SC: ![]() CImpact: ERROR/TIMEOUT[8] 251.98sec ESBMC: ![]() Threader-monolithic: ERROR/TIMEOUT[1] 0.08sec Threader-owicki-gries: ERROR/TIMEOUT[1] 0.11sec Threader-rely-guarantee: ERROR/TIMEOUT[1] 0.11sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT |
Cycles
SatAbs: ![]() 4.25sec (x5.82) Satabs-prefix-first: ![]() CBMC-WMM: ![]() CBMC-SC: ![]() CImpact: ERROR/TIMEOUT[8] 278.32sec ESBMC: ![]() Threader-monolithic: ERROR/TIMEOUT[1] 0.12sec Threader-owicki-gries: ERROR/TIMEOUT[1] 0.11sec Threader-rely-guarantee: ERROR/TIMEOUT[1] 0.13sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT |
Cycles
SatAbs: ![]() 4.09sec (x5.60) Satabs-prefix-first: ![]() CBMC-WMM: ![]() CBMC-SC: ![]() CImpact: ERROR/TIMEOUT[8] 312.15sec ESBMC: ![]() Threader-monolithic: ERROR/TIMEOUT[1] 0.12sec Threader-owicki-gries: ERROR/TIMEOUT[1] 0.11sec Threader-rely-guarantee: ERROR/TIMEOUT[1] 0.12sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT |
![]() |
Cycles
SatAbs: ERROR/TIMEOUT[130] 1258.41sec (x1723.84) Satabs-prefix-first: ![]() CBMC-WMM: ![]() CBMC-SC: ![]() CImpact: ![]() ESBMC: ![]() Threader-monolithic: ERROR/TIMEOUT[130] 897.77sec Threader-owicki-gries: ERROR/TIMEOUT[130] 895.75sec Threader-rely-guarantee: ERROR/TIMEOUT[130] 896.94sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT |
Cycles
SatAbs: ![]() 46.80sec (x64.10) Satabs-prefix-first: ![]() CBMC-WMM: ![]() CBMC-SC: ![]() CImpact: ![]() ESBMC: ![]() Threader-monolithic: ERROR/TIMEOUT[1] 421.76sec Threader-owicki-gries: ERROR/TIMEOUT[1] 382.11sec Threader-rely-guarantee: ERROR/TIMEOUT[1] 344.79sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT |
Cycles
SatAbs: ![]() 44.68sec (x61.20) Satabs-prefix-first: ![]() CBMC-WMM: ![]() CBMC-SC: ![]() CImpact: ![]() ESBMC: ![]() Threader-monolithic: ERROR/TIMEOUT[1] 327.42sec Threader-owicki-gries: ERROR/TIMEOUT[1] 403.30sec Threader-rely-guarantee: ERROR/TIMEOUT[1] 381.05sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT |
![]() |
ppc/bclwdww003 |
SatAbs: ![]() 2.49sec Satabs-prefix-first: ![]() CBMC-WMM: ![]() CBMC-SC: ![]() CImpact: ERROR/TIMEOUT[8] 283.39sec Checkfence: 0.01sec ESBMC: ![]() Threader-monolithic: ![]() Threader-owicki-gries: ![]() Threader-rely-guarantee: ![]() Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT MMChecker (MM: sc): ERROR/TIMEOUT[1] 0.09sec |
Cycles
SatAbs: ![]() 8.12sec (x3.26) Satabs-prefix-first: ![]() CBMC-WMM: ![]() CBMC-SC: ![]() CImpact: ![]() ESBMC: ![]() Threader-monolithic: ERROR/TIMEOUT[130] 897.39sec Threader-owicki-gries: ERROR/TIMEOUT[130] 897.62sec Threader-rely-guarantee: ERROR/TIMEOUT[130] 897.47sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT MMChecker (MM: csharp): ERROR/TIMEOUT[1] 0.10sec |
Cycles
SatAbs: ![]() 12.94sec (x5.19) Satabs-prefix-first: ![]() CBMC-WMM: ![]() CBMC-SC: ![]() CImpact: ERROR/TIMEOUT[8] 261.79sec Checkfence: 0.01sec ESBMC: ![]() Threader-monolithic: ERROR/TIMEOUT[1] 0.11sec Threader-owicki-gries: ERROR/TIMEOUT[1] 0.12sec Threader-rely-guarantee: ERROR/TIMEOUT[1] 0.12sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT MMChecker (MM: csharp): ERROR/TIMEOUT[1] 0.10sec |
Cycles
SatAbs: ![]() 13.04sec (x5.23) Satabs-prefix-first: ![]() CBMC-WMM: ![]() CBMC-SC: ![]() CImpact: ERROR/TIMEOUT[8] 301.39sec ESBMC: ![]() Threader-monolithic: ERROR/TIMEOUT[1] 0.12sec Threader-owicki-gries: ERROR/TIMEOUT[1] 0.11sec Threader-rely-guarantee: ERROR/TIMEOUT[1] 0.11sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT MMChecker (MM: csharp): ERROR/TIMEOUT[1] 0.09sec |
Cycles
SatAbs: ![]() 12.45sec (x5.00) Satabs-prefix-first: ![]() CBMC-WMM: ![]() CBMC-SC: ![]() CImpact: ERROR/TIMEOUT[8] 288.45sec ESBMC: ![]() Threader-monolithic: ERROR/TIMEOUT[1] 0.09sec Threader-owicki-gries: ERROR/TIMEOUT[1] 0.12sec Threader-rely-guarantee: ERROR/TIMEOUT[1] 0.12sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT MMChecker (MM: csharp): ERROR/TIMEOUT[1] 0.10sec |
![]() |
Cycles
SatAbs: ![]() 12.48sec (x5.01) Satabs-prefix-first: ![]() CBMC-WMM: ![]() CBMC-SC: ![]() CImpact: ERROR/TIMEOUT[8] 262.41sec ESBMC: ![]() Threader-monolithic: ERROR/TIMEOUT[1] 0.11sec Threader-owicki-gries: ERROR/TIMEOUT[1] 0.13sec Threader-rely-guarantee: ERROR/TIMEOUT[1] 0.12sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT Blender: ![]() |
Cycles
SatAbs: ![]() 14.62sec (x5.87) Satabs-prefix-first: ![]() CBMC-WMM: ![]() CBMC-SC: ![]() CImpact: ERROR/TIMEOUT[8] 210.65sec ESBMC: ![]() Threader-monolithic: ERROR/TIMEOUT[1] 0.11sec Threader-owicki-gries: ERROR/TIMEOUT[1] 0.11sec Threader-rely-guarantee: ERROR/TIMEOUT[1] 0.09sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT Blender: ![]() |
Cycles
SatAbs: ![]() 13.35sec (x5.36) Satabs-prefix-first: ![]() CBMC-WMM: ![]() CBMC-SC: ![]() CImpact: ERROR/TIMEOUT[8] 273.32sec ESBMC: ![]() Threader-monolithic: ERROR/TIMEOUT[1] 0.12sec Threader-owicki-gries: ERROR/TIMEOUT[1] 0.11sec Threader-rely-guarantee: ERROR/TIMEOUT[1] 0.12sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT Blender: ![]() |
![]() |
Cycles
SatAbs: ![]() 11.36sec (x4.56) Satabs-prefix-first: ![]() CBMC-WMM: ![]() CBMC-SC: ![]() CImpact: ERROR/TIMEOUT[8] 246.42sec ESBMC: ![]() Threader-monolithic: ERROR/TIMEOUT[1] 0.09sec Threader-owicki-gries: ERROR/TIMEOUT[1] 0.10sec Threader-rely-guarantee: ERROR/TIMEOUT[1] 0.12sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT |
Cycles
SatAbs: ![]() 12.41sec (x4.98) Satabs-prefix-first: ![]() CBMC-WMM: ![]() CBMC-SC: ![]() CImpact: ERROR/TIMEOUT[8] 221.01sec ESBMC: ![]() Threader-monolithic: ERROR/TIMEOUT[1] 0.12sec Threader-owicki-gries: ERROR/TIMEOUT[1] 0.12sec Threader-rely-guarantee: ERROR/TIMEOUT[1] 0.08sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT |
Cycles
SatAbs: ![]() 12.55sec (x5.04) Satabs-prefix-first: ![]() CBMC-WMM: ![]() CBMC-SC: ![]() CImpact: ERROR/TIMEOUT[8] 219.04sec ESBMC: ![]() Threader-monolithic: ERROR/TIMEOUT[1] 0.12sec Threader-owicki-gries: ERROR/TIMEOUT[1] 0.12sec Threader-rely-guarantee: ERROR/TIMEOUT[1] 0.11sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT |
![]() |
Cycles
SatAbs: ![]() 510.81sec (x205.14) Satabs-prefix-first: ![]() CBMC-WMM: ![]() CBMC-SC: ![]() CImpact: ![]() ESBMC: ![]() Threader-monolithic: ERROR/TIMEOUT[130] 897.26sec Threader-owicki-gries: ERROR/TIMEOUT[130] 897.71sec Threader-rely-guarantee: ERROR/TIMEOUT[130] 897.67sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT |
Cycles
SatAbs: ![]() 104.69sec (x42.04) Satabs-prefix-first: ![]() CBMC-WMM: ![]() CBMC-SC: ![]() CImpact: ![]() ESBMC: ![]() Threader-monolithic: ERROR/TIMEOUT[1] 306.81sec Threader-owicki-gries: ERROR/TIMEOUT[1] 308.24sec Threader-rely-guarantee: ERROR/TIMEOUT[1] 308.76sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT |
Cycles
SatAbs: ![]() 122.58sec (x49.22) Satabs-prefix-first: ![]() CBMC-WMM: ![]() CBMC-SC: ![]() CImpact: ![]() ESBMC: ![]() Threader-monolithic: ERROR/TIMEOUT[1] 311.31sec Threader-owicki-gries: ERROR/TIMEOUT[1] 309.92sec Threader-rely-guarantee: ERROR/TIMEOUT[1] 309.19sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT |
![]() |
ppc/bclwdww004 |
SatAbs: ![]() 1.25sec Satabs-prefix-first: ![]() CBMC-WMM: ![]() CBMC-SC: ![]() CImpact: ERROR/TIMEOUT[8] 218.71sec Checkfence: 0.01sec ESBMC: ![]() Threader-monolithic: ![]() Threader-owicki-gries: ![]() Threader-rely-guarantee: ![]() Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT MMChecker (MM: sc): ERROR/TIMEOUT[1] 0.08sec |
Cycles
SatAbs: ![]() 38.45sec (x30.76) Satabs-prefix-first: ![]() CBMC-WMM: ![]() CBMC-SC: ![]() CImpact: ![]() ESBMC: ![]() Threader-monolithic: ERROR/TIMEOUT[130] 897.40sec Threader-owicki-gries: ERROR/TIMEOUT[130] 897.50sec Threader-rely-guarantee: ERROR/TIMEOUT[130] 897.54sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT MMChecker (MM: csharp): ERROR/TIMEOUT[1] 0.07sec |
Cycles
SatAbs: ![]() 17.08sec (x13.66) Satabs-prefix-first: ![]() CBMC-WMM: ![]() CBMC-SC: ![]() CImpact: ERROR/TIMEOUT[8] 194.49sec Checkfence: 0.01sec ESBMC: ![]() Threader-monolithic: ERROR/TIMEOUT[1] 0.08sec Threader-owicki-gries: ERROR/TIMEOUT[1] 0.09sec Threader-rely-guarantee: ERROR/TIMEOUT[1] 0.09sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT MMChecker (MM: csharp): ERROR/TIMEOUT[1] 0.06sec |
Cycles
SatAbs: ![]() 17.44sec (x13.95) Satabs-prefix-first: ![]() CBMC-WMM: ![]() CBMC-SC: ![]() CImpact: ERROR/TIMEOUT[8] 187.15sec ESBMC: ![]() Threader-monolithic: ERROR/TIMEOUT[1] 0.08sec Threader-owicki-gries: ERROR/TIMEOUT[1] 0.09sec Threader-rely-guarantee: ERROR/TIMEOUT[1] 0.10sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT MMChecker (MM: csharp): ERROR/TIMEOUT[1] 0.06sec |
Cycles
SatAbs: ![]() 16.67sec (x13.33) Satabs-prefix-first: ![]() CBMC-WMM: ![]() CBMC-SC: ![]() CImpact: ERROR/TIMEOUT[8] 195.91sec ESBMC: ![]() Threader-monolithic: ERROR/TIMEOUT[1] 0.09sec Threader-owicki-gries: ERROR/TIMEOUT[1] 0.09sec Threader-rely-guarantee: ERROR/TIMEOUT[1] 0.08sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT MMChecker (MM: csharp): ERROR/TIMEOUT[1] 0.09sec |
![]() |
Cycles
SatAbs: ![]() 13.42sec (x10.73) Satabs-prefix-first: ![]() CBMC-WMM: ![]() CBMC-SC: ![]() CImpact: ERROR/TIMEOUT[8] 189.48sec ESBMC: ![]() Threader-monolithic: ERROR/TIMEOUT[1] 0.08sec Threader-owicki-gries: ERROR/TIMEOUT[1] 0.09sec Threader-rely-guarantee: ERROR/TIMEOUT[1] 0.09sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT Blender: ![]() |
Cycles
SatAbs: ![]() 15.01sec (x12.00) Satabs-prefix-first: ![]() CBMC-WMM: ![]() CBMC-SC: ![]() CImpact: ERROR/TIMEOUT[8] 218.94sec ESBMC: ![]() Threader-monolithic: ERROR/TIMEOUT[1] 0.09sec Threader-owicki-gries: ERROR/TIMEOUT[1] 0.15sec Threader-rely-guarantee: ERROR/TIMEOUT[1] 0.12sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT Blender: ![]() |
Cycles
SatAbs: ![]() 15.82sec (x12.65) Satabs-prefix-first: ![]() CBMC-WMM: ![]() CBMC-SC: ![]() CImpact: ERROR/TIMEOUT[8] 196.28sec ESBMC: ![]() Threader-monolithic: ERROR/TIMEOUT[1] 0.10sec Threader-owicki-gries: ERROR/TIMEOUT[1] 0.08sec Threader-rely-guarantee: ERROR/TIMEOUT[1] 0.10sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT Blender: ![]() |
![]() |
Cycles
SatAbs: ![]() 18.45sec (x14.76) Satabs-prefix-first: ![]() CBMC-WMM: ![]() CBMC-SC: ![]() CImpact: ERROR/TIMEOUT[8] 197.25sec ESBMC: ![]() Threader-monolithic: ERROR/TIMEOUT[1] 0.08sec Threader-owicki-gries: ERROR/TIMEOUT[1] 0.08sec Threader-rely-guarantee: ERROR/TIMEOUT[1] 0.10sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT |
Cycles
SatAbs: ![]() 18.79sec (x15.03) Satabs-prefix-first: ![]() CBMC-WMM: ![]() CBMC-SC: ![]() CImpact: ERROR/TIMEOUT[8] 197.38sec ESBMC: ![]() Threader-monolithic: ERROR/TIMEOUT[1] 0.09sec Threader-owicki-gries: ERROR/TIMEOUT[1] 0.10sec Threader-rely-guarantee: ERROR/TIMEOUT[1] 0.10sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT |
Cycles
SatAbs: ![]() 18.33sec (x14.66) Satabs-prefix-first: ![]() CBMC-WMM: ![]() CBMC-SC: ![]() CImpact: ERROR/TIMEOUT[8] 197.68sec ESBMC: ![]() Threader-monolithic: ERROR/TIMEOUT[1] 0.08sec Threader-owicki-gries: ERROR/TIMEOUT[1] 0.09sec Threader-rely-guarantee: ERROR/TIMEOUT[1] 0.08sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT |
![]() |
Cycles
SatAbs: ERROR/TIMEOUT[130] 1207.91sec (x966.32) Satabs-prefix-first: ERROR/TIMEOUT[130] 923.41sec CBMC-WMM: ![]() CBMC-SC: ![]() CImpact: ERROR/TIMEOUT[8] 297.49sec ESBMC: ![]() Threader-monolithic: ERROR/TIMEOUT[130] 897.42sec Threader-owicki-gries: ERROR/TIMEOUT[130] 897.25sec Threader-rely-guarantee: ERROR/TIMEOUT[130] 897.71sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT |
Cycles
SatAbs: ERROR/TIMEOUT[130] 1172.48sec (x937.98) Satabs-prefix-first: ERROR/TIMEOUT[130] 930.70sec CBMC-WMM: ![]() CBMC-SC: ![]() CImpact: ERROR/TIMEOUT[8] 287.36sec ESBMC: ![]() Threader-monolithic: ERROR/TIMEOUT[130] 897.62sec Threader-owicki-gries: ERROR/TIMEOUT[130] 897.74sec Threader-rely-guarantee: ERROR/TIMEOUT[130] 897.67sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT |
Cycles
SatAbs: ERROR/TIMEOUT[130] 1144.54sec (x915.63) Satabs-prefix-first: ERROR/TIMEOUT[130] 924.98sec CBMC-WMM: ![]() CBMC-SC: ![]() CImpact: ERROR/TIMEOUT[8] 323.49sec ESBMC: ![]() Threader-monolithic: ERROR/TIMEOUT[130] 897.68sec Threader-owicki-gries: ERROR/TIMEOUT[130] 897.70sec Threader-rely-guarantee: ERROR/TIMEOUT[130] 897.63sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT |
![]() |
ppc/bclwdww005 |
SatAbs: ![]() 0.57sec Satabs-prefix-first: ![]() CBMC-WMM: ![]() CBMC-SC: ![]() CImpact: ERROR/TIMEOUT[8] 189.88sec Checkfence: 0.01sec ESBMC: ![]() Threader-monolithic: ![]() Threader-owicki-gries: ![]() Threader-rely-guarantee: ![]() Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT MMChecker (MM: sc): ![]() |
Cycles
SatAbs: ![]() 8.19sec (x14.36) Satabs-prefix-first: ![]() CBMC-WMM: ![]() CBMC-SC: ![]() CImpact: ![]() ESBMC: ![]() Threader-monolithic: ERROR/TIMEOUT[130] 897.51sec Threader-owicki-gries: ERROR/TIMEOUT[130] 897.45sec Threader-rely-guarantee: ERROR/TIMEOUT[130] 897.60sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT MMChecker (MM: csharp): ![]() |
Cycles
SatAbs: ![]() 6.70sec (x11.75) Satabs-prefix-first: ![]() CBMC-WMM: ![]() CBMC-SC: ![]() CImpact: ERROR/TIMEOUT[8] 210.86sec Checkfence: 0.00sec ESBMC: ![]() Threader-monolithic: ERROR/TIMEOUT[1] 0.08sec Threader-owicki-gries: ERROR/TIMEOUT[1] 0.09sec Threader-rely-guarantee: ERROR/TIMEOUT[1] 0.08sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT MMChecker (MM: csharp): ![]() |
Cycles
SatAbs: ![]() 6.51sec (x11.42) Satabs-prefix-first: ![]() CBMC-WMM: ![]() CBMC-SC: ![]() CImpact: ERROR/TIMEOUT[8] 209.93sec ESBMC: ![]() Threader-monolithic: ERROR/TIMEOUT[1] 0.09sec Threader-owicki-gries: ERROR/TIMEOUT[1] 0.08sec Threader-rely-guarantee: ERROR/TIMEOUT[1] 0.09sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT MMChecker (MM: csharp): ![]() |
Cycles
SatAbs: ![]() 6.41sec (x11.24) Satabs-prefix-first: ![]() CBMC-WMM: ![]() CBMC-SC: ![]() CImpact: ERROR/TIMEOUT[8] 210.18sec ESBMC: ![]() Threader-monolithic: ERROR/TIMEOUT[1] 0.09sec Threader-owicki-gries: ERROR/TIMEOUT[1] 0.09sec Threader-rely-guarantee: ERROR/TIMEOUT[1] 0.08sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT MMChecker (MM: csharp): ![]() |
![]() |
Cycles
SatAbs: ![]() 6.64sec (x11.64) Satabs-prefix-first: ![]() CBMC-WMM: ![]() CBMC-SC: ![]() CImpact: ERROR/TIMEOUT[8] 206.11sec ESBMC: ![]() Threader-monolithic: ERROR/TIMEOUT[1] 0.08sec Threader-owicki-gries: ERROR/TIMEOUT[1] 0.09sec Threader-rely-guarantee: ERROR/TIMEOUT[1] 0.09sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT Blender: ![]() |
Cycles
SatAbs: ![]() 6.64sec (x11.64) Satabs-prefix-first: ![]() CBMC-WMM: ![]() CBMC-SC: ![]() CImpact: ERROR/TIMEOUT[8] 206.90sec ESBMC: ![]() Threader-monolithic: ERROR/TIMEOUT[1] 0.09sec Threader-owicki-gries: ERROR/TIMEOUT[1] 0.08sec Threader-rely-guarantee: ERROR/TIMEOUT[1] 0.07sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT Blender: ![]() |
Cycles
SatAbs: ![]() 6.30sec (x11.05) Satabs-prefix-first: ![]() CBMC-WMM: ![]() CBMC-SC: ![]() CImpact: ERROR/TIMEOUT[8] 208.99sec ESBMC: ![]() Threader-monolithic: ERROR/TIMEOUT[1] 0.10sec Threader-owicki-gries: ERROR/TIMEOUT[1] 0.09sec Threader-rely-guarantee: ERROR/TIMEOUT[1] 0.08sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT Blender: ![]() |
![]() |
Cycles
SatAbs: ![]() 6.43sec (x11.28) Satabs-prefix-first: ![]() CBMC-WMM: ![]() CBMC-SC: ![]() CImpact: ERROR/TIMEOUT[8] 206.36sec ESBMC: ![]() Threader-monolithic: ERROR/TIMEOUT[1] 0.08sec Threader-owicki-gries: ERROR/TIMEOUT[1] 0.10sec Threader-rely-guarantee: ERROR/TIMEOUT[1] 0.09sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT |
Cycles
SatAbs: ![]() 6.53sec (x11.45) Satabs-prefix-first: ![]() CBMC-WMM: ![]() CBMC-SC: ![]() CImpact: ERROR/TIMEOUT[8] 207.69sec ESBMC: ![]() Threader-monolithic: ERROR/TIMEOUT[1] 0.08sec Threader-owicki-gries: ERROR/TIMEOUT[1] 0.07sec Threader-rely-guarantee: ERROR/TIMEOUT[1] 0.09sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT |
Cycles
SatAbs: ![]() 6.61sec (x11.59) Satabs-prefix-first: ![]() CBMC-WMM: ![]() CBMC-SC: ![]() CImpact: ERROR/TIMEOUT[8] 205.13sec ESBMC: ![]() Threader-monolithic: ERROR/TIMEOUT[1] 0.08sec Threader-owicki-gries: ERROR/TIMEOUT[1] 0.08sec Threader-rely-guarantee: ERROR/TIMEOUT[1] 0.08sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT |
![]() |
Cycles
SatAbs: ![]() 252.80sec (x443.50) Satabs-prefix-first: ![]() CBMC-WMM: ![]() CBMC-SC: ![]() CImpact: ![]() ESBMC: ![]() Threader-monolithic: ERROR/TIMEOUT[130] 897.35sec Threader-owicki-gries: ERROR/TIMEOUT[130] 897.28sec Threader-rely-guarantee: ERROR/TIMEOUT[130] 897.53sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT |
Cycles
SatAbs: ![]() 35.46sec (x62.21) Satabs-prefix-first: ![]() CBMC-WMM: ![]() CBMC-SC: ![]() CImpact: ![]() ESBMC: ![]() Threader-monolithic: ERROR/TIMEOUT[1] 304.89sec Threader-owicki-gries: ERROR/TIMEOUT[1] 305.92sec Threader-rely-guarantee: ERROR/TIMEOUT[1] 308.32sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT |
Cycles
SatAbs: ![]() 28.29sec (x49.63) Satabs-prefix-first: ![]() CBMC-WMM: ![]() CBMC-SC: ![]() CImpact: ![]() ESBMC: ![]() Threader-monolithic: ERROR/TIMEOUT[1] 306.43sec Threader-owicki-gries: ERROR/TIMEOUT[1] 306.50sec Threader-rely-guarantee: ERROR/TIMEOUT[1] 304.87sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT |
![]() |
ppc/bclwdww006 |
SatAbs: ![]() 0.92sec Satabs-prefix-first: ![]() CBMC-WMM: ![]() CBMC-SC: ![]() CImpact: ERROR/TIMEOUT[8] 205.76sec Checkfence: 0.01sec ESBMC: ![]() Threader-monolithic: ![]() Threader-owicki-gries: ![]() Threader-rely-guarantee: ![]() Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT MMChecker (MM: sc): ![]() |
Cycles
SatAbs: ![]() 36.03sec (x39.16) Satabs-prefix-first: ![]() CBMC-WMM: ![]() CBMC-SC: ![]() CImpact: ![]() ESBMC: ![]() Threader-monolithic: ERROR/TIMEOUT[130] 897.77sec Threader-owicki-gries: ERROR/TIMEOUT[130] 897.05sec Threader-rely-guarantee: ERROR/TIMEOUT[130] 897.66sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT MMChecker (MM: csharp): ![]() |
Cycles
SatAbs: ![]() 3.78sec (x4.10) Satabs-prefix-first: ![]() CBMC-WMM: ![]() CBMC-SC: ![]() CImpact: ERROR/TIMEOUT[8] 226.81sec Checkfence: 0.01sec ESBMC: ![]() Threader-monolithic: ERROR/TIMEOUT[1] 0.09sec Threader-owicki-gries: ERROR/TIMEOUT[1] 0.08sec Threader-rely-guarantee: ERROR/TIMEOUT[1] 0.08sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT MMChecker (MM: csharp): ![]() |
Cycles
SatAbs: ![]() 4.12sec (x4.47) Satabs-prefix-first: ![]() CBMC-WMM: ![]() CBMC-SC: ![]() CImpact: ERROR/TIMEOUT[8] 235.46sec ESBMC: ![]() Threader-monolithic: ERROR/TIMEOUT[1] 0.09sec Threader-owicki-gries: ERROR/TIMEOUT[1] 0.09sec Threader-rely-guarantee: ERROR/TIMEOUT[1] 0.09sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT MMChecker (MM: csharp): ![]() |
Cycles
SatAbs: ![]() 4.23sec (x4.59) Satabs-prefix-first: ![]() CBMC-WMM: ![]() CBMC-SC: ![]() CImpact: ERROR/TIMEOUT[8] 226.88sec ESBMC: ![]() Threader-monolithic: ERROR/TIMEOUT[1] 0.07sec Threader-owicki-gries: ERROR/TIMEOUT[1] 0.08sec Threader-rely-guarantee: ERROR/TIMEOUT[1] 0.10sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT MMChecker (MM: csharp): ![]() |
![]() |
Cycles
SatAbs: ![]() 3.95sec (x4.29) Satabs-prefix-first: ![]() CBMC-WMM: ![]() CBMC-SC: ![]() CImpact: ERROR/TIMEOUT[8] 226.47sec ESBMC: ![]() Threader-monolithic: ERROR/TIMEOUT[1] 0.08sec Threader-owicki-gries: ERROR/TIMEOUT[1] 0.08sec Threader-rely-guarantee: ERROR/TIMEOUT[1] 0.08sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT Blender: ![]() |
Cycles
SatAbs: ![]() 3.64sec (x3.95) Satabs-prefix-first: ![]() CBMC-WMM: ![]() CBMC-SC: ![]() CImpact: ERROR/TIMEOUT[8] 230.01sec ESBMC: ![]() Threader-monolithic: ERROR/TIMEOUT[1] 0.09sec Threader-owicki-gries: ERROR/TIMEOUT[1] 0.08sec Threader-rely-guarantee: ERROR/TIMEOUT[1] 0.09sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT Blender: ![]() |
Cycles
SatAbs: ![]() 3.70sec (x4.02) Satabs-prefix-first: ![]() CBMC-WMM: ![]() CBMC-SC: ![]() CImpact: ERROR/TIMEOUT[8] 230.97sec ESBMC: ![]() Threader-monolithic: ERROR/TIMEOUT[1] 0.09sec Threader-owicki-gries: ERROR/TIMEOUT[1] 0.09sec Threader-rely-guarantee: ERROR/TIMEOUT[1] 0.07sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT Blender: ![]() |
![]() |
Cycles
SatAbs: ![]() 3.82sec (x4.15) Satabs-prefix-first: ![]() CBMC-WMM: ![]() CBMC-SC: ![]() CImpact: ERROR/TIMEOUT[8] 227.63sec ESBMC: ![]() Threader-monolithic: ERROR/TIMEOUT[1] 0.09sec Threader-owicki-gries: ERROR/TIMEOUT[1] 0.09sec Threader-rely-guarantee: ERROR/TIMEOUT[1] 0.09sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT |
Cycles
SatAbs: ![]() 3.78sec (x4.10) Satabs-prefix-first: ![]() CBMC-WMM: ![]() CBMC-SC: ![]() CImpact: ERROR/TIMEOUT[8] 226.30sec ESBMC: ![]() Threader-monolithic: ERROR/TIMEOUT[1] 0.09sec Threader-owicki-gries: ERROR/TIMEOUT[1] 0.07sec Threader-rely-guarantee: ERROR/TIMEOUT[1] 0.07sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT |
Cycles
SatAbs: ![]() 3.54sec (x3.84) Satabs-prefix-first: ![]() CBMC-WMM: ![]() CBMC-SC: ![]() CImpact: ERROR/TIMEOUT[8] 226.85sec ESBMC: ![]() Threader-monolithic: ERROR/TIMEOUT[1] 0.07sec Threader-owicki-gries: ERROR/TIMEOUT[1] 0.08sec Threader-rely-guarantee: ERROR/TIMEOUT[1] 0.06sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT |
![]() |
Cycles
SatAbs: ![]() 640.45sec (x696.14) Satabs-prefix-first: ![]() CBMC-WMM: ![]() CBMC-SC: ![]() CImpact: ![]() ESBMC: ![]() Threader-monolithic: ERROR/TIMEOUT[130] 897.60sec Threader-owicki-gries: ERROR/TIMEOUT[130] 897.59sec Threader-rely-guarantee: ERROR/TIMEOUT[130] 897.33sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT |
Cycles
SatAbs: ![]() 720.48sec (x783.13) Satabs-prefix-first: ![]() CBMC-WMM: ![]() CBMC-SC: ![]() CImpact: ![]() ESBMC: ![]() Threader-monolithic: ERROR/TIMEOUT[130] 897.13sec Threader-owicki-gries: ERROR/TIMEOUT[130] 897.70sec Threader-rely-guarantee: ERROR/TIMEOUT[130] 897.69sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT |
Cycles
SatAbs: ERROR/TIMEOUT[130] 1098.25sec (x1193.75) Satabs-prefix-first: ERROR/TIMEOUT[130] 918.24sec CBMC-WMM: ![]() CBMC-SC: ![]() CImpact: ERROR/TIMEOUT[8] 310.10sec ESBMC: ![]() Threader-monolithic: ERROR/TIMEOUT[130] 897.43sec Threader-owicki-gries: ERROR/TIMEOUT[130] 897.48sec Threader-rely-guarantee: ERROR/TIMEOUT[130] 897.69sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT |
![]() |
ppc/bclwdww007 |
SatAbs: ![]() 0.41sec Satabs-prefix-first: ![]() CBMC-WMM: ![]() CBMC-SC: ![]() CImpact: ![]() Checkfence: 0.01sec ESBMC: ![]() Threader-monolithic: ![]() Threader-owicki-gries: ![]() Threader-rely-guarantee: ![]() Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT MMChecker (MM: sc): ![]() |
Cycles
SatAbs: ![]() 6.06sec (x14.78) Satabs-prefix-first: ![]() CBMC-WMM: ![]() CBMC-SC: ![]() CImpact: ![]() ESBMC: ![]() Threader-monolithic: ERROR/TIMEOUT[130] 897.41sec Threader-owicki-gries: ERROR/TIMEOUT[130] 897.55sec Threader-rely-guarantee: ERROR/TIMEOUT[130] 897.31sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT MMChecker (MM: csharp): ![]() |
Cycles
SatAbs: ![]() 1.11sec (x2.70) Satabs-prefix-first: ![]() CBMC-WMM: ![]() CBMC-SC: ![]() CImpact: ![]() Checkfence: 0.01sec ESBMC: ![]() Threader-monolithic: ERROR/TIMEOUT[1] 0.08sec Threader-owicki-gries: ERROR/TIMEOUT[1] 0.08sec Threader-rely-guarantee: ERROR/TIMEOUT[1] 0.08sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT MMChecker (MM: csharp): ![]() |
Cycles
SatAbs: ![]() 0.96sec (x2.34) Satabs-prefix-first: ![]() CBMC-WMM: ![]() CBMC-SC: ![]() CImpact: ![]() ESBMC: ![]() Threader-monolithic: ERROR/TIMEOUT[1] 0.08sec Threader-owicki-gries: ERROR/TIMEOUT[1] 0.09sec Threader-rely-guarantee: ERROR/TIMEOUT[1] 0.06sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT MMChecker (MM: csharp): ![]() |
Cycles
SatAbs: ![]() 0.91sec (x2.21) Satabs-prefix-first: ![]() CBMC-WMM: ![]() CBMC-SC: ![]() CImpact: ![]() ESBMC: ![]() Threader-monolithic: ERROR/TIMEOUT[1] 0.07sec Threader-owicki-gries: ERROR/TIMEOUT[1] 0.08sec Threader-rely-guarantee: ERROR/TIMEOUT[1] 0.10sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT MMChecker (MM: csharp): ![]() |
![]() |
Cycles
SatAbs: ![]() 0.95sec (x2.31) Satabs-prefix-first: ![]() CBMC-WMM: ![]() CBMC-SC: ![]() CImpact: ![]() ESBMC: ![]() Threader-monolithic: ERROR/TIMEOUT[1] 0.08sec Threader-owicki-gries: ERROR/TIMEOUT[1] 0.08sec Threader-rely-guarantee: ERROR/TIMEOUT[1] 0.08sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT Blender: ![]() |
Cycles
SatAbs: ![]() 0.92sec (x2.24) Satabs-prefix-first: ![]() CBMC-WMM: ![]() CBMC-SC: ![]() CImpact: ![]() ESBMC: ![]() Threader-monolithic: ERROR/TIMEOUT[1] 0.09sec Threader-owicki-gries: ERROR/TIMEOUT[1] 0.09sec Threader-rely-guarantee: ERROR/TIMEOUT[1] 0.08sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT Blender: ![]() |
Cycles
SatAbs: ![]() 0.84sec (x2.04) Satabs-prefix-first: ![]() CBMC-WMM: ![]() CBMC-SC: ![]() CImpact: ![]() ESBMC: ![]() Threader-monolithic: ERROR/TIMEOUT[1] 0.08sec Threader-owicki-gries: ERROR/TIMEOUT[1] 0.08sec Threader-rely-guarantee: ERROR/TIMEOUT[1] 0.08sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT Blender: ![]() |
![]() |
Cycles
SatAbs: ![]() 0.80sec (x1.95) Satabs-prefix-first: ![]() CBMC-WMM: ![]() CBMC-SC: ![]() CImpact: ![]() ESBMC: ![]() Threader-monolithic: ERROR/TIMEOUT[1] 0.07sec Threader-owicki-gries: ERROR/TIMEOUT[1] 0.07sec Threader-rely-guarantee: ERROR/TIMEOUT[1] 0.06sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT |
Cycles
SatAbs: ![]() 0.86sec (x2.09) Satabs-prefix-first: ![]() CBMC-WMM: ![]() CBMC-SC: ![]() CImpact: ![]() ESBMC: ![]() Threader-monolithic: ERROR/TIMEOUT[1] 0.06sec Threader-owicki-gries: ERROR/TIMEOUT[1] 0.06sec Threader-rely-guarantee: ERROR/TIMEOUT[1] 0.04sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT |
Cycles
SatAbs: ![]() 0.90sec (x2.19) Satabs-prefix-first: ![]() CBMC-WMM: ![]() CBMC-SC: ![]() CImpact: ![]() ESBMC: ![]() Threader-monolithic: ERROR/TIMEOUT[1] 0.06sec Threader-owicki-gries: ERROR/TIMEOUT[1] 0.09sec Threader-rely-guarantee: ERROR/TIMEOUT[1] 0.07sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT |
![]() |
Cycles
SatAbs: ![]() 71.65sec (x174.75) Satabs-prefix-first: ![]() CBMC-WMM: ![]() CBMC-SC: ![]() CImpact: ![]() ESBMC: ![]() Threader-monolithic: ERROR/TIMEOUT[130] 897.70sec Threader-owicki-gries: ERROR/TIMEOUT[130] 897.67sec Threader-rely-guarantee: ERROR/TIMEOUT[130] 897.57sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT |
Cycles
SatAbs: ![]() 6.17sec (x15.04) Satabs-prefix-first: ![]() CBMC-WMM: ![]() CBMC-SC: ![]() CImpact: ![]() ESBMC: ![]() Threader-monolithic: ERROR/TIMEOUT[1] 252.43sec Threader-owicki-gries: ERROR/TIMEOUT[1] 249.91sec Threader-rely-guarantee: ERROR/TIMEOUT[1] 252.24sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT |
Cycles
SatAbs: ![]() 6.03sec (x14.70) Satabs-prefix-first: ![]() CBMC-WMM: ![]() CBMC-SC: ![]() CImpact: ![]() ESBMC: ![]() Threader-monolithic: ERROR/TIMEOUT[1] 252.42sec Threader-owicki-gries: ERROR/TIMEOUT[1] 251.79sec Threader-rely-guarantee: ERROR/TIMEOUT[1] 252.41sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT |
![]() |
ppc/bclwdww008 Rfe DpAddrdR Fre LwSyncdWW |
Generated C code SatAbs: ![]() 1.51sec CImpact: ![]() Checkfence: 0.01sec ESBMC: ![]() Threader: ![]() Poirot: ERROR/TIMEOUT MMChecker (MM: sc): ERROR/TIMEOUT[1] 0.10sec |
Generated C code SatAbs: ![]() 1.57sec (x1.03) CImpact: ![]() Checkfence: 0.01sec ESBMC: ![]() Threader: ERROR/TIMEOUT[1] 0.16sec Poirot: ERROR/TIMEOUT MMChecker (MM: csharp): ERROR/TIMEOUT[1] 0.07sec |
Generated C code SatAbs: ![]() 1.16sec (x.76) CImpact: ![]() Checkfence: 0.01sec ESBMC: ![]() Threader: ERROR/TIMEOUT[1] 0.12sec Poirot: ![]() MMChecker (MM: csharp): ERROR/TIMEOUT[1] 0.10sec |
![]() |
Generated C code SatAbs: ![]() 1.69sec (x1.11) CImpact: ![]() ESBMC: ![]() Threader: ERROR/TIMEOUT[1] 0.18sec Poirot: ![]() Blender: ![]() |
Generated C code SatAbs: ![]() 1.69sec (x1.11) CImpact: ![]() ESBMC: ![]() Threader: ERROR/TIMEOUT[1] 0.15sec Poirot: ERROR/TIMEOUT Blender: ![]() |
![]() |
Generated C code SatAbs: ![]() 1.22sec (x.80) CImpact: ![]() ESBMC: ![]() Threader: ERROR/TIMEOUT[1] 0.13sec Poirot: ERROR/TIMEOUT |
Generated C code SatAbs: ![]() 1.79sec (x1.18) CImpact: ![]() ESBMC: ![]() Threader: ERROR/TIMEOUT[1] 0.14sec Poirot: ERROR/TIMEOUT |
![]() |
Generated C code SatAbs: ![]() 2.88sec (x1.90) CImpact: ![]() ESBMC: ![]() Threader: ERROR/TIMEOUT[1] 0.51sec Poirot: ![]() |
Generated C code SatAbs: ![]() 4.15sec (x2.74) CImpact: ![]() ESBMC: ![]() Threader: ERROR/TIMEOUT[1] 0.65sec Poirot: ![]() |
![]() |
|||||
ppc/bclwdww009 |
SatAbs: ![]() 1.17sec Satabs-prefix-first: ![]() CBMC-WMM: ![]() CBMC-SC: ![]() CImpact: ![]() Checkfence: 0.01sec ESBMC: ![]() Threader-monolithic: ![]() Threader-owicki-gries: ![]() Threader-rely-guarantee: ![]() Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT MMChecker (MM: sc): ![]() |
Cycles
SatAbs: ![]() 6.81sec (x5.82) Satabs-prefix-first: ![]() CBMC-WMM: ![]() CBMC-SC: ![]() CImpact: ![]() ESBMC: ![]() Threader-monolithic: ERROR/TIMEOUT[130] 896.80sec Threader-owicki-gries: ERROR/TIMEOUT[130] 896.62sec Threader-rely-guarantee: ERROR/TIMEOUT[130] 896.62sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT MMChecker (MM: csharp): ![]() |
Cycles
SatAbs: ![]() 0.65sec (x.55) Satabs-prefix-first: ![]() CBMC-WMM: ![]() CBMC-SC: ![]() CImpact: ![]() Checkfence: 0.01sec ESBMC: ![]() Threader-monolithic: ERROR/TIMEOUT[1] 0.07sec Threader-owicki-gries: ERROR/TIMEOUT[1] 0.08sec Threader-rely-guarantee: ERROR/TIMEOUT[1] 0.07sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT MMChecker (MM: csharp): ![]() |
Cycles
SatAbs: ![]() 0.69sec (x.58) Satabs-prefix-first: ![]() CBMC-WMM: ![]() CBMC-SC: ![]() CImpact: ![]() ESBMC: ![]() Threader-monolithic: ERROR/TIMEOUT[1] 0.07sec Threader-owicki-gries: ERROR/TIMEOUT[1] 0.07sec Threader-rely-guarantee: ERROR/TIMEOUT[1] 0.08sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT MMChecker (MM: csharp): ![]() |
Cycles
SatAbs: ![]() 0.62sec (x.52) Satabs-prefix-first: ![]() CBMC-WMM: ![]() CBMC-SC: ![]() CImpact: ![]() ESBMC: ![]() Threader-monolithic: ERROR/TIMEOUT[1] 0.07sec Threader-owicki-gries: ERROR/TIMEOUT[1] 0.06sec Threader-rely-guarantee: ERROR/TIMEOUT[1] 0.07sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT MMChecker (MM: csharp): ![]() |
![]() |
Cycles
SatAbs: ![]() 0.67sec (x.57) Satabs-prefix-first: ![]() CBMC-WMM: ![]() CBMC-SC: ![]() CImpact: ![]() ESBMC: ![]() Threader-monolithic: ERROR/TIMEOUT[1] 0.07sec Threader-owicki-gries: ERROR/TIMEOUT[1] 0.08sec Threader-rely-guarantee: ERROR/TIMEOUT[1] 0.07sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT Blender: ![]() |
Cycles
SatAbs: ![]() 0.68sec (x.58) Satabs-prefix-first: ![]() CBMC-WMM: ![]() CBMC-SC: ![]() CImpact: ![]() ESBMC: ![]() Threader-monolithic: ERROR/TIMEOUT[1] 0.08sec Threader-owicki-gries: ERROR/TIMEOUT[1] 0.06sec Threader-rely-guarantee: ERROR/TIMEOUT[1] 0.07sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT Blender: ![]() |
Cycles
SatAbs: ![]() 0.60sec (x.51) Satabs-prefix-first: ![]() CBMC-WMM: ![]() CBMC-SC: ![]() CImpact: ![]() ESBMC: ![]() Threader-monolithic: ERROR/TIMEOUT[1] 0.08sec Threader-owicki-gries: ERROR/TIMEOUT[1] 0.08sec Threader-rely-guarantee: ERROR/TIMEOUT[1] 0.08sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT Blender: ![]() |
![]() |
Cycles
SatAbs: ![]() 0.61sec (x.52) Satabs-prefix-first: ![]() CBMC-WMM: ![]() CBMC-SC: ![]() CImpact: ![]() ESBMC: ![]() Threader-monolithic: ERROR/TIMEOUT[1] 0.08sec Threader-owicki-gries: ERROR/TIMEOUT[1] 0.08sec Threader-rely-guarantee: ERROR/TIMEOUT[1] 0.08sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT |
Cycles
SatAbs: ![]() 0.59sec (x.50) Satabs-prefix-first: ![]() CBMC-WMM: ![]() CBMC-SC: ![]() CImpact: ![]() ESBMC: ![]() Threader-monolithic: ERROR/TIMEOUT[1] 0.08sec Threader-owicki-gries: ERROR/TIMEOUT[1] 0.06sec Threader-rely-guarantee: ERROR/TIMEOUT[1] 0.07sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT |
Cycles
SatAbs: ![]() 0.61sec (x.52) Satabs-prefix-first: ![]() CBMC-WMM: ![]() CBMC-SC: ![]() CImpact: ![]() ESBMC: ![]() Threader-monolithic: ERROR/TIMEOUT[1] 0.07sec Threader-owicki-gries: ERROR/TIMEOUT[1] 0.08sec Threader-rely-guarantee: ERROR/TIMEOUT[1] 0.07sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT |
![]() |
Cycles
SatAbs: ![]() 14.81sec (x12.65) Satabs-prefix-first: ![]() CBMC-WMM: ![]() CBMC-SC: ![]() CImpact: ![]() ESBMC: ![]() Threader-monolithic: ERROR/TIMEOUT[1] 250.38sec Threader-owicki-gries: ERROR/TIMEOUT[1] 252.64sec Threader-rely-guarantee: ERROR/TIMEOUT[1] 250.71sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT |
Cycles
SatAbs: ![]() 16.18sec (x13.82) Satabs-prefix-first: ![]() CBMC-WMM: ![]() CBMC-SC: ![]() CImpact: ![]() ESBMC: ![]() Threader-monolithic: ERROR/TIMEOUT[1] 250.97sec Threader-owicki-gries: ERROR/TIMEOUT[1] 250.05sec Threader-rely-guarantee: ERROR/TIMEOUT[1] 251.07sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT |
Cycles
SatAbs: ![]() 18.07sec (x15.44) Satabs-prefix-first: ![]() CBMC-WMM: ![]() CBMC-SC: ![]() CImpact: ![]() ESBMC: ![]() Threader-monolithic: ERROR/TIMEOUT[1] 251.84sec Threader-owicki-gries: ERROR/TIMEOUT[1] 251.61sec Threader-rely-guarantee: ERROR/TIMEOUT[1] 250.46sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT |
![]() |