Proving linearizability of fault-tolerant register protocols: dependency graph approach

We propose a framework for proving linearizability of fault-tolerant register implementations in message-passing systems. Our framework is inspired by the declarative semantics approach commonly used in the programming languages community to specify the correctness of weak memory systems. It builds upon an abstraction of a dependency graph—a union of partial orders among read and write operations induced by an execution of the implementation algorithm. This approach yields surprisingly simple proofs that avoid the difficulties associated with standard techniques, such as linearization point arguments and forward simulations.