Skip to main content
Kent Academic Repository

Nitpicking C++ concurrency

Blanchette, Jasmin Christian and Weber, Tjark and Batty, Mark and Owens, Scott and Sarkar, Susmit (2011) Nitpicking C++ concurrency. In: Proceedings of the 13th international ACM SIGPLAN symposium on Principles and practices of declarative programming. ACM, New York, USA, pp. 113-124. ISBN 978-1-4503-0776-5. (doi:10.1145/2003476.2003493) (KAR id:50260)


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.

Item Type: Book section
DOI/Identification number: 10.1145/2003476.2003493
Uncontrolled keywords: software engineering; general programming languages; theory of computation; logic
Subjects: Q Science > QA Mathematics (inc Computing science) > QA 75 Electronic computers. Computer science
Divisions: Divisions > Division of Computing, Engineering and Mathematical Sciences > School of Computing
Depositing User: Mark Batty
Date Deposited: 03 Nov 2015 08:27 UTC
Last Modified: 16 Nov 2021 10:20 UTC
Resource URI: (The current URI for this page, for reference purposes)

University of Kent Author Information

  • Depositors only (login required):

Total unique views for this document in KAR since July 2020. For more details click on the image.