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 Conference on Principles and Practice of Declarative Programming, 20-22 Jul 2011, Odense, Denmark. (doi:https://doi.org/10.1145/2003476.2003493) (Full text available)

PDF - Author's Accepted Manuscript
Download (388kB) Preview
[img]
Preview
Official URL
http://doi.acm.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: Conference or workshop item (Paper)
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: 11 Oct 2018 09:37 UTC
Resource URI: https://kar.kent.ac.uk/id/eprint/50260 (The current URI for this page, for reference purposes)
  • Depositors only (login required):

Downloads

Downloads per month over past year