第27篇 FaRM 本地有限模型证据

日期：2026-09-25
源码：examples/distributed-systems/farm27/check.py
源码 SHA-256：61220941dd8d1d6cfa77bc8314259e0e72c246ea50b2856423f121e17ab73d11
解释器：Python 3.12.3

正式命令从仓库根目录执行；TMPDIR、TMP、TEMP 均指向：
examples/distributed-systems/.build/farm27/tmp
设置 PYTHONDONTWRITEBYTECODE=1，并使用 python3 -B。

首次运行：工具 chunk 1d9578，退出1。失败原因是测试错误地断言正确验证会令两笔 write-skew 事务都中止。按实际固定顺序，T1 验证失败后释放 x，T2 随后可以通过并提交。修正测试预期后才重新运行；该次失败不算协议反例或通过证据。

修正后正式全场景：工具 chunk 211cdf，退出0；输出同时写入 .build/farm27/observations.json。

观察结果：
1. 写写冲突：T1锁定并提交，T2在LOCK失败并中止，最终counter=1。
2. 正确write-skew验证：T1中止、T2提交，最终x=0,y=1，属于模型列举的串行结果。
3. 忽略锁位的变异：T1、T2都提交，最终x=1,y=1，不属于模型列举的串行结果。
4. 恢复切点：只有LOCK时abort；所有region均有COMMIT-BACKUP时commit；一个COMMIT-PRIMARY存活时commit。
5. 错误变体跳过r2 backup后假设primaries已经暴露，再丢失primaries，只能恢复r1；模型标记atomic_durability_preserved=false。

CLI帮助：随正式运行执行，退出0。
非法参数：--scenario unknown，工具 chunk 418537，argparse退出2。

运行期间未启动网络服务、未下载依赖、未编译原生二进制。只使用Python标准库。当前环境只取得一个独立Python解释器，因此没有声称跨版本复跑。

边界：这是确定性教学模型，不实现或验证真实RDMA、NIC ACK、NVRAM/SSD掉电、ZooKeeper、成员关系、租约、任意调度、网络分区、完整FaRM恢复或性能。