Checking linearizability of concurrent priority queues

DOI10.4230/LIPICS.CONCUR.2017.16MaRDI QIDQ5111629zbMATH OpenFDO

Authors Ahmed Bouajjani, Constantin Enea, Chao Wang

Publication date 27 May 2020

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

zbMATH Keywords

model checkingconcurrencylinearizability

Mathematics Subject Classification ID

Specification and verification (program logics, model checking, etc.) (68Q60) Abstract data types; algebraic specification (68Q65) Models and methods for concurrent and distributed computing (process algebras, bisimulation, transition nets, etc.) (68Q85)

Recommendations

• Testing and verifying concurrent objects
• A sound and complete proof technique for linearizability of concurrent data structures
• Verifying concurrent programs against sequential specifications

Cites work

• scientific article; zbMATH DE number 2077150 (Why is no real title available?)
• A scalable, correct time-stamped stack
• An integrated specification and verification technique for highly concurrent data structures
• Aspect-oriented linearizability proofs
• Automata based verification over linearly ordered data domains
• Checking linearizability of concurrent priority queues
• Finite-memory automata
• Model-checking of correctness conditions for concurrent objects
• On the complexity of linearizability
• Testing Shared Memories
• Tractable refinement checking for concurrent objects
• Verifying concurrent programs against sequential specifications

Cited in

(12)

• A program logic for concurrent objects under fair scheduling
• Concurrent correctness in vector space
• Verifying concurrent programs against sequential specifications
• Model checking simulation rules for linearizability
• Model-checking of correctness conditions for concurrent objects
• Checking linearizability of concurrent priority queues
• Tractable refinement checking for concurrent objects
• Black-box correctness tests for basic parallel data structures
• Testing and verifying concurrent objects
• Automatically verifying concurrent queue algorithms
• On the complexity of linearizability
• Linearizable Wait-Free Iteration Operations in Shared Double-Ended Queues

Describes a project that uses

Uses Software

• SprayList

This page was built for publication: Checking linearizability of concurrent priority queues

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