A Concurrency Semantics for Relaxed Atomics that Permits Optimisation and Avoids Thin-Air Executions
A Concurrency Semantics for Relaxed Atomics that Permits Optimisation and Avoids Thin-Air Executions
复制标题
DOI：
10.1145/2914770.2837616
复制
发表时间：
2016-01-01
影响因子：
--
通讯作者：
Sewell, Peter
中科院分区：
文献类型：
--
作者：
Pichon-Pharabod, Jean;Sewell, Peter
尽管对并发编程语言进行了大量研究，特别是针对Java和C/C++，但我们仍然没有对它们的语义有一个令人满意的定义，一个既能接受所有常见的优化又不能承认不受欢迎的行为的定义。尤其有问题的是涉及高性能并发访问的“稀薄的”示例，例如C/C++11 RELAX ATOM。C/C++11是一种按候选者执行的模型，以前的工作已经发现，编译器优化不是孤立地对单个候选者执行进行操作，而是对表示所有执行的句法表示进行操作，这两者之间存在着紧张关系。我们为核心演算定义了并发语义，包括松弛的原子和非原子访问，以及锁，它允许广泛的优化，同时仍然禁止经典的空洞例子。它还解决了与未定义行为相关的其他问题。基本思想是使用每个线程的当前状态的事件结构表示，捕获其所有可能的执行，并允许交错执行和转换步骤，以反映代码的优化(可能是动态的)。语义是以机械化和可执行的形式定义的，设计为可在当前松散的硬件之上实现，并且足够强大，足以支持C/C++11为该片段所做的编程习惯。它为并发编程语言语义提供了一种潜在的前进方向，超越了当前的C/C++11和Java模型。
Despite much research on concurrent programming languages, especially for Java and C/C++, we still do not have a satisfactory definition of their semantics, one that admits all common optimisations without also admitting undesired behaviour. Especially problematic are the "thin-air" examples involving high-performance concurrent accesses, such as C/C++11 relaxed atomics. The C/C++11 model is in a per-candidate-execution style, and previous work has identified a tension between that and the fact that compiler optimisations do not operate over single candidate executions in isolation; rather, they operate over syntactic representations that represent all executions.In this paper we propose a novel approach that circumvents this difficulty. We define a concurrency semantics for a core calculus, including relaxed-atomic and non-atomic accesses, and locks, that admits a wide range of optimisation while still forbidding the classic thin-air examples. It also addresses other problems relating to undefined behaviour.The basic idea is to use an event-structure representation of the current state of each thread, capturing all of its potential executions, and to permit interleaving of execution and transformation steps over that to reflect optimisation (possibly dynamic) of the code. These are combined with a non-multi-copy-atomic storage subsystem, to reflect common hardware behaviour.The semantics is defined in a mechanised and executable form, and designed to be implementable above current relaxed hardware and strong enough to support the programming idioms that C/C++11 does for this fragment. It offers a potential way forward for concurrent programming language semantics, beyond the current C/C++11 and Java models.