Parameterized Verification under Release Acquire is PSPACE-complete

Shankaranarayanan Krishna, Adwait Godbole, Roland Meyer, Soham Chakraborty

Research output: Chapter in Book/Conference proceedings/Edited volumeConference contributionScientificpeer-review

2 Citations (Scopus)
69 Downloads (Pure)


We study the safety verification problem for parameterized systems under the release-acquire (RA) semantics. In the non-parameterized setting, access to atomic compare-and-swap (CAS) instructions renders the safety verification problem undecidable. In the light of this result, we consider parameterized systems consisting of an unbounded number of environment threads executing identical but CAS-free programs combined with a fixed number of distinguished threads that are unrestricted. Our first contribution is an effective and simplified RA semantics for such systems. We leverage the simplified semantics to show that safety verification becomes PSPACE in the parameterized case, an optimistic result for algorithmic verification. Our proof uses an encoding to Datalog which, in addition to the complexity upper bound, suggests a verification algorithm based on Horn clause solvers. We also provide a matching lower bound showing that safety verification is PSPACE-hard.

Original languageEnglish
Title of host publicationPODC 2022 - Proceedings of the 2022 ACM Symposium on Principles of Distributed Computing
PublisherAssociation for Computing Machinery (ACM)
Number of pages11
ISBN (Electronic)978-1-4503-9262-4
Publication statusPublished - 2022
Event41st ACM Symposium on Principles of Distributed Computing, PODC 2022 - Salerno, Italy
Duration: 25 Jul 202229 Jul 2022

Publication series

NameProceedings of the Annual ACM Symposium on Principles of Distributed Computing


Conference41st ACM Symposium on Principles of Distributed Computing, PODC 2022


  • model-checking
  • parameterized verification
  • release-acquire semantics
  • shared memory
  • weak memory models


Dive into the research topics of 'Parameterized Verification under Release Acquire is PSPACE-complete'. Together they form a unique fingerprint.

Cite this