【NJU OS】10 状态机模型的应用

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

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

C=compile(S)

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

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

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

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

查看状态机执行

Trace 和调试器

程序执行 = 状态机执行

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

应用 (1): Time-Travel Debugging

应用 (2): Record & Replay

总结

• 编程 (状态机) 就是全世界
• 状态机可以帮我们
  • 建立物理世界的公理体系
  • 理解调试器、Trace, profiler
  • 自动分析程序的执行 (model checker)