Invariant-at-Complie-Time

As our case is new, we must think and act anew.

— Abraham Lincoln

graph TB
    D["① 定义 Definition<br/>类型 + 文档化的不变量"] --> E["② 强制 Enforcement<br/>封装 · unsafe impl · 宏<br/>保证属性永不被破坏"]
    E --> C["③ 消费 Consumption<br/>把属性当前置条件<br/>换取优化与健全性"]
    C -.->|"新抽象成为下一层构建块<br/>(turtles all the way down)"| D

定义(Definition)

定义一个 Rust 类型系统可推理的对象,并用文字文档附上 Rust 无法推理的安全属性:

1
2
3
4
5
6
7
8
9
struct Node<T> {
// INVARIANT: `left` 中所有值都小于 `value`
left: Option<Box<Node<T>>>,

// INVARIANT: `right` 中所有值都大于 `value`
right: Option<Box<Node<T>>>,

value: T,
}

强制(Enforcement)

构造时建立不变量,修改时保持不变量,并且用封装(字段私有)堵住外部破坏的入口:

1
2
3
4
5
6
7
8
9
impl<T> Node<T> {
pub fn new(value: T) -> Node<T> {
Node { left: None, right: None, value }
}

// 前置条件:不变量成立
// 后置条件:不变量仍成立
pub fn insert(&mut self, value: T) -> Option<T> { /* 维护有序地插入 */ }
}

消费(Consumption)

1
2
3
4
5
6
7
8
9
10
11
12
13
impl<T: Ord> Node<T> {
// 依赖"有序"不变量 → 可以 O(log N) 定位,无需全树遍历
pub fn contains(&self, target: &T) -> bool {
let mut cur = self;
loop {
match cur.value.cmp(target) {
Equal => return true,
Less => cur = cur.left.as_deref()?,
Greater => cur = cur.right.as_deref()?,
}
}
}
}

对模块外的 safe 代码而言,"语言提供的安全保证"与"本模块提供的不变量"没有任何区别——违反两者的代码都编译不过。等于给 Rust 增加了一个新安全属性。


示例一:线程安全

Rust 引以为傲的线程安全并非语言特性,而是标准库用核心抽象实现的,原则上可以由第三方 crate 提供。

起点:spawn 必须走出语言边界

线程是 OS 概念,语言本身无法与线程交互,只能 unsafe 调系统 API:

1
2
3
pub fn spawn<F: FnOnce()>(f: F) {
unsafe { libc::pthread_create(/* ... */) }; // Rust 无法推理其行为
}

unsafe 的含义:不是"必定出事",而是"Rust 不够聪明、无法自证安全,程序员证明soundness"。

问题:不是所有值都能跨线程

上述 spawnunsound 的——闭包可能捕获非线程安全的值。解法:把"线程安全"编码进类型系统。

1
2
3
4
5
6
7
8
/// # Safety
/// 实现者必须保证:Self 可以安全地跨线程传递。
pub unsafe trait Send {}
// ^^^^^^ unsafe trait:实现者须显式 unsafe impl,主动担责

pub fn spawn<F: FnOnce() + Send>(f: F) { // 加上 bound → sound ✅
unsafe { libc::pthread_create(/* ... */) };
}

实现:axiom 式声明 + 组合式传播

1
2
3
4
5
6
7
8
9
10
11
12
// ① 对已知线程安全的基础类型:直接"钦定"(Rust 只能相信我们)
unsafe impl Send for u8 {}
unsafe impl Send for u32 {}

// ② 组合类型:受约束地实现
unsafe impl<'a, T: Send> Send for &'a Mutex<T> {}

// ③ derive(由 auto trait 机制达成同样效果)
#[derive(Send)]
struct Foo<T, U>(T, U);
// derive 展开 ≈
unsafe impl<T: Send, U: Send> Send for Foo<T, U> {}

使用侧:

1
2
let foo: Foo<&Mutex<u8>, u16> = /* ... */;
spawn(move || { /* use foo */ }); // 编译通过:整条 Send 链成立

示例二:编译期死锁预防

问题:锁顺序不一致 → 死锁

1
2
3
4
5
6
7
8
struct Stack {
ip: Mutex<IpState>,
device: Mutex<DeviceState>,
}

// Thread A // Thread B
stack.ip.lock(); stack.device.lock();
stack.device.lock(); stack.ip.lock(); // 经典死锁
sequenceDiagram
    participant TA as 线程 A
    participant TB as 线程 B
    TA->>TA: lock(ip) 成功
    TB->>TB: lock(device) 成功
    TA->>TA: 阻塞:等待 device
    TB->>TB: 阻塞:等待 ip
    Note over TA,TB: 互相持有对方想要的锁 → 死锁 💀

两个线程在"锁获取图"上形成环。思路:把无环锁顺序图编码进类型系统,且只允许沿图加锁

graph TB
    U["Unlocked(起点)"] --> IP["IpLock"]
    U --> DEV["DeviceLock"]
    IP -->|"允许:先 ip 后 device"| DEV
    DEV -.->|"❌ 环:此边无法通过编译"| IP

第一步:给每个互斥锁命名

1
2
3
4
5
6
7
struct Mutex<Id, T> {
mtx: std::sync::Mutex<T>,
_marker: PhantomData<Id>, // 仅存在于类型层面,零运行时成本
}

enum IpLock {} // 永不构造,只当"名字"用
enum DeviceLock {}

第二步:把锁顺序图编码为 trait

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
/// # Safety
/// 实现所构成的图必须无环!
pub unsafe trait LockAfter<M> {}
pub unsafe trait LockBefore<M> {}
unsafe impl<B: LockAfter<A>, A> LockBefore<B> for A {} // 对偶推导,A befoer B == B after A

macro_rules! impl_lock_after {
($A:ty => $B:ty) => {
// SAFETY: 若引入环,blanket impl 之间会冲突 编译失败
unsafe impl LockAfter<$A> for $B {}
unsafe impl<X: LockBefore<$A>> LockAfter<X> for $B {}
};
}

// 声明图:Unlocked → IpLock → DeviceLock
impl_lock_after!(Unlocked => IpLock);
impl_lock_after!(IpLock => DeviceLock);

宏展开出的 blanket impl 使得一旦声明出环,impl 之间发生冲突,有环的图直接编译不过

第三步:用 LockCtx 跟踪"当前在图上的位置"

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
struct LockCtx<Id>(PhantomData<Id>);   // 零大小类型

pub enum Unlocked {} // 图的根
impl LockCtx<Unlocked> {
pub const UNLOCKED: Self = LockCtx(PhantomData);
}

impl<Id, T> Mutex<Id, T> {
pub fn lock<L>(&self, ctx: &mut LockCtx<L>)
-> (MutexGuard<'_, T>, LockCtx<Id>)
where
L: LockBefore<Id>, // 只能沿图往下游加锁
{
(self.mtx.lock().unwrap(), LockCtx(PhantomData))
}
}

签名里的三个机关:

  1. &mut LockCtx<L>可变借用旧上下文 → 持锁期间旧上下文被"冻结",不可复用;
  2. L: LockBefore<Id>:新锁必须是当前节点的下游 → 已持有的锁不可能再锁(无环);
  3. 返回新 LockCtx<Id>:持锁期间唯一可用的上下文,且只允许继续往下游走。

第四步:使用与"编译期报错"

1
2
3
4
5
6
7
8
9
10
// ✅ 顺序合法
let mut ctx = LockCtx::UNLOCKED;
let (ip, mut ctx) = stack.ip.lock(&mut ctx);
let (dev, ctx) = stack.device.lock(&mut ctx);

// ❌ 违反顺序 → 编译错误
let mut ctx = LockCtx::UNLOCKED;
let (dev, mut ctx) = stack.device.lock(&mut ctx);
let (ip, _) = stack.ip.lock(&mut ctx);
// ^^^^^^^^^^^^ ERROR: Unlocked 不是 DeviceLock 的 LockBefore

实践建议

"部分函数(partial function)" bad smell

公开函数不应 panic,也不应因为"调用方传了非法值"而返回 Option/Result(I/O 失败这类内在错误除外)——"非法参数"这种代码本来就不该编译通过:

1
2
3
4
5
6
7
8
// ❌ bad smell:错误被推迟到运行时
fn set_port(p: u16) -> Result<(), InvalidPort>;
fn get(l: &List, i: usize) -> Option<Item>;

// ✅ 让非法状态不可表示(illegal states unrepresentable)
struct Port(NonZeroU16); // 0 端口在类型上不可能
struct Index(usize);
fn get(l: &List, i: Index) -> Item; // Index 只能经 l.new_index() 等合法途径产生

让 API 精确匹配问题

1
2
3
4
5
6
7
8
9
10
pub enum IpParseError<I: IcmpIpExt> {
Parse { error: ParseError },
ParameterProblem {
src_ip: I::Addr,
dst_ip: I::Addr,
pointer: I::ParameterProblemPointer, // IPv4: u8 / IPv6: u32 —— 泛型锁定宽度
must_send_icmp: bool,
// ...
},
}

简单是隐藏复杂的艺术

内部可以很丑,但用户的心智模型必须极简:

1
2
锁顺序库内部:blanket impl 对偶推导 + 宏展开 + PhantomData 状态机(丑)
用户心智模型:环 → 编译错误(5 个字)

内部 API 严格

内部 API 也要有安全要求就标 unsafe fn,可能 panic 就写文档

1
2
3
/// # Safety
/// `buf` 必须以一个完整的 IP 头部开头。
unsafe fn parse_ip(buf: &[u8]) -> IpHeader; // 内部函数照样 unsafe + 文档

收益

  1. 若整类 bug 在编译期消失,code review 与测试的压力骤减,开发速度有望大幅提升(不是取消 review,而是让它聚焦于真正需要人的部分)。
  2. 软件复杂度随代码规模超线性增长,且大多是偶然复杂度;人的心智容量有限,偶然复杂度会挤占对本质复杂度的推理能力,限制我们能解决的问题上限。该方法论在每个模块上省下的小额复杂度会在大型代码库中复利式叠加
  3. AI 在这种类似问题场景下,缺少zero shot的能力。

本博客所有文章除特别声明外,均采用 CC BY-SA 4.0 协议 ,转载请注明出处!