💻 computer science

Reasoning about concurrent loops and recursion with rely-guarantee rules

This paper presents mechanically verified, general refinement rules for reasoning about recursive programs and while loops in concurrent systems using the rely-guarantee approach, without assuming atomic expression evaluation.

Original authors: Ian J. Hayes, Larissa A. Meinicke, Cliff B. Jones

Published 2026-06-12

📖 5 min read🧠 Deep dive

CC BY 4.0

Original authors: Ian J. Hayes, Larissa A. Meinicke, Cliff B. Jones

Original paper licensed under CC BY 4.0 (http://creativecommons.org/licenses/by/4.0/). ✨ This is an AI-generated explanation of the paper below. It is not written or endorsed by the authors. For technical accuracy, refer to the original paper. Read full disclaimer

Imagine you are trying to write a recipe for a team of chefs working in a chaotic, shared kitchen. Everyone is chopping, stirring, and tasting at the same time. The problem is that while Chef A is reading a recipe step, Chef B might sneak in and move an ingredient, change the temperature, or even hide a tool. This is the world of concurrent programming: multiple programs running at the same time, messing with each other's data.

This paper by Hayes, Meinicke, and Jones is like a new, ultra-strict rulebook for writing these recipes so they are guaranteed to work, even in the chaos. They focus on two specific types of cooking instructions: loops (doing something over and over) and recursion (a recipe that calls itself to solve a smaller part of the problem).

Here is the breakdown of their "kitchen rules" using simple analogies:

1. The "Rely-Guarantee" Pact

In a normal kitchen, you might just trust that no one will touch your pot. In this paper, the authors say: "Trust is not enough. We need a contract."

The Rely Condition (The "Don't Touch" List): Before you start your task, you assume the other chefs will follow certain rules. For example, "I rely on the fact that no one will add salt to my soup while I'm tasting it."
The Guarantee Condition (The "I Promise" List): In return, you promise that you will follow rules too. "I guarantee that I will never throw my spoon at the wall."
The Magic: If everyone follows their "Rely" and "Guarantee" contracts, the whole kitchen runs smoothly, even if they are all working at once.

2. The Problem with "Atomic" Assumptions

Many old rulebooks assumed that when a chef reads a recipe step, they do it instantly, like a magic snap of the fingers. They assumed the chef reads "Add 2 eggs" and adds them before anyone else can blink.

The authors say: "No, that's not how real kitchens work."
In reality, reading "Add 2 eggs" takes time. While the chef is reaching for the eggs, another chef might move the carton. This paper builds rules that account for this messy reality. They don't assume anything happens instantly; they assume everything takes a little time and can be interrupted.

3. Taming the "While" Loop (The Never-Ending Stir)

A "while loop" is like a chef stirring a pot "until the sauce is thick."

The Old Problem: In a shared kitchen, a chef might stir, check the sauce, and decide it's not thick yet. But while they are walking to the stove, another chef might add water, making it thin again. The first chef might keep stirring forever, or stop when they shouldn't.
The New Rule (Early Termination): The authors introduce a clever trick called "Early Termination."
- Imagine the chef has a timer (a "variant"). Every time they stir, the timer goes down.
- Usually, the chef must stir to make the timer go down.
- The Twist: If another chef accidentally adds water (interference), the timer might go down faster than expected, or the sauce might suddenly become thick enough that the loop should stop.
- The new rule allows the loop to stop early if the environment (the other chefs) helps finish the job, rather than forcing the loop to do all the work itself. It's like saying, "If the sauce is already thick because someone else helped, you can stop stirring immediately."

4. Taming Recursion (The Recipe That Calls Itself)

Recursion is like a chef who says, "To make this big stew, I need to make a small batch of broth first. To make that broth, I need to make a tiny bit of stock..."

The Challenge: In a shared kitchen, if Chef A is making the broth, Chef B might steal the stock pot.
The Solution: The authors created a mathematical "ladder" (a well-founded relation). Imagine the chef is climbing down a ladder to solve smaller and smaller problems.
- The Rule: You can only go down the ladder if you are sure you won't get stuck.
- The "Early Exit" Trick: Just like with the loops, if the other chefs help you get to the bottom of the ladder faster (by solving a sub-problem for you), you are allowed to stop climbing down early. You don't have to force every single step yourself if the environment helps you finish.

5. The "Aczel Trace" (The Kitchen Security Camera)

To prove their rules work, the authors use a concept called an Aczel trace.

Imagine a security camera recording the kitchen.
The camera records two types of movements: Program moves (what the chef you are watching does) and Environment moves (what the other chefs do).
The authors' rules ensure that no matter how the camera records the chaos, if the "Rely" and "Guarantee" contracts are kept, the final dish will be perfect.

Summary

This paper provides a new, robust way to write instructions for computer programs that run at the same time.

No Magic: It stops assuming things happen instantly.
Contracts: It uses "Rely" and "Guarantee" to manage how programs interact.
Flexibility: It allows loops and recursive functions to stop early if the environment helps them finish, preventing them from getting stuck in infinite loops or failing because of interference.

The authors have already tested these rules using a computer proof assistant (Isabelle/HOL), which acts like a super-strict math teacher, checking every single step to ensure the logic is flawless. They didn't just guess; they proved it works.

Technical Summary: Reasoning about Concurrent Loops and Recursion with Rely-Guarantee Rules

Problem Statement

The verification of concurrent programs, particularly those involving recursive structures and while loops, faces significant challenges when dealing with interference from parallel threads. Traditional Hoare-style verification rules for loops rely on invariants and variant expressions to prove correctness and termination. However, in a concurrent setting, interference can invalidate loop invariants, increase variant expressions, or disrupt the evaluation of loop guards, rendering standard sequential rules invalid.

Furthermore, many existing Rely-Guarantee (RG) approaches assume that expression evaluation is atomic. This assumption does not reflect the reality of programming language implementations, where expressions may involve multiple accesses to shared variables that can be interleaved with environment transitions. This atomicity assumption breaks the formal chain of reasoning for complex expressions and limits the applicability of the verification rules.

Methodology

The authors develop a framework for reasoning about recursive programs and while loops within a Rely-Guarantee context, utilizing a wide-spectrum language based on a complete distributive lattice of commands. The methodology is grounded in the following key components:

Aczel Trace Semantics: The semantic model uses sets of Aczel traces, which record sequences of program ( $\pi$ ) and environment ( $\epsilon$ ) transitions. This allows for a compositional treatment of interference without assuming atomicity of expression evaluation or assignment commands.
Rely-Guarantee Conditions: The framework employs rely conditions ( $r$ ) to constrain the environment's behavior and guarantee conditions ( $g$ ) to constrain the program's behavior. The guarantee of a thread must imply the rely condition of all parallel threads.
Fixed-Point Theory: Recursive programs are defined as fixed points over a lattice of commands. The authors develop laws for reasoning about these fixed points, specifically utilizing well-founded induction with variant expressions and relations to prove termination.
Early Termination: A central methodological innovation is the development of "early termination" versions of laws for both recursion and loops. Unlike standard approaches that require the variant to be strictly reduced by the function body before any recursive calls, these laws allow the function body to either reduce the variant or establish a condition (a base case) that ensures no further recursive calls are made. This is crucial for concurrency, where interference might reduce the variant in a way that precludes the function body from reducing it, yet still ensures termination.
Non-Atomic Expression Evaluation: The approach explicitly handles the non-atomic evaluation of expressions. It uses a compositional method to establish postconditions for complex expressions by analyzing their sub-expressions, avoiding the need for syntactic restrictions like the "single critical reference" found in atomic-assumption theories.

Key Contributions

The paper presents several specific contributions to the theory of concurrent program verification:

General Refinement Rules for Recursion: Theorem 5 ("recursion-early") provides a rule for introducing recursion that accommodates interference. It uses a well-founded relation and a variant expression, allowing termination to be proven even if the variant is reduced by the environment rather than the function body, provided a base case is established.
General Refinement Rules for While Loops: Theorem 6 ("intro-while") derives a law for introducing while loops based on the recursion law. It includes an "early termination" condition ( $p_X$ ) that allows the loop to exit if the guard evaluates to false due to interference, even if the loop body did not strictly decrease the variant.
Handling Non-Atomic Expressions: The framework provides inference rules (e.g., Theorem 2 for conditionals, Theorem 3 for function calls) that allow compositional reasoning about expressions and guards under interference without assuming atomic evaluation.
Formal Verification: All lemmas and theorems presented in the paper have been mechanically verified using the Isabelle/HOL theorem prover.
Fair Termination: The paper addresses fair termination, defining a command fair that disallows infinite contiguous sequences of environment transitions, and showing how to prove that a command performs only a finite number of transitions under fair execution.

Results and Examples

The paper demonstrates the utility of the developed laws through two primary examples:

Parallel Recursive Search: A recursive search algorithm is developed to find a value $i$ in a range $[0, N)$ satisfying a predicate $P$ . The implementation uses a divide-and-conquer strategy with parallel recursive calls. The proof utilizes the "recursion-early" law to handle the case where a concurrent thread may have already found a solution (setting a found flag), allowing the recursive calls to terminate early without further processing.
Atomic Update with CAS: An example of implementing an atomic specification to update a variable $m$ to $\min(m, lo)$ using a Compare-And-Swap (CAS) instruction. The loop repeatedly attempts the CAS. The "early termination" version of the loop law is essential here: if interference decreases $m$ below $lo$ between the guard check and the CAS execution, the CAS may fail to decrease $m$ (the variant). However, the loop terminates because the guard ($lo < m$) becomes false. The standard loop law would fail to prove termination in this scenario, but the proposed law succeeds by recognizing the early exit condition.

Significance and Claims

The authors claim that their work provides general, mechanically verified refinement rules for reasoning about recursion and loops in the presence of concurrency. The significance of this work lies in:

Removing Atomicity Assumptions: By not assuming expression evaluation is atomic, the rules are applicable to a broader range of realistic programming scenarios and avoid breaking the formal chain of reasoning found in theories that rely on atomicity.
Handling Interference in Termination Proofs: The "early termination" laws address a specific gap in concurrent verification where interference can invalidate standard termination arguments. This allows for the verification of programs where the environment's actions contribute to the termination condition.
Compositional Development: The approach supports the compositional development of shared-variable concurrent programs, allowing threads to be designed and verified independently based on their rely and guarantee conditions.
Formal Rigor: The results are not merely theoretical proposals but have been formalized and verified within the Isabelle/HOL theorem prover, ensuring their logical soundness.

The paper positions itself as an extension of previous algebraic Rely-Guarantee research, specifically targeting the complexities introduced by recursion, loops, and non-atomic expression evaluation in concurrent systems. It does not claim to replace other logics like Concurrent Separation Logic (CSL) but offers an alternative compositional method, particularly noting that while CSL supports reasoning about race freedom, RG is designed for the development of "racy" programs (programs where races are managed via rely/guarantee conditions).