科研选题：基于 ptrace 实现的适用于分布式系统测试的操控执行框架

1.1 研究背景

分布式系统运行的过程中往往会出现大量不确定性的因素。在多个节点上运行的进程协同工作，会产生通信、调度上的偶然变化，构造分布式系统的时候往往无法穷举这些情况，程序的异常处理不完善导致系统潜在的崩溃可能。并且在错误发生之后，引发问题的执行路径通常难以还原，导致最终定位不到问题所在。

面对这一问题，通常的做法是模型检测。使用 TLA+ 等形式化验证工具对分布式算法进行建模。然而，面对真实而复杂的系统实现，强行使用形式化的方法进行建模则面临着困难的约简：约简过多，则与实际系统偏差越远；约简越少，则执行的分支越多，容易出现“状态爆炸”的问题。

为了解决上述问题，Mandanlal 等人提出了 CMC，一个用于直接对代码进行模型检测的执行框架。在工作中，他们对一个 ad-hoc 网络协议 AODV 的三种实现进行了模型检测。Junfeng Yang 等人提出了 eXplode 对文件系统进行穷举式的测试。后提出了一个在 Windows 上对实现级的分布式系统进行透明的模型检验的 MoDist 框架。类似的工作还有 MaceMC、CristalBall 等。

1.2 ptrace 简介

ptrace 是 Linux 内核提供的进程跟踪的系统调用，它允许父进程检查和替换子进程的内核镜像（包括寄存器）的值。

子进程调用 ptrace(PTRACE_TRACEME) 且父进程调用 ptrace(PTRACE_SEIZE) 后，父进程即可对子进程的执行进行控制：在子进程进行系统调用前或系统调用返回后停止；获取子进程系统调用信息；读写子进程内存和寄存器的值；模拟系统调用执行等。通过几种基本操作，能够实现程序的确定性执行。

2 系统设计

单线程程序从一个特定的状态出发，其状态转换分为两类。一是进行系统调用，对操作系统对象进行创建、删除、读写；二是系统调用以外的运算逻辑。对于第二类而言，其代表的状态转换是确定性的，即给定进程状态和代码，执行代码达到的目标状态是唯一确定的；对于第一类而言，则状态转换还要取决于操作系统对象的状态。比如同样执行 read() 系统调用，如果文件的内容正同时被其他进程改变，则产生的结果不确定。

在多线程程序以及分布式系统中，由于其由多个独立执行的程序组成，因而其执行路径还受到各执行流之间的调度的影响。

因此，为了对分布式系统进行模型检验，首先需要穷尽系统调用的可能结果；同时穷尽系统所有节点的各操作执行的先后顺序。

2.1 整体框架

对于 n 个节点的分布式系统，我们用 n + 1 个进程进行整个系统的操控执行：

  • 一个 tracer 进程，用以控制所有的进程
  • n 个 tracee 节点进程，即受控运行的分布式系统

以 3 个节点为例，对于一个运行中的分布式系统，其状态为 $S= <Env, Node1, Node2, Node3>$，其中：

$Node$N$ 代表节点的状态，包括节点的堆、栈、寄存器。

$Env$ 代表节点之外的环境，包括被节点使用的操作系统对象的状态，如网络消息，系统时间，打开的文件等。

在分布式系统执行的过程中，能够引发状态不确定性的分歧操作包括：消息的先后顺序，消息是否到达，以及消息等待是否超时。

tracer 进程每次从一个状态 $S$ 开始控制其中一个节点，运行到下一个分歧操作前，即：消息发送前，消息接受前，以及请求系统时间之前。之后对于每一个节点，都由 Choose() 函数根据运行时的上下文决定下一个分歧操作可能的状态转换集合$Transfer$，且对于每一种可能性 $t \in Transfer$，生成如下的“转换边”： $(Node$N.t(), <Env, Node1, Node2, Node3)>)$

它表示，状态的下一次转换从状态四元组出发，通过 $Node$N$ 执行 $p()$ 所代表的转换可达到下一个状态：

$(Node$1.p(), <Env, Node1, Node2, Node3)>)\rightarrow <Env’, Node1’, Node2, Node3)>$

$(Node$2.p(), <Env, Node1, Node2, Node3)>)\rightarrow <Env’’, Node1, Node2’, Node3)>$

$(Node$3.p(), <Env, Node1, Node2, Node3)>)\rightarrow <Env’’’, Node1, Node2, Node3’)>$

总的工作流程是：设置一个状态转换边的队列；每一次从中取出一条边并执行达到新的状态，在新的状态的基础上，生成新的转换边并入队。

对于 DMCK 的实现有两种，一种是 stateful，即通过保存和恢复节点的内存、寄存器等信息来重现状态；一种是 stateless，通过重放记录的执行路径来重现状态。我们的工作主要是 stateful 的。

1
2
3
4
5
6
7
8
9
10
11
12
13
14
S = <Env, Node1, Node2, Node3>

q.add(Edge(skip, S))
while (!q.empty()) {
    edge = q.deque()
    S' = edge.transfer()
    forall (node in Nodes) {
        // 只根据 node 的状态就可以算出当前执行上下文了
    	Transfers = Choose(node)    
    	forall (t in Transfers) {
    		q.add(Edge(t, S'))
    	}
    }
}
1
2
3
4
5
6
7
def transfer(edge) {
	S = edge.getState()
	t = edge.getTransfer()
	node = t.getNode()
	nodeState = S.getNodeState(node)
	nodeState.t()
}

2.2 相关工作

CMC 是一个 stateful 的模型检测工具，能够对 C 代码直接进行模型检测，被用于检测网络协议和文件系统（FiSC）。但是 CMC 的检测需要侵入式地修改源程序代码，以使得被测程序运行在 CMC 的地址空间内。

MaceMC 使用深度优先搜索和随机行走来检测网络协议实现中的 liveness 问题，但是被测系统需要是 Mace 生成的 C/C++ 实现。Yabandeh 等人基于 MaceMC 提出的 CrystalBall 增加了 Steering Execution，在运行的过程中分析未来的错误状态，并通过控制执行来避免。

Yang 等人提出的 MoDist 是一个适用于 Windows 上的分布式系统的模型检测框架。它与 MaceMC 一样是 stateless 的。

2.3 目标场景（与相关工作不一样的）

  • 支持对 go 语言编写的程序进行检测
  • stateful，不用每次都从头开始控制获得最新状态（节省运算性能，可能更占用空间）
  • 无侵入性（不用修改实现的源码）

3 被测案例

3.1 计数器

被测的程序是 3 个独立的递增计数器，由 tracer 同时控制其运行，能够生成并执行 3 个进程的全部可能的调度顺序。

3.2 client/server

客户端定时向服务端发送心跳消息，服务端每次收到心跳消息就刷新计时器，若超时则打印一条超时信息。tracer 通过调度顺序以及虚拟时钟模拟延迟，通过截获网络的调用模拟丢包，进行错误注入。

3.3 共识

3.3.1 编程作业

3.3.2 开源案例(待测)

github.com/willemt/raft 是一个 C 实现的 Raft 共识协议。其优势在于单线程，且本身没有指定通信方式。数据发送与接收的接口在 raft 运行实例启动时由使用者通过注册回调函数自定义，因而可以自由选取节点间的通信协议。

TODO: 另选取一个 go 语言的实现。

4 实现方法