Unified Fairness for Weak Memory Verification

TL;DR

It is obtained that under the fairness assumptions, both qualitative and quantitative verification Turing-reduce to close variants of control state reachability: a safety-verification problem is obtained.

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.

Figures (15)

• Figure 1: Load buffering in a very simple concurrent program. Assume initially $x = y = 0$.
• Figure 2: Store buffering. Assume initially $x = y = 0$, and that the instructions cannot be (locally) reordered.
• Figure 3: Concurrency from a programmer's perspective
• Figure 4: Our blueprint to use fairness for the verification of linear temporal specifications on the evolution of control state
• Figure 5: Transition fairness is required to guarantee termination even under SC

Theorems & Definitions (15)

• proposition thmcounterproposition: Invariants
• definition thmcounterdefinition: Synchronous Composition
• definition thmcounterdefinition: Transition Fairness
• definition thmcounterdefinition: $\alpha$-Transition Fairness
• definition thmcounterdefinition: Configuration Size
• definition thmcounterdefinition: Size Bounded Executions
• definition thmcounterdefinition: Plain Configurations
• definition thmcounterdefinition: Repeatedly Plain Executions
• definition thmcounterdefinition: Probabilistic Memory Fairness
• theorem thmcountertheorem: Equivalence result of originalCAV