学习# OS# 南京大学《操作系统原理》

OS-数学视角的操作系统

学习自 B 站 UP 主绿导师原谅你了。

资源

正文

4. 数学视角的操作系统

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

4.1 数学视角的计算机程序

程序的本质

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

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

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

webp

为什么会有程序？

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

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

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

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

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

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

我们还需要 “什么叫对”

  • Specification: 不 crash; 没有 UB; assert satisfy, ...

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

  • 程序不会崩溃；
  • 不触发未定义行为（UB, Undefined Behavior）；
  • 对所有输入都满足断言（assert）中描述的语义条件。
C
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）。

所以：

  1. 要证明 popcount 正确，必须先定义它“正确”的含义（specification）。
  2. 定义完后，才能用逻辑（如循环不变式）证明它满足这个规范。

证明程序 ff 正确

暴力枚举

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

写出证明

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

我们希望像数学家证明定理那样，严格地证明一个程序 f 是正确的。也就是说，不只是“我测试了很多样例，看起来没错”，而是要在 数学逻辑系统 中，写出一份严密的形式化证明：

∀x.  spec(x,f(x))∀x.\; \text{spec}(x, f(x))

即对所有输入 xx，程序 ff 的输出满足规范（specification）。

“Proof Assistant” (Coq, Lean, ...)

这里指的是一类交互式定理证明器（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：

python
#!/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：

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

命令行中：

shell
python os-model.py hello.py
x = 1110101001b

打开并发程序的大门

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

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

创建一个 proc.py：

python
def Process(name):
    for _ in range(5):
        sys_write(name)
 
def main():
    sys_spawn(Process, 'A')
    sys_spawn(Process, 'B')

之后执行：

shell
python os-model.py proc.py
ABABBBABAA

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

数学视角的操作系统

状态

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

初始状态

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

迁移

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

计算机系统中的不确定性

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

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

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

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

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

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

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

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

  • 加上一个起点 v0v_0
  • 再加上 F⊆VF \subseteq V 表示“坏”（faulty）的状态。
    • 程序正确   ⟺  \iff 不存在从 v0v_0 到 v∈Fv \in F 的路径。

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

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

需要找一个 tractable 的问题。

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

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

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

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

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

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

Putting Them Together

模型

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

检查器

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

可视化

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