On the complexity of linearizability

DOI10.1007/S00607-018-0596-7MaRDI QIDQ2218465zbMATH OpenOpenAlexFDO

Authors Jad Hamza

Publication date 15 January 2021

Published in Computing (Search for Journal in Brave)

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

zbMATH Keywords

verificationcomplexityconcurrencylinearizability

Mathematics Subject Classification ID

Analysis of algorithms and problem complexity (68Q25) Computational difficulty of problems (lower bounds, completeness, difficulty of approximation, etc.) (68Q17) Specification and verification (program logics, model checking, etc.) (68Q60) Models and methods for concurrent and distributed computing (process algebras, bisimulation, transition nets, etc.) (68Q85)

Abstract: It was shown in Alur et al. [1] that the problem of verifying finite concurrent systems through Linearizability is in EXPSPACE. However, there was still a complexity gap between the easy to obtain PSPACE lower bound and the EXPSPACE upper bound. We show in this paper that Linearizability is EXPSPACE-complete.

Recommendations

• Verifying concurrent programs against sequential specifications
• Checking linearizability of concurrent priority queues
• Comparison Under Abstraction for Verifying Linearizability

Cites work

• scientific article; zbMATH DE number 3694622 (Why is no real title available?)
• Abstraction for concurrent objects
• Model-checking of correctness conditions for concurrent objects
• Simplifying linearizability proofs with reduction and abstraction
• Testing Shared Memories
• Verifying concurrent programs against sequential specifications

Cited in

(8)

• Linearity of algorithms and a result of Ando
• TSO-to-TSO linearizability is undecidable
• The Density of Linear-Time Properties
• Verifying concurrent programs against sequential specifications
• Linear Realizability
• Checking linearizability of concurrent priority queues
• scientific article; zbMATH DE number 6819785 (Why is no real title available?)
• Intermediate value linearizability: a quantitative correctness criterion

Describes a project that uses

Uses Software

• Line-up

This page was built for publication: On the complexity of linearizability

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