Decidability and Complexity for Quiescent Consistency
Decidability and Complexity for Quiescent Consistency
复制标题
静态一致性的可判定性和复杂性
DOI：
10.1145/2933575.2933576
复制
发表时间：
2016
期刊：
影响因子：
--
通讯作者：
Dongol B
中科院分区：
文献类型：
--
作者：
Dongol B
静态一致性是并发对象的正确性的概念，它赋予对象在静态中的行为以意义，即，没有对象的操作被执行的状态。该条件允许更多的行为被接纳，从而使更大的灵活性，在对象设计，这反过来又允许算法实现静态一致的对象是更有效的（当在多线程环境中执行时）。静态一致性的实现对象定义在一个相应的抽象规范。这就产生了两个重要的验证问题：成员资格（检查实现的行为是否被规范允许）和正确性（检查实现的所有行为是否被规范允许）。在本文中，我们考虑静态一致性的成员资格和正确性条件，以及一个限制的形式，假设两个静态之间的事件数量的上限。我们表明，成员资格的问题，无限制的静态一致性是NP-完全的，正确性问题是可判定的，coNEXPTIME-硬，在EXPSPACE。对于限制的形式，我们表明，成员是在PTIME，而正确性是PSPACE完全的。
Quiescent consistency is a notion of correctness for a concurrent object that gives meaning to the object's behaviours in quiescent states, i.e., states in which none of the object's operations are being executed. The condition enables greater flexibility in object design by allowing more behaviours to be admitted, which in turn allows the algorithms implementing quiescent consistent objects to be more efficient (when executed in a multithreaded environment).Quiescent consistency of an implementation object is defined in terms of a corresponding abstract specification. This gives rise to two important verification questions: membership (checking whether a behaviour of the implementation is allowed by the specification) and correctness (checking whether all behaviours of the implementation are allowed by the specification). In this paper, we consider the membership and correctness conditions for quiescent consistency, as well as a restricted form that assumes an upper limit on the number of events between two quiescent states. We show that the membership problem for unrestricted quiescent consistency is NP-complete and that the correctness problem is decidable, coNEXPTIME-hard, and in EXPSPACE. For the restricted form, we show that membership is in PTIME, while correctness is PSPACE-complete.
登录
查看更多内容
线性化与静态一致性之间 - 定量静态一致性
DOI：
10.1007/978-3-662-43951-7_19
发表时间：
2014
期刊：
ArXiv
影响因子：
--
作者：
R. Jagadeesan;James Riely
通讯作者：
James Riely
影响因子：
--
作者：
D. Huynh
通讯作者：
D. Huynh
承认你的弱点：验证 TSO 架构的正确性
影响因子：
3.3
作者：
Graeme Smith;J. Derrick;Brijesh Dongol
通讯作者：
Brijesh Dongol
通过放宽分布式数据结构来提高平均性能
DOI：
--
发表时间：
2014
期刊：
International Symposium on Distributed Computing
影响因子：
--
作者：
Edward Talmage;J. Welch
通讯作者：
J. Welch
重复数据库系统的一致性和正确性
DOI：
--
发表时间：
1977
期刊：
Symposium on Operating Systems Principles
影响因子：
--
作者：
C. Ellis
通讯作者：
C. Ellis