Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

Reasoning about concurrent loops and recursion with rely-guarantee rules

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

TL;DR

The paper develops mechanically verified, rely-guarantee-based refinement laws for reasoning about concurrent recursion and while loops without assuming atomic expression evaluation. It introduces a wide-spectrum CIP language with Aczel-trace semantics, enabling compositional reasoning about interference, and defines loops/recursion via greatest fixed points with termination guided by a variant and early-termination conditions. Key contributions include fine-grained expression evaluation under interference, compositional reasoning rules for expressions and conditionals, well-founded recursion theorems, and an early-termination approach for loops in concurrent settings, all formalized in Isabelle/HOL. The work enables robust verification of concurrent data-structure algorithms, such as CAS-based removals, under non-atomic operations and arbitrary interleaving environments.

Abstract

The objective of this paper is to present general, mechanically verified, refinement rules for reasoning about recursive programs and while loops in the context of concurrency. Unlike many approaches to concurrency, we do not assume that expression evaluation is atomic. We make use of the rely-guarantee approach to concurrency that facilitates reasoning about interference from concurrent threads in a compositional manner. Recursive programs can be defined as fixed points over a lattice of commands and hence we develop laws for reasoning about fixed points. Loops can be defined in terms of fixed points and hence the laws for recursion can be applied to develop laws for loops.

Reasoning about concurrent loops and recursion with rely-guarantee rules

TL;DR

The paper develops mechanically verified, rely-guarantee-based refinement laws for reasoning about concurrent recursion and while loops without assuming atomic expression evaluation. It introduces a wide-spectrum CIP language with Aczel-trace semantics, enabling compositional reasoning about interference, and defines loops/recursion via greatest fixed points with termination guided by a variant and early-termination conditions. Key contributions include fine-grained expression evaluation under interference, compositional reasoning rules for expressions and conditionals, well-founded recursion theorems, and an early-termination approach for loops in concurrent settings, all formalized in Isabelle/HOL. The work enables robust verification of concurrent data-structure algorithms, such as CAS-based removals, under non-atomic operations and arbitrary interleaving environments.

Abstract

The objective of this paper is to present general, mechanically verified, refinement rules for reasoning about recursive programs and while loops in the context of concurrency. Unlike many approaches to concurrency, we do not assume that expression evaluation is atomic. We make use of the rely-guarantee approach to concurrency that facilitates reasoning about interference from concurrent threads in a compositional manner. Recursive programs can be defined as fixed points over a lattice of commands and hence we develop laws for reasoning about fixed points. Loops can be defined in terms of fixed points and hence the laws for recursion can be applied to develop laws for loops.

Paper Structure

This paper contains 27 sections, 5 theorems, 48 equations, 1 figure.

Table of Contents

  1. Introduction
  2. Example: removing an element from a set.
  3. Fixed points and recursion.
  4. Wide-spectrum language
  5. Naming and syntactic precedence conventions.
  6. Command lattice and primitive operations.
  7. Aczel trace semantics.
  8. Values, left values and states.
  9. Primitive commands.
  10. Derived commands.
  11. Expressions.
  12. Related work.
  13. Programming language commands.
  14. Expression evaluation under interference
  15. Related work.
  16. ...and 12 more sections

Key Result

theorem 1

For a relation $r$ and set of states $p$ that is stable under $r$, constants $\kappa$, $k$, $k_1$ and $k_2$, l-value expression $lve$, l-values $lv$ and $lv_1$, expressions $e$, $e_1$ and $e_2$, and variable $v$,

Figures (1)

  • Figure 1: An Aczel 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.

Theorems & Definitions (11)

  • definition 1: Hoare-triple
  • definition 2: stable
  • theorem 1: expressions
  • definition 3: tolerates
  • theorem 2: rely-conditional-spec
  • Lemma 3: well-founded-variant
  • theorem 4: well-founded-recursion-early
  • theorem 5: intro-while
  • proof
  • proof
  • ...and 1 more