On the complexity of Linearizability

TL;DR

This paper proves that verifying finite concurrent systems for Linearizability is EXPSPACE-complete, closing the previous complexity gap and providing a precise complexity classification.

Contribution

It establishes that the problem of verifying Linearizability is exactly EXPSPACE-complete, resolving a longstanding open question.

Findings

Linearizability verification is EXPSPACE-complete.

The complexity gap between lower and upper bounds is closed.

Provides a precise complexity classification for the problem.

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.