本文提出了 Yggdrasil，Yggdrasil 是一个工具包，可用于编写具有一键验证功能的文件系统。它通过一种称为崩溃细化的新颖正确性定义实现自动化验证，无需手动注释或证明实现代码，并在出现错误时生成反例。崩溃细化适用于完全自动化的 SMT 推理，并使开发人员能够模块化地实现文件系统以进行验证。 
Yggdrasil
程序员需要编写 specification, implementation 和 consistency invariant (all in python language)。
验证器会生成反例来可视化 implementation 或 consistency invariant 中的 bug。
Yggdrasil 可以进行优化并重新验证代码以提高运行时性能。
验证通过后，Yggdrasil 会生成C代码，通过C编译器编译和链接生成可执行文件系统和fsck检查器。
specification
Yggdrasil文件系统规范包括三个部分：
- 表示逻辑布局的抽象数据结构（Abstract data structure）
- 定义预期行为的操作集合
- 定义实现是否符合规范的等价谓词（equivalence predicate）
下面均以作者实现的一个小文件系统YminLFS做演示。
Abstract data structure
抽象数据结构由五个抽象映射描述，包括childmap、parentmap和三个存储inode元数据的映射。其中，childmap将目录inode号和名称映射到子inode号，parentmap将inode号映射回其父目录的inode号。InoT和U64T是64位整数类型，NameT是字符串类型。
FSSpec数据结构对YminLFS的逻辑布局没有强制约束。FSSpec规范通过invariant来防止无效的布局。 
invariant指出父子节点之间有效索引节点号的映射的相互一致。ForAll和Implies是内置的逻辑运算符。
文件系统操作
文件系统操作包括只读操作和读写操作。只读操作包括lookup和stat。 
修改文件系统的操作更复杂，因为它们涉及更新抽象映射的状态。 
InoT()构造函数返回一个抽象的inode号码，必须是有效的且不在任何目录中。对文件系统的更改被包装在一个事务中，以确保它们是原子的。
state equivalence predicate
implementation
在Yggdrasil中实现文件系统需要
- 选择磁盘模型
- 编写每个操作的代码
- 编写磁盘布局的consistency invariants
磁盘模型
Yggdrasil提供了异步磁盘模型和同步磁盘模型。
异步磁盘模型具有无限制的易失性缓存（volatile cache），并允许任意重排序。其接口包括以下操作：
d.write (a, v): write a data blockvto disk addressa;d.read (a): return a data block at disk addressa;d.flush (): flush the disk cache.
初始化磁盘创建一个空的根目录文件系统，包括超级块、根目录索引节点和索引节点映射块。初始化后，索引节点映射块只有一个条目，根目录索引节点没有指向数据块。超级块指向索引节点映射块，并存储下一个可用的索引节点和块号。
mknod命令将磁盘状态从Figure 2a变为Figure 2b，以将文件添加到根目录。
- 为新文件添加一个索引节点块
； - 为根目录添加一个数据块
，现在根目录有一个条目，该条目将新文件的名称映射到它的索引节点号2； - 为更新后的根目录添加一个索引节点块
，它指向它的数据块 ； - 添加一个索引节点映射块
，其中包含两个条目： 和 ； - 最后，更新超级块
，使其指向最新的索引节点映射 。
为了保证系统崩溃时数据的完整性，mknod必须发出flush操作。如果在最后两次写操作之间没有flush操作，磁盘可能会重新排序这些写操作。如果系统在重新排序的写操作之间崩溃，超级块将指向flush操作，共5个可解决这个问题。
Consistency invariants
Consistency invariants是文件系统实现的一种约束条件，用于确定磁盘状态是否对应于有效的文件系统映像。Yggdrasil使用Consistency invariants进行验证和运行时检查，以确保文件系统的正确性。验证时，Yggdrasil检查初始文件系统状态是否满足Consistency invariants，并将其作为每个操作的前置条件和后置条件进行检查。此外，Yggdrasil还可以生成类似于fsck的检查器，用于检查文件系统的完整性。
Consistency invariants约束了磁盘布局的三个组件：超级块
Crash Refinement
基于传统的状态机的证明强调步步互锁，要求 implementation 和 specification 始终保持一致，这个要求 is too strong to satisfy，因为文件系统在实际的读写时可能会出现乱序的情况（类似的CPU的指令重拍），此外还有崩溃、恢复等情况（这俩和too strong有啥关系？）。
本文提出的Crash Refinement放松了要求，any implementation 的状态只需要和 some specification 的状态一致即可。
Crash-free equivalence：如果在没有崩溃的情况下，implementation 和 specification 从等价一致状态开始，执行相同操作后能够到达等价一致状态，则 implementation 和 specification 在无崩溃的情况下等价。
Crash refinement without recovery：对任意的 crash schedule，implementation 在该 crash schedule 下执行后得到的任意状态（不包括恢复），specification 在某个 crash schedule 下也能得到等价状态，则 implementation 是 specification 的 crash refinement。
Recovery idempotence：恢复函数是幂等的，多次崩溃和重启过程中调用多次该函数，结果状态相同。
Crash refinement with recovery：对任意的 crash schedule，implementation 在该 crash schedule 下执行后得到的任意状态，包括多次执行恢复函数后的任意状态，specification 在某个 crash schedule 下也能得到等价状态，则 implementation 是 specification 的 crash refinement。
No-op: 不改变对外可见状态的后台操作。
Yxv6 file system
