1并发交错语义
闭卷重建并发交错语义的对象、公式、算例、算法与失败边界。
形式化方法与程序验证 · 小纸条
选一章打印。双面打印（按长边翻页）后沿虚线剪开，每张卡片正面题目、背面答案。
第 1 页 · 正面（题目）
2互斥与竞态规约
闭卷重建互斥与竞态规约的对象、公式、算例、算法与失败边界。
3死锁、活锁与饥饿
闭卷重建死锁、活锁与饥饿的对象、公式、算例、算法与失败边界。
4线性化点与并发对象
闭卷重建线性化点与并发对象的对象、公式、算例、算法与失败边界。
5可串行化与事务不变量
闭卷重建可串行化与事务不变量的对象、公式、算例、算法与失败边界。
6弱内存与重排序
闭卷重建弱内存与重排序的对象、公式、算例、算法与失败边界。
7TLA风格状态机与精化映射
闭卷重建TLA风格状态机与精化映射的对象、公式、算例、算法与失败边界。
第 1 页 · 背面（答案）
对象：互斥是安全性质；数据竞态指未同步的冲突访问，需结合内存模型。；公式：□¬(crit_i∧crit_j)。；算例：两个线程同时crit为真即一个坏状态，反例到达即足够。；边界：无数据竞态就声称高层原子性；锁模型漏失败路径。。
对象：并发程序全局执行由任一已启用线程原子步交错形成。；公式：(C1||C2,σ)→(C1′||C2,σ′)或对称。；算例：两线程各1步有AB、BA两种调度；若操作不交换结果可能不同。；边界：把源码一行误当硬件原子；只测一种调度。。
对象：线性一致性要求每次操作可放到调用和返回之间某点，得到尊重实时序的顺序历史。；公式：call(op)<lin(op)<return(op)。；算例：入队先完成后出队才调用，线性序必须入队在前；重叠操作可择序。；边界：只比较最终容器状态；忽略返回值和实时先后。。
对象：死锁无启用进展；活锁有步骤但无业务进展；饥饿是个体长期不得服务。；公式：deadlock(s):Enabled(s)=∅∧¬terminal(s)。；算例：两线程各持一把锁等待另一把，Enabled为空且非终止。；边界：把CPU忙碌当有进展；有限运行未服务就判饥饿。。
对象：现代硬件/语言内存模型允许部分读写重排；正确性需用happens-before而非源码顺序直觉。；公式：hb=program-order∪synchronizes-with的传递闭包。；算例：线程写data再release flag，另一线程acquire flag后读data，建立hb。；边界：用顺序一致模型证明release/acquire实现；普通变量有数据竞态。。
对象：并发事务历史若等价于某串行序则可串行化；数据库不变量需在提交边界保持。；公式：conflict graph acyclic⇒conflict-serializable。；算例：T1→T2和T2→T1构成环，因此不可冲突串行化。；边界：只看最终余额；快照隔离写偏斜未建模。。
对象：系统规格以Init和Next描述行为，不变量和活性在行为上检查；精化映射连接实现状态与抽象状态。；公式：Spec=Init∧□[Next]_vars。；算例：计数器Init x=0，Next x′=x+1或停顿；不变量x≥0保持。；边界：Next漏动作导致虚假证明；把实现内部步当抽象可见变化。。