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)

Abstract

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)
Pages482-492
Number of pages11
ISBN (Electronic)978-1-4503-9262-4
DOIs
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

Conference

Conference41st ACM Symposium on Principles of Distributed Computing, PODC 2022
Country/TerritoryItaly
CitySalerno
Period25/07/2229/07/22

Keywords

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

Fingerprint

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

Cite this