Nitpicking C plus plus Concurrency

被引：0

作者：

Blanchette, Jasmin Christian ^{[1
]}

Weber, Tjark ^{[1
]}

Batty, Mark ^{[1
]}

Owens, Scott ^{[1
]}

Sarkar, Susmit ^{[1
]}

机构：

[1] Tech Univ Munich, Munich, Germany

来源：

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

关键词：

C plus plus memory model; concurrency; model finding; SAT solving; higher-order logic; Isabelle/HOL; Nitpick; Kodkod; !text type='JAVA']JAVA[!/text] MEMORY MODEL;

D O I：

暂无

中图分类号：

TP31 [计算机软件];

学科分类号：

081202 ; 0835 ;

摘要：

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.

引用

页码：113 / 123

页数：11

共 50 条

[1] Mathematizing C plus plus Concurrency
Batty, Mark
Owens, Scott
Sarkar, Susmit
Sewell, Peter
Weber, Tjark
ACM SIGPLAN NOTICES, 2011, 46 (01) : 55 - 66
[2] Mathematizing C plus plus Concurrency
Batty, Mark
Owens, Scott
Sarkar, Susmit
Sewell, Peter
Weber, Tjark
POPL 11: PROCEEDINGS OF THE 38TH ANNUAL ACM SIGPLAN-SIGACT SYMPOSIUM ON PRINCIPLES OF PROGRAMMING LANGUAGES, 2011, : 55 - 66
[3] Foundations of the C plus plus Concurrency Memory Model
Boehm, Hans-J.
Adve, Sarita V.
PLDI'08: PROCEEDINGS OF THE 2008 SIGPLAN CONFERENCE ON PROGRAMMING LANGUAGE DESIGN & IMPLEMENTATION, 2008, : 68 - 78
[4] An empirical study on C plus plus concurrency constructs
Wu, Di
Chen, Lin
Zhou, Yuming
Xu, Baowen
2015 ACM/IEEE INTERNATIONAL SYMPOSIUM ON EMPIRICAL SOFTWARE ENGINEERING AND MEASUREMENT (ESEM), 2015, : 257 - 266
[5] An extensive empirical study on C plus plus concurrency constructs
Wu, Di
Chen, Lin
Zhou, Yuming
Xu, Baowen
INFORMATION AND SOFTWARE TECHNOLOGY, 2016, 76 : 1 - 18
[6] The Cilk plus plus Concurrency Platform
Leiserson, Charles E.
DAC: 2009 46TH ACM/IEEE DESIGN AUTOMATION CONFERENCE, VOLS 1 AND 2, 2009, : 522 - 527
[7] The Cilk plus plus concurrency platform
Leiserson, Charles E.
JOURNAL OF SUPERCOMPUTING, 2010, 51 (03): : 244 - 257
[8] CCmutator: A Mutation Generator for Concurrency Constructs in Multithreaded C/C plus plus Applications
Kusano, Markus
Wang, Chao
2013 28TH IEEE/ACM INTERNATIONAL CONFERENCE ON AUTOMATED SOFTWARE ENGINEERING (ASE), 2013, : 722 - 725
[9] Clarifying and Compiling C/C plus plus Concurrency: from C++11 to POWER
Batty, Mark
Memarian, Kayvan
Owens, Scott
Sarkar, Susmit
Sewell, Peter
POPL 12: PROCEEDINGS OF THE 39TH ANNUAL ACM SIGPLAN-SIGACT SYMPOSIUM ON PRINCIPLES OF PROGRAMMING LANGUAGES, 2012, : 509 - 520
[10] ARITHMETIC PLUS LOGIC PLUS GEOMETRY = CONCURRENCY
PRATT, V
LECTURE NOTES IN COMPUTER SCIENCE, 1992, 583 : 430 - 447

← 1 2 3 4 5 →