Checking Presence Reachability Properties on Parameterized Shared-Memory Systems

TL;DR

This paper investigates the verification of parameterized shared-memory systems with unbounded processes and registers, establishing complexity results and identifying conditions for polynomial-time solvability.

Contribution

It introduces the first complexity analysis for presence reachability in round-based shared-memory systems with unbounded parameters and identifies tractable cases.

Findings

Parameterized verification is PSPACE-complete in round-based models.

In roundless models with finitely many registers, verification is NP-complete.

Certain restrictions enable polynomial-time verification.

Abstract

We consider the verification of distributed systems composed of an arbitrary number of asynchronous processes. Processes are identical finite-state machines that communicate by reading from and writing to a shared memory. Beyond the standard model with finitely many registers, we tackle round-based shared-memory systems with fresh registers at each round. In the latter model, both the number of processes and the number of registers are unbounded, making verification particularly challenging. The properties studied are generic presence reachability objectives, which subsume classical questions such as safety or synchronization by expressing the presence or absence of processes in some states. In the more general round-based setting, we establish that the parameterized verification of presence reachability properties is PSPACE-complete. Moreover, for the roundless model with finitely many registers, we prove that the complexity drops down to NP-complete and we provide several natural restrictions that make the problem solvable in polynomial time.