本文最后更新于：2 年前

状态机是一种思维方式，一种视角，一种很重要的工具！通过它，可以看到很多研究后面，最重要的思想！！！所有的东西都是状态机！！！状态机拓展！！！惊人的威力！！！

状态机复习

状态机：理论
- 数字电路：logisim.c 和 seven-seg.py -> 模拟底层电路，logisim.c的输出，可以作为seven-seg.py的输入，很酷！！！晶体二极管！！！所有底层的硬件，都是状态机！！！ -> Computer就是状态机。
- Model checker: 理解并发程序执行的新方法，模拟状态机的状态，从而推导出不符合逻辑的并发状态 -> 找到Bug
状态机：实践
- thread-os.c

本次课回答的问题

Q: 状态机模型如此有用，还能更有用一点吗？

本次课主要内容

终于做完了铺垫，是时候让你感受到 “真正的力量” 了
- 都是没用的内容，当我口胡就行了

状态机：理解我们的世界

我们的物理世界是 “确定规则” 的状态机吗？

宏观物理世界近似于 deterministic 的状态机 (经典力学)
微观世界可能是 non-deterministic 的 (量子力学)

物理数据的状态机 & 状态机的状态机

把物理世界建模成基本粒子的运动

Conway’s game of life

可以在这个模型上严肃地定义很多概念：预测未来、时间旅行……

成为你理解物理 (和计算机) 世界的参考

例子

Cellular automata 不支持 “时间旅行”
- 怎么添加一个公理使它可以支持？
  - 平行宇宙
  - 如果世界线需要合并？可以收敛于某个分布

公理体系下，是可以严谨的定义，“回到过去”，这种特殊的状态机，造成状态的分叉的。（平行宇宙！）

Cellular automata 不支持 “预测外来”
- 能否添加一个 syscall 使它支持？
  - Why philosophers should care about computational complexity, Ch. 10

上面这种情况也是，一个时间单位，预测后面很久时间单位后的状态机。把连续的时间 -> 一格一格的帧，进行预测！！！

状态机模型：理解编译器和现代 CPU

编译器：源代码 S (状态机) → 二进制代码 C (状态机)

编译器无非是对于不同层面的状态机转换！保持转换过程中，语意一致。

转换过程中，CPU就可以知道，完全可以一个时钟周期之内，执行两条 or 多条可并行的指令。（instruction-level parellism）

编译 (优化) 的正确性 (Soundness):

S 与 C 的可观测行为严格一致
- system calls; volatile variable loads/stores; termination

超标量 (superscalar)/乱序执行处理器

允许在状态机上 “跳跃”
ilp-demo.c

上面这个例子，用执行的指令的数量 / 执行时间，和CPU的时钟周期做对比。发现CPU为4.2GHz，但是执行的指令数量为17GHz左右。也就是说，一个时钟周期内，执行了很多条可以并行的执行昂！（需要绑定到一个CPU来执行，这个结果才有意义昂！！！）

查看状态机的执行

状态机解释程序/编译器理解：

程序执行（逻辑） = 状态机执行（实际），有点像代码和进程的感觉，比进程还深入，在底层硬件设备和软件环境上，是如何执行的！

我们能不能 “hack” 进这个状态机
- 观察状态机的执行
  - strace/gdb
- 甚至记录和改变状态机的执行

调试过程本质就是启动了一个状态机啊！！！帮助我们查看一个状态，甚至能够帮助我们，通过指令进行状态间的转换。Debug本身就是在和状态机打交道哇！！！

以状态机的视角来理解GDB，很多想法，

既然是状态转换，为什么不可以回溯呢？

为什么不可以保存状态，后面接着调试呢，反正就是状态+状态流转而已啊。。。

为什么不能记录整个状态机的一次执行呢？

状态机上能干的事情，GDB为啥不能干呢？（为啥我每次错过了断点，还要重新开始啊orz呜呜呜，不能回溯，早有疑问了。）

应用一(Time-Travel Debugging)

记录每一个状态（状态机太大了！！！）

但是每一条指令的作用域有限！

初始化状态 + 指令对于状态机的改变（？？？有点像MySQL中，数据持久化那一块儿，redo log的设计了）

#include <stdio.h>
#include <stdint.h>

int main() {
  uint64_t val;
  asm volatile ("rdrand %0": "=r"(val));
  printf("rdrand returns %016lx\n", val);
}

随机数每次不一样，反复执行不一样，可能导致Bug没法复现了呜呜呜！！！有很大的问题！！！GDB的回溯很重要昂！！！

GDB的回溯功能的打开：
- record full命令：打开记录的模式
- rsi就可以往回执行（因为每一条指令，GDB都记录了diff，就可以回退昂！！！） -> 状态机的威力！！！啥啥都是状态机！！！

gdb 的隐藏功能 (大家读过 gdb 的手册了吗？)

record full - 开始记录
record stop - 结束记录
reverse-step/reverse-stepi - “时间旅行调试”

例子：调试 rdrand.c

Reverse execution 不是万能的
- 有些复杂的指令 (syscall) 无法保证

应用二(Record & Replay)

在程序执行时记录信息，结束后重现程序的行为

确定的程序不需要任何记录
- 假设s0执行 1,000,000 条确定的指令后得到s‘
  - 那么只要记录 s0和 1,000,000
  - 就能通过 “再执行一次” 推导出 s’

执行结果确定的指令，不用记录。

执行结果非确定的指令，记录下来。

记录（确定结果的指令数+非确定结果的指令的运行结果） -> 得到一个确定的状态机昂！！！

多处理器和并发线程也可以的！！！ -> 只要加下来所有的上锁和解锁的顺序，包括条件变量等同步操作的顺序。 -> 程序的执行，可以完整的重现出来！！！

Record & Replay: 只需记录 non-deterministic 的指令的效果

(单线程) 应用程序
- syscall, rdrand, rdtsc, …
- rr (Mozilla)
  - To catch a failure: The record-and-replay approach to debugging (CACM’20)
(单处理器) 操作系统
- mmio, in, out, rdrand, rdtsc, 中断, …
- QEMU (-icount shift=auto,rr=record,rrfile=replay.bin)
  - ReVirt: Enabling intrusion analysis through virtual-machine logging and replay (OSDI’02, Best Paper 🏅) -> 重放整个虚拟机的执行！！！比如时间啊之类的不确定的值的操作，对于程序中对应的操作（比如读取当前时钟），直接替换成我们记录的结果就可以重放啦！！！

拓展一步，那不止是重放程序，重放操作系统的执行呢？重放整个操作系统的执行：绝大多数的指令都是确定的，不需要记录的。记录不确定的结果：IO，中断。 -> 自然就可以重放操作系统了嗷，思路和程序都是一致的！！！

situation -> determinitic instructions -> uncertain instructions’ results -> determinitic instructions -> uncertain instructions’ results -> …… -> final same results

采样状态机执行

管理性能优化

Premature optimization is the root of all evil. (D. E. Knuth)

那到底怎么样才算 mature 呢？-> 理解真实环境中，状态机的执行。只有知道了哪里有性能瓶颈，才能谈优化。

状态机的执行需要时间；对象需要占用空间
需要理解好 “时间花在哪里”、“什么对象占用了空间”

我们需要真实执行的性能摘要！

本质的回答：“为了做某件事到底花去了多少资源”
简化的回答：“一段时间内资源的消耗情况”

减少程序的侵入性，不用debug一步一步走，也检测不到具体的性能。（比如某条语句的执行时间）

Profiler和性能摘要：性能摘要需要对程序执行性能影响最小，往往不需要 full trace。

隔一段时间 “暂停” 程序、观察状态机的执行（利用操作系统的中断！！！）

中断就可以做到
将状态s→s′，“记账”：
- 执行的语句
- 函数调用栈
- 服务的请求
得到统计意义的性能摘要

例子：Linux Kernel perf (支持硬件 PMU) - ilp-demo.c

perf list, perf stat (-e), perf record, perf report

e.g. perf stat ./a.out

e.g. perf record ./a.out -> perf report（可以看到具体的报告，点进去具体的报告就可以看到统计信息）。e.g.

上面红色的就是耗时最长的昂！！！

perf list可以展现出来，其实我们的perf有很多的功能昂，都可以看看捏！！！

Perf能够告诉你哪里去优化
- 但是优化可能会带来，可读性，可维护性啊，等很多的bugs.

我们遇到的大部分情况

二八定律：80% 的时间消耗在非常集中的几处代码
Lab1 (pmm): 小内存分配时的 lock contention
- profiler 直接帮你解决问题

工业界遇到的大部分情况

木桶效应：每个部分都已经 tune 到局部最优了
- 剩下的部分要么 profiler 信息不完整，要么就不好解决
- (工程师整天都对着 profiler 看得头都大了)
- The flame graph (CACM’16) -> 火焰图，好工具！

Model Checker/Verifier

帮我们探索整个状态机，寻找程序的运行空间和边界，帮助我们调试。

150 行代码的 model-checker.py

证完所有《操作系统》课上涉及的并发程序
复现 OSTEP 教科书上的并发 bug (条件变量错误唤醒)

一些真正的 model checkers

TLA+ by Leslie Lamport; -> Amazon用来检验分布式程序的正确性。（分布式程序也是并发程序嘛（但是并发的程序甚至会直接寄））
Java PathFinder (JPF) 和 SPIN
- 它们都喜欢用 Peterson 算法做 tutorial 😁
- 上面的是在实践中可以直接用的，甚至不需要自己对于代码模型进行建模。

Model Checker: 不仅是并发

任何 “non-deterministic” 的状态机都可以检查

u32 x = rdrand();
u32 y = rdrand();
if (x > y)
  if (x * x + y * y == 65)
    bug();
...
assert(ptr); // 可能空指针吗？

上面这种，所有的状态机，太大啦。一层就是2^32个状态，很离谱的！！！状态减少（减枝）

求出上面的状态之后，就能够通过约束求解器，找出结果，x = 8, y = 1之类的。

状态机不仅能够理解程序的执行，还能够证明程序的正确性。 -> 非常重要，比如可以自动生成对应的测试用例！！！ -> 形式化验证？？？

更高效的 Model Checker: “将相似状态合并”

KLEE: Unassisted and automatic generation of high-coverage tests for complex systems programs (OSDI’08, Best Paper 🏅)
基于 LLVM bitcode 解释器实现

Model Check不只是并发，可以检查任务程序！！！单线程也可以检查啊，不同类型的Input，本质上就对应了不同的执行空间。

References

视频链接：https://www.bilibili.com/video/BV1xU4y1Z7xK/?spm_id_from=333.999.0.0&vd_source=ff957cd8fbaeb55d52afc75fbcc87dfd
gdb调试过程中，layout asm是以底层汇编的形式执行，layout src是以c语言的形式展示，C的执行形式。
课件：http://jyywiki.cn/OS/2022/slides/10.slides#/2/3

南京大学操作系统

#研0自学

NJUOS-10-状态机模型的应用

https://alexanderliu-creator.github.io/2022/12/21/njuos-10-zhuang-tai-ji-mo-xing-de-ying-yong/

作者

Alexander Liu

发布于

2022年12月21日

许可协议

NJUOS-11-操作系统上的进程上一篇

NJUOS-9-操作系统的状态机模型下一篇