Integrated Formal Methods - 11th International Conference, IFM 2014, Bertinoro, Italy, September 9-11, 2014, Proceedings
Integrated Formal Methods - 11th International Conference, IFM 2014, Bertinoro, Italy, September 9-11, 2014, Proceedings
复制标题
综合形式方法 - 第 11 届国际会议，IFM 2014，意大利贝尔蒂诺罗，2014 年 9 月 9-11 日，会议记录
DOI：
10.1007/978-3-319-10181-1_21
复制
发表时间：
2014
期刊：
影响因子：
--
通讯作者：
Derrick J
中科院分区：
文献类型：
--
作者：
Derrick J
线性性是细粒度、非原子并发算法的标准正确性准则，并且已经开发了各种验证线性性的方法。然而，大多数方法都假设一个顺序一致的内存模型，这在实践中并不总是实现的。在本文中，我们定义了一个弱内存模型的线性化：TSO （Total Store Order）内存模型，它是在x86多核架构中实现的。我们还展示了如何采用基于仿真的证明方法来验证在TSO架构上运行的算法的线性性。我们在一个典型的并发算法——自旋锁上演示了我们的方法，并使用基于仿真的方法证明了它是线性化的。以前在TSO体系结构上证明线性性的方法需要对算法的自然抽象规范进行修改。据我们所知，我们的证明方法是第一个证明正确性而不需要修改的方法。
Linearizability is the standard correctness criterion for fine-grained, non-atomic concurrent algorithms, and a variety of methods for verifying linearizability have been developed. However, most approaches assume a sequentially consistent memory model, which is not always realised in practice. In this paper we define linearizability on aweakmemory model: the TSO (Total Store Order) memory model, which is implemented in the x86 multicore architecture. We also show how a simulation-based proof method can be adapted to verify linearizability for algorithms running on TSO architectures. We demonstrate our approach on a typical concurrent algorithm, spinlock, and prove it linearizable using our simulation-based approach. Previous approaches to proving linearizabilty on TSO architectures have required a modification to the algorithm’s natural abstract specification. Our proof method is the first, to our knowledge, for proving correctness without the need for such modification.