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

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	Proceedings of the 2011 Symposium on Prinicples and Practices of Declarative Programming (PDP'11)
Place of Publication	New York, NY
Publisher	ACM
Pages	113-123
Number of pages	11
ISBN (Print)	9781450307765
DOIs	https://doi.org/10.1145/2003476.2003493
Publication status	Published - 20 Jul 2011
Event	13th International ACM SIGPLAN Symposium on Principles and Practice of Declarative Programming - 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
Country/Territory	Denmark
City	Odense
Period	20/07/11 → 22/07/11

Keywords

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

Access to Document

10.1145/2003476.2003493

Cite this

@inproceedings{2c735c225c954a8daa53ce608f097569,

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 = "SAT solving, JAVA memory model, Isabelle/HOL, Higher-order logic, Concurrency, C plus plus memory model, Nitpick, Kodkod, Model finding",

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

note = "Funding: The authors acknowledge funding from the Deutsche Forschungsgemeinschaft (grant Ni 491/11-2) and the British EPSRC (grants EP/F036345, EP/F067909, EP/H005633, EP/H027351).; 13th International ACM SIGPLAN Symposium on Principles and Practice of Declarative Programming ; Conference date: 20-07-2011 Through 22-07-2011",

year = "2011",

month = jul,

day = "20",

doi = "10.1145/2003476.2003493",

language = "English",

isbn = "9781450307765",

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

publisher = "ACM",

pages = "113--123",

booktitle = "Proceedings of the 2011 Symposium on Prinicples and Practices of Declarative Programming (PDP'11)",

address = "United States",

}

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

Nitpicking C++ concurrency. / Blanchette, Jasmin Christian; Weber, Tjark; Batty, Mark et al.
Proceedings of the 2011 Symposium on Prinicples and Practices of Declarative Programming (PDP'11). New York, NY: ACM, 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

N1 - Funding: The authors acknowledge funding from the Deutsche Forschungsgemeinschaft (grant Ni 491/11-2) and the British EPSRC (grants EP/F036345, EP/F067909, EP/H005633, EP/H027351).

PY - 2011/7/20

Y1 - 2011/7/20

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 - SAT solving

KW - JAVA memory model

KW - Isabelle/HOL

KW - Higher-order logic

KW - Concurrency

KW - C plus plus memory model

KW - Nitpick

KW - Kodkod

KW - Model finding

UR - https://dl.acm.org/doi/proceedings/10.1145/2003476

U2 - 10.1145/2003476.2003493

DO - 10.1145/2003476.2003493

M3 - Conference contribution

SN - 9781450307765

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

SP - 113

EP - 123

BT - Proceedings of the 2011 Symposium on Prinicples and Practices of Declarative Programming (PDP'11)

PB - ACM

CY - New York, NY

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

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