写在前面这是本系列的第四篇。操作系统是什么它就是直接运行在计算机硬件上的程序。内核被加载后拥有了完整的计算机控制权限包括中断和 I/O 设备因此它可以通过“障眼法”构造出多个应用程序同时执行的假象。但今天我们要换一个更加极其硬核、甚至有些烧脑的视角数学视角。抛开具体的代码程序到底是什么我们如何用严谨的数学去证明一个操作系统是绝对正确的内容回顾万物皆状态机程序 状态机GDB 里的单步执行step/next本质上就是我们在微观尺度上看着状态机发生了一次状态迁移。硬件 状态机CPU 的时钟周期跳动与指令执行就是硬件状态的不断迁移。操作系统 状态机的管理者毫无疑问OS 也是状态机而且它是一个用来管理其他状态机的“超级状态机”。成为 Power UserGDB 的终极调教AI Prompt 咒语“我在命令行中使用 gdb 调试。如果你是一位专业人士有更好的方法和建议吗尽可能全面。”在 AI 的加持下我们可以瞬间获得黑客级别的调试技巧。抛弃枯燥的print试试这些极客操作启用 TUI 模式 (终极杀器)输入gdb -tui或在 GDB 中按下CtrlXA可以在终端上方直接开启一个代码可视化窗口边看代码边调试。条件断点 (精准狙击)break location if condition。当循环执行一万次你只想看第 9999 次的状态时这是唯一的救命稻草。自动监视变量display variable。每次步进step时GDB 会自动为你打印这个变量的值不需要反复敲print。反汇编与底层观测disassemble查看当前函数的汇编代码结合info registers查看 CPU 寄存器状态。学习感悟不要卷 GPA把 AI 当成一个不厌其烦教你的专业私教。你的学习效率会极大提高因为留给人类的时间真的不多了。数学视角的计算机程序程序的本质是“数学严格”的对象程序 初始状态 迁移函数程序 ~ 数学对象在计算机科学中离散数学是不可或缺的。它提供了描述计算机世界的严谨数学语言。为什么会有程序因为程序必须在无情执行指令的机器上运行只有严谨的逻辑才配得上机器的无情。程序天生是“人类”的也是“反人类”的人类的一面程序连接了人类世界的需求如今的大语言模型LLM展现出了极其强大的编程能力。反人类的一面程序是在机器上执行的。大模型会产生幻觉人类小白也会产生幻觉“我的代码怎么看都是对的为什么输出就不对”。要想 100% 掌握程序的运行行为极其困难。可维护性 (Maintainability) 的终极定义什么是好的代码代码的字面意义必须和它的实际行为直接关联。Online Judge (算法刷题平台) 只会为你本次提交的正确性负责但不会保证 Maintainability。好的代码就像优秀的文章出了问题容易修别人读起来容易懂。软件危机我们能证明程序的正确性吗大模型能自动生产出看起来正确的代码。但是过不了测试用例一定是错的能过测试用例就一定是对的吗来看一段经典的计算二进制中1的个数的代码 (popcount)intpopcount(intx){intcount0;while(x){x-(x-x);count;}returncount;}极客解析x -x在底层的作用是提取出x的二进制表示中最低位的1其余位全部清零。减去它就能快速消灭所有的1。但问题来了这段程序真的 100% 绝对正确吗什么叫“对” (Specification)在数学意义上“正确”意味着不会 Crash (崩溃)没有 UB (Undefined Behavior未定义行为)满足所有的 Assert (断言)。如何证明程序 f 的正确暴力枚举写一个 Driver Code从-2147483648到2147483647全部跑一遍对于 32 位整数还能接受64 位就无能为力了。写出严谨的数学证明直接进行数学推导。“Proof Assistant” (交互式定理证明工具)如 Coq, Lean 等。它们会无情地拒绝你的一切伪证。核心哲学Curry-Howard 对应 (同构)计算机辅助证明揭示了数学证明与类型系统之间极其深刻的联系命题即类型 (Propositions as Types)逻辑中的命题如 $ A \rightarrow B $对应编程中的函数类型。证明即程序 (Proofs as Programs)命题的构造性证明过程就对应着实现该类型的一个具体程序。如果你能写出一个类型检查绝对通过的函数你就完成了一个严谨的数学证明这就是人工智能时代完美的辅助工具——如果我们不敢完全信任 AI 写的代码那就让 AI 给出一个 Proof Assistant 认可的证明吧操作系统 状态机的管理者操作系统作为一个“超级状态机”它可以同时容纳多个“程序状态机”。程序内计算选一个程序让它执行一步状态迁移。系统调用 (Syscall)提供创建新状态机、退出状态机、打印字符等服务。玩具操作系统用 Python 建立 OS 模型JYY 老师用一段优雅的 Python 代码展示了操作系统的本质。这里用到了一项核心特性生成器 (Generators / Coroutines)。在 Python 中使用yield关键字可以在函数执行过程中暂停并交出控制权。这完美契合了系统调用的本质当应用程序发起read或write时它yield出去操作系统内核接管控制权内核处理完后再让应用程序从暂停的地方继续往下跑。系统调用模型read(): 返回随机的 0 或 1。write(s): 向共享的 buffer 输出字符串。spawn(f): 创建一个新的状态机。你会在真实的 Linux Kernel 中看到类似的影子这里的procs列表对应着 Linux 内核中的cpu-runqueue(运行队列)。获取当前状态机对应着 Linux 中的current_thread_info()-task。短短 30 行 Python 代码就讲透了 UNIX 系统的基本模型进程、系统调用、上下文切换、调度。状态机模型与模型检查器 (Model Checker)现实中的计算机充满了不确定性 (Non-determinism)调度的不确定操作系统随机选择哪个进程执行下一步你无法预测。I/O 的不确定read()可能会返回任意结果。分支的不确定程序的执行不是一条直线而是一棵庞大的状态树。Mosaic 工具与并发编程的雷区通过构建这样的 Python 模型解释器 (mosaic)我们可以模拟真实的并发漏洞并发编程 (cond-var.py)互斥锁、条件变量的模拟。持久化异常 (fs-crash.py)模拟文件系统写到一半突然断电崩溃。TOCTTOU 漏洞 (tocttou.py)Time-of-check to time-of-use。这是一个极其经典的并发漏洞攻击者在系统“检查文件权限”和“真正打开文件”的微小时间差内利用并发机制偷偷把文件替换成了符号链接从而绕过权限控制。如何找到这些漏洞(检查器的原理)既然程序是状态图 $ G(V, E) $我们只需要写一个简单的BFS (广度优先搜索)遍历这棵状态树上所有可能的分支和未来如果在这几百万种平行的未来状态中有一个状态触发了 Assert 报错我们就抓住了这个并发 Bug。Take-away Messages (核心要义)程序就是状态机我们可以用图论、数理逻辑中的工具甚至是图遍历的方法去穷举、去探索、去证明程序的正确性。终极补课时序逻辑 (Temporal Logic)为了在数学上严谨地描述多线程和并发我们引入了时序逻辑。它允许我们描述和推理关于时间与未来的命题。1. 线性时序逻辑 (Linear Temporal Logic, LTL)将时间建模为一条单一的、无限延伸的路径。G(Globally总是)从当前时刻起系统永远不会 Crash。F(Eventually最终)从当前时刻起无论怎么调度线程最终一定能拿到锁。X(Next下一个)下一个状态一定满足条件。U(Until直到)电梯门一直保持开启直到有人按下关门键。2. 分支时序逻辑 (Branching Temporal Logic, CTL)将时间建模为一棵不断分叉的树完美对应多线程并发执行的各个平行宇宙。A(All)在所有可能的分支路径上都成立。E(Exists)至少存在一条路径成立比如是否存在一种恶意的并发调度序列能导致系统死锁只要 $ E $ 成立系统就不安全。有了这些严谨的逻辑符号我们就可以彻底驯服并发编程这头野兽从“试一试能不能跑”走向了“在数学上绝对正确”的计算机科学之巅。
南京大学 操作系统 (JYY) 学习笔记：数学视角下的操作系统与状态机模型
写在前面这是本系列的第四篇。操作系统是什么它就是直接运行在计算机硬件上的程序。内核被加载后拥有了完整的计算机控制权限包括中断和 I/O 设备因此它可以通过“障眼法”构造出多个应用程序同时执行的假象。但今天我们要换一个更加极其硬核、甚至有些烧脑的视角数学视角。抛开具体的代码程序到底是什么我们如何用严谨的数学去证明一个操作系统是绝对正确的内容回顾万物皆状态机程序 状态机GDB 里的单步执行step/next本质上就是我们在微观尺度上看着状态机发生了一次状态迁移。硬件 状态机CPU 的时钟周期跳动与指令执行就是硬件状态的不断迁移。操作系统 状态机的管理者毫无疑问OS 也是状态机而且它是一个用来管理其他状态机的“超级状态机”。成为 Power UserGDB 的终极调教AI Prompt 咒语“我在命令行中使用 gdb 调试。如果你是一位专业人士有更好的方法和建议吗尽可能全面。”在 AI 的加持下我们可以瞬间获得黑客级别的调试技巧。抛弃枯燥的print试试这些极客操作启用 TUI 模式 (终极杀器)输入gdb -tui或在 GDB 中按下CtrlXA可以在终端上方直接开启一个代码可视化窗口边看代码边调试。条件断点 (精准狙击)break location if condition。当循环执行一万次你只想看第 9999 次的状态时这是唯一的救命稻草。自动监视变量display variable。每次步进step时GDB 会自动为你打印这个变量的值不需要反复敲print。反汇编与底层观测disassemble查看当前函数的汇编代码结合info registers查看 CPU 寄存器状态。学习感悟不要卷 GPA把 AI 当成一个不厌其烦教你的专业私教。你的学习效率会极大提高因为留给人类的时间真的不多了。数学视角的计算机程序程序的本质是“数学严格”的对象程序 初始状态 迁移函数程序 ~ 数学对象在计算机科学中离散数学是不可或缺的。它提供了描述计算机世界的严谨数学语言。为什么会有程序因为程序必须在无情执行指令的机器上运行只有严谨的逻辑才配得上机器的无情。程序天生是“人类”的也是“反人类”的人类的一面程序连接了人类世界的需求如今的大语言模型LLM展现出了极其强大的编程能力。反人类的一面程序是在机器上执行的。大模型会产生幻觉人类小白也会产生幻觉“我的代码怎么看都是对的为什么输出就不对”。要想 100% 掌握程序的运行行为极其困难。可维护性 (Maintainability) 的终极定义什么是好的代码代码的字面意义必须和它的实际行为直接关联。Online Judge (算法刷题平台) 只会为你本次提交的正确性负责但不会保证 Maintainability。好的代码就像优秀的文章出了问题容易修别人读起来容易懂。软件危机我们能证明程序的正确性吗大模型能自动生产出看起来正确的代码。但是过不了测试用例一定是错的能过测试用例就一定是对的吗来看一段经典的计算二进制中1的个数的代码 (popcount)intpopcount(intx){intcount0;while(x){x-(x-x);count;}returncount;}极客解析x -x在底层的作用是提取出x的二进制表示中最低位的1其余位全部清零。减去它就能快速消灭所有的1。但问题来了这段程序真的 100% 绝对正确吗什么叫“对” (Specification)在数学意义上“正确”意味着不会 Crash (崩溃)没有 UB (Undefined Behavior未定义行为)满足所有的 Assert (断言)。如何证明程序 f 的正确暴力枚举写一个 Driver Code从-2147483648到2147483647全部跑一遍对于 32 位整数还能接受64 位就无能为力了。写出严谨的数学证明直接进行数学推导。“Proof Assistant” (交互式定理证明工具)如 Coq, Lean 等。它们会无情地拒绝你的一切伪证。核心哲学Curry-Howard 对应 (同构)计算机辅助证明揭示了数学证明与类型系统之间极其深刻的联系命题即类型 (Propositions as Types)逻辑中的命题如 $ A \rightarrow B $对应编程中的函数类型。证明即程序 (Proofs as Programs)命题的构造性证明过程就对应着实现该类型的一个具体程序。如果你能写出一个类型检查绝对通过的函数你就完成了一个严谨的数学证明这就是人工智能时代完美的辅助工具——如果我们不敢完全信任 AI 写的代码那就让 AI 给出一个 Proof Assistant 认可的证明吧操作系统 状态机的管理者操作系统作为一个“超级状态机”它可以同时容纳多个“程序状态机”。程序内计算选一个程序让它执行一步状态迁移。系统调用 (Syscall)提供创建新状态机、退出状态机、打印字符等服务。玩具操作系统用 Python 建立 OS 模型JYY 老师用一段优雅的 Python 代码展示了操作系统的本质。这里用到了一项核心特性生成器 (Generators / Coroutines)。在 Python 中使用yield关键字可以在函数执行过程中暂停并交出控制权。这完美契合了系统调用的本质当应用程序发起read或write时它yield出去操作系统内核接管控制权内核处理完后再让应用程序从暂停的地方继续往下跑。系统调用模型read(): 返回随机的 0 或 1。write(s): 向共享的 buffer 输出字符串。spawn(f): 创建一个新的状态机。你会在真实的 Linux Kernel 中看到类似的影子这里的procs列表对应着 Linux 内核中的cpu-runqueue(运行队列)。获取当前状态机对应着 Linux 中的current_thread_info()-task。短短 30 行 Python 代码就讲透了 UNIX 系统的基本模型进程、系统调用、上下文切换、调度。状态机模型与模型检查器 (Model Checker)现实中的计算机充满了不确定性 (Non-determinism)调度的不确定操作系统随机选择哪个进程执行下一步你无法预测。I/O 的不确定read()可能会返回任意结果。分支的不确定程序的执行不是一条直线而是一棵庞大的状态树。Mosaic 工具与并发编程的雷区通过构建这样的 Python 模型解释器 (mosaic)我们可以模拟真实的并发漏洞并发编程 (cond-var.py)互斥锁、条件变量的模拟。持久化异常 (fs-crash.py)模拟文件系统写到一半突然断电崩溃。TOCTTOU 漏洞 (tocttou.py)Time-of-check to time-of-use。这是一个极其经典的并发漏洞攻击者在系统“检查文件权限”和“真正打开文件”的微小时间差内利用并发机制偷偷把文件替换成了符号链接从而绕过权限控制。如何找到这些漏洞(检查器的原理)既然程序是状态图 $ G(V, E) $我们只需要写一个简单的BFS (广度优先搜索)遍历这棵状态树上所有可能的分支和未来如果在这几百万种平行的未来状态中有一个状态触发了 Assert 报错我们就抓住了这个并发 Bug。Take-away Messages (核心要义)程序就是状态机我们可以用图论、数理逻辑中的工具甚至是图遍历的方法去穷举、去探索、去证明程序的正确性。终极补课时序逻辑 (Temporal Logic)为了在数学上严谨地描述多线程和并发我们引入了时序逻辑。它允许我们描述和推理关于时间与未来的命题。1. 线性时序逻辑 (Linear Temporal Logic, LTL)将时间建模为一条单一的、无限延伸的路径。G(Globally总是)从当前时刻起系统永远不会 Crash。F(Eventually最终)从当前时刻起无论怎么调度线程最终一定能拿到锁。X(Next下一个)下一个状态一定满足条件。U(Until直到)电梯门一直保持开启直到有人按下关门键。2. 分支时序逻辑 (Branching Temporal Logic, CTL)将时间建模为一棵不断分叉的树完美对应多线程并发执行的各个平行宇宙。A(All)在所有可能的分支路径上都成立。E(Exists)至少存在一条路径成立比如是否存在一种恶意的并发调度序列能导致系统死锁只要 $ E $ 成立系统就不安全。有了这些严谨的逻辑符号我们就可以彻底驯服并发编程这头野兽从“试一试能不能跑”走向了“在数学上绝对正确”的计算机科学之巅。
