[isabelle] New AFP entry: Abortable Linearizable Modules


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:


This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.