Parameterized Verification of Asynchronous Shared-Memory Systems
Javier Esparza, Pierre Ganty, Rupak Majumdar · Journal of the ACM · 2016
We characterize the complexity of the safety verification problem for parameterized systems consisting of a leader process and arbitrarily many anonymous and identical contributors. Processes communicate through a shared, bounded-value register. While each operation on the register is atomic, there is no synchronization primitive to execute a sequence of operations atomically. We analyze the complexity of the safety verification problem when processes are modeled by finite-state machines, pushdown machines, and Turing machines. The problem is coNP-complete when all processes are finite-state machines, and is PSPACE-complete when they are pushdown machines. The complexity remains coNP-complete when each Turing machine is allowed boundedly many interactions with the register. Our proofs use combinatorial characterizations of computations in the model, and in the case of pushdown systems, some language-theoretic constructions of independent interest. Our results are surprising, because parameterized verification problems on slight variations of our model are known to be undecidable. For example, the problem is undecidable for finite-state machines operating with synchronization primitives, and already for two communicating pushdown machines. Thus, our results show that a robust, decidable class can be obtained under the assumptions of anonymity and asynchrony.