1 程序正确性证明

数千年来，数学的“严格性”都是由人类保证的

1.1 程序的本质

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

  • Everything is a state machine

    • 程序 = 初始状态 + 迁移函数
    • 在这个视角下，程序和数学对象已经无限接近了

    f(s)=s′f(s) = s'

  • 我们经常写出 “似是而非” 的代码

  • 类似于细节有错但可以修正的数学证明

    • for (int j = 0; j < n; i++)
    • (有时候也会疏忽，导致设计全错)

为什么会有程序？

  • 是因为我们有无情的执行指令的机器 (计算机)
  • 只有程序才配得上它

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

  • 人类的一面：程序连接了人类世界需求
    • 程序写的一切都能在现实生活观测到
    • 我们并不是在实现 “uniform-random” 的 𝑓
  • 反人类的一面：程序会在机器上执行
    • 初学者对 “机器严格” 普遍不太适应
    • 部分原因是对程序的行为没有 100% 的掌控
    • 使用秘技：debug来观察程序的行为

1.2 当我们谈论数学的时候，我们想谈论什么？

证明程序正确性！

1
2
3
4
5
6
7
@dataclass
class AlipayAccount:
    b: int = 0  # Balance

    def deposit(...): ...
    def withdraw(...): ...
    def transfer(...): ...

针对这段python代码，我们可以用数学的语言提出程序的规约

  • 例如：任意时刻 a.b≥0a.b≥0
  • 有没有可能真正 “证明” 它呢？
    任意状态中b都大于0

证明方式

1.3 程序正确性证明的两种方法

暴力枚举-启发

  • 写一个 driver code，运行所有可能的函数调用序列，proof assistant 帮助我们检查
    • PL/SE 已经研究生成 driver code 几十年了
    • assert(b≥0)assert(b≥0)
  • 如果机器和 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
2
3
4
5
6
7
8
9
10
def StateMachine():
    b = sys_read()

    if b == 0:
        sys_write('I got a zero.')
    else:
        sys_write('I got a one.')

def main():
    sys_spawn(StateMachine)

系统调用

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

操作系统中的对象

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

因为 spawn 的存在，操作系统中有多个状态机 (进程)

1
2
# 可以拿到一个python模拟的状态机
wget -r -np -nH --cut-dirs=2 -R "index.html*" "https://jyywiki.cn/os-demos/introduction/os-model/"
1
2
3
4
5
6
7
8
#链接中的proc.py
def Process(name):
    for _ in range(5):
        sys_write(name)

def main():
    sys_spawn(Process, 'A')
    sys_spawn(Process, 'B')
  • 操作系统会 “雨露均沾” 地运行它们
  • 但 buffer 是所有状态机共享的
    • 于是有了并发……
    • 操作系统是最早的实用并发程序

3 数学视角的操作系统

状态

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

初始状态

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

迁移

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

3.1 计算机系统中的不确定性

ps: 算法定义：一个有穷的指令集，这些指令为解决某一特定任务规定了一个运算序列 （就是一个描述集，就是一个指令集，就是一个序列集）

调度：状态机的选择不确定（并发：反人类直觉的一个过程）

  • current = random.choice(self.procs)
  • 操作系统每次可以随机选择一个状态机执行一步

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

  • read 返回的结果也有两种可能性
  • t = sys_read() 后，可能 t=0 或 t=1

推论：我们得到了状态图

  • 𝑢→𝑣⇔𝑢𝑢→𝑣⇔𝑢 可以通过一步迁移到达 𝑣
  • 当然，我们只关心s0s_0可达的状态

Breadth-first search（广度优先算法）可以构建 “状态图”

maze.webp

3.2 蛮力法(Brute-force)

想要证明程序的性质？

  • 只要稍微 “修改” 一下模拟器的实现就行了

构建状态图，检查程序正确性

  • read()：创建两个状态，分别是 𝑟=0和 𝑟=1
  • 调度：为每个进程 𝑝 创建一个状态，对应选择 𝑝 执行
  • 程序正确：不存在从s0s_0可达的 “坏状态”
    • 例如：最终 buffer 中 A 和 B 的数量相同
    • “模型检查器”；Turing Award Lecture

c4-3.2-1.webp

1
2
#下面是我们绘制一个 “Hello World” 状态空间的例子。Hello 会调用一个有趣的系统调用 fork，它的行为是复制状态机的当前状态：
wget -r -np -nH --cut-dirs=2 -R "index.html*" "https://jyywiki.cn/os-demos/mosaic/mosaic/"

程序就是状态机；状态机可以用程序表示。因此：

  • 我们可以用更 “简单” 的方式 (例如 Python) 描述状态机、建模操作系统上的应用，并且实现操作系统的可执行模型。
  • 一旦把操作系统、应用程序当做 “数学对象” 处理，那么我们图论、数理逻辑中的工具就能被应用于处理程序——例如，可以用图遍历 “暴力枚举” 的方法证明程序的正确性。