On the Correctness Problem for Serializability
On the Correctness Problem for Serializability
复制标题
关于可串行化的正确性问题
DOI：
10.1007/978-3-030-85315-0_4
复制
发表时间：
2021
期刊：
影响因子：
--
通讯作者：
Heike Wehrheim
中科院分区：
文献类型：
--
作者：
Jürgen König;Heike Wehrheim
并发正确性条件形式化了对共享对象状态的并发访问中“看似原子性”的概念。对于不同种类的对象（数据库，并发数据结构，软件事务存储器），不同种类的正确性条件已被提出（可串行化，线性化，不透明）。并发正确性条件的可判定性研究两个问题：成员资格问题是关于单个执行是否正确的问题;正确性问题是关于给定实现的所有执行是否正确的问题.本文研究了Papadimitrious的数据库事务可串行化概念的可判定性. Papadimitriou已经证明了可串行化的成员问题是NP完全的。对于正确性，我们考虑一个更严格的版本也提出了Papadimitriou，这需要一个额外的真实的时间顺序约束。我们证明这个版本是可判定的，因为所有的交易都是实时的。
Concurrent correctness conditions formalize the notion of “seeming atomicity” in concurrent access to shared object state. For different sorts of objects (databases, concurrent data structures, software transactional memory) different sorts of correctness conditions have been proposed (serializability, linearizability, opacity). Decidability of concurrent correctness conditions studies two problems: themembership problemasks whether a single execution is correct; thecorrectness problemasks whether all executions of a given implementation are correct.In this paper we investigate decidability of Papadimitrious’s notion of serializability for database transactions. Papadimitriou has proved the membership problem for serializability to be NP-complete. For correctness we consider a stricter version also proposed by Papadimitriou, which requires an additional real time order constraint. We show this version to be decidable given that all transactions are live.
通过模型检查验证共享内存多处理器上的顺序一致性
DOI：
--
发表时间：
2001
期刊：
IEEE Trans. Parallel Distributed Syst.
影响因子：
--
作者：
S. Qadeer
通讯作者：
S. Qadeer
监控并发程序中的原子性
DOI：
--
发表时间：
2008
期刊：
International Conference on Computer Aided Verification
影响因子：
--
作者：
Azadeh Farzan;P. Madhusudan
通讯作者：
P. Madhusudan
影响因子：
1
作者：
Doherty, Simon;Groves, Lindsay;Moir, Mark
通讯作者：
Moir, Mark