VCC — 给并发 C 加注解，让 SMT 自动证它对

待复核

是什么

VCC（Verifying C Compiler）是一套给 C 程序加注解、让机器自动判断它在并发下还对不对的工具。日常类比：你写菜谱时，每一步都顺手画两条线——「下锅前必须 X」「出锅后必然 Y」；机器照着这些线自己核对，错了立刻报。

工作流大致是：

带注解的 C  →  Boogie 中间语言  →  Z3（SMT solver）  →  通过 / 反例

注解不改变运行行为（就像注释一样），但被工具读出来，转成数学问题去证。

VCC 的代表项目是给微软 Hyper-V hypervisor（约 35K 行 C 加 5K 行汇编）推进功能正确性验证——大头模块过了关，整机并未证完；这是当时把”演绎验证”推到工业代码体量的最大尝试之一。

为什么重要

C 是大量基础软件（OS 内核、驱动、hypervisor、加解密库）的母语；这些软件错一行就可能让整台机器崩。但 C 几乎是所有形式化工具最难啃的目标——指针随便指、内存随便改、还能多线程。

不理解 VCC，很多事讲不清：

为什么 2008 年前后，“演绎验证”突然能上 35K 行真实工业代码（不是教科书例子）
为什么微软愿意在 Hyper-V 这种产品线上投三年做形式验证
为什么后来 Dafny / Why3 / Frama-C 走的路都和 VCC 像——共享同一套 IVL 思路（intermediate verification language）
为什么”自动 SMT”和”交互式证明”在 2010 年代分成两派——VCC 是自动派的工业旗手

核心要点

VCC 把”证明 C 程序对”拆成 三件事：

怎么写注解：用 _(requires ...)（前置条件）、_(ensures ...)（后置条件）、_(invariant ...)（类型/循环不变式）。形式跟 Hoare logic 直接对应（见 hoare-logic）。
怎么管共享内存：VCC 的招牌是 ownership tree（所有权树）——每个对象在任意时刻有唯一”拥有者”。要并发修改一块内存，要么独占持有它，要么把字段标 volatile 走两态不变式（two-state invariants：不变式必须在每次原子写跨过去都成立）。
怎么自动证：注解 + C 程序被翻译成 Boogie（见 boogie-2005）这种验证中间语言；Boogie 把它丢给 Z3（见 z3-2008）这种 SMT solver。证不出来就给反例，让你回去改注解。

实践案例

案例 1：一个最小例子感受语法

int abs(int x)
    _(requires x > INT_MIN)        // 否则取绝对值会溢出
    _(ensures \result >= 0)        // 保证返回非负
    _(ensures \result == x || \result == -x)
{
    if (x < 0) return -x;
    return x;
}

逐部分解释：

_(requires ...)：调用前必须成立——这里禁止 INT_MIN，否则 -x 溢出
_(ensures ...)：返回后必须成立——\result 就是返回值
VCC 翻成 Boogie → Z3；几毫秒判定通过，不用手写证明

案例 2：并发场景下 VCC 的核心招——ownership

类比：改快递包裹前先拆封，改完再封回并核对清单；没拆封不许动里面的东西。

struct Node {
    int data;
    _(invariant data >= 0)         // 类型不变式：data 永远非负
};

void update(struct Node *n)
    _(writes n)                    // 这次调用允许修改 n
    _(maintains \wrapped(n))       // 进出时 n 都处于"已封装"
{
    _(unwrap n)                    // 1. 拆封：拿到修改权
    n->data += 1;                  // 2. 改字段
    _(wrap n)                      // 3. 封回：自动复检 invariant
}

三步：unwrap 拆封 → 改内存 → wrap 封回。并发下别人只能看见”封好”的对象，SMT 才推得动。

案例 3：Hyper-V 的工业拷问

Verisoft XT 用 VCC 验 Hyper-V。挑战：35K 行底层 C、多核改共享结构、代码非为验证而写。注解常长这样：

_(invariant \mine(page_table) && page_table->valid)
_(writes \extent(vcpu))

工程实际：注解量 ≈ 代码量甚至更多；一条 invariant 可能琢磨几小时；Z3 超时就得手写 trigger。大头模块过了——工业体量可行，但贵。

踩过的坑

注解不是写完就完——你得调它。Z3 不是万能，遇到量词（forall）就需要手工写 trigger。“为什么 30 秒前还能过，加了一行就 timeout”——是 VCC 用户的日常。
ownership 限制写法。一个对象只能有一个 owner，拆/封都要显式标。设计阶段就要想好谁拥有谁，否则代码改一半发现验不通。
不证终止性。VCC 默认证的是”如果终止，结果对”——这叫 partial correctness。要证终止性得另写 ranking function（VCC 里通过 decreases 注解，但工程上常被略过）。
不证编译器和硬件。VCC 假设编译器把 C 编译成等价机器码、CPU 按 C 内存模型执行。Hyper-V 项目里部分汇编另用 isabelle-hol-2002 验。

适用 vs 不适用场景

适用：

自动化优先的并发 C 验证（OS 内核、hypervisor、驱动、加解密原语）
已有 C 代码、不想改语言的团队（不像 fstar 要重写）
能接受注解/代码行数比常 ≥ 1，并预留周级调 trigger 的工程成本

不适用：

想要近乎”零注解”——找静态分析（astree、cousot-abstract-interpretation）
不能容忍 SMT 不可预测——找交互式证明（isabelle-hol-2002、Coq/seL4）
完全函数式或纯研究性代码——直接用 dafny-2010、why3-2013、fstar 更顺
需要证终止性、复杂时序属性——VCC 不是首选

历史小故事（可跳过）

2003 年前后：微软研究院起 Spec#（C# 加契约），用 Boogie + Z3 自动证。这是 VCC 的工程母舰。
2007 年：欧洲微软创新中心（EMIC）+ 萨尔大学 + 柏林洪堡启动 Verisoft XT 项目，目标是 Hyper-V 形式验证。Spec# 不能直接验 C，于是把 Spec# 工程链路移植到 C——这就是 VCC。
2009 年：TPHOLs 这篇论文是 VCC 的官方亮相，作者列表横跨 EMIC 和 MSR。
同年另一条线：澳洲 NICTA 用 Coq/Isabelle 完成 seL4 微内核证明（约 9K 行 C）——交互式路线的代表。两个团队几乎同时证明：千行级 C 操作系统级代码可以被形式化。
之后：Boogie 被 Dafny 接棒；VCC 本身没像 Dafny 那样火出圈，但工业 C 验证的工程问题（注解量、SMT 不稳定、ownership 模型）都被这套实践提前蹚过。

学到什么

演绎验证 = 注解 + 翻译 + SMT——这条流水线 2009 年就被打通到 35K 行真实代码体量
ownership 是并发验证的钥匙——把”谁能改谁”显式上墙，机器才推得动
自动 vs 交互——VCC 选自动 SMT，付出的代价是 trigger 调试和 timeout 不确定性；seL4 选交互证明，付出的代价是工时数倍
工业级形式验证不是免费——Hyper-V 项目证明它可行，也证明它贵；后续工具链都在围绕”怎么少写注解”演化

关联

boogie-2005 —— VCC 的翻译后端，每条注解最终落到 Boogie 程序
z3-2008 —— Boogie 调用的 SMT solver，VCC 体感的”快或慢”主要由 Z3 决定
dafny-2010 —— 同 Boogie 家族的姐妹，但目标是新写的代码，不是已有 C
frama-c-2012 —— 同代 C 验证平台，更交互、更模块化
why3-2013 —— 走 IVL 思路的法国学派工具
hoare-logic —— requires/ensures 的理论祖先
reynolds-separation-logic —— 处理共享堆的另一条路（VCC 没走但常被对比）
isabelle-hol-2002 —— 交互式证明代表；Hyper-V 项目里汇编部分用它
csp-hoare-1978 —— 并发推理的早期奠基

反向链接

hoare-logic —— Hoare Logic — 把”程序对不对”变成”数学证明对不对”
ironfleet-2015 —— IronFleet — 把分布式协议证到一行 bug 都没有