Reasoning about expression evaluation under interference

TL;DR

This paper formalizes how rely-guarantee reasoning can be algebraically presented to safely reuse expressions in logical contexts for concurrent programs, addressing interference issues especially with multiple shared variables.

Contribution

It introduces an algebraic framework for rely-guarantee reasoning that clarifies conditions for safe expression reuse in concurrent program verification.

Findings

Algebraic presentation of rely-guarantee reasoning.

Formal conditions for safe expression reuse.

Application to complex concurrent examples.

Abstract

Hoare-style inference rules for program constructs permit the copying of expressions and tests from program text into logical contexts. It is known that this requires care even for sequential programs but much more serious issues arise with concurrent programs because of potential interference to the values of variables. The "rely-guarantee" approach tackles the challenge of recording acceptable interference and offers a way to provide safe inference rules for concurrent constructs. This paper shows how the algebraic presentation of rely-guarantee ideas can clarify and formalise the conditions for safely re-using expressions and tests from program text in logical contexts for reasoning about concurrent programs; crucially this extends to handling expressions that reference more than one shared variable. A non-trivial example related to the Fischer-Galler forest representation of equivalence relations is treated.