Aspect-oriented linearizability proofs

DOI10.1007/978-3-642-40184-8_18MaRDI QIDQ2842111zbMATH OpenOpenAlexFDO

Authors Ali Sezgin, Viktor Vafeiadis, Thomas A. Henzinger

Publication date 12 August 2013

Published in CONCUR 2013 – Concurrency Theory (Search for Journal in Brave)

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

Mathematics Subject Classification ID

Data structures (68P05) Models and methods for concurrent and distributed computing (process algebras, bisimulation, transition nets, etc.) (68Q85) Parallel algorithms in computer science (68W10)

Abstract: Linearizability of concurrent data structures is usually proved by monolithic simulation arguments relying on the identification of the so-called linearization points. Regrettably, such proofs, whether manual or automatic, are often complicated and scale poorly to advanced non-blocking concurrency patterns, such as helping and optimistic updates. In response, we propose a more modular way of checking linearizability of concurrent queue algorithms that does not involve identifying linearization points. We reduce the task of proving linearizability with respect to the queue specification to establishing four basic properties, each of which can be proved independently by simpler arguments. As a demonstration of our approach, we verify the Herlihy and Wing queue, an algorithm that is challenging to verify by a simulation proof.

Recommendations

• Aspect-oriented linearizability proofs
• A sound and complete proof technique for linearizability of concurrent data structures
• Proving linearizability using forward simulations
• Proving linearizability using partial orders
• \textsc{Poling}: SMT aided linearizability proofs

Cited in

(16)

• Modular verification of concurrency-aware linearizability
• \textsc{Poling}: SMT aided linearizability proofs
• Proving linearizability using forward simulations
• A mechanized refinement proof of the Chase-Lev deque using a proof system
• A generic logic for proving linearizability
• A sound and complete proof technique for linearizability of concurrent data structures
• Decomposable relaxation for concurrent data structures
• Proving linearizability using partial orders
• Simplifying linearizability proofs with reduction and abstraction
• Order out of chaos: proving linearizability using local views
• Checking linearizability of concurrent priority queues
• Wait-free linearization with a mechanical proof
• Verifying linearizability with hindsight
• Aspect-oriented linearizability proofs
• Strict linearizability and abstract atomicity
• Visibility and separability for a declarative linearizability proof of the timestamped stack

This page was built for publication: Aspect-oriented linearizability proofs

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