Order out of chaos: proving linearizability using local views

DOI10.4230/LIPICS.DISC.2018.23MaRDI QIDQ5090915zbMATH OpenFDO

Authors Yotam M. Y. Feldman, Constantin Enea, Adam Morrison, Noam Rinetzky, Sharon Shoham

Publication date 21 July 2022

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

zbMATH Keywords

concurrencyconcurrent data structuresformal methodslineariazabilityoptimistic concurrency controlsynchronizationverification

Mathematics Subject Classification ID

Data structures (68P05) Models and methods for concurrent and distributed computing (process algebras, bisimulation, transition nets, etc.) (68Q85)

Recommendations

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

Cites work

• \textsc{Poling}: SMT aided linearizability proofs
• A constructive approach for proving data structures' linearizability
• A fast contention-friendly binary search tree
• A Simple Optimistic Skiplist Algorithm
• An integrated specification and verification technique for highly concurrent data structures
• Aspect-oriented linearizability proofs
• Comparison Under Abstraction for Verifying Linearizability
• CONCUR 2004 - Concurrency Theory
• CONCUR 2004 - Concurrency Theory
• Concurrent search structure algorithms
• scientific article; zbMATH DE number 2006660 (Why is no real title available?)
• Iris: monoids and invariants as an orthogonal basis for concurrent reasoning
• Modular verification of a non-blocking stack
• Permission accounting in separation logic
• Pragmatic primitives for non-blocking data structures
• Proving linearizability using forward simulations
• Shape-Value Abstraction for Verifying Linearizability
• Specifying and verifying concurrent algorithms with histories and subjectivity
• Subjective auxiliary state for coarse-grained concurrency
• The topological structure of asynchronous computability
• Unifying refinement and Hoare-style reasoning in a logic for higher-order concurrency
• Verifying concurrent programs against sequential specifications
• Verifying linearizability with hindsight
• Verifying properties of parallel programs

Cited in

(4)

• A constructive approach for proving data structures' linearizability
• In the search for optimal concurrency
• Verifying linearizability with hindsight
• Make flows small again: revisiting the flow framework

This page was built for publication: Order out of chaos: proving linearizability using local views

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