Operating System Chapter10 状态机模型的应用
Operating System
$Nanjing\ University\rightarrow Yanyan\ Jiang\newline$
Overview
复习
- 状态机:理论
- 数字电路:logisim.c 和 seven-seg.py
- Model checker: 理解并发程序执行的新方法
- 状态机:实践
本次课回答的问题
- Q: 状态机模型如此有用,还能更有用一点吗?
本次课主要内容
- 终于做完了铺垫,是时候让你感受到 “真正的力量” 了
- 都是没用的内容,当我口胡就行了
状态机:理解我们的世界
哲 ♂ 学探讨
-
我们的物理世界是 “确定规则” 的状态机吗?
-
宏观物理世界近似于 deterministic 的状态机 (经典力学)
-
微观世界可能是 non-deterministic 的 (量子力学)
-
把物理世界建模成基本粒子的运动
- Conway’s game of life $\Longrightarrow$ Turing Complete
哲 ♂ 学探讨 (cont’d)
可以在这个模型上严肃地定义很多概念:预测未来、时间旅行……
- 成为你理解物理 (和计算机) 世界的参考
- 例子
- Cellular automata 不支持 “时间旅行”
- 怎么添加一个公理使它可以支持?
- 平行宇宙
- 如果世界线需要合并?可以收敛于某个分布
- 怎么添加一个公理使它可以支持?
- Cellular automata 不支持 “预测外来”
- 能否添加一个 syscall 使它支持?
- Why philosophers should care about computational complexity, Ch. 10 (jyy 强烈推荐,解释部分在10th-section)
- 能否添加一个 syscall 使它支持?
- Cellular automata 不支持 “时间旅行”
状态机模型:理解编译器和现代 CPU
- 编译器:源代码$S$(状态机) → 二进制代码$C$(状态机)
$$ C=compile(S) $$
-
编译 (优化) 的正确性 (Soundness):
- S 与 C 的可观测行为严格一致 (二进制落实到硬件也是如此,严格一致不是句句对应,而是状态机一致,比如一个时钟周期内执行两条指令 $\Longrightarrow$ instruction-level parallelism)
- system calls; volatile variable loads/stores; termination
- S 与 C 的可观测行为严格一致 (二进制落实到硬件也是如此,严格一致不是句句对应,而是状态机一致,比如一个时钟周期内执行两条指令 $\Longrightarrow$ instruction-level parallelism)
-
超标量 (superscalar)/乱序执行处理器
-
允许在状态机上 “跳跃”
-
|
|
- 在优化下执行的效果
|
|
- 优化过后,每一个时钟周期可以执行远远超过一条指令
查看状态机执行
Trace 和调试器
-
程序执行 = 状态机执行
- 我们能不能 “hack” 进这个状态机
- 观察状态机的执行
- strace/gdb
- 观察状态机的执行
- 我们能不能 “hack” 进这个状态机
-
甚至记录和改变状态机的执行
|
|
strace
调试最小的Hello OS,可以清楚地看到系统调用
|
|
- -T看每一个系统调用花费的时间
|
|
- 注意为了让
layout src
能够成功显示,编译时需要使用gcc
的-g
编译选项
|
|
应用 (1): Time-Travel Debugging
-
程序执行是随时间 “前进” 的$s_0 \rightarrow s_1 \rightarrow s_2 \rightarrow \dots$
-
能否在时间上 “后退”? (time-travel)
- 经常 gdb 不小心 step 过了,从头再来……
- 记录所有的$s_i$,就能实现任意的 time-traveling
凉性循环,看一会
rust
- 记录所有$s_i$的开销太大($s_i$由内存+寄存器组成)
- 但一条指令的side-effect通常有限
应用 (1): Time-Travel Debugging (cont’d)
-
gdb 的隐藏功能 (大家读过 gdb 的手册了吗?)
-
record full
- 开始记录 -
record stop
- 结束记录 -
reverse-step
/reverse-stepi
- “时间旅行调试”
-
- 例子:调试 rdrand.c
- Reverse execution 不是万能的
- 有些复杂的指令 (
syscall
) 无法保证 $\Longrightarrow$record and replay
- 有些复杂的指令 (
- Reverse execution 不是万能的
|
|
asm volatile ("rdrand %0": "=r"(val));
使用了GCC
内联汇编(Inline Assembly
)的语法,使用 Intel 的 RDRAND 指令生成一个随机数,并将该随机数保存到变量val
中。具体来说,
%0
表示占位符,用来代表第一个输入或输出操作数,这里是val
。而=r
则表示将val
寄存器中的值作为输出值,同时通知编译器该变量会被修改。因此,该代码使用 RDRAND 生成一个随机数,并将其保存到
val
变量中。最后通过printf
打印出该随机数。
|
|
volatile
提醒编译器它后面所定义的变量随时都有可能改变,因此编译后的程序每次需要存储或读取这个变量的时候,告诉编译器对该变量不做优化,都会直接从变量内存地址中读取数据,从而可以提供对特殊地址的稳定访问。如果没有
volatile
关键字,则编译器可能优化读取和存储,可能暂时使用寄存器中的值,如果这个变量由别的程序更新了的话,将出现不一致的现象。(简洁的说就是:volatile
关键词影响编译器编译的结果,用volatile
声明的变量表示该变量随时可能发生变化,与该变量有关的运算,不要进行编译优化,以免出错)
- 更改之后进行
gdb
|
|
- 每一次的调试结果都不一样,那我们应该如何复现
BUG
?- 打开记录模式
|
|
val
的值已经改变,如何向上回溯?- 使用
rsi
往回执行
- 使用
应用 (2): Record & Replay
- 在程序执行时记录信息,结束后重现程序的行为
- 确定的程序不需要任何记录
- 假设$s_0$执行 1,000,000 条确定的指令后得到$s^{`}$
- 那么只要记录$s_0$和1,000,000
- 就能通过“再执行一次” 推导出$s^{`}$
- 假设$s_0$执行 1,000,000 条确定的指令后得到$s^{`}$
- 确定的程序不需要任何记录
- 记录:[指令数(确定指令) + 结果(非确定指令)] $\times n$
应用 (2): Record & Replay (cont’d)
-
Record & Replay
: 只需记录non-deterministic
的指令的效果 -
(单线程) 应用程序
- syscall, rdrand, rdtsc, …
- rr (Mozilla)
-
(单处理器) 操作系统
-
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 🏅)
-
采样状态机执行
关于性能优化
Premature optimization is the root of all evil. (D. E. Knuth)
-
那到底怎么样才算
mature
呢?-
状态机的执行需要时间;对象需要占用空间
-
需要理解好 “时间花在哪里”、“什么对象占用了空间”
-
-
我们需要真实执行的性能摘要!
-
本质的回答:“为了做某件事到底花去了多少资源”
-
简化的回答:“一段时间内资源的消耗情况”
-
Profiler 和性能摘要
性能摘要需要对程序执行性能影响最小(不能因为这个进程过多影响你检测的程序),往往不需要 full trace。
- 隔一段时间 (比如一毫秒)“暂停” 程序、观察状态机的执行
- 中断就可以做到
- 将状态 [s→s′] “记账”
- 执行的语句
- 函数调用栈
- 服务的请求
- 得到统计意义的性能摘要
例子:Linux Kernel perf (支持硬件 PMU) - ilp-demo.c
- perf list, perf stat (-e), perf record, perf report
|
|
- 安装
perf
|
|
实际中的性能优化
-
你们遇到的大部分情况
-
二八定律:80% 的时间消耗在非常集中的几处代码
-
L1 (pmm)
: 小内存分配时的lock contention
profiler
直接帮你解决问题
-
- 工业界遇到的大部分情况
- 木桶效应:每个部分都已经 tune 到局部最优了
- 剩下的部分要么 profiler 信息不完整,要么就不好解决
- (工程师整天都对着 profiler 看得头都大了)
- The flame graph(火焰图) (CACM'16)
- 木桶效应:每个部分都已经 tune 到局部最优了
Model Checker/Verifier
Model Checker 的威力大家已经知道了
-
150 行代码的 model-checker.py
-
证完所有《操作系统》课上涉及的并发程序
-
复现 OSTEP 教科书上的并发 bug (条件变量错误唤醒)
-
-
一些真正的 model checkers
-
TLA+ by Leslie Lamport;
-
- 它们都喜欢用 Peterson 算法做 tutorial 😁
-
Model Checker: 不仅是并发
- 任何 “
non-deterministic
” 的状态机都可以检查
|
|
- 更高效的
Model Checker
: “将相似状态合并”- KLEE: Unassisted and automatic generation of high-coverage tests for complex systems programs (OSDI'08, Best Paper 🏅)
- 基于
LLVM bitcode
解释器实现
总结
- 本次课回答的问题
- Q: 状态机的视角给了我们什么?
-
Take-away messages
-
编程 (状态机) 就是全世界
-
状态机可以帮我们
- 建立物理世界的公理体系
- 理解调试器、
Trace, profiler
- 自动分析程序的执行 (
model checker
)
- 理解调试器、
- 建立物理世界的公理体系
-
声明:本文章引用资料与图像均已做标注,如有侵权本人会马上删除