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 。