Reading Papers - File System Verification

# Overview

# Crash Consistency

# SOSP'15 - FSCQ

本文将霍尔逻辑扩展为 CHL 以支持对文件系统 crash 和 recovery 行为的形式化描述及验证，同时提出 logical address space 的抽象以支持对文件系统不同层级的概念的模块化描述，最后利用上述方法描述和验证了（对标 xv6 的）简单文件系统 FSCQ 。

SOSP'15 - Using Crash Hoare Logic for Certifying the FSCQ File System
Taxonomy : system verification / file system
Tag : crash consistency / hoare logic / separation logic / Coq

推理和验证文件系统所用的 formal specification 应当具有如下能力：

能够以某种方式（例如形式化语言）描述系统行为，并对系统实现进行自动化证明；
支持模块化或分层地对系统进行验证；
能够描述文件系统的崩溃时行为；
能够描述文件系统实现常用的重要优化手段（例如异步磁盘 I/O）。

描述文件系统的崩溃时行为是 non-trivial 的，这要求所用的形式化方法至少具备表征以下语义的能力：

文件系统可能在运行期间的任意时刻崩溃（通常假设文件系统操作是 atomic 的，此时需要描述的语义是：系统可能在任意两个操作之间崩溃）；
若未显式调用 fsync() 一类的系统调用，文件系统可能在后台以不同方式将数据同步到磁盘，取决于对应文件系统实现的某种 specification ；
崩溃后的恢复操作：能将系统恢复到某个符合某种 specification 的状态，并且（通常）应当是 幂等 (idempotent) 的；

本文是首个既能描述崩溃时行为、又支持系统实现的自动化证明的文件系统验证工作。

本文以伪函数 atomic_two_write 作为贯穿全文的示例来描述 CHL 的能力，其反映了文件系统中普遍存在的一类行为，其语义如下所示：

def atomic_two_write(a1, v1, a2, v2):
    log_begin()
    log_write(a1, v1)
    log_write(a2, v2)
    log_commit()

# Crash Hoare Logic

本文将 霍尔逻辑 (Hoare Logic) 扩展为 Crash Hoare Logic (CHL) 以支持对文件系统崩溃时行为（以及崩溃后恢复，下同）的形式化描述及验证。在霍尔逻辑的基础上，CHL 引入了 crash condition, logical address space, recovery execution semantics 这三个新的概念。

CHL 利用 分离逻辑 (separation logic) 来描述和推理存储器上多个不相交的部分，从而支持对磁盘数据的模块化推理。具体地讲：

$a \mapsto v$ 表示地址 $a$ 处存储的值为 $v$ ；这里的地址对于磁盘而言是 block number 。
给定两个谓词 $x$ 和 $y$ ，分离合取 $x * y$ 表示磁盘可以被划分为两个不相交的部分，分别满足谓词 $x$ 和 $y$ 。

为了描述系统崩溃时的磁盘状态，CHL 将磁盘建模为形如 $a \mapsto \braket{v,\ vs}$ 的映射，其中 $v$ 为最后一次写入 $a$ 的值， $vs$ 为 $a$ 处所有历史值的集合。

读操作将返回最后一次写入的值 $v$ ，写操作将替换 $v$ 并将原先的 $v$ 加入集合 $vs$ 中。
同步操作将清空所有地址处的 $vs$ 。

例如 disk_write 的 CHL specification 如下：

\begin{aligned} & \text{SPEC} && \text{disk\_write}(a,\ v) \\ & \text{PRE} && \textbf{disk} :\ a \mapsto \braket{v_0,\ vs} * other\_blocks \\ & \text{POST} && \textbf{disk} :\ a \mapsto \braket{v,\ [v_0] \oplus vs} * other\_blocks \\ & \text{CRASH} && \textbf{disk} :\ a \mapsto \braket{v_0,\ vs} * other\_blocks \lor a \mapsto \braket{v,\ [v_0] \oplus vs} * other\_blocks \\ \end{aligned}

CHL 的模型捕获了真实磁盘的两个重要性质：异步 I/O 的不确定性，以及可重排 (reordered) 的写操作。事实上，简单映射 $a \mapsto v$ 对应了易于证明但性能低下的同步磁盘。

# CHL: Logical Address Space

验证文件系统通常需要在不同的抽象层级上描述系统行为，例如 pwrite 系统调用和 disk\_write 非常相似，但 pwrite 的 specification 需要描述文件内容的 offset 和取值，而不是磁盘上的 block number 和取值。

在磁盘的抽象上描述 pwrite 的 specification 是过于复杂且 error-prone 的，需要描述的系统行为可能包括：分配一个新的 block 、分配一个新的 inode 、处理 indirect mapping 、将文件内容的 offset 映射到磁盘上的对应 block ……

CHL 提出 logical address space 以简洁地描述文件系统的多层抽象，允许开发者定义干净的 specification ，例如向文件系统的高层级提供简单的同步磁盘抽象，使处在高层的开发者可以很大程度上忽略底层异步磁盘的细节。

例如 atomic_two_write 的 CHL specification 如下：

\begin{aligned} & \text{SPEC} && \text{atomic\_two\_write}(a_1,\ v_1,\ a_2,\ v_2) \\ & \text{PRE} && \textbf{disk} :\ \text{log\_rep}(\text{NoTxn},\ start\_state) \\ &&& \textbf{start\_state} :\ a_1 \mapsto v_x * a_2 \mapsto v_y * others \\ & \text{POST} && \textbf{disk} :\ \text{log\_rep}(\text{NoTxn},\ new\_state) \\ &&& \textbf{new\_state} :\ a_1 \mapsto v_1 * a_2 \mapsto v_2 * others \\ & \text{CRASH} && \textbf{disk} :\ \text{log\_intact}(start\_state,\ new\_state) \end{aligned}

和 disk_write 对物理磁盘的描述不同，在这里，logical address space 将单个值而不是一组值与每个地址（即磁盘块）相关联，因为 transaction system (?) 导出了一组 sound 的同步接口，在下层的异步接口之上被证明是正确的（？）。

要使 specification 更加精确，必须描述出对于每个 logical address space 而言 $a \mapsto v$ 的确切含义是什么。为此，CHL 利用 representation invariant 将 logical address space 与其在磁盘上的物理表示相关联。

$\text{log\_rep}(\text{DiskState},\ las)$ 表示 logical address space $las$ 在磁盘上的表示方式处在 $\text{DiskState}$ 的状态下；例如 $\text{log\_rep}(\text{NoTxn},\ start\_state)$ 表示磁盘上的对应部分没有正在活动的 transaction 且处于 $start\_state$ 的状态下。
$\textbf{las}: predicate$ 表示 logical address space $\textbf{las}$ 与特定的谓词相匹配；特别地，如果谓词为 $\text{log\_rep}()$ ，则表示将对应的 representation invariant 应用于 $\textbf{las}$ 。
$\text{log\_intact}(d1,\ d2)$ 表示恢复到 transaction state (?) $d1$ 或 $d2$ 的所有可能的 $\text{log\_rep}$ 状态，这捕获了函数执行期间所有可能的崩溃状态（包括在执行子过程内崩溃产生的状态，例如 log_commit 内）。

例如在 atomic_two_write 中：

precondition 中的 $\textbf{disk} :\ \text{log\_rep}(\text{NoTxn},\ start\_state)$ 将执行前的磁盘状态与 logical address space $start\_state$ 相关联，
postcondition 中的 $\textbf{disk} :\ \text{log\_rep}(\text{NoTxn},\ new\_state)$ 将执行后的磁盘状态与 logical address space $new\_state$ 相关联，

如下是一个较复杂的 $\text{log\_rep}()$ 示例的语义：

$\text{log_rep}(\text{ActiveTxn},\ start_state,\ cur_state) := \ \enspace\enspace \text{COMMITBLOCK} \mapsto \braket{0,\ \emptyset} \ \enspace\enspace\enspace\enspace * \ \enspace\enspace (\forall a,\ start_state[a] = v \to a \mapsto \braket{v,\ \emptyset}) \land \text{replay}(start_state,\ InMemoryLog) = cur_state$

# CHL: Recovery Execution Semantics

诸如 atomic_two_write 一类的 transactional functions 提供了 all-or-nothing 的保证，然而在其 specification 中仅描述 all-or-nothing 是不够 precise 的；例如极端地讲，如果文件系统实现保证 always nothing ，也是满足该约束的。

CHL 定义了崩溃后恢复行为的具体语义，以获得更精确的 specification ：在未发生崩溃时，事务总是能完成；在发生崩溃时，满足 all-or-nothing property 。

log_recover 的 CHL specification 如下：

\begin{aligned} & \text{SPEC} && \text{log\_recover}() \\ & \text{PRE} && \textbf{disk} :\ \text{log\_intact}(last\_state,\ committed\_state) \\ & \text{POST} && \textbf{disk} :\ \text{log\_rep}(\text{NoTxn},\ last\_state) \lor \text{log\_rep}(\text{NoTxn},\ committed\_state) \\ & \text{CRASH} && \textbf{disk} :\ \text{log\_intact}(last\_state,\ committed\_state) \\ \end{aligned}

CHL 将 log_recover 引入文件系统操作的 CHL specification 中，将执行语义划分为 normal procedure 和 recovery procedure 。以 atomic_two_write 为例：

\begin{aligned} & \text{SPEC} && \text{atomic\_two\_write}(a_1,\ v_1,\ a_2,\ v_2) >> \text{log\_recover}\\ & \text{PRE} && \textbf{disk} :\ \text{log\_rep}(\text{NoTxn},\ start\_state) \\ &&& \textbf{start\_state} :\ a_1 \mapsto v_x * a_2 \mapsto v_y * others \\ & \text{POST} && \textbf{disk} :\ \text{log\_rep}(\text{NoTxn},\ new\_state) \lor (ret = \text{RECOVERED} \land \text{log\_rep}(\text{NoTxn},\ start\_state)) \\ &&& \textbf{new\_state} :\ a_1 \mapsto v_1 * a_2 \mapsto v_2 * others \end{aligned}

引入额外的 ret 变量来指示函数执行终止后的状态（即 normal / recovery procedure），不再需要原先的 crash condition ，而更精确地描述函数的崩溃时行为，

# Proving CHL Specifications

对于给定待验证的 procedure $p$ ，CHL 自动化验证的流程如下：

假定 $p$ 内的每一步骤（例如调用的子过程）都已被证明，否则应当先予以证明。

首先，根据 $p$ 的控制流串联所有步骤的 postcondition 和 precondition ，自动生成 proof obligations ，并递归地匹配前后步骤的 logical address spaces ：

前一步骤的 postcondition 蕴含（ $\to$ ）后一步骤的 precondition 。链上初始为 $p$ 的 precondition ，末尾为 $p$ 的 postcondition 。
每一步骤的 crash condition 蕴含 $p$ 的 crash condition 。

例如对于 atomic_two_write ：

然后，对于 trivial 的 proof obligations 直接完成证明，否则利用分离逻辑来完成步骤内 precondition 到 postcondition 的信息传递，并完成证明。

有些 proof obligations 中的蕴含关系无法被自动证明（为什么？），需要开发人员手动完成。这种情况出现在不同抽象层级之间，例如一个谓词中的目录由 filename -> inode number 的映射表示，而另一个谓词中的目录由 file 对象的 directory entries 表示。

例如对于 atomic_two_write 中第一次调用的 log_write ：

TBD.

# FSCQ 设计和实现

TBD.

# ASPLOS'16 - Ferrite

本文提出了崩溃一致性模型来精确描述文件系统在崩溃时的行为正确性标准，并实现了 Ferrite 框架以支持 testcases, specifications 和 implementation 之间的交叉验证。

ASPLOS'16 - Specifying and Checking File System Crash-Consistency Models
Taxonomy : system verification / file system
Tag : crash consistency / correctness criteria

# Crash Consistency Model

POSIX 标准定义了 fsync 系统调用的 rationale ，但严重缺乏对其它系统调用的崩溃时行为的明确定义，甚至是完全没有定义。

尽管现代操作系统都应用了各种不同的技术来保障崩溃时的数据完整性，精确描述文件系统的崩溃时行为仍面临以下挑战：

out-of-order writes ：现代操作系统都具有复杂的 multi-layer I/O stack ，每一层都实现了自己的优化机制，从不同抽象层次打乱最终数据写入磁盘的顺序。
** ：
** ：

本文提出了 崩溃一致性模型 (crash consistency model) 来精确描述文件系统在崩溃时的行为正确性标准，使上层应用的开发者无需调查底层系统的实现。

崩溃一致性模型由两个部分组成：

litmus tests ：由一组小规模程序组成，直观但不完备地描述了文件系统崩溃时一些被允许或被禁止的行为。
formal specifications ：使用形式化方法（逻辑语言或状态机）描述的文件系统崩溃时所有行为的正确性，提供了自动化证明的基础。

本文实现了用于自动化验证文件系统崩溃时行为正确性的工具箱 Ferrite 。

本文所验证的文件系统都兼容 POSIX 标准，运行的都是单线程程序，且都仅挂载单个磁盘。

# Litmus Tests

每个 litmus test 由三部分组成，initial setup 和 main body 包含一系列文件系统操作，而 final checking 则包含一系列的 predicates ：

initial setup 用于创建初始文件系统状态，其执行总会成功且不会发生崩溃，由隐式的 sync 确保其完成。
程序执行可以在 main body 内的任意位置崩溃。由于每个文件系统操作是 atomic 的，实际上是在任意两个操作之间崩溃。
- 特殊函数 mark 用于标记对外可见的事件，例如输出到屏幕或反馈信息给上层应用等。
final checking predicate 为真意味着存在某个 crash trace 使得程序状态满足该条件。
- 辅助函数 content(name) 返回对应文件的数据内容，marked(label) 返回对应（由 mark 标记的）事件是否在程序崩溃之前发生。

prefix-append (PA)

TBD.

ordered-file-overwrites

实验结果表明，许多文件系统对其崩溃时数据完整性的描述是含糊其辞的，容易使应用程序开发者误解的，而 litmus tests 精确地描述了这些正确性标准。

# Formal Specifications

本文提供了两种不同的形式 formal specification ：axiomatic model 是定义描述式的，而 operational model 是状态机抽象描述的。

axiomatic models 在一组概念定义的基础上用一组定理和排序关系来描述正确的崩溃时行为。
operational models 类似于操作语义，用包含 non-deterministic event 的状态机来描述程序的崩溃及其崩溃时行为。

Ferrite 的实现中使用的是用 Rosette 编写的 axiomatic specification 。

sequential consistency model (SCC) 是最强的模型，

真实文件系统所实现的模型都比 SCC 更弱，例如 ext4 的模型：xxx

TBD.

# Ferrite 设计和实现

Ferrite 由两个部分组成：

enumerator 用于测试文件系统的实际实现是否能通过所有 litmus tests ，即 excuting tests against implementations ；
model checker 用于验证 litmus tests 所表征的崩溃时行为正确性是否符合给定的 formal specification 中的描述，即 executing tests against specifications 。

enumerator

对于给定的文件系统实现和 litmus test ，Ferrite enumerator 枚举所有可能的 crash trace ，输出所有可能的崩溃后程序状态。

；

model checker

根据并发领域 memory model 相关测试工作的经验，类似地，为给定的崩溃一致性模型编写 formal specification 很容易产生偏差，包括可能会 under-constrained 或 over-constrained 。

；

# Experience with Specifications

；

# OSDI'16 - Yggdrasil

Yggdrasil 提出了 crash refinement 的概念，显著减小了文件系统验证的 proof burden ，避免使用晦涩难懂的形式化语言来编写 specification 。

Yggdrasil
Taxonomy : system verification / file system / push-button verification
Tag : crash consistency / symbolic execution

# Optimization Handling

# SOSP'17 - DFSCQ

DFSCQ
Taxonomy : system verification / file system
Tag : crash consistency / hoare logic / separation logic / Coq
Preceding Work : SOSP'15 - FSCQ

#Research #Paper Reading #Verification #File System Verification

← Reading Papers - Fuzzing (Others) Reading Papers - Concurrency Testing Overview (unfinished)→