Safety Verification of Parameterized Systems under Release-Acquire

TL;DR

This paper introduces a simplified semantics for verifying safety in parameterized systems under release-acquire, showing that certain verification problems are PSPACE-complete or NEXP-complete depending on system restrictions.

Contribution

It proposes a new semantics equivalent for safety verification, analyzes complexity bounds for subclasses, and clarifies the tractability limits under release-acquire semantics.

Findings

Safety verification is PSPACE-complete for loop-free distinguished threads.

Verification complexity increases to NEXP-complete with an unrestricted distinguished thread.

The new semantics simplifies RA while preserving verification equivalence.

Abstract

We study the safety verification problem for parameterized systems under the release-acquire (RA) semantics. It has been shown that the problem is intractable for systems with unlimited access to atomic compare-and-swap (CAS) instructions. We show that, from a verification perspective where approximate results help, this is overly pessimistic. We study parameterized systems consisting of an unbounded number of environment threads executing identical but CAS-free programs and a fixed number of distinguished threads that are unrestricted. Our first contribution is a new semantics that considerably simplifies RA but is still equivalent for the above systems as far as safety verification is concerned. We apply this (general) result to two subclasses of our model. We show that safety verification is only \pspace-complete for the bounded model checking problem where the distinguished threads are loop-free. Interestingly, we can still afford the unbounded environment. We show that the complexity jumps to \nexp-complete for thread-modular verification where an unrestricted distinguished `ego' thread interacts with an environment of CAS-free threads plus loop-free distinguished threads (as in the earlier setting). Besides the usefulness for verification, the results are strong in that they delineate the tractability border for an established semantics.