Please use this identifier to cite or link to this item:
Title: On abstraction and compositionality for weak-memory linearisability
Authors: Dongol, B
Jagadeesan, R
Riely, J
Armstrong, A
Issue Date: 2017
Citation: VMCAI, (2017)
Abstract: Linearisability is the de facto standard correctness condition for concurrent objects. Classical linearisability assumes that the e ect of a method is captured entirely by the allowed sequences of calls and returns. This assumption is inadequate in the presence of relaxed memory models, where happens-before relations are also of importance. In this paper, we develop hb-linearisability for relaxed memory models by extending the classical notion with happens-before information. We con- sider two variants: Real time hb-linearisability, which adopts the classical view that time runs on a single global clock, and causal hb-linearisability, which eschews real-time and is appropriate for systems without a global clock. For both variants, we prove abstraction (so that programmers can reason about a client program using the sequential speci cation of an object rather than its more complex concurrent implementation) and composition (so that reasoning about independent objects can be con- ducted in isolation).
Appears in Collections:Dept of Computer Science Research Papers

Files in This Item:
File Description SizeFormat 
Fulltext.pdf386.17 kBAdobe PDFView/Open

Items in BURA are protected by copyright, with all rights reserved, unless otherwise indicated.