Lifting the Reasoning Level in Generic Weak Memory Verification (Extended Version)

TL;DR

This paper enhances generic weak memory verification by elevating reasoning to a more abstract level using view-based assertions, reducing proof complexity and improving transferability across models.

Contribution

It introduces novel proof rules for reasoning on program constructs, lifting low-level axiomatic proofs to a higher abstraction level in weak memory verification.

Findings

Significant reduction in proof steps compared to low-level axioms

Proof rules are sound and applicable to write-to-read causality tests

Enhanced transferability of verification techniques across different memory models

Abstract

Weak memory models specify the semantics of concurrent programs on multi-core architectures. Reasoning techniques for weak memory models are often specialized to one fixed model and verification results are hence not transferable to other memory models. A recent proposal of a generic verification technique based on axioms on program behaviour expressed via weakest preconditions aims at overcoming this specialization to dedicated models. Due to the usage of weakest preconditions, reasoning however takes place on a very low level requiring the application of numerous axioms for deriving program properties, even for a single statement. In this paper, we lift reasoning in this generic verification approach to a more abstract level. Based on a view-based assertion language, we provide a number of novel proof rules for directly reasoning on the level of program constructs. We prove soundness of our proof rules and exemplify them on the write-to-read causality (WRC) litmus test. A comparison to the axiom-based low-level proof reveals a significant reduction in the number of required proof steps.