Admit Your Weakness: Verifying Correctness on TSO Architectures
Admit Your Weakness: Verifying Correctness on TSO Architectures
复制标题
承认你的弱点：验证 TSO 架构的正确性
DOI：
10.1007/978-3-319-15317-9_22
复制
发表时间：
2014
影响因子：
3.3
通讯作者：
Brijesh Dongol
中科院分区：
文献类型：
--
作者：
Graeme Smith;J. Derrick;Brijesh Dongol
线性化性已成为细粒度非原子并发算法的标准正确性标准，但是，大多数方法都采用顺序一致的记忆模型，在本文中，这并不总是实现的。模型：TSO（总存储订单）内存模型，通常由多项架构实现。因此，我们证明了一个较弱的标准，而Quiestcent的一致性像线性性，QuiestCent的一致性是组成，使其成为基于组件的上下文中的理想正确性标准。基于仿真的方法。据我们所知，修改算法的高水平要求是证明正确性的，而无需进行这种修改。
Linearizability has become the standard correctness criterion for fine-grained non-atomic concurrent algorithms, however, most approaches assume a sequentially consistent memory model, which is not always realised in practice. In this paper we study the correctness of concurrent algorithms on a weak memory model: the TSO (Total Store Order) memory model, which is commonly implemented by multicore architectures. Here, linearizability is often too strict, and hence, we prove a weaker criterion, quiescent consistency instead. Like linearizability, quiescent consistency is compositional making it an ideal correctness criterion in a component-based context. We demonstrate how to model a typical concurrent algorithm, seqlock, and prove it quiescent consistent using a simulation-based approach. Previous approaches to proving correctness on TSO architectures have been based on linearizabilty which makes it necessary to modify the algorithm’s high-level requirements. Our approach is the first, to our knowledge, for proving correctness without the need for such a modification.
DOI：
10.1145/1889997.1890001
发表时间：
2011
期刊：
ACM Trans. Program. Lang. Syst.
影响因子：
--
作者：
J. Derrick;G. Schellhorn;H. Wehrheim
通讯作者：
J. Derrick;G. Schellhorn;H. Wehrheim