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 条
  • [21] C plus plus constructors
    Plochan, F
    DR DOBBS JOURNAL, 1997, 22 (08): : 10 - +
  • [22] Synchronising C/C plus plus and POWER
    Sarkar, Susmit
    Memarian, Kayvan
    Owens, Scott
    Batty, Mark
    Sewell, Peter
    Maranget, Luc
    Alglave, Jade
    Williams, Derek
    ACM SIGPLAN NOTICES, 2012, 47 (06) : 311 - 321
  • [23] UPC plus plus : A PGAS Extension for C plus
    Zheng, Yili
    Kamil, Amir
    Driscoll, Michael B.
    Shan, Hongzhang
    Yelick, Katherine
    2014 IEEE 28TH INTERNATIONAL PARALLEL AND DISTRIBUTED PROCESSING SYMPOSIUM, 2014,
  • [24] ROC plus plus : Robust Optimization in C plus
    Vayanos, Phebe
    Jin, Qing
    Elissaios, George
    INFORMS JOURNAL ON COMPUTING, 2022, 34 (06) : 2873 - 2888
  • [25] Quantum plus plus : A modern C plus plus quantum computing library
    Gheorghiu, Vlad
    PLOS ONE, 2018, 13 (12):
  • [26] aflow plus plus : A C plus plus framework for autonomous materials design
    Oses, Corey
    Esters, Marco
    Hicks, David
    Divilov, Simon
    Eckert, Hagen
    Friedrich, Rico
    Mehl, Michael J.
    Smolyanyuk, Andriy
    Campilongo, Xiomara
    van de Walle, Axel
    Schroers, Jan
    Kusne, A. Gilad
    Takeuchi, Ichiro
    Zurek, Eva
    Nardelli, Marco Buongiorno
    Fornari, Marco
    Lederer, Yoav
    Levy, Ohad
    Toher, Cormac
    Curtarolo, Stefano
    COMPUTATIONAL MATERIALS SCIENCE, 2023, 217
  • [27] The magnetic spectrum of beta rays emitted by the ThB plus C plus C' plus C"
    Arnoult, R
    COMPTES RENDUS HEBDOMADAIRES DES SEANCES DE L ACADEMIE DES SCIENCES, 1934, 198 : 1603 - 1605
  • [28] The magnetic spectrum of beta rays emitted by AcB plus C plus C' plus C''
    Graf, T
    COMPTES RENDUS HEBDOMADAIRES DES SEANCES DE L ACADEMIE DES SCIENCES, 1933, 197 : 238 - 241
  • [29] The Pinocchio C plus plus library
    Carpentier, Justin
    Saurel, Guilhem
    Buondonno, Gabriele
    Mirabel, Joseph
    Lamiraux, Florent
    Stasse, Olivier
    Mansard, Nicolas
    2019 IEEE/SICE INTERNATIONAL SYMPOSIUM ON SYSTEM INTEGRATION (SII), 2019, : 614 - 619
  • [30] C plus plus constructors - Response
    Meyers, S
    DR DOBBS JOURNAL, 1997, 22 (08): : 12 - 12
12345