状态机模型的应用

回顾

• 状态机理论

  • 数字电路

  • Model checker：理解并发程序执行的新方法

• 状态机实践

  • thread-os.c

这些都是理论上的结果。上一章，见了机器的启动，也可以用状态机来理解。

既然状态机模型这么有用，能不能更有用一点。

惊人的威力，这些内容属于思路扩展，而非操作系统教材上的东西。

状态机模型：帮助理解真实世界

物理世界是“确定规则”的吗？

物理世界理解状态机，反过来状态机理解物理世界。

能不能把物理世界的状态表达出来？

生命游戏，被证明是图灵完备的，即所有再计算机上可以写出来的东西都能在此实现。

在状态机模型上尝试解释物理世界。可以在这个模型上定义更多的概念：预测未来、时间旅行。还是从 Game of life 来看，这使得状态机出现了新的分支。

需要添加一个公里使它可以支持

• 平行宇宙(新的状态机分支)可以从数学上严格定义出来

• 如果世界线需要合并？

···

最主要的，用状态机理解编译器和现代 CPU。第一节内容。

编译器就是让源代码S状态到二进制代码C状态机，syscall 到 syscall 的翻译都保持相同，除此之外可以做任何事情。

CPU 在内部实现此状态机时只要让状态机的执行结果看起来一样就行，不需要按照状态极模型的定义一样每个周期执行一次。

这就是超标量/乱序执行CPU。

可以写个程序来测试。

查看状态机执行

状态机想法在程序调试的应用。

程序执行 = 状态机执行

我们能不能看到这个状态机里的状态，观察状态机的执行，甚至改变状态，干预其执行。

strace/gdb

前面那个程序

strace ./a.out
strace -T ./a.out | vim - #输出到vim，系统调用花的时间

vim 设置 :set nowrap

源程序调用了 clock 函数，C语言里，时间戳这个概念时不存在的，肯定调用了系统调用。通过 strace 可以看到调用了 clock_gettime 获得了时间戳，还能看到调用了 write

如果想看到所有的过程，可以使用gdb

gcc -O2 ilp-demo -g
gdb a.out

• start

• layout src

• n 或者 s 调式

调试器不仅仅是语句和汇编指令的展示，而是展示的状态机。gdb 停下来，是停在个状态上。走一步就是前进一个状态。

在时间上后退。程序的执行序列 $s0 \to s1 \to \cdots$

记录所有的栈和寄存器状态不太靠谱，因此只记录初始状态和前后状态的 diff。这个功能并不麻烦，gdb里已经有了。