1竞态不是同时运行的同义词
闭卷重建竞态不是同时运行的同义词的对象、状态、事件、不变量与一个失败反例。
操作系统与系统实验 · 小纸条
选一章打印。双面打印（按长边翻页）后沿虚线剪开，每张卡片正面题目、背面答案。
第 1 页 · 正面（题目）
2临界区与正确性条件
闭卷重建临界区与正确性条件的对象、状态、事件、不变量与一个失败反例。
3锁、原子操作与内存可见性
闭卷重建锁、原子操作与内存可见性的对象、状态、事件、不变量与一个失败反例。
4信号量的资源语义
闭卷重建信号量的资源语义的对象、状态、事件、不变量与一个失败反例。
5条件变量与管程
闭卷重建条件变量与管程的对象、状态、事件、不变量与一个失败反例。
6实验：信号量许可守恒
闭卷重建实验：信号量许可守恒的对象、状态、事件、不变量与一个失败反例。
7实验：交错枚举找丢失更新
闭卷重建实验：交错枚举找丢失更新的对象、状态、事件、不变量与一个失败反例。
第 1 页 · 背面（答案）
核心机制：互斥、进展和有限等待共同描述临界区协议，入口和退出必须对所有路径成对；实验入口：为两个线程列出Peterson算法共享变量的读写顺序，验证假设成立时不会同时进入；边界：经典软件算法依赖内存模型与原子读写假设，不能直接替代现代语言同步原语。
核心机制：当结果依赖未受约束的事件交错且至少一个操作写共享状态时形成数据竞态或更广义逻辑竞态；实验入口：把counter++拆成读、加、写，让两线程交错得到丢失更新，再用串行执行反查；边界：线程并发不必然错误；即使无数据竞态，也可能有检查后使用的逻辑竞态。
核心机制：计数信号量表示可用许可，wait原子地消耗许可或阻塞，post归还并唤醒等待者；实验入口：用empty、full、mutex三信号量推演容量3的生产者消费者队列；边界：信号量初值和每条路径的P/V次序决定安全；多post或漏post都会破坏许可守恒。
核心机制：互斥锁提供所有权和happens-before关系，原子读改写保证单变量操作不可分割；实验入口：比较普通计数、mutex计数与atomic计数，记录正确性、争用和扩展曲线；边界：原子变量只保护自身，不自动维持多个变量之间的不变量；忙等也会消耗CPU。
核心机制：离散模拟器记录每次P/V后的许可与阻塞数，用不变量检测负许可或资源泄漏；实验入口：输入初值与P/V事件序列，输出完成操作数、阻塞数和最终许可；边界：模拟策略必须声明阻塞P是否排队以及后续V是否直接转交许可。
核心机制：条件变量让线程在持锁检查谓词后原子释放锁并等待，唤醒后必须循环重查谓词；实验入口：为有界队列写while not_full wait与while not_empty wait，模拟虚假唤醒和多个等待者；边界：if代替while会在竞争或虚假唤醒后越界；通知不是把条件本身永久记住。
核心机制：系统化测试枚举两线程读改写步骤的所有保持程序序的交错，收集可能终值；实验入口：对两个counter++各拆三步，程序输出全部可能结果和产生错误结果的交错数；边界：枚举只能覆盖有限模型；现实编译器与弱内存还会引入额外重排，需要同步语义约束。