How to read the tables?

Meaning of the model-checker's results
Model-checker on the instrumented programObserved state in LitmusPicture
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.
NameSCTSO (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/aclwdrr (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/aclwdrr000
SatAbs:
0.69sec

Satabs-prefix-first: 0.61sec
CBMC-WMM: 0.06sec
CBMC-SC: 0.08sec
CImpact: ERROR/TIMEOUT[8] 278.30sec
Checkfence: 0.01sec
ESBMC: 0.05sec
Threader-monolithic: 0.15sec
Threader-owicki-gries: 0.13sec
Threader-rely-guarantee: 0.14sec
Poirot-Integer: ERROR/TIMEOUT
Poirot-BitVector: ERROR/TIMEOUT
MMChecker (MM: sc): 0.27sec
Cycles
SatAbs:
2.86sec (x4.14)

Satabs-prefix-first: 3.63sec
CBMC-WMM: 0.16sec
CBMC-SC: 24.55sec
CImpact: ERROR/TIMEOUT[8] 435.81sec
ESBMC: 0.08sec
Threader-monolithic: ERROR/TIMEOUT[130] 897.17sec
Threader-owicki-gries: ERROR/TIMEOUT[130] 897.68sec
Threader-rely-guarantee: ERROR/TIMEOUT[130] 897.59sec
Poirot-Integer: ERROR/TIMEOUT
Poirot-BitVector: ERROR/TIMEOUT
MMChecker (MM: csharp): 0.27sec
Cycles
SatAbs:
7.74sec (x11.21)

Satabs-prefix-first: 4.27sec
CBMC-WMM: 0.17sec
CBMC-SC: 0.08sec
CImpact: ERROR/TIMEOUT[8] 269.05sec
Checkfence: 0.01sec
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.11sec
Poirot-Integer: ERROR/TIMEOUT
Poirot-BitVector: ERROR/TIMEOUT
MMChecker (MM: csharp): 0.27sec
Cycles
SatAbs:
6.97sec (x10.10)

Satabs-prefix-first: 4.38sec
CBMC-WMM: 0.16sec
CBMC-SC: 0.08sec
CImpact: ERROR/TIMEOUT[8] 274.38sec
ESBMC: 0.06sec
Threader-monolithic: ERROR/TIMEOUT[1] 0.12sec
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): 0.28sec
Cycles
SatAbs:
7.91sec (x11.46)

Satabs-prefix-first: 4.36sec
CBMC-WMM: 0.15sec
CBMC-SC: 0.08sec
CImpact: ERROR/TIMEOUT[8] 344.63sec
ESBMC: 0.07sec
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): 0.28sec
Cycles
SatAbs:
7.93sec (x11.49)

Satabs-prefix-first: 4.63sec
CBMC-WMM: 0.15sec
CBMC-SC: 0.08sec
CImpact: ERROR/TIMEOUT[8] 336.91sec
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.10sec
Poirot-Integer: ERROR/TIMEOUT
Poirot-BitVector: ERROR/TIMEOUT
Blender:
Cycles
SatAbs:
8.12sec (x11.76)

Satabs-prefix-first: 4.56sec
CBMC-WMM: 0.17sec
CBMC-SC: 0.08sec
CImpact: ERROR/TIMEOUT[8] 294.06sec
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:
7.98sec (x11.56)

Satabs-prefix-first: 4.46sec
CBMC-WMM: 0.17sec
CBMC-SC: 0.08sec
CImpact: ERROR/TIMEOUT[8] 331.64sec
ESBMC: 0.07sec
Threader-monolithic: ERROR/TIMEOUT[1] 0.10sec
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:
7.77sec (x11.26)

Satabs-prefix-first: 4.59sec
CBMC-WMM: 0.18sec
CBMC-SC: 0.08sec
CImpact: ERROR/TIMEOUT[8] 321.18sec
ESBMC: 0.06sec
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
Cycles
SatAbs:
7.72sec (x11.18)

Satabs-prefix-first: 4.59sec
CBMC-WMM: 0.18sec
CBMC-SC: 0.08sec
CImpact: ERROR/TIMEOUT[8] 280.18sec
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
Cycles
SatAbs:
7.76sec (x11.24)

Satabs-prefix-first: 4.22sec
CBMC-WMM: 0.17sec
CBMC-SC: 0.08sec
CImpact: ERROR/TIMEOUT[8] 260.25sec
ESBMC: 0.06sec
Threader-monolithic: ERROR/TIMEOUT[1] 0.12sec
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:
96.07sec (x139.23)

Satabs-prefix-first: 109.57sec
CBMC-WMM: 0.15sec
CBMC-SC: 3.13sec
CImpact: ERROR/TIMEOUT[8] 302.49sec
ESBMC: 0.11sec
Threader-monolithic: ERROR/TIMEOUT[130] 896.97sec
Threader-owicki-gries: ERROR/TIMEOUT[130] 897.22sec
Threader-rely-guarantee: ERROR/TIMEOUT[130] 897.55sec
Poirot-Integer: ERROR/TIMEOUT
Poirot-BitVector: ERROR/TIMEOUT
Cycles
SatAbs:
85.21sec (x123.49)

Satabs-prefix-first: 110.33sec
CBMC-WMM: 0.17sec
CBMC-SC: 3.25sec
CImpact: ERROR/TIMEOUT[8] 307.04sec
ESBMC: 0.10sec
Threader-monolithic: ERROR/TIMEOUT[130] 897.24sec
Threader-owicki-gries: ERROR/TIMEOUT[130] 896.16sec
Threader-rely-guarantee: ERROR/TIMEOUT[130] 897.44sec
Poirot-Integer: ERROR/TIMEOUT
Poirot-BitVector: ERROR/TIMEOUT
Cycles
SatAbs:
87.60sec (x126.95)

Satabs-prefix-first: 98.03sec
CBMC-WMM: 0.15sec
CBMC-SC: 3.13sec
CImpact: ERROR/TIMEOUT[8] 282.30sec
ESBMC: 0.11sec
Threader-monolithic: ERROR/TIMEOUT[130] 896.98sec
Threader-owicki-gries: ERROR/TIMEOUT[130] 897.50sec
Threader-rely-guarantee: ERROR/TIMEOUT[130] 897.19sec
Poirot-Integer: ERROR/TIMEOUT
Poirot-BitVector: ERROR/TIMEOUT
ppc/aclwdrr001
SatAbs:
0.66sec

Satabs-prefix-first: 0.67sec
CBMC-WMM: 0.09sec
CBMC-SC: 0.08sec
CImpact: ERROR/TIMEOUT[8] 277.91sec
Checkfence: 0.01sec
ESBMC: 0.07sec
Threader-monolithic: 0.11sec
Threader-owicki-gries: 0.13sec
Threader-rely-guarantee: 0.14sec
Poirot-Integer: ERROR/TIMEOUT
Poirot-BitVector: ERROR/TIMEOUT
MMChecker (MM: sc): 0.26sec
Cycles
SatAbs:
2.75sec (x4.16)

Satabs-prefix-first: 3.52sec
CBMC-WMM: 0.15sec
CBMC-SC: 8.36sec
CImpact: ERROR/TIMEOUT[8] 440.59sec
ESBMC: 0.11sec
Threader-monolithic: ERROR/TIMEOUT[130] 897.54sec
Threader-owicki-gries: ERROR/TIMEOUT[130] 897.56sec
Threader-rely-guarantee: ERROR/TIMEOUT[130] 897.27sec
Poirot-Integer: ERROR/TIMEOUT
Poirot-BitVector: ERROR/TIMEOUT
MMChecker (MM: csharp): 0.29sec
Cycles
SatAbs:
7.73sec (x11.71)

Satabs-prefix-first: 4.29sec
CBMC-WMM: 0.16sec
CBMC-SC: 0.08sec
CImpact: ERROR/TIMEOUT[8] 335.95sec
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): 0.26sec
Cycles
SatAbs:
8.84sec (x13.39)

Satabs-prefix-first: 4.26sec
CBMC-WMM: 0.15sec
CBMC-SC: 0.08sec
CImpact: ERROR/TIMEOUT[8] 325.28sec
ESBMC: 0.08sec
Threader-monolithic: ERROR/TIMEOUT[1] 0.11sec
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): 0.39sec
Cycles
SatAbs:
7.95sec (x12.04)

Satabs-prefix-first: 4.71sec
CBMC-WMM: 0.18sec
CBMC-SC: 0.07sec
CImpact: ERROR/TIMEOUT[8] 257.73sec
ESBMC: 0.07sec
Threader-monolithic: ERROR/TIMEOUT[1] 0.12sec
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): 0.27sec
Cycles
SatAbs:
8.09sec (x12.25)

Satabs-prefix-first: 4.58sec
CBMC-WMM: 0.16sec
CBMC-SC: 0.08sec
CImpact: ERROR/TIMEOUT[8] 321.27sec
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.10sec
Poirot-Integer: ERROR/TIMEOUT
Poirot-BitVector: ERROR/TIMEOUT
Blender:
Cycles
SatAbs:
7.60sec (x11.51)

Satabs-prefix-first: 4.53sec
CBMC-WMM: 0.14sec
CBMC-SC: 0.08sec
CImpact: ERROR/TIMEOUT[8] 322.87sec
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.09sec
Poirot-Integer: ERROR/TIMEOUT
Poirot-BitVector: ERROR/TIMEOUT
Blender:
Cycles
SatAbs:
7.81sec (x11.83)

Satabs-prefix-first: 4.56sec
CBMC-WMM: 0.14sec
CBMC-SC: 0.08sec
CImpact: ERROR/TIMEOUT[8] 319.33sec
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.09sec
Poirot-Integer: ERROR/TIMEOUT
Poirot-BitVector: ERROR/TIMEOUT
Blender:
Cycles
SatAbs:
7.72sec (x11.69)

Satabs-prefix-first: 4.66sec
CBMC-WMM: 0.15sec
CBMC-SC: 0.08sec
CImpact: ERROR/TIMEOUT[8] 278.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.12sec
Poirot-Integer: ERROR/TIMEOUT
Poirot-BitVector: ERROR/TIMEOUT
Cycles
SatAbs:
7.42sec (x11.24)

Satabs-prefix-first: 4.37sec
CBMC-WMM: 0.17sec
CBMC-SC: 0.08sec
CImpact: ERROR/TIMEOUT[8] 324.42sec
ESBMC: 0.13sec
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:
9.52sec (x14.42)

Satabs-prefix-first: 5.49sec
CBMC-WMM: 0.18sec
CBMC-SC: 0.10sec
CImpact: ERROR/TIMEOUT[8] 330.10sec
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.11sec
Poirot-Integer: ERROR/TIMEOUT
Poirot-BitVector: ERROR/TIMEOUT
Cycles
SatAbs:
3.89sec (x5.89)

Satabs-prefix-first: 4.60sec
CBMC-WMM: 0.15sec
CBMC-SC: 33.00sec
CImpact: ERROR/TIMEOUT[8] 340.17sec
ESBMC: 0.11sec
Threader-monolithic: ERROR/TIMEOUT[130] 897.58sec
Threader-owicki-gries: ERROR/TIMEOUT[130] 897.37sec
Threader-rely-guarantee: ERROR/TIMEOUT[130] 897.45sec
Poirot-Integer: ERROR/TIMEOUT
Poirot-BitVector: ERROR/TIMEOUT
Cycles
SatAbs:
3.34sec (x5.06)

Satabs-prefix-first: 3.87sec
CBMC-WMM: 0.17sec
CBMC-SC: 22.09sec
CImpact: ERROR/TIMEOUT[8] 335.71sec
ESBMC: 0.11sec
Threader-monolithic: ERROR/TIMEOUT[130] 897.35sec
Threader-owicki-gries: ERROR/TIMEOUT[130] 897.55sec
Threader-rely-guarantee: ERROR/TIMEOUT[130] 897.34sec
Poirot-Integer: ERROR/TIMEOUT
Poirot-BitVector: ERROR/TIMEOUT
Cycles
SatAbs:
3.29sec (x4.98)

Satabs-prefix-first: 3.72sec
CBMC-WMM: 0.15sec
CBMC-SC: 28.12sec
CImpact: ERROR/TIMEOUT[8] 289.37sec
ESBMC: 0.07sec
Threader-monolithic: ERROR/TIMEOUT[130] 896.96sec
Threader-owicki-gries: ERROR/TIMEOUT[130] 897.28sec
Threader-rely-guarantee: ERROR/TIMEOUT[130] 896.80sec
Poirot-Integer: ERROR/TIMEOUT
Poirot-BitVector: ERROR/TIMEOUT
ppc/aclwdrr002
SatAbs:
4.46sec

Satabs-prefix-first: 5.59sec
CBMC-WMM: 0.12sec
CBMC-SC: 0.12sec
CImpact: ERROR/TIMEOUT[8] 301.39sec
Checkfence: 0.01sec
ESBMC: 0.07sec
Threader-monolithic: 0.14sec
Threader-owicki-gries: 0.14sec
Threader-rely-guarantee: 0.17sec
Poirot-Integer: ERROR/TIMEOUT
Poirot-BitVector: ERROR/TIMEOUT
MMChecker (MM: sc): 0.81sec
Cycles
SatAbs:
221.43sec (x49.64)

Satabs-prefix-first: 181.88sec
CBMC-WMM: 0.25sec
CBMC-SC: 20.89sec
CImpact: ERROR/TIMEOUT[8] 284.27sec
ESBMC: 0.05sec
Threader-monolithic: ERROR/TIMEOUT[130] 896.80sec
Threader-owicki-gries: ERROR/TIMEOUT[130] 896.41sec
Threader-rely-guarantee: ERROR/TIMEOUT[130] 896.47sec
Poirot-Integer: ERROR/TIMEOUT
Poirot-BitVector: ERROR/TIMEOUT
MMChecker (MM: csharp): 0.55sec
Cycles
SatAbs:
17.23sec (x3.86)

Satabs-prefix-first: 18.88sec
CBMC-WMM: 0.29sec
CBMC-SC: 0.10sec
CImpact: ERROR/TIMEOUT[8] 269.37sec
Checkfence: 0.01sec
ESBMC: 0.04sec
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): 0.57sec
Cycles
SatAbs:
14.80sec (x3.31)

Satabs-prefix-first: 16.60sec
CBMC-WMM: 0.17sec
CBMC-SC: 0.07sec
CImpact: ERROR/TIMEOUT[8] 267.83sec
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.08sec
Poirot-Integer: ERROR/TIMEOUT
Poirot-BitVector: ERROR/TIMEOUT
MMChecker (MM: csharp): 0.58sec
Cycles
SatAbs:
15.36sec (x3.44)

Satabs-prefix-first: 16.53sec
CBMC-WMM: 0.17sec
CBMC-SC: 0.07sec
CImpact: ERROR/TIMEOUT[8] 254.10sec
ESBMC: 0.06sec
Threader-monolithic: ERROR/TIMEOUT[1] 0.09sec
Threader-owicki-gries: ERROR/TIMEOUT[1] 0.10sec
Threader-rely-guarantee: ERROR/TIMEOUT[1] 0.09sec
Poirot-Integer: ERROR/TIMEOUT
Poirot-BitVector: ERROR/TIMEOUT
MMChecker (MM: csharp): 0.55sec
Cycles
SatAbs:
15.33sec (x3.43)

Satabs-prefix-first: 16.54sec
CBMC-WMM: 0.13sec
CBMC-SC: 0.09sec
CImpact: ERROR/TIMEOUT[8] 258.42sec
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.08sec
Poirot-Integer: ERROR/TIMEOUT
Poirot-BitVector: ERROR/TIMEOUT
Blender:
Cycles
SatAbs:
16.15sec (x3.62)

Satabs-prefix-first: 17.33sec
CBMC-WMM: 0.16sec
CBMC-SC: 0.09sec
CImpact: ERROR/TIMEOUT[8] 262.66sec
ESBMC: 0.06sec
Threader-monolithic: ERROR/TIMEOUT[1] 0.09sec
Threader-owicki-gries: ERROR/TIMEOUT[1] 0.07sec
Threader-rely-guarantee: ERROR/TIMEOUT[1] 0.11sec
Poirot-Integer: ERROR/TIMEOUT
Poirot-BitVector: ERROR/TIMEOUT
Blender:
Cycles
SatAbs:
15.66sec (x3.51)

Satabs-prefix-first: 16.90sec
CBMC-WMM: 0.15sec
CBMC-SC: 0.07sec
CImpact: ERROR/TIMEOUT[8] 273.03sec
ESBMC: 0.06sec
Threader-monolithic: ERROR/TIMEOUT[1] 0.09sec
Threader-owicki-gries: ERROR/TIMEOUT[1] 0.06sec
Threader-rely-guarantee: ERROR/TIMEOUT[1] 0.10sec
Poirot-Integer: ERROR/TIMEOUT
Poirot-BitVector: ERROR/TIMEOUT
Blender:
Cycles
SatAbs:
16.34sec (x3.66)

Satabs-prefix-first: 18.30sec
CBMC-WMM: 0.18sec
CBMC-SC: 0.06sec
CImpact: ERROR/TIMEOUT[8] 256.32sec
ESBMC: 0.06sec
Threader-monolithic: ERROR/TIMEOUT[1] 0.08sec
Threader-owicki-gries: ERROR/TIMEOUT[1] 0.08sec
Threader-rely-guarantee: ERROR/TIMEOUT[1] 0.09sec
Poirot-Integer: ERROR/TIMEOUT
Poirot-BitVector: ERROR/TIMEOUT
Cycles
SatAbs:
16.84sec (x3.77)

Satabs-prefix-first: 18.37sec
CBMC-WMM: 0.19sec
CBMC-SC: 0.07sec
CImpact: ERROR/TIMEOUT[8] 254.28sec
ESBMC: 0.06sec
Threader-monolithic: ERROR/TIMEOUT[1] 0.10sec
Threader-owicki-gries: ERROR/TIMEOUT[1] 0.08sec
Threader-rely-guarantee: ERROR/TIMEOUT[1] 0.09sec
Poirot-Integer: ERROR/TIMEOUT
Poirot-BitVector: ERROR/TIMEOUT
Cycles
SatAbs:
16.68sec (x3.73)

Satabs-prefix-first: 18.24sec
CBMC-WMM: 0.19sec
CBMC-SC: 0.09sec
CImpact: ERROR/TIMEOUT[8] 255.45sec
ESBMC: 0.06sec
Threader-monolithic: ERROR/TIMEOUT[1] 0.07sec
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: ERROR/TIMEOUT[130]
1072.29sec (x240.42)

Satabs-prefix-first: 116.85sec
CBMC-WMM: 0.14sec
CBMC-SC: 15.82sec
CImpact: 0.02sec
ESBMC: 0.07sec
Threader-monolithic: ERROR/TIMEOUT[130] 897.63sec
Threader-owicki-gries: ERROR/TIMEOUT[130] 897.56sec
Threader-rely-guarantee: ERROR/TIMEOUT[130] 897.62sec
Poirot-Integer: ERROR/TIMEOUT
Poirot-BitVector: ERROR/TIMEOUT
Cycles
SatAbs:
235.85sec (x52.88)

Satabs-prefix-first: 208.01sec
CBMC-WMM: 0.14sec
CBMC-SC: 4.64sec
CImpact: ERROR/TIMEOUT[8] 256.68sec
ESBMC: 0.07sec
Threader-monolithic: ERROR/TIMEOUT[1] 374.49sec
Threader-owicki-gries: ERROR/TIMEOUT[1] 376.38sec
Threader-rely-guarantee: ERROR/TIMEOUT[1] 374.10sec
Poirot-Integer: ERROR/TIMEOUT
Poirot-BitVector: ERROR/TIMEOUT
Cycles
SatAbs:
202.11sec (x45.31)

Satabs-prefix-first: 198.45sec
CBMC-WMM: 0.14sec
CBMC-SC: 4.26sec
CImpact: ERROR/TIMEOUT[8] 246.54sec
ESBMC: 0.06sec
Threader-monolithic: ERROR/TIMEOUT[1] 379.66sec
Threader-owicki-gries: ERROR/TIMEOUT[1] 372.39sec
Threader-rely-guarantee: ERROR/TIMEOUT[1] 371.42sec
Poirot-Integer: ERROR/TIMEOUT
Poirot-BitVector: ERROR/TIMEOUT
ppc/aclwdrr003
SatAbs:
1.41sec

Satabs-prefix-first: 1.48sec
CBMC-WMM: 0.06sec
CBMC-SC: 0.06sec
CImpact: ERROR/TIMEOUT[8] 183.28sec
Checkfence: 0.01sec
ESBMC: 0.05sec
Threader-monolithic: 0.09sec
Threader-owicki-gries: 0.09sec
Threader-rely-guarantee: 0.09sec
Poirot-Integer: ERROR/TIMEOUT
Poirot-BitVector: ERROR/TIMEOUT
MMChecker (MM: sc): 0.17sec
Cycles
SatAbs:
51.74sec (x36.69)

Satabs-prefix-first: 57.00sec
CBMC-WMM: 0.09sec
CBMC-SC: 20.73sec
CImpact: ERROR/TIMEOUT[8] 266.26sec
ESBMC: 0.06sec
Threader-monolithic: ERROR/TIMEOUT[130] 896.72sec
Threader-owicki-gries: ERROR/TIMEOUT[130] 896.81sec
Threader-rely-guarantee: ERROR/TIMEOUT[130] 896.87sec
Poirot-Integer: ERROR/TIMEOUT
Poirot-BitVector: ERROR/TIMEOUT
MMChecker (MM: csharp): 0.18sec
Cycles
SatAbs:
6.30sec (x4.46)

Satabs-prefix-first: 4.26sec
CBMC-WMM: 0.11sec
CBMC-SC: 0.06sec
CImpact: ERROR/TIMEOUT[8] 218.57sec
Checkfence: 0.01sec
ESBMC: 0.05sec
Threader-monolithic: ERROR/TIMEOUT[1] 0.06sec
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): 0.17sec
Cycles
SatAbs:
6.04sec (x4.28)

Satabs-prefix-first: 4.38sec
CBMC-WMM: 0.10sec
CBMC-SC: 0.06sec
CImpact: ERROR/TIMEOUT[8] 223.21sec
ESBMC: 0.06sec
Threader-monolithic: ERROR/TIMEOUT[1] 0.07sec
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): 0.17sec
Cycles
SatAbs:
6.44sec (x4.56)

Satabs-prefix-first: 4.57sec
CBMC-WMM: 0.11sec
CBMC-SC: 0.06sec
CImpact: ERROR/TIMEOUT[8] 238.56sec
ESBMC: 0.06sec
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): 0.17sec
Cycles
SatAbs:
6.50sec (x4.60)

Satabs-prefix-first: 4.40sec
CBMC-WMM: 0.11sec
CBMC-SC: 0.06sec
CImpact: ERROR/TIMEOUT[8] 231.42sec
ESBMC: 0.04sec
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:
6.04sec (x4.28)

Satabs-prefix-first: 4.20sec
CBMC-WMM: 0.10sec
CBMC-SC: 0.06sec
CImpact: ERROR/TIMEOUT[8] 216.82sec
ESBMC: 0.05sec
Threader-monolithic: ERROR/TIMEOUT[1] 0.08sec
Threader-owicki-gries: ERROR/TIMEOUT[1] 0.07sec
Threader-rely-guarantee: ERROR/TIMEOUT[1] 0.08sec
Poirot-Integer: ERROR/TIMEOUT
Poirot-BitVector: ERROR/TIMEOUT
Blender:
Cycles
SatAbs:
6.14sec (x4.35)

Satabs-prefix-first: 4.25sec
CBMC-WMM: 0.09sec
CBMC-SC: 0.06sec
CImpact: ERROR/TIMEOUT[8] 216.51sec
ESBMC: 0.05sec
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
Blender:
Cycles
SatAbs:
6.16sec (x4.36)

Satabs-prefix-first: 4.31sec
CBMC-WMM: 0.11sec
CBMC-SC: 0.04sec
CImpact: ERROR/TIMEOUT[8] 215.93sec
ESBMC: 0.05sec
Threader-monolithic: ERROR/TIMEOUT[1] 0.08sec
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:
6.41sec (x4.54)

Satabs-prefix-first: 4.14sec
CBMC-WMM: 0.10sec
CBMC-SC: 0.06sec
CImpact: ERROR/TIMEOUT[8] 215.84sec
ESBMC: 0.06sec
Threader-monolithic: ERROR/TIMEOUT[1] 0.07sec
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:
6.10sec (x4.32)

Satabs-prefix-first: 3.91sec
CBMC-WMM: 0.12sec
CBMC-SC: 0.06sec
CImpact: ERROR/TIMEOUT[8] 215.49sec
ESBMC: 0.04sec
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
Cycles
SatAbs:
46.46sec (x32.95)

Satabs-prefix-first: 33.57sec
CBMC-WMM: 0.11sec
CBMC-SC: 1.96sec
CImpact: ERROR/TIMEOUT[8] 222.42sec
ESBMC: 0.07sec
Threader-monolithic: ERROR/TIMEOUT[1] 319.20sec
Threader-owicki-gries: ERROR/TIMEOUT[1] 304.66sec
Threader-rely-guarantee: ERROR/TIMEOUT[1] 309.29sec
Poirot-Integer: ERROR/TIMEOUT
Poirot-BitVector: ERROR/TIMEOUT
Cycles
SatAbs:
42.40sec (x30.07)

Satabs-prefix-first: 28.22sec
CBMC-WMM: 0.11sec
CBMC-SC: 1.98sec
CImpact: ERROR/TIMEOUT[8] 226.21sec
ESBMC: 0.06sec
Threader-monolithic: ERROR/TIMEOUT[1] 305.01sec
Threader-owicki-gries: ERROR/TIMEOUT[1] 301.36sec
Threader-rely-guarantee: ERROR/TIMEOUT[1] 303.80sec
Poirot-Integer: ERROR/TIMEOUT
Poirot-BitVector: ERROR/TIMEOUT
Cycles
SatAbs:
47.10sec (x33.40)

Satabs-prefix-first: 33.74sec
CBMC-WMM: 0.11sec
CBMC-SC: 2.07sec
CImpact: ERROR/TIMEOUT[8] 241.72sec
ESBMC: 0.07sec
Threader-monolithic: ERROR/TIMEOUT[1] 301.64sec
Threader-owicki-gries: ERROR/TIMEOUT[1] 299.80sec
Threader-rely-guarantee: ERROR/TIMEOUT[1] 301.04sec
Poirot-Integer: ERROR/TIMEOUT
Poirot-BitVector: ERROR/TIMEOUT
ppc/aclwdrr004
SatAbs:
0.51sec

Satabs-prefix-first: 0.63sec
CBMC-WMM: 0.06sec
CBMC-SC: 0.06sec
CImpact: ERROR/TIMEOUT[8] 196.38sec
Checkfence: 0.01sec
ESBMC: 0.05sec
Threader-monolithic: 0.11sec
Threader-owicki-gries: 0.10sec
Threader-rely-guarantee: 0.09sec
Poirot-Integer: ERROR/TIMEOUT
Poirot-BitVector: ERROR/TIMEOUT
MMChecker (MM: sc): 0.26sec
Cycles
SatAbs:
3.17sec (x6.21)

Satabs-prefix-first: 3.50sec
CBMC-WMM: 0.12sec
CBMC-SC: 22.83sec
CImpact: ERROR/TIMEOUT[8] 299.70sec
ESBMC: 0.07sec
Threader-monolithic: ERROR/TIMEOUT[130] 897.58sec
Threader-owicki-gries: ERROR/TIMEOUT[130] 897.48sec
Threader-rely-guarantee: ERROR/TIMEOUT[130] 897.52sec
Poirot-Integer: ERROR/TIMEOUT
Poirot-BitVector: ERROR/TIMEOUT
MMChecker (MM: csharp): 0.28sec
Cycles
SatAbs:
5.47sec (x10.72)

Satabs-prefix-first: 5.10sec
CBMC-WMM: 0.12sec
CBMC-SC: 0.06sec
CImpact: ERROR/TIMEOUT[8] 233.32sec
Checkfence: 0.01sec
ESBMC: 0.05sec
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): 0.29sec
Cycles
SatAbs:
5.15sec (x10.09)

Satabs-prefix-first: 4.34sec
CBMC-WMM: 0.11sec
CBMC-SC: 0.05sec
CImpact: ERROR/TIMEOUT[8] 228.14sec
ESBMC: 0.07sec
Threader-monolithic: ERROR/TIMEOUT[1] 0.10sec
Threader-owicki-gries: ERROR/TIMEOUT[1] 0.08sec
Threader-rely-guarantee: ERROR/TIMEOUT[1] 0.11sec
Poirot-Integer: ERROR/TIMEOUT
Poirot-BitVector: ERROR/TIMEOUT
MMChecker (MM: csharp): 0.30sec
Cycles
SatAbs:
8.24sec (x16.15)

Satabs-prefix-first: 5.80sec
CBMC-WMM: 0.12sec
CBMC-SC: 0.05sec
CImpact: ERROR/TIMEOUT[8] 246.62sec
ESBMC: 0.03sec
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): 0.28sec
Cycles
SatAbs:
5.14sec (x10.07)

Satabs-prefix-first: 4.44sec
CBMC-WMM: 0.11sec
CBMC-SC: 0.04sec
CImpact: ERROR/TIMEOUT[8] 232.54sec
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.09sec
Poirot-Integer: ERROR/TIMEOUT
Poirot-BitVector: ERROR/TIMEOUT
Blender:
Cycles
SatAbs:
5.41sec (x10.60)

Satabs-prefix-first: 4.69sec
CBMC-WMM: 0.12sec
CBMC-SC: 0.05sec
CImpact: ERROR/TIMEOUT[8] 228.28sec
ESBMC: 0.06sec
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
Blender:
Cycles
SatAbs:
5.73sec (x11.23)

Satabs-prefix-first: 4.87sec
CBMC-WMM: 0.11sec
CBMC-SC: 0.06sec
CImpact: ERROR/TIMEOUT[8] 234.95sec
ESBMC: 0.06sec
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
Blender:
Cycles
SatAbs:
5.41sec (x10.60)

Satabs-prefix-first: 4.59sec
CBMC-WMM: 0.13sec
CBMC-SC: 0.06sec
CImpact: ERROR/TIMEOUT[8] 235.13sec
ESBMC: 0.05sec
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:
5.54sec (x10.86)

Satabs-prefix-first: 4.38sec
CBMC-WMM: 0.12sec
CBMC-SC: 0.04sec
CImpact: ERROR/TIMEOUT[8] 233.58sec
ESBMC: 0.06sec
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
Cycles
SatAbs:
5.45sec (x10.68)

Satabs-prefix-first: 4.49sec
CBMC-WMM: 0.11sec
CBMC-SC: 0.06sec
CImpact: ERROR/TIMEOUT[8] 234.19sec
ESBMC: 0.06sec
Threader-monolithic: ERROR/TIMEOUT[1] 0.09sec
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:
5.28sec (x10.35)

Satabs-prefix-first: 4.44sec
CBMC-WMM: 0.14sec
CBMC-SC: 0.04sec
CImpact: ERROR/TIMEOUT[8] 233.97sec
ESBMC: 0.04sec
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
Cycles
SatAbs:
6.02sec (x11.80)

Satabs-prefix-first: 5.14sec
CBMC-WMM: 0.14sec
CBMC-SC: 0.05sec
CImpact: ERROR/TIMEOUT[8] 234.46sec
ESBMC: 0.06sec
Threader-monolithic: ERROR/TIMEOUT[1] 0.06sec
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:
5.60sec (x10.98)

Satabs-prefix-first: 4.45sec
CBMC-WMM: 0.11sec
CBMC-SC: 0.06sec
CImpact: ERROR/TIMEOUT[8] 234.19sec
ESBMC: 0.05sec
Threader-monolithic: ERROR/TIMEOUT[1] 0.08sec
Threader-owicki-gries: ERROR/TIMEOUT[1] 0.08sec
Threader-rely-guarantee: ERROR/TIMEOUT[1] 0.09sec
Poirot-Integer: ERROR/TIMEOUT
Poirot-BitVector: ERROR/TIMEOUT
ppc/aclwdrr005
SatAbs:
0.60sec

Satabs-prefix-first: 0.60sec
CBMC-WMM: 0.06sec
CBMC-SC: 0.04sec
CImpact: ERROR/TIMEOUT[8] 205.16sec
Checkfence: 0.01sec
ESBMC: 0.05sec
Threader-monolithic: 0.13sec
Threader-owicki-gries: 0.13sec
Threader-rely-guarantee: 0.12sec
Poirot-Integer: ERROR/TIMEOUT
Poirot-BitVector: ERROR/TIMEOUT
MMChecker (MM: sc): 0.48sec
Cycles
SatAbs:
5.24sec (x8.73)

Satabs-prefix-first: 5.80sec
CBMC-WMM: 0.22sec
CBMC-SC: 17.41sec
CImpact: ERROR/TIMEOUT[8] 306.53sec
ESBMC: 0.09sec
Threader-monolithic: ERROR/TIMEOUT[130] 897.56sec
Threader-owicki-gries: ERROR/TIMEOUT[130] 897.48sec
Threader-rely-guarantee: ERROR/TIMEOUT[130] 897.59sec
Poirot-Integer: ERROR/TIMEOUT
Poirot-BitVector: ERROR/TIMEOUT
MMChecker (MM: csharp): 0.26sec
Cycles
SatAbs:
4.83sec (x8.05)

Satabs-prefix-first: 3.77sec
CBMC-WMM: 0.11sec
CBMC-SC: 0.05sec
CImpact: ERROR/TIMEOUT[8] 218.31sec
Checkfence: 0.01sec
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
MMChecker (MM: csharp): 0.30sec
Cycles
SatAbs:
5.06sec (x8.43)

Satabs-prefix-first: 3.90sec
CBMC-WMM: 0.12sec
CBMC-SC: 0.07sec
CImpact: ERROR/TIMEOUT[8] 214.54sec
ESBMC: 0.04sec
Threader-monolithic: ERROR/TIMEOUT[1] 0.08sec
Threader-owicki-gries: ERROR/TIMEOUT[1] 0.09sec
Threader-rely-guarantee: ERROR/TIMEOUT[1] 0.07sec
Poirot-Integer: ERROR/TIMEOUT
Poirot-BitVector: ERROR/TIMEOUT
MMChecker (MM: csharp): 0.26sec
Cycles
SatAbs:
4.93sec (x8.21)

Satabs-prefix-first: 3.83sec
CBMC-WMM: 0.12sec
CBMC-SC: 0.05sec
CImpact: ERROR/TIMEOUT[8] 209.72sec
ESBMC: 0.05sec
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): 0.26sec
Cycles
SatAbs:
4.97sec (x8.28)

Satabs-prefix-first: 3.96sec
CBMC-WMM: 0.11sec
CBMC-SC: 0.05sec
CImpact: ERROR/TIMEOUT[8] 215.23sec
ESBMC: 0.05sec
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:
4.86sec (x8.10)

Satabs-prefix-first: 3.68sec
CBMC-WMM: 0.12sec
CBMC-SC: 0.05sec
CImpact: ERROR/TIMEOUT[8] 209.17sec
ESBMC: 0.05sec
Threader-monolithic: ERROR/TIMEOUT[1] 0.07sec
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:
4.83sec (x8.05)

Satabs-prefix-first: 4.10sec
CBMC-WMM: 0.11sec
CBMC-SC: 0.05sec
CImpact: ERROR/TIMEOUT[8] 209.83sec
ESBMC: 0.05sec
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:
4.49sec (x7.48)

Satabs-prefix-first: 3.75sec
CBMC-WMM: 0.13sec
CBMC-SC: 0.05sec
CImpact: ERROR/TIMEOUT[8] 210.20sec
ESBMC: 0.03sec
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:
4.80sec (x8.00)

Satabs-prefix-first: 3.84sec
CBMC-WMM: 0.13sec
CBMC-SC: 0.05sec
CImpact: ERROR/TIMEOUT[8] 214.99sec
ESBMC: 0.04sec
Threader-monolithic: ERROR/TIMEOUT[1] 0.08sec
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:
4.84sec (x8.06)

Satabs-prefix-first: 3.77sec
CBMC-WMM: 0.12sec
CBMC-SC: 0.06sec
CImpact: ERROR/TIMEOUT[8] 216.72sec
ESBMC: 0.06sec
Threader-monolithic: ERROR/TIMEOUT[1] 0.07sec
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:
36.24sec (x60.40)

Satabs-prefix-first: 52.80sec
CBMC-WMM: 0.12sec
CBMC-SC: 2.71sec
CImpact: ERROR/TIMEOUT[8] 243.30sec
ESBMC: 0.05sec
Threader-monolithic: ERROR/TIMEOUT[130] 897.54sec
Threader-owicki-gries: ERROR/TIMEOUT[130] 897.67sec
Threader-rely-guarantee: ERROR/TIMEOUT[130] 897.54sec
Poirot-Integer: ERROR/TIMEOUT
Poirot-BitVector: ERROR/TIMEOUT
Cycles
SatAbs:
37.98sec (x63.30)

Satabs-prefix-first: 59.01sec
CBMC-WMM: 0.12sec
CBMC-SC: 2.73sec
CImpact: ERROR/TIMEOUT[8] 245.98sec
ESBMC: 0.05sec
Threader-monolithic: ERROR/TIMEOUT[130] 897.50sec
Threader-owicki-gries: ERROR/TIMEOUT[130] 897.58sec
Threader-rely-guarantee: ERROR/TIMEOUT[130] 897.37sec
Poirot-Integer: ERROR/TIMEOUT
Poirot-BitVector: ERROR/TIMEOUT
Cycles
SatAbs:
36.34sec (x60.56)

Satabs-prefix-first: 55.40sec
CBMC-WMM: 0.12sec
CBMC-SC: 2.71sec
CImpact: ERROR/TIMEOUT[8] 241.69sec
ESBMC: 0.07sec
Threader-monolithic: ERROR/TIMEOUT[130] 897.51sec
Threader-owicki-gries: ERROR/TIMEOUT[130] 897.52sec
Threader-rely-guarantee: ERROR/TIMEOUT[130] 897.45sec
Poirot-Integer: ERROR/TIMEOUT
Poirot-BitVector: ERROR/TIMEOUT
ppc/aclwdrr006
SatAbs:
0.48sec

Satabs-prefix-first: 0.25sec
CBMC-WMM: 0.04sec
CBMC-SC: 0.04sec
CImpact: 0.33sec
Checkfence: 0.01sec
ESBMC: 0.05sec
Threader-monolithic: 0.10sec
Threader-owicki-gries: 0.10sec
Threader-rely-guarantee: 0.10sec
Poirot-Integer: ERROR/TIMEOUT
Poirot-BitVector: ERROR/TIMEOUT
MMChecker (MM: sc): 0.12sec
Cycles
SatAbs:
10.19sec (x21.22)

Satabs-prefix-first: 13.44sec
CBMC-WMM: 0.07sec
CBMC-SC: 4.68sec
CImpact: 51.43sec
ESBMC: 0.07sec
Threader-monolithic: ERROR/TIMEOUT[130] 897.04sec
Threader-owicki-gries: ERROR/TIMEOUT[130] 896.92sec
Threader-rely-guarantee: ERROR/TIMEOUT[130] 896.68sec
Poirot-Integer: ERROR/TIMEOUT
Poirot-BitVector: ERROR/TIMEOUT
MMChecker (MM: csharp): 0.34sec
Cycles
SatAbs:
1.42sec (x2.95)

Satabs-prefix-first: 2.08sec
CBMC-WMM: 0.07sec
CBMC-SC: 0.07sec
CImpact: 21.05sec
Checkfence: 0.01sec
ESBMC: 0.11sec
Threader-monolithic: ERROR/TIMEOUT[1] 0.06sec
Threader-owicki-gries: ERROR/TIMEOUT[1] 0.11sec
Threader-rely-guarantee: ERROR/TIMEOUT[1] 0.07sec
Poirot-Integer: ERROR/TIMEOUT
Poirot-BitVector: ERROR/TIMEOUT
MMChecker (MM: csharp): 0.20sec
Cycles
SatAbs:
1.41sec (x2.93)

Satabs-prefix-first: 2.10sec
CBMC-WMM: 0.07sec
CBMC-SC: 0.08sec
CImpact: 21.21sec
ESBMC: 0.05sec
Threader-monolithic: ERROR/TIMEOUT[1] 0.11sec
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): 0.11sec
Cycles
SatAbs:
0.76sec (x1.58)

Satabs-prefix-first: 1.14sec
CBMC-WMM: 0.06sec
CBMC-SC: 0.04sec
CImpact: 18.44sec
ESBMC: 0.06sec
Threader-monolithic: ERROR/TIMEOUT[1] 0.08sec
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): 0.12sec
Cycles
SatAbs:
0.77sec (x1.60)

Satabs-prefix-first: 1.09sec
CBMC-WMM: 0.05sec
CBMC-SC: 0.04sec
CImpact: 19.24sec
ESBMC: 0.05sec
Threader-monolithic: ERROR/TIMEOUT[1] 0.05sec
Threader-owicki-gries: ERROR/TIMEOUT[1] 0.06sec
Threader-rely-guarantee: ERROR/TIMEOUT[1] 0.08sec
Poirot-Integer: ERROR/TIMEOUT
Poirot-BitVector: ERROR/TIMEOUT
Blender:
Cycles
SatAbs:
0.86sec (x1.79)

Satabs-prefix-first: 1.29sec
CBMC-WMM: 0.07sec
CBMC-SC: 0.04sec
CImpact: 19.30sec
ESBMC: 0.05sec
Threader-monolithic: ERROR/TIMEOUT[1] 0.08sec
Threader-owicki-gries: ERROR/TIMEOUT[1] 0.05sec
Threader-rely-guarantee: ERROR/TIMEOUT[1] 0.06sec
Poirot-Integer: ERROR/TIMEOUT
Poirot-BitVector: ERROR/TIMEOUT
Blender:
Cycles
SatAbs:
1.01sec (x2.10)

Satabs-prefix-first: 1.41sec
CBMC-WMM: 0.06sec
CBMC-SC: 0.04sec
CImpact: 18.72sec
ESBMC: 0.04sec
Threader-monolithic: ERROR/TIMEOUT[1] 0.07sec
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.68sec (x1.41)

Satabs-prefix-first: 1.13sec
CBMC-WMM: 0.07sec
CBMC-SC: 0.04sec
CImpact: 18.94sec
ESBMC: 0.06sec
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
Cycles
SatAbs:
0.77sec (x1.60)

Satabs-prefix-first: 1.11sec
CBMC-WMM: 0.08sec
CBMC-SC: 0.04sec
CImpact: 22.08sec
ESBMC: 0.05sec
Threader-monolithic: ERROR/TIMEOUT[1] 0.11sec
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:
0.74sec (x1.54)

Satabs-prefix-first: 1.04sec
CBMC-WMM: 0.11sec
CBMC-SC: 0.06sec
CImpact: 19.44sec
ESBMC: 0.06sec
Threader-monolithic: ERROR/TIMEOUT[1] 0.09sec
Threader-owicki-gries: ERROR/TIMEOUT[1] 0.09sec
Threader-rely-guarantee: ERROR/TIMEOUT[1] 0.11sec
Poirot-Integer: ERROR/TIMEOUT
Poirot-BitVector: ERROR/TIMEOUT
Cycles
SatAbs:
1.12sec (x2.33)

Satabs-prefix-first: 1.53sec
CBMC-WMM: 0.08sec
CBMC-SC: 0.04sec
CImpact: 19.56sec
ESBMC: 0.15sec
Threader-monolithic: ERROR/TIMEOUT[1] 0.10sec
Threader-owicki-gries: ERROR/TIMEOUT[1] 0.07sec
Threader-rely-guarantee: ERROR/TIMEOUT[1] 0.11sec
Poirot-Integer: ERROR/TIMEOUT
Poirot-BitVector: ERROR/TIMEOUT
Cycles
SatAbs:
1.76sec (x3.66)

Satabs-prefix-first: 2.21sec
CBMC-WMM: 0.24sec
CBMC-SC: 0.03sec
CImpact: 25.35sec
ESBMC: 0.09sec
Threader-monolithic: ERROR/TIMEOUT[1] 0.13sec
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:
1.62sec (x3.37)

Satabs-prefix-first: 2.03sec
CBMC-WMM: 0.07sec
CBMC-SC: 0.04sec
CImpact: 20.61sec
ESBMC: 0.06sec
Threader-monolithic: ERROR/TIMEOUT[1] 0.12sec
Threader-owicki-gries: ERROR/TIMEOUT[1] 0.08sec
Threader-rely-guarantee: ERROR/TIMEOUT[1] 0.12sec
Poirot-Integer: ERROR/TIMEOUT
Poirot-BitVector: ERROR/TIMEOUT
ppc/aclwdrr007
SatAbs:
1.99sec

Satabs-prefix-first: 1.20sec
CBMC-WMM: 0.07sec
CBMC-SC: 0.05sec
CImpact: ERROR/TIMEOUT[8] 205.63sec
Checkfence: 0.01sec
ESBMC: 0.05sec
Threader-monolithic: 0.10sec
Threader-owicki-gries: 0.10sec
Threader-rely-guarantee: 0.08sec
Poirot-Integer: ERROR/TIMEOUT
Poirot-BitVector: ERROR/TIMEOUT
MMChecker (MM: sc): 0.25sec
Cycles
SatAbs:
62.10sec (x31.20)

Satabs-prefix-first: 60.10sec
CBMC-WMM: 0.11sec
CBMC-SC: 26.53sec
CImpact: ERROR/TIMEOUT[8] 288.00sec
ESBMC: 0.07sec
Threader-monolithic: ERROR/TIMEOUT[130] 897.16sec
Threader-owicki-gries: ERROR/TIMEOUT[130] 897.09sec
Threader-rely-guarantee: ERROR/TIMEOUT[130] 896.88sec
Poirot-Integer: ERROR/TIMEOUT
Poirot-BitVector: ERROR/TIMEOUT
MMChecker (MM: csharp): 0.26sec
Cycles
SatAbs:
8.48sec (x4.26)

Satabs-prefix-first: 5.18sec
CBMC-WMM: 0.12sec
CBMC-SC: 0.06sec
CImpact: ERROR/TIMEOUT[8] 223.35sec
Checkfence: 0.01sec
ESBMC: 0.04sec
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): 0.26sec
Cycles
SatAbs:
8.41sec (x4.22)

Satabs-prefix-first: 4.85sec
CBMC-WMM: 0.11sec
CBMC-SC: 0.06sec
CImpact: ERROR/TIMEOUT[8] 224.41sec
ESBMC: 0.06sec
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): 0.25sec
Cycles
SatAbs:
8.72sec (x4.38)

Satabs-prefix-first: 4.84sec
CBMC-WMM: 0.11sec
CBMC-SC: 0.06sec
CImpact: ERROR/TIMEOUT[8] 224.55sec
ESBMC: 0.05sec
Threader-monolithic: ERROR/TIMEOUT[1] 0.07sec
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): 0.26sec
Cycles
SatAbs:
7.35sec (x3.69)

Satabs-prefix-first: 5.50sec
CBMC-WMM: 0.27sec
CBMC-SC: 0.06sec
CImpact: ERROR/TIMEOUT[8] 223.04sec
ESBMC: 0.05sec
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:
8.20sec (x4.12)

Satabs-prefix-first: 4.82sec
CBMC-WMM: 0.11sec
CBMC-SC: 0.06sec
CImpact: ERROR/TIMEOUT[8] 221.80sec
ESBMC: 0.05sec
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
Blender:
Cycles
SatAbs:
8.37sec (x4.20)

Satabs-prefix-first: 4.78sec
CBMC-WMM: 0.11sec
CBMC-SC: 0.06sec
CImpact: ERROR/TIMEOUT[8] 224.39sec
ESBMC: 0.05sec
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
Blender:
Cycles
SatAbs:
8.25sec (x4.14)

Satabs-prefix-first: 4.54sec
CBMC-WMM: 0.13sec
CBMC-SC: 0.04sec
CImpact: ERROR/TIMEOUT[8] 219.83sec
ESBMC: 0.04sec
Threader-monolithic: ERROR/TIMEOUT[1] 0.09sec
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:
8.19sec (x4.11)

Satabs-prefix-first: 4.69sec
CBMC-WMM: 0.13sec
CBMC-SC: 0.06sec
CImpact: ERROR/TIMEOUT[8] 220.19sec
ESBMC: 0.05sec
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
Cycles
SatAbs:
7.83sec (x3.93)

Satabs-prefix-first: 4.71sec
CBMC-WMM: 0.13sec
CBMC-SC: 0.06sec
CImpact: ERROR/TIMEOUT[8] 229.79sec
ESBMC: 0.05sec
Threader-monolithic: ERROR/TIMEOUT[1] 0.07sec
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:
8.36sec (x4.20)

Satabs-prefix-first: 4.78sec
CBMC-WMM: 0.14sec
CBMC-SC: 0.04sec
CImpact: ERROR/TIMEOUT[8] 222.49sec
ESBMC: 0.04sec
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:
6.46sec (x3.24)

Satabs-prefix-first: 3.74sec
CBMC-WMM: 0.12sec
CBMC-SC: 0.06sec
CImpact: ERROR/TIMEOUT[8] 222.02sec
ESBMC: 0.04sec
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
Cycles
SatAbs:
6.28sec (x3.15)

Satabs-prefix-first: 3.69sec
CBMC-WMM: 0.12sec
CBMC-SC: 0.06sec
CImpact: ERROR/TIMEOUT[8] 229.54sec
ESBMC: 0.05sec
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
ppc/aclwdrr008
SatAbs:
0.72sec

Satabs-prefix-first: 1.55sec
CBMC-WMM: 0.05sec
CBMC-SC: 0.04sec
CImpact: ERROR/TIMEOUT[8] 205.96sec
Checkfence: 0.01sec
ESBMC: 0.05sec
Threader-monolithic: 0.08sec
Threader-owicki-gries: 0.10sec
Threader-rely-guarantee: 0.10sec
Poirot-Integer: ERROR/TIMEOUT
Poirot-BitVector: ERROR/TIMEOUT
MMChecker (MM: sc): 0.48sec
Cycles
SatAbs:
2.62sec (x3.63)

Satabs-prefix-first: 4.69sec
CBMC-WMM: 0.12sec
CBMC-SC: 78.57sec
CImpact: ERROR/TIMEOUT[8] 304.70sec
ESBMC: 0.09sec
Threader-monolithic: ERROR/TIMEOUT[130] 897.47sec
Threader-owicki-gries: ERROR/TIMEOUT[130] 897.36sec
Threader-rely-guarantee: ERROR/TIMEOUT[130] 896.77sec
Poirot-Integer: ERROR/TIMEOUT
Poirot-BitVector: ERROR/TIMEOUT
MMChecker (MM: csharp): 0.33sec
Cycles
SatAbs:
6.05sec (x8.40)

Satabs-prefix-first: 3.43sec
CBMC-WMM: 0.10sec
CBMC-SC: 0.04sec
CImpact: ERROR/TIMEOUT[8] 221.38sec
Checkfence: 0.01sec
ESBMC: 0.04sec
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): 0.33sec
Cycles
SatAbs:
5.55sec (x7.70)

Satabs-prefix-first: 2.56sec
CBMC-WMM: 0.11sec
CBMC-SC: 0.05sec
CImpact: ERROR/TIMEOUT[8] 225.81sec
ESBMC: 0.05sec
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): 0.33sec
Cycles
SatAbs:
5.94sec (x8.25)

Satabs-prefix-first: 3.31sec
CBMC-WMM: 0.11sec
CBMC-SC: 0.05sec
CImpact: ERROR/TIMEOUT[8] 223.02sec
ESBMC: 0.04sec
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): 0.33sec
Cycles
SatAbs:
5.74sec (x7.97)

Satabs-prefix-first: 2.80sec
CBMC-WMM: 0.10sec
CBMC-SC: 0.06sec
CImpact: ERROR/TIMEOUT[8] 224.62sec
ESBMC: 0.03sec
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:
4.67sec (x6.48)

Satabs-prefix-first: 2.30sec
CBMC-WMM: 0.10sec
CBMC-SC: 0.06sec
CImpact: ERROR/TIMEOUT[8] 224.08sec
ESBMC: 0.05sec
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:
4.45sec (x6.18)

Satabs-prefix-first: 2.35sec
CBMC-WMM: 0.10sec
CBMC-SC: 0.06sec
CImpact: ERROR/TIMEOUT[8] 222.04sec
ESBMC: 0.05sec
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
Blender:
Cycles
SatAbs:
4.79sec (x6.65)

Satabs-prefix-first: 2.66sec
CBMC-WMM: 0.11sec
CBMC-SC: 0.04sec
CImpact: ERROR/TIMEOUT[8] 221.11sec
ESBMC: 0.05sec
Threader-monolithic: ERROR/TIMEOUT[1] 0.08sec
Threader-owicki-gries: ERROR/TIMEOUT[1] 0.08sec
Threader-rely-guarantee: ERROR/TIMEOUT[1] 0.09sec
Poirot-Integer: ERROR/TIMEOUT
Poirot-BitVector: ERROR/TIMEOUT
Cycles
SatAbs:
4.74sec (x6.58)

Satabs-prefix-first: 2.53sec
CBMC-WMM: 0.12sec
CBMC-SC: 0.06sec
CImpact: ERROR/TIMEOUT[8] 233.72sec
ESBMC: 0.04sec
Threader-monolithic: ERROR/TIMEOUT[1] 0.06sec
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:
4.75sec (x6.59)

Satabs-prefix-first: 2.46sec
CBMC-WMM: 0.13sec
CBMC-SC: 0.05sec
CImpact: ERROR/TIMEOUT[8] 221.72sec
ESBMC: 0.04sec
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:
163.90sec (x227.63)

Satabs-prefix-first: ERROR/TIMEOUT[100] 529.47sec
CBMC-WMM: 0.11sec
CBMC-SC: 11.09sec
CImpact: ERROR/TIMEOUT[8] 281.13sec
ESBMC: 0.06sec
Threader-monolithic: ERROR/TIMEOUT[130] 897.53sec
Threader-owicki-gries: ERROR/TIMEOUT[130] 897.55sec
Threader-rely-guarantee: ERROR/TIMEOUT[130] 897.29sec
Poirot-Integer: ERROR/TIMEOUT
Poirot-BitVector: ERROR/TIMEOUT
Cycles
SatAbs:
163.83sec (x227.54)

Satabs-prefix-first: ERROR/TIMEOUT[100] 525.63sec
CBMC-WMM: 0.13sec
CBMC-SC: 10.99sec
CImpact: ERROR/TIMEOUT[8] 292.85sec
ESBMC: 0.07sec
Threader-monolithic: ERROR/TIMEOUT[130] 897.43sec
Threader-owicki-gries: ERROR/TIMEOUT[130] 897.51sec
Threader-rely-guarantee: ERROR/TIMEOUT[130] 897.45sec
Poirot-Integer: ERROR/TIMEOUT
Poirot-BitVector: ERROR/TIMEOUT
Cycles
SatAbs:
163.91sec (x227.65)

Satabs-prefix-first: ERROR/TIMEOUT[100] 511.69sec
CBMC-WMM: 0.13sec
CBMC-SC: 11.52sec
CImpact: ERROR/TIMEOUT[8] 284.38sec
ESBMC: 0.07sec
Threader-monolithic: ERROR/TIMEOUT[130] 897.51sec
Threader-owicki-gries: ERROR/TIMEOUT[130] 897.63sec
Threader-rely-guarantee: ERROR/TIMEOUT[130] 897.45sec
Poirot-Integer: ERROR/TIMEOUT
Poirot-BitVector: ERROR/TIMEOUT
ppc/aclwdrr009
SatAbs:
2.24sec

Satabs-prefix-first: 2.75sec
CBMC-WMM: 0.06sec
CBMC-SC: 0.06sec
CImpact: ERROR/TIMEOUT[8] 207.66sec
Checkfence: 0.01sec
ESBMC: 0.05sec
Threader-monolithic: 0.10sec
Threader-owicki-gries: 0.10sec
Threader-rely-guarantee: 0.11sec
Poirot-Integer: ERROR/TIMEOUT
Poirot-BitVector: ERROR/TIMEOUT
MMChecker (MM: sc): 0.33sec
Cycles
SatAbs:
124.59sec (x55.62)

Satabs-prefix-first: 276.76sec
CBMC-WMM: 0.12sec
CBMC-SC: 40.35sec
CImpact: ERROR/TIMEOUT[8] 293.37sec
ESBMC: 0.08sec
Threader-monolithic: ERROR/TIMEOUT[130] 897.29sec
Threader-owicki-gries: ERROR/TIMEOUT[130] 897.40sec
Threader-rely-guarantee: ERROR/TIMEOUT[130] 897.50sec
Poirot-Integer: ERROR/TIMEOUT
Poirot-BitVector: ERROR/TIMEOUT
MMChecker (MM: csharp): 0.33sec
Cycles
SatAbs:
6.36sec (x2.83)

Satabs-prefix-first: 4.36sec
CBMC-WMM: 0.12sec
CBMC-SC: 0.06sec
CImpact: ERROR/TIMEOUT[8] 219.21sec
Checkfence: 0.01sec
ESBMC: 0.04sec
Threader-monolithic: ERROR/TIMEOUT[1] 0.09sec
Threader-owicki-gries: ERROR/TIMEOUT[1] 0.11sec
Threader-rely-guarantee: ERROR/TIMEOUT[1] 0.07sec
Poirot-Integer: ERROR/TIMEOUT
Poirot-BitVector: ERROR/TIMEOUT
MMChecker (MM: csharp): 0.33sec
Cycles
SatAbs:
6.60sec (x2.94)

Satabs-prefix-first: 4.23sec
CBMC-WMM: 0.12sec
CBMC-SC: 0.06sec
CImpact: ERROR/TIMEOUT[8] 220.64sec
ESBMC: 0.04sec
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.34sec
Cycles
SatAbs:
6.09sec (x2.71)

Satabs-prefix-first: 4.76sec
CBMC-WMM: 0.09sec
CBMC-SC: 0.05sec
CImpact: ERROR/TIMEOUT[8] 220.11sec
ESBMC: 0.05sec
Threader-monolithic: ERROR/TIMEOUT[1] 0.08sec
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): 0.33sec
Cycles
SatAbs:
6.91sec (x3.08)

Satabs-prefix-first: 4.85sec
CBMC-WMM: 0.12sec
CBMC-SC: 0.06sec
CImpact: ERROR/TIMEOUT[8] 219.36sec
ESBMC: 0.05sec
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.78sec (x3.02)

Satabs-prefix-first: 4.67sec
CBMC-WMM: 0.12sec
CBMC-SC: 0.05sec
CImpact: ERROR/TIMEOUT[8] 220.42sec
ESBMC: 0.05sec
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
Blender:
Cycles
SatAbs:
7.26sec (x3.24)

Satabs-prefix-first: 4.65sec
CBMC-WMM: 0.12sec
CBMC-SC: 0.05sec
CImpact: ERROR/TIMEOUT[8] 219.77sec
ESBMC: 0.05sec
Threader-monolithic: ERROR/TIMEOUT[1] 0.07sec
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.86sec (x3.06)

Satabs-prefix-first: 4.59sec
CBMC-WMM: 0.12sec
CBMC-SC: 0.06sec
CImpact: ERROR/TIMEOUT[8] 222.93sec
ESBMC: 0.06sec
Threader-monolithic: ERROR/TIMEOUT[1] 0.09sec
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:
7.92sec (x3.53)

Satabs-prefix-first: 4.33sec
CBMC-WMM: 0.14sec
CBMC-SC: 0.06sec
CImpact: ERROR/TIMEOUT[8] 219.36sec
ESBMC: 0.07sec
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:
6.29sec (x2.80)

Satabs-prefix-first: 4.18sec
CBMC-WMM: 0.11sec
CBMC-SC: 0.04sec
CImpact: ERROR/TIMEOUT[8] 220.46sec
ESBMC: 0.05sec
Threader-monolithic: ERROR/TIMEOUT[1] 0.10sec
Threader-owicki-gries: ERROR/TIMEOUT[1] 0.05sec
Threader-rely-guarantee: ERROR/TIMEOUT[1] 0.10sec
Poirot-Integer: ERROR/TIMEOUT
Poirot-BitVector: ERROR/TIMEOUT
Cycles
SatAbs:
174.95sec (x78.10)

Satabs-prefix-first: 848.65sec
CBMC-WMM: 0.12sec
CBMC-SC: 53.00sec
CImpact: ERROR/TIMEOUT[8] 284.77sec
ESBMC: 0.05sec
Threader-monolithic: ERROR/TIMEOUT[130] 897.45sec
Threader-owicki-gries: ERROR/TIMEOUT[130] 897.43sec
Threader-rely-guarantee: ERROR/TIMEOUT[130] 897.48sec
Poirot-Integer: ERROR/TIMEOUT
Poirot-BitVector: ERROR/TIMEOUT
Cycles
SatAbs:
152.86sec (x68.24)

Satabs-prefix-first: 825.20sec
CBMC-WMM: 0.14sec
CBMC-SC: 52.93sec
CImpact: ERROR/TIMEOUT[8] 284.17sec
ESBMC: 0.06sec
Threader-monolithic: ERROR/TIMEOUT[130] 897.56sec
Threader-owicki-gries: ERROR/TIMEOUT[130] 897.49sec
Threader-rely-guarantee: ERROR/TIMEOUT[130] 897.55sec
Poirot-Integer: ERROR/TIMEOUT
Poirot-BitVector: ERROR/TIMEOUT
Cycles
SatAbs:
109.48sec (x48.87)

Satabs-prefix-first: 40.40sec
CBMC-WMM: 0.12sec
CBMC-SC: 46.39sec
CImpact: ERROR/TIMEOUT[8] 265.75sec
ESBMC: 0.06sec
Threader-monolithic: ERROR/TIMEOUT[130] 897.52sec
Threader-owicki-gries: ERROR/TIMEOUT[130] 897.52sec
Threader-rely-guarantee: ERROR/TIMEOUT[130] 897.40sec
Poirot-Integer: ERROR/TIMEOUT
Poirot-BitVector: ERROR/TIMEOUT
ppc/aclwdrr010
SatAbs:
0.68sec

Satabs-prefix-first: 0.65sec
CBMC-WMM: 0.05sec
CBMC-SC: 0.06sec
CImpact: ERROR/TIMEOUT[8] 196.80sec
Checkfence: 0.01sec
ESBMC: 0.04sec
Threader-monolithic: 0.09sec
Threader-owicki-gries: 0.10sec
Threader-rely-guarantee: 0.09sec
Poirot-Integer: ERROR/TIMEOUT
Poirot-BitVector: ERROR/TIMEOUT
MMChecker (MM: sc): 0.28sec
Cycles
SatAbs:
2.26sec (x3.32)

Satabs-prefix-first: 1.71sec
CBMC-WMM: 0.12sec
CBMC-SC: 15.64sec
CImpact: ERROR/TIMEOUT[8] 296.85sec
ESBMC: 0.08sec
Threader-monolithic: ERROR/TIMEOUT[130] 897.45sec
Threader-owicki-gries: ERROR/TIMEOUT[130] 897.63sec
Threader-rely-guarantee: ERROR/TIMEOUT[130] 897.43sec
Poirot-Integer: ERROR/TIMEOUT
Poirot-BitVector: ERROR/TIMEOUT
MMChecker (MM: csharp): 0.27sec
Cycles
SatAbs:
5.54sec (x8.14)

Satabs-prefix-first: 4.04sec
CBMC-WMM: 0.12sec
CBMC-SC: 0.04sec
CImpact: ERROR/TIMEOUT[8] 226.02sec
Checkfence: 0.01sec
ESBMC: 0.05sec
Threader-monolithic: ERROR/TIMEOUT[1] 0.06sec
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): 0.26sec
Cycles
SatAbs:
5.52sec (x8.11)

Satabs-prefix-first: 4.04sec
CBMC-WMM: 0.11sec
CBMC-SC: 0.05sec
CImpact: ERROR/TIMEOUT[8] 226.84sec
ESBMC: 0.04sec
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): 0.27sec
Cycles
SatAbs:
5.63sec (x8.27)

Satabs-prefix-first: 3.91sec
CBMC-WMM: 0.12sec
CBMC-SC: 0.04sec
CImpact: ERROR/TIMEOUT[8] 228.25sec
ESBMC: 0.06sec
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): 0.27sec
Cycles
SatAbs:
5.71sec (x8.39)

Satabs-prefix-first: 4.21sec
CBMC-WMM: 0.12sec
CBMC-SC: 0.06sec
CImpact: ERROR/TIMEOUT[8] 239.16sec
ESBMC: 0.05sec
Threader-monolithic: ERROR/TIMEOUT[1] 0.07sec
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:
5.63sec (x8.27)

Satabs-prefix-first: 3.91sec
CBMC-WMM: 0.12sec
CBMC-SC: 0.06sec
CImpact: ERROR/TIMEOUT[8] 231.37sec
ESBMC: 0.06sec
Threader-monolithic: ERROR/TIMEOUT[1] 0.09sec
Threader-owicki-gries: ERROR/TIMEOUT[1] 0.06sec
Threader-rely-guarantee: ERROR/TIMEOUT[1] 0.08sec
Poirot-Integer: ERROR/TIMEOUT
Poirot-BitVector: ERROR/TIMEOUT
Blender:
Cycles
SatAbs:
5.27sec (x7.75)

Satabs-prefix-first: 3.80sec
CBMC-WMM: 0.12sec
CBMC-SC: 0.04sec
CImpact: ERROR/TIMEOUT[8] 239.96sec
ESBMC: 0.04sec
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
Blender:
Cycles
SatAbs:
5.57sec (x8.19)

Satabs-prefix-first: 4.05sec
CBMC-WMM: 0.12sec
CBMC-SC: 0.04sec
CImpact: ERROR/TIMEOUT[8] 227.75sec
ESBMC: 0.05sec
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
Cycles
SatAbs:
5.56sec (x8.17)

Satabs-prefix-first: 3.89sec
CBMC-WMM: 0.10sec
CBMC-SC: 0.05sec
CImpact: ERROR/TIMEOUT[8] 225.15sec
ESBMC: 0.05sec
Threader-monolithic: ERROR/TIMEOUT[1] 0.07sec
Threader-owicki-gries: ERROR/TIMEOUT[1] 0.08sec
Threader-rely-guarantee: ERROR/TIMEOUT[1] 0.09sec
Poirot-Integer: ERROR/TIMEOUT
Poirot-BitVector: ERROR/TIMEOUT
Cycles
SatAbs:
5.29sec (x7.77)

Satabs-prefix-first: 3.88sec
CBMC-WMM: 0.13sec
CBMC-SC: 0.05sec
CImpact: ERROR/TIMEOUT[8] 227.88sec
ESBMC: 0.04sec
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
Cycles
SatAbs:
35.54sec (x52.26)

Satabs-prefix-first: 28.82sec
CBMC-WMM: 0.11sec
CBMC-SC: 0.80sec
CImpact: ERROR/TIMEOUT[8] 210.00sec
ESBMC: 0.05sec
Threader-monolithic: ERROR/TIMEOUT[1] 302.59sec
Threader-owicki-gries: ERROR/TIMEOUT[1] 304.57sec
Threader-rely-guarantee: ERROR/TIMEOUT[1] 303.65sec
Poirot-Integer: ERROR/TIMEOUT
Poirot-BitVector: ERROR/TIMEOUT
Cycles
SatAbs:
34.90sec (x51.32)

Satabs-prefix-first: 28.61sec
CBMC-WMM: 0.11sec
CBMC-SC: 0.77sec
CImpact: ERROR/TIMEOUT[8] 209.30sec
ESBMC: 0.07sec
Threader-monolithic: ERROR/TIMEOUT[1] 303.45sec
Threader-owicki-gries: ERROR/TIMEOUT[1] 303.58sec
Threader-rely-guarantee: ERROR/TIMEOUT[1] 306.31sec
Poirot-Integer: ERROR/TIMEOUT
Poirot-BitVector: ERROR/TIMEOUT
Cycles
SatAbs:
33.99sec (x49.98)

Satabs-prefix-first: 28.77sec
CBMC-WMM: 0.12sec
CBMC-SC: 0.77sec
CImpact: ERROR/TIMEOUT[8] 208.58sec
ESBMC: 0.05sec
Threader-monolithic: ERROR/TIMEOUT[1] 302.73sec
Threader-owicki-gries: ERROR/TIMEOUT[1] 303.76sec
Threader-rely-guarantee: ERROR/TIMEOUT[1] 303.98sec
Poirot-Integer: ERROR/TIMEOUT
Poirot-BitVector: ERROR/TIMEOUT
ppc/aclwdrr011
SatAbs:
0.75sec

Satabs-prefix-first: 0.76sec
CBMC-WMM: 0.06sec
CBMC-SC: 0.05sec
CImpact: ERROR/TIMEOUT[8] 192.78sec
Checkfence: 0.01sec
ESBMC: 0.02sec
Threader-monolithic: 0.11sec
Threader-owicki-gries: 0.10sec
Threader-rely-guarantee: 0.11sec
Poirot-Integer: ERROR/TIMEOUT
Poirot-BitVector: ERROR/TIMEOUT
MMChecker (MM: sc): 0.28sec
Cycles
SatAbs:
1.97sec (x2.62)

Satabs-prefix-first: 1.47sec
CBMC-WMM: 0.13sec
CBMC-SC: 6.29sec
CImpact: ERROR/TIMEOUT[8] 292.37sec
ESBMC: 0.06sec
Threader-monolithic: ERROR/TIMEOUT[130] 897.59sec
Threader-owicki-gries: ERROR/TIMEOUT[130] 897.55sec
Threader-rely-guarantee: ERROR/TIMEOUT[130] 897.42sec
Poirot-Integer: ERROR/TIMEOUT
Poirot-BitVector: ERROR/TIMEOUT
MMChecker (MM: csharp): 0.29sec
Cycles
SatAbs:
4.73sec (x6.30)

Satabs-prefix-first: 3.95sec
CBMC-WMM: 0.13sec
CBMC-SC: 0.05sec
CImpact: ERROR/TIMEOUT[8] 221.05sec
Checkfence: 0.01sec
ESBMC: 0.05sec
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): 0.27sec
Cycles
SatAbs:
5.72sec (x7.62)

Satabs-prefix-first: 4.36sec
CBMC-WMM: 0.11sec
CBMC-SC: 0.04sec
CImpact: ERROR/TIMEOUT[8] 222.55sec
ESBMC: 0.03sec
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
MMChecker (MM: csharp): 0.27sec
Cycles
SatAbs:
5.38sec (x7.17)

Satabs-prefix-first: 4.59sec
CBMC-WMM: 0.12sec
CBMC-SC: 0.06sec
CImpact: ERROR/TIMEOUT[8] 225.47sec
ESBMC: 0.05sec
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): 0.26sec
Cycles
SatAbs:
5.65sec (x7.53)

Satabs-prefix-first: 4.52sec
CBMC-WMM: 0.13sec
CBMC-SC: 0.05sec
CImpact: ERROR/TIMEOUT[8] 223.32sec
ESBMC: 0.05sec
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:
5.37sec (x7.16)

Satabs-prefix-first: 4.43sec
CBMC-WMM: 0.13sec
CBMC-SC: 0.05sec
CImpact: ERROR/TIMEOUT[8] 239.79sec
ESBMC: 0.03sec
Threader-monolithic: ERROR/TIMEOUT[1] 0.08sec
Threader-owicki-gries: ERROR/TIMEOUT[1] 0.07sec
Threader-rely-guarantee: ERROR/TIMEOUT[1] 0.07sec
Poirot-Integer: ERROR/TIMEOUT
Poirot-BitVector: ERROR/TIMEOUT
Blender:
Cycles
SatAbs:
5.76sec (x7.68)

Satabs-prefix-first: 4.49sec
CBMC-WMM: 0.13sec
CBMC-SC: 0.05sec
CImpact: ERROR/TIMEOUT[8] 224.48sec
ESBMC: 0.03sec
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:
5.52sec (x7.36)

Satabs-prefix-first: 4.84sec
CBMC-WMM: 0.14sec
CBMC-SC: 0.06sec
CImpact: ERROR/TIMEOUT[8] 223.98sec
ESBMC: 0.03sec
Threader-monolithic: ERROR/TIMEOUT[1] 0.06sec
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:
5.32sec (x7.09)

Satabs-prefix-first: 4.68sec
CBMC-WMM: 0.13sec
CBMC-SC: 0.05sec
CImpact: ERROR/TIMEOUT[8] 222.34sec
ESBMC: 0.05sec
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
Cycles
SatAbs:
5.68sec (x7.57)

Satabs-prefix-first: 4.61sec
CBMC-WMM: 0.13sec
CBMC-SC: 0.05sec
CImpact: ERROR/TIMEOUT[8] 223.45sec
ESBMC: 0.05sec
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:
258.87sec (x345.16)

Satabs-prefix-first: 233.24sec
CBMC-WMM: 0.12sec
CBMC-SC: 10.94sec
CImpact: ERROR/TIMEOUT[8] 283.10sec
ESBMC: 0.06sec
Threader-monolithic: ERROR/TIMEOUT[130] 897.70sec
Threader-owicki-gries: ERROR/TIMEOUT[130] 897.38sec
Threader-rely-guarantee: ERROR/TIMEOUT[130] 897.44sec
Poirot-Integer: ERROR/TIMEOUT
Poirot-BitVector: ERROR/TIMEOUT
Cycles
SatAbs:
34.01sec (x45.34)

Satabs-prefix-first: 25.94sec
CBMC-WMM: 0.12sec
CBMC-SC: 0.88sec
CImpact: ERROR/TIMEOUT[8] 211.36sec
ESBMC: 0.05sec
Threader-monolithic: ERROR/TIMEOUT[1] 303.95sec
Threader-owicki-gries: ERROR/TIMEOUT[1] 304.71sec
Threader-rely-guarantee: ERROR/TIMEOUT[1] 304.11sec
Poirot-Integer: ERROR/TIMEOUT
Poirot-BitVector: ERROR/TIMEOUT
Cycles
SatAbs:
33.63sec (x44.84)

Satabs-prefix-first: 25.50sec
CBMC-WMM: 0.12sec
CBMC-SC: 0.89sec
CImpact: ERROR/TIMEOUT[8] 212.00sec
ESBMC: 0.07sec
Threader-monolithic: ERROR/TIMEOUT[1] 305.08sec
Threader-owicki-gries: ERROR/TIMEOUT[1] 305.55sec
Threader-rely-guarantee: ERROR/TIMEOUT[1] 303.83sec
Poirot-Integer: ERROR/TIMEOUT
Poirot-BitVector: ERROR/TIMEOUT
ppc/aclwdrr012
SatAbs:
0.67sec

Satabs-prefix-first: 0.39sec
CBMC-WMM: 0.04sec
CBMC-SC: 0.03sec
CImpact: 0.34sec
Checkfence: 0.01sec
ESBMC: 0.05sec
Threader-monolithic: 0.10sec
Threader-owicki-gries: 0.10sec
Threader-rely-guarantee: 0.10sec
Poirot-Integer: ERROR/TIMEOUT
Poirot-BitVector: ERROR/TIMEOUT
MMChecker (MM: sc): 0.11sec
Cycles
SatAbs:
12.17sec (x18.16)

Satabs-prefix-first: 14.29sec
CBMC-WMM: 0.08sec
CBMC-SC: 3.78sec
CImpact: 25.14sec
ESBMC: 0.08sec
Threader-monolithic: ERROR/TIMEOUT[130] 896.78sec
Threader-owicki-gries: ERROR/TIMEOUT[130] 896.84sec
Threader-rely-guarantee: ERROR/TIMEOUT[130] 896.58sec
Poirot-Integer: ERROR/TIMEOUT
Poirot-BitVector: ERROR/TIMEOUT
MMChecker (MM: csharp): 0.12sec
Cycles
SatAbs:
0.93sec (x1.38)

Satabs-prefix-first: 1.30sec
CBMC-WMM: 0.07sec
CBMC-SC: 0.04sec
CImpact: 9.00sec
Checkfence: 0.01sec
ESBMC: 0.05sec
Threader-monolithic: ERROR/TIMEOUT[1] 0.07sec
Threader-owicki-gries: ERROR/TIMEOUT[1] 0.05sec
Threader-rely-guarantee: ERROR/TIMEOUT[1] 0.08sec
Poirot-Integer: ERROR/TIMEOUT
Poirot-BitVector: ERROR/TIMEOUT
MMChecker (MM: csharp): 0.11sec
Cycles
SatAbs:
0.97sec (x1.44)

Satabs-prefix-first: 1.31sec
CBMC-WMM: 0.07sec
CBMC-SC: 0.04sec
CImpact: 9.03sec
ESBMC: 0.04sec
Threader-monolithic: ERROR/TIMEOUT[1] 0.07sec
Threader-owicki-gries: ERROR/TIMEOUT[1] 0.08sec
Threader-rely-guarantee: ERROR/TIMEOUT[1] 0.04sec
Poirot-Integer: ERROR/TIMEOUT
Poirot-BitVector: ERROR/TIMEOUT
MMChecker (MM: csharp): 0.11sec
Cycles
SatAbs:
0.92sec (x1.37)

Satabs-prefix-first: 1.28sec
CBMC-WMM: 0.07sec
CBMC-SC: 0.03sec
CImpact: 8.87sec
ESBMC: 0.05sec
Threader-monolithic: ERROR/TIMEOUT[1] 0.06sec
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): 0.12sec
Cycles
SatAbs:
0.92sec (x1.37)

Satabs-prefix-first: 1.24sec
CBMC-WMM: 0.07sec
CBMC-SC: 0.04sec
CImpact: 8.92sec
ESBMC: 0.04sec
Threader-monolithic: ERROR/TIMEOUT[1] 0.08sec
Threader-owicki-gries: ERROR/TIMEOUT[1] 0.06sec
Threader-rely-guarantee: ERROR/TIMEOUT[1] 0.06sec
Poirot-Integer: ERROR/TIMEOUT
Poirot-BitVector: ERROR/TIMEOUT
Blender:
Cycles
SatAbs:
0.84sec (x1.25)

Satabs-prefix-first: 1.30sec
CBMC-WMM: 0.06sec
CBMC-SC: 0.03sec
CImpact: 8.88sec
ESBMC: 0.05sec
Threader-monolithic: ERROR/TIMEOUT[1] 0.08sec
Threader-owicki-gries: ERROR/TIMEOUT[1] 0.07sec
Threader-rely-guarantee: ERROR/TIMEOUT[1] 0.08sec
Poirot-Integer: ERROR/TIMEOUT
Poirot-BitVector: ERROR/TIMEOUT
Blender:
Cycles
SatAbs:
0.89sec (x1.32)

Satabs-prefix-first: 1.19sec
CBMC-WMM: 0.06sec
CBMC-SC: 0.03sec
CImpact: 8.96sec
ESBMC: 0.05sec
Threader-monolithic: ERROR/TIMEOUT[1] 0.07sec
Threader-owicki-gries: ERROR/TIMEOUT[1] 0.06sec
Threader-rely-guarantee: ERROR/TIMEOUT[1] 0.08sec
Poirot-Integer: ERROR/TIMEOUT
Poirot-BitVector: ERROR/TIMEOUT
Blender:
Cycles
SatAbs:
0.86sec (x1.28)

Satabs-prefix-first: 1.27sec
CBMC-WMM: 0.08sec
CBMC-SC: 0.04sec
CImpact: 8.78sec
ESBMC: 0.03sec
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.95sec (x1.41)

Satabs-prefix-first: 1.35sec
CBMC-WMM: 0.08sec
CBMC-SC: 0.03sec
CImpact: 8.89sec
ESBMC: 0.05sec
Threader-monolithic: ERROR/TIMEOUT[1] 0.08sec
Threader-owicki-gries: ERROR/TIMEOUT[1] 0.07sec
Threader-rely-guarantee: ERROR/TIMEOUT[1] 0.08sec
Poirot-Integer: ERROR/TIMEOUT
Poirot-BitVector: ERROR/TIMEOUT
Cycles
SatAbs:
0.86sec (x1.28)

Satabs-prefix-first: 1.22sec
CBMC-WMM: 0.08sec
CBMC-SC: 0.03sec
CImpact: 8.85sec
ESBMC: 0.04sec
Threader-monolithic: ERROR/TIMEOUT[1] 0.08sec
Threader-owicki-gries: ERROR/TIMEOUT[1] 0.07sec
Threader-rely-guarantee: ERROR/TIMEOUT[1] 0.08sec
Poirot-Integer: ERROR/TIMEOUT
Poirot-BitVector: ERROR/TIMEOUT
Cycles
SatAbs:
22.34sec (x33.34)

Satabs-prefix-first: 7.43sec
CBMC-WMM: 0.08sec
CBMC-SC: 0.67sec
CImpact: 3.60sec
ESBMC: 0.05sec
Threader-monolithic: ERROR/TIMEOUT[1] 251.33sec
Threader-owicki-gries: ERROR/TIMEOUT[1] 251.99sec
Threader-rely-guarantee: ERROR/TIMEOUT[1] 250.52sec
Poirot-Integer: ERROR/TIMEOUT
Poirot-BitVector: ERROR/TIMEOUT
Cycles
SatAbs:
22.83sec (x34.07)

Satabs-prefix-first: 7.60sec
CBMC-WMM: 0.08sec
CBMC-SC: 0.66sec
CImpact: 3.59sec
ESBMC: 0.05sec
Threader-monolithic: ERROR/TIMEOUT[1] 251.77sec
Threader-owicki-gries: ERROR/TIMEOUT[1] 250.94sec
Threader-rely-guarantee: ERROR/TIMEOUT[1] 251.93sec
Poirot-Integer: ERROR/TIMEOUT
Poirot-BitVector: ERROR/TIMEOUT
Cycles
SatAbs:
22.47sec (x33.53)

Satabs-prefix-first: 7.39sec
CBMC-WMM: 0.08sec
CBMC-SC: 0.67sec
CImpact: 3.64sec
ESBMC: 0.06sec
Threader-monolithic: ERROR/TIMEOUT[1] 252.32sec
Threader-owicki-gries: ERROR/TIMEOUT[1] 250.73sec
Threader-rely-guarantee: ERROR/TIMEOUT[1] 251.62sec
Poirot-Integer: ERROR/TIMEOUT
Poirot-BitVector: ERROR/TIMEOUT
ppc/aclwdrr013
SatAbs:
1.73sec

Satabs-prefix-first: 1.11sec
CBMC-WMM: 0.07sec
CBMC-SC: 0.06sec
CImpact: ERROR/TIMEOUT[8] 193.73sec
Checkfence: 0.01sec
ESBMC: 0.04sec
Threader-monolithic: 0.12sec
Threader-owicki-gries: 0.12sec
Threader-rely-guarantee: 0.12sec
Poirot-Integer: ERROR/TIMEOUT
Poirot-BitVector: ERROR/TIMEOUT
MMChecker (MM: sc): 0.29sec
Cycles
SatAbs:
46.47sec (x26.86)

Satabs-prefix-first: 55.01sec
CBMC-WMM: 0.12sec
CBMC-SC: 18.07sec
CImpact: ERROR/TIMEOUT[8] 281.61sec
ESBMC: 0.05sec
Threader-monolithic: ERROR/TIMEOUT[130] 896.73sec
Threader-owicki-gries: ERROR/TIMEOUT[130] 897.39sec
Threader-rely-guarantee: ERROR/TIMEOUT[130] 897.41sec
Poirot-Integer: ERROR/TIMEOUT
Poirot-BitVector: ERROR/TIMEOUT
MMChecker (MM: csharp): 0.26sec
Cycles
SatAbs:
7.15sec (x4.13)

Satabs-prefix-first: 4.72sec
CBMC-WMM: 0.12sec
CBMC-SC: 0.05sec
CImpact: ERROR/TIMEOUT[8] 211.53sec
Checkfence: 0.01sec
ESBMC: 0.04sec
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): 0.25sec
Cycles
SatAbs:
6.84sec (x3.95)

Satabs-prefix-first: 4.60sec
CBMC-WMM: 0.10sec
CBMC-SC: 0.06sec
CImpact: ERROR/TIMEOUT[8] 219.53sec
ESBMC: 0.04sec
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): 0.26sec
Cycles
SatAbs:
7.12sec (x4.11)

Satabs-prefix-first: 4.75sec
CBMC-WMM: 0.11sec
CBMC-SC: 0.06sec
CImpact: ERROR/TIMEOUT[8] 209.51sec
ESBMC: 0.05sec
Threader-monolithic: ERROR/TIMEOUT[1] 0.09sec
Threader-owicki-gries: ERROR/TIMEOUT[1] 0.08sec
Threader-rely-guarantee: ERROR/TIMEOUT[1] 0.06sec
Poirot-Integer: ERROR/TIMEOUT
Poirot-BitVector: ERROR/TIMEOUT
MMChecker (MM: csharp): 0.25sec
Cycles
SatAbs:
7.23sec (x4.17)

Satabs-prefix-first: 4.65sec
CBMC-WMM: 0.12sec
CBMC-SC: 0.06sec
CImpact: ERROR/TIMEOUT[8] 210.59sec
ESBMC: 0.05sec
Threader-monolithic: ERROR/TIMEOUT[1] 0.06sec
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.90sec (x3.98)

Satabs-prefix-first: 4.57sec
CBMC-WMM: 0.10sec
CBMC-SC: 0.04sec
CImpact: ERROR/TIMEOUT[8] 212.15sec
ESBMC: 0.05sec
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:
7.12sec (x4.11)

Satabs-prefix-first: 4.69sec
CBMC-WMM: 0.12sec
CBMC-SC: 0.06sec
CImpact: ERROR/TIMEOUT[8] 212.28sec
ESBMC: 0.05sec
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:
6.67sec (x3.85)

Satabs-prefix-first: 4.64sec
CBMC-WMM: 0.13sec
CBMC-SC: 0.06sec
CImpact: ERROR/TIMEOUT[8] 211.43sec
ESBMC: 0.05sec
Threader-monolithic: ERROR/TIMEOUT[1] 0.09sec
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:
7.03sec (x4.06)

Satabs-prefix-first: 4.69sec
CBMC-WMM: 0.12sec
CBMC-SC: 0.06sec
CImpact: ERROR/TIMEOUT[8] 216.60sec
ESBMC: 0.05sec
Threader-monolithic: ERROR/TIMEOUT[1] 0.09sec
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:
7.29sec (x4.21)

Satabs-prefix-first: 4.63sec
CBMC-WMM: 0.12sec
CBMC-SC: 0.06sec
CImpact: ERROR/TIMEOUT[8] 210.12sec
ESBMC: 0.04sec
Threader-monolithic: ERROR/TIMEOUT[1] 0.09sec
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:
40.97sec (x23.68)

Satabs-prefix-first: 32.89sec
CBMC-WMM: 0.12sec
CBMC-SC: 0.78sec
CImpact: ERROR/TIMEOUT[8] 211.42sec
ESBMC: 0.07sec
Threader-monolithic: ERROR/TIMEOUT[1] 302.91sec
Threader-owicki-gries: ERROR/TIMEOUT[1] 304.63sec
Threader-rely-guarantee: ERROR/TIMEOUT[1] 304.71sec
Poirot-Integer: ERROR/TIMEOUT
Poirot-BitVector: ERROR/TIMEOUT
Cycles
SatAbs:
40.42sec (x23.36)

Satabs-prefix-first: 33.18sec
CBMC-WMM: 0.11sec
CBMC-SC: 0.80sec
CImpact: ERROR/TIMEOUT[8] 207.43sec
ESBMC: 0.05sec
Threader-monolithic: ERROR/TIMEOUT[1] 304.34sec
Threader-owicki-gries: ERROR/TIMEOUT[1] 304.73sec
Threader-rely-guarantee: ERROR/TIMEOUT[1] 303.06sec
Poirot-Integer: ERROR/TIMEOUT
Poirot-BitVector: ERROR/TIMEOUT
Cycles
SatAbs:
42.43sec (x24.52)

Satabs-prefix-first: 35.28sec
CBMC-WMM: 0.13sec
CBMC-SC: 0.86sec
CImpact: ERROR/TIMEOUT[8] 208.89sec
ESBMC: 0.07sec
Threader-monolithic: ERROR/TIMEOUT[1] 304.45sec
Threader-owicki-gries: ERROR/TIMEOUT[1] 305.29sec
Threader-rely-guarantee: ERROR/TIMEOUT[1] 304.19sec
Poirot-Integer: ERROR/TIMEOUT
Poirot-BitVector: ERROR/TIMEOUT
ppc/aclwdrr014
SatAbs:
1.16sec

Satabs-prefix-first: 1.62sec
CBMC-WMM: 0.06sec
CBMC-SC: 0.04sec
CImpact: ERROR/TIMEOUT[8] 201.49sec
Checkfence: 0.01sec
ESBMC: 0.06sec
Threader-monolithic: 0.10sec
Threader-owicki-gries: 0.09sec
Threader-rely-guarantee: 0.11sec
Poirot-Integer: ERROR/TIMEOUT
Poirot-BitVector: ERROR/TIMEOUT
MMChecker (MM: sc): 0.33sec
Cycles
SatAbs:
2.41sec (x2.07)

Satabs-prefix-first: 4.75sec
CBMC-WMM: 0.11sec
CBMC-SC: 59.41sec
CImpact: ERROR/TIMEOUT[8] 291.41sec
ESBMC: 0.06sec
Threader-monolithic: ERROR/TIMEOUT[130] 897.30sec
Threader-owicki-gries: ERROR/TIMEOUT[130] 896.59sec
Threader-rely-guarantee: ERROR/TIMEOUT[130] 897.10sec
Poirot-Integer: ERROR/TIMEOUT
Poirot-BitVector: ERROR/TIMEOUT
MMChecker (MM: csharp): 0.36sec
Cycles
SatAbs:
4.68sec (x4.03)

Satabs-prefix-first: 2.64sec
CBMC-WMM: 0.13sec
CBMC-SC: 0.06sec
CImpact: ERROR/TIMEOUT[8] 228.85sec
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): 0.35sec
Cycles
SatAbs:
4.94sec (x4.25)

Satabs-prefix-first: 2.76sec
CBMC-WMM: 0.12sec
CBMC-SC: 0.06sec
CImpact: ERROR/TIMEOUT[8] 230.38sec
ESBMC: 0.07sec
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
MMChecker (MM: csharp): 0.33sec
Cycles
SatAbs:
5.00sec (x4.31)

Satabs-prefix-first: 2.78sec
CBMC-WMM: 0.09sec
CBMC-SC: 0.05sec
CImpact: ERROR/TIMEOUT[8] 227.10sec
ESBMC: 0.07sec
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
MMChecker (MM: csharp): 0.35sec
Cycles
SatAbs:
4.90sec (x4.22)

Satabs-prefix-first: 2.76sec
CBMC-WMM: 0.10sec
CBMC-SC: 0.06sec
CImpact: ERROR/TIMEOUT[8] 227.93sec
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.10sec
Poirot-Integer: ERROR/TIMEOUT
Poirot-BitVector: ERROR/TIMEOUT
Blender:
Cycles
SatAbs:
4.85sec (x4.18)

Satabs-prefix-first: 2.84sec
CBMC-WMM: 0.11sec
CBMC-SC: 0.06sec
CImpact: ERROR/TIMEOUT[8] 227.12sec
ESBMC: 0.07sec
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
Blender:
Cycles
SatAbs:
5.02sec (x4.32)

Satabs-prefix-first: 2.72sec
CBMC-WMM: 0.11sec
CBMC-SC: 0.06sec
CImpact: ERROR/TIMEOUT[8] 241.59sec
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.08sec
Poirot-Integer: ERROR/TIMEOUT
Poirot-BitVector: ERROR/TIMEOUT
Blender:
Cycles
SatAbs:
5.10sec (x4.39)

Satabs-prefix-first: 2.86sec
CBMC-WMM: 0.18sec
CBMC-SC: 0.06sec
CImpact: ERROR/TIMEOUT[8] 232.03sec
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.09sec
Poirot-Integer: ERROR/TIMEOUT
Poirot-BitVector: ERROR/TIMEOUT
Cycles
SatAbs:
5.23sec (x4.50)

Satabs-prefix-first: 2.84sec
CBMC-WMM: 0.12sec
CBMC-SC: 0.06sec
CImpact: ERROR/TIMEOUT[8] 229.83sec
ESBMC: 0.04sec
Threader-monolithic: ERROR/TIMEOUT[1] 0.10sec
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:
4.94sec (x4.25)

Satabs-prefix-first: 2.80sec
CBMC-WMM: 0.13sec
CBMC-SC: 0.06sec
CImpact: ERROR/TIMEOUT[8] 232.22sec
ESBMC: 0.05sec
Threader-monolithic: ERROR/TIMEOUT[1] 0.07sec
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:
112.41sec (x96.90)

Satabs-prefix-first: ERROR/TIMEOUT[130] 915.07sec
CBMC-WMM: 0.13sec
CBMC-SC: 47.56sec
CImpact: ERROR/TIMEOUT[8] 306.89sec
ESBMC: 0.09sec
Threader-monolithic: ERROR/TIMEOUT[130] 897.61sec
Threader-owicki-gries: ERROR/TIMEOUT[130] 897.26sec
Threader-rely-guarantee: ERROR/TIMEOUT[130] 897.11sec
Poirot-Integer: ERROR/TIMEOUT
Poirot-BitVector: ERROR/TIMEOUT
Cycles
SatAbs:
31.43sec (x27.09)

Satabs-prefix-first: 34.00sec
CBMC-WMM: 0.13sec
CBMC-SC: 0.74sec
CImpact: ERROR/TIMEOUT[8] 211.96sec
ESBMC: 0.05sec
Threader-monolithic: ERROR/TIMEOUT[1] 338.26sec
Threader-owicki-gries: ERROR/TIMEOUT[1] 339.46sec
Threader-rely-guarantee: ERROR/TIMEOUT[1] 338.75sec
Poirot-Integer: ERROR/TIMEOUT
Poirot-BitVector: ERROR/TIMEOUT
Cycles
SatAbs:
32.00sec (x27.58)

Satabs-prefix-first: 35.63sec
CBMC-WMM: 0.19sec
CBMC-SC: 0.97sec
CImpact: ERROR/TIMEOUT[8] 216.51sec
ESBMC: 0.07sec
Threader-monolithic: ERROR/TIMEOUT[1] 340.52sec
Threader-owicki-gries: ERROR/TIMEOUT[1] 339.17sec
Threader-rely-guarantee: ERROR/TIMEOUT[1] 339.92sec
Poirot-Integer: ERROR/TIMEOUT
Poirot-BitVector: ERROR/TIMEOUT
ppc/aclwdrr015
SatAbs:
2.46sec

Satabs-prefix-first: 3.26sec
CBMC-WMM: 0.03sec
CBMC-SC: 0.06sec
CImpact: ERROR/TIMEOUT[8] 211.32sec
Checkfence: 0.01sec
ESBMC: 0.04sec
Threader-monolithic: 0.11sec
Threader-owicki-gries: 0.11sec
Threader-rely-guarantee: 0.11sec
Poirot-Integer: ERROR/TIMEOUT
Poirot-BitVector: ERROR/TIMEOUT
MMChecker (MM: sc): 0.33sec
Cycles
SatAbs:
2.42sec (x.98)

Satabs-prefix-first: 2.18sec
CBMC-WMM: 0.11sec
CBMC-SC: 14.92sec
CImpact: 0.01sec
ESBMC: 0.06sec
Threader-monolithic: ERROR/TIMEOUT[130] 897.56sec
Threader-owicki-gries: ERROR/TIMEOUT[130] 897.50sec
Threader-rely-guarantee: ERROR/TIMEOUT[130] 897.44sec
Poirot-Integer: ERROR/TIMEOUT
Poirot-BitVector: ERROR/TIMEOUT
MMChecker (MM: csharp): 0.35sec
Cycles
SatAbs:
6.29sec (x2.55)

Satabs-prefix-first: 3.74sec
CBMC-WMM: 0.13sec
CBMC-SC: 0.06sec
CImpact: ERROR/TIMEOUT[8] 232.06sec
Checkfence: 0.01sec
ESBMC: 0.03sec
Threader-monolithic: ERROR/TIMEOUT[1] 0.08sec
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): 0.34sec
Cycles
SatAbs:
6.54sec (x2.65)

Satabs-prefix-first: 4.03sec
CBMC-WMM: 0.13sec
CBMC-SC: 0.06sec
CImpact: ERROR/TIMEOUT[8] 235.39sec
ESBMC: 0.04sec
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): 0.35sec
Cycles
SatAbs:
6.74sec (x2.73)

Satabs-prefix-first: 4.02sec
CBMC-WMM: 0.12sec
CBMC-SC: 0.06sec
CImpact: ERROR/TIMEOUT[8] 234.83sec
ESBMC: 0.03sec
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): 0.35sec
Cycles
SatAbs:
6.91sec (x2.80)

Satabs-prefix-first: 4.05sec
CBMC-WMM: 0.13sec
CBMC-SC: 0.05sec
CImpact: ERROR/TIMEOUT[8] 243.36sec
ESBMC: 0.04sec
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
Blender:
Cycles
SatAbs:
7.35sec (x2.98)

Satabs-prefix-first: 4.34sec
CBMC-WMM: 0.12sec
CBMC-SC: 0.06sec
CImpact: ERROR/TIMEOUT[8] 230.83sec
ESBMC: 0.06sec
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:
6.26sec (x2.54)

Satabs-prefix-first: 3.61sec
CBMC-WMM: 0.10sec
CBMC-SC: 0.06sec
CImpact: ERROR/TIMEOUT[8] 228.29sec
ESBMC: 0.07sec
Threader-monolithic: ERROR/TIMEOUT[1] 0.07sec
Threader-owicki-gries: ERROR/TIMEOUT[1] 0.10sec
Threader-rely-guarantee: ERROR/TIMEOUT[1] 0.09sec
Poirot-Integer: ERROR/TIMEOUT
Poirot-BitVector: ERROR/TIMEOUT
Blender:
Cycles
SatAbs:
6.16sec (x2.50)

Satabs-prefix-first: 3.79sec
CBMC-WMM: 0.11sec
CBMC-SC: 0.07sec
CImpact: ERROR/TIMEOUT[8] 230.04sec
ESBMC: 0.06sec
Threader-monolithic: ERROR/TIMEOUT[1] 0.09sec
Threader-owicki-gries: ERROR/TIMEOUT[1] 0.07sec
Threader-rely-guarantee: ERROR/TIMEOUT[1] 0.08sec
Poirot-Integer: ERROR/TIMEOUT
Poirot-BitVector: ERROR/TIMEOUT
Cycles
SatAbs:
6.09sec (x2.47)

Satabs-prefix-first: 3.68sec
CBMC-WMM: 0.14sec
CBMC-SC: 0.04sec
CImpact: ERROR/TIMEOUT[8] 227.81sec
ESBMC: 0.05sec
Threader-monolithic: ERROR/TIMEOUT[1] 0.10sec
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.62sec (x2.69)

Satabs-prefix-first: 4.08sec
CBMC-WMM: 0.14sec
CBMC-SC: 0.06sec
CImpact: ERROR/TIMEOUT[8] 228.99sec
ESBMC: 0.05sec
Threader-monolithic: ERROR/TIMEOUT[1] 0.08sec
Threader-owicki-gries: ERROR/TIMEOUT[1] 0.08sec
Threader-rely-guarantee: ERROR/TIMEOUT[1] 0.09sec
Poirot-Integer: ERROR/TIMEOUT
Poirot-BitVector: ERROR/TIMEOUT
Cycles
SatAbs:
3.26sec (x1.32)

Satabs-prefix-first: 6.85sec
CBMC-WMM: 0.12sec
CBMC-SC: 34.12sec
CImpact: 0.01sec
ESBMC: 0.07sec
Threader-monolithic: ERROR/TIMEOUT[130] 897.29sec
Threader-owicki-gries: ERROR/TIMEOUT[130] 897.70sec
Threader-rely-guarantee: ERROR/TIMEOUT[130] 897.55sec
Poirot-Integer: ERROR/TIMEOUT
Poirot-BitVector: ERROR/TIMEOUT
Cycles
SatAbs:
2.65sec (x1.07)

Satabs-prefix-first: 4.49sec
CBMC-WMM: 0.11sec
CBMC-SC: 29.46sec
CImpact: 0.01sec
ESBMC: 0.09sec
Threader-monolithic: ERROR/TIMEOUT[130] 897.43sec
Threader-owicki-gries: ERROR/TIMEOUT[130] 897.53sec
Threader-rely-guarantee: ERROR/TIMEOUT[130] 897.36sec
Poirot-Integer: ERROR/TIMEOUT
Poirot-BitVector: ERROR/TIMEOUT
Cycles
SatAbs:
2.95sec (x1.19)

Satabs-prefix-first: 4.59sec
CBMC-WMM: 0.11sec
CBMC-SC: 30.51sec
CImpact: 0.01sec
ESBMC: 0.07sec
Threader-monolithic: ERROR/TIMEOUT[130] 897.20sec
Threader-owicki-gries: ERROR/TIMEOUT[130] 897.34sec
Threader-rely-guarantee: ERROR/TIMEOUT[130] 897.35sec
Poirot-Integer: ERROR/TIMEOUT
Poirot-BitVector: ERROR/TIMEOUT