Separation and Equivalence results for the Crash-stop and Crash-recovery Shared Memory Models

TL;DR

This paper investigates the relationship between crash-stop and crash-recovery shared memory models, formalizing strict-linearizability and analyzing how helping mechanisms affect implementation correctness.

Contribution

It formalizes the crash-recovery model, proves independence of strict-linearizability from help definitions, and characterizes when help-free, linearizable, obstruction-free implementations are also strict-linearizable.

Findings

Strict-linearizability is independent of help mechanisms.

Help-free, obstruction-free, linearizable implementations are also strict-linearizable.

Non-blocking strict-linearizable implementations generally cannot have helping.

Abstract

Linearizability, the traditional correctness condition for concurrent data structures is considered insufficient for the non-volatile shared memory model where processes recover following a crash. For this crash-recovery shared memory model, strict-linearizability is considered appropriate since, unlike linearizability, it ensures operations that crash take effect prior to the crash or not at all. This work formalizes and answers the question of whether an implementation of a data type derived for the crash-stop shared memory model is also strict-linearizable in the crash-recovery model. This work presents a rigorous study to prove how helping mechanisms, typically employed by non-blocking implementations, is the algorithmic abstraction that delineates linearizability from strict-linearizability. Our first contribution formalizes the crash-recovery model and how explicit process crashes and recovery introduces further dimensionalities over the standard crash-stop shared memory model. We make the following technical contributions: (i) we prove that strict-linearizability is independent of any known help definition; (ii) we then present a natural definition of help-freedom to prove that any obstruction-free, linearizable and help-free implementation of a total object type is also strict-linearizable; (iii) finally, we prove that for a large class of object types, a non-blocking strict-linearizable implementation cannot have helping. Viewed holistically, this work provides the first precise characterization of the intricacies in applying a concurrent implementation designed for the crash-stop model to the crash-recovery model, and vice-versa.