Electronic Communications of the EASST Volume 66 ( 2013 ) Proceedings of the Automated Verification of Critical Systems ( AVoCS 2013 ) Simplifying proofs of linearisability using layers of abstraction
Electronic Communications of the EASST Volume 66 ( 2013 ) Proceedings of the Automated Verification of Critical Systems ( AVoCS 2013 ) Simplifying proofs of linearisability using layers of abstraction
复制标题
EASST 电子通信第 66 卷 (2013) 关键系统自动验证论文集 (AVoCS 2013) 使用抽象层简化线性化证明
DOI：
--
复制
发表时间：
2014
期刊：
影响因子：
--
通讯作者：
J. Derrick
中科院分区：
文献类型：
--
作者：
Brijesh Dongol;J. Derrick
线性性已成为并发数据结构的标准正确性标准，确保并发操作的每个调用和响应历史记录都有匹配的顺序历史记录。现有的线性化证明要求人们在所考虑的操作中识别所谓的线性化点，这些点是原子语句，其执行会导致操作的效果被感受到。然而，识别线性化点是一项艰巨的任务，需要高度的专业知识。对于复杂的算法，例如 Heller 等人的惰性集，甚至可以通过在正在验证的操作之外并发执行语句来线性化操作。本文提出了一种验证线性化的方法，该方法不需要识别线性化点。相反，使用基于间隔的逻辑，我们表明任何间隔上每个具体操作的每个行为都是以粗粒度原子性执行的相应抽象的可能行为。该方法应用于 Heller 等人的惰性集，以表明无需考虑程序代码中的线性化点即可验证线性化能力。
Linearisability has become the standard correctness criterion for concurrent data structures, ensuring that every history of invocations and responses of concurrent operations has a matching sequential history. Existing proofs of linearisability require one to identify so-called linearisation points within the operations under consideration, which are atomic statements whose execution causes the effect of an operation to be felt. However, identification of linearisation points is a nontrivial task, requiring a high degree of expertise. For sophisticated algorithms such as Heller et al’s lazy set, it even is possible for an operation to be linearised by the concurrent execution of a statement outside the operation being verified. This paper proposes a method for verifying linearisability that does not require identification of linearisation points. Instead, using an interval-based logic, we show that every behaviour of each concrete operation over any interval is a possible behaviour of a corresponding abstraction that executes with coarse-grained atomicity. This approach is applied to Heller et al’s lazy set to show that verification of linearisability is possible without having to consider linearisation points within the program code.