Unified Fairness for Weak Memory Verification
Abstract
We consider the verification of omega-regular linear temporal properties of concurrent programs running under weak memory semantics. We observe that in particular, these properties may enforce liveness clauses, whose verification in this context is seldom studied. The challenge lies in precluding demonic nondeterminism arising due to scheduling, as well as due to multiple possible causes of weak memory consistency. We systematically account for the latter with a generic operational model of programs running under weak memory semantics, which can be instantiated to a host of memory models. This generic model serves as the formal basis for our definitions of fairness to preclude demonic nondeterminism: we provide both language-theoretic and probabilistic versions, and prove them equivalent in the context of the verification of omega-regular linear temporal properties. As a corollary of this proof, we obtain that under our fairness assumptions, both qualitative and quantitative verification Turing-reduce to close variants of control state reachability: a safety-verification problem. A preliminary version of this article titled "Overcoming Memory Weakness with Unified Fairness" appeared in the proceedings of CAV 2023.
Cite
@article{arxiv.2305.17605,
title = {Unified Fairness for Weak Memory Verification},
author = {Parosh Aziz Abdulla and Mohamed Faouzi Atig and Adwait Godbole and Shankaranarayanan Krishna and Mihir Vahanwala},
journal= {arXiv preprint arXiv:2305.17605},
year = {2024}
}
Comments
v2: Extended version of the CAV proceedings article (see v1). Framework for expressing memory models augmented to express models of ARM and POWER. Instantiations of models RMO, FIFO fixed. Fairness and Verification now consider general omega-regular properties. Exposition remastered. v1: Titled "Overcoming Memory Weakness with Unified Fairness". Version without Appendix appeared in CAV 2023