Jasmin Christian Blanchette, Tjark Weber, Mark Batty, Scott Owens, and Susmit Sarkar. In Peter Schneider-Kamp and Michael Hanus, editors, Proceedings of the 13th International ACM SIGPLAN Conference on Principles and Practice of Declarative Programming, July 20-22, 2011, Odense, Denmark, pages 113-124. ACM, 2011.
Previous work formalized the C++ memory model in Isabelle/HOL in an effort to clarify the proposed standard's semantics. Here we employ the model finder Nitpick to check litmus test programs that exercise the memory model, including a simple locking algorithm. Nitpick is built on Kodkod (Alloy's backend) but understands Isabelle's richer logic; hence it can be applied directly to the C++ memory model. We only need to give it a few hints, and thanks to the underlying SAT solver it scales much better than the CPPMEM explicit-state model checker. This case study inspired optimizations in Nitpick from which other formalizations can now benefit.
@inproceedings{blanchette11nitpicking,
author = {Jasmin Christian Blanchette and Tjark Weber and Mark Batty and Scott Owens and Susmit Sarkar},
title = {Nitpicking {C++} Concurrency},
editor = {Peter Schneider-Kamp and Michael Hanus},
booktitle = {Proceedings of the 13th International ACM SIGPLAN Conference on Principles and Practice of Declarative Programming, July~20-22, 2011, Odense, Denmark},
pages = {113--124},
publisher = {ACM},
url = {http://doi.acm.org/10.1145/2003476.2003493},
year = {2011}
}