文章基本信息

标题：Simplifying proofs of linearisability using layers of abstraction
本地全文：下载
作者：Brijesh Dongol ; John Derrick
期刊名称：Electronic Communications of the EASST
电子版ISSN：1863-2122
出版年度：2014
卷号：66
语种：English
出版社：European Association of Software Science and Technology (EASST)
摘要：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 non-trivial 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.