Mathematizing C++ Concurrency: The Post-Rapperswil Model

Mathematizing C++ Concurrency: The Post-Rapperswil Model
复制标题

C 并发数学化：后 Rapperswil 模型

DOI：
--
复制
发表时间：
2010
期刊：
影响因子：
--
通讯作者：
Tjark Weber
Tjark Weber
中科院分区：
--
文献类型：
--
作者：
Mark Batty;Scott Owens;Susmit Sarkar;Peter Sewell;Tjark Weber

文献摘要

被引文献

相似文献

在本文中，我们描述了一个严格的语义C++并发。据我们所知，这抓住了最终委员会草案（N3092）文本的意图，并在2010年7月的C++标准委员会拉佩斯维尔会议上进行了修改。我们讨论了导致这些变化的N3092文本的一些问题。为了使我们的语义在数学上精确和明确，我们在Isabelle/HOL证明助手中用机器形式化的数学表达它。为了便于理解，我们用一系列例子来介绍它，并给出定义的英语散文翻译和数学的打字版本，并排;应该可以单独阅读其中任何一个。为了能够探索语义的后果，我们开发了一个工具（CPPMEM），用于计算Litmus测试示例程序的允许执行（使用从Isabelle/HOL定义自动生成的检查代码，以获得高保证）。我们进一步验证的语义证明，提出的x86实现的并发原语是正确的x86-TSO内存模型。我们希望，这将有助于讨论任何进一步的变化，标准草案，提供一个明确的正确性条件的编译器，并提供了一个急需的基础，分析和验证并发C和C++程序。
In this paper we describe a rigorous semantics for C++ concurrency. To the best of our knowledge, this captures the intent of the Final Committee Draft (N3092) text, modified as discussed at the Rapperswil meeting of the C++ Standards Committee in July 2010. We discuss some issues with the N3092 text that led to those changes. To make our semantics mathematically precise and unambigous, we express it in machine-formalised mathematics, in the Isabelle/HOL proof assistant. To make it accessible, we introduce it with a series of examples, and give both an English-prose translation of the definitions and a typeset version of the mathematics, side-by-side; it should be possible to read either one in isolation. To make it possible to explore the consequences of the semantics, we have developed a tool (CPPMEM) that calculates the allowed executions of litmus-test example programs (using checking code automatically generated from our Isabelle/HOL definitions, for high assurance). We further validate the semantics by proving that a proposed x86 implementation of the concurrency primitives is correct with respect to the x86-TSO memory model. We hope that this will aid discussion of any further changes to the draft standard, provide an unambiguous correctness condition for compilers, and give a much-needed basis for analysis and verification of concurrent C and C++ programs.