Proving linearizability using forward simulations

DOI10.1007/978-3-319-63390-9_28zbMATH Open1494.68067arXiv1702.02705OpenAlexW2592567368MaRDI QIDQ2164258FDOQ2164258

Authors: Ahmed Bouajjani, Michael Emmi, Constantin Enea, Suha Orhun Mutluergil 

Publication date: 12 August 2022

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.

Full work available at URL: https://arxiv.org/abs/1702.02705

Recommendations

• A sound and complete proof technique for linearizability of concurrent data structures
• Aspect-oriented linearizability proofs
• Aspect-oriented linearizability proofs
• Proving linearizability using partial orders
• Proving Linearizability Via Non-atomic Refinement

Mathematics Subject Classification ID

Data structures (68P05) Specification and verification (program logics, model checking, etc.) (68Q60) Models and methods for concurrent and distributed computing (process algebras, bisimulation, transition nets, etc.) (68Q85)

Cited In (16)

• A mechanized refinement proof of the Chase-Lev deque using a proof system
• Aspect-oriented linearizability proofs
• Proving linearizability with temporal logic
• Verifying visibility-based weak consistency
• Aspect-oriented linearizability proofs
• Model checking simulation rules for linearizability
• Order out of chaos: proving linearizability using local views
• A constructive approach for proving data structures' linearizability
• A scalable, correct time-stamped stack
• A sound and complete proof technique for linearizability of concurrent data structures
• Proving Linearizability Via Non-atomic Refinement
• Making Linearizability Compositional for Partially Ordered Executions
• Simplifying linearizability proofs with reduction and abstraction
• Parsimonious, Simulation Based Verification of Linear Systems
• Proving linearizability using partial orders
• \textsc{Poling}: SMT aided linearizability proofs

This page was built for publication: Proving linearizability using forward simulations

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q2164258)