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/posrr (tooling date Sun Jan 22 02:23:23 GMT 2012)
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/posrr000 |
SatAbs: 0.78sec Satabs-prefix-first: 0.42sec CBMC-WMM: 0.05sec CBMC-SC: 0.05sec CImpact: 4.54sec Checkfence: 0.01sec ESBMC: 0.07sec Threader-monolithic: 0.15sec Threader-owicki-gries: 0.14sec Threader-rely-guarantee: 0.15sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT MMChecker (MM: sc): ERROR/TIMEOUT[1] 0.09sec |
Cycles
SatAbs: 29.53sec (x37.85) Satabs-prefix-first: 49.63sec CBMC-WMM: 0.10sec CBMC-SC: 19.77sec CImpact: ERROR/TIMEOUT[8] 440.68sec ESBMC: 0.11sec Threader-monolithic: ERROR/TIMEOUT[130] 896.97sec Threader-owicki-gries: ERROR/TIMEOUT[130] 896.83sec Threader-rely-guarantee: ERROR/TIMEOUT[130] 896.46sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT MMChecker (MM: csharp): ERROR/TIMEOUT[1] 0.10sec |
Cycles
SatAbs: 1.00sec (x1.28) Satabs-prefix-first: 1.55sec CBMC-WMM: 0.13sec CBMC-SC: 0.07sec CImpact: ERROR/TIMEOUT[8] 229.29sec Checkfence: 0.01sec ESBMC: 0.08sec Threader-monolithic: ERROR/TIMEOUT[1] 0.08sec 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: 1.24sec (x1.58) Satabs-prefix-first: 1.52sec CBMC-WMM: 0.12sec CBMC-SC: 0.05sec CImpact: ERROR/TIMEOUT[8] 239.55sec ESBMC: 0.08sec Threader-monolithic: ERROR/TIMEOUT[1] 0.11sec Threader-owicki-gries: ERROR/TIMEOUT[1] 0.06sec Threader-rely-guarantee: ERROR/TIMEOUT[1] 0.08sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT MMChecker (MM: csharp): ERROR/TIMEOUT[1] 0.10sec |
Cycles
SatAbs: 0.91sec (x1.16) Satabs-prefix-first: 1.40sec CBMC-WMM: 0.12sec CBMC-SC: 0.07sec CImpact: ERROR/TIMEOUT[8] 260.08sec ESBMC: 0.05sec Threader-monolithic: ERROR/TIMEOUT[1] 0.09sec Threader-owicki-gries: ERROR/TIMEOUT[1] 0.11sec Threader-rely-guarantee: ERROR/TIMEOUT[1] 0.11sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT MMChecker (MM: csharp): ERROR/TIMEOUT[1] 0.10sec |
Cycles
SatAbs: 0.93sec (x1.19) Satabs-prefix-first: 1.39sec CBMC-WMM: 0.13sec CBMC-SC: 0.07sec CImpact: ERROR/TIMEOUT[8] 236.86sec 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.12sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT Blender: |
Cycles
SatAbs: 0.88sec (x1.12) Satabs-prefix-first: 1.39sec CBMC-WMM: 0.11sec CBMC-SC: 0.07sec CImpact: ERROR/TIMEOUT[8] 238.60sec ESBMC: 0.07sec 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 Blender: |
Cycles
SatAbs: 1.00sec (x1.28) Satabs-prefix-first: 1.41sec CBMC-WMM: 0.12sec CBMC-SC: 0.07sec CImpact: ERROR/TIMEOUT[8] 237.69sec 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.10sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT Blender: |
Cycles
SatAbs: 132.49sec (x169.85) Satabs-prefix-first: 165.78sec CBMC-WMM: 0.12sec CBMC-SC: 1.46sec CImpact: 129.20sec ESBMC: 0.10sec Threader-monolithic: ERROR/TIMEOUT[1] 411.00sec Threader-owicki-gries: ERROR/TIMEOUT[1] 386.19sec Threader-rely-guarantee: ERROR/TIMEOUT[1] 436.57sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT |
Cycles
SatAbs: 132.41sec (x169.75) Satabs-prefix-first: 184.14sec CBMC-WMM: 0.13sec CBMC-SC: 1.51sec CImpact: 95.06sec ESBMC: 0.09sec Threader-monolithic: ERROR/TIMEOUT[1] 373.61sec Threader-owicki-gries: ERROR/TIMEOUT[1] 299.08sec Threader-rely-guarantee: ERROR/TIMEOUT[1] 400.95sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT |
Cycles
SatAbs: 142.37sec (x182.52) Satabs-prefix-first: 210.49sec CBMC-WMM: 0.13sec CBMC-SC: 1.74sec CImpact: 117.89sec ESBMC: 0.13sec Threader-monolithic: ERROR/TIMEOUT[1] 445.78sec Threader-owicki-gries: ERROR/TIMEOUT[1] 410.32sec Threader-rely-guarantee: ERROR/TIMEOUT[1] 362.26sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT |
Cycles
SatAbs: 79.43sec (x101.83) Satabs-prefix-first: 56.66sec CBMC-WMM: 0.15sec CBMC-SC: 2.62sec CImpact: 128.43sec ESBMC: 0.11sec Threader-monolithic: ERROR/TIMEOUT[1] 342.40sec Threader-owicki-gries: ERROR/TIMEOUT[1] 326.69sec Threader-rely-guarantee: ERROR/TIMEOUT[1] 354.88sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT |
Cycles
SatAbs: 85.12sec (x109.12) Satabs-prefix-first: 60.10sec CBMC-WMM: 0.14sec CBMC-SC: 2.59sec CImpact: 127.48sec ESBMC: 0.11sec Threader-monolithic: ERROR/TIMEOUT[1] 453.64sec Threader-owicki-gries: ERROR/TIMEOUT[1] 413.63sec Threader-rely-guarantee: ERROR/TIMEOUT[1] 325.55sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT |
Cycles
SatAbs: 81.10sec (x103.97) Satabs-prefix-first: 54.80sec CBMC-WMM: 0.15sec CBMC-SC: 2.82sec CImpact: 87.45sec ESBMC: 0.09sec Threader-monolithic: ERROR/TIMEOUT[1] 448.36sec Threader-owicki-gries: ERROR/TIMEOUT[1] 449.87sec Threader-rely-guarantee: ERROR/TIMEOUT[1] 447.58sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT |
||||
ppc/posrr001 |
SatAbs: 0.74sec Satabs-prefix-first: 0.39sec CBMC-WMM: 0.06sec CBMC-SC: 0.06sec CImpact: 2.37sec Checkfence: 0.01sec ESBMC: 0.06sec Threader-monolithic: 0.13sec Threader-owicki-gries: 0.13sec Threader-rely-guarantee: 0.14sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT MMChecker (MM: sc): ERROR/TIMEOUT[1] 0.09sec |
Cycles
SatAbs: 26.25sec (x35.47) Satabs-prefix-first: 38.28sec CBMC-WMM: 0.12sec CBMC-SC: 16.62sec CImpact: ERROR/TIMEOUT[8] 253.26sec ESBMC: 0.09sec Threader-monolithic: ERROR/TIMEOUT[130] 896.35sec Threader-owicki-gries: ERROR/TIMEOUT[130] 897.08sec Threader-rely-guarantee: ERROR/TIMEOUT[130] 897.00sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT MMChecker (MM: csharp): ERROR/TIMEOUT[1] 0.10sec |
Cycles
SatAbs: 0.94sec (x1.27) Satabs-prefix-first: 1.14sec CBMC-WMM: 0.12sec CBMC-SC: 0.05sec CImpact: 220.97sec Checkfence: 0.01sec ESBMC: 0.07sec Threader-monolithic: ERROR/TIMEOUT[1] 0.11sec Threader-owicki-gries: ERROR/TIMEOUT[1] 0.11sec Threader-rely-guarantee: ERROR/TIMEOUT[1] 0.11sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT MMChecker (MM: csharp): ERROR/TIMEOUT[1] 0.10sec |
Cycles
SatAbs: 1.00sec (x1.35) Satabs-prefix-first: 1.36sec CBMC-WMM: 0.12sec CBMC-SC: 0.06sec CImpact: 214.30sec 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.11sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT MMChecker (MM: csharp): ERROR/TIMEOUT[1] 0.09sec |
Cycles
SatAbs: 0.94sec (x1.27) Satabs-prefix-first: 1.29sec CBMC-WMM: 0.11sec CBMC-SC: 0.06sec CImpact: 199.27sec ESBMC: 0.05sec Threader-monolithic: ERROR/TIMEOUT[1] 0.10sec Threader-owicki-gries: ERROR/TIMEOUT[1] 0.12sec Threader-rely-guarantee: ERROR/TIMEOUT[1] 0.11sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT MMChecker (MM: csharp): ERROR/TIMEOUT[1] 0.10sec |
Cycles
SatAbs: 1.01sec (x1.36) Satabs-prefix-first: 1.40sec CBMC-WMM: 0.10sec CBMC-SC: 0.06sec CImpact: 230.41sec ESBMC: 0.06sec Threader-monolithic: ERROR/TIMEOUT[1] 0.10sec 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: 0.95sec (x1.28) Satabs-prefix-first: 1.54sec CBMC-WMM: 0.10sec CBMC-SC: 0.06sec CImpact: 190.57sec ESBMC: 0.07sec 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 Blender: |
Cycles
SatAbs: 1.02sec (x1.37) Satabs-prefix-first: 1.39sec CBMC-WMM: 0.12sec CBMC-SC: 0.05sec CImpact: 245.62sec ESBMC: 0.07sec Threader-monolithic: ERROR/TIMEOUT[1] 0.12sec Threader-owicki-gries: ERROR/TIMEOUT[1] 0.08sec Threader-rely-guarantee: ERROR/TIMEOUT[1] 0.11sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT Blender: |
Cycles
SatAbs: 3.51sec (x4.74) Satabs-prefix-first: 22.12sec CBMC-WMM: 0.10sec CBMC-SC: 0.74sec CImpact: 58.13sec ESBMC: 0.08sec Threader-monolithic: ERROR/TIMEOUT[1] 300.26sec Threader-owicki-gries: ERROR/TIMEOUT[1] 340.93sec Threader-rely-guarantee: ERROR/TIMEOUT[1] 284.46sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT |
Cycles
SatAbs: 4.60sec (x6.21) Satabs-prefix-first: 24.89sec CBMC-WMM: 0.13sec CBMC-SC: 0.79sec CImpact: 64.85sec ESBMC: 0.08sec Threader-monolithic: ERROR/TIMEOUT[1] 327.56sec Threader-owicki-gries: ERROR/TIMEOUT[1] 382.24sec Threader-rely-guarantee: ERROR/TIMEOUT[1] 381.24sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT |
Cycles
SatAbs: 3.51sec (x4.74) Satabs-prefix-first: 23.42sec CBMC-WMM: 0.10sec CBMC-SC: 0.75sec CImpact: 58.34sec ESBMC: 0.08sec Threader-monolithic: ERROR/TIMEOUT[1] 381.84sec Threader-owicki-gries: ERROR/TIMEOUT[1] 374.43sec Threader-rely-guarantee: ERROR/TIMEOUT[1] 379.16sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT |
Cycles
SatAbs: 3.57sec (x4.82) Satabs-prefix-first: 12.61sec CBMC-WMM: 0.11sec CBMC-SC: 0.80sec CImpact: 57.14sec ESBMC: 0.09sec Threader-monolithic: ERROR/TIMEOUT[1] 323.10sec Threader-owicki-gries: ERROR/TIMEOUT[1] 369.01sec Threader-rely-guarantee: ERROR/TIMEOUT[1] 290.72sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT |
Cycles
SatAbs: 3.67sec (x4.95) Satabs-prefix-first: 13.16sec CBMC-WMM: 0.12sec CBMC-SC: 0.80sec CImpact: 59.73sec ESBMC: 0.09sec Threader-monolithic: ERROR/TIMEOUT[1] 287.69sec Threader-owicki-gries: ERROR/TIMEOUT[1] 272.31sec Threader-rely-guarantee: ERROR/TIMEOUT[1] 278.28sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT |
Cycles
SatAbs: 3.77sec (x5.09) Satabs-prefix-first: 12.33sec CBMC-WMM: 0.14sec CBMC-SC: 0.82sec CImpact: 62.91sec ESBMC: 0.10sec Threader-monolithic: ERROR/TIMEOUT[1] 329.90sec Threader-owicki-gries: ERROR/TIMEOUT[1] 314.07sec Threader-rely-guarantee: ERROR/TIMEOUT[1] 351.69sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT |
||||
ppc/posrr002 |
SatAbs: 1.35sec Satabs-prefix-first: 1.66sec CBMC-WMM: 0.07sec CBMC-SC: 0.06sec CImpact: 8.81sec Checkfence: 0.01sec ESBMC: 0.07sec Threader-monolithic: 0.13sec Threader-owicki-gries: 0.16sec Threader-rely-guarantee: 0.15sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT MMChecker (MM: sc): ERROR/TIMEOUT[1] 0.09sec |
Cycles
SatAbs: 34.18sec (x25.31) Satabs-prefix-first: 34.93sec CBMC-WMM: 0.13sec CBMC-SC: 10.17sec CImpact: ERROR/TIMEOUT[8] 365.07sec ESBMC: 0.12sec Threader-monolithic: ERROR/TIMEOUT[130] 896.31sec Threader-owicki-gries: ERROR/TIMEOUT[130] 896.74sec Threader-rely-guarantee: ERROR/TIMEOUT[130] 896.11sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT MMChecker (MM: csharp): ERROR/TIMEOUT[1] 0.10sec |
Cycles
SatAbs: 2.09sec (x1.54) Satabs-prefix-first: 4.09sec CBMC-WMM: 0.12sec CBMC-SC: 0.07sec CImpact: ERROR/TIMEOUT[8] 231.64sec Checkfence: 0.01sec 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.09sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT MMChecker (MM: csharp): ERROR/TIMEOUT[1] 0.09sec |
Cycles
SatAbs: 2.07sec (x1.53) Satabs-prefix-first: 4.35sec CBMC-WMM: 0.11sec CBMC-SC: 0.07sec CImpact: ERROR/TIMEOUT[8] 206.46sec 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): ERROR/TIMEOUT[1] 0.09sec |
Cycles
SatAbs: 2.26sec (x1.67) Satabs-prefix-first: 4.34sec CBMC-WMM: 0.14sec CBMC-SC: 0.05sec CImpact: ERROR/TIMEOUT[8] 234.99sec ESBMC: 0.07sec 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 MMChecker (MM: csharp): ERROR/TIMEOUT[1] 0.10sec |
Cycles
SatAbs: 2.09sec (x1.54) Satabs-prefix-first: 4.16sec CBMC-WMM: 0.11sec CBMC-SC: 0.07sec CImpact: ERROR/TIMEOUT[8] 224.20sec 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.10sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT Blender: |
Cycles
SatAbs: 2.05sec (x1.51) Satabs-prefix-first: 4.28sec CBMC-WMM: 0.14sec CBMC-SC: 0.07sec CImpact: ERROR/TIMEOUT[8] 256.80sec 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.12sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT Blender: |
Cycles
SatAbs: 2.11sec (x1.56) Satabs-prefix-first: 4.37sec CBMC-WMM: 0.13sec CBMC-SC: 0.06sec CImpact: ERROR/TIMEOUT[8] 236.34sec ESBMC: 0.08sec Threader-monolithic: ERROR/TIMEOUT[1] 0.12sec Threader-owicki-gries: ERROR/TIMEOUT[1] 0.10sec Threader-rely-guarantee: ERROR/TIMEOUT[1] 0.11sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT Blender: |
Cycles
SatAbs: 4.51sec (x3.34) Satabs-prefix-first: 113.43sec CBMC-WMM: 0.16sec CBMC-SC: 2.12sec CImpact: 289.87sec ESBMC: 0.11sec Threader-monolithic: ERROR/TIMEOUT[1] 337.74sec Threader-owicki-gries: ERROR/TIMEOUT[1] 485.97sec Threader-rely-guarantee: ERROR/TIMEOUT[1] 445.89sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT |
Cycles
SatAbs: 5.16sec (x3.82) Satabs-prefix-first: 120.80sec CBMC-WMM: 0.15sec CBMC-SC: 2.47sec CImpact: 231.21sec ESBMC: 0.09sec Threader-monolithic: ERROR/TIMEOUT[1] 362.39sec Threader-owicki-gries: ERROR/TIMEOUT[1] 391.55sec Threader-rely-guarantee: ERROR/TIMEOUT[1] 484.49sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT |
Cycles
SatAbs: 4.50sec (x3.33) Satabs-prefix-first: 113.15sec CBMC-WMM: 0.12sec CBMC-SC: 1.95sec CImpact: 259.73sec ESBMC: 0.09sec Threader-monolithic: ERROR/TIMEOUT[1] 376.49sec Threader-owicki-gries: ERROR/TIMEOUT[1] 469.06sec Threader-rely-guarantee: ERROR/TIMEOUT[1] 445.15sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT |
Cycles
SatAbs: 5.67sec (x4.20) Satabs-prefix-first: 146.77sec CBMC-WMM: 0.20sec CBMC-SC: 2.74sec CImpact: 313.75sec ESBMC: 0.12sec Threader-monolithic: ERROR/TIMEOUT[1] 443.13sec Threader-owicki-gries: ERROR/TIMEOUT[1] 401.53sec Threader-rely-guarantee: ERROR/TIMEOUT[1] 344.67sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT |
Cycles
SatAbs: 5.00sec (x3.70) Satabs-prefix-first: 126.44sec CBMC-WMM: 0.16sec CBMC-SC: 2.43sec CImpact: 289.46sec ESBMC: 0.17sec Threader-monolithic: ERROR/TIMEOUT[1] 454.70sec Threader-owicki-gries: ERROR/TIMEOUT[1] 365.41sec Threader-rely-guarantee: ERROR/TIMEOUT[1] 354.27sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT |
Cycles
SatAbs: 4.84sec (x3.58) Satabs-prefix-first: 116.71sec CBMC-WMM: 0.15sec CBMC-SC: 2.29sec CImpact: 283.77sec ESBMC: 0.10sec Threader-monolithic: ERROR/TIMEOUT[1] 467.28sec Threader-owicki-gries: ERROR/TIMEOUT[1] 491.71sec Threader-rely-guarantee: ERROR/TIMEOUT[1] 470.52sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT |
||||
ppc/posrr003 |
SatAbs: 2.35sec Satabs-prefix-first: 2.08sec CBMC-WMM: 0.05sec CBMC-SC: 0.06sec CImpact: 2.64sec Checkfence: 0.01sec ESBMC: 0.05sec Threader-monolithic: 0.15sec Threader-owicki-gries: 0.11sec Threader-rely-guarantee: 0.13sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT MMChecker (MM: sc): ERROR/TIMEOUT[1] 0.09sec |
Cycles
SatAbs: 21.29sec (x9.05) Satabs-prefix-first: 37.18sec CBMC-WMM: 0.12sec CBMC-SC: 13.99sec CImpact: ERROR/TIMEOUT[8] 275.88sec ESBMC: 0.11sec Threader-monolithic: ERROR/TIMEOUT[130] 897.05sec Threader-owicki-gries: ERROR/TIMEOUT[130] 897.14sec Threader-rely-guarantee: ERROR/TIMEOUT[130] 896.69sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT MMChecker (MM: csharp): ERROR/TIMEOUT[1] 0.10sec |
Cycles
SatAbs: 6.78sec (x2.88) Satabs-prefix-first: 3.39sec CBMC-WMM: 0.11sec CBMC-SC: 0.06sec CImpact: 193.95sec Checkfence: 0.01sec 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.10sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT MMChecker (MM: csharp): ERROR/TIMEOUT[1] 0.09sec |
Cycles
SatAbs: 8.14sec (x3.46) Satabs-prefix-first: 3.93sec CBMC-WMM: 0.11sec CBMC-SC: 0.06sec CImpact: 244.00sec ESBMC: 0.08sec Threader-monolithic: ERROR/TIMEOUT[1] 0.10sec Threader-owicki-gries: ERROR/TIMEOUT[1] 0.10sec Threader-rely-guarantee: ERROR/TIMEOUT[1] 0.10sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT MMChecker (MM: csharp): ERROR/TIMEOUT[1] 0.09sec |
Cycles
SatAbs: 5.76sec (x2.45) Satabs-prefix-first: 3.34sec CBMC-WMM: 0.10sec CBMC-SC: 0.05sec CImpact: 184.79sec 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.10sec |
Cycles
SatAbs: 6.32sec (x2.68) Satabs-prefix-first: 3.50sec CBMC-WMM: 0.12sec CBMC-SC: 0.05sec CImpact: 237.16sec ESBMC: 0.08sec Threader-monolithic: ERROR/TIMEOUT[1] 0.10sec Threader-owicki-gries: ERROR/TIMEOUT[1] 0.10sec Threader-rely-guarantee: ERROR/TIMEOUT[1] 0.10sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT Blender: |
Cycles
SatAbs: 6.40sec (x2.72) Satabs-prefix-first: 3.76sec CBMC-WMM: 0.13sec CBMC-SC: 0.07sec CImpact: 236.25sec 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.11sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT Blender: |
Cycles
SatAbs: 6.40sec (x2.72) Satabs-prefix-first: 3.42sec CBMC-WMM: 0.12sec CBMC-SC: 0.06sec CImpact: 226.29sec 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.10sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT Blender: |
Cycles
SatAbs: 4.89sec (x2.08) Satabs-prefix-first: 102.96sec CBMC-WMM: 0.12sec CBMC-SC: 1.11sec CImpact: 62.99sec ESBMC: 0.08sec Threader-monolithic: ERROR/TIMEOUT[1] 373.86sec Threader-owicki-gries: ERROR/TIMEOUT[1] 381.85sec Threader-rely-guarantee: ERROR/TIMEOUT[1] 257.01sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT |
Cycles
SatAbs: 4.12sec (x1.75) Satabs-prefix-first: 102.23sec CBMC-WMM: 0.13sec CBMC-SC: 1.12sec CImpact: 61.61sec ESBMC: 0.08sec Threader-monolithic: ERROR/TIMEOUT[1] 379.29sec Threader-owicki-gries: ERROR/TIMEOUT[1] 281.96sec Threader-rely-guarantee: ERROR/TIMEOUT[1] 382.78sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT |
Cycles
SatAbs: 3.48sec (x1.48) Satabs-prefix-first: 71.24sec CBMC-WMM: 0.10sec CBMC-SC: 0.79sec CImpact: 62.54sec ESBMC: 0.08sec Threader-monolithic: ERROR/TIMEOUT[1] 381.32sec Threader-owicki-gries: ERROR/TIMEOUT[1] 381.67sec Threader-rely-guarantee: ERROR/TIMEOUT[1] 380.06sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT |
Cycles
SatAbs: 3.59sec (x1.52) Satabs-prefix-first: 41.73sec CBMC-WMM: 0.13sec CBMC-SC: 1.41sec CImpact: 62.60sec ESBMC: 0.08sec Threader-monolithic: ERROR/TIMEOUT[1] 376.30sec Threader-owicki-gries: ERROR/TIMEOUT[1] 365.57sec Threader-rely-guarantee: ERROR/TIMEOUT[1] 382.48sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT |
Cycles
SatAbs: 3.61sec (x1.53) Satabs-prefix-first: 43.86sec CBMC-WMM: 0.13sec CBMC-SC: 1.46sec CImpact: 61.74sec ESBMC: 0.11sec Threader-monolithic: ERROR/TIMEOUT[1] 375.24sec Threader-owicki-gries: ERROR/TIMEOUT[1] 343.56sec Threader-rely-guarantee: ERROR/TIMEOUT[1] 383.06sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT |
Cycles
SatAbs: 3.70sec (x1.57) Satabs-prefix-first: 42.08sec CBMC-WMM: 0.12sec CBMC-SC: 1.40sec CImpact: 63.18sec ESBMC: 0.09sec Threader-monolithic: ERROR/TIMEOUT[1] 379.58sec Threader-owicki-gries: ERROR/TIMEOUT[1] 382.05sec Threader-rely-guarantee: ERROR/TIMEOUT[1] 351.74sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT |
||||
ppc/posrr004 |
SatAbs: 0.96sec Satabs-prefix-first: 1.29sec CBMC-WMM: 0.08sec CBMC-SC: 0.08sec CImpact: ERROR/TIMEOUT[8] 298.88sec Checkfence: 0.01sec ESBMC: 0.06sec Threader-monolithic: 0.12sec Threader-owicki-gries: 0.16sec Threader-rely-guarantee: 0.16sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT MMChecker (MM: sc): 0.45sec |
Cycles
SatAbs: 3.21sec (x3.34) Satabs-prefix-first: 4.37sec CBMC-WMM: 0.16sec CBMC-SC: 171.87sec CImpact: ERROR/TIMEOUT[8] 453.06sec ESBMC: 0.12sec Threader-monolithic: ERROR/TIMEOUT[130] 897.49sec Threader-owicki-gries: ERROR/TIMEOUT[130] 897.61sec Threader-rely-guarantee: ERROR/TIMEOUT[130] 897.49sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT MMChecker (MM: csharp): 0.64sec |
Cycles
SatAbs: 2.83sec (x2.94) Satabs-prefix-first: 6.87sec CBMC-WMM: 0.15sec CBMC-SC: 0.07sec CImpact: ERROR/TIMEOUT[8] 343.41sec Checkfence: 0.01sec 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.12sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT MMChecker (MM: csharp): 0.62sec |
Cycles
SatAbs: 2.93sec (x3.05) Satabs-prefix-first: 6.88sec CBMC-WMM: 0.16sec CBMC-SC: 0.06sec CImpact: ERROR/TIMEOUT[8] 290.50sec 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 MMChecker (MM: csharp): 0.62sec |
Cycles
SatAbs: 2.91sec (x3.03) Satabs-prefix-first: 6.81sec CBMC-WMM: 0.14sec CBMC-SC: 0.07sec CImpact: ERROR/TIMEOUT[8] 295.86sec 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.09sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT MMChecker (MM: csharp): 0.68sec |
Cycles
SatAbs: 2.97sec (x3.09) Satabs-prefix-first: 6.89sec CBMC-WMM: 0.16sec CBMC-SC: 0.07sec CImpact: ERROR/TIMEOUT[8] 347.97sec 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.12sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT Blender: |
Cycles
SatAbs: 3.00sec (x3.12) Satabs-prefix-first: 8.59sec CBMC-WMM: 0.14sec CBMC-SC: 0.06sec CImpact: ERROR/TIMEOUT[8] 343.37sec ESBMC: 0.06sec Threader-monolithic: ERROR/TIMEOUT[1] 0.09sec 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: 2.71sec (x2.82) Satabs-prefix-first: 6.86sec CBMC-WMM: 0.14sec CBMC-SC: 0.08sec CImpact: ERROR/TIMEOUT[8] 353.58sec 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: 3.02sec (x3.14) Satabs-prefix-first: 7.02sec CBMC-WMM: 0.17sec CBMC-SC: 0.06sec CImpact: ERROR/TIMEOUT[8] 345.44sec ESBMC: 0.08sec Threader-monolithic: ERROR/TIMEOUT[1] 0.12sec Threader-owicki-gries: ERROR/TIMEOUT[1] 0.09sec Threader-rely-guarantee: ERROR/TIMEOUT[1] 0.10sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT |
Cycles
SatAbs: 3.03sec (x3.15) Satabs-prefix-first: 6.71sec CBMC-WMM: 0.16sec CBMC-SC: 0.06sec CImpact: ERROR/TIMEOUT[8] 349.28sec 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 |
Cycles
SatAbs: 2.95sec (x3.07) Satabs-prefix-first: 6.64sec CBMC-WMM: 0.17sec CBMC-SC: 0.07sec CImpact: ERROR/TIMEOUT[8] 349.48sec ESBMC: 0.08sec Threader-monolithic: ERROR/TIMEOUT[1] 0.09sec Threader-owicki-gries: ERROR/TIMEOUT[1] 0.17sec Threader-rely-guarantee: ERROR/TIMEOUT[1] 0.13sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT |
Cycles
SatAbs: 4.05sec (x4.21) Satabs-prefix-first: 10.53sec CBMC-WMM: 0.20sec CBMC-SC: 0.07sec CImpact: ERROR/TIMEOUT[8] 317.41sec 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.12sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT |
Cycles
SatAbs: 3.25sec (x3.38) Satabs-prefix-first: 6.57sec CBMC-WMM: 0.14sec CBMC-SC: 0.06sec CImpact: ERROR/TIMEOUT[8] 325.92sec ESBMC: 0.06sec Threader-monolithic: ERROR/TIMEOUT[1] 0.10sec Threader-owicki-gries: ERROR/TIMEOUT[1] 0.09sec Threader-rely-guarantee: ERROR/TIMEOUT[1] 0.12sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT |
Cycles
SatAbs: 2.96sec (x3.08) Satabs-prefix-first: 7.00sec CBMC-WMM: 0.17sec CBMC-SC: 0.07sec CImpact: ERROR/TIMEOUT[8] 366.95sec 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.10sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT |