绪论
字数
576 字
阅读时间
3 分钟
[Yanyan's Wiki (jyywiki.cn)](Yanyan's Wiki (jyywiki.cn))
应用视角的操作系统
程序无法自己停下来，指令集没有关机指令，那么操作系统如何关闭所有软件后，进行关机？
回想在计组课程设计里，有一个停机指令，通过控制启停电路，从而实现连续脉冲的阻塞，而使得指令和微指令都无法继续执行，但时钟脉冲仍在继续，可能算不上一种真正的停机。 而现实电脑中是如何实现关机的呢？也是通过硬件电路，上有一个微型操作系统，通过I/O发送指令，控制电源的关闭。 ACPI（Advanced Configuration and Power Interface，高级配置与电源接口）是一种开放的工业标准，用于操作系统管理计算机硬件的电源状态和配置。
system call trace（strace）跟踪程序里的系统调用。
编译优化
编译优化“三板斧"
- 函数内联：将函数调用替换为函数体本身的内容
- 常量传播：在编译时计算常量表达式的值并替换
- 死代码消除：删除永远不会执行到的代码
编译正确性
C代码中不可优化部分
- External function calls
- 编译器提供的”不可优化“标注
volatitle[load | store | inline assembly] 这和面向对象中的单例模型里的双重加锁懒汉里用的一样，防止编译器对于创建对象进行编译优化，防止多线程出现问题。
硬件视角的操作系统
状态机的起始状态为Reset
数学视角的操作系统
伪证：所有的三角形都是等腰三角形。
证明程序的正确性
- 暴力枚举
- 启发：把需要证明的性质写成assertions，
assert(u->prev->next == u)正确的双向链表的性质
- 启发：把需要证明的性质写成assertions，
- 写出证明 "proof assistant"
- 启发：容易阅读、容易验证的代码是好代码
操作系统也是状态机，也作为状态机管理器。
贡献者
Yiming Li