Abstractions from Proofs — 討論用

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

Abstractions from Proofs

POPL 2004 · Henzinger, Jhala, Majumdar, McMillan

一個問題：程式驗證器該記住哪些事實？

1 先自己試一次

這支程式是對的

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

lock 和 unlock 嚴格交替。

但驗證器會誤報

它說：「找到一條路徑，lock() 之後沒有 unlock()。」

那條路徑：

進入第一個 if → 上鎖
不進入第二個 if → 沒解鎖

從控制流程看，這條路徑確實存在。

停一下

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

答案

記住 p1 的值。

$p_1$ 為真 → 第一個 if 進得去 → 第二個 if 也進得去。

兩個 if 的條件是同一個。

但問題還沒完

這裡有 $n$ 個這樣的 if。

全部都要記嗎？

$$2^n \text{ 種組合} \quad (n = 30 \Rightarrow \text{十億})$$

再看仔細一點

$p_1$ 這個事實，只在標籤 1 和 2 之間有用。

過了標籤 2，那對 lock/unlock 已經配好，$p_1$ 再也用不到。

所以真正的問題是

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

這篇論文在回答這個。

而它的答案有點出乎意料——

不要用猜的。去讀「這條路走不通」的那份證明。

2 這個問題為什麼值得解

一段簡短的歷史

年代	發生了什麼
1980s	model checking 在硬體上很成功——狀態有限，窮舉得完
—	但軟體不行：一個 32 位元整數就有四十億種值
1997 前後	predicate abstraction：不追蹤數值，只追蹤是非問句
2000s 初	CEGAR 自動化 refinement；SLAM 驗證 Windows 驅動成功
2004	這篇：predicate 到底該從哪裡來

predicate abstraction

不追蹤變數的確切數值，只追蹤一組 predicate 的真假。

三個 predicate → 每個狀態壓成三個位元 → 最多 $2^3 = 8$ 種。

無限變有限，就能窮舉。

代價：資訊流失。而那正是我們要的——抽象就是刻意丟掉不重要的東西。

CEGAR 迴圈

1. 用很少的 predicate 做粗略抽象
2. 在抽象上找通往 ERROR 的路徑
3. 找不到  → 程式安全，結束
4. 找到了  → 把路徑翻成公式，丟給 solver
5. 有解    → 真的 bug
6. 無解    → 誤報。加新的 predicate，回到 2

難的全部集中在第 6 步

「加入新的 predicate」

加哪些？加多少？加在哪裡？

加太少 → 同一條誤報又冒出來，迴圈不終止加太多 → $2^n$ 爆炸

到 2004 年，這一步仍然靠啟發式規則在猜。

3 前人做到哪裡

先看第 4 步在做什麼

把路徑翻成公式，規則只有兩條：

賦值 v = e → 等式 v = e
條件成立 if (c) → c

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

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

路徑走得通 ⟺ 公式有解。

一個陷阱：為什麼要加下標

x = 1;
x = x + 1;

照規則翻成 $x = 1 \wedge x = x + 1$。

但 $x = x + 1$ 永遠是假的。

SSA

給每次賦值後的值一個新名字：

$$x_1 = 1 \;\wedge\; x_2 = x_1 + 1$$

有解了（$x_1 = 1, x_2 = 2$），而且忠實。

論文寫成 $\langle x, 1 \rangle$。

下標不是指令編號——p.234 說 $\langle \mathit{ctr},1 \rangle$ 是「前兩個指令後」的值。

前人的兩個毛病

一、數量爆炸。 $p_1 \dots p_n$ 全要追蹤 → $2^n$

二、位置放錯。 找到的 predicate 被一視同仁撒到許多、甚至全部的程式位置

但 $p_1$ 只在標籤 1 到 2 之間有用。

論文要的是 parsimonious

在每個控制位置，只指定當下變數之間的關係，而且只留證明正確性真正需要的那些 — Abstract, p.232

這個觀察值多少？

一個 138,000 行的 C 驅動程式：


證明正確總共需要	382 個 predicate
但每個位置平均只需要	約 8 個

382 對 8。

4 這篇的解法

洞察：證明裡面就有答案

一條抽象路徑之所以走不通，理由已經簡潔地編碼在「它走不通」的證明裡了。 — §1, p.233

solver 說「無解」時，它握有一份反駁證明。

讀它，需要的事實就浮出來。而且只要對證明做一次線性掃描。

工具：只用共同語言說話

把走不通的路徑切開：前半 $\varphi^-$，後半 $\varphi^+$。

interpolant 是一個公式 $\psi$：

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

比喻

前半段講中文，後半段講日文。

$\psi$ 只能用兩邊都寫得出來的漢字。

條件 1：$\psi$ 是前半段的合理摘要
條件 2：這份摘要足以拆穿後半段
條件 3：摘要只能用共同詞彙

第 3 條就是我們要的東西

切點兩側的共同符號 = 執行到切點時，各變數當下的值。

不多不少，剛好是那個位置需要記住的事實。

回頭看前人的毛病：predicate 混進了變數的「舊值」——被條件 3 直接擋掉。

但貢獻不是「用了 interpolation」

Craig interpolation 是 1957 年的定理（論文參考文獻 [9]）。

它只保證 interpolant 存在——沒說怎麼算。

貢獻是一套可以機械執行的規則

第一層：一個證明系統（Fig. 3, p.235）——HYP、COMB、CONTRA、RES

第二層：把每條規則改寫成

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

方括號同步累積。推到矛盾時，裡面剩下的就是 interpolant。

不用猜，不用事後驗證，照著走就會掉出來。

第二個洞察：locality

不要只切一刀。沿路徑每個切點都切一次。

第 $i$ 個切點的 interpolant，只含那裡的共同符號 → 「第 $i$ 個位置需要知道的事實」

於是得到一張表，不是一包全域 predicate。

382 對 8 就是這樣來的。

5 動手算

案例一：回看 locking

誤報路徑：進第一個 if、不進第二個。

前半有 $p_1 \ne 0$
後半有 $p_1 = 0$
共同符號只有 $p_1$

所以那個切點的 interpolant 不可能牽扯 $p_2 \dots p_n$——那些符號在一側根本不出現。

條件 3 自動做到了「只記必要的」。

案例二：論文的主例（Figure 2, p.234）

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

為什麼走不通？

翻成公式

行	約束
1	$\langle x,1 \rangle = \langle \mathit{ctr},0 \rangle$
2	$\langle \mathit{ctr},1 \rangle = \langle \mathit{ctr},0 \rangle + 1$
3	$\langle y,2 \rangle = \langle \mathit{ctr},1 \rangle$
4	$\langle x,1 \rangle = \langle m,0 \rangle$
5	$\langle y,2 \rangle \ne \langle m,0 \rangle + 1$

在第 2 行後面切一刀

$\varphi^-_2$ = 前兩條，$\varphi^+_2$ = 後三條

共同符號：$\langle x,1 \rangle$、$\langle \mathit{ctr},1 \rangle$

也就是「執行完前兩行後，$x$ 和 ctr 的值」。

算出來的 interpolant

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

翻回程式變數：

$$\hat\psi_2 = (x = \mathit{ctr} - 1)$$

位置 2 需要記住的唯一事實。

不是 ctr 的值，不是 x 的值——是它們的差。

案例三：現在換你算

用論文 Figure 4（p.237）的例子，照規則自己推一次。

$$\varphi^- = (0 \le y-x) \wedge (0 \le z-y) \qquad \varphi^+ = (0 \le x-z-1)$$

做完之後，一個陷阱

問題一：$y$ 在哪裡消失的？ → 兩個不等式相加，$-y$ 和 $+y$ 抵銷。國中代數。

問題二：為什麼保證只含共同變數？ → 不是因為代數消去，是因為整套規則維持的不變量。

混為一談的後果：換到 resolution 那半套規則就完全對不上。

6 實驗：他們比了什麼

三組設定，同一個工具

設定	意思
Previous	舊版 BLAST，不用 interpolant
Craig	用 interpolant 找 predicate，但不分位置
Craig+Locality	用 interpolant，而且每個位置只追蹤相關的

同一批 Windows 驅動程式、同一台機器。

Table 1（節錄，p.244）

程式	行數	Previous	Craig	C+L	C+L 的 Reach	Preds	Avg/Max
floppy	17,707	7m10s	7m56s	25m20s	0m46s	240	7.7/37
parclass	138,373	—	42m24s	77m40s	1m6s	382	7.2/28

— = 六小時跑不完

反直覺的一格

Craig+Locality 的總時間反而比 Craig 慢。

floppy：25m20s vs 7m56s

那它贏在哪？

看 Reach（給定所有 predicate 後，只做可達性分析）：

	Craig	Craig+Locality
floppy	3m21s	0m46s
parclass	9m1s	1m6s

快了將近九倍。

因為每個位置只帶 7 個 predicate，不是全部 382 個。

所以「哪個比較好」取決於你在測什麼

一次性驗證 → 看 Disc，Craig 贏
反覆驗證、要輸出證明 → 看 Reach 和記憶體，Craig+Locality 大勝

論文還提到（表上沒有數字）：記憶體顯著較少、證明樹更小。

他們沒有比什麼

沒跟其他工具比（沒有 SLAM 的數字）
記憶體只有文字描述，沒有數字
「後續執行更快」也沒有數字
benchmark 全是 Windows 驅動，性質是同一個 22 狀態自動機

7 怎麼讀原文

一組動作，不是一個順序

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

如果只有一小時

Abstract → §1 → §2（含 Locality 段）→ §3 的 Fig. 3 與 Fig. 4 → §7 的 Table 1

注意：Locality 那段在 p.235，排在「3 Interpolants from Proofs」標題之前，屬於 §2。

回到最初那個問題

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

答案：去讀「這條路走不通」的證明。

切點兩側的共同符號，就是那個位置需要記住的東西。

382 對 8。