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 的谓词函数 $p$ 。

• 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 。