04 - Mathematical Perspectives on Operating Systems

04 - 数学视角的操作系统

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

1. 内容回顾

1.1. 程序 = 状态机

  • gdb 为例 - 状态改变

1.2. 硬件 = 状态机

  • 指令执行 = 状态迁移

1.3. 操作系统 = 状态机

毫无疑问

2. 数学视角的计算机程序

2.1. 程序的本质

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

  • 程序 = 初始状态 + 迁移函数

  • 程序 ~ 数学对象

2.2. 离散数学

其实应该拆成两件

  • 计算机科学的数学基础

  • 结构

离不开用数学语言去描述计算机世界...

离散数学真的重要吗？...

2.3. 再看程序的本质

为什么会有程序？

  • 程序必须在无情执行指令的机器上执行

  • 只有程序才配得上它

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

  • 人类：程序连接了人类世界需求

    • 大模型强大的编程能力

  • 反人类：程序在机器上执行

    • 大模型有幻觉

    • 对程序的行为 100% 掌握非常困难

跟小白人类一样：

你感觉你的程序怎么看都是对的，但是就是不能按要求输出...

“Maintianability”：代码字面意义和实际行为直接关联

online judge 只会为本次提交负责，但是不会保证 maintain...

总之就是没有可维护性...

  • 出了问题修起来容易

  • 别人读起来容易...

  • 代码就像文章...可以阅读...保证字面意义 == 实际行为

2.4. 软件危机

AI...等能自动生产出绝对正确的代码！

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

过不了测试用例就一定是错的，但是能过测试用例，就一定是对的吗？？？

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

上面程序是对的吗？

什么叫对？

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

  • 没有 undefine behavior

2.6. 证明程序 f 的正确

暴力枚举

  • 写一个 driver code

写出证明

直接证明

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

计算机辅助证明并不是一个新概念：我们不再用自然语言，而是用严格的、机器可检查的逻辑语言书写证明，核心技术是揭示了数学证明与类型系统之间的深刻联系的 Curry-Howard Correspondence：

  1. 命题即类型：逻辑中的命题 (如 A→B) 对应函数类型 A→B。

  2. 证明即程序：命题的构造性证明过程对应该类型的一个具体程序（例如，一个实现 A→BA→B 的函数即为 “A 蕴含 B” 的证明）。

逻辑中的蕴含消除规则对应函数调用：若有一个类型为 A→B 的函数 (证明)，且输入类型 A 的值 (前提)，则输出类型 B 的值 (结论)。而对于一阶谓词，例如 ∃x.P(x)，就必须提供一个 x 的实例，这构成了基于构造的 “直觉逻辑” 的基础。

Proof assistant 是人工智能时代堪称完美的辅助工具：如果我们要信任 AI 产生的结果，就让它们给出一个 proof assistant 认可的证明吧！延伸阅读：科普文章: “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”

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

3.1. 可以同时容纳多个“程序状态机”

  • 程序内计算：选一个程序执行一步

  • 系统调用：创建新状态机、退出状态机、打印字符......

3.2. 有了一个有趣的想法...

  • 定义我们自己的状态机

    • 喜欢的语言、喜欢的方式

  • 自己模拟状态机的执行

    • 玩具操作系统

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

3.3. Python 程序表示状态机 - 玩具操作系统

review：

在主程序：

  • 定义一个 OS 类，内部模拟了进程的：read、write、spawn...

    • __init__方法：

      • 执行传入的源代码，使其成为运行的一部分

      • 初始化一个 main 进程

    • run 方法

      • 模拟操作系统的主循环，随机选择一个进程运行

      • 根据系统调用的类型，执行相应的操作

      • 如果进程运行结束，从进程列表中移除

  • 定义一个 Process 类，初始化 generator，step 恢复进程

  • 读取传入的程序文件：hello.py or proc.py

  • 将程序中的系统调用替换为 yield 语句

  • 创建操作系统模型并运行程序

对象

  • 状态机（进程）

    • 初始状态，仅有一个状态机 main

    • 允许执行计算或 read，write，spawn 系统调用

  • 一个进程间共享的 buffer（“设备”）

系统调用

  • read(): 返回随机的 0 或 1

  • write(s): 向 buffer 输出字符串 s

  • spawn(f): 创建一个可运行的状态机 f

多状态机的管理

  • 如何在状态机之间来回切换

  • 实现我们单 CPU 上运行多个程序的效果

  • 每个程序可以看作是一个状态机，状态机的状态包括程序的当前执行位置、寄存器的值、内存状态等

一些途径

  • 用一个模拟器去解释执行语句 (2022 年的实现)

    • 创建多个模拟器对象单步执行 (J2ME KVM 就是如此) Java 2 Micro Edition KVM

      • 每个对象负责解释执行一个程序的语句。每个模拟器对象可以看作是一个独立的“虚拟CPU”，它会逐步执行程序的指令

    • “虚拟机” (QEMU TCG)

      • 虚拟机是一种更高级的模拟器，它可以在一个物理CPU上模拟多个虚拟CPU。

  • 是否有语言机制能 “暂存” 函数的运行状态，并且之后回复？

    • 有：Generators/Coroutines

      • 在Python中，生成器是一种特殊的函数，使用 yield 关键字可以在函数执行过程中暂停，并返回一个值。下次调用生成器时，函数会从上次暂停的地方继续执行

      • 协程是一种更通用的机制，允许函数在执行过程中暂停和恢复。Python中的 async 和 await 关键字就是协程的实现

    • DeepSeek-R1 几乎做对了 (给了一个 99% 正确的代码)

3.4. 30 行代码讲完 UNIX 系统的基本模型

  • 进程

  • 系统调用

  • 上下文切换

  • 调度

    • 为什么会有调度？

    • 有哪些调度算法？

3.5. 你会在 Linux Kernel 中看到 “类似” 的代码

  • “procs” → cpu->runqueue

  • “current” → current = (current_thread_info()->task)

  • 通过课上的 python 模型，慢慢理解 操作系统的东西

3.6. 打开并发程序的大门

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

  • 每个进程（程序）都是顺序状态机

    • 发生中断/系统调用后，操作系统代码直接执行

    • 如果有多个处理器（或者允许此时切换到另一个程序执行），就有了并发

  • 并发编程的困难...

4. 状态机模型与模型检查器

review:

  • mosaic/mosaic.py

    • 系统调用定义: 9个

    • 操作系统类 OperatingSystem：初始化、系统调用、状态转换、状态序列化

    • Mosaic 类：模型解释器和检查器、源代码解析和重写：主要是加上了 yield 关键字

  • mosaic/examples/concurrency/cond-var.py并发编程

    • Tworker 函数：工作线程的逻辑，互斥锁、条件变量...

    • main 函数：初始化共享堆的状态，创建生产者和消费者线程

  • mosaic/examples/virtualization/fork-buf.py虚拟化编程

    • main 函数：初始化共享堆的缓冲区

  • mosaic/examples/persistence/持久化编程

    • xv6-log.py模拟了 xv6 文件系统的日志机制。

      • 初始化日志头，记录写入操作，模拟系统崩溃，恢复日志，安装事务，更新日志头

    • tocttou.py模拟了 TOCTTOU（Time-of-check-to-time-of-use）漏洞。

      • 初始化文件系统，多次调用 sys_fork 创建子进程，攻击者进程创建符号链接，发送邮件进程检查文件类型并写入邮件

    • fs-crash.py模拟了文件系统的崩溃和恢复过程。

      • 初始化文件系统，追加新的数据块，模拟系统崩溃，恢复文件系统状态并输出

4.1. 计算机系统中的不确定性（non-determinism）

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

  • 多处理器的选择是无法控制的

  • 操作系统可以主动随机选择状态机执行一步

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

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

程序的执行不是一条线

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

4.2. 模型

  • 理论上，我们可以建模任何系统调用

  • 当然，我们选择建模最重要的那些

    • Three Easy Pieces!

4.3. 检查器

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

4.4. 可视化

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

Take-away Messages

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

5. 补课：Temporal Logic（时序逻辑或时态逻辑）

补课

时序逻辑是一种扩展了经典逻辑的逻辑系统，它引入了时间的概念，允许我们描述和推理关于时间的命题。它不仅可以描述当前的状态，还可以描述过去、现在和未来的状态。

5.1. 线性时序逻辑（Linear Temporal Logic, LTL）

线性时序逻辑将时间建模为一条单一的、无限延伸的路径（状态序列），称为计算路径。它主要用于描述单个计算路径上的性质。

时间操作符

  • G （Globally，总是）：从当前时刻起，某个命题始终为真。

  • F （Eventually，最终）：从当前时刻起，某个命题在未来某个时刻为真。

  • X （Next，下一个）：某个命题在下一个时刻为真。

  • U （Until，直到）：某个命题一直为真，直到另一个命题为真。

5.2. 分支时序逻辑（Branching Temporal Logic, CTL）

分支时序逻辑将时间建模为一棵树，每个节点代表一个状态，每个分支代表一个可能的计算路径。它主要用于描述多个计算路径上的性质。

  • A （All）：对所有路径都成立。

  • E （Exists）：至少存在一条路径成立。

  • G （Globally，总是）：从当前时刻起，某个命题始终为真。

  • F （Eventually，最终）：从当前时刻起，某个命题在未来某个时刻为真。

  • X （Next，下一个）：某个命题在下一个时刻为真。

  • U （Until，直到）：某个命题一直为真，直到另一个命题为真。

Previous03 - Hardware Perspective on Operating SystemsNext05 - Programs and processes

Last updated