### 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.

### License

BSD License

### Topics

- Computer science/Algorithms/Distributed

### Session Abortable_Linearizable_Modules

- Sequences
- IOA
- RDR
- SLin
- Simulations
- Idempotence
- Consensus

## Cite

×

Abortable_Linearizable_Modules-AFP

    @article{Abortable_Linearizable_Modules-AFP,
      author  = {Rachid Guerraoui and Viktor Kuncak and Giuliano Losa},
      title   = {Abortable Linearizable Modules},
      journal = {Archive of Formal Proofs},
      month   = {March},
      year    = {2012},
      note    = {\url{https://isa-afp.org/entries/Abortable_Linearizable_Modules.html},
                 Formal proof development},
      ISSN    = {2150-914x},
    }

Download

## Download

× Download latest

Older releases:

- Sep 13, 2023 : Isabelle2023
- Oct 27, 2022 : Isabelle2022
- Dec 14, 2021 : Isabelle2021-1
- Feb 23, 2021 : Isabelle2021
- Apr 18, 2020 : Isabelle2020
- Jun 11, 2019 : Isabelle2019
- Aug 16, 2018 : Isabelle2018
- Oct 10, 2017 : Isabelle2017
- Dec 17, 2016 : Isabelle2016-1
- Feb 22, 2016 : Isabelle2016
- May 27, 2015 : Isabelle2015
- Aug 28, 2014 : Isabelle2014
- Dec 11, 2013 : Isabelle2013-2
- Nov 17, 2013 : Isabelle2013-1
- Feb 16, 2013 : Isabelle2013
- May 24, 2012 : Isabelle2012
- Mar 2, 2012 : Isabelle2011-1