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/aclwsrr (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 an A-cumulative ordering when placed between two reads. 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/aclwsrr000 |
SatAbs: 2.65sec Satabs-prefix-first: 3.92sec CBMC-WMM: 0.09sec CBMC-SC: 0.09sec CImpact: ERROR/TIMEOUT[8] 243.25sec Checkfence: 0.01sec ESBMC: 0.06sec Threader-monolithic: 0.15sec Threader-owicki-gries: 0.14sec Threader-rely-guarantee: 0.14sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT MMChecker (MM: sc): ERROR/TIMEOUT[1] 0.10sec |
Cycles
SatAbs: 3.00sec (x1.13) Satabs-prefix-first: 3.97sec CBMC-WMM: 0.16sec CBMC-SC: 32.63sec CImpact: ERROR/TIMEOUT[8] 373.52sec ESBMC: 0.11sec Threader-monolithic: ERROR/TIMEOUT[130] 897.33sec Threader-owicki-gries: ERROR/TIMEOUT[130] 897.31sec Threader-rely-guarantee: ERROR/TIMEOUT[130] 897.23sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT MMChecker (MM: csharp): ERROR/TIMEOUT[1] 0.10sec |
Cycles
SatAbs: 20.20sec (x7.62) Satabs-prefix-first: 9.22sec CBMC-WMM: 0.19sec CBMC-SC: 0.09sec CImpact: ERROR/TIMEOUT[8] 341.19sec Checkfence: 0.01sec ESBMC: 0.08sec Threader-monolithic: ERROR/TIMEOUT[1] 0.11sec Threader-owicki-gries: ERROR/TIMEOUT[1] 0.12sec Threader-rely-guarantee: ERROR/TIMEOUT[1] 0.10sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT MMChecker (MM: csharp): ERROR/TIMEOUT[1] 0.09sec |
Cycles
SatAbs: 19.40sec (x7.32) Satabs-prefix-first: 10.66sec CBMC-WMM: 0.19sec CBMC-SC: 0.08sec CImpact: ERROR/TIMEOUT[8] 352.16sec ESBMC: 0.06sec Threader-monolithic: ERROR/TIMEOUT[1] 0.12sec 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.09sec |
Cycles
SatAbs: 22.58sec (x8.52) Satabs-prefix-first: 10.21sec CBMC-WMM: 0.19sec CBMC-SC: 0.12sec CImpact: ERROR/TIMEOUT[8] 359.64sec ESBMC: 0.07sec Threader-monolithic: ERROR/TIMEOUT[1] 0.12sec Threader-owicki-gries: ERROR/TIMEOUT[1] 0.11sec Threader-rely-guarantee: ERROR/TIMEOUT[1] 0.12sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT MMChecker (MM: csharp): ERROR/TIMEOUT[1] 0.10sec |
Cycles
SatAbs: 19.66sec (x7.41) Satabs-prefix-first: 8.79sec CBMC-WMM: 0.19sec CBMC-SC: 0.06sec CImpact: ERROR/TIMEOUT[8] 357.56sec ESBMC: 0.05sec 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 Blender: |
Cycles
SatAbs: 24.18sec (x9.12) Satabs-prefix-first: 8.89sec CBMC-WMM: 0.17sec CBMC-SC: 0.08sec CImpact: ERROR/TIMEOUT[8] 262.75sec ESBMC: 0.09sec Threader-monolithic: ERROR/TIMEOUT[1] 0.12sec Threader-owicki-gries: ERROR/TIMEOUT[1] 0.11sec Threader-rely-guarantee: ERROR/TIMEOUT[1] 0.10sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT Blender: |
Cycles
SatAbs: 24.07sec (x9.08) Satabs-prefix-first: 9.20sec CBMC-WMM: 0.20sec CBMC-SC: 0.09sec CImpact: ERROR/TIMEOUT[8] 254.55sec ESBMC: 0.08sec Threader-monolithic: ERROR/TIMEOUT[1] 0.11sec Threader-owicki-gries: ERROR/TIMEOUT[1] 0.10sec Threader-rely-guarantee: ERROR/TIMEOUT[1] 0.12sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT Blender: |
Cycles
SatAbs: 19.97sec (x7.53) Satabs-prefix-first: 8.94sec CBMC-WMM: 0.20sec CBMC-SC: 0.09sec CImpact: ERROR/TIMEOUT[8] 344.58sec ESBMC: 0.08sec Threader-monolithic: ERROR/TIMEOUT[1] 0.11sec Threader-owicki-gries: ERROR/TIMEOUT[1] 0.11sec Threader-rely-guarantee: ERROR/TIMEOUT[1] 0.12sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT |
Cycles
SatAbs: 19.90sec (x7.50) Satabs-prefix-first: 8.60sec CBMC-WMM: 0.23sec CBMC-SC: 0.09sec CImpact: ERROR/TIMEOUT[8] 318.78sec ESBMC: 0.09sec Threader-monolithic: ERROR/TIMEOUT[1] 0.10sec Threader-owicki-gries: ERROR/TIMEOUT[1] 0.13sec Threader-rely-guarantee: ERROR/TIMEOUT[1] 0.13sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT |
Cycles
SatAbs: 21.42sec (x8.08) Satabs-prefix-first: 8.86sec CBMC-WMM: 0.22sec CBMC-SC: 0.06sec CImpact: ERROR/TIMEOUT[8] 351.64sec ESBMC: 0.08sec Threader-monolithic: ERROR/TIMEOUT[1] 0.10sec Threader-owicki-gries: ERROR/TIMEOUT[1] 0.09sec Threader-rely-guarantee: ERROR/TIMEOUT[1] 0.13sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT |
Cycles
SatAbs: 592.92sec (x223.74) Satabs-prefix-first: 301.37sec CBMC-WMM: 0.34sec CBMC-SC: 6.84sec CImpact: ERROR/TIMEOUT[8] 434.38sec ESBMC: 0.11sec Threader-monolithic: ERROR/TIMEOUT[130] 896.96sec Threader-owicki-gries: ERROR/TIMEOUT[130] 897.28sec Threader-rely-guarantee: ERROR/TIMEOUT[130] 897.27sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT |
Cycles
SatAbs: 542.87sec (x204.85) Satabs-prefix-first: 348.18sec CBMC-WMM: 0.20sec CBMC-SC: 5.53sec CImpact: ERROR/TIMEOUT[8] 276.09sec ESBMC: 0.11sec Threader-monolithic: ERROR/TIMEOUT[130] 897.32sec Threader-owicki-gries: ERROR/TIMEOUT[130] 897.62sec Threader-rely-guarantee: ERROR/TIMEOUT[130] 897.61sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT |
Cycles
SatAbs: 489.83sec (x184.84) Satabs-prefix-first: 326.02sec CBMC-WMM: 0.17sec CBMC-SC: 5.35sec CImpact: ERROR/TIMEOUT[8] 422.73sec ESBMC: 0.12sec Threader-monolithic: ERROR/TIMEOUT[130] 897.29sec Threader-owicki-gries: ERROR/TIMEOUT[130] 897.13sec Threader-rely-guarantee: ERROR/TIMEOUT[130] 896.74sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT |
||||
ppc/aclwsrr001 |
SatAbs: 7.83sec Satabs-prefix-first: 2.41sec CBMC-WMM: 0.09sec CBMC-SC: 0.09sec CImpact: ERROR/TIMEOUT[8] 262.90sec Checkfence: 0.01sec ESBMC: 0.06sec Threader-monolithic: 0.16sec Threader-owicki-gries: 0.14sec Threader-rely-guarantee: 0.14sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT MMChecker (MM: sc): 0.52sec |
Cycles
SatAbs: 4.23sec (x.54) Satabs-prefix-first: 5.85sec CBMC-WMM: 0.19sec CBMC-SC: 118.18sec CImpact: ERROR/TIMEOUT[8] 458.06sec ESBMC: 0.12sec Threader-monolithic: ERROR/TIMEOUT[130] 897.57sec Threader-owicki-gries: ERROR/TIMEOUT[130] 897.48sec Threader-rely-guarantee: ERROR/TIMEOUT[130] 897.43sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT MMChecker (MM: csharp): 0.52sec |
Cycles
SatAbs: 7.37sec (x.94) Satabs-prefix-first: 7.39sec CBMC-WMM: 0.19sec CBMC-SC: 0.09sec CImpact: ERROR/TIMEOUT[8] 373.56sec Checkfence: 0.01sec ESBMC: 0.06sec Threader-monolithic: ERROR/TIMEOUT[1] 0.11sec 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): 0.52sec |
Cycles
SatAbs: 7.04sec (x.89) Satabs-prefix-first: 6.96sec CBMC-WMM: 0.20sec CBMC-SC: 0.09sec CImpact: ERROR/TIMEOUT[8] 336.36sec ESBMC: 0.07sec Threader-monolithic: ERROR/TIMEOUT[1] 0.12sec Threader-owicki-gries: ERROR/TIMEOUT[1] 0.12sec Threader-rely-guarantee: ERROR/TIMEOUT[1] 0.12sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT MMChecker (MM: csharp): 0.68sec |
Cycles
SatAbs: 8.16sec (x1.04) Satabs-prefix-first: 8.05sec CBMC-WMM: 0.17sec CBMC-SC: 0.10sec CImpact: ERROR/TIMEOUT[8] 335.87sec ESBMC: 0.05sec Threader-monolithic: ERROR/TIMEOUT[1] 0.12sec Threader-owicki-gries: ERROR/TIMEOUT[1] 0.12sec Threader-rely-guarantee: ERROR/TIMEOUT[1] 0.12sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT MMChecker (MM: csharp): 0.51sec |
Cycles
SatAbs: 6.77sec (x.86) Satabs-prefix-first: 6.71sec CBMC-WMM: 0.17sec CBMC-SC: 0.08sec CImpact: ERROR/TIMEOUT[8] 290.06sec ESBMC: 0.05sec Threader-monolithic: ERROR/TIMEOUT[1] 0.12sec Threader-owicki-gries: ERROR/TIMEOUT[1] 0.11sec Threader-rely-guarantee: ERROR/TIMEOUT[1] 0.11sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT Blender: |
Cycles
SatAbs: 7.05sec (x.90) Satabs-prefix-first: 6.73sec CBMC-WMM: 0.17sec CBMC-SC: 0.08sec CImpact: ERROR/TIMEOUT[8] 233.97sec ESBMC: 0.05sec 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: 6.66sec (x.85) Satabs-prefix-first: 6.53sec CBMC-WMM: 0.17sec CBMC-SC: 0.08sec CImpact: ERROR/TIMEOUT[8] 305.06sec ESBMC: 0.08sec Threader-monolithic: ERROR/TIMEOUT[1] 0.12sec Threader-owicki-gries: ERROR/TIMEOUT[1] 0.11sec Threader-rely-guarantee: ERROR/TIMEOUT[1] 0.12sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT Blender: |
Cycles
SatAbs: 6.51sec (x.83) Satabs-prefix-first: 6.46sec CBMC-WMM: 0.21sec CBMC-SC: 0.08sec CImpact: ERROR/TIMEOUT[8] 328.92sec ESBMC: 0.06sec 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 |
Cycles
SatAbs: 6.26sec (x.79) Satabs-prefix-first: 6.51sec CBMC-WMM: 0.20sec CBMC-SC: 0.08sec CImpact: ERROR/TIMEOUT[8] 338.17sec ESBMC: 0.04sec Threader-monolithic: ERROR/TIMEOUT[1] 0.10sec 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: 6.75sec (x.86) Satabs-prefix-first: 6.63sec CBMC-WMM: 0.16sec CBMC-SC: 0.08sec CImpact: ERROR/TIMEOUT[8] 290.59sec ESBMC: 0.08sec Threader-monolithic: ERROR/TIMEOUT[1] 0.11sec Threader-owicki-gries: ERROR/TIMEOUT[1] 0.12sec Threader-rely-guarantee: ERROR/TIMEOUT[1] 0.10sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT |
Cycles
SatAbs: 6.76sec (x.86) Satabs-prefix-first: 6.65sec CBMC-WMM: 0.19sec CBMC-SC: 0.08sec CImpact: ERROR/TIMEOUT[8] 287.34sec ESBMC: 0.14sec Threader-monolithic: ERROR/TIMEOUT[1] 0.11sec Threader-owicki-gries: ERROR/TIMEOUT[1] 0.06sec Threader-rely-guarantee: ERROR/TIMEOUT[1] 0.11sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT |
Cycles
SatAbs: 6.57sec (x.83) Satabs-prefix-first: 6.30sec CBMC-WMM: 0.22sec CBMC-SC: 0.08sec CImpact: ERROR/TIMEOUT[8] 310.32sec ESBMC: 0.07sec Threader-monolithic: ERROR/TIMEOUT[1] 0.11sec Threader-owicki-gries: ERROR/TIMEOUT[1] 0.12sec Threader-rely-guarantee: ERROR/TIMEOUT[1] 0.11sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT |
Cycles
SatAbs: 6.36sec (x.81) Satabs-prefix-first: 6.38sec CBMC-WMM: 0.18sec CBMC-SC: 0.07sec CImpact: ERROR/TIMEOUT[8] 316.62sec ESBMC: 0.06sec Threader-monolithic: ERROR/TIMEOUT[1] 0.11sec Threader-owicki-gries: ERROR/TIMEOUT[1] 0.12sec Threader-rely-guarantee: ERROR/TIMEOUT[1] 0.11sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT |
||||
ppc/aclwsrr002 |
SatAbs: 1.57sec Satabs-prefix-first: 2.21sec CBMC-WMM: 0.06sec CBMC-SC: 0.06sec CImpact: 2.74sec Checkfence: 0.01sec ESBMC: 0.10sec 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[1] 0.09sec |
Cycles
SatAbs: 21.04sec (x13.40) Satabs-prefix-first: 36.76sec CBMC-WMM: 0.11sec CBMC-SC: 13.37sec CImpact: ERROR/TIMEOUT[8] 362.50sec ESBMC: 0.11sec Threader-monolithic: ERROR/TIMEOUT[130] 896.83sec Threader-owicki-gries: ERROR/TIMEOUT[130] 897.10sec Threader-rely-guarantee: ERROR/TIMEOUT[130] 896.71sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT MMChecker (MM: csharp): ERROR/TIMEOUT[1] 0.10sec |
Cycles
SatAbs: 5.94sec (x3.78) Satabs-prefix-first: 3.50sec CBMC-WMM: 0.13sec CBMC-SC: 0.06sec CImpact: 222.81sec Checkfence: 0.01sec ESBMC: 0.08sec Threader-monolithic: ERROR/TIMEOUT[1] 0.11sec Threader-owicki-gries: ERROR/TIMEOUT[1] 0.11sec Threader-rely-guarantee: ERROR/TIMEOUT[1] 0.12sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT MMChecker (MM: csharp): ERROR/TIMEOUT[1] 0.09sec |
Cycles
SatAbs: 5.35sec (x3.40) Satabs-prefix-first: 3.28sec CBMC-WMM: 0.10sec CBMC-SC: 0.04sec CImpact: 195.64sec ESBMC: 0.06sec Threader-monolithic: ERROR/TIMEOUT[1] 0.09sec Threader-owicki-gries: ERROR/TIMEOUT[1] 0.12sec Threader-rely-guarantee: ERROR/TIMEOUT[1] 0.09sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT MMChecker (MM: csharp): ERROR/TIMEOUT[1] 0.09sec |
Cycles
SatAbs: 3.82sec (x2.43) Satabs-prefix-first: 2.49sec CBMC-WMM: 0.10sec CBMC-SC: 0.06sec CImpact: 159.16sec ESBMC: 0.08sec Threader-monolithic: ERROR/TIMEOUT[1] 0.12sec Threader-owicki-gries: ERROR/TIMEOUT[1] 0.12sec Threader-rely-guarantee: ERROR/TIMEOUT[1] 0.11sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT MMChecker (MM: csharp): ERROR/TIMEOUT[1] 0.10sec |
Cycles
SatAbs: 5.37sec (x3.42) Satabs-prefix-first: 3.37sec CBMC-WMM: 0.13sec CBMC-SC: 0.05sec CImpact: 167.65sec ESBMC: 0.08sec Threader-monolithic: ERROR/TIMEOUT[1] 0.10sec Threader-owicki-gries: ERROR/TIMEOUT[1] 0.11sec Threader-rely-guarantee: ERROR/TIMEOUT[1] 0.08sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT Blender: |
Cycles
SatAbs: 5.44sec (x3.46) Satabs-prefix-first: 3.09sec CBMC-WMM: 0.10sec CBMC-SC: 0.05sec CImpact: 195.57sec ESBMC: 0.07sec Threader-monolithic: ERROR/TIMEOUT[1] 0.08sec Threader-owicki-gries: ERROR/TIMEOUT[1] 0.12sec Threader-rely-guarantee: ERROR/TIMEOUT[1] 0.12sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT Blender: |
Cycles
SatAbs: 5.56sec (x3.54) Satabs-prefix-first: 3.18sec CBMC-WMM: 0.12sec CBMC-SC: 0.05sec CImpact: 205.83sec ESBMC: 0.05sec Threader-monolithic: ERROR/TIMEOUT[1] 0.11sec Threader-owicki-gries: ERROR/TIMEOUT[1] 0.11sec Threader-rely-guarantee: ERROR/TIMEOUT[1] 0.12sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT Blender: |
Cycles
SatAbs: 5.27sec (x3.35) Satabs-prefix-first: 3.37sec CBMC-WMM: 0.15sec CBMC-SC: 0.06sec CImpact: 165.40sec ESBMC: 0.07sec Threader-monolithic: ERROR/TIMEOUT[1] 0.12sec Threader-owicki-gries: ERROR/TIMEOUT[1] 0.11sec Threader-rely-guarantee: ERROR/TIMEOUT[1] 0.11sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT |
Cycles
SatAbs: 5.15sec (x3.28) Satabs-prefix-first: 3.32sec CBMC-WMM: 0.08sec CBMC-SC: 0.03sec CImpact: 208.94sec ESBMC: 0.07sec Threader-monolithic: ERROR/TIMEOUT[1] 0.09sec Threader-owicki-gries: ERROR/TIMEOUT[1] 0.11sec Threader-rely-guarantee: ERROR/TIMEOUT[1] 0.10sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT |
Cycles
SatAbs: 5.47sec (x3.48) Satabs-prefix-first: 4.46sec CBMC-WMM: 0.16sec CBMC-SC: 0.05sec CImpact: 187.71sec ESBMC: 0.04sec 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: 5.57sec (x3.54) Satabs-prefix-first: 3.94sec CBMC-WMM: 0.15sec CBMC-SC: 0.06sec CImpact: 176.61sec ESBMC: 0.06sec Threader-monolithic: ERROR/TIMEOUT[1] 0.12sec Threader-owicki-gries: ERROR/TIMEOUT[1] 0.12sec Threader-rely-guarantee: ERROR/TIMEOUT[1] 0.10sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT |
Cycles
SatAbs: 5.46sec (x3.47) Satabs-prefix-first: 3.41sec CBMC-WMM: 0.15sec CBMC-SC: 0.06sec CImpact: 164.02sec ESBMC: 0.08sec Threader-monolithic: ERROR/TIMEOUT[1] 0.11sec Threader-owicki-gries: ERROR/TIMEOUT[1] 0.12sec Threader-rely-guarantee: ERROR/TIMEOUT[1] 0.11sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT |
Cycles
SatAbs: 5.54sec (x3.52) Satabs-prefix-first: 3.47sec CBMC-WMM: 0.15sec CBMC-SC: 0.06sec CImpact: 180.98sec ESBMC: 0.06sec Threader-monolithic: ERROR/TIMEOUT[1] 0.10sec Threader-owicki-gries: ERROR/TIMEOUT[1] 0.12sec Threader-rely-guarantee: ERROR/TIMEOUT[1] 0.11sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT |