Iris 2015 — 把并发推理拆成 monoid + invariant 两块积木

是什么

Iris 是一套证明并发程序对不对的”积木系统”。它做的事是：把以前每个并发场景（锁、通道、原子操作、消息队列）都得现搭一套证明规则的痛苦，浓缩成两块基础积木——monoid（可组合的资源）+ invariant（共享不变式）——其它一切高级抽象都从这两块拼出来。

日常类比：以前每修一种家具都得新发明一种螺丝，Iris 说”其实只要标准化的螺丝 + 螺帽两种，所有家具都能拼”。

注意 Iris 不是 Rust 专用，也不是某个具体程序——它是一套数学逻辑 + 一份 Coq 形式化实现。

为什么重要

不理解 Iris，下面的事说不清：

为什么 RustBelt（POPL 2018）能给 Rust 的 unsafe 代码做出第一个机械化安全证明——它的底座就是 Iris
为什么 2015 之后，所有证明并发数据结构、内核片段、锁实现的论文都开始往一个工具上汇——之前每篇论文都得自造一套 logic
为什么”分离逻辑”从 2007 年的小众理论变成形式化主流——Iris 把它做成了能扩展、能机器检查、能复用的工程产品

核心要点

Iris 的核心思想可以拆成三步：

挑两个最小原语：monoid（用户自定义的、可组合的资源）+ invariant（线程间共享的契约）。
其它全部派生：锁 = invariant + token monoid；通道 = invariant + 消息列表 monoid；fork/join = invariant + barrier monoid。logic 本体不再 hard-code 这些。
机械化：整个 logic 在 Coq 里完整形式化。用户写自己的 monoid 就能拿到完整证明工具链。

这种”最小核心 + 用户派生”的设计哲学，是 Iris 之所以替代了之前十几个分离逻辑变体（CSL / RGSep / CAP / iCAP / HOCAP / TaDA）的原因。

实践案例

案例 1：ghost state 是什么——洗碗黑板

你和朋友合租，门口黑板写”今天谁洗碗”。这个黑板不影响饭菜本身（程序运行结果不变），但影响你们关于”谁该干活”的证明。

Iris 的 ghost state 就是这种黑板：不出现在程序里，只出现在证明里。logic 给你一条规则 own(a)，意思是”我手里持有 monoid 元素 a”。

为什么必须是 monoid？因为多线程同时改黑板时，必须有”两人各写一半再合并”的合法运算——这正是 monoid 的 · 算子。

案例 2：fractional permission 是什么 monoid

读写锁里常用的”读权限可以分裂、写权限独占”，在 Iris 里就是一个具体的 monoid：

元素：Q ∩ [0, 1] 里的有理数
合并：加法
1.0 = 全权限（可写）；0.5 + 0.5 = 1.0；任意 < 1 = 只读
合法条件：合起来 ≤ 1

own(0.5) * own(0.5)  -*  own(1.0)   // 两个读权限合成写权限
own(1.0)             -*  own(0.5) * own(0.5)   // 写权限分两份

这一套之前是每个分离逻辑变体内置的，Iris 让用户自己挑 monoid 就能得到。

案例 3：invariant 是图书馆

invariant 写作 ⌜I⌝，意思是”不变式 I 在共享区域里恒成立”。日常类比：图书馆”所有书必须按编号排列”。

任何线程在原子步骤内可以打开 I（看一眼或临时打乱）→ 修改 → 关回去（必须再次满足 I）。多个线程都能拿到 ⌜I⌝ 的副本（duplicable），所以可以共享。

锁就是这么实现的：定义 invariant”如果 lock_bit = 0 则资源 R 在内”。线程 acquire 时打开 invariant、把资源拿走、置 lock_bit = 1、关回（此时 invariant 自动满足，因为前提变假了）。

案例 4：用同一套规则证锁、证通道、证 RCU

证锁：invariant 装”锁开 ⇒ 资源在里面”，monoid 装一张”独占票”。证通道：invariant 装”消息列表 = 当前队列状态”，monoid 装”发送了几条 / 收到了几条”。证 RCU（read-copy-update）：invariant 装”旧版本何时可回收”，monoid 装”哪些 reader 还在引用旧版”。

三种结构、三种证明，但底层规则完全相同——之前每证一种都要重写一套 logic，Iris 把这部分公共逻辑一次性抽出。

关键技术词汇（一句话翻译）

术语	一句话说人话
resource algebra	比 monoid 再宽松一点的代数：允许某些组合”非法”，逻辑自动用它推”此分支不可能”
view shift `a V b`	”ghost state 从 a 编辑到 b 的合法权限”
frame rule	”只动我自己的资源 → 别人的状态自动不变”——分离逻辑共同核心
weakest precondition	”要让 e 跑完得到 Q，开始时至少需要哪些资源”——和 Hoare triple 等价但更顺手
atomic triple	”原子操作”专用三元组，从 TaDA 引入，Iris 当作派生品
impredicative	”assertion 里能引用 assertion 自身”，让锁能装任意资源（包括另一把锁）

踩过的坑

Iris 不是 Rust 专用：Iris 是通用的并发分离逻辑。Rust（通过 RustBelt / λRust）只是它最有名的一个应用。学 Iris ≠ 必须懂 Rust。
ghost state 看起来”假”但省不掉：新人觉得”既然不影响运行结果，省了不就行了”。不行——它承载的是证明义务。没有黑板你证不出”我们俩没冲洗”。
monoid 不只是数学，是 API：用户挑 monoid 就是在设计自己的”证明语言”。挑得不好，证明会写得很痛苦。这是 Iris 的工程难点之一。
Iris 高阶 ≠ 慢 ≠ 复杂：高阶（assertion 自身可量化 assertion）让你能用同一套机制证锁、证通道、证 RCU，反而省事。
想直接拿 Iris 验证业务代码？不行：Iris 仍需要专家手写 Coq 证明。它替你提供了”框架和原语”，没替你写出”证明本身”。

适用 vs 不适用场景

适用：

证明并发数据结构（lock-free queue、hazard pointer、RCU）
证明 unsafe Rust 代码的内存安全（RustBelt 路线）
证明锁、通道、futures 等同步原语自己的实现正确
证明操作系统内核片段（CertiKOS-Iris）

不适用：

纯顺序代码（用普通 Hoare logic 或 CSL 已够，Iris 是 overkill）
性能验证（Iris 只证功能正确性，不证延迟、吞吐）
概率程序、分布式共识（需要另外专门的逻辑）
业务代码的 bug 排查（成本太高，不实际）

历史小故事（可跳过）

2007 年：OHearn 提出 Concurrent Separation Logic（CSL），把分离逻辑扩展到并发——这是 Iris 的祖父。
2010-2014 年：CAP / iCAP / HOCAP / TaDA 等十几个变体涌现，每个加一种特性（user-defined region / impredicativity / 高阶 / atomic triple），logic 越来越臃肿，论文之间互不兼容。
2015 年（POPL）：Jung-Swasey 等人发表 Iris 第一版，主张”拆出最小核心 = monoid + invariant”，其它全部派生。
2016 年（ICFP）：Iris 2.0，分成 base logic + program logic 两层。
2018 年（POPL）：RustBelt 用 Iris 给 Rust 做了第一个机械化安全证明，让 Iris 出圈。
2018 年（JFP）：《Iris from the Ground Up》80 页综述发表，相当于教科书化。
现在：Iris 5.x，几乎所有学术界做并发形式化验证的工作都在它上面。

学到什么

设计哲学：“最小核心 + 用户派生” > “把所有需求堆进系统本体”——这一招让 Iris 替代了十几个前辈
ghost state 的本质：让证明能引用”程序里没有但逻辑上必要”的状态
monoid 是资源的代数：可组合资源的最小数学描述，比 heap 更通用
工具化才能复用：理论 + Coq 实现一起开源，才让其它团队真用得上

关联

concurrent-separation-logic —— 2007 年的祖先，Iris 把它工程化
rustbelt —— 用 Iris 证明 Rust unsafe 代码安全的代表作
hoare-logic —— 再上一层祖先，“程序对不对 = 逻辑公式对不对”的源头
linear-types —— “资源观点”的近亲，思想相通
coq —— Iris 的形式化宿主语言

反向链接

certikos-2016 —— CertiKOS — 把整个并发内核拆成 30 多层每层都被 Coq 证过
hoare-logic —— Hoare Logic — 把”程序对不对”变成”数学证明对不对”
linear-types —— 线性类型（Linear Types）