分类： 项目管理
2008-04-23 17:06:50
这个列表可能很长，但它是可以穷尽的。将上述列表稍微转化一下，我们就可以得到如图1 所示的一棵并发系统的“计算树（Computation Tree）”。这棵计算树显示了getObject()方法在两个线程并发的情况下，所有可能的执行路径。树中每一个矩形结点表示应用程序在执行过程中的一个特定状态，每一个箭头表示了由现有状态到新状态的一次转换，箭头旁边标注的记号则记录了引发此次状态转换的代码单元。即使对PoolMan 这样简单的代码，在只有两个线程的最简情况下，我们得到的计算树也如此庞大，以至于图1 不得不用虚线隐去了大部分的执行路径。但无论怎样，如果我们把PoolMan 看作一个有穷状态机，那么，这棵树所描绘的正是该状态机在两个线程并发时的状态图（Statechart）。
根据上述讨论，只要我们能把并发系统抽象成由代码单元组成的执行序列，使用测试程序自动地绘制出该系统的状态图就至少在理论上具备了可行性。一旦测试程序得到了并发系统的状态图，它就可以使用状态搜索算法，沿着状态图中的每一条路径，检查系统的状态是否符合并发系统的基本属性。对系统状态的检查包括许多种不同的方法。例如，测试程序可以根据系统状态的转换绘制出不同线程为特定对象加锁的操作关系图，然后在图中搜索循环的路径，在这里，循环的路径意味着循环的锁定关系，它必将导致死锁Bug。再比如，测试程序可以根据测试者的要求，在每个状态结点检查共享资源的一致性和完整性，以寻找系统中可能存在的竞态条件Bug。当测试程序发现系统在某一条执行路径上存在状态异常时，它就会自动记录并报告Bug，这和普通测试工具发现并报告Bug 的流程大体相仿。
模型检查方法并不是一件新鲜事物。在硬件研发领域，模型检查早就取得了不俗的成绩，包括CPU 电路设计在内的许多工作都需要依靠模型检查工具来完成最终的测试或检验。在通信协议开发方面，模型检查方法也大有用武之地，因为通信协议在本质上就是发送方和接受方之间的并发协作规范，其合理性完全可以利用模型检查工具来验证。在软件测试领域，现在也有许多实用的模型检查工具可供选择。这包括简单易用的Jlint（），NASA 的Java PathFinder
（），堪萨斯州立大学的Bandera（），卡内基·梅隆大学的SMV
（~modelcheck/smv.html）以及贝尔实验室的Spin（）等等。
百闻不如一见，下面，我们不妨用著名的模型检查工具Spin 对案例中的PoolMan 类进行一次自动化的测试。根据Spin 的要求，在测试前，我们需要用一种名为Promela（Promela 是过程元语言PROcess MEta Language 的缩写）的语言把待测系统的模型（即基本的数据和操作逻辑）表达出来。尽管Bandera 和Java PathFinder 等工具提供了由Java 代码或可执行程序自动生成Promela 模型的功能，但为了加深读者对Spin 的印象，这里仍然用Promela 语言给出PoolMan 类的抽象描述（Promela 的语法类似于C 语言，下面的代码也基本是从案例里的Java 代码转译而来的，并不难懂）：
#define SIZE 10 #define ID0 0 #define ID1 1 bool pool[SIZE]; /* 共享的对象池*/ int ret[2]; /* 用于断言检查的全局变量*/ proctype PoolMan(int id) /* PoolMan 线程*/ { int count; atomic /* 这相当于Java 语言中的synchronized */ { count = 0; do /* 寻找未用对象的循环*/ :: (count < SIZE) -> if :: (pool[count] == false) -> goto done; :: else -> count = count + 1 fi :: (count == SIZE) -> break od }
done: if ::(count < SIZE) -> pool[count] = true; /* 将获得的对象序号存入全局变量*/ ret[id] = count; /* 断言：两个线程获得的对象不能相同*/ assert(ret[ID0] != ret[ID1]) ; :: else -> skip fi } init /* 这里是程序运行的起点*/ { /* 初始化全局变量*/ ret[ID0] = SIZE; ret[ID1] = SIZE; /* 启动线程1 */ run PoolMan(ID0); /* 启动线程2 */ run PoolMan (ID1) }
在上面的Promela 代码中，我们使用断言（assert）来检查对象池的状态是否符合对象分配的基本规则。用Spin打开这段代码，执行Spin 提供的验证（Verification）功能，不一会儿，Spin 就会报出这样的错误信息：
pan: assertion violated (ret[0]!=ret[1]) (at depth18)
pan: wrote pan_in.trail
(Spin Version
Warning: Search not completed
+ Partial Order Reduction
上述信息表明，在系统状态图第18 层的某个位置，代码中的断言不能成立，两个线程所获得的是同一个对象。也就是说，Spin 自动找到了PoolMan 类中的竞态条件Bug。接下来，我们还可以使用Spin 提供的命令行工具或图形界面程序，显示系统状态图中的错误路径。例如，Spin 可以将出现竞态条件Bug 时，PoolMan 所经历的18 次状态转换显示为：
1: proc 0 (:init:) line 38 "pan_in" (state 1)
[ret[0] = 10]
2: proc 0 (:init:) line 38 "pan_in" (state 2)
[ret[1] = 10]
3: proc 0 (:init:) line 40 "pan_in" (state 3)
[(run PoolMan(0))]
4: proc 0 (:init:) line 42 "pan_in" (state 4)
[(run PoolMan(1))]
5: proc 2 (PoolMan) line 12 "pan_in" (state 1)
[count = 0]
6: proc 2 (PoolMan) line 14 "pan_in" (state 2)
[((count<10))]
7: proc 2 (PoolMan) line 16 "pan_in" (state 3)
[((pool[count]==0))]
8: proc 2 (PoolMan) line 26 "pan_in" (state 15)
[((count<10))]
9: proc 1 (PoolMan) line 12 "pan_in" (state 1)
[count = 0]
10: proc 1 (PoolMan) line 14 "pan_in" (state 2)
[((count<10))]
11: proc 1 (PoolMan) line 16 "pan_in" (state 3)
[((pool[count]==0))]
12: proc 1 (PoolMan) line 26 "pan_in" (state 15)
[((count<10))]
13: proc 2 (PoolMan) line 27 "pan_in" (state 16)
[pool[count] = 1]
14: proc 2 (PoolMan) line 29 "pan_in" (state 17)
[ret[id] = count]
15: proc 2 (PoolMan) line 31 "pan_in" (state 18)
[assert((ret[0]!=ret[1]))]
16: proc 2 terminates
17: proc 1 (PoolMan) line 27 "pan_in" (state 16)
[pool[count] = 1]
18: proc 1 (PoolMan) line 29 "pan_in" (state 17)
[ret[id] = count]
spin: line 31 "pan_in", Error: assertion violated
spin: text of failed assertion:
assert((ret[0]!=ret[1]))
#processes: 2
19: proc 1 (PoolMan) line 31 "pan_in" (state 18)
19: proc 0 (:init:) line 43 "pan_in" (state 5)
3 processes created
这样一来，在Spin 的帮助下，测试者不但可以寻找并发系统中可能存在的Bug，而且可以根据错误路径找出重现Bug 的方法，并发现Bug 在代码中的位置（有关Spin使用方法的详细说明请参考Spin 的联机文档）。
现在，我们已经大致了解了模型检查工具的操作过程。毋庸讳言，模型检查也有一些局限性，其中最重要的一点是模型检查面对“状态爆炸（State Explosion）”问题时的尴尬和无奈。我们已经知道，即使是像PoolMan 这样简单的系统模型，其状态图已经非常庞大了。对于任何真实的系统，在几十个线程并发的时候，系统状态图的结点数目肯定是一个天文数字。模型检查工具大都无法在有限的资源条件下穷尽真实系统的所有状态。因此，许多模型检查工具都提供了简化系统模型或简化状态图的算法和工具——但这样的操作需要测试者具备较多的理论知识和实践经验，实施起来并不那么容易。
在某些时候，动态的测试方法可以弥补静态方法的不足。动态方法的核心思想是，让编译后的并发系统在预先设定的环境和输入条件下执行，在执行过程中监测并发系统的状态转换和属性特征，并通过断言、日志等方式捕获Bug。常见的动态测试方法包括：根据对系统模型和状态图的分析，预先设计系统的输入条件，以使系统按预定的状态转换路径执行；在系统代码中插入同步点，根据测试者的要求控制系统的执行路径；使用随机的方式选择系统的执行路径，并在系统代码中插入断言等检测代码；等等。这些动态方法关心的是在特定情况下系统的运行过程，一般不需要在整个系统状态图中进行费时费力的穷举搜索。——顺便说一句，普通程序员最熟悉的，让系统在实际环境中试运行几天的测试方法也是一种最原始的动态测试，但这种测试缺乏理论的指导，是盲目和低效的。
人们已经设计出了许多专用于并发系统的动态测试工具。事实上，前面提到的，包括Spin 在内的不少静态测试工具为了提高测试效率，也已嵌入了若干动态测试功能。此外， 像贝尔实验室开发的Verisoft（），HP公司的VisualThreads（）等都是非常著名的动态测试工具。
如果我们对并发系统的状态转换关系有足够的了解，那么，自己动手开发简单的动态测试工具也不是什么难事。例如，如果在单CPU 计算机上运行案例中提到的PoolMan程序，因为每个线程的执行周期很短，线程之间较难发生执行序列上的交叉，我们通常无法看到错误的运行结果。但如果我们已经意识到，不同线程对pool 数组的并发访问可能会导致系统故障，那么，我们完全可以在getObject()方法中加入同步代码，以强制系统进入特殊的执行路径，激活可能存在的Bug。
我自己用Java 语言实现了一个非常简单的同步测试工具contest。contest 包括两个基本的Java 类：TestEvent类用于定义同步事件，TestManager 类用于管理同步测试过程。测试者首先通过TestManager 类的getInstance()方法获得TestManager 类惟一的对象实例，然后用addThread()方法向其中添加两个或多个待测线程（具体的线程代码需要测试者自己实现），接下来，测试者可以用addEvent()方法配置测试过程中的同步事件和每个同步事件的激活时间。随后，测试者在自己的线程代码中，使用TestManager 类提供的一组名为waitFor 的静态方法，强制线程在适当的位置等待某个特定的事件。
比如说，为了测试PoolMan 类的getObject()方法，我们可以在getObject()方法两次访问pool 数组的过程中加入一个同步点。改造后的getObject()方法如下所示：
public int getObject()
{
int i;
synchronized (this)
{
for (i = 0; i < pool.length; i++)
if (!pool[i])
break;
}
// 等待事件Event01
TestManager.waitFor("Event01");
// 打印输出每个线程获得的对象序号
System.out.println(
Thread.currentThread().
getName() + ": " + i);
if (i < pool.length)
{
pool[i] = true;
return i;
}
else
return -1;
}
也就是说，利用contest 提供的同步功能，我们让每个线程在执行完synchronized 结构后都先停一停，等事件“Event01”被激活后，再接着执行后续的代码。
现在，我们编译执行PoolMan 和contest 组合后的测试程序，正如我们所料，程序的输出结果为（假定我们运行两个测试线程）：
Thread1: 0
Thread2: 0
这表明，两个线程都获得了0 号对象，我们加入的同步代码让PoolMan 类在动态运行中暴露出了共享资源访问冲突的Bug。这是一次相当成功的动态测试（感兴趣的读者可以到
下载contest 工具，其中包含完整的源代码、说明文档和示例程序）。
本文的案例是一段Java 代码，用于动态测试的小工具contest 也是用Java 语言实现的。不过，这并不妨碍本文所讨论的话题在其他语言和平台上的适用性。大多数静态和动态的测试方法对C 语言、C++语言、Ada 语言等同样有效。根据contest 的源代码，读者也不难用C 语言或C++语言实现类似的功能。
l 并发系统的测试重点是与死锁和竞态条件相关的Bug。
l 并发系统的测试方法包括静态方法和动态方法两大类。
并发系统的测试过程大都可以实现自动化。如果图片无法显示请到： 《测试员》电子杂志下载区下载查看。
