2015 Iris 迷案：並行程式的幽靈證據與分離邏輯#

報案人：並行程式設計師。案情：多執行緒一跑就崩，鎖對了還是錯，傳統 Hoare 邏輯束手無策。偵探：Ralf Jung、Jacques-Henri Jourdan、Robbert Krebbers、Derek Dreyer 團隊。兇器：Iris 高階並行分離邏輯。

案發現場#

2015 年之前，並行驗證是一樁著名的懸案。1969 年的 Hoare 邏輯擅長循序程式，但一遇到並行就失靈：兩個執行緒同時讀寫共享記憶體，斷言會被對方悄悄改掉，證明根本寫不下去。

2002 年，Reynolds 與 O'Hearn 提出了分離邏輯（separation logic），引入了分離合取 \(P * Q\) ，表示堆積可以拆成兩個不相交的部分，分別滿足 \(P\) 與 \(Q\) 。這讓模組化推理成為可能，卻仍不足以對付細粒度並行、弱記憶體模型與高階函數的組合技。

更棘手的是，當時的並行邏輯各自為政： concurrent separation logic、CAP、FCSL、GPS，每種邏輯都有自己的 soundness 證明，互不相容。研究者每發明一種新推理模式，就要重建一次元理論，猶如每破一案就要重建一間警局。

2015 年，Jung 等人在 POPL 發表了 Iris 1.0，口氣不小：不要再發明新邏輯了，來用一個能吞掉所有邏輯的邏輯。這就是 Iris——以希臘彩虹女神為名的「邏輯中的邏輯」。

偵查過程#

線索一：分離合取 \(P * Q\) 與框架規則#

分離邏輯的核心直覺是「擁有的才可言說」。命題 \(l \mapsto v\) 表示執行緒獨佔了位址 \(l\) 且其值為 \(v\) 。而 \(P * Q\) 斷言堆積可分割為兩塊不交部分，各自成立。

最關鍵的推理規則是框架規則（frame rule）：

\[ \frac{\{P\} e \{Q\}}{\{P * R\} e \{Q * R\}} \]

它說：若程式 \(e\) 在小堆積 \(P\) 上能從 \(Q\) 結案，那麼把它放進更大的堆積 \(P * R\) 裡，旁觀者 \(R\) 不受干擾。這正是模組化的靈魂。

Iris 把這套思想推向高階：命題可以談論命題，斷言可以存放在堆積裡（impredicative invariants），從而支援函數式語言的閉包、遞迴型別與高階並行抽象。

線索二：Step-indexed 模型與 Ghost State——幽靈證據#

Iris 最精妙的偵查手法是「幽靈狀態」（ghost state）：在證明中虛構一些只存在於邏輯世界、不影響執行的輔助資源，用來記錄協議、歷史與權限。

例如，要證明一個並行計數器，偵探可以虛構一個單調遞增的幽靈計數 \(\gamma\) ，讓每個執行緒的貢獻都有據可查，即使實體記憶體只有一個整數格。

為了讓這種自指結構不陷入悖論，Iris 採用步進索引（step-indexed）模型：所有斷言都按「還剩多少步可觀察」分層， \(n + 1\) 層的真理只能依賴 \(n\) 層的真理。後模態（later modality） \(\triangleright P\) 精確捕捉了這層延遲：

\[ \triangleright P \vdash P \quad \text{在一步之後成立} \]

而不變式（invariant） \(knowInv(N, P)\) 則表示：命題 \(P\) 是一個可被多執行緒共享、但每次只能短暫打開的不變知識。打開與關閉的規則大致是：

\[ knowInv(N, P) * ownGhost(\gamma) \vdash \triangleright P * closeRule \]

偵探憑「搜查令」暫時借出 \(P\) ，用完必須原樣歸還，否則證據鏈斷裂。這套機制統一了鎖、屏障、讀寫協議等所有並行模式。

線索三：Iris Proof Mode 與 RustBelt——從理論到實戰#

再漂亮的邏輯，沒有好用的審訊工具也是白搭。Iris 團隊在 Coq 上打造了 Iris Proof Mode（IPM），讓分離邏輯證明寫起來像日常 tactic：

iIntros "[Hl Hk]".
iSplitL "Hl".
- iApply "Hl".
- iFrame "Hk".

其中 \(iIntros\) 引入分離假設， \(iSplitL\) 拆分擁有權， \(iFrame\) 自動消去框架部分。符號 \(*\) 的管理從此半自動化，證明長度驟減。

Iris 的代表作是 RustBelt（2017 起）：用 Iris 為 Rust 的型別系統建立語意模型，證明了 safe Rust 的記憶體安全，以及 Cell、Rc、Arc、Mutex 等不安全底層庫的封裝正確性。Rust 的所有權型別 \(&mut T\) 在 Iris 中被解釋為獨佔資源 \(l \mapsto v * ghostTok\) ，借用檢查器從此有了數學背書。

下表總結了 Iris 破獲的連環案件：

案件	傳統方法	Iris 解法
細粒度並行計數器	推理爆炸	幽靈計數＋不變式
讀寫鎖	臨時發明新邏輯	通用協議即 ghost state
Rust 生命週期	僅靠編譯器測試	RustBelt 語意模型
弱記憶體	另起爐灶	Iris 參數化即可容納

結案報告#

Iris 在 2015 年立案，此後每年升級（Iris 2.0、3.0、4.0），至今仍是並行驗證的頭號偵探社。它的結案意義有四：

邏輯的大一統：證明了絕大多數並行分離邏輯都可以嵌入同一個框架，終結了諸侯割據。
機械化元理論：Iris 自身的可靠性在 Coq 中完整驗證，偵探的手銬本身也被檢查過。
征服 Rust：RustBelt 讓 Iris 從學術走向工業，成為 Mozilla 與 Rust 基金會都關注的驗證後盾。
方法論遺產：ghost state ＋ invariants ＋ step-indexing 的三件套，成為後來所有並行邏輯教材的標準配備，也影響了 Lean 與 AI 時代的程式驗證。

用探案的話說：Iris 沒有只破一樁兇殺案，它端掉的是整個並行犯罪集團的保護傘。

證據與工具#

證據一：分離邏輯基本規則表

規則	形式
框架	\(\{P\} e \{Q\} \Rightarrow \{P * R\} e \{Q * R\}\)
並行組合	\(\{P_{1}\} e_{1} \{Q_{1}\}, \{P_{2}\} e_{2} \{Q_{2}\} \Rightarrow \{P_{1} * P_{2}\} e_{1} \parallel e_{2} \{Q_{1} * Q_{2}\}\)
存取	\(\{l \mapsto v\} !l \{w. w = v * l \mapsto v\}\)
更新	\(\{l \mapsto v\} l := w \{l \mapsto w\}\)

其中 \(e_{1} \parallel e_{2}\) 表示並行執行， \(l \mapsto v\) 是獨佔指向斷言。

證據二：Iris Proof Mode 片段

Lemma counter_incr (l : loc) (n : nat) :
  {{{ l ↦ #n }}} incr l {{{ RET #(); l ↦ #(n + 1) }}}.
Proof.
  iIntros (Φ) "Hl HΦ".
  wp_lam. wp_load. wp_op. wp_store.
  iApply "HΦ". iFrame.
Qed.

這裡的三段式 \(P\) 、 \(e\) 、 \(Q\) 是 Hoare 三元組的 Iris 版本， \(↦\) 即分離擁有， \(wp\) 是 weakest precondition 策略。

證據三：偵探工具箱

工具	作用
Coq ＋ Iris 函式庫	高階並行邏輯本體與可靠性證明
Iris Proof Mode	分離邏輯專用 tactic 方言
RustBelt	Rust 安全性的語意模型大案卷宗
Perennial / GoJournal	Iris 在分散式系統的後續追擊

延伸閱讀：Jung et al., "Iris: Monoids and Invariants as an Orthogonal Basis for Concurrent Reasoning"（POPL 2015）；Jung et al., "RustBelt: Securing the Foundations of the Rust Programming Language"（POPL 2018）。