Checking linearizability of concurrent priority queues

DOI10.4230/LIPICS.CONCUR.2017.16zbMATH Open1442.68126arXiv1707.00639MaRDI QIDQ5111629FDOQ5111629

Authors: Ahmed Bouajjani, Constantin Enea, Chao Wang 

Publication date: 27 May 2020

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

Recommendations

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

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)

Cites Work

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

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

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)