Nitpicking C++ concurrency

Jasmin Christian Blanchette; Tjark Weber; Mark Batty; Scott Owens; Susmit Sarkar

doi:10.1145/2003476.2003493

Nitpicking C++ concurrency

Jasmin Christian Blanchette^*, Tjark Weber, Mark Batty, Scott Owens, Susmit Sarkar

^*Corresponding author for this work

School of Computer Science

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution

31 Citations (Scopus)

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.

Original language	English
Title of host publication	PPDP'11 - Proceedings of the 2011 Symposium on Principles and Practices of Declarative Programming
Pages	113-123
Number of pages	11
DOIs	https://doi.org/10.1145/2003476.2003493
Publication status	Published - 2011
Event	13th International ACM SIGPLAN Symposium on Principles and Practice of Declarative Programming, PPDP 2011 - Odense, Denmark Duration: 20 Jul 2011 → 22 Jul 2011

Publication series

Name	PPDP'11 - Proceedings of the 2011 Symposium on Principles and Practices of Declarative Programming

Conference

Conference	13th International ACM SIGPLAN Symposium on Principles and Practice of Declarative Programming, PPDP 2011
Country/Territory	Denmark
City	Odense
Period	20/07/11 → 22/07/11

Keywords

C++ memory model
Concurrency
Higher-order logic
Isabelle/HOL
Kodkod
Model finding
Nitpick
SAT solving

Access to Document

10.1145/2003476.2003493

Cite this

@inproceedings{6967c38035e7421eab36cf4560e5e7d0,

title = "Nitpicking C++ concurrency",

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.",

keywords = "C++ memory model, Concurrency, Higher-order logic, Isabelle/HOL, Kodkod, Model finding, Nitpick, SAT solving",

author = "Blanchette, {Jasmin Christian} and Tjark Weber and Mark Batty and Scott Owens and Susmit Sarkar",

year = "2011",

doi = "10.1145/2003476.2003493",

language = "English",

isbn = "9781450307765",

series = "PPDP'11 - Proceedings of the 2011 Symposium on Principles and Practices of Declarative Programming",

pages = "113--123",

booktitle = "PPDP'11 - Proceedings of the 2011 Symposium on Principles and Practices of Declarative Programming",

note = "13th International ACM SIGPLAN Symposium on Principles and Practice of Declarative Programming, PPDP 2011 ; Conference date: 20-07-2011 Through 22-07-2011",

}

Blanchette, JC, Weber, T, Batty, M, Owens, S & Sarkar, S 2011, Nitpicking C++ concurrency. in PPDP'11 - Proceedings of the 2011 Symposium on Principles and Practices of Declarative Programming. PPDP'11 - Proceedings of the 2011 Symposium on Principles and Practices of Declarative Programming, pp. 113-123, 13th International ACM SIGPLAN Symposium on Principles and Practice of Declarative Programming, PPDP 2011, Odense, Denmark, 20/07/11. https://doi.org/10.1145/2003476.2003493

Nitpicking C++ concurrency. / Blanchette, Jasmin Christian; Weber, Tjark; Batty, Mark et al.
PPDP'11 - Proceedings of the 2011 Symposium on Principles and Practices of Declarative Programming. 2011. p. 113-123 (PPDP'11 - Proceedings of the 2011 Symposium on Principles and Practices of Declarative Programming).

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution

TY - GEN

T1 - Nitpicking C++ concurrency

AU - Blanchette, Jasmin Christian

AU - Weber, Tjark

AU - Batty, Mark

AU - Owens, Scott

AU - Sarkar, Susmit

PY - 2011

Y1 - 2011

N2 - 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.

AB - 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.

KW - C++ memory model

KW - Concurrency

KW - Higher-order logic

KW - Isabelle/HOL

KW - Kodkod

KW - Model finding

KW - Nitpick

KW - SAT solving

UR - http://www.scopus.com/inward/record.url?scp=80052137438&partnerID=8YFLogxK

U2 - 10.1145/2003476.2003493

DO - 10.1145/2003476.2003493

M3 - Conference contribution

AN - SCOPUS:80052137438

SN - 9781450307765

T3 - PPDP'11 - Proceedings of the 2011 Symposium on Principles and Practices of Declarative Programming

SP - 113

EP - 123

BT - PPDP'11 - Proceedings of the 2011 Symposium on Principles and Practices of Declarative Programming

T2 - 13th International ACM SIGPLAN Symposium on Principles and Practice of Declarative Programming, PPDP 2011

Y2 - 20 July 2011 through 22 July 2011

ER -

Nitpicking C++ concurrency

Abstract

Publication series

Conference

Keywords

Access to Document

Other files and links

Fingerprint

Cite this