Programming Languages and Systems - 24th European Symposium on Programming, ESOP 2015, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2015, London, UK, April 11-18, 2015, Proceedings
Programming Languages and Systems - 24th European Symposium on Programming, ESOP 2015, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2015, London, UK, April 11-18, 2015, Proceedings
复制标题
编程语言和系统 - 第 24 届欧洲编程研讨会，ESOP 2015，作为欧洲软件理论与实践联合会议的一部分举行，ETAPS 2015，英国伦敦，2015 年 4 月 11-18 日，会议记录
DOI：
10.1007/978-3-662-46669-8_12
复制
发表时间：
2015
期刊：
影响因子：
--
通讯作者：
Batty M
中科院分区：
文献类型：
--
作者：
Batty M
尽管经过了数十年的研究，我们仍然没有为任何旨在支持并发系统代码的通用编程语言提供令人满意的并发语义。 Java 内存模型已被证明在标准编译器优化方面不健全，而 C/C++11 模型太弱，会出现不良的凭空执行。本文的目标是尽可能清楚地阐明这一主要的开放问题，展示它是如何从多处理器宽松内存行为和适应当前编译器优化的愿望的组合中产生的。我们做出了几个新颖的贡献，每个贡献都对问题有所启发，限制了可能的解决方案并识别了新的困难。首先，我们给出了一个积极的结果，在 HOL4 中证明了 C/C++11 的现有公理模型保证了不使用低级原子的简单无竞争程序的顺序一致语义（DRF-SC，核心设计目标之一）。然后，我们描述了稀薄的问题，并表明，如果不限制当前编译器优化，使用 C/C++11 模型风格的任何每个候选执行条件，就无法解决该问题。凭空执行被认为仅限于使用宽松原子的程序，但我们进一步表明，当尝试将并发模型与更多 C 语言集成、混合原子和非原子访问时，它们会重复出现，这也破坏了 DRF-SC 结果。然后，我们描述基于无序执行的显式操作构造的语义，给出了凭空示例所需的行为，但暴露了适应现有编译器优化的进一步困难。最后，我们表明将并发语义与未定义行为的 C/C++ 概念集成起来存在重大困难。我们希望由此能够刺激并促进对这一关键问题的研究。
Despite decades of research, we do not have a satisfactory concurrency semantics for any general-purpose programming language that aims to support concurrent systems code. The Java Memory Model has been shown to be unsound with respect to standard compiler optimisations, while the C/C++11 model is too weak, admitting undesirable thin-air executions.Our goal in this paper is to articulate this major open problem as clearly as is currently possible, showing how it arises from the combination of multiprocessor relaxed-memory behaviour and the desire to accommodate current compiler optimisations. We make several novel contributions that each shed some light on the problem, constraining the possible solutions and identifying new difficulties.First we give a positive result, proving in HOL4 that the existing axiomatic model for C/C++11 guarantees sequentially consistent semantics for simple race-free programs that do not use low-level atomics (DRF-SC, one of the core design goals). We then describe the thin-air problem and show that it cannot be solved, without restricting current compiler optimisations, using any per-candidate-execution condition in the style of the C/C++11 model. Thin-air executions were thought to be confined to programs using relaxed atomics, but we further show that they recur when one attempts to integrate the concurrency model with more of C, mixing atomic and nonatomic accesses, and that also breaks the DRF-SC result. We then describe a semantics based on an explicit operational construction of out-of-order execution, giving the desired behaviour for thin-air examples but exposing further difficulties with accommodating existing compiler optimisations. Finally, we show that there are major difficulties integrating concurrency semantics with the C/C++ notion of undefined behaviour.We hope thereby to stimulate and enable research on this key issue.