**崩溃一致性**：我们可以使用 model checker 模拟崩溃时的文件系统行为，假设所有的 block write 都可能被任意乱序。这个程序对应了教科书中的例子，展示了磁盘没有多操作原子性 (all or nothing) 支持时对文件系统带来的麻烦。