How to read the tables?
Meaning of the model-checker's resultsModel-checker on the instrumented program | Observed state in Litmus | Picture |
VERIFICATION FAILED | YES | ![]() |
VERIFICATION SUCCESSFUL | NO | ![]() |
Reading the results in the experiments tables
The table below is an excerpt of former results we obtained for x86/podwr experiments.
- In the first column, we can read the name of the original Litmus test (with a link to the file), and the expected violation cycle. The second column gathers the results of the model-checkers for SC. As we are interested in WMM bugs, the verification for SC should be
.
- The three next columns concern TSO model. The last column tells which result we should get for this program under TSO, namely
. We see in the third column that Satabs indeed finds the correct result when checking the instrumented program. ESBMC in this example is missing the counterexample. Threader is either returning an error, or killed by timeout (here, it is an error).
- Note that there are two columns for TSO results: in the first one, we instrument all the delays; in the second one, we instrument only one delay per cycle.
- We also experiment under PSO, RMO and Power, and with additional model-checkers: additional columns of results (and expected results) appear after TSO's columns.
Name | SC | TSO (all delay/cyc) | TSO (1 delay/cyc) | Expected (TSO) | ... |
x86/podwr000 Fre PodWR Fre PodWR |
SatAbs: ![]() 0.60sec ESBMC: ![]() Threader: ![]() ... |
Cycles SatAbs: ![]() 3.94sec (x6.56) ESBMC: ![]() Threader: ERROR/TIMEOUT[1] 491.99sec ... |
Cycles SatAbs: ![]() 2.43sec (x4.05) ESBMC: ![]() Threader: ERROR/TIMEOUT[1] 182.60sec ... |
![]() |
... |
Standard C programs
This family consists of Dekker, Szymanski, Lamport, Peterson's mutual exclusion algorithms, and Lamport's bakery algorithm.
They should answer Yes in litmus terms, or Verification Failed in verification terms, starting from x86/TSO.
All tools successfully check these programs on SC, as expected. SatAbs fails to verify their instrumented versions for every model, as expected (except in the cases where it times out). The other tools either wrongly claim to have verify it, or timeout.
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) |
gb_dekker.c |
SatAbs: ![]() 0.23sec Satabs-prefix-first: ![]() CBMC-WMM: ![]() CBMC-SC: ![]() C code |
Cycles
SatAbs: ![]() 2.27sec (x9.86) Satabs-prefix-first: ![]() CBMC-WMM: ![]() CBMC-SC: ![]() Instrumented C code |
Cycles
SatAbs: ![]() 2.31sec (x10.04) Satabs-prefix-first: ![]() CBMC-WMM: ![]() CBMC-SC: ![]() Instrumented C code |
Cycles
SatAbs: ![]() 1.63sec (x7.08) Satabs-prefix-first: ![]() CBMC-WMM: ![]() CBMC-SC: ![]() Instrumented C code |
Cycles
SatAbs: ![]() 1.68sec (x7.30) Satabs-prefix-first: ![]() CBMC-WMM: ![]() CBMC-SC: ![]() Instrumented C code |
UNKNOWN |
Cycles
SatAbs: ![]() 18.57sec (x80.73) Satabs-prefix-first: ![]() CBMC-WMM: ![]() CBMC-SC: ![]() Instrumented C code |
Cycles
SatAbs: ![]() 18.54sec (x80.60) Satabs-prefix-first: ![]() CBMC-WMM: ![]() CBMC-SC: ![]() Instrumented C code |
Cycles
SatAbs: ![]() 17.83sec (x77.52) Satabs-prefix-first: ![]() CBMC-WMM: ![]() CBMC-SC: ![]() Instrumented C code |
UNKNOWN |
Cycles
SatAbs: ![]() 16.71sec (x72.65) Satabs-prefix-first: ![]() CBMC-WMM: ![]() CBMC-SC: ![]() Instrumented C code |
Cycles
SatAbs: ![]() 8.44sec (x36.69) Satabs-prefix-first: ![]() CBMC-WMM: ![]() CBMC-SC: ![]() Instrumented C code |
Cycles
SatAbs: ![]() 1.48sec (x6.43) Satabs-prefix-first: ![]() CBMC-WMM: ![]() CBMC-SC: ![]() Instrumented C code |
UNKNOWN |
Cycles
SatAbs: ![]() 3.38sec (x14.69) Satabs-prefix-first: ![]() CBMC-WMM: ![]() CBMC-SC: ![]() Instrumented C code |
Cycles
SatAbs: ![]() 8.04sec (x34.95) Satabs-prefix-first: ![]() CBMC-WMM: ![]() CBMC-SC: ![]() Instrumented C code |
Cycles
SatAbs: ![]() 4.32sec (x18.78) Satabs-prefix-first: ![]() CBMC-WMM: ![]() CBMC-SC: ![]() Instrumented C code |
UNKNOWN |
gb_lamport.c |
SatAbs: ![]() 0.62sec Satabs-prefix-first: ![]() CBMC-WMM: ![]() CBMC-SC: ![]() C code |
Cycles
SatAbs: ![]() 7.27sec (x11.72) Satabs-prefix-first: ![]() CBMC-WMM: ![]() CBMC-SC: ERROR/TIMEOUT[130] 0.01sec Instrumented C code |
Cycles
SatAbs: ![]() 5.38sec (x8.67) Satabs-prefix-first: ![]() CBMC-WMM: ![]() CBMC-SC: ERROR/TIMEOUT[130] 0.01sec Instrumented C code |
Cycles
SatAbs: ![]() 16.00sec (x25.80) Satabs-prefix-first: ![]() CBMC-WMM: ![]() CBMC-SC: ERROR/TIMEOUT[130] 0.01sec Instrumented C code |
Cycles
SatAbs: ![]() 11.52sec (x18.58) Satabs-prefix-first: ![]() CBMC-WMM: ![]() CBMC-SC: ERROR/TIMEOUT[130] 0.01sec Instrumented C code |
UNKNOWN |
Cycles
SatAbs: ![]() 6.56sec (x10.58) Satabs-prefix-first: ![]() CBMC-WMM: ![]() CBMC-SC: ERROR/TIMEOUT[130] 0.01sec Instrumented C code |
Cycles
SatAbs: ![]() 6.59sec (x10.62) Satabs-prefix-first: ![]() CBMC-WMM: ![]() CBMC-SC: ERROR/TIMEOUT[130] 0.01sec Instrumented C code |
Cycles
SatAbs: ![]() 30.51sec (x49.20) Satabs-prefix-first: ![]() CBMC-WMM: ![]() CBMC-SC: ERROR/TIMEOUT[130] 0.01sec Instrumented C code |
UNKNOWN |
Cycles
SatAbs: ![]() 5.73sec (x9.24) Satabs-prefix-first: ![]() CBMC-WMM: ![]() CBMC-SC: ERROR/TIMEOUT[130] 0.01sec Instrumented C code |
Cycles
SatAbs: ![]() 5.47sec (x8.82) Satabs-prefix-first: ![]() CBMC-WMM: ![]() CBMC-SC: ERROR/TIMEOUT[130] 0.01sec Instrumented C code |
Cycles
SatAbs: ![]() 12.21sec (x19.69) Satabs-prefix-first: ![]() CBMC-WMM: ![]() CBMC-SC: ERROR/TIMEOUT[130] 0.01sec Instrumented C code |
UNKNOWN |
Cycles
SatAbs: ![]() 8.07sec (x13.01) Satabs-prefix-first: ![]() CBMC-WMM: ![]() CBMC-SC: ERROR/TIMEOUT[130] 0.00sec Instrumented C code |
Cycles
SatAbs: ![]() 5.89sec (x9.50) Satabs-prefix-first: ![]() CBMC-WMM: ![]() CBMC-SC: ERROR/TIMEOUT[130] 0.01sec Instrumented C code |
Cycles
SatAbs: ![]() 5.19sec (x8.37) Satabs-prefix-first: ![]() CBMC-WMM: ![]() CBMC-SC: ERROR/TIMEOUT[130] 0.01sec Instrumented C code |
UNKNOWN |
gb_peterson.c |
SatAbs: ![]() 0.21sec Satabs-prefix-first: ![]() CBMC-WMM: ![]() CBMC-SC: ![]() C code |
Cycles
SatAbs: ![]() 1.05sec (x5.00) Satabs-prefix-first: ![]() CBMC-WMM: ![]() CBMC-SC: ![]() Instrumented C code |
Cycles
SatAbs: ![]() 1.30sec (x6.19) Satabs-prefix-first: ![]() CBMC-WMM: ![]() CBMC-SC: ![]() Instrumented C code |
Cycles
SatAbs: ![]() 0.77sec (x3.66) Satabs-prefix-first: ![]() CBMC-WMM: ![]() CBMC-SC: ![]() Instrumented C code |
Cycles
SatAbs: ![]() 0.92sec (x4.38) Satabs-prefix-first: ![]() CBMC-WMM: ![]() CBMC-SC: ![]() Instrumented C code |
UNKNOWN |
Cycles
SatAbs: ![]() 1.61sec (x7.66) Satabs-prefix-first: ![]() CBMC-WMM: ![]() CBMC-SC: ![]() Instrumented C code |
Cycles
SatAbs: ![]() 1.36sec (x6.47) Satabs-prefix-first: ![]() CBMC-WMM: ![]() CBMC-SC: ![]() Instrumented C code |
Cycles
SatAbs: ![]() 0.96sec (x4.57) Satabs-prefix-first: ![]() CBMC-WMM: ![]() CBMC-SC: ![]() Instrumented C code |
UNKNOWN |
Cycles
SatAbs: ![]() 1.70sec (x8.09) Satabs-prefix-first: ![]() CBMC-WMM: ![]() CBMC-SC: ![]() Instrumented C code |
Cycles
SatAbs: ![]() 24.74sec (x117.80) Satabs-prefix-first: ![]() CBMC-WMM: ![]() CBMC-SC: ![]() Instrumented C code |
Cycles
SatAbs: ![]() 4.72sec (x22.47) Satabs-prefix-first: ![]() CBMC-WMM: ![]() CBMC-SC: ![]() Instrumented C code |
UNKNOWN |
Cycles
SatAbs: ![]() 1.41sec (x6.71) Satabs-prefix-first: ![]() CBMC-WMM: ![]() CBMC-SC: ![]() Instrumented C code |
Cycles
SatAbs: ![]() 16.89sec (x80.42) Satabs-prefix-first: ![]() CBMC-WMM: ![]() CBMC-SC: ![]() Instrumented C code |
Cycles
SatAbs: ![]() 0.36sec (x1.71) Satabs-prefix-first: ![]() CBMC-WMM: ![]() CBMC-SC: ![]() Instrumented C code |
UNKNOWN |
gb_szymanski.c |
SatAbs: ![]() 0.28sec Satabs-prefix-first: ![]() CBMC-WMM: ![]() CBMC-SC: ![]() C code |
Cycles
SatAbs: ![]() 0.31sec (x1.10) Satabs-prefix-first: ![]() CBMC-WMM: ![]() CBMC-SC: ERROR/TIMEOUT[130] 0.01sec Instrumented C code |
Cycles
SatAbs: ![]() 0.10sec (x.35) Satabs-prefix-first: ![]() CBMC-WMM: ![]() CBMC-SC: ERROR/TIMEOUT[130] 0.01sec Instrumented C code |
Cycles
SatAbs: ![]() 3.57sec (x12.75) Satabs-prefix-first: ![]() CBMC-WMM: ![]() CBMC-SC: ERROR/TIMEOUT[130] 0.01sec Instrumented C code |
Cycles
SatAbs: ![]() 0.26sec (x.92) Satabs-prefix-first: ![]() CBMC-WMM: ![]() CBMC-SC: ERROR/TIMEOUT[130] 0.01sec Instrumented C code |
UNKNOWN |
Cycles
SatAbs: ![]() 0.20sec (x.71) Satabs-prefix-first: ![]() CBMC-WMM: ![]() CBMC-SC: ERROR/TIMEOUT[130] 0.01sec Instrumented C code |
Cycles
SatAbs: ![]() 0.12sec (x.42) Satabs-prefix-first: ![]() CBMC-WMM: ![]() CBMC-SC: ERROR/TIMEOUT[130] 0.01sec Instrumented C code |
Cycles
SatAbs: ![]() 0.16sec (x.57) Satabs-prefix-first: ![]() CBMC-WMM: ![]() CBMC-SC: ERROR/TIMEOUT[130] 0.01sec Instrumented C code |
UNKNOWN |
Cycles
SatAbs: ![]() 0.22sec (x.78) Satabs-prefix-first: ![]() CBMC-WMM: ![]() CBMC-SC: ERROR/TIMEOUT[0] 20.47sec Instrumented C code |
Cycles
SatAbs: ![]() 1.18sec (x4.21) Satabs-prefix-first: ![]() CBMC-WMM: ![]() CBMC-SC: ERROR/TIMEOUT[0] 59.37sec Instrumented C code |
Cycles
SatAbs: ![]() 0.18sec (x.64) Satabs-prefix-first: ![]() CBMC-WMM: ![]() CBMC-SC: ERROR/TIMEOUT[0] 19.87sec Instrumented C code |
UNKNOWN |
Cycles
SatAbs: ![]() 0.26sec (x.92) Satabs-prefix-first: ![]() CBMC-WMM: ![]() CBMC-SC: ERROR/TIMEOUT[0] 24.11sec Instrumented C code |
Cycles
SatAbs: ![]() 1.01sec (x3.60) Satabs-prefix-first: ![]() CBMC-WMM: ![]() CBMC-SC: ERROR/TIMEOUT[0] 31.89sec Instrumented C code |
Cycles
SatAbs: ![]() 30.44sec (x108.71) Satabs-prefix-first: ERROR/TIMEOUT[130] CBMC-WMM: ![]() CBMC-SC: ERROR/TIMEOUT[0] 18.34sec Instrumented C code |
UNKNOWN |