【NJU OS】04 理解并发程序执行

Peterson 算法

A 和 B 争用厕所的包厢

想进入包厢之前，A/B 都要先举起自己的旗子

• A 确认旗子举好以后，往厕所门上贴上 “B 正在使用” 的标签
• B 确认旗子举好以后，往厕所门上贴上 “A 正在使用” 的标签
• 然后，如果对方的旗子举起来，且门上的名字不是自己，等待
  • 否则可以进入包厢
• 出包厢后，放下自己的旗子

证明

• 枚举状态机
  • 可以忽略对称状态（类似剪枝）

(自动) 画状态机理解并发程序

• Python
  • 容易 hack 的动态语言
  • 丰富的库函数
• 死循环也能返回？
  • yeild
• Generator: 也是状态机

Model Checker

Model checker 的一切就是状态机！

• Safety: 红色的状态不可到达
  • G(V,E) 上的可达性问题
• (Strong) Liveness: 从任意状态出发，都能到达绿/蓝色状态
  • G(V,E) 上的什么问题？
• 如何展示这个状态机？
• 如何能避免无效的探索？

工具的故事

没有人能阻止程序员写 bug，但工具可以。

至今为止我们用过的自动化工具 (他们拯救了你无数次)

Type safety check

• -Wall -Werror
• Differential testing
• Model checker
• ……

这门课的另一个 take-away

• 操作系统是一个巨大的工程
• 没有工具 (编程、测试、调试……)，不做系统