Abstractions from Proofs — 自動投影片

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

1 先自己試一次

下面這支程式是對的。lock() 和 unlock() 嚴格交替，沒有連續上兩次鎖，也沒有解一個沒上的鎖。

while (*) {
1:  if (p1) lock();
    if (p1) unlock();
2:  if (p2) lock();
    if (p2) unlock();
    ...
n:  if (pn) lock();
    if (pn) unlock();
}

但一個自動驗證器很容易在這裡誤報。它會說：「我找到一條路徑，lock() 之後沒有 unlock()。」

那條路徑是這樣走的：進入第一個 if（所以上了鎖），然後不進入第二個 if（所以沒解鎖）。從控制流程上看，這條路徑確實存在。

先停下來想一分鐘：驗證器要記住什麼事實，才會知道這條路徑走不通？

想好了再往下。

好。那現在把問題放大：

這裡有 $n$ 個這樣的 if。 你要記住 $p_1$ 到 $p_n$ 全部嗎？如果每個都是一個布林事實，那狀態就有 $2^n$ 種組合。$n = 30$ 就是十億。

所以真正的問題不是「要記住哪些事實」，而是：

哪些事實，該在哪個程式位置記住？

2 這個問題為什麼值得解

要看懂這篇的位置，得知道它掉在一段什麼樣的歷史裡。

1980 年代，model checking 在硬體驗證上非常成功。 電路的狀態是有限的，可以窮舉。但軟體不行——一個 32 位元的整數變數就有四十億種取值，再加上迴圈、遞迴、heap，狀態空間直接無限。

1997 年前後出現的關鍵想法是 predicate abstraction。 概念很直接：不要追蹤變數的確切數值，只追蹤一組是非問句的真假。

代價是資訊流失：兩個不同的具體狀態可能壓成同一組位元。但這正是我們要的——抽象就是刻意丟掉不重要的細節。難的是決定哪些不重要。

接著的問題是：那組 predicate 從哪來？ 沒有人一開始就知道該選哪些。標準做法是一個叫 CEGAR（counterexample-guided abstraction refinement）的迴圈：

1. 先用很少的 predicate 做一個粗略的抽象
2. 在抽象上找通往 ERROR 的路徑
3. 找不到 → 程式安全，結束
4. 找到了 → 把這條路徑翻成一條數學公式，丟給求解器
5. 公式有解 → 這條路真的走得通，是真的 bug，回報
6. 公式無解 → 這是誤報。加入新的 predicate 讓抽象變細，回到第 2 步

這個迴圈本身不難懂。難的全部集中在第 6 步那幾個字：「加入新的 predicate」。

猜出來的東西有兩個毛病，而那正是下一節的內容。

3 前人做到哪裡

要看懂「前人的毛病」，得先看懂第 4 步在做什麼——那裡有幾個記號，後面整篇都會用到。

3.1 把一條路徑翻成公式

第 4 步說「把路徑翻成公式」。規則只有兩條：

• 賦值 v = e 變成等式 v = e
• 條件成立（if (c) 走 true 分支）變成 c 本身

例如這條通往 ERROR 的路徑：

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

翻譯後是 $x = 1 \;\wedge\; y = x + 1 \;\wedge\; y < 0$。

現在問題變成純數學的了：這三個條件能同時成立嗎？不能——前兩式逼出 $y = 2$，跟第三式牴觸。

「路徑走得通」等價於「公式有解」。 這個轉換是整個領域的地基。回答「有沒有解」的程式叫 SMT solver；你不需要知道它內部怎麼運作，只要知道它回答什麼：有解（satisfiable，這條路走得通）或無解（unsatisfiable，走不通、是誤報）。

3.2 為什麼變數要加下標

上面那個翻譯有個漏洞。看這兩行：

x = 1;
x = x + 1;

照規則會翻成 $x = 1 \wedge x = x + 1$。但 $x = x+1$ 在數學上永遠是假的——沒有任何數字等於自己加一。翻譯出錯了。

問題在於：程式裡的 x 是一個會變的盒子，數學裡的 $x$ 是一個固定的值。同一個名字被當成兩種東西用。

3.3 前人的兩個毛病

現在可以講清楚問題出在哪了。回到第 1 節那個 locking 例子。

第一，數量爆炸。 要排除所有誤報，$p_1, \dots, p_n$ 全都得追蹤。$n$ 個布林 predicate 就是 $2^n$ 種組合，抽象狀態指數成長。

第二，位置放錯。 前人的做法是把找到的 predicate 靠啟發式撒出去，而且往往一視同仁地加到許多、甚至全部的程式位置。但 $p_1$ 只在標籤 1 和 2 之間有用，把它帶到程式的每個角落是純粹的浪費。

382 對 8。這就是「哪些 predicate 用在哪裡」值得單獨解一次的理由。

4 這篇的解法

4.1 證明裡面就有答案

論文 §1（p.233）的原話是：一條抽象路徑之所以走不通，理由已經簡潔地編碼在「它走不通」的證明裡了。

4.2 工具：只用共同語言說話

把一條走不通的路徑從中間切開，前半段叫 $\varphi^-$，後半段叫 $\varphi^+$。兩者合起來無解（因為路徑走不通）。

interpolant（插值式）是一個公式 $\psi$，滿足三個條件（論文 §2, p.234）：

1. $\varphi^- \Rightarrow \psi$ —— 前半段成立時，$\psi$ 一定成立
2. $\psi \wedge \varphi^+$ 無解 —— $\psi$ 已經足以跟後半段矛盾
3. $\psi$ 只用同時出現在 $\varphi^-$ 和 $\varphi^+$ 裡的符號

第 3 條就是我們要的東西。 切點兩側的共同符號，正是「執行到切點時各變數當下的值」——不多不少，剛好是那個程式位置需要記住的事實。回頭看第 3.3 節說的前人毛病：predicate 裡混進「舊值」，正好被條件 3 擋掉了。

4.3 真正的貢獻不是「用了 interpolation」

這點很容易被誤讀。Craig 的定理只保證 interpolant 存在，沒說怎麼把它算出來。

這篇發明的是一套可以機械執行的推導規則。 論文 §3 定義了兩層東西：

第一層，一個證明系統（Fig. 3, p.235）。四條規則 HYP、COMB、CONTRA、RES，用來對線性算術的子句集合產生反駁證明。

第二層，帶插值的推導規則。 把上面每條規則改寫成這個形式：

方括號就是重點。 推導一路往下走，方括號裡的東西同步累積；推到矛盾（$\vdash \bot$）時，方括號裡剩下的就是 interpolant。

4.4 每個位置一份清單

不要只在一個地方切開路徑。沿著路徑的每一個切點都切一次，每個切點各求一個 interpolant。

5 案例：三個，由淺入深

論文裡有四個具體案例。這一節走前三個，由淺入深；第四個放在最後當延伸。

5.1 案例一：locking（不用算，先建立直覺）

回到第 1 節那支程式，這是論文的 Figure 1（p.233）。

我們已經知道答案是「記住 $p_1$」。現在用 4.4 的眼光重看一次：

條件 3 自動幫你做到了「只記必要的」。 這不是啟發式撈出來的結果，是規則的直接後果。

5.2 案例二：算出一個 interpolant（論文 Figure 2）

這是論文的主案例（p.234）。ctr 是計數器，m 是另一個變數：

1:  x := ctr;
2:  ctr := ctr + 1;
3:  y := ctr;
4:  assume(x = m);
5:  assume(y ≠ m + 1);

這條路徑走不通。 原因：$x$ 抄下舊的 ctr，然後 ctr 加一，$y$ 抄下新的 ctr，所以必然 $y = x + 1$。既然 $x = m$，就有 $y = m+1$，第 5 行的 $y \ne m+1$ 不可能成立。

照 3.2 的 SSA 規則翻成公式：

這五條的 conjunction 就是這條路徑的 trace formula，它無解。

原文這裡有個排版錯誤，順便學一課。 論文 Figure 2 第 5 列的約束印成 $\langle y,2 \rangle = \langle m,0 \rangle + 1$（等號），但那一行的指令是 assume(y ≠ m+1)，而且論文同一頁明說「the conjunction $\varphi$ of all constraints is unsatisfiable」。照等號讀，這五條其實有解（取 $\mathit{ctr}_0 = m_0 = 0$ 就成立），整個例子會垮掉。所以原意必然是 $\ne$，上表已經改正。 讀論文本來就會遇到這種事。算不出來的時候，先確認是不是自己錯了；真的對不上，原文也可能有 typo。

論文算出的 interpolant 是 $\psi_2 = (\langle x,1 \rangle = \langle \mathit{ctr},1 \rangle - 1)$，翻回程式變數就是 $\hat\psi_2 = (x = \mathit{ctr} - 1)$。

這就是位置 2 需要記住的唯一事實。 不是 ctr 的值，不是 x 的值，而是它們的差。

5.3 案例三：自己用規則導一次（論文 Figure 4）

上面兩個案例都是看答案。但這篇的重點是不用猜——照著規則走，interpolant 會自己掉出來。

為了讓你專心在機制上，這裡只用線性算術的三條規則，不碰 resolution。

5.4 一個容易混淆的地方

做完上面那題，有個陷阱要先拆掉，很多人第一次會弄混。

問題一：推導過程中 $y$ 是在哪裡消失的？

問題二：那為什麼 interpolant 能『保證』只含共同變數？

把這兩件事混為一談的後果：你會以為「代數消去 = 只含共同變數」。這在上面那個例子恰好看起來成立，但換到 resolution 那半套規則就完全對不上。

記住：消去是這個例子的計算過程，不變量才是通則的保證。

5.5 案例四（延伸）：resolution

6 他們比了什麼、沒比什麼

這一節值得慢慢讀，因為論文的實驗結果有一個反直覺的地方，而論文自己誠實地寫出來了。

6.1 實驗設定

• 實作：BLAST，論文作者群的軟體模型檢查器。求 interpolant 用 VAMPYRE 這個能產生證明的定理證明器。
• 對象：數個 Windows NT 裝置驅動程式，驗證的性質是一個關於 I/O Request packet 處理的有限狀態自動機（22 個狀態）。
• 硬體：IBM ThinkPad T30，2.4 GHz Pentium，512MB RAM。
• 比較的三組設定（同一個工具、同一批程式、同一台機器）：

6.2 數字

6.3 讀出反直覺的那一格

但接著看 Disc 那幾欄，會發現一件怪事：

Craig+Locality 的總時間反而比 Craig 慢，而且慢不少（floppy：25m20s vs 7m56s）。

那它贏在哪？看 Reach 欄——給定所有 predicate 之後，只做可達性分析：

• floppy：3m21s → 0m46s
• parclass：9m1s → 1m6s

所以「哪個比較好」的答案取決於你在測什麼。 一次性的驗證看 Disc，Craig 贏；要反覆驗證、或要輸出證明，看 Reach 和記憶體，Craig+Locality 大幅領先。

6.4 他們沒比什麼

但也因此有幾件事它沒有告訴你：

• 沒有跟其他工具比。 表裡沒有 SLAM 或任何外部系統的數字，所以看不出這套方法相對於當時其他做法的位置。
• 記憶體只有文字描述，沒有數字。 「顯著較少」是論文的說法，表格裡沒有這一欄。
• 「後續執行更快」也沒有數字。 同樣只是文字宣稱。
• benchmark 全部是 Windows 裝置驅動程式，性質是同一個 22 狀態的自動機。換一種程式、換一種性質會怎樣，這份實驗答不了。
• 論文提到在 parclass 上找到數個違反規範的地方，表中數字是把含錯誤的 case 註解掉之後的版本——也就是說，表格量的是「驗證正確程式」的成本。

7 怎麼讀原文

只有 13 頁（pp.232–244），但密度很高。

7.1 一組動作，不只是順序

讀這類論文時，專業讀者做的不是「從頭讀到尾」，而是一組固定的動作。拿這篇練習：

• 看到定義，先找反例。 讀到 interpolant 的三個條件，問「拿掉第 3 條會怎樣？」——答案是 $\varphi^-$ 自己就成了合法的 interpolant，等於什麼都沒壓縮。第 3 條是唯一逼迫壓縮發生的條件。
• 看到定理，先問它排除了什麼。 Craig 的定理保證存在性，那它沒有保證什麼？沒有保證好算、沒有保證唯一、沒有保證算出來的那個對驗證有用。這篇的貢獻正好落在它沒保證的那一格。
• 看到表格，先找沒有比較的那一格。 就是 6.4 做的事。
• 看到「我們的方法快 N 倍」，先問變因。 這篇沒有這個問題（它是自我比較），但這個習慣要帶著走。
• 讀不懂的段落，先確認是不是自己錯了；真的對不上，原文也可能有 typo。 5.2 那個等號就是。

7.2 各節導覽

下表的章節名與起始頁都逐頁對照過原文。

如果只有一小時：Abstract → §1 → §2（含 Locality）→ §3 的 Fig. 3 與 Fig. 4 → §7 的 Table 1。這條線涵蓋了問題、洞察、機制與證據，其餘都是把它做嚴謹的細節。

取得原文：本頁頂端有 DOI 與作者公開版 PDF 的連結，教材裡每個 p.NNN 也都直接連到原文那一頁。