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 程序对”拆成 三件事：

1. 怎么写注解：用 _(requires ...)（前置条件）、_(ensures ...)（后置条件）、_(invariant ...)（类型/循环不变式）。形式跟 Hoare logic 直接对应（见 hoare-logic）。

2. 怎么管共享内存：VCC 的招牌是 ownership tree（所有权树）——每个对象在任意时刻有唯一”拥有者”。要并发修改一块内存，要么独占持有它，要么把字段标 volatile 走两态不变式（two-state invariants：不变式必须在每次原子写跨过去都成立）。

3. 怎么自动证：注解 + 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 / ensures 是注解。VCC 把它翻成 Boogie，Boogie 转成 SMT 公式给 Z3。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)                    // 拆封：进入修改区
    n->data += 1;
    _(wrap n)                      // 重新封装：检查不变式
}

wrapped / unwrap / wrap 是 ownership 机制的语法：拆开一段内存修改前必须显式声明，封回去时不变式自动复检。这一招让 VCC 既能精细控制并发可见性，又能让 SMT 跑得动。

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

Verisoft XT 项目用 VCC 验证 Hyper-V hypervisor。挑战是：

• 35K 行 C，几乎全是底层指针和位操作
• 多核并发：多个虚拟 CPU 同时改共享数据结构
• 真实代码不是为验证写的，要逆向加注解

工程实际：注解量经常和代码量同数量级或更多；写一条 invariant 可能要琢磨几小时；Z3 偶尔超时，得手动给 hint（trigger）。但最终大头模块通过了——证明这条路在工业体量上可行，哪怕昂贵。

踩过的坑

1. 注解不是写完就完——你得调它。Z3 不是万能，遇到量词（forall）就需要手工写 trigger。“为什么 30 秒前还能过，加了一行就 timeout”——是 VCC 用户的日常。

2. ownership 限制写法。一个对象只能有一个 owner，拆/封都要显式标。设计阶段就要想好谁拥有谁，否则代码改一半发现验不通。

3. 不证终止性。VCC 默认证的是”如果终止，结果对”——这叫 partial correctness。要证终止性得另写 ranking function（VCC 里通过 decreases 注解，但工程上常被略过）。

4. 不证编译器和硬件。VCC 假设编译器把 C 编译成等价机器码、CPU 按 C 内存模型执行。Hyper-V 项目里部分汇编另用 isabelle-hol-2002 验。

适用 vs 不适用场景

适用：

• 自动化优先的并发 C 验证（OS 内核、hypervisor、驱动、加解密原语）
• 已有 C 代码、不想改语言的团队（不像 fstar 要重写）
• 团队能投入大量”注解工程”成本（注解经常和代码同体量）

不适用：

• 想要近乎”零注解”——找静态分析（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 模型）都被这套实践提前蹚过。

学到什么

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

延伸阅读

• 论文 PDF：Cohen et al. 2009
• VCC 源码与教程：microsoft/vcc on GitHub（含完整 tutorial）
• Verisoft XT 项目主页（已停更但文档还在）：verisoftxt.de
• 对照阅读：seL4 论文 Klein et al. SOSP 2009，看交互证明路线怎么做同代的事

关联

• 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 —— 并发推理的早期奠基

反向链接

• astree —— ASTRÉE 分析器 — 让飞机控制代码的静态分析做到零警告
• cousot-abstract-interpretation —— Cousot 抽象解释 — 给静态分析一套统一数学框架
• csp-hoare-1978 —— CSP — 进程之间只许喊话不许共用内存
• frama-c-2012 —— Frama-C — 一个开源平台把 C 程序的多种验证方法拼到一起
• fstar —— F* — 把依赖类型、SMT 自动化、副作用追踪揉到一门语言里
• hoare-logic —— Hoare Logic — 把”程序对不对”变成”数学证明对不对”
• ironfleet-2015 —— IronFleet — 把分布式协议证到一行 bug 都没有
• reynolds-separation-logic —— Separation Logic — 把 Hoare 逻辑扩到带指针的程序
• why3-2013 —— Why3 — 写一次程序规范，多个证明器一起来证
• z3-2008 —— Z3 2008 — 把 SMT 工程化到工业默认