4. 数学视角的操作系统
1 程序正确性证明
数千年来,数学的“严格性”都是由人类保证的
1.1 程序的本质
程序是一种 “数学严格” 的对象
-
Everything is a state machine
- 程序 = 初始状态 + 迁移函数
- 在这个视角下,程序和数学对象已经无限接近了
-
我们经常写出 “似是而非” 的代码
-
类似于细节有错但可以修正的数学证明
for (int j = 0; j < n; i++)
- (有时候也会疏忽,导致设计全错)
为什么会有程序?
- 是因为我们有无情的执行指令的机器 (计算机)
- 只有程序才配得上它
程序天生是 “人类” 的,也是 “反人类” 的
- 人类的一面:程序连接了人类世界需求
- 程序写的一切都能在现实生活观测到
- 我们并不是在实现 “uniform-random” 的 𝑓
- 反人类的一面:程序会在机器上执行
- 初学者对 “机器严格” 普遍不太适应
- 部分原因是对程序的行为没有 100% 的掌控
- 使用秘技:debug来观察程序的行为
1.2 当我们谈论数学的时候,我们想谈论什么?
证明程序正确性!
1 |
|
针对这段python代码,我们可以用数学的语言提出程序的规约
- 例如:任意时刻
- 有没有可能真正 “证明” 它呢?
任意状态中b都大于0
1.3 程序正确性证明的两种方法
暴力枚举-启发
- 写一个 driver code,运行所有可能的函数调用序列,proof assistant 帮助我们检查
- PL/SE 已经研究生成 driver code 几十年了
- 如果机器和 driver 都没有 bug,程序就是对的
写出证明-启发
- 我们可以多写
assert
断言来避免出错 - For all 𝑓 - reachable states, b≥0 holds.
- 为 𝑓 写一份数学证明就行了
- 就像你在上数学课时做的习题一样
没错,计算机科学和数学的发展速度可能超过大家的想象——我们有被 “证明正确” 的 编译器、操作系统内核;可以阅读科普文章:
Formal verification doesn’t result in perfect code; it simply narrows the possibility for errors and vulnerabilities to creep in, ” Parno says. “What makes the technique so attractive is that you push the uncertainty or scope of problems down to smaller and smaller windows.
同时,proof assistant 也是人工智能时代堪称完美的辅助工具:如果我们要信任 AI 产生的结果,就让它们给出一个 proof assistant 认可的证明吧!
2 为操作系统建模
2.1 操作系统的两个视角
应用视角 (自顶向下)
- 操作系统 = 对象 + API
- 应用通过
syscall
访问操作系统
- 应用通过
机器视角 (自底向上)
- 操作系统 = C 程序
- 运行在计算机硬件上的一个普通程序
2.2 为操作系统建模
操作系统 = 状态机的管理者(状态机的容器)
- 当然,它自己也是状态机,有自己的状态
有了一个有趣的想法……
- 能不能我们自己定义 “状态机”
- 用我们喜欢的语言、喜欢的方式
- 不要受限于 C、汇编……
- 自己模拟状态机的执行
- 形成一个 “玩具操作系统”
简化的操作系统模型
- 用更方便的编程语言描述状态机
- 依然是程序
- 依旧是 “数学严格” 的对象
- 但用更简单的方法实现操作系统
- 管理状态机
- 执行系统调用
2.3 表示状态机
1 | def StateMachine(): |
系统调用
- read(): 返回随机的 0 或 1
- write(s): 向 buffer 输出字符串
s
- spawn(f): 创建一个可运行的状态机
f
操作系统中的对象
- 状态机 (进程)
- Python 代码
- 初始时,仅有一个状态机 (main)
- 允许执行计算或 read, write, spawn 系统调用
- 一个进程间共享的 buffer (“设备”)
因为 spawn 的存在,操作系统中有多个状态机 (进程)
1 | # 可以拿到一个python模拟的状态机 |
1 | #链接中的proc.py |
- 操作系统会 “雨露均沾” 地运行它们
- 但 buffer 是所有状态机共享的
- 于是有了并发……
- 操作系统是最早的实用并发程序
3 数学视角的操作系统
状态
- 多个 “应用程序” 状态机
- 当然,可以是模型
初始状态
- 仅有一个 “main” 状态机
- 这个状态机处于初始状态
迁移
- 选择一个状态机执行一步
- 就像我们在操作系统模型上看到的那样
3.1 计算机系统中的不确定性
ps: 算法定义:一个有穷的指令集,这些指令为解决某一特定任务规定了一个运算序列 (就是一个描述集,就是一个指令集,就是一个序列集)
调度:状态机的选择不确定(并发:反人类直觉的一个过程)
current = random.choice(self.procs)
- 操作系统每次可以随机选择一个状态机执行一步
I/O:系统外的输入不确定
- read 返回的结果也有两种可能性
t = sys_read()
后,可能 t=0 或 t=1
推论:我们得到了状态图
- 可以通过一步迁移到达 𝑣
- 当然,我们只关心可达的状态
Breadth-first search(广度优先算法)可以构建 “状态图”
3.2 蛮力法(Brute-force)
想要证明程序的性质?
- 只要稍微 “修改” 一下模拟器的实现就行了
构建状态图,检查程序正确性
- read():创建两个状态,分别是 𝑟=0和 𝑟=1
- 调度:为每个进程 𝑝 创建一个状态,对应选择 𝑝 执行
- 程序正确:不存在从可达的 “坏状态”
- 例如:最终 buffer 中 A 和 B 的数量相同
- “模型检查器”;Turing Award Lecture
1 | 下面是我们绘制一个 “Hello World” 状态空间的例子。Hello 会调用一个有趣的系统调用 fork,它的行为是复制状态机的当前状态: |
程序就是状态机;状态机可以用程序表示。因此:
- 我们可以用更 “简单” 的方式 (例如 Python) 描述状态机、建模操作系统上的应用,并且实现操作系统的可执行模型。
- 一旦把操作系统、应用程序当做 “数学对象” 处理,那么我们图论、数理逻辑中的工具就能被应用于处理程序——例如,可以用图遍历 “暴力枚举” 的方法证明程序的正确性。