【操作系统百科】内核并发的形式化验证

并发 bug 难以复现、难以调试。lockdep 和 KCSAN 能抓一部分，但形式化验证可以穷举所有可能的执行序列。

一、先看图

flowchart TD
    CODE[内核并发代码] --> LITMUS[Litmus Test<br/>小片段建模]
    CODE --> CBMC_M[CBMC<br/>C 代码有界验证]
    CODE --> TLA[TLA+<br/>协议级建模]

    LITMUS --> HERD[herd7 + LKMM<br/>穷举内存序]
    CBMC_M --> SAT[SAT/SMT 求解器]
    TLA --> TLC[TLC 模型检查器]

    HERD --> BUG[发现违反？]
    SAT --> BUG
    TLC --> BUG

    classDef tool fill:#388bfd22,stroke:#388bfd,color:#adbac7;
    classDef result fill:#f0883e22,stroke:#f0883e,color:#adbac7;
    class LITMUS,CBMC_M,TLA tool
    class HERD,SAT,TLC tool
    class BUG result

二、herd7 与 Litmus Test

2.1 什么是 litmus test

一个最小化的并发场景——几行代码、两三个线程、一个待验证的断言。

C MP+wmb+rmb
{
    int x = 0; int y = 0;
}

P0(int *x, int *y) {
    WRITE_ONCE(*x, 1);
    smp_wmb();
    WRITE_ONCE(*y, 1);
}

P1(int *x, int *y) {
    int r0 = READ_ONCE(*y);
    smp_rmb();
    int r1 = READ_ONCE(*x);
}

exists (1:r0=1 /\ 1:r1=0)

2.2 运行

herd7 -conf linux-kernel.cfg MP+wmb+rmb.litmus
# 结果：Never（不可能出现）或 Sometimes（可能出现）

herd7 穷举 LKMM 允许的所有执行序列。

2.3 内核中的 litmus tests

ls tools/memory-model/litmus-tests/
# 几十个标准 litmus tests

三、CBMC

3.1 什么是 CBMC

C Bounded Model Checker：对 C 代码做有界模型检查。

给定循环上界 → 展开所有路径 → 转化为 SAT 问题 → 求解器判断 assert 是否可能违反。

3.2 用法

cbmc --unwind 5 my_code.c

3.3 内核中的应用

• 验证 RCU 的 publish-subscribe 正确性
• 检查 lock-free 数据结构的不变量
• 限制：代码规模不能太大（状态空间爆炸）

四、TLA+

4.1 协议级验证

TLA+ 不验证 C 代码——验证算法/协议的抽象模型。

---- MODULE SimpleLock ----
VARIABLES lock, waiting

Acquire(t) ==
    /\ lock = 0
    /\ lock' = t
    /\ waiting' = waiting \ {t}

Release(t) ==
    /\ lock = t
    /\ lock' = 0
    /\ UNCHANGED waiting

Invariant == \A t1, t2 \in Threads : ~(InCS(t1) /\ InCS(t2) /\ t1 /= t2)
====

4.2 应用

• Amazon 用 TLA+ 验证 S3 内部协议
• 内核社区用于 IPC 协议设计
• 不是验证实现，而是验证设计

五、KCSAN（Kernel Concurrency Sanitizer）

运行时数据竞争检测：

CONFIG_KCSAN=y

KCSAN 在运行时采样内存访问 → 发现 marked access 缺失 → 报告数据竞争。

BUG: KCSAN: data-race in func_a / func_b
  write to 0xffff... of 4 bytes by task 123:
    func_a+0x42/0x80
  read to 0xffff... of 4 bytes by task 456:
    func_b+0x18/0x60

5.1 与 herd7 的关系

• herd7：静态，穷举所有可能的执行序
• KCSAN：动态，只报告实际运行中观察到的竞争

互补，不替代。

六、rcutorture

modprobe rcutorture

对 RCU 进行暴力压力测试——多线程并发读/写/grace period → 检测语义违反。

不是形式化验证，但是 RCU 正确性的第一道防线。

七、实际案例

7.1 litmus test 发现的 bug

Paul McKenney 用 litmus test 发现多个内存序 bug：

• 缺少 smp_mb 导致的 publish-subscribe 失败
• ARM 弱序下的 control dependency 不足

7.2 CBMC 验证 RCU

cbmc --unwind 3 rcu_simplified.c --property "assert(readers_see_consistent_data)"

在简化模型上验证 RCU 的核心不变量。

八、工具对比

九、与测试的权衡

形式化验证不能替代测试：

• 形式化验证 → 证明模型正确
• 测试 → 验证实现行为
• 两者结合 → 信心最大化

十、小结

• litmus test + herd7：验证内存序正确性
• CBMC：C 代码有界模型检查
• TLA+：协议/算法设计验证
• KCSAN：运行时数据竞争检测
• 形式化验证与测试互补

参考文献

• tools/memory-model/
• Paul McKenney, “A Formal Model of Linux-Kernel Memory Ordering.” 2018
• Documentation/dev-tools/kcsan.rst
• Jade Alglave et al., “Herding Cats: Modelling, Simulation, Testing, and Data Mining for Weak Memory.” TOPLAS 2014
• 分布式百科-55-formal-verification（交叉引用）

工具

• herd7 / klitmus7（diy 工具套件）
• CBMC
• TLA+ / TLC
• KCSAN（CONFIG_KCSAN）
• rcutorture

上一篇：优先级反转 下一篇：中断架构