Abortable Linearizable Modules

Rachid Guerraoui 📧, Viktor Kuncak 🌐 and Giuliano Losa 📧

March 1, 2012

This is a development version of this entry. It might change over time and is not stable. Please refer to release versions for citations.


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.


BSD License


Session Abortable_Linearizable_Modules