Reading Papers - In-Situ Model Checking
# Stateful Model Checking
# OSDI'02 - CMC
CMC 为被测系统构建 event-driven 的环境模型,其最初的目标是检测网络协议实现,但其最终目标是实现通用的系统代码检查器。
OSDI'02 - CMC - A Pragmatic Approach to Model Checking Real Code
Taxonomy : in-situ / stateful model checking
Tag : network protocol
CMC 将系统建模为一组并发交互的进程的集合,每个进程直接运行 mostly unmodified 的 C/C++ 原始实现代码,而 CMC 负责执行和调度这些进程,并运行一系列检查器。
- CMC 本身作为单个普通进程与其它进程一同运行在操作系统上。
定义 transition 为被测系统运行时可以执行的一个原子步骤,可能包含一系列的指令。transition 的执行顺序决定了被测系统各进程之间的交错。每个进程在被 CMC 调度时可以执行 deterministic 且 non-blocking 的 transition 。
- 在 event-driven 的协议中,每个 event handler 都可以映射到 CMC 中的一个 transition 。
应用 CMC 需要对测试环境建模,要求能够充分地表征被测系统执行的实际环境。CMC 用 CMCChoose(n)
函数(类似 VeriSoft 中的 VS_toss(n)
)表示环境中的不确定性。
环境模型应尽可能细致,以期能尽量减小搜索空间,包括从状态中去除无关成员以及避免检查无关的环境行为。
对于网络协议,环境模型需要伪造除操作系统之外的一切。
检测内存泄漏的标准方法是 mark-and-sweep 算法,但 CMC 的方法不同:从当前状态的副本出发,调用系统实现本身提供的各种清理函数,如果仍存在标记为已分配的内存,则认为存在内存泄漏。
- 这种方法需要额外的人工工作,但也可能发现清理函数实现中的潜在错误。
# CMC 减缓状态空间爆炸
程序中存在不确定性,这导致大量状态都具有不止一个的后继状态。为避免显式地存储程序状态机图,CMC 需要计算每个状态的所有可能的直接后继状态:
对于一个给定的状态,CMC 选定一个进程,选定该进程的一个 enabled 的 event handler 。
然后,CMC 存储选中的进程的上下文、复制当前时刻的堆中数据和全局变量,然后调用选中的 event handler 。
CMC 枚举所有的非确定性选择,重复此过程以生成所有的后继状态。
在存储已访问状态时,CMC 利用 哈希压缩 (hash compression) 来减小内存消耗:在哈希表中存储状态的签名(大小通常为 或 字节)而不是整个状态。这可能会导致哈希冲突,进而导致状态丢失,但其概率低到可以接受(小于等于 )。
- 队列中的状态无法压缩(因为还需其完整信息用于计算后继状态),但是队列的访问具有局部性,可以在 model checking 期间将其大部分内容交换到磁盘中。此外,可以利用队列中连续的状态的共性进行压缩,例如在生成后继状态时可以仅存储其与出发状态之间的差异。
standardizing data structures :内存中的两个等效的数据结构可能有不同的表示形式。CMC 可以确定性地遍历指针数据结构,将其自动转换为相同的表示,然后再计算其所属状态的签名。
(?内存碎片?)例如,如果对象在堆中分配的顺序不同,则应将其视为等效相同。
在特定的程序中,状态间可能存在其它等价,例如用链表实现的无序集合。
CMC 使用如下方法高效地缩减状态空间,但是会导致漏报:
down-scaling :限制被测系统的规模,例如限制网络中的路由节点的数量。这可能更容易发现那些由少数进程之间的复杂交互导致地方错误,但是会遗漏那些仅在大规模系统中才会出现的错误。
state abstraction :消除用户认为对检查属性没有帮助的信息。在计算状态的哈希签名时忽略对应的内存位置即可。这可能会产生漏报,但不会产生误报。
heuristics :使用启发式策略来确定状态空间搜索的优先级。CMC 实现了一个专门的模块用于监视状态变量,记录 model checking 过程中状态信息的修改历史。如果状态的变化量突然增加,或者变量采用了较少出现的值,则认为该状态更有趣并更早地对其进行探索。
# OSDI'04 - FiSC
# Stateless Model Checking
# OSDI'08 - CHESS
CHESS 系统性地探索并发程序的线程交错空间,以较小的代价尽可能控制被测程序中的不确定性。
OSDI'08 - Finding and Reproducing Heisenbugs in Concurrent Programs
Taxonomy : in-situ / stateless model checking / concurrency testing / scheduling control
Tag : happens-before
要构建针对真实并发程序的系统性测试工具,需要解决如下挑战:
工具应该尽量避免修改被测系统或在测试期间干扰被测系统。
工具应当易于和现有的测试基础设施集成。
工具需要具备捕获、控制和探索被测系统的 interleaving non-determinism 的能力。
工具需要以优秀的策略探索被测系统的交错空间,因为穷竭搜索所有可能的交错是不可能的。
# CHESS 控制不确定性
并发程序的不确定性可以分为两类:
输入不确定性 (input nondeterminism) :包括由环境提供的、可以影响被测程序执行的值。例如对于用户程序来说包括所有系统调用的返回值和初始的内存状态。
交错不确定性 (interleaving nondeterminism) :包括线程交错和异步事件(例如抢占、callback 、计时器等)的调度。
对于输入不确定性,CHESS 认为精心设计的 log and replay mechanism 是不必要且负载过高的,并通过如下方式来确保控制输入不确定性:
利用已有类似工作中的 cleanup utilities 来重置内存、磁盘、网络等环境状态。
在运行时刻记录难以直接控制的输入,例如生成随机数、读取系统时钟、读取进程 ID 、系统调用的返回值等,以支持 deterministic replay 。
CHESS 主要关注交错不确定性,通过 CHESS scheduler 来控制被测程序的线程调度。具体地讲:
CHESS 重定向所有对 concurrency primitives 的调用到一组另外实现的 wrapper libraries ,这组库函数充分理解 concurrency primitives 的语义,并将其中的不确定性暴露给 CHESS 的 scheduler 。作者认为这种方式对被测程序正常执行流的影响足够小。
- 对于复杂的 primitives(例如复杂的 user-mode lock library),CHESS 可以选择将其视为被测程序的一部分而非 concurrency primitives ,这降低了实现的难度,但也失去了暴露所有不确定性的能力。
接下来依次回答两个问题:
CHESS 如何选取 scheduling point ,如何在 scheduling point 处获得控制权,以及如何确定每个 scheduling point 处的 enabled thread set ?
CHESS 如何系统性地探索不同的 schedule trace(即不同的 scheduling choice sequence)?
# Happens-Before Graph
Definition :
为简化 scheduler 的实现,CHESS 将并发程序的执行建模为 happens-before graph ,图上的每个节点上都被标记了一个三元组 (task, sync variable, operation) :
task 表示包括正在执行的线程(或其它可调度执行的实体,例如 async callback);
sync variable 指的是用于同步通信的共享资源(例如互斥锁、信号量、atomic access 等);
operation 是操作该 sync variable 的指令。
每个资源(即 sync variable)都对应一组可用的操作,其中一些操作可能具有复杂的语义,但 CHESS 只需理解每个操作的两位信息:
isWrite 表示该操作是否会改变被访问资源的状态。若节点 上 isWrite 为 true ,则对于图上所有与 具有相同 sync variable 的节点 ,连边 或 ,取决于 是在 的前面还是后面。
isRelease 表示该操作是否会解除那些正在等待资源的 task 的阻塞状态。CHESS 会为每个资源维护一个 waiting task set ,在执行 isRelease 为 true 的 operation 时将该集合中的 task 激活。
事实上只有 isWrite 是必须的,而 isRelease 主要是用于提高维护程序状态信息的效率。
要决定如何维护每个操作的 isWrite 和 isRelease 两位信息,CHESS 可能需要深度理解 API 的语义,但这种理解可以是不精确的;甚至,如果可以牺牲效率,任意将这两位信息设为 true 都不会影响正确性,这一性质保证了模型的 robustness 。
Construction :
CHESS 的 wrapper libraries 理解 concurrency primitives 的语义并据此构建 happens-before graph :
wrapper 必须知道每个 task 可能会在执行哪些 API 时被阻塞。观察发现,许多这样的函数实现遵循 try/else 的模式:首先尝试获取资源,如果未能成功则阻塞。
wrapper 必须为所有 concurrency primitive callsite 标记如前所述的三元组。
wrapper 必须告知 CHESS scheduler 每个 task 的创建和终止行为。
Capturing Data Races :
对于 race-free 的程序,happens-before graph 足以对被测程序的所有内存访问操作进行确定性排序,然而实际的并发程序中经常含有大量 intentional / benign data race ,这会从根本上影响 deterministic replay 的正常工作;为此,需要在 happens-before graph 中引入新的边来决定 race access 的顺序。
可以利用 dynamic race detection 工具来捕获并处理程序执行中遇到的所有 data race ,但这会引入过高的 overhead(一个数量级)。
CHESS 借鉴了 deterministic replay 的相关工作,通过 enforced single-threaded execution 来解决此问题。这种方法有两个显著的缺点,但都可以用其他方法弥补:
这会破坏程序的并行性,但这可以通过并行运行多个 CHESS 实例来弥补;
这会导致 CHESS 探索 race access 的不同执行结果的能力下降,因为 CHESS 不知道 race 是何时发生的;为此,CHESS 预先利用 dynamic race detection 工具运行被测程序若干次,标记发现的所有 race point ,然后在这些位置插桩 CHESS scheduling ,以此弥补损失的路径覆盖率。
# CHESS Scheduler
CHESS scheduler 的工作流程包括三个阶段,每个阶段都面临不同的技术挑战:
在 replay 阶段,CHESS scheduler 从 recorded trace file 中读取并重放一系列的 scheduling choices ,重放完成后进入 record 阶段。初次运行时 trace file 为空,意即直接进入 record 阶段。
在 record 阶段,CHESS scheduler 以 fair and non-preemptive 的方式工作,并记录在每个 scheduling point 的 enabled thread set 以及此处选择调度的线程。本次执行终止后进入 search 阶段。
在 search 阶段,CHESS scheduler 根据 record 阶段记录的信息来指导后续的 test run ,并根据某种策略选择探索不同 scheduling 的顺序。
replay phase :
deterministic replay 的相关工作表明,fully-deterministic replay 是 heavy-weight 且需要巨大的编程代价的;因此 CHESS 牺牲路径覆盖以换取快速且 robust 地处理无关 non-determinism 的能力。
replay 可能在以下两种情况下失败,即遭遇了无关的 non-determinism :
在某个 scheduling point 处选择调度的线程被发现是 disabled 的;这可能是由于某些共享资源变得不可用。
replay 时执行的 sync operation 序列与 trace 中记录的不同;这可能是由于上一轮 test run 之后程序状态的某些部分未被重置(?为什么),进而导致程序控制流的偏转。
对于这种无关的 non-determinism ,CHESS scheduler 的处理流程如下:
首先立即放弃 replay 并进入 record 阶段,以确保此次 test run 能顺利终止。
随后尝试再次重放该 trace ,期望这种偏差是罕见的、暂时的;
若仍然失败,则放弃该 trace ,回到 search 阶段继续探索其它调度。
为了减轻路径覆盖的损失,CHESS 对实践中常见的 non-determinism 进行了特殊处理:
lazy initialization :系统中经常存在一些数据结构,仅在程序首次访问时才执行初始化;如果其中存在 sync operation ,则后续的 test run 将无法触发这些操作。为此,CHESS 预先运行若干轮 test run 以期能触发这些 lazy initialization ,不过这仍然会造成路径覆盖的损失。
environment interference :
non-deterministic function calls :例如
random()
和gettimeofday()
等;对于前者,使用固定的 random seed ;对于后者,实践表明无需做特殊处理。
fair scheduling :
许多并发程序都天然地假设 OS scheduler 是 fair 的;因此,CHESS scheduler 也必须限制仅探索 fair scheduling 。
由于存在 spin loop 等情况,fair scheduling 的数量通常是无限的;CHESS scheduler 选择优先探索那些更可能在实践中出现的调度序列,具体策略详见 PLDI'08 - CHESS 。
# CHESS 减缓状态空间爆炸
作者在先前的工作 PLDI'07 - ICB 中发现限制 preemption 的次数是非常有效的;然而实践发现,在大型系统中仅仅限制 preemption 的次数对于减缓状态空间爆炸而言是不足的。为此,CHESS 将 preemption 的范围扩大到感兴趣的代码段,从而减小 (?)。
作者发现,相当多的 sync operation 发生在系统功能层(例如 C runtime)或是使用底层库实现,可以合理地假设这些代码是 thread-safe 的;因此 CHESS 不会在这些代码区域内插入 preemption ,牺牲路径覆盖以换取 scalability 。
作者发现,相当多的 synchronization 是对 volatile 变量的访问;已有工作 TACAS'03 - xxx 表明,如果对特定 volatile 变量的访问总是被其它 synchronization 限制执行顺序,则无需在这些程序点发起线程交错。
CHESS 以 stateless 的方式运行,不直接存储,而是使用 trace 来表示程序状态,在减少内存消耗的同时避免了一些冗余探索,并且能与 ICB 配合运行。
- race-free trace 的每次执行都会引向相同的程序状态,在 happens-before graph 上总是对应同一节点。
- 01
- Reading Papers - Kernel Concurrency06-01
- 02
- Linux Kernel - Source Code Overview05-01
- 03
- Linux Kernel - Per-CPU Storage05-01