Skip to main content

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)

PDF Author's Accepted Manuscript
Language: English
Download (258kB) Preview
[img]
Preview
Official URL
http://dx.doi.org/10.1145/2003476.2003493

Abstract

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: Faculties > Sciences > School of Computing > Programming Languages and Systems Group
Depositing User: Mark Batty
Date Deposited: 03 Nov 2015 08:27 UTC
Last Modified: 06 May 2020 03:12 UTC
Resource URI: https://kar.kent.ac.uk/id/eprint/50260 (The current URI for this page, for reference purposes)
Batty, Mark: https://orcid.org/0000-0001-7053-4364
Owens, Scott: https://orcid.org/0000-0002-7437-4780
  • Depositors only (login required):

Downloads

Downloads per month over past year