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 条

[41] Computational wave optics library for C plus plus: CWO plus plus library
Shimobaba, Tomoyoshi
Weng, Jiantong
Sakurai, Takahiro
Okada, Naohisa
Nishitsuji, Takashi
Takada, Naoki
Shiraki, Atsushi
Masuda, Nobuyuki
Ito, Tomoyoshi
COMPUTER PHYSICS COMMUNICATIONS, 2012, 183 (05) : 1124 - 1138
[42] Video plus plus , a Modern Image and Video Processing C plus plus Framework
Garrigues, Matthieu
Manzanera, Antoine
PROCEEDINGS OF THE 2014 CONFERENCE ON DESIGN AND ARCHITECTURES FOR SIGNAL AND IMAGE PROCESSING, 2014,
[43] Cosmo plus plus : An object-oriented C plus plus library for cosmology
Aslanyan, Grigor
COMPUTER PHYSICS COMMUNICATIONS, 2014, 185 (12) : 3215 - 3227
[44] CGP plus plus : A Modern C plus plus Implementation of Cartesian Genetic Programming
Kalkreuth, Roman
Back, Thomas
PROCEEDINGS OF THE 2024 GENETIC AND EVOLUTIONARY COMPUTATION CONFERENCE, GECCO 2024, 2024, : 13 - 22
[45] Infosel plus plus : Information Based Feature Selection C plus plus Library
Kachel, Adam
Biesiada, Jacek
Blachnik, Marcin
Duch, Wlodzislaw
ARTIFICIAL INTELLIGENCE AND SOFT COMPUTING, PT I, 2010, 6113 : 388 - +
[46] On hard gamma-rays from Ra (C plus C' plus C" plus D)
Nishida, S
PHYSICAL REVIEW, 1937, 51 (11): : 0996 - 0996
[47] Interactive C plus plus code development using C plus plus Explorer and GitHub classroom for educational purposes
Diehl, Patrick
Brandt, Steven R.
CONCURRENCY AND COMPUTATION-PRACTICE & EXPERIENCE, 2023, 35 (18):
[48] AATT plus : Effectively manifesting concurrency bugs in Android apps
Wang, Jue
Jiang, Yanyan
Xu, Chang
Li, Qiwei
Gu, Tianxiao
Ma, Jun
Ma, Xiaoxing
Lu, Jian
SCIENCE OF COMPUTER PROGRAMMING, 2018, 163 : 1 - 18
[49] NSC plus plus : Non-standard cosmologies in C plus
Karamitros, Dimitrios
COMPUTER PHYSICS COMMUNICATIONS, 2023, 288
[50] Genetic Optimisation of C plus plus Applications
Giavrimis, Rafail
Butler, Alexis
Petrescu, Constantin Cezar
Basios, Michail
Dash, Santanu Kumar
2021 36TH IEEE/ACM INTERNATIONAL CONFERENCE ON AUTOMATED SOFTWARE ENGINEERING ASE 2021, 2021, : 1180 - 1182

← 1 2 3 4 5 →