Software Engineering and Formal Methods
Software Engineering and Formal Methods
复制标题
软件工程和形式化方法
DOI：
10.1007/978-3-319-41591-8_4
复制
发表时间：
2016
期刊：
影响因子：
--
通讯作者：
Doherty S
中科院分区：
文献类型：
--
作者：
Doherty S
大多数共享内存并发对象的验证工作都假设顺序一致性，但大多数多核处理器只支持不提供顺序一致性的弱内存模型。此外，大多数的验证工作集中在thelinearizabilityof并发对象，但也有现有的实现优化运行在弱内存模型是nonlinearizable.In本文中，我们解决这些问题，通过引入因果线性化，并发对象运行在弱内存模型的正确性条件。像线性化本身一样，因果线性化允许在对客户端行为的弱约束下组合并发对象。我们通过引入操作竞争自由度的概念来指定这些约束，其中满足此属性的程序保证其行为就像它们的共享对象实际上是可线性化的一样。我们将这些想法应用于Linux内核中的对象，这些对象被优化为在x86处理器家族的内存模型TSO上运行。
Most work on the verification of concurrent objects for shared memory assumes sequential consistency, but most multicore processors support onlyweak memory modelsthat do not provide sequential consistency. Furthermore, most verification efforts focus on thelinearizabilityof concurrent objects, but there are existing implementations optimized to run on weak memory models that are not linearizable.In this paper, we address these problems by introducingcausal linearizability, a correctness condition for concurrent objects running on weak memory models. Like linearizability itself, causal linearizability enables concurrent objects to be composed, under weak constraints on the client’s behaviour. We specify these constraints by introducing a notion ofoperation-race freedom, where programs that satisfy this property are guaranteed to behave as if their shared objects were in fact linearizable.We apply these ideas to objects from the Linux kernel, optimized to run on TSO, the memory model of the x86 processor family.
登录
查看更多内容
DOI：
--
发表时间：
2014
期刊：
International Conference on Hybrid Systems: Computation and Control
影响因子：
--
作者：
A. Sistla;Miloý Žefran;Yao Feng;Yue Ben
通讯作者：
Yue Ben
DOI：
10.1007/s10009-014-0308-3
发表时间：
2015-11-01
影响因子：
1.5
作者：
Ernst, Gidon;Pfaehler, Joerg;Reif, Wolfgang
通讯作者：
Reif, Wolfgang
DOI：
--
发表时间：
2008
期刊：
International Conference on Verification, Model Checking and Abstract Interpretation
影响因子：
--
作者：
A. Sistla;Abhigna R. Srinivas;Probabilistic Algorithms
通讯作者：
Probabilistic Algorithms
影响因子：
1
作者：
Doherty, Simon;Groves, Lindsay;Moir, Mark
通讯作者：
Moir, Mark
证明悲观 STM 的不透明性
DOI：
10.4230/lipics.opodis.2016.35
发表时间：
2016
期刊：
影响因子：
--
作者：
Simon Doherty;Brijesh Dongol;John Derrick;Gerhard Schellhorn;Heike Wehrheim
通讯作者：
Heike Wehrheim