Abortable Linearizable Modules


Title: Abortable Linearizable Modules
Authors: Rachid Guerraoui (rachid /dot/ guerraoui /at/ epfl /dot/ ch), Viktor Kuncak and Giuliano Losa (giuliano /dot/ losa /at/ epfl /dot/ ch)
Submission date: 2012-03-01
Abstract: We define the Abortable Linearizable Module automaton (ALM for short) and prove its key composition property using the IOA theory of HOLCF. The ALM is at the heart of the Speculative Linearizability framework. This framework simplifies devising correct speculative algorithms by enabling their decomposition into independent modules that can be analyzed and proved correct in isolation. It is particularly useful when working in a distributed environment, where the need to tolerate faults and asynchrony has made current monolithic protocols so intricate that it is no longer tractable to check their correctness. Our theory contains a typical example of a refinement proof in the I/O-automata framework of Lynch and Tuttle.
  author  = {Rachid Guerraoui and Viktor Kuncak and Giuliano Losa},
  title   = {Abortable Linearizable Modules},
  journal = {Archive of Formal Proofs},
  month   = mar,
  year    = 2012,
  note    = {\url{http://isa-afp.org/entries/Abortable_Linearizable_Modules.shtml},
            Formal proof development},
  ISSN    = {2150-914x},
License: BSD License
Status: [ok] This is a development version of this entry. It might change over time and is not stable. Please refer to release versions for citations.