兩種編排草案一 · 現行草案二 · 新編排講課版自動生成圖解版

Abstractions from Proofs — 圖解版

原文：POPL 2004 · doi:10.1145/982962.964021 · 開啟原文 PDF ↗

1 這是在解什麼問題

這支程式是對的：每個 `lock()` 後面都緊跟著條件相同的 `unlock()`。

Figure 1, p.233
Figure 1, p.233

但驗證器會誤報——右欄就是它找到的那條路徑：進第一個 `if` 上鎖，不進第二個 `if`，於是沒解鎖。

Figure 1 右欄即論文畫出的誤報路徑, p.233
Figure 1 右欄即論文畫出的誤報路徑, p.233

停一下：驗證器要記住什麼事實，才知道這條路走不通？

``` 1: if (p1) lock(); ← 進去了 if (p1) unlock(); ← 卻沒進去？ ```

答案是記住 `p1` 的值：$p_1$ 為真時第一個 `if` 進得去，第二個也一定進得去。兩個條件是同一個。

$$p_1 \text{ 為真} \;\Longrightarrow\; \text{兩個 if 都進} \;\Longrightarrow\; \text{lock/unlock 配成對}$$

但這裡有 $n$ 個這樣的 `if`。全部都記，狀態就有 $2^n$ 種組合。

$$n = 30 \;\Longrightarrow\; 2^{30} \approx 10^9$$

而 $p_1$ 這個事實只在標籤 1 到 2 之間有用。過了標籤 2，那對 lock/unlock 已經配好，它再也用不到。

``` 1: if (p1) lock(); ┐ if (p1) unlock(); ┘ p1 只在這段有用 2: if (p2) lock(); ← 這之後 p1 是死的 ```

所以真正的問題不是「要記住哪些事實」，而是——哪些事實，該在哪個程式位置記住？

2 這個問題為什麼值得解

predicate abstraction：不追蹤變數的數值，只追蹤一組是非問句的真假——無限狀態因此變成有限。

$$\text{無限多個狀態} \;\xrightarrow{\;p_1, p_2, p_3\;}\; \text{最多 } 2^3 = 8 \text{ 種}$$

那組 predicate 從哪來？標準做法是 CEGAR 迴圈：粗略抽象 → 找錯誤路徑 → 檢查是不是誤報 → 加 predicate 再來。

1用少量 predicate做粗略抽象2在抽象上找通往 ERROR 的路徑3找不到 → 安全4路徑翻成公式丟給 solver5有解 → 真的 bug6無解 → 誤報加新的 predicate這一步「加哪些 predicate」就是 POPL’04 要回答的問題
示意圖（自製，非論文原圖）

難的全部集中在第 6 步那幾個字：「加入新的 predicate」。 加哪些？加多少？加在哪裡？

1用少量 predicate做粗略抽象2在抽象上找通往 ERROR 的路徑3找不到 → 安全4路徑翻成公式丟給 solver5有解 → 真的 bug6無解 → 誤報加新的 predicate這一步「加哪些 predicate」就是 POPL’04 要回答的問題
示意圖（自製，非論文原圖）

3 前人做到哪裡

第 4 步「翻成公式」只有兩條規則，而它建立了整個領域的地基：路徑走得通 ⟺ 公式有解。

```c int x = 1; int y = x + 1; if (y < 0) { ERROR; } ```

$$x = 1 \;\wedge\; y = x + 1 \;\wedge\; y < 0$$

但直接翻會出錯：$x = x+1$ 永遠是假的。程式的 `x` 是會變的盒子，數學的 $x$ 是固定的值。

$$\text{錯：} \; x = 1 \wedge x = x+1 \qquad\qquad \text{對：} \; x_1 = 1 \wedge x_2 = x_1 + 1$$

前人的做法有兩個毛病：數量爆炸，以及位置放錯——找到的 predicate 被一視同仁撒到許多、甚至全部的程式位置。

毛病後果
$p_1 \dots p_n$ 全要追蹤$2^n$ 種抽象狀態
撒到所有位置$p_1$ 被帶到它早就沒用的地方

論文要的是 parsimonious：在每個控制位置，只指定當下變數之間的關係，而且只留證明正確性真正需要的那些。

if at each control location, it specifies only relationships between current values of variables, and only those which are required for proving correctness

4 這篇的解法

洞察：一條路走不通的理由，已經編碼在「它走不通」的證明裡了——不要猜，去讀那份證明。

the reason why an abstract trace is infeasible is succinctly encoded in a proof that the trace is infeasible

interpolant 是切點兩側之間的那個公式 $\psi$，要滿足三個條件——其中第 3 條才是關鍵。

  1. $\varphi^- \Rightarrow \psi$
  2. $\psi \wedge \varphi^+$ 無解
  3. $\psi$ 只用兩邊共同的符號

第 3 條逼出了我們要的東西：共同符號 = 執行到切點時各變數當下的值 = 那個位置需要記住的事實。

前半段 φ⁻（已經走過的）後半段 φ⁺（還沒走的）切點符號：x₀ x₁ ctr₀ ctr₁符號：x₁ ctr₁ y₂ m₀共同符號：x₁、ctr₁共同符號 = 執行到切點時各變數當下的值 = 這個程式位置需要記住的事實
示意圖（自製，非論文原圖）

但貢獻不是「用了 interpolation」——Craig 的定理是 1957 年的，而且它只保證 interpolant 存在，沒說怎麼算。

[9] W. Craig. Linear reasoning. J. Symbolic Logic, 22:250–268, 1957.

（論文自己的參考文獻）

真正的貢獻是一套可以機械執行的推導規則：四條規則產生反駁證明，再把每條改寫成帶插值的版本。

Figure 3, p.235
Figure 3, p.235

帶插值的規則長這樣。方括號同步累積，推到矛盾時裡面剩下的就是 interpolant——不用猜，不用事後驗證。

$$(\varphi^-, \varphi^+) \vdash \Delta \;[\psi]$$

第二個洞察：沿路徑每個切點都切一次，於是得到一張「每個位置一份清單」的表，而不是一包全域 predicate。

$$\text{全域 382 個} \quad\longrightarrow\quad \text{每個位置平均 7.2 個}$$

5 案例

論文的主例：這條路徑走不通，因為 $x$ 抄舊的 `ctr`、$y$ 抄新的，所以必然 $y = x+1$，與第 5 行矛盾。

Figure 2, p.234
Figure 2, p.234

注意第 5 列的約束印成等號——但指令是 `assume(y ≠ m+1)`，而同一頁明說這些約束的合取無解。原文 typo。

Figure 2, p.234
Figure 2, p.234

在第 2 行後面切一刀：兩邊的共同符號是 $\langle x,1 \rangle$ 和 $\langle \mathit{ctr},1 \rangle$——正好是「執行完前兩行後的值」。

前半段 φ⁻（已經走過的）後半段 φ⁺（還沒走的）切點符號：x₀ x₁ ctr₀ ctr₁符號：x₁ ctr₁ y₂ m₀共同符號：x₁、ctr₁共同符號 = 執行到切點時各變數當下的值 = 這個程式位置需要記住的事實
示意圖（自製，非論文原圖）

算出來的 interpolant 翻回程式變數是 $x = \mathit{ctr} - 1$。位置 2 要記的不是任何一個變數的值，是它們的差。

$$\psi_2 = (\langle x,1 \rangle = \langle \mathit{ctr},1 \rangle - 1) \quad\longrightarrow\quad \hat\psi_2 = (x = \mathit{ctr} - 1)$$

換你算：照規則推一次，方括號裡的東西會自己累積成 interpolant。

Figure 4, p.237
Figure 4, p.237

做完有個陷阱：$y$ 消失是國中代數消去，但「保證只含共同變數」靠的是整套規則維持的不變量。兩件事。

問題答案
$y$ 在哪消失？兩個不等式相加，$-y$ 與 $+y$ 抵銷
為何保證只含共同符號？Invariant 1、2，不是代數消去

6 實驗：他們比了什麼

實驗比的是三組設定，同一個工具、同一批 Windows 驅動、同一台機器——變因控制得很乾淨。

Table 1, p.244
Table 1, p.244

最直接的結果：舊方法在最大的兩支上六小時跑不完（`-`），兩個新設定都跑完了。

Table 1, p.244
Table 1, p.244

但看 `Disc` 欄會發現怪事：Craig+Locality 的總時間反而更慢（floppy 25m20s vs 7m56s）。

Table 1, p.244
Table 1, p.244

它贏在 `Reach`——給定所有 predicate 後只做可達性分析，快了將近九倍，因為每個位置只帶 7 個而不是 382 個。

Table 1, p.244
Table 1, p.244
CraigCraig+Locality
floppy3m21s0m46s
parclass9m1s1m6s

而他們沒有比的東西同樣要看見：沒跟其他工具比、記憶體只有文字沒有數字、benchmark 全是同一類程式。

  • 沒有 SLAM 或任何外部系統的數字
  • 「記憶體顯著較少」沒有進表格
  • 「後續執行更快」也沒有數字
  • 全部是 Windows 驅動，性質是同一個 22 狀態自動機

7 怎麼讀原文

帶走的其實是一組動作，不是這篇論文的結論。

  • 看到定義 → 先找反例（拿掉這條會怎樣）
  • 看到定理 → 先問它排除了什麼
  • 看到表格 → 先找沒有比較的那一格
  • 看到「快 N 倍」 → 先問變因控制了幾個
  • 讀不懂 → 先確認是不是自己錯了；真的對不上，原文也可能有 typo

回到最初：哪些事實，該在哪個程式位置記住？ 答案是去讀那份「走不通」的證明，共同符號就是答案。

$$\text{全域 } 382 \text{ 個} \qquad\text{對}\qquad \text{每個位置 } 7.2 \text{ 個}$$