Crash Consistency

File System

OSDI'14 - BOB and ALICE

persistence property

• ordering

• atomicity : content-atomicity, size-atomicity

empirical study ：

BOB 用于 empirically 地寻找违反 persistence property 的测试用例：首先执行一个针对 persistence property 的简单的 stress workload ，收集运行时的 block IO ，然后在遵循 disk barrier 的前提下对收集的 block IO 进行前缀截断和重排，由此生成一系列的可能的 crash state ，最后检查它们是否违反了 persistence property 。

• crash state ：系统 crash & reboot 后可能出现的系统状态。

不同的系统调用可能导致相同的文件系统更新操作，据此将系统调用划分为 file overwrite 、file append 、directory (mkdir/rename/link/unlink/...) 三类。

• ? The size and alignment of an overwrite or append affects its atomicity.

• ? For ordering, we show whether given properties hold assuming different orderings of overwrite, append, and directory operations;

不同文件系统，或同一文件系统的不同配置，支持的 persistence property 是不同的，因此 fs-based applications 的正确性不应建立在 fs-specific 的 persistence property 之上。

application-level crash consistency ：

ALICE 为 fs-based applications 寻找通用的（即 non-fs-specified 的）persistence property 并检查属性是否被满足：首先从某个给定的初始状态出发执行 application workload 并用 strace 记录 syscall trace ，将其转换为 logical operation 序列，然后根据 APM 计算所有可达的 crash state 。

• syscall → logical operation ：抽象 disk IO 操作的不同细节，例如 offset 、fd 等，仅关心其读写的 inode 。

• logical operation → micro-operation ：能够应用于文件系统逻辑实体（inode）的最小原子操作。

• APM (abstract persistence model) : specifies all constraints on the atomicity and ordering of logical operations for a given file system, thus defining which crash states are possible. 默认为 generic 、low-restricted 的，可定制。

OSDI'16 - Yggdrasil

基于分层的架构，模块化地验证文件系统：

• 将文件系统的 implementation 与 specification 视为两个状态机，implementation 每个满足一致性条件的状态必须对应 specification 的某个合法状态。

• 系统的每一层都有自己的实现和规范，高层会利用低层的 specification ，由此划分并限制单次程序验证的规模。

• 许多文件系统操作只会涉及到磁盘中的一小部分，考虑将磁盘划分为多个子盘（根据数据的逻辑语义进行划分，例如 log 和 free bitmap 分到不同子盘）。

crash refinement ：从等价的状态出发执行相同的文件系统操作，到达的状态也必须是等价的。

• 形式化地定义 crash schedule vector ，即每个程序点处对易失性缓存的读写是否完成、是否同步到持久性内存，均为真时才更新磁盘。

• 对于规范 $f_0$ 和实现 $f_1$ ，若 $f_1$ 使用任意的 crash schedule $b_1$ 都与 $f_0$ 使用某个 crash schedule 等价，则称 $f_1$ 是 $f_0$ 的某个 crash refinement 。

基于符号执行和 SMT solver 进行验证。

OSDI'18 - B3

KEY Idea : From empirical study of crash-consistency bugs in Linux file systems in the last 5 years.

• 大部分崩溃一致性错误可以由小规模的 workload（除 persistence point 外仅包含两三个 fs operation）在全新的 fs image 上触发。

• 大部分崩溃一致性错误由紧随 persistence point 之后的崩溃触发。

• 系统性的测试是必要的：一些补丁仅修复了一部分能触发错误的路径，但错误仍能被其它 workload 触发。

持久化 (persistence) ：fs operation 通常只会修改 in-memory data ，只有 persistence point（例如 fsync() 等）保证可靠地修改 storage data 。没有 persistence point 的 workload 即便触发了崩溃一致性错误也是难以确定性重现的。

B3 (bounded black-box crash testing) 在有界空间内生成 workload ，仅在 persistence point 之后插入 crash ，并且仅在简单的 fs image 上测试。

• B3 选择放弃探索由发生在 fs operation 期间的崩溃引起的一致性错误。一方面是因为 empirical study ，另一方面是因为文件系统对此类错误经常没有 specification ，而且这也能极大地限制搜索空间。

• B3 的有界空间限制了 workload 中 fs operation 的个数、涉及文件和目录的个数、涉及的数据操作（仅考虑 overlapping ranges 而不关心具体实际的 offset 和 length）、以及限制所用 fs image 是 small 且 new 的。

搜索策略 ：

B3 按规模从小到大的顺序穷竭枚举，依次生成包含 $1, 2, ...$ 个 fs operation 的所有 workload ，记为 seq-x : $f_1f_2...f_x$ 。在这样的顺序下，总是只需要在 workload 中插入一个 persistence point $p$ 。

• 例如对于 seq-2 : $f_1f_2$ ，如果考虑 $f_1p_1f_2p_2$ ，其前缀 $f_1p_1$ 是已经测试过的 seq-1 : $f_1p$ ，所以只需要考虑 $f_1f_2p$ 即可。

limitations ：

• B3 有效限制了搜索空间的大小，但也无法探索部分错误，例如需要大规模输入才能触发的错误、或是需要耗尽资源才能触发的错误，等等。

• B3 不会在 fs operation 期间插入 crash ，并且不会通过重排 IO request 来生成 crash state 。

• B3 仅考虑文件系统是否遵循 persistence point 的显式持久化：If we created a file, waited one hour, then crashed, and found that the file was gone after the file-system recovered, this would also be a crash-consistency bug.

Storage System

OSDI'14 - ACID_iSCSI

仅针对最简单的 crash 进行检验，即仅考虑数据库在发生 clean power fault 时的 crash state 是否满足 ACID 要求。

设计了 4 种由简到繁的 workload 以及对应的 crash ACID checking 方法。

基于 iSCSI 设计和实现测试框架：record and replay 。

• iSCSI is a standard allowing one machine (the initiator) to access the block storage of another machine (the target) through the network.

multi-layer trace

fault injection / pattern-based ranking ：对于每个 block IO 操作，用五种 empirical / experimental 的 pattern 与之进行匹配，为五次匹配契合度之和更高的 block IO 操作赋予更高的优先级，以作为断电位置进行 crash ACID checking 。

SOSP'21 - Witcher (reading unfinished)

crash consistency bugs

• correctness : persistence ordering bugs & persistence atomicity bugs

• performance : redundant flush/fence & redundant logging

crash correctness : all-or-nothing ，将 "all" 和 "nothing" 作为 test oracle 。可能存在漏报（有些 crash consistency bugs 可能不会产生诸如 segmentation fault 或错误输出的 visible symptoms），但不存在误报。

• 设程序在执行指令 $s$ 时 crash ，则其 crash state 要么等价于没有执行 $s$ 的状态、要么等价于成功执行了 $s$ 的状态。

Witcher 的测试目标是 NVM-Backed Key-Value Stores 的 crash consistency 。

• flush (x86 clwb) : write back cache -> memory

• fence (x86 sfence) : ordering guarantee between flushes

KEY Idea ：实现代码中经常会以 data/control dependence 的形式隐含了实现者希望保证的 persistence specification 。

• 例如 if (token[x] && key[x] == k) ... 先检查 token 再检查 key ，这里的 control dependence 就隐含了先 key 后 token 的 persistence ordering specification 。

likely-correctness condition ：可能隐含了 specification 的 data/control dependence 。

Witcher 静态或动态地分析被测系统，从中推断 likely-correctness conditions ，然后只检测违反这些条件的 crash states（对于上例就是只持久化了 token 的情况）。这会导致漏报，但能够极大地缩减状态空间。