Nitpicking C plus plus Concurrency

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

Nitpicking C plus plus 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	PPDP 11 - PROCEEDINGS OF THE 2011 SYMPOSIUM ON PRINCIPLES AND PRACTICES OF DECLARATIVE PROGRAMMING
Place of Publication	NEW YORK
Publisher	ACM
Pages	113-123
Number of pages	11
ISBN (Print)	978-1-4503-0776-5
Publication status	Published - 2011
Event	13th International ACM SIGPLAN Symposium on Principles and Practice of Declarative Programming - Odense, Denmark Duration: 20 Jul 2011 → 22 Jul 2011

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

Cite this

@inproceedings{2c735c225c954a8daa53ce608f097569,

title = "Nitpicking C plus plus 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",

year = "2011",

language = "English",

isbn = "978-1-4503-0776-5",

pages = "113--123",

booktitle = "PPDP 11 - PROCEEDINGS OF THE 2011 SYMPOSIUM ON PRINCIPLES AND PRACTICES OF DECLARATIVE PROGRAMMING",

publisher = "ACM",

address = "United States",

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

}

TY - GEN

T1 - Nitpicking C plus plus 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 - 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

M3 - Conference contribution

SN - 978-1-4503-0776-5

SP - 113

EP - 123

BT - PPDP 11 - PROCEEDINGS OF THE 2011 SYMPOSIUM ON PRINCIPLES AND PRACTICES OF DECLARATIVE PROGRAMMING

PB - ACM

CY - NEW YORK

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

Y2 - 20 July 2011 through 22 July 2011

ER -

Nitpicking C plus plus Concurrency

Abstract

Conference

Keywords

Fingerprint

Cite this