Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

Reasoning about expression evaluation under interference

Ian J. Hayes, Cliff B. Jones, Larissa A. Meinicke

TL;DR

The paper tackles the problem of reasoning about expression evaluation under interference in concurrent programs. It introduces a fine-grained, algebraic rely-guarantee framework in which expressions are modeled as non-atomic evaluation commands ⟨|e|⟩_k, enabling precise treatment of multi-variable interference. It provides a comprehensive set of compositional laws for constant, l-value, unary, and binary expressions, along with refinement rules for conditionals and assignments, all without restricting expressions to a single critical reference. The approach is demonstrated through a Fischer-Galler forest example and is formalized and proven in Isabelle/HOL, illustrating practical applicability to trustworthy, concurrent data-structure reasoning. Overall, the work advances safe, compositional reasoning about expression evaluation under interference, avoiding oversimplified atomics and syntactic constraints while strengthening the chain of formal proofs for concurrent programming.

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.

Reasoning about expression evaluation under interference

TL;DR

The paper tackles the problem of reasoning about expression evaluation under interference in concurrent programs. It introduces a fine-grained, algebraic rely-guarantee framework in which expressions are modeled as non-atomic evaluation commands ⟨|e|⟩_k, enabling precise treatment of multi-variable interference. It provides a comprehensive set of compositional laws for constant, l-value, unary, and binary expressions, along with refinement rules for conditionals and assignments, all without restricting expressions to a single critical reference. The approach is demonstrated through a Fischer-Galler forest example and is formalized and proven in Isabelle/HOL, illustrating practical applicability to trustworthy, concurrent data-structure reasoning. Overall, the work advances safe, compositional reasoning about expression evaluation under interference, avoiding oversimplified atomics and syntactic constraints while strengthening the chain of formal proofs for concurrent programming.

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.
Paper Structure (38 sections, 116 equations, 2 figures)

This paper contains 38 sections, 116 equations, 2 figures.

Table of Contents

  1. Introduction
  2. Issues with existing approaches.
  3. Our approach
  4. Overview
  5. Wide-spectrum language
  6. Naming and syntactic precedence conventions.
  7. Command lattice and primitive operations
  8. Abstraction of program variables, values and states
  9. Primitive commands
  10. Derived commands
  11. Hoare inference rules in a rely context
  12. Expressions
  13. Evaluating expressions in a single state
  14. Evaluating expressions in the presence of interference
  15. Boolean-valued expressions
  16. ...and 23 more sections

Figures (2)

  • Figure 1: A trace satisfying a specification with precondition $p$, postcondition $q$, rely condition $r$ and guarantee condition $g$. If the initial state, $\sigma_0$, is in $p$ and all environment transitions ($\epsilon$) satisfy $r$, then all program transitions ($\pi$) must satisfy $g$ and the initial state $\sigma_0$ must be related to the final state $\sigma_7$ by the postcondition $q$, also a relation between states. The $\checkmark$ at the right indicates a terminating trace.
  • Figure 2: Operation to test equivalence with multiple references to $f$ in its guard

Theorems & Definitions (18)

  • proof
  • proof
  • proof
  • proof
  • proof
  • proof
  • proof
  • proof
  • proof
  • proof
  • ...and 8 more