Please use this identifier to cite or link to this item:
Full metadata record
DC FieldValueLanguage
dc.contributor.authorDongol, B-
dc.contributor.authorJagadeesan, R-
dc.contributor.authorRiely, J-
dc.contributor.authorArmstrong, A-
dc.coverage.spatialLos Angeles, USA-
dc.identifier.citationVMCAI, (2017)en_US
dc.description.abstractLinearisability 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).en_US
dc.titleOn abstraction and compositionality for weak-memory linearisabilityen_US
dc.typeConference Paperen_US
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.