<aside> 📖 一个干净的理论模型 (Simple Sequential Execution)

• $\text{State}=\text{Memory}+\text{Register}$
• 初始状态：程序启动时操作系统给安排的状态
• 状态转移 = 时钟驱动的指令执行 </aside>

$$ \text{Program} = \text{State Machine} \\ \text{OS} = \text{Object} + \text{API} $$

<aside> 📖 指令分为两种

1. 内部指令
   • 确定的：完全根据当前 (M,R) 计算出一个新的 (M,R)
   • 非确定的：rdrand
2. 外部指令（只有一条）
   • syscall：交给操作系统，让操作系统决定下一个状态是什么
     • 除了可以观察 syscall 返回的结果，程序完全不知道 syscall “发生了什么” </aside>

<aside> 📖 一个普通的 C 程序执行的第一条指令在哪里？

动态链接的加载器中

</aside>

<aside> 📖 本质上，所有的程序和 Hello World 类似

• 被操作系统加载
  • 通过另一个进程执行 execve
• 状态机执行 (内部 + 唯一的外部指令 syscall)
  • 进程管理：fork, execve, exit, ...
  • 文件/设备管理：open, close, read, write, ...
  • 存储管理：mmap, brk, ...
• 直到 _exit (exit_group) 退出

用strace跟踪\

</aside>

<aside> 📖 如何在程序的两个视角之间切换？

• 编译器：源代码$S \rightarrow$ 二进制代码$C$

  $C=\text{compile}(S)$

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

  $S$与$C$的可观测行为严格一致

</aside>