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

complexityconcurrencylinearizabilityverification

Mathematics Subject Classification ID

Computational difficulty of problems (lower bounds, completeness, difficulty of approximation, etc.) (68Q17) Analysis of algorithms and problem complexity (68Q25) 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

• Abstraction for concurrent objects
• scientific article; zbMATH DE number 3694622 (Why is no real title available?)
• 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
• Linear Realizability
• scientific article; zbMATH DE number 6819785 (Why is no real title available?)
• The Density of Linear-Time Properties
• Checking linearizability of concurrent priority queues
• Verifying concurrent programs against sequential specifications
• 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)