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 条
  • [31] C plus plus constructors - Response
    Meyers, S
    DR DOBBS JOURNAL, 1997, 22 (08): : 12 - 12
  • [32] Programming with C plus plus concepts
    Jaervi, Jaakko
    Marcus, Mat
    Smith, Jacob N.
    SCIENCE OF COMPUTER PROGRAMMING, 2010, 75 (07) : 596 - 614
  • [33] C plus plus standards - Response
    Stevens, A
    DR DOBBS JOURNAL, 1997, 22 (11): : 12 - 12
  • [34] A C plus plus integrator class
    Conway, DJ
    DR DOBBS JOURNAL, 1995, 20 (12): : 52 - +
  • [35] Optimizations in C plus plus Compilers
    Godbolt, Matt
    COMMUNICATIONS OF THE ACM, 2020, 63 (02) : 41 - 49
  • [36] C/C plus plus Thread Safety Analysis
    Hutchins, DeLesley
    Ballman, Aaron
    Sutherland, Dean
    2014 14TH IEEE INTERNATIONAL WORKING CONFERENCE ON SOURCE CODE ANALYSIS AND MANIPULATION (SCAM 2014), 2014, : 41 - 46
  • [37] Bridging Excel and C/C plus plus Code
    Punuru, Janardhana R.
    Knopf, F. Carl
    COMPUTER APPLICATIONS IN ENGINEERING EDUCATION, 2008, 16 (04) : 289 - 304
  • [38] C plus plus Web Framework: A Web Framework for Web Development using C plus plus and Qt
    Lima, Herik
    Eler, Marcelo Medeiros
    ICEIS: PROCEEDINGS OF THE 23RD INTERNATIONAL CONFERENCE ON ENTERPRISE INFORMATION SYSTEMS - VOL 2, 2021, : 76 - 87
  • [39] Clacc: OpenACC for C/C plus plus in Clang
    Denny, Joel E.
    Lee, Seyong
    Valero-Lara, Pedro
    Gonzalez-Tallada, Marc
    Teranishi, Keita
    Vetter, Jeffrey S.
    INTERNATIONAL JOURNAL OF HIGH PERFORMANCE COMPUTING APPLICATIONS, 2024, 38 (05): : 427 - 446
  • [40] Precise measurement of the branching fractions of J/ψ→<overline>Λπ plus Σ- plus c.c. and J/ψ→<overline>Λπ-Σ plus plus c.c
    Ablikim, M.
    Achasov, M. N.
    Adlarson, P.
    Aliberti, R.
    Amoroso, A.
    An, M. R.
    An, Q.
    Bai, Y.
    Bakina, O.
    Balossino, I.
    Ban, Y.
    Batozskaya, V.
    Begzsuren, K.
    Berger, N.
    Berlowski, M.
    Bertani, M.
    Bettoni, D.
    Bianchi, F.
    Bianco, E.
    Bloms, J.
    Bortone, A.
    Boyko, I.
    Briere, R. A.
    Brueggemann, A.
    Cai, H.
    Cai, X.
    Calcaterra, A.
    Cao, G. F.
    Cao, N.
    Cetin, S. A.
    Chang, J. F.
    Chang, T. T.
    Chang, W. L.
    Che, G. R.
    Chelkov, G.
    Chen, C.
    Chen, Chao
    Chen, G.
    Chen, H. S.
    Chen, M. L.
    Chen, S. J.
    Chen, S. M.
    Chen, T.
    Chen, X. R.
    Chen, X. T.
    Chen, Y. B.
    Chen, Y. Q.
    Chen, Z. J.
    Cheng, W. S.
    Choi, S. K.
    PHYSICAL REVIEW D, 2023, 108 (11)
12345