FSCQ文件系统

写于 | 归档 | | 翻阅:
| 共计: 8.8k 字 | 时长 ≈ 31 min

FSCQ：可以应对crash的文件系统，with a machine-checkable proof (using the Coq proof assistant) 为说明FSCQ的定理，本文介绍了Crash Hoare Logic（CHL），它扩展了传统的Hoare逻辑，包括崩溃条件，恢复过程和用于指定不同抽象级别磁盘状态的逻辑地址空间。

FSCQ论文

基础背景

文件系统

为避免操作系统知识的遗忘而影响接下来的阅读体验，这里简单给出一点OS文件系统的基础知识。

所谓文件系统，就是文件的储存方式。简单说，它就是一个门牌系统，为储存设备划分门牌号，每个文件分配一个门牌，然后就能按照门牌找到文件。没有文件系统的硬盘，就是片原始丛林，你根本不知道那户文件住在哪，就更别谈去高效访问了。

文件存取单位

文件储存在硬盘上，硬盘最小存储单位叫做扇区（Sector），每个扇区储存512字节（0.5KB）但OS读取硬盘时，不会一个个扇区地读取，而是一次性连续读取多个扇区以提高效率，即一次性读取一个块（block）。这种由多个扇区组成的块，是文件存取的最小单位。块的大小，最常见的是4KB，即连续八个 sector 组成一个 block。

索引节点 iNode

文件数据都储存在块中，但还须找个地方来储存文件的元信息，比如文件的创建者、创建日期、文件大小等。这种储存文件元信息的区域就叫做索引节点（inode）。每一个文件都有对应的inode，里面包含了除文件名外与该文件有关的一些信息。Unix系统内部不使用文件名，而用inode号码来识别文件。对系统来说，文件名只是inode号码便于识别的别称或者绰号。表面上用户通过文件名打开文件，实际上系统内部这个过程分成三步：1. 系统找到该文件名对应的inode号码；2. 通过inode号码，获取inode信息；3. 根据inode信息，找到文件数据所在的block，读出数据。

目录文件

Unix系统中目录（directory）也是一种文件。打开目录，实际是在打开目录文件。目录文件的结构非常简单，就是一系列目录项（dirent）的列表。每个目录项由两部分组成：文件名和该文件名对应的inode号码。

以ls命令为例，ls命令只列出目录文件中的所有文件名；ls -i命令列出整个目录文件，即文件名和inode号码；ls -l查看文件的详细信息，即必须要根据inode号码，访问inode节点。

目录文件的读权限r和写权限w，都是针对目录文件本身。由于目录文件内只有文件名和inode号码，所以如果只有读权限，只能获取文件名，无法获取其他信息，因为其他信息都储存在inode节点中，而读取inode节点内的信息需要目录文件的执行权限x。

硬链接

Unix系统允许多个文件名指向同一个inode号码。也即可以用不同的文件名访问同样的内容；对文件内容进行修改，会影响到所有文件名；但删除一个文件名，不影响另一个文件名的访问。这种被称为硬链接（hard link）

运行ln命令后，源文件与目标文件的inode号码相同，即指向同一个inode。inode信息中有一项叫做”链接数Links”，记录指向该inode的文件名总数，这时就会加1。反过来，删除一个文件名，inode节点中Links减1。当Links值减到0，表明没有文件名指向这个inode，系统就会回收这个inode号码及其所对应block区域。

目录文件的链接数：创建目录时，默认生成两个目录项：”.”和”..”。前者的inode号码就是当前目录的inode号码，等同于当前目录的硬链接；后者的inode号码就是当前目录的父目录的inode号码，等同于父目录的硬链接。所以，任何一个目录的硬链接总数，总是等于2加上它的子目录总数（含隐藏目录）。

软链接

除硬链接外，还有种特殊情况，文件A和文件B的inode号码虽然不一样，但文件A的内容是文件B的路径。读取文件A时，系统会自动将访问者导向文件B。即无论打开哪一个文件，最终读取的都是文件B。这时，文件A就称为文件B的软链接（soft link）或符号链接（symbolic link）。软链接类似于Windows的快捷方式，ln -s命令可以创建软链接。文件A依赖文件B存在，如果删除文件B，打开文件A就会报错：No such file or directory。

iNode特殊作用

由于inode号码与文件名分离，这种机制导致了一些Unix系统特有的现象：

  1. 有时文件名包含特殊字符，无法正常删除。这时，直接删除inode节点，就能起到删除文件的作用。
  2. 移动文件或重命名文件，只改变文件名，不影响inode号码。
  3. 打开一个文件以后，系统就以inode号码来识别这个文件，不再考虑文件名。因此，通常来说，系统无法从inode号码得知文件名。

第3点使得软件更新变得简单，可以在不关闭软件的情况下进行更新，不需要重启。因为系统通过inode号码，识别运行中的文件，不通过文件名。更新的时候，新版文件以同样的文件名，生成一个新的inode，不会影响到运行中的文件。等到下一次运行这个软件的时候，文件名就自动指向新版文件，旧版文件的inode则被回收。

数据缓存区

访问磁盘比访问内存要慢几个数量级，因此需要在内存中维护一块磁盘的数据缓存区。 在读取磁盘时，先从缓冲区中查找想要读取的块是否已经缓存了，如果没有的话才会到磁盘去把数据块取回来，在写磁盘时，也会先把数据写到缓存区。如果缓存区已满，则通常会把最不常访问的数据驱逐出缓存区，为新的数据腾出空间。数据缓冲区在写时，可以选择直接将数据同步写到磁盘里（直写），或者将写延迟，直到数据块被驱逐的时候再写（写回）。

实例

$ who > userlist 在文件系统中增加了一个存放命令who输出内容的新文件。

  1. 存储属性：也就是文件属性的存储，内核先找到一块空的inode节点（内核找到inode节点号47）内核把文件元信息记录其中，如文件的大小、文件所有者、和创建时间等。
  2. 存储数据：即文件内容的存储，假设该文件需要3个数据块。因此内核从自由块的列表中找到3个自由块（中分别为627、200、992，内核缓冲区的第一块数据复制到块627，第二和第三分别复制到200和992）
  3. 记录分配情况：数据保存到了627、200、992三个数据块中，分配情况记录在文件的inode节点中的磁盘序号列表里。这3个编号分别放在最开始的3个位置。
  4. 添加文件名到目录：新文件的名字是userlist， 内核将文件的入口 (47,userlist) 添加到目录文件里。文件名和inode节点号之间的对应关系将文件名和文件及其内容属性连接起来，找到文件名就找到文件的inode节点号，通过inode节点号就能找到文件的属性和内容。

FSCQ_createFile.png

cp /path/src /path/dst 在path路径下新建dst文件，内容为同目录下的src文件内容。
文件系统首先需要从目录树中定位src文件位置，为此，它在根目录条目中找到“path”（通常已经缓存在数据缓存区里），拿到 path 的索引值 ipath，将path的目录条目加载到数据缓存区中，定位和名称“src”相对应的索引值isrc， 然后文件系统读取 isrc 索引节点的文件内容。要创建目标文件，文件系统将分配一个新的索引节点 idst，并在 inode 分配位图中标记为已使用，然后根据 src 文件大小来给 dst 文件分配新的磁盘块，在 idst 中记录分配的块号，并且在块的的数据位图中将其标记为已使用，再将 src 的内容写入到新分配的块中。最后，文件系统将一个新的目录条目 （“dst”，idst）添加到 path 的目录条目中，并将目录的新内容写回到磁盘里。注意：此处的顺序并不能保证崩溃安全性。

崩溃安全性

应用完成某个操作可能涉及到多次写磁盘，该过程中系统可能随时崩溃，有可能一个写操作只完成一部分，崩溃后磁盘会处于一个中间状态，这个状态下数据可能不一致，因此再重启之后通常需要运行一个恢复程序，检查磁盘的状态，将其恢复到一个数据一致的状态，以便将来能继续正确执行程序，文件系统的这种属性称为崩溃安全性。

写屏障（磁盘同步）

现代硬盘驱动通常会增加一层缓存来优化 I/O 实际写入磁盘的顺序，即发给磁盘的写入不会立即持久化，最近的写往往会被缓存在内部缓存中，并由硬盘驱动器决定什么时候会将这些未完成的写刷到磁盘。同时，硬盘驱动器可以对这些写重新排序进行写入以提高磁盘吞吐量。假如系统没有崩溃，一个读总是能够读到最新写得值，但假如系统崩溃并重启，可能会发现崩溃之前稍后发出的写持久到了磁盘，但是之前的写却没有。

硬盘驱动器提供了写屏障操作，称为磁盘同步，这会强制将写的缓存全部刷到磁盘上，磁盘同步操作可以用来保证不会有未完成的写操作，之前所有的写都会保留在磁盘上。但是磁盘同步非常的耗时，应当尽可能的避免，而这种异步的 I/O 使得论证崩溃安全性变得更加复杂。

预写式日志 WAL

许多文件系统操作涉及多个对磁盘的写。例如，创建文件至少涉及两个写操作，分配未使用的索引节点，并将索引节点添加到父目录中。如果系统在两次写之间崩溃，则索引节点在索引节点位图中可能被标记为已经使用，但却不属于任何一个目录。 文件系统一般会实现事务保证原子性+预写日志来解决这个问题，以确保系统崩溃重新启动的时候，磁盘上的数据结构处于一致的状态。磁盘通常会分配一块固定的区域给日志，日志通常由两部分构成，一部分是连续的日志条目，每个日志条目记录希望对磁盘进行的写操作，另一部分是 一个单一的提交块，记录日志条目的数量。

日志协议

一个基本的日志协议工作如下：（1）日志记录系统为文件系统的一个操作开启一个事务log_begin() （2）对于该操作引发的每一个磁盘写入的地址和值，日志记录系统向日志条目附加一个新的地址/值对log_write() （3）当日志记录系统提交事务log_commit()时，它会发出一个磁盘同步来保存磁盘上的日志条目，然后更新提交块以反映日志的长度，然后再次同步磁盘以完成这个事务（4）日志系统将日志中的修改应用到实际的磁盘位置，并发出磁盘同步将更改持久化到磁盘上（5）最后，将零写入提交块来截断日志，并同步到磁盘上（6）无论何时系统崩溃并重新启动，都会运行恢复过程。它根据提交块的长度读取日志；如果日志不为空，则跳到步骤（4）重新执行。

上述协议的正确性依赖于一个重要的假设：更新提交块是原子的同步的操作。原子性确保了提交块上要么是原长度，要么是新长度，同步则保证了磁盘控制器不会对磁盘的写操作进行重新排序，将提交块的写和其他的写调换顺序，这是通过在更新提交块之前和之后发出两个屏障（磁盘同步操作）来强制执行。在这个协议下，在事务中途，还没有更新提交块之前系统崩溃的话，提交块的长度为零，此时磁盘的数据没有被写，这个事务就像没有执行一 样，数据处于一致的状态；提交之后但在应用完成之前的系统崩溃将导致提交块长度非零，并且日志中包含相同数目的有效条目，这时就只需要重新执行提交操作，会达到事务执行完的状态。 这个基本的日志协议会增加磁盘写操作以及耗时的磁盘同步操作。例如，写入单个磁盘块的操作将需要完成四次磁盘写入（两次为提交块，两次为块的内容）和四个磁盘同步（上文加粗处）。

举例说明

1
2
3
4
5
def atomic_two_write(a1, v1, a2, v2): 
	log_begin() 
	log_write(a1, v1) 
	log_write(a2, v2) 
	log_commit()

该过程使用预写日志在事务内部执行两次磁盘写操作，该日志提供log_begin，log_commit和log_write的API，log_write() 将块的内容追加到内存日志中，而不是直接更新磁盘块。log_commit() 将日志写入磁盘，写入提交记录，然后将块内容从日志复制到磁盘上的块位置。如果此过程崩溃且系统重新启动，则将运行事务系统的恢复过程。恢复过程将查找提交记录。如果存在提交记录，它将通过将日志中的块内容复制到正确的位置来完成事务，然后清除日志。如果没有提交记录，则恢复过程仅清除日志。
如果恢复期间发生崩溃，则重新启动后，恢复过程将再次运行。不管崩溃多少次，只要恢复完成，则两个块要么都已更新，要么都未更新。因此，atomic_two_write过程中，事务系统保证无论怎么崩溃，两次写入要么都发生，要么都不发生。

日志优化

  1. 延迟应用日志：日志系统提交事务后，并不立即应用日志，而是等日志填满后，再一次性将日志内容应用。可以将每个事务的磁盘同步由四个 降为两个，同时将写磁盘的次数也由四次降为两次。

  2. 组提交：在内存中累积多个系统调用的写入，并将其合并到单个事物当中。

  3. 其实还有蛮多优化的，这里就不一一列举了……反正论文后续也用不太到。

CHL框架

CHL (Crash Hoare Logic) 框架是用 Coq 实现的用来书写规范的框架，它允许文件系统开发人员编写包含崩溃条件和恢复过程的规范，并提供了较好的证明自动化的支持。这涉及到了形式化验证的知识，我也只是刚有个模糊的认识。FSCQ 是从 Coq 提取出 Haskell 代码，再进一步获得可执行的文件系统，因此具有较高的 CPU 开销。

Haskell是一门纯粹的函数式编程语言。

Coq 是一种基于构造演算的证明助手，被用于形式化各种领域的证明，包括数学和编程语言。如果对其感兴趣想了解更多，可以参照此网站进一步学习 -> https://github.com/coq/coq/wiki#coq-tutorials

磁盘模型

磁盘被定义成从整数块号a到内容v的偏函数a → v，其中超过磁盘范围的块号不会映射到任何东西。

因为I/O写入并不是同步的，中间会经过buffer异步写入磁盘。为了捕获这种异步的性质，CHL 用一个值集（v,vs）来描述一个块的内容，而不是一个单一的值，其中 v 代表着这个地址最近写入的值， 而 vs 是一系列的之前写入的值，假如系统突然崩溃，v 和 vs 中的任何一个值都可能出现在磁盘上。而磁盘同步操作意味着对应的缓存已经全部应用到该地址上，先前写入的值已经全部处理，即 vs 为 ∅，最新的值会出现在崩溃之后，否则，这个磁盘块就是未同步的。 CHL 的磁盘模型假设块是原子写的，也就是说，在系统崩溃之后，块必须包含最后写入的值或者是先前值中的一个，并且不允许部分块写入。

崩溃条件

给定了异步磁盘模型，我们还需要一种手段来描述可能崩溃的中间状态，CHL 将霍尔逻辑扩展成一个具有崩溃条件的四元组， 写为：{P}C{Q}{R} 其中 P 是前置条件，描述C过程之前应满足的状态；Q 是后置条件，描述 C 在没有崩溃情况下执行结束时的状态，而 R 是描述 C 执行过程中可能发生的中间状态的崩溃条件。 我们以disk_write(a, v)举例：

前置条件：a -> (v0, vs) * other_blocks
后置条件：a -> (v, {v0} U vs) * other_blocks
崩溃条件：a -> (v0, vs) * other_blocks ∨ a -> (v, {v0} U vs) * other_blocks

推理过程disk_write(a, v)，即把值v写到地址a上。其前置条件声明的是磁盘上地址 a 的地方指向的值是一个集合，v0是最新写入的值，vs则表示之前写入的值的序列，除 a 以外的地址满足谓词other_blocks；其后置条件说的是 a 以外的值依旧满足谓词other_blocks，而地址 a 指向的值的集合中，最新元素是v，旧的值则是由vs加上v0组成的序列；由于磁盘写是一个原子操作，因此它要么完成了值的写入，要么没有完成，因此可能发生系统崩溃时有两种状态，一是前置条件的状态，二是后置条件的状态，通过将前置条件和后置条件并起来则表示了系统崩溃时可能的所有状态，即系统崩溃时必须满足的谓词。

磁盘写的规范说明还表明了真实磁盘的两个重要行为，保证了磁盘的性能：

  • 磁盘实际 I/O 可以异步发生
  • 磁盘的写可以重新排序

因为一个地址a会指向一组值而不是一个值，指向一组值表明系统崩溃恢复的时候，磁盘上的值可能是之前的某个值，而不同地址之间可能会呈现出不一致的状态，这也表明了磁盘对写进行了重新排序。

CHL 的崩溃条件有一个微妙的地方，他们描述的是系统崩溃之前磁盘的状态，而不是系统崩溃之后。在崩溃后，CHL 磁盘模型认为，每个块将从崩溃之前的值的集合中选择一个值，例如disk_write(a, v)的前置条件中表明，磁盘的 a 地址指向的可能是一系列值的集合，而不是一个值（明确表示a地址只指向一个值时，需要声明a → (v, ∅) 即之前写入序列为空集）这样的好处就是，崩溃条件会跟前置条件和后置条件类似，有利于证明自动化。

逻辑地址空间

文件系统的许多地方涉及到逻辑地址空间。例如，磁盘是从磁盘块号到磁盘块内容的地址空间；文件索引层是从文件索引号到文件索引的地址空间；每个文件里，是从该文件中的偏移量到数据的地址空间；目录是从文件名到索引节点号的地址空间。基于这个观察，CHL 扩展了关于磁盘推理的分离逻辑， 使其以同样的方式表达诸如文件，目录或逻辑文件内容的更高级的地址空间。

作为逻辑地址空间的实例，我们考虑 inc_two 的简单过程，inc_two 表达在一个操作中需要同时更新两个块的文件系统调用。我们先读取两个块的内容，然后将这两个块的内容加一，再写回。该过程使用日志系统提供的 log_begin 开始一个事务，用 log_read 来读取数据，然后用 log_write 来写数据，最后用 log_commit 来提交事务。假如在执行 inc_two 的过程中发生了系统崩溃并且重新启动，首先系统会运行 log_recover 这个恢复程序，如果在恢复过程中依然发生系统崩溃，则重新启动后，恢复过程将再次运行。原则上来说恢复过程可能运行若干次。尽管如此，只要 log_recover 完成， 日志记录系统就能保证两个写入要么都发生，要么都没有发生，不管经历了多少次系统崩溃。

为了简化说明，我们假设现在的日志系统只是采用前面所述的基础的日志协议:

SPEC inc_two(a1, a2)

PRE disk: log_rep(NoTxn, start_state)
start_state: a1 → (v_x, vs_x) ⋆ a2 → (v_y, vs_y) ⋆ others

POST disk: log_rep(NoTxn, new_state)
new_state: a1 → (v_x+1, ∅) ⋆ a2 → (v_y+1, ∅) ⋆ others

CRASH disk: log_intact(start_state, new_state)

前置条件中，a1 → (v_x, vs_x) 适用于日志系统提供的逻辑磁盘的地址空间，后置条件中，a1 → (v_x+1, ∅) 适用于逻辑磁盘的新的内容。就像物理磁盘一样，这个地址空间也是从地址到值的偏函数。与物理磁盘不同的是，通过日志系统写入逻辑磁盘的操作展现的是一个同步的接口，即整个操作完成之后，能保证要写入地址的值被刷到磁盘上，因此在后置条件中，我们看到的是单个同步的值，这层抽象做的具体的事情就是隐藏更下层的异步的接口，这也是引入地址空间的好处。

我们在 log_rep 将逻辑地址空间和实际的物理磁盘连接起来。例如，log_rep(NoTxn, start_state) 表示磁盘没有活动事务，并且处于状态start_state。。通过 log_rep 的这层转化，对逻辑地址空间的描述将会变成对物理磁盘的描述，并且隐藏了一 些琐碎的细节。log_rep 将会把逻辑地址空间作为参数，结合日志系统的状态和逻辑磁盘状态准确的反映出物理磁盘上的状态。日志系统中有好几个可能的状态：

  1. NoTxn ：表示当前磁盘没有事务活动。
  2. ActiveTxn ：表示活跃状态中的事务所有的修改只会发生在内存中。
  3. FlushedUnsync ：表示此时开始进入提交事务的过程，首先把内存中的修改刷到数据缓冲区的日志记录区中，Unsync表示还没有刷到磁盘上。
  4. Flushed ：表示此时有了一次磁盘同步，已经将日志数据区的内容刷到了磁盘上。
  5. CommittedUnsync ：表示我们现在将提交块写到了数据缓冲区里，但还没有同步到磁盘里。
  6. Committed ：表示提交块被同步到了磁盘里，这个点之前和之后作为事务是否完成的分界点。
  7. AppliedUnsync ：表示现在已经开始将数据缓存区里日志的内容实际应用到磁盘上。
  8. AppliedSync ：表示日志应用的工作已经完全反映到了磁盘上，整个事务至此完成。

崩溃条件中使用的 log_intact(d1, d2) 表示可以使过程C崩溃的所有状态，该状态代表恢复到事务状态d1或d2的所有可能的log_rep状态。log_intact(start_state, new_state) 可使我们简洁地捕获atomic_two_write期间所有可能的崩溃状态，包括atomic_two_write可能调用的任何过程内部的崩溃（例如log_commit内的崩溃）

恢复执行语义

计算机遇到崩溃并重新启动后，它会在恢复正常操作前先运行恢复程序（如 log_recover）。崩溃条件和地址空间可以指定计算机在执行过程中可能会崩溃的状态， 但还需要一种证明恢复过程正确性的方法（包括恢复期间的系统崩溃）。日志系统必须在每次崩溃后运行 log_recover 来将已提交的事务继续做完，包括在运行 log_recover 本身发生崩溃之后。 log_recover 指出，从与 log_would_recover(last_state, committed_state) 相匹配的任何状态开始，log_recover 会将事务回滚到 last_state 或将提交的事务继续执行到 committed_state。此外，log_recover 的规范是幂等的，因此它的崩溃条件等同于其前置条件，这将允许 log_recover 在执行的过程中崩溃多次。

SPEC log_recover()
PRE disk: log_intact(last_state, committed_state)
POST disk: log_rep(NoTxn, last_state) ∨ log_rep(NoTxn, committed_state)
CRASH disk: log_intact(last_state, committed_state)

为了表达 log_recover 在遇到崩溃之后运行，CHL 提供了恢复执行语义。恢复执行语义考虑了两个程序的执行，一个是正常程序，一个是恢复程序，并且要么产生一个错误，一个完成状态（正常程序完成执行）或者一个恢复状态（恢复程序完成执行）。这种模型下，首先正常程序尝试完成，但如果系统崩溃，它将开始运行恢复程序，如果再回复过程中系统崩溃，有可能需要多次运行恢复程序，最终达到恢复状态的过程。

由此我们对崩溃霍尔逻辑扩展恢复执行语义，扩展后{P}C≫R{Q}表示，假如 C 在满足前置条件 P 下执行，且每当系统在 C 崩溃或 R 自身崩溃时执行恢复过程 R，则当 C 或 R 终止时，条件 Q 将成 立。 我们可以由此扩展 inc_two 规范以包括恢复执行：

SPEC inc_two(a1, a2) ≫ log_recover

PRE disk: log_rep(NoTxn, start_state)
start_state: F ⋆ a1 → (v_x, vs_x) ⋆ a2 → (v_y, vs_y)

POST disk: log_rep(NoTxn, new_state) ∨ (status = recovered ∧ log_rep(NoTxn, start_state))
new_state: F ⋆ a1 → (v_x+1, ∅) ⋆ a2 → (v_y+1, ∅)

后置条件表示，如果 inc_two 在没有崩溃的情况下完成，则两个块都已经更新，或者两者都没有更新，这时一定是因为发生了崩溃，运行恢复程序之后达到了原状态。状态变量 status 指示系统当前状态。

证明规范

证明自动化

为证明一个程序 C 是正确的，我们需证明如果 C 执行，且执行前 C 前置条件成立，那么，C 的后置条件的正常运行之后成立，且恢复条件在恢复程序运行之后成立。

正常执行下，我们必须证明顶层程序的前置条件蕴含第一个子过程的前置条件，第一个子程序的后置条件蕴含着接下来要执行程序的前置条件，并这样一直下去。 对于崩溃，我们则必须证明每个过程的崩溃条件都蕴含这恢复程序的前置条件，恢复程序的后置条件蕴含着顶层程序的恢复条件。 在这两种情况下，逻辑蕴涵关系都按着控制流的方向传递，在 CHL 框架里面，有用策略语言写好的证明搜索的 Ltac 程序，假如前置条件很容易被之前程序的后置条件蕴涵，那么 Ltac 程序可以自动完成这个过程，开发人员不需要进行手动的证明，在实际中，通常开发人员只需要证明程序的不变量的成立。

证明崩溃条件规范

程序分解

CHL 的第一个阶段是使用 组合规则 将证明目标分解成一系列的证明义务。具体来说，CHL 会考虑 C 中的每个步骤，并查看每个步骤的前置条件和后置条件，假设每个小的步骤已经有一个证明好了的规范，比如最基本的磁盘读写，同步操作。CHL 首先假设 C 前置条件成立，并为每个步骤产生两个证明义务，（1）当前所能给定的条件，要么是 C 的前置条件（即当前步骤为第一步骤），要么是前一个步骤的后置条件，不管是那种情况，都要求给定条件能蕴涵当前步骤的前置条件；（2） 当前步骤的崩溃条件蕴涵 C 的崩溃条件（小范围推出大范围）。而对程序 C 的最后一个小步骤，会产生最后一个步骤蕴涵 C 的后置条件的证明义务。

组合规则：{P1}C1{P2}{R1} {P2}C2{P3}{R2}B -> {P1}C1; C2{P3}{R1∨R2}
正常运行，P1→C1→P2→C2→P3；如若崩溃，可能在C1可能在C2，故用∨

谓词蕴涵

有些程序分解之后产生的证明义务很容易证明，CHL 根据一阶逻辑会立即证明这个蕴涵成立。 对更复杂的情况，CHL 会依赖于分离逻辑的 结构规则 来证明。当 inc_two 第一次调用 log_write 时，我们需要证明F1 ⋆ a1 → (v_x, vs_x) ⋆ a2 → (v_y, vs_y) 蕴涵 F ⋆ a → (v0, vs0)，CHL 会自动将 a1 → (v_x, vs_x) 与a → (v0, vs0) 匹配，并将这些项从证明义务的两边同时去掉，然后将 F 匹配为F1 ⋆ a2 → (v_y, vs_y)，这样会将这个证明义务完成，然后将a2 → (v_y, vs_y) 的信息带入到接下来的证明义务中。

蕴涵：如果P，那么Q，表示为P→Q。蕴涵式中，只有当P真Q假时判断为假，其余均为真。
结构规则：{P}C{Q}{R} -> {P⋆S}C{Q⋆S}{R⋆S}

证明恢复语义规范

如果恢复程序是幂等的，CHL 可以使用崩溃条件的规范直接来证明具有恢复条件的规范，证明恢复规范的规则称为恢复规则：对程序C有 {P}C{Q}{T} 当崩溃条件T触发时，启用恢复语义 {T}R{S}{T} 即可推出 {P}C≫R{Q∨S}

恢复规则说的是假如恢复过程的前置条件既是C的崩溃条件又是自身的崩溃条件，如果 C 和 R 的后置条件分别是 Q 和 S，那么将C和R一起运行的结果就是Q∨S

文件系统构建

FSCQ参照xv6文件系统设计，但不支持多处理器，同时采用单独的位图来分配索引节点。

系统结构

FscqLog提供了一个简单的预写日志，FSCQ使用它来原子地更新几个磁盘块。其他组件提供标准文件系统抽象的简单实现。缓存模块提供缓冲区缓存。 Balloc实现了一个位图分配器，用于块和inode分配。索引节点实现索引节点层；这里最有趣的逻辑是将直接块和间接块组合在一起，形成单个块地址列表。 Inode调用Balloc分配间接块。 BFile实现了一个块级文件接口，在更高级别上公开了一个接口，其中每个文件都是一个块列表。 BFile调用Balloc分配文件数据块。 Dir在块级文件的顶部实现目录。 ByteFile实现文件的字节级接口，其中每个文件都是字节数组。 DirTree将目录和字节级文件组合为分层目录树结构；在创建/删除文件或子目录时，它调用Balloc来分配/取消分配索引节点。最后，FSCQ在事务中实现完整的系统调用。

磁盘模型

FSCQ 崩溃后，并非每次发出的写入都将反映在磁盘状态中。 CHL模型的另外两个磁盘操作是读取磁盘块（disk_read），并等待所有写操作到达非易失性内存（disk_sync）disk_sync将块地址作为附加参数，以指示必须同步的块。 disk_sync的按地址变体会丢弃该块的所有先前值，从而使最后写入的值成为崩溃后可能出现的唯一可能值。在执行时，每个地址disk_syncs的连续调用被折叠为单个全局disk_sync操作，以实现所需的性能。

POSIX接口

FSCQ在顶层提供类似于POSIX的接口。 与POSIX的主要区别是：FSCQ不支持硬链接，以及 FSCQ不实现文件描述符，而是需要按索引节点编号命名打开的文件。 FSCQ依靠FUSE驱动程序来维护打开文件描述符和inode编号之间的映射。

FscqLog

FscqLog一次仅允许一个事务，并假定内存足够大以容纳当前事务的内存日志。但即使对于这种简单的设计，日志记录协议也很复杂，因为disk_write是异步的。崩溃后，FSCQ的恢复过程fs_recover读取布局块以确定日志的位置，然后调用FscqLog的log_recover将磁盘置于一致状态。
FSCQ仅通过log_write更新磁盘，并将这些写入以sysCall的粒度包装到事务中，以实现崩溃安全。此外，它为上级软件提供了一个更简单的同步接口。因为事务API公开了一个逻辑地址空间，该逻辑地址空间会将每个块映射到唯一的块内容，哪怕物理磁盘会将每个块映射到最后写入值和一组先前值的元组。因此，在FscqLog之上编写的软件不必担心异步写入。