Email Gateway (Aug 18 2022 at 19:15): Email Gateway (Aug 18 2022 at 19:15):From: Tobias Nipkow <nipkow@in.tum.de>
http://afp.sourceforge.net/entries/Abortable_Linearizable_Modules.shtml
Abortable Linearizable Module
Rachid Guerraoui, Viktor Kuncak, and Giuliano Losa
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.
These proofs accompany an upcoming PLDI paper:
http://lara.epfl.ch/w/slin
Enjoy!
Last updated: Apr 19 2024 at 01:05 UTC