# Proving linearizability using forward simulations

## TL;DR

This paper demonstrates that many complex concurrent data structure implementations can be proven linearizable using only forward simulation, simplifying correctness proofs and enabling automation.

## Contribution

It shows that forward simulation alone suffices for proving linearizability of complex implementations, challenging the belief that backward reasoning is necessary.

## Key findings

- Many complex implementations can be proved correct with forward simulation.
- Forward simulation proofs are simpler and more natural.
- These proofs are suitable for automation.

## Abstract

Linearizability is the standard correctness criterion concurrent data structures such as stacks and queues. It allows to establish observational refinement between a concurrent implementation and an atomic reference implementation.Proving linearizability requires identifying linearization points for each method invocation along all possible computations, leading to valid sequential executions, or alternatively, establishing forward and backward simulations. In both cases, carrying out proofs is hard and complex in general. In particular, backward reasoning is difficult in the context of programs with data structures, and strategies for identifying statically linearization points cannot be defined for all existing implementations. In this paper, we show that, contrary to common belief, many such complex implementations, including, e.g., the Herlihy&Wing Queue and the Time-Stamped Stack, can be proved correct using only forward simulation arguments. This leads to conceptually simple and natural correctness proofs for these implementations that are amenable to automation.