Reading Papers 01 - Model Checking
# Model Checking
# Distributed System
# NSDI'09 - MoDist (to-be-readed)
# SOSP'11 - DIR (to-be-reviewed)
dynamic interface reduction (DIR) 是模型检验的一种新的状态空间缩减技术。DEMETER 是实现了 DIR 技术的框架,基于该框架能够在已有的 model checker 中以合理的工作量实现 DIR 技术。
DIR 基于以下两个原则:
分别检查不同组件 :
使用良好定义的接口来封装软件复杂性是实践中常见的做法。基于这一点,model checker 可以认为被测软件系统是由一组 组件 (component) 构成的,每个组件都向软件系统的其它部分提供一组良好定义的接口。
更一般地,所有导致一个组件影响到另一个组件的行为(例如共享内存,failure correlatons ,或其它隐式通道)都由 接口行为 (interface behaviour) 捕获。除接口行为外的其它行为都是包含在局部状态空间内的。
组件之间通过 接口对象 (interface object) 进行交互,例如通信通道或共享对象等。 给定每个组件的接口行为,DIR 可以分别检查每个组件的局部状态空间,尽可能避免对全局状态空间进行不必要的搜索。
动态地发现接口行为 :
DIR 真实地运行目标组件,并在状态空间的探索过程中动态地发现各组件的接口行为。
# OSDI'14 - SAMC
利用 white-box 的信息作为指导以删减冗余的事件交错,即根据分布式系统中各节点对 message 的处理方式,判定 message 之间的依赖关系,并避免枚举 independent message 之间的交错。
基于四种 semantic-aware 的删减策略,由测试人员补全 protocol-specific 的谓词函数 。
Local-Message Independence (LMI) : Discard, Increment, Constant, Modify
Crash-Message Independence (CMI) : Global/Local Impact
message event vs crash/reboot event :前者只能删减冗余的事件交错,但后者是 model checker 引入的,因而如不必要则可删减事件本身。
Crash Recovery Symmetry (CRS) :不同节点的崩溃可能引起 symmetrical 的 recovery 行为,即产生相同的 message 并以相同的方式改变节点的局部状态。从节点的实现中提取影响 recovery 行为的 if 分支,据此在插入 crash event 之前推断如果 crash 将会发生何种 recovery ,维护已执行的 recovery history 并跳过不必要的 crash event 。
Reboot Synchronization Symmetry (RSS) :类似于 CRS 。
# File System / Storage System
# OSDI'04 - FiSC
# OSDI'06 - EXPLODE
EXPLODE 不是把被测系统强行塞入 model checker(将被测系统的一部分删除,或是为被测系统建立复杂模型),而是以 in situ 的方式将控制点交错在整个被测系统中,尽量减少对被测系统的修改,使其能在真实硬件上运行测试。
作者根据几年来的技术研究和使用经验提炼出 model checking 的两个原则,显示了 model checking 的基本特征:系统地对一个状态执行每一个合法的动作,不遗漏任何可能性,并对每个状态重复。
Explore all choices :当一个程序点处可以合法地执行 个不同操作中的一个时,分叉执行 次并分别执行每个操作。
Exhaust states :在探索另一个状态之前,对一个状态执行所有可能的操作。本文中状态被定义为整个被测系统的快照。
model checking 使得低概率事件(例如内存分配失败等)与高概率事件具有相同的发生概率,从而迅速将被检查的系统推向棘手的 corner case 。
而对于在真实的大型系统上进行 model checking ,作者还总结了另外两个原则:
Touch nothing :基于大型系统内部实现的复杂性,尽可能减少对被测系统的修改,按原样运行被测系统。
Report only true errors, deterministically :model checker 标记的错误应该是真正的错误,并尽量约束为确定性的、可重放的路径。这对于特别难以检查的存储系统而言尤其重要,因为不确定性和不可重放引起的代价过大。
# EXPLODE 概述
EXPLODE 是一个可以轻松而彻底地检查真实系统是否存在存储系统 crash-recovery 错误的系统,它为客户端提供了一个干净的框架来构建和插入强大的、可能 system-specific 的 dynamic storage checker 。
EXPLODE 可以在没有源代码的情况下对系统进行检查,这很有价值,因为许多强大的系统依赖于 thirdparty software that must be vetted in the context of the integrated system (?) 。
EXPLODE 和其上的 checker 协同工作,生成所有可能的 crash disk(即如果系统在当前执行点崩溃时可能产生的磁盘映像),然后检查错误。对于被测系统中的每个存储子系统,客户端都需要提供一个存储组件和一个 checker 供 EXPLODE 用来驱动和检查被测系统。该存储组件和 checker 需要实现一组指定的 API 。
在假设资源足够的理想状态下,忽略一些细节,则 EXPLODE 所做的事情非常简单:
创建被测系统的初始状态,并在其上调用
mutate
方法开始检查;每当调用
choose(N)
时fork
出 个状态;根据客户端请求,生成所有可能的 crash disk ,使用底层存储组件修复和安装这些磁盘,然后检查每个磁盘是否被正确地恢复;
当
mutate
方法返回时重新调用它。
EXPLODE 的大部分代码都是在试图用有限资源逼近这个循环,主要是保存和恢复被测系统的机制,使其可以一次运行一个子状态,而不是运行由 fork
生成的指数数量级的进程。
因此,EXPLODE 看起来就像是一个原始的操作系统:它有一个队列来维护当前的进程、一个调度器来选择运行的作业中、以及时间片(对应 mutate
方法的一组调用和返回)。
EXPLODE 的调度算法:在单次 mutate
调用中穷尽所有可能的选择组合。
在发生崩溃之后,被测系统可能有一个 butchered 的内部状态,因此 EXPLODE 需要在继续检查之前将当前状态恢复到它的一个干净副本(即未进行崩溃检查的状态)。此外,用户可以设置一个检查数量阈值以处理 crash disk 种类过多的情况。
EXPLODE 在运行时动态加载 kernel-level 的组件,然后初始化存储系统,再进行检查工作。实时地检查内核可以简化很多事情,但是 EXPLODE 发现的许多错误都会导致内核崩溃,因此 EXPLODE 在虚拟机监视器 VMware Workstation 中运行被测系统。
此外,很容易就可以将 EXPLODE 转换为随机测试框架,只需不再保存和恢复状态,使 choose(N)
不再产生 fork
而返回一个 范围内的随机整数,并记录序列以便于 replay 即可。
# EXPLODE 处理不确定性
EXPLODE 探索一个选择点的流程:检查当前状态 、探索一个选择、恢复 ,然后探索 的其它选择,再探索其它状态。
常见的检查点实现会将当前系统状态复制到一个临时缓冲区,然后在恢复时将其复制回来,然而我们无法简单地保存和恢复运行在原生硬件上的内核。
EXPLODE 使用计算而不是复制来恢复状态,它将被测系统到达状态 的选择序列作为 的检查点,并从干净的初始状态开始 replay 选择序列以恢复状态 。
此方法假设被测系统的代码是 deterministic 的。
此方法的优点是减少了实现的复杂性和工作量,并且相当程度地轻量化了状态检查点的表示。
此方法的问题在于其恢复出的状态的时间戳与原始的时间戳不匹配,这使得对某些时间相关的属性的检查更加困难。
要重新得到初始状态通常需要重启整个系统,这是一种有效但代价很大的方法。而存储系统的特性使其重启的代价要容易接受得多,只需卸载后重新挂载即可。EXPLODE 就是直接调用客户端提供的 unmount
和 mount
方法来完成重启。
恢复状态的成本会随着选择序列的长度而增加。EXPLODE 可以周期性地切断选择序列的前缀,使用指定的磁盘映像作为新的初始状态。
EXPLODE 通过以下方法来保证 replay 的确定性:
过滤不可控的选择:丢弃来自中断上下文的任何调用、以及来自与被测系统无关的任何进程的调用。
控制线程调度:使用优先级来控制存储系统线程何时运行。
此外,许多环境特征会随着运行而改变,提供许多潜在的非确定性输入来源,例如不同位置的线程堆栈、返回不同块的内存分配、具有不同大小的数据结构等。这些扰动都不应该导致被测系统 replay 时的行为与之前不同。幸运的是,存储系统本身有可用性的要求,这会强制系统确保执行相同的用户命令会产生相同的系统状态,而这通常会产生相同的系统执行路径(即经过了相同的 choose
调用)。
- 01
- Reading Papers - Kernel Concurrency06-01
- 02
- Linux Kernel - Source Code Overview05-01
- 03
- Linux Kernel - Per-CPU Storage05-01