Borrowed C Programs

This family contains the bug found by Sebastian Burckhart and Madan Musuvathi with their Sober tool, presented in their CAV 2008 paper, and our own fix for it.

It should answer Yes in litmus terms, or Verification Failed in verification terms, starting from x86/TSO. Its fixed version should answer No in litmus terms, or Verification Successful in verification terms, regardless of the model.

All tools successfully check the code and its fix for SC, as expected. SatAbs fails to verify the buggy code on all models, as expected, and verifies its fix on all models, as expected. CImpact times out on every model for both the initial buggy code and its fix. ESBMC claims to verify the buggy code on all models, and successfully verifies its fix on all models. Threader aborts on both the initial code and its fix for all models (more precisely, the error message is "Fatal error: exception Failure("Error: nesting atomic blocks!")).

Name

SC

TSO (all delay/cyc)

TSO (1 delay/cyc)

Expected (TSO)

PSO (all delay/cyc)

PSO (1 delay/cyc)

Expected (PSO)

RMO (all delay/cyc)

RMO (1 delay/cyc)

Expected (RMO)

Power (all delay/cyc)

Power (1 delay/cyc)

Expected (Power)