TY - GEN
T1 - Parameterized Verification under Release Acquire is PSPACE-complete
AU - Krishna, Shankaranarayanan
AU - Godbole, Adwait
AU - Meyer, Roland
AU - Chakraborty, Soham
PY - 2022
Y1 - 2022
N2 - 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.
AB - 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.
KW - model-checking
KW - parameterized verification
KW - release-acquire semantics
KW - shared memory
KW - weak memory models
UR - http://www.scopus.com/inward/record.url?scp=85135337367&partnerID=8YFLogxK
U2 - 10.1145/3519270.3538445
DO - 10.1145/3519270.3538445
M3 - Conference contribution
AN - SCOPUS:85135337367
T3 - Proceedings of the Annual ACM Symposium on Principles of Distributed Computing
SP - 482
EP - 492
BT - PODC 2022 - Proceedings of the 2022 ACM Symposium on Principles of Distributed Computing
PB - Association for Computing Machinery (ACM)
T2 - 41st ACM Symposium on Principles of Distributed Computing, PODC 2022
Y2 - 25 July 2022 through 29 July 2022
ER -