资源

正文

4. 数学视角的操作系统

程序是一个状态机（gdb 单步执行 = 状态迁移），硬件是一个状态机（指令执行 = 状态迁移），操作系统毫无疑问也是一个状态机。

4.1 数学视角的计算机程序

程序的本质

程序是一种 “数学严格” 的对象

Everything is a state machine
- 程序 = 初始状态 + 迁移函数
- 在这个视角下，程序和数学对象已经无限接近了： $f(s)=s'$

原作者认为大学的培养方案有问题，他给出了一个设想：

webp

为什么会有程序？

是因为程序必须在无情执行指令的机器上执行
只有程序才配得上它

程序天生是 “人类” 的，也是 “反人类” 的

人类的一面：程序连接了人类世界需求
- 大语言模型有非常惊艳的编程能力
反人类的一面：程序会在机器上执行
- 大语言模型还是经常有幻觉
  - （对程序的行为的 100% 掌控就是非常困难的）
“Maintainability”: 代码字面意义和实际行为直接关联

我们能证明程序的正确性吗？

不同于 OJ 平台只要跑通就算正确，如果要用“数学严格”的方式证明下面计算整数 x 的二进制中 1 的个数的函数是否正确：

int popcount(int x) {
    int count = 0;
    while (x) {
        x -= (x & -x);
        count++;
    }
    return count;
}

我们还需要 “什么叫对”

Specification: 不 crash; 没有 UB; assert satisfy, …

我们要证明的“正确性”包括：

程序不会崩溃；

不触发未定义行为（UB, Undefined Behavior）；

对所有输入都满足断言（assert）中描述的语义条件。

int popcount(int x) {
    int count = 0;
    while (x) {
        x -= (x & -x);
        count++;
    }
    return count;
}

void popcount_spec() {
    for (uint64_t x = 0; x <= 0xffffffff; x++) {
        assert( ((x >> 0) & 1) + 
                ((x >> 1) & 1) + ...
                ((x >> 31) & 1) == popcount(x) );
    }
}

对于所有 32 位无符号整数 x，popcount(x) 的返回值应当等于 x 的二进制展开中 1 的数量。

“程序正确性”不是一句空话，它必须基于明确的 规范（spec）。

所以：

要证明 popcount 正确，必须先定义它“正确”的含义（specification）。

定义完后，才能用逻辑（如循环不变式）证明它满足这个规范。

证明程序 $f$ 正确

暴力枚举

写一个 driver code，枚举所有的 $x$ $x$ ，运行 $f(x)$ $f (x)$
- Testing: 选一些有代表性的

写出证明

直接证明 “For all executions of $f$ $f$ the specification is satisfied.”
- 就和你在《离散数学》课上的证明一样

我们希望像数学家证明定理那样，严格地证明一个程序 f 是正确的。也就是说，不只是“我测试了很多样例，看起来没错”，而是要在 数学逻辑系统 中，写出一份严密的形式化证明：
∀x.\; \text{spec}(x, f(x))
即对所有输入 $x$ ，程序 $f$ 的输出满足规范（specification）。

“Proof Assistant” (Coq, Lean, …)

它会拒绝一切伪证
- EMMS Lecture by Terence Tao

这里指的是一类交互式定理证明器（Interactive Theorem Prover）——它们是 数学与计算机的结合体，用于：

形式化地描述数学对象、算法、逻辑规则；

检查证明的每一步是否有效；

自动化推理或帮助人类完成大部分繁琐的逻辑推导。

webp

Proof assistant 是人工智能时代堪称完美的辅助工具：如果我们要信任 AI 产生的结果，就让它们给出一个 proof assistant 认可的证明吧！

延伸阅读：科普文章

4.2 数学视角的操作系统

操作系统 = 状态机的管理者

可以同时容纳多个 “程序状态机”
- 程序内计算：选一个程序执行一步
- 系统调用：创建新状态机、退出状态机、打印字符……

有了一个有趣的想法……

能不能我们自己定义 “状态机”
- 用我们喜欢的语言、喜欢的方式
- 不要受限于 C、汇编……
自己模拟状态机的执行
- 不就有了一个 “玩具操作系统” 吗？

操作系统中的对象

状态机 (进程)
- Python 代码
- 初始时，仅有一个状态机 (main)
- 允许执行计算或 read, write, spawn 系统调用
一个进程间共享的 buffer (“设备”)

系统调用

read(): 返回随机的 0 或 1
write(s): 向 buffer 输出字符串 s
spawn(f): 创建一个可运行的状态机 f

玩具操作系统

创建一个 os-model.py：

#!/usr/bin/env python3
import sys
import random
from pathlib import Path

class OS:
    # 定义可用的系统调用
    SYSCALLS = ['read', 'write', 'spawn']
    
    class Process:
        """模拟用户进程（使用 Python 生成器实现）"""
        def __init__(self, func, *args):
            # 初始化进程，将传入的函数转换为生成器对象
            self.func = func(*args)
            # 上一次系统调用的返回值（用于 send()）
            self.retval = None
            
        def step(self):
            """执行进程的一个系统调用步骤"""
            # 恢复生成器的执行，并传入上一次的返回值
            syscall, args, *_ = self.func.send(self.retval)
            # 清空返回值（等待下一次设置）
            self.retval = None
            # 返回系统调用的名称和参数
            return syscall, args
    
    
    def __init__(self, src):
        """初始化操作系统并加载用户程序"""
        # 执行用户代码，使得其中的 main() 函数可用
        exec(src, globals())
        # 创建第一个进程（入口为 main）
        self.procs = [OS.Process(main)]
        # 输出缓冲区，用于保存所有 write 的内容
        self.buffer = ''
        
    
    def run(self):
        """运行操作系统主循环，直到所有进程结束"""
        while self.procs:
            # 随机选择一个进程执行（模拟随机调度）
            current = random.choice(self.procs)
            try:
                # 执行该进程的一个系统调用
                match current.step():
                    case 'read', _:
                        # 模拟读取输入：返回随机的 0 或 1
                        current.retval = random.choice([0, 1])
                    case 'write', s:
                        # 模拟写操作：将输出内容加入缓冲区
                        self.buffer += s
                    case 'spawn', (fn, *args):
                        # 模拟创建新进程
                        self.procs += [OS.Process(fn, *args)]
                    case _:
                        # 无效的系统调用
                        assert 0
                        
            except StopIteration:
                # 当前进程执行完毕（生成器结束）
                self.procs.remove(current)
        
        # 所有进程结束后，返回输出内容
        return self.buffer
    

if __name__ == '__main__':
    # 检查命令行参数
    if len(sys.argv) < 2:
        print(f'Usage: {sys.argv[0]} file')
        exit(1)
    
    # 读取用户程序源码（例如 hello.py）
    src = Path(sys.argv[1]).read_text()
    
    # 将源码中所有的 sys_xxx 调用替换为 yield 形式
    # 例如：sys_write("Hi") -> yield "write", "Hi"
    for syscall in OS.SYSCALLS:
        src = src.replace(f'sys_{syscall}',
                          f'yield "{syscall}", ')
    
    # 运行模拟的操作系统
    stdout = OS(src).run()
    # 输出结果
    print(stdout)

模块	作用	类比真实系统
`Process`	封装生成器，表示一个进程	PCB（进程控制块）
`OS.run()`	主调度循环	内核调度器
`sys_read`	模拟输入	read 系统调用
`sys_write`	模拟输出	write 系统调用
`sys_spawn`	创建新协程	fork/spawn 系统调用
`random.choice(self.procs)`	随机调度一个进程	时间片轮转/抢占式调度
`self.buffer`	累积输出结果	标准输出缓冲区

创建一个 hello.py：

def main():
    x = 0
    for _ in range(10):
        b = sys_read()
        x = x * 2 + b
    
    sys_write(f'x = {x:010b}b')

命令行中：

1	`python os-model.py hello.py`

1	`x = 1110101001b`

打开并发程序的大门

操作系统是最早的实用并发程序

每个进程（程序）都是顺序状态机
- 但发生中断/系统调用以后，操作系统代码直接执行
- 如果有多个处理器（或者允许此时切换到另一个程序执行），就有了并发

创建一个 proc.py：

def Process(name):
    for _ in range(5):
        sys_write(name)

def main():
    sys_spawn(Process, 'A')
    sys_spawn(Process, 'B')

之后执行：

1	`python os-model.py proc.py`

1	`ABABBBABAA`

4.3 状态机模型与模型检查器

数学视角的操作系统

状态

多个 “应用程序” 状态机
- 当然，可以是模型

初始状态

仅有一个 “main” 状态机
- 这个状态机处于初始状态

迁移

选择一个状态机执行一步
- 就像我们在操作系统模型上看到的那样

计算机系统中的不确定性

调度：状态机的选择不确定

多处理器的 “选择” 是无法控制的
操作系统可以主动随机选择状态机执行一步

I/O：系统外的输入不确定

read 返回的结果也有两种可能性

这样程序的执行就不是 “一条线” 了

从初始状态出发，可能有多个可能的 “下一个状态”

《离散数学》忽然更有用了

程序定义了状态机 $G(V, E)$

加上一个起点 $v_0$
再加上 $F \subseteq V$ $F \subseteq V$ 表示“坏”（faulty）的状态。
- 程序正确 \iff 不存在从 $v_0$ 到 $v \in F$ 的路径。

还记得你们怎么在 $G$ 里找路径吗？

DFS / BFS 啊！
恭喜你！你离图灵奖进了一步（迈出了重要的第一步）
- 疯狂的想法：软件是可以自动证明的！
- Turing Award Lecture: Model checking: algorithmic verification and debugging

插曲：如果你想获得图灵奖？

需要找一个 tractable 的问题。

$F \subseteq V$ $F \subseteq V$ + 暴力枚举显然太 trivial 了。
- 我们有更好的方式表达规约 (temporal logic)：
- $G(A \to F B)$ $G (A \to F B)$
  - “如果 $A$ 发生，则最终 $B$ 会发生”。
  - 哦！你需要构建一个好的逻辑系统😭
- 提出一些有趣的检查算法

当问题规模增大时，暴力枚举所有状态或路径会指数级增长，计算上不可行，这就是 intractable（难解） 的问题。

Tractable 问题 是指存在 多项式时间算法 或其他可行方法可以求解的问题，比如通过逻辑规约、模型检查算法而不是暴力搜索就能验证程序正确性。

**在软件系统里又是 useful **

要走很多弯路，而且今天 temporal logic 也没落了，
但 Verification 没有死，而且在 AI 时代肯定会走得更远 🚀

验证软件正确性不能靠暴力枚举状态，需要用时序逻辑等形式化方法表达程序行为，并设计高效的检查算法。虽然 temporal logic 曾经没那么流行，但程序验证仍有价值，未来在 AI 时代会有更大发展空间。

Putting Them Together

模型

理论上，我们可以建模任何系统调用
当然，我们选择建模最重要的那些
- Three Easy Pieces!

检查器

最简单的 BFS 就行 (只要能获得状态机的状态)

可视化

我们就是绘制一个顶点是状态的图 $G(V,E)$

模块	系统调用	行为
基础	`choose(xs)`	返回一个 `xs` 中的随机选择
基础	`write(s)`	向调试终端输出字符串 `s`
基础	`sched()`	切换到随机的线程/进程执行
虚拟化	`fork()`	创建当前状态机的完整复制
并发	`spawn(fn)`	创建从 `fn` 开始执行的线程
持久化	`bread(k)`	读取虚拟磁盘块 `k` 的数据
持久化	`bwrite(k, v)`	向虚拟磁盘块 `k` 写入数据 `v`
持久化	`sync()`	将所有向虚拟磁盘的数据写入落盘
持久化	`crash()`	模拟系统崩溃

资源

正文