Proving linearizability using partial orders

DOI10.1007/978-3-662-54434-1_24MaRDI QIDQ2988662zbMATH OpenOpenAlexFDO

Authors Artem Khyzha, Mike Dodds, Alexey Gotsman, Matthew J. Parkinson

Publication date 19 May 2017

Published in Programming Languages and Systems (Search for Journal in Brave)

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

Mathematics Subject Classification ID

Logic in computer science (03B70) Partial orders, general (06A06) Data structures (68P05)

Abstract: Linearizability is the commonly accepted notion of correctness for concurrent data structures. It requires that any execution of the data structure is justified by a linearization --- a linear order on operations satisfying the data structure's sequential specification. Proving linearizability is often challenging because an operation's position in the linearization order may depend on future operations. This makes it very difficult to incrementally construct the linearization in a proof. We propose a new proof method that can handle data structures with such future-dependent linearizations. Our key idea is to incrementally construct not a single linear order of operations, but a partial order that describes multiple linearizations satisfying the sequential specification. This allows decisions about the ordering of operations to be delayed, mirroring the behaviour of data structure implementations. We formalise our method as a program logic based on rely-guarantee reasoning, and demonstrate its effectiveness by verifying several challenging data structures: the Herlihy-Wing queue, the TS queue and the Optimistic set.

Recommendations

• Aspect-oriented linearizability proofs
• Aspect-oriented linearizability proofs
• A sound and complete proof technique for linearizability of concurrent data structures
• Proving linearizability using forward simulations
• A constructive approach for proving data structures' linearizability

Cites work

• A scalable, correct time-stamped stack
• A sound and complete proof technique for linearizability of concurrent data structures
• Abstraction for concurrent objects
• An axiomatic proof technique for parallel programs
• Aspect-oriented linearizability proofs
• Intransitive indifference with unequal indifference intervals
• Linearizability with ownership transfer
• Logical relations for fine-grained concurrency
• Modular verification of concurrency-aware linearizability
• Proving linearizability using partial orders
• Unifying refinement and Hoare-style reasoning in a logic for higher-order concurrency
• Verifying linearizability with hindsight

Cited in

(14)

• Completeness of a prover for dense linear orders
• A constructive approach for proving data structures' linearizability
• \textsc{Poling}: SMT aided linearizability proofs
• Proving linearizability using forward simulations
• Aspect-oriented linearizability proofs
• A sound and complete proof technique for linearizability of concurrent data structures
• Proving linearizability using partial orders
• Verifying visibility-based weak consistency
• Order out of chaos: proving linearizability using local views
• scientific article; zbMATH DE number 7407781 (Why is no real title available?)
• Aspect-oriented linearizability proofs
• Making Linearizability Compositional for Partially Ordered Executions
• Visibility and separability for a declarative linearizability proof of the timestamped stack
• A compositional theory of linearizability

This page was built for publication: Proving linearizability using partial orders

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