Defining Correctness Conditions for Concurrent Objects in Multicore Architectures
Defining Correctness Conditions for Concurrent Objects in Multicore Architectures
复制标题
定义多核架构中并发对象的正确性条件
DOI：
--
复制
发表时间：
2015
期刊：
影响因子：
--
通讯作者：
Graeme Smith
中科院分区：
文献类型：
--
作者：
Brijesh Dongol;J. Derrick;L. Groves;Graeme Smith
并发对象的正确性是根据确定并发对象与相应顺序对象的历史对象之间的允许关系定义的。多年来，已经提出了许多正确性条件，并且最近提出了更多的正确条件，因为实现并发对象的算法已适应以应对具有放松的内存体系结构的多层处理器。
我们提出了一个正式的框架，用于定义多层体系结构的正确性条件，涵盖了完全有序记忆的标准条件和放松记忆的较新条件，这使它们可以统一地表达，从而简化比较。我们的框架区分了顺序和承诺属性，这又使得可以建立正确的条件层次结构。我们详细考虑了总存储订单（TSO）内存模型，使用我们的框架正式将TSO的已知条件形式化，并将其顺序一致的变化。我们提出了一个用于TSO内存的工作窃取Deque，该脱口非常不可线，但相对于这些新条件是正确的。使用我们的框架，我们确定了一种新的非阻滞组成条件，即围栏一致性，围栏一致性位于已知条件之间，旨在捕获程序员指定的围栏的意图。
Correctness of concurrent objects is defined in terms of conditions that determine allowable relationships between histories of a concurrent object and those of the corresponding sequential object. Numerous correctness conditions have been proposed over the years, and more have been proposed recently as the algorithms implementing concurrent objects have been adapted to cope with multicore processors with relaxed memory architectures.
We present a formal framework for defining correctness conditions for multicore architectures, covering both standard conditions for totally ordered memory and newer conditions for relaxed memory, which allows them to be expressed in uniform manner, simplifying comparison. Our framework distinguishes between order and commitment properties, which in turn enables a hierarchy of correctness conditions to be established. We consider the Total Store Order (TSO) memory model in detail, formalise known conditions for TSO using our framework, and develop sequentially consistent variations of these. We present a work-stealing deque for TSO memory that is not linearizable, but is correct with respect to these new conditions. Using our framework, we identify a new non-blocking compositional condition, fence consistency, which lies between known conditions for TSO, and aims to capture the intention of a programmer-specified fence.
登录
查看更多内容
DOI：
10.1145/1889997.1890001
发表时间：
2011
期刊：
ACM Trans. Program. Lang. Syst.
影响因子：
--
作者：
J. Derrick;G. Schellhorn;H. Wehrheim
通讯作者：
J. Derrick;G. Schellhorn;H. Wehrheim
影响因子：
1.1
作者：
Filipovic I
通讯作者：
Filipovic I
所有权转移的线性化
影响因子：
0.6
作者：
Gotsman A
通讯作者：
Gotsman A
C/C 并发的库抽象
DOI：
10.1145/2429069.2429099
发表时间：
2013
期刊：
--
影响因子：
--
作者：
Batty M
通讯作者：
Batty M