💻 computer science

Recursive Mutexes in Separation Logic

本文将标准互斥锁的 separation logic 规范扩展到了递归互斥锁，针对同一线程多次获取和释放锁的行为，基于客户端是否持有该锁，提供了统一的处理方式。

原作者： Ke Du, William Mansky, Paolo G. Giarrusso, Gregory Malecha

发布于 2026-02-02

📖 1 分钟阅读☕ 轻松阅读

原作者： Ke Du, William Mansky, Paolo G. Giarrusso, Gregory Malecha

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

想象一下，你是一位非常繁忙、高安全性保险库的管理员。在计算机编程的世界里，这个保险库就是一个 互斥锁（mutex），而里面珍贵的物品就是多个线程（人）可能想要修改的数据。

问题所在：“一次性”锁

在标准的编程中，对于这个保险库有一条规则：如果你已经拿着钥匙在里面了，你就不能再次上锁。

想象一下，你正在保险库里修理一个保险箱。你需要走出保险库去走廊拿一个工具，但你不能直接走出去，因为你必须锁上门以防他人进入。如果你在已经持有钥匙的情况下尝试再次上锁，系统就会崩溃或冻结。这就是一个“非递归”互斥锁。它非常严格：你要么拥有这把锁，要么不拥有。你不能重新进入你已经处于“锁定”的状态。

解决方案：“递归”锁

这篇论文介绍了一种 递归互斥锁（recursive mutex）。你可以把它想象成一把神奇的钥匙，它允许你在已经持有钥匙的情况下再次上锁。

运作方式： 如果你在保险库内部，并且需要再次锁定门（例如，你需要调用一个同样需要保证安全性的辅助函数），你可以这样做。系统不会惊慌失措，它只会记录你上锁了多少次。
代价： 你必须解锁与上锁次数相同次数的门，才能最终让门重新开启，让其他人进入。

挑战：证明其安全性

作者们（Du, Mansky, Giarrusso, 和 Malecha）正在使用一种叫做 分离逻辑（Separation Logic） 的数学系统来证明这种“神奇钥匙”的使用是安全的。

通常，证明一个锁是安全的就像是在说：“如果我拿着钥匙，我就能看到里面的宝藏。”
但有了递归锁，事情变得复杂了。如果我已经拿着钥匙，然后我再次上锁，我是不是就能得到两份宝藏？不，那会破坏规则。

论文中的新规则（“计数器”系统）：
与其简单地判断“是/否”拥有钥匙，作者们提出了一个 计数器系统：

计数： 每当你上锁一次，你的个人计数器就会加 1。每当你解锁一次，它就会减 1。
权限： 只要你的计数器 大于零，你就被允许查看宝藏（数据）。
安全性： 数学证明了，即使你上锁了 5 次，你也只能获得一次查看宝藏的权限。你不能仅仅因为上锁了两次就“双重获利”去窃取数据。

给程序员的“魔术技巧”

这篇论文对简化程序员的工作非常有帮助。

在这篇论文之前：
如果一个程序员编写了一个需要上锁的函数，他们必须询问自己：“等等，我现在已经在里面了吗？如果我在里面，我就不能再次上锁。我需要写两个不同版本的代码：一个用于我在里面时，另一个用于我在外面时。” 这既混乱又容易出错。

有了这篇论文之后：
程序员只需要说：“上锁，做我的工作，解锁。”

如果他们之前已经在里面，计数器就会增加，他们完成工作，然后计数器减少。
如果他们之前在外面，计数器会从 0 变为 1，他们完成工作，然后回到 0。

数学保证了在 这两种 场景下，数据都能保持安全和一致。程序员不需要知道锁的历史记录；他们只需要知道，只要他们持有锁（计数器 > 0），就可以安全地操作数据。

“元组（Tuple）”修复

论文还提到了一个涉及“元组”（一种信息分组方式）的小技术修复。
想象一下，宝藏不仅仅是一堆金子，而是特定数量的金子（例如，“500 枚硬币”）。

旧方法： 当你解锁门时，你可能会忘记到底有多少硬币，只记得“那里有一些金子”。
新方法： 作者的系统确保了特定的硬币数量（参数）会始终附着在你的锁计数上。即使你多次上锁和解锁，你也永远不会丢失你所保护的数据的精确状态。

总结

这篇论文提供了一套新的数学规则，用以证明 递归锁（即你可以持有并再次上锁的锁）是安全的。它允许程序员编写更简洁、更自然的代码，而不必担心自己是否已经在“锁定”区域内，因为系统会自动追踪门被锁定的次数，并确保内部的数据保持受保护且一致的状态。

技术摘要：分离逻辑中的递归互斥锁

问题陈述
虽然机械化的并发分离逻辑（mechanized concurrent separation logic）在验证 C++ 和 Rust 等语言的真实世界程序方面已取得了显著进展（例如使用 VST、BRiCk 和 RustBelt 等工具），但在标准并发库的形式化验证方面仍存在空白。具体而言，递归互斥锁（在 C++ 和 Java 中很常见）缺乏建立好的分离逻辑规范。与标准互斥锁（线程在已持有锁的情况下无法再次获取）不同，递归互斥锁允许单个线程多次获取同一个锁。这种能力支持了惯用的代码模式，即持有锁的函数可以安全地调用同样尝试获取该锁的另一个函数（例如图 1 中的 transfer 调用 update_a）。标准互斥锁规范无法支持这种透明性和封装性，往往迫使开发者创建非加锁的替代函数，或进行复杂的案例分析来处理锁的所有权。

方法论
作者提出了一种新的递归互斥锁分离逻辑规范，该规范无论调用线程当前的持有状态如何，都统一处理锁的获取与释放。该方法引入了两个主要组件：

分数句柄与线程特定谓词：
- 一个具有不变式 $P$ 的递归互斥锁 $\gamma$ 与一个分数句柄 $\ell \mapsto_q \text{rmutex}(\gamma, P)$ 相关联。
- 至关重要的是，每个与该互斥锁交互的线程 $t$ 都拥有自己的谓词： $\text{holds}(\gamma, t, n, P)$ 。这里， $n$ 代表线程 $t$ 获取该互斥锁的次数。
- 互斥是通过以下规则强制执行的：如果两个线程持有该互斥锁，则至少其中一个必须持有计数为零（ $n_1 = 0 \lor n_2 = 0$ ）。
- 为了防止单个线程“双重计数”资源，逻辑规定一个线程不能同时持有两个 $\text{holds}$ 谓词；因此， $\text{holds}(\gamma, t, n_1, P) * \text{holds}(\gamma, t, n_2, P) \vdash \text{False}$ 。
状态转换与借用：
- 加锁/解锁： 获取锁会增加线程的计数 $n$ ( $n \to n+1$ )，释放锁会减少 $n$ ( $n \to n-1$ )。
- 借用规则： 当且仅当线程的计数 $n > 0$ 时，该线程才能访问受保护的不变式 $P$ 。该规则允许线程将 $\text{holds}(\gamma, t, n, P)$ （其中 $n>0$ ）交换为实际的资源 $P$ 以及一个用于追踪计数的保留项 $\text{held}(\gamma, t, n)$ ，后者并不授予对 $P$ 的访问权。
- 处理量化参数： 为了解决锁不变式中包含存在量化变量（例如 $\exists v. x \mapsto v$ ）的问题，作者引入了一个传递给 $\text{holds}$ 谓词的参数元组 $a$ 。这确保了当线程借用 $P$ 时，它保留了关于资源的特定知识（例如变量的具体值），而不是在返回不变式状态时重新量化并丢失这些信息。

核心贡献

统一规范： 本文提供了一种规范，允许客户端仅通过检查其计数 $n$ 是否大于零来确定是否持有互斥锁，而无需区分是“首次”获取还是“递归”获取。
惯用推理： 这些规范支持了如下代码模式的证明：即持有同一把锁的函数调用另一个同样获取该锁的函数，这镜像了标准的 C++ 用法，而无需专门的“无锁”版本函数。
C++ 并发的形式化验证： 该工作展示了利用这些规范在 BRiCk 框架下验证 C++ 并发库（特别是 std::recursive_mutex）的应用。

结果
作者成功应用这些规范验证了图 1 中的示例，其中 transfer 函数在持有同一递归互斥锁的同时调用了 update_a 和 update_b。验证确认了：

transfer 函数即使在两者都获取相同互斥锁的情况下，也能安全地复用 update_a。
不变式（balance_a 与 balance_b 之和）在操作过程中得到了保持。
逻辑正确处理了线程最初持有或未持有锁时的不变式状态，并在调用栈中保留了特定的变量值（如 $a$ 和 $b$ ）。

意义
论文声称，与使用普通互斥锁相比，这些规范使得对递归互斥锁的推理“更加透明且具有更好的封装性”。通过将获取锁（增加 $n$ ）与借用不变式（当 $n>0$ 时访问 $P$ ）的操作分离，该方法支持了主流语言中常见的软件工程模式。这项工作被视为验证整个 C++ 标准库这一更宏大目标的一步，旨在强调对现实世界并发编程具有实用性的推理原则。作者指出，他们目前的规范同时也涵盖了其他标准库组件，如 std::atomic 和 std::vector。