How to read the tables?

Meaning of the model-checker's results

Model-checker on the instrumented program	Observed state in Litmus	Picture
VERIFICATION FAILED	YES
VERIFICATION SUCCESSFUL	NO

Switch between Model-checker/Litmus outputs

Reading the results in the experiments tables
The table below is an excerpt of former results we obtained for x86/podwr experiments.

• In the first column, we can read the name of the original Litmus test (with a link to the file), and the expected violation cycle. The second column gathers the results of the model-checkers for SC. As we are interested in WMM bugs, the verification for SC should be .
• The three next columns concern TSO model. The last column tells which result we should get for this program under TSO, namely . We see in the third column that Satabs indeed finds the correct result when checking the instrumented program. ESBMC in this example is missing the counterexample. Threader is either returning an error, or killed by timeout (here, it is an error).
• Note that there are two columns for TSO results: in the first one, we instrument all the delays; in the second one, we instrument only one delay per cycle.
• We also experiment under PSO, RMO and Power, and with additional model-checkers: additional columns of results (and expected results) appear after TSO's columns.

Name	SC	TSO (all delay/cyc)	TSO (1 delay/cyc)	Expected (TSO)	...
x86/podwr000 Fre PodWR Fre PodWR	SatAbs: 0.60sec ESBMC: 0.30sec Threader: 7.92sec ...	Cycles SatAbs: 3.94sec (x6.56) ESBMC: 8.34sec Threader: ERROR/TIMEOUT[1] 491.99sec ...	Cycles SatAbs: 2.43sec (x4.05) ESBMC: 7.58sec Threader: ERROR/TIMEOUT[1] 182.60sec ...		...