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. We first formalize the crash-recovery model and how explicit process crashes and recovery introduces further dimensionalities over …

Date

November 9, 2022

Authors

Ohad Ben-Baruch, Srivatsan Ravi

Book

International Symposium on Stabilizing, Safety, and Security of Distributed Systems

Pages

84-98

Publisher

Springer International Publishing