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)