Handling TSO in Mechanized Linearizability Proofs
Handling TSO in Mechanized Linearizability Proofs
复制标题
在机械化线性化证明中处理 TSO
DOI：
10.1007/978-3-319-13338-6_11
复制
发表时间：
2014
期刊：
影响因子：
--
通讯作者：
H. Wehrheim
中科院分区：
文献类型：
--
作者：
Oleg Travkin;H. Wehrheim
线性化性是并发数据结构的关键正确性标准。近年来，已经开发了许多用于线性化的验证技术，从模型检查到机械化证明。如今，这些验证技术受到以下事实的挑战：并发软件最有可能在配备有弱内存语义的多核处理器上运行（例如Total Store Order，TSO），从而使标准技术不符合。对于模型检查和静态分析技术，已经出现了验证中弱记忆的方法，但对于受过机械化的机械化正确性证明，这缺乏这一点。
Linearizability is the key correctness criterion for concurrent data structures. In recent years, numerous verification techniques for linearizability have been developed, ranging from model checking to mechanized proving. Today, these verification techniques are challenged by the fact that concurrent software is most likely to be run on multi-core processors equipped with a weak memory semantics (like total store order, TSO), making standard techniques unsound. While for model checking and static analysis techniques, approaches for handling weak memory in verification have already emerged, this is lacking for theorem-prover supported, mechanized correctness proofs.
DOI：
10.1145/1889997.1890001
发表时间：
2011
期刊：
ACM Trans. Program. Lang. Syst.
影响因子：
--
作者：
J. Derrick;G. Schellhorn;H. Wehrheim
通讯作者：
J. Derrick;G. Schellhorn;H. Wehrheim
C/C 并发的库抽象
DOI：
10.1145/2429069.2429099
发表时间：
2013
期刊：
--
影响因子：
--
作者：
Batty M
通讯作者：
Batty M