4. 数学视角的操作系统

背景回顾：在理解了 “软件 (应用)” 和 “硬件 (计算机)” 之后，操作系统就是直接运行在计算机硬件上的程序，它提供了应用程序执行的支撑和一组 API (系统调用)：操作系统内核被加载后，拥有完整计算机的控制权限，包括中断和 I/O 设备，因此可以构造出多个应用程序同时执行的 “假象”。

本讲内容：一个 Python “操作系统玩具” 的设计与实现，帮助大家在更高的 “抽象层次” 上理解操作系统的行为。这个 “玩具” 将贯穿整个课程。

4.1 程序正确性证明

没错，计算机科学和数学的发展速度可能超过大家的想象——我们有被 “证明正确” 的 编译器、操作系统内核；大家也可以阅读科普文章：

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 认可的证明吧！

4.2 为操作系统建模

4.3 数学视角的操作系统 🌶️

下面是我们绘制一个 “Hello World” 状态空间的例子。Hello 会调用一个有趣的系统调用 fork，它的行为是复制状态机的当前状态：

我们将会在这个学期的时间里，仔细分析模型和真实操作系统 (Linux) 系统调用的行为，并用它们实现很多有趣的程序。

Take-away Messages

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

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

课后习题/编程作业