💻 computer science

Reasoning about concurrent loops and recursion with rely-guarantee rules

本文提出了经过机械验证的、通用的细化规则，用于在不假设表达式求值具有原子性的情况下，利用依赖-保证（rely-guarantee）方法对并发系统中的递归程序和 while 循环进行推理。

原作者： Ian J. Hayes, Larissa A. Meinicke, Cliff B. Jones

发布于 2026-06-12

📖 1 分钟阅读☕ 轻松阅读

原作者： Ian J. Hayes, Larissa A. Meinicke, Cliff B. Jones

原始论文采用 CC BY 4.0 许可（http://creativecommons.org/licenses/by/4.0/）。 ✨ 这是对下方论文的AI生成解释。它不是由作者撰写或认可的。如需技术准确性，请参阅原始论文。阅读完整免责声明

想象一下，你正试图为一个在混乱的共享厨房里工作的厨师团队编写一份食谱。每个人都在同时切菜、搅拌和品尝。问题在于，当厨师 A 正在阅读食谱步骤时，厨师 B 可能会溜进来移动食材、改变温度，或者藏起某个工具。这就是**并发编程（concurrent programming）**的世界：多个程序同时运行，互相干扰彼此的数据。

Hayes、Meinicke 和 Jones 的这篇论文就像是一本全新的、极其严格的规则手册，旨在确保这些食谱即使在混乱中也能保证成功执行。他们专注于两种特定类型的烹饪指令：循环（loops）（重复做某事）和递归（recursion）（一个通过调用自身来解决较小部分问题的食谱）。

以下是他们“厨房规则”的简单类比拆解：

1. “依赖-保证”（Rely-Guarantee）契约

在普通的厨房里，你可能只是默认没人会碰你的锅。在这篇论文中，作者说：“仅仅信任是不够的。我们需要一份合同。”

依赖条件（“不要碰”清单）： 在开始任务之前，你假设其他厨师会遵守某些规则。例如，“我依赖于‘在我品尝汤的时候没有人往里面加盐’这一事实。”
保证条件（“我承诺”清单）： 作为回报，你也承诺会遵守规则。例如，“我保证我绝不会把勺子扔向墙壁。”
神奇之处： 如果每个人都遵守各自的“依赖”和“保证”契约，即使大家都在同时工作，整个厨房也会运行得非常顺畅。

2. 关于“原子性”（Atomic）假设的问题

许多旧的规则手册假设当厨师阅读食谱步骤时，它是瞬间完成的，就像打了一个响指一样。它们假设厨师读到“加入 2 个鸡蛋”后，会在其他人眨眼之前就完成加蛋动作。

作者说：“不，现实中的厨房不是这样运作的。”
在现实中，阅读“加入 2 个鸡蛋”是需要时间的。在厨师伸手去拿鸡蛋的过程中，另一位厨师可能已经把蛋盒挪动了位置。这篇论文构建的规则考虑到了这种混乱的现实。它们不假设任何事情都是瞬间发生的；它们假设一切都需要时间，并且可能会被中断。

3. 驯服“While”循环（永不停歇的搅拌）

“While 循环”就像是一个厨师在搅拌一锅酱料“直到酱汁变浓为止”。

旧有的问题： 在共享厨房里，厨师可能会搅拌、检查酱汁，然后决定酱汁还没变浓。但在他走向炉灶的过程中，另一位厨师可能加入了水，导致酱汁又变稀了。第一个厨师可能会永远搅拌下去，或者在不该停止的时候停止。
新规则（提前终止）： 作者引入了一个聪明的技巧，叫做**“提前终止”（Early Termination）**。
- 想象厨师有一个计时器（一个“变体/variant”）。每当他们搅拌一次，计时器就会减少。
- 通常情况下，厨师必须通过搅拌来让计时器减少。
- 转折点： 如果另一位厨师不小心加了水（干扰），计时器可能会比预期下降得更快，或者酱汁可能突然变得足够浓稠，以至于循环应该停止。
- 新规则允许循环提前停止，如果环境（其他厨师）帮助完成了这项工作，而不是强迫循环本身完成所有工作。这就像是在说：“如果因为别人帮忙，酱汁已经变浓了，你可以立即停止搅拌。”

4. 驯服递归（调用自身的食谱）

递归就像是一个厨师说：“为了做这锅大炖肉，我需要先做一个小份的清汤。为了做这个清汤，我需要先做一点点高汤……”

挑战： 在共享厨房里，如果厨师 A 正在制作清汤，厨师 B 可能会偷走那个高汤锅。
解决方案： 作者创建了一个数学上的“阶梯”（良基关系/well-founded relation）。想象厨师正在通过解决越来越小的子问题来向下爬楼梯。
- 规则： 你只能在确定自己不会被卡住的情况下向下爬。
- “提前退出”技巧： 就像对待循环一样，如果其他厨师帮你更快地到达了阶梯底部（通过为你解决了子问题），你被允许提前停止向下爬。你不需要强迫自己完成每一个步骤，如果环境帮你完成了任务。

5. “Aczel Trace”（厨房监控摄像头）

为了证明他们的规则有效，作者使用了名为 Aczel trace 的概念。

想象一个记录厨房情况的监控摄像头。
摄像头记录两种类型的动作：程序动作（你正在观察的那个厨师所做的动作）和环境动作（其他厨师所做的动作）。
作者的规则确保，无论摄像头记录下的混乱情况如何，只要遵守了“依赖”和“保证”契约，最终的成品一定是完美的。

总结

这篇论文为同时运行的计算机程序提供了一种全新的、稳健的编写指令的方法。

拒绝魔法： 它不再假设事情是瞬间发生的。
契约管理： 它使用“依赖”和“保证”来管理程序的交互。
灵活性： 它允许循环和递归函数在环境帮助其完成任务时提前结束，从而防止它们陷入死循环或因受到干扰而失败。

作者已经使用计算机证明助手 Isabelle/HOL 测试了这些规则，这个助手就像一位超级严厉的数学老师，检查每一个步骤以确保逻辑无懈可击。他们不仅仅是猜测；他们证明了这是行得通的。

技术摘要：基于 Rely-Guarantee 规则的并发循环与递归推理

问题陈述

并发程序的验证，特别是涉及递归结构和 while 循环的部分，在处理来自并行线程的干扰时面临着重大挑战。传统的用于循环的 Hoare 式验证规则依赖于不变式（invariants）和变体表达式（variant expressions）来证明正确性和终止性。然而，在并发环境下，干扰可能会使循环不变式失效、增加变体表达式或破坏循环条件的评估，从而导致标准的顺序执行规则失效。

此外，许多现有的 Rely-Guarantee (RG) 方法假设表达式的求值是原子的。这种假设并不反映编程语言实现的现实情况，因为表达式可能涉及对共享变量的多次访问，而这些访问可能与环境转换交织在一起。这种原子性假设破坏了复杂表达式的正式推理链，并限制了验证规则的适用性。

方法论

作者开发了一个在 Rely-Guarantee 背景下对递归程序和 while 循环进行推理的框架，该框架基于一个基于完全分配格（complete distributive lattice）的命令宽谱语言。该方法论基于以下核心组件：

Aczel Trace 语义： 语义模型使用 Aczel trace 集，记录程序转换 ( $\pi$ ) 和环境转换 ( $\epsilon$ ) 的序列。这允许在不假设表达式赋值命令为原子性的情况下，对干扰进行组合式处理。
Rely-Guarantee 条件： 框架使用 rely 条件 ( $r$ ) 来约束环境的行为，并使用 guarantee 条件 ( $g$ ) 来约束程序的行为。一个线程的保证必须隐含所有并行线程的 rely 条件。
不动点理论： 递归程序被定义为命令格上的不动点。作者开发了用于推理这些不动点的法则，特别是在利用基于变体表达式和关系的良基归纳法（well-founded induction）来证明终止性方面。
早期终止（Early Termination）： 一个核心的方法论创新是为递归和循环开发了“早期终止”版本的法则。不同于要求函数体在任何递归调用之前必须严格减少变体的标准方法，这些法则允许函数体要么减少变体，要么建立一个条件（基本情况/base case），以确保不再进行进一步的递归调用。这对于并发至关重要，因为干扰可能会以一种使得函数体无法减少变体的方式来减少变体，但仍能确保终止。
非原子表达式求值： 该方法显式处理了表达式的非原子求值。它通过分析子表达式来建立复杂表达式和守卫（guards）的后置条件，从而实现组合式推理，避免了需要“单一关键引用”等语法限制的原子假设理论。

核心贡献

论文提出了对并发程序验证理论的几项具体贡献：

递归的一般精化规则： 定理 5 ("recursion-early") 提供了一个引入递归的规则，该规则能够容纳干扰。它使用良基关系和变体表达式，允许即使变体是由环境而非函数体减少时也能证明终止，只要建立了基本情况即可。
While 循环的一般精化规则： 定理 6 ("intro-while") 基于递归法则推导出了引入 while 循环的法则。它包含一个“早期终止”条件 ( $p_X$ )，允许循环在由于干扰导致守卫评估为假时退出，即使循环体并未严格减少变体。
处理非原子表达式： 该框架提供了推理规则（例如定理 2 关于条件判断，定理 3 关于函数调用），允许在不假设原子求值的情况下，对存在干扰的表达式和守卫进行组合式推理。
形式化验证： 论文中呈现的所有引理和定理都已使用 Isabelle/HOL 定理证明器进行了机械化验证。
公平终止（Fair Termination）： 论文讨论了公平终止，定义了一个 fair 命令，该命令不允许出现无限连续的环境转换序列，并展示了如何证明一个命令在公平执行下仅执行有限次转换。

结果与示例

论文通过两个主要示例展示了所开发法则的效用：

并行递归搜索： 开发了一个递归搜索算法，用于在范围 $[0, N)$ 中寻找满足谓词 $P$ 的值 $i$ 。该实现采用了分治策略，包含并行递归调用。证明过程利用了 "recursion-early" 法则来处理并发线程可能已经找到解（设置了 found 标志）的情况，从而允许递归调用在无需进一步处理的情况下提前终止。
带有 CAS 的原子更新： 一个使用 Compare-And-Swap (CAS) 指令将变量 $m$ 更新为 $\min(m, lo)$ 的原子规范实现示例。循环重复尝试 CAS 操作。这里的“早期终止”版本循环法则至关重要：如果如果在守卫检查与 CAS 执行之间，干扰使 $m$ 减小到低于 $lo$，则 CAS 可能无法减少 $m$ （即变体）。然而，循环会因为守卫 ($lo < m$) 变为假而终止。标准的循环法则在此场景下会无法证明终止，但所提议的法则通过识别早期退出条件成功完成了证明。

意义与主张

作者声称，其工作为在并发存在的情况下对递归和循环进行推理提供了通用的、经过机械化验证的精化规则。这项工作的意义在于：

消除原子性假设： 通过不假设表达式求值是原子的，这些规则适用于更广泛的现实编程场景，并避免了依赖原子性的理论中出现的逻辑链断裂问题。
在终止性证明中处理干扰： “早期终止”法则解决了并发验证中的一个特定空白，即干扰可能使标准的终止论证失效。这使得验证那些由环境行为促成终止条件的程序成为可能。
组合式开发： 该方法支持共享变量并发程序的组合式开发，允许根据其 rely 和 guarantee 条件独立地设计和验证线程。
形式化严谨性： 研究结果不仅是理论上的提议，而且已在 Isabelle/HOL 定理证明器中进行了形式化和验证，确保了其逻辑上的完备性。

该论文将自身定位为以往代数化 Rely-Guarantee 研究的扩展，特别针对并发系统中由递归、循环和非原子表达式求值引入的复杂性。它并不声称要取代像并发分离逻辑（CSL）这样的其他逻辑，而是提供了一种替代的组合式方法；作者特别指出，虽然 CSL 支持关于无竞争（race-free）的推理，但 RG 旨在开发“有竞争”的程序（即通过 rely/guarantee 条件管理竞争的程序）。