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/rfi (tooling date Sun Jan 22 02:23:23 GMT 2012)
This family corresponds to litmus tests showing that Power authorises store buffering. 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/rfi000 |
SatAbs: ![]() 5.47sec 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.11sec |
Cycles
SatAbs: ![]() 9.46sec (x1.72) Satabs-prefix-first: ![]() CBMC-WMM: ![]() CBMC-SC: ![]() CImpact: ![]() ESBMC: ![]() Threader-monolithic: ERROR/TIMEOUT[130] 897.04sec Threader-owicki-gries: ERROR/TIMEOUT[130] 896.78sec Threader-rely-guarantee: ERROR/TIMEOUT[130] 896.35sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT MMChecker (MM: csharp): ERROR/TIMEOUT[1] 0.10sec |
Cycles
SatAbs: ![]() 11.74sec (x2.14) Satabs-prefix-first: ![]() CBMC-WMM: ![]() CBMC-SC: ![]() CImpact: ![]() Checkfence: 0.01sec ESBMC: ![]() Threader-monolithic: ERROR/TIMEOUT[130] 896.71sec Threader-owicki-gries: ERROR/TIMEOUT[130] 896.35sec Threader-rely-guarantee: ERROR/TIMEOUT[130] 896.33sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT MMChecker (MM: csharp): ERROR/TIMEOUT[1] 0.09sec |
Cycles
SatAbs: ![]() 5.33sec (x.97) Satabs-prefix-first: ![]() CBMC-WMM: ![]() CBMC-SC: ![]() CImpact: ![]() ESBMC: ![]() Threader-monolithic: ERROR/TIMEOUT[1] 197.61sec Threader-owicki-gries: ERROR/TIMEOUT[1] 263.67sec Threader-rely-guarantee: ERROR/TIMEOUT[1] 245.10sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT MMChecker (MM: csharp): ERROR/TIMEOUT[1] 0.09sec |
Cycles
SatAbs: ![]() 18.18sec (x3.32) Satabs-prefix-first: ![]() CBMC-WMM: ![]() CBMC-SC: ![]() CImpact: ![]() ESBMC: ![]() Threader-monolithic: ERROR/TIMEOUT[1] 262.71sec Threader-owicki-gries: ERROR/TIMEOUT[1] 262.79sec Threader-rely-guarantee: ERROR/TIMEOUT[1] 246.05sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT MMChecker (MM: csharp): ERROR/TIMEOUT[1] 0.10sec |
![]() |
Cycles
SatAbs: ![]() 9.98sec (x1.82) Satabs-prefix-first: ![]() CBMC-WMM: ![]() CBMC-SC: ![]() CImpact: ![]() ESBMC: ![]() Threader-monolithic: ERROR/TIMEOUT[130] 896.18sec Threader-owicki-gries: ERROR/TIMEOUT[130] 896.91sec Threader-rely-guarantee: ERROR/TIMEOUT[130] 896.60sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT Blender: ![]() |
Cycles
SatAbs: ![]() 5.65sec (x1.03) Satabs-prefix-first: ![]() CBMC-WMM: ![]() CBMC-SC: ![]() CImpact: ![]() ESBMC: ![]() Threader-monolithic: ERROR/TIMEOUT[1] 234.88sec Threader-owicki-gries: ERROR/TIMEOUT[1] 255.87sec Threader-rely-guarantee: ERROR/TIMEOUT[1] 261.45sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT Blender: ![]() |
Cycles
SatAbs: ![]() 27.38sec (x5.00) Satabs-prefix-first: ![]() CBMC-WMM: ![]() CBMC-SC: ![]() CImpact: ![]() ESBMC: ![]() Threader-monolithic: ERROR/TIMEOUT[1] 183.09sec Threader-owicki-gries: ERROR/TIMEOUT[1] 205.12sec Threader-rely-guarantee: ERROR/TIMEOUT[1] 196.19sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT Blender: ![]() |
![]() |
Cycles
SatAbs: ![]() 10.12sec (x1.85) Satabs-prefix-first: ![]() CBMC-WMM: ![]() CBMC-SC: ![]() CImpact: ![]() ESBMC: ![]() Threader-monolithic: ERROR/TIMEOUT[130] 896.92sec Threader-owicki-gries: ERROR/TIMEOUT[130] 897.14sec Threader-rely-guarantee: ERROR/TIMEOUT[130] 896.08sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT |
Cycles
SatAbs: ![]() 5.56sec (x1.01) Satabs-prefix-first: ![]() CBMC-WMM: ![]() CBMC-SC: ![]() CImpact: ![]() ESBMC: ![]() Threader-monolithic: ERROR/TIMEOUT[1] 203.12sec Threader-owicki-gries: ERROR/TIMEOUT[1] 248.57sec Threader-rely-guarantee: ERROR/TIMEOUT[1] 255.89sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT |
Cycles
SatAbs: ![]() 17.36sec (x3.17) Satabs-prefix-first: ![]() CBMC-WMM: ![]() CBMC-SC: ![]() CImpact: ![]() ESBMC: ![]() Threader-monolithic: ERROR/TIMEOUT[1] 262.72sec Threader-owicki-gries: ERROR/TIMEOUT[1] 260.67sec Threader-rely-guarantee: ERROR/TIMEOUT[1] 188.37sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT |
![]() |
Cycles
SatAbs: ![]() 9.09sec (x1.66) Satabs-prefix-first: ![]() CBMC-WMM: ![]() CBMC-SC: ![]() CImpact: ![]() ESBMC: ![]() Threader-monolithic: ERROR/TIMEOUT[130] 896.59sec Threader-owicki-gries: ERROR/TIMEOUT[130] 897.08sec Threader-rely-guarantee: ERROR/TIMEOUT[130] 897.16sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT |
Cycles
SatAbs: ![]() 4.94sec (x.90) Satabs-prefix-first: ![]() CBMC-WMM: ![]() CBMC-SC: ![]() CImpact: ![]() ESBMC: ![]() Threader-monolithic: ERROR/TIMEOUT[1] 249.56sec Threader-owicki-gries: ERROR/TIMEOUT[1] 254.50sec Threader-rely-guarantee: ERROR/TIMEOUT[1] 244.50sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT |
Cycles
SatAbs: ![]() 17.37sec (x3.17) Satabs-prefix-first: ![]() CBMC-WMM: ![]() CBMC-SC: ![]() CImpact: ![]() ESBMC: ![]() Threader-monolithic: ERROR/TIMEOUT[1] 259.00sec Threader-owicki-gries: ERROR/TIMEOUT[1] 252.71sec Threader-rely-guarantee: ERROR/TIMEOUT[1] 263.20sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT |
![]() |
ppc/rfi001 |
SatAbs: ![]() 8.56sec 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: ![]() 2.37sec (x.27) Satabs-prefix-first: ![]() CBMC-WMM: ![]() CBMC-SC: ![]() CImpact: ![]() ESBMC: ![]() Threader-monolithic: ERROR/TIMEOUT[130] 897.43sec Threader-owicki-gries: ERROR/TIMEOUT[130] 897.29sec Threader-rely-guarantee: ERROR/TIMEOUT[130] 897.22sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT MMChecker (MM: csharp): ERROR/TIMEOUT[1] 0.10sec |
Cycles
SatAbs: ![]() 15.30sec (x1.78) Satabs-prefix-first: ![]() CBMC-WMM: ![]() CBMC-SC: ![]() CImpact: ![]() Checkfence: 0.01sec ESBMC: ![]() Threader-monolithic: ERROR/TIMEOUT[130] 897.53sec Threader-owicki-gries: ERROR/TIMEOUT[130] 897.55sec Threader-rely-guarantee: ERROR/TIMEOUT[130] 897.58sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT MMChecker (MM: csharp): ERROR/TIMEOUT[1] 0.09sec |
Cycles
SatAbs: ![]() 14.90sec (x1.74) Satabs-prefix-first: ![]() CBMC-WMM: ![]() CBMC-SC: ![]() CImpact: ![]() ESBMC: ![]() Threader-monolithic: ERROR/TIMEOUT[130] 897.33sec Threader-owicki-gries: ERROR/TIMEOUT[130] 897.48sec Threader-rely-guarantee: ERROR/TIMEOUT[130] 897.48sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT MMChecker (MM: csharp): ERROR/TIMEOUT[1] 0.09sec |
Cycles
SatAbs: ![]() 14.93sec (x1.74) Satabs-prefix-first: ![]() CBMC-WMM: ![]() CBMC-SC: ![]() CImpact: ![]() ESBMC: ![]() Threader-monolithic: ERROR/TIMEOUT[130] 897.31sec Threader-owicki-gries: ERROR/TIMEOUT[130] 897.31sec Threader-rely-guarantee: ERROR/TIMEOUT[130] 897.26sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT MMChecker (MM: csharp): ERROR/TIMEOUT[1] 0.10sec |
![]() |
Cycles
SatAbs: ![]() 15.94sec (x1.86) Satabs-prefix-first: ![]() CBMC-WMM: ![]() CBMC-SC: ![]() CImpact: ![]() ESBMC: ![]() Threader-monolithic: ERROR/TIMEOUT[130] 897.51sec Threader-owicki-gries: ERROR/TIMEOUT[130] 897.48sec Threader-rely-guarantee: ERROR/TIMEOUT[130] 897.36sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT Blender: ![]() |
Cycles
SatAbs: ![]() 14.83sec (x1.73) Satabs-prefix-first: ![]() CBMC-WMM: ![]() CBMC-SC: ![]() CImpact: ![]() ESBMC: ![]() Threader-monolithic: ERROR/TIMEOUT[130] 897.10sec Threader-owicki-gries: ERROR/TIMEOUT[130] 897.08sec Threader-rely-guarantee: ERROR/TIMEOUT[130] 897.11sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT Blender: ![]() |
Cycles
SatAbs: ![]() 32.64sec (x3.81) Satabs-prefix-first: ![]() CBMC-WMM: ![]() CBMC-SC: ![]() CImpact: ![]() ESBMC: ![]() Threader-monolithic: ERROR/TIMEOUT[1] 263.03sec Threader-owicki-gries: ERROR/TIMEOUT[1] 224.32sec Threader-rely-guarantee: ERROR/TIMEOUT[1] 255.14sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT Blender: ![]() |
![]() |
Cycles
SatAbs: ![]() 14.22sec (x1.66) Satabs-prefix-first: ![]() CBMC-WMM: ![]() CBMC-SC: ![]() CImpact: ![]() ESBMC: ![]() Threader-monolithic: ERROR/TIMEOUT[130] 897.41sec Threader-owicki-gries: ERROR/TIMEOUT[130] 896.84sec Threader-rely-guarantee: ERROR/TIMEOUT[130] 897.17sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT |
Cycles
SatAbs: ![]() 16.90sec (x1.97) Satabs-prefix-first: ![]() CBMC-WMM: ![]() CBMC-SC: ![]() CImpact: ![]() ESBMC: ![]() Threader-monolithic: ERROR/TIMEOUT[130] 897.34sec Threader-owicki-gries: ERROR/TIMEOUT[130] 897.27sec Threader-rely-guarantee: ERROR/TIMEOUT[130] 897.35sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT |
Cycles
SatAbs: ![]() 35.25sec (x4.11) Satabs-prefix-first: ![]() CBMC-WMM: ![]() CBMC-SC: ![]() CImpact: ![]() ESBMC: ![]() Threader-monolithic: ERROR/TIMEOUT[1] 259.81sec Threader-owicki-gries: ERROR/TIMEOUT[1] 259.83sec Threader-rely-guarantee: ERROR/TIMEOUT[1] 260.95sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT |
![]() |
Cycles
SatAbs: ![]() 9.28sec (x1.08) Satabs-prefix-first: ![]() CBMC-WMM: ![]() CBMC-SC: ![]() CImpact: ![]() ESBMC: ![]() Threader-monolithic: ERROR/TIMEOUT[130] 897.55sec Threader-owicki-gries: ERROR/TIMEOUT[130] 897.31sec Threader-rely-guarantee: ERROR/TIMEOUT[130] 896.59sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT |
Cycles
SatAbs: ![]() 15.00sec (x1.75) Satabs-prefix-first: ![]() CBMC-WMM: ![]() CBMC-SC: ![]() CImpact: ![]() ESBMC: ![]() Threader-monolithic: ERROR/TIMEOUT[130] 897.00sec Threader-owicki-gries: ERROR/TIMEOUT[130] 897.58sec Threader-rely-guarantee: ERROR/TIMEOUT[130] 897.48sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT |
Cycles
SatAbs: ![]() 32.49sec (x3.79) Satabs-prefix-first: ![]() CBMC-WMM: ![]() CBMC-SC: ![]() CImpact: ![]() ESBMC: ![]() Threader-monolithic: ERROR/TIMEOUT[1] 218.85sec Threader-owicki-gries: ERROR/TIMEOUT[1] 234.35sec Threader-rely-guarantee: ERROR/TIMEOUT[1] 211.84sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT |
![]() |
ppc/rfi002 |
SatAbs: ![]() 10.60sec 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.11sec |
Cycles
SatAbs: ![]() 3.39sec (x.31) Satabs-prefix-first: ![]() CBMC-WMM: ![]() CBMC-SC: ![]() CImpact: ![]() ESBMC: ![]() Threader-monolithic: ERROR/TIMEOUT[130] 897.57sec Threader-owicki-gries: ERROR/TIMEOUT[130] 897.43sec Threader-rely-guarantee: ERROR/TIMEOUT[130] 897.10sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT MMChecker (MM: csharp): ERROR/TIMEOUT[1] 0.10sec |
Cycles
SatAbs: ![]() 2.15sec (x.20) Satabs-prefix-first: ![]() CBMC-WMM: ![]() CBMC-SC: ![]() CImpact: ERROR/TIMEOUT[8] 242.96sec Checkfence: 0.01sec 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 MMChecker (MM: csharp): ERROR/TIMEOUT[1] 0.09sec |
Cycles
SatAbs: ![]() 2.30sec (x.21) Satabs-prefix-first: ![]() CBMC-WMM: ![]() CBMC-SC: ![]() CImpact: ERROR/TIMEOUT[8] 241.25sec 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: ![]() 2.12sec (x.20) Satabs-prefix-first: ![]() CBMC-WMM: ![]() CBMC-SC: ![]() CImpact: ERROR/TIMEOUT[8] 240.01sec ESBMC: ![]() Threader-monolithic: ERROR/TIMEOUT[1] 0.12sec Threader-owicki-gries: ERROR/TIMEOUT[1] 0.09sec Threader-rely-guarantee: ERROR/TIMEOUT[1] 0.11sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT MMChecker (MM: csharp): ERROR/TIMEOUT[1] 0.10sec |
![]() |
Cycles
SatAbs: ![]() 16.31sec (x1.53) Satabs-prefix-first: ![]() CBMC-WMM: ![]() CBMC-SC: ![]() CImpact: ![]() ESBMC: ![]() Threader-monolithic: ERROR/TIMEOUT[130] 897.58sec Threader-owicki-gries: ERROR/TIMEOUT[130] 896.48sec Threader-rely-guarantee: ERROR/TIMEOUT[130] 895.75sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT Blender: ![]() |
Cycles
SatAbs: ![]() 17.67sec (x1.66) Satabs-prefix-first: ![]() CBMC-WMM: ![]() CBMC-SC: ![]() CImpact: ![]() ESBMC: ![]() Threader-monolithic: ERROR/TIMEOUT[130] 897.37sec Threader-owicki-gries: ERROR/TIMEOUT[130] 896.08sec Threader-rely-guarantee: ERROR/TIMEOUT[130] 897.41sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT Blender: ![]() |
Cycles
SatAbs: ![]() 16.96sec (x1.60) Satabs-prefix-first: ![]() CBMC-WMM: ![]() CBMC-SC: ![]() CImpact: ![]() ESBMC: ![]() Threader-monolithic: ERROR/TIMEOUT[130] 897.68sec Threader-owicki-gries: ERROR/TIMEOUT[130] 897.42sec Threader-rely-guarantee: ERROR/TIMEOUT[130] 896.94sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT Blender: ![]() |
![]() |
Cycles
SatAbs: ![]() 16.48sec (x1.55) Satabs-prefix-first: ![]() CBMC-WMM: ![]() CBMC-SC: ![]() CImpact: ![]() ESBMC: ![]() Threader-monolithic: ERROR/TIMEOUT[130] 897.32sec Threader-owicki-gries: ERROR/TIMEOUT[130] 897.27sec Threader-rely-guarantee: ERROR/TIMEOUT[130] 897.58sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT |
Cycles
SatAbs: ![]() 16.47sec (x1.55) Satabs-prefix-first: ![]() CBMC-WMM: ![]() CBMC-SC: ![]() CImpact: ![]() ESBMC: ![]() Threader-monolithic: ERROR/TIMEOUT[130] 897.29sec Threader-owicki-gries: ERROR/TIMEOUT[130] 897.38sec Threader-rely-guarantee: ERROR/TIMEOUT[130] 897.20sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT |
Cycles
SatAbs: ![]() 16.60sec (x1.56) Satabs-prefix-first: ![]() CBMC-WMM: ![]() CBMC-SC: ![]() CImpact: ![]() ESBMC: ![]() Threader-monolithic: ERROR/TIMEOUT[130] 897.53sec Threader-owicki-gries: ERROR/TIMEOUT[130] 897.52sec Threader-rely-guarantee: ERROR/TIMEOUT[130] 896.99sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT |
![]() |
Cycles
SatAbs: ![]() 19.73sec (x1.86) Satabs-prefix-first: ![]() CBMC-WMM: ![]() CBMC-SC: ![]() CImpact: ![]() ESBMC: ![]() Threader-monolithic: ERROR/TIMEOUT[130] 897.41sec Threader-owicki-gries: ERROR/TIMEOUT[130] 897.63sec Threader-rely-guarantee: ERROR/TIMEOUT[130] 897.66sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT |
Cycles
SatAbs: ![]() 10.63sec (x1.00) Satabs-prefix-first: ![]() CBMC-WMM: ![]() CBMC-SC: ![]() CImpact: ![]() ESBMC: ![]() Threader-monolithic: ERROR/TIMEOUT[130] 897.55sec Threader-owicki-gries: ERROR/TIMEOUT[130] 897.67sec Threader-rely-guarantee: ERROR/TIMEOUT[130] 897.49sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT |
Cycles
SatAbs: ![]() 5.00sec (x.47) Satabs-prefix-first: ![]() CBMC-WMM: ![]() CBMC-SC: ![]() CImpact: ![]() ESBMC: ![]() Threader-monolithic: ERROR/TIMEOUT[130] 896.73sec Threader-owicki-gries: ERROR/TIMEOUT[130] 897.24sec Threader-rely-guarantee: ERROR/TIMEOUT[130] 897.31sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT |
![]() |