ABSTRACT

In recent years, with the improving degree of automation of real-time embedded systems, their design complexity continues to increase. Concurrent programming methods were widely used in designing. But due to real-time embedded system interrupts and threads overlap, in the testing and checking process of real-time embedded system, there is always lack of an effective program testing tool. So we designed a testing tool for VXWORKS systems dynamic concurrent programs. We use Labeled Transition Systems as a system of concurrent programming model, and have given formal definition for common concurrency error, and use of partial order reduction algorithm to reduce the state space of the program. Finally, we have realized the testing tool which can detect multi-threaded and multi-interrupt program concurrent errors.

Keywords:Real-Time Embedded Systems, Concurrent Program, Multiple Interrupts, Multithread, Concurrency Errors

VXWORKS系统并发程序动态测试工具设计

梁  昊¹，艾云峰²，沈怀荣³，赵永超⁴

¹装备学院，研究生管理大队，北京

²中国科学院大学，工程管理与信息技术学院，北京

³装备学院，航天装备系，北京

⁴国防大学，作战与指挥训练教研部，北京

Email: mouse1292000@hotmail.com, 85283611@qq.com, shenhuair@tom.com, 314976196@qq.com

收稿日期：2014年4月15日；修回日期：2014年5月14日；录用日期：2014年5月22日

摘  要

近年来随着实时嵌入式系统自动化程度的不断提升，其设计复杂度不断加大，在设计中大量的使用了并发程序设计方法。但在实时嵌入式系统测试的过程中，由于实时嵌入式系统中中断和线程相互交叠，始终缺乏有效的并发程序测试工具。为此本文设计了针对VXWORKS系统并发程序动态测试工具，提出以标记迁移系统作为并发程序的系统模型，对常见的并发错误给出了形式化定义，使用偏序化简算法缩减程序的状态空间，实现了对多线程、多重中断的并发程序错误检测。

关键词

实时嵌入式系统，并发程序，多重中断，多线程，并发错误

1. 引言

近年来随着控制系统的自动化程度不断提升，对其数据处理能力、通信处理能力、系统集能力都提出的要求也越来越高。因此并发多线程、多重中断程序设计技术在嵌入式实时操作系统中得到了广泛的发展和应用。然而并发程序由于其执行过程中并发交叠的随机性，系统安全性带来了大量的不确定因素。一般情况下，一个由n个线程、每个线程有k个语句组成的多线程并发程序，多线程之间所有可能交叠总数为。同时，操作系统线程调度策略、程序执行环境，如I/O状态、处理器状态等，均会直接影响程序的执行序列，最终影响程序执行的结果，即使用同一输入数据执行同一并发程序多次，可能会得到多种不同的结果。

目前国内外针对并发程序的测试工具主要分为：静态分析工具、动态测试工具。

静态分析工具的设计思想是不编译运行程序，而对程序中多线程访问共享资源时的锁集合进行静态检查，如果与不同线程访问同一共享对象相关的两个锁集合的交集为空，则发出警告，提示可能出现数据竞争。如国防科技大学设计的MIDAC[1] 检测工具。MIDAC采用了函数摘要的技术来缩减静态分析过程中需要遍历的状态空间。文档[2] [3] 所采用的类线程测试方法为多重中断的测试提出了新的思路，其主要原理是将中断程序改写为“语义”等价的多线程程序，然后对多线程程序进行静态或者动态测试。

动态验证工具的基本设计思想是对在给定测试数据驱动下执行的程序进行验证，它避免了可执行程序代码(包括编译、运行时库等)与模型之间的不一致问题。其中典型的工具有：

VeriSoft[4] 面向可执行程序，能够验证由C、C++、Tcl等任何程序编写的可执行代码，它还支持对包含多个进程的并发程序的验证。VeriSoft采用了无状态的动态模型检验方法。

加州伯克利大学开发了可扩展的主动测试工具框架CalFuzzer[5] ，其可对Java程序的数据竞争、原子性违背、死锁进行测试；并可集成不同的动态分析工具，已集成动态分析工具有：Lockset、Atomizer和ATOMFUZZER、iGoodlock。已设计了用于数据竞争、原子性违背、死锁检测工具；亦可集成用户定制的线程调度策略。

2009年美国犹他州大学研发的动态验证框架原型Inspect[6] ，可发现多线程C程序中的“并行错误”，并保证在给定测试数据下没有数据竞争、原子性违背这两种并发错误。

航天二院706提出的多重中断程序测试框架[7] 亦是一种动态测试工具，它的主要设计思想是对中断进行两两对比测试，通过不断提高两个中断的触发频率来加速并发错误的出现。但是该方是只能针对两个中断进行独立测试，且需要人为干预，很难保证测试的覆盖率。

本在参考了国内外相关技术的基础上，设计了面向VXWORKS实时操作系统并发程序的动态测试工具，该工具可以测试包括多线程、多重中断在内的并发程序，错误检测范围涵盖了数据竞争、死锁、原子性违背这三种常见的并发错误。本文首先介绍了动态测试的总体构架；之后详细叙述了程序分析器、程序插装器、控制执行器、中断发生器这四个主要组成部分的详细设计方案；最后通过实验数据说明了该测试工具在功能完备的前提下拥有较好的时效性和可靠性。

2. 测试工具总体设计概述

2.1. 动态测试工具设计框架

多重中断程序动态测试工具构架主要包含4个部分：程序分析器、程序插装器、控制执行器、中断发生器。其总体设计构架如图1所示。

2.2. 动态测试工具执行流程

第一步对源程序使用程序分析器，得到并发程序的状态空间模型；第二步对分析后的程序使用程序插装器对程序中的共享对象、中断服务函数、线程函数进行标记、插装；第三步对插装后的程序进行编译，因此在编译的过程中，必须配合为本测试工具所设计的相应软硬件平台的C语言插装库文件，这样就可以到的可被控制执行的目标程序；最后将目标程序烧写入目标机，建立目标机和控制执行器的通信

图1. 并发程序动态测试工具设计框架图

链路，启动中断发生器，目标机就进入了实时动态执行阶段，控制执行器根据目标机反馈执行状态和动态测试算法实时地控制中断发生器产生特定的中断，直到所有的并发程序路径被搜索完毕后测试结束，控制执行报告可能存在的并发错误。

3. 动态测试工具详细设计方案

本小节将详细的介绍程序分析器、程序插装器、中断发生器、控制执行器的详细设计方案。

3.1. 程序分析器设计方案

程序分析器的主要作用是构建并发程序的系统模型。程序分析器采用了CIL(C Intermediate Language) [8] 开源工具对被测是程序进行分析，构型被测试程序的标记迁移系统模型。其主要工作可以分为：第一，对并发程序进行分析，标记出程序中的共享对象，得到的共享对象及相关操作，在程序中插入临时变量记录共享对象读写前后的取值，从而抽象出程序状态空间；第二，将程序中的复杂语句转换为：if、else、goto、while、赋值等5种简单语句，抽象出程序迁移空间。由此我们可以获得并发程序的标记迁移系统模型。

标记迁移系统(Labeled Transition Systems, LTS)[9] ，其模型的具体描述如下：

定义2.1 LTS(标记迁移系统)是一个四元组其中S表示并发程序的状态集合；表示初始状态(也可表示为)，并且有；表示所有迁移集合，并且有；表示迁移关系集合，并且有。

3.2. 程序插装器设计方案

程序插装器主要完成对共享对象相关操作的插装，对中断服务函数的插装。这里我们使用了CIL工具的API[8] ，针对共享对象、线程函数、中断服务函数进行了特殊处理。

共享对象插装主要是标记共享对象，识别对共享对象的相关操作(表1)。

对中断服务函数的插装主要作用是识别中断服务函数以及相关的中断源；确定中断的性质和中断优先级；对开关中断的函数进行识别，向控制执行发送开关中断的操作(表2)。

表1. 共享对象插装功能示意表

对线程的插装主要作用是识别线程，标记所有线程的相关操作并通知控制执行器(表3)。

3.3. 中断发生器设计方案

通过分析典型的被测程序，考虑测试工具的通用性，中断信号发生器的包含了大量的常用硬件接口，其硬件设计构架图如图2所示。

为了保证中断信号产生的实时性，中断信号发生器采用了HSSI高速串行接口与控制执行器进行通信，该接口比常规串行接口拥有更高的速率，比LAN接口拥有更短的延时时间。

3.4. 控制执行器设计方案

动态测试的过程中，函数空间注册、状态空间化简、并发错误检测这三个任务主要是由控制执行器

表3. 线程函数插装示意表

图2. 中断发生器硬件设计方案

完成的。

3.4.1. 函数空间注册

由于测试工具要处理包含普通函数、线程函数、中断服务函数的交叠路径，因此本文对被测试程序的函数空间做出了重新的映射。

本文使用来代表程序的函数空间，即为函数的唯一标识，函数空间包括：线程集合；中断服务函数集合；以及主线程main函数。

假设被测试程序包含个函数(1个main函数即主线程，个线程函数，个中断服务函数，)，。本文规定的优先级为，main函数的中断优先级为，的优先级为，这样所有中断的优先级都高于线程及函数的优先级，主线程的优先级高于其他线程的优先级。由此我可以进一步得到并发程序的扩展模型其中表示允许中断发生的标识，P表示函数的优先级。

3.4.2. 状态空间化简算法

本文在多线程程序动态偏序化简[10] -[12] (Dynamic Partial-Order Reduction，以下简称DPOR)算法的基础上，设计了可以处理多线程程序、多重中断程序的DPOR算法。DPOR算法的关键是剔除状态S上所有执行迁移中存在的独立关系。

定义3.1 对于一个全局状态，当且仅当其上的迁移t在全局状态上的一个局部状态上是可执行的，此时不属于的局部状态有，则迁移在全局状态上才是可执行的，记作。

定义3.2 是独立关系，当且仅当如果对于每一个，如果他们是相互独立的，则必须满足下面两个关系：

1) 若在状态是可执行的，且有，当且仅当在状态是可执行的，则在状态是可执行的。

2) 如果在状态是可执行的，则存在一个唯一的状态，有并且。

定义3.3 当且仅当状态上所有非空迁移序列，满足迁移， ，与集合中的所有迁移是相互独立的，则在状态上可执行的迁移集合是一个persistent集合。使用persistent集合的选择性搜索可以保证测试工具在动态测试过程中的完备性[11] 。

动态偏序化简的主要思想就是计算各个状态的Persistent集合。

图3的算法设计中，我们使用了递归的调用方式，采用基于深度优先的搜索方式来对程序的状态空间进行搜索。算法中使用集来表示动态执行过程中状态所处的当前函数，表示该迁移所在的函数表示。为全局对象的搜索堆栈，为每一个状态的可执行迁移集合，为回溯集合表示需要搜索的状态的中断集合。表示被检测过的状态的中断集合。

由于控制系统程序往往主线程中会包含无线循环以维持系统的不断工作。因此本文在算法中加入了一个hash表H用来记录检索过的状态，从而达到使控制执行器不反复循环检索已经检索过的状态。

本算法引入了可见操作依赖关系图的处理机制，可见关系依赖图记作为模型中的有向图，它包含了遍历状态空间中所有可见操作之间的发生前关系[10] 。对于中的每一个节点是一个可见操作，即。对于在动态搜索中执行的每一个迁移序列，算法都会在图中加入一个方向边，这样在除程序的第一次动态执行以外，之后的执行过程会首先搜索可见关系依赖图并执行回溯，进一步提高了状态空间搜索效率。

通过在图2中第8、14、15行中，加入对函数优先级的比较，如果函数的优先级高于函数

图3. DPOR算法描述

的优先级，则该路径不可行，也就不再求取状态上迁移的回溯点。

算法的18~30行为控制执行部分，与传统的DPOR算法不同的之处在于算法第25行包含了对函数性质以及中断允许标志位的判断，如果函数为线程函数则迁移可行；如果函数为中断服务函数则必须要在使能中断的情况下，迁移才可行。

函数UPDATEBACKTRACESETS(,)作用是动态计算回溯集合，与经典的DPOR算法相同，其具体描述如图4所示。

关于DPOR的算法的详细理论与数学证明请参考文献[10] 。

3.4.3. 并发错误检测算法

函数BUGDETECT的作用是在状态处检测是否存在原子性违背和数据竞争错误。算法的描述如图5所示。

如图5算法的第2、3行为对死锁算法的检测，算法的第4行至第16行是目标程序的原子性违背错误的检测方法，主要是检测多重中断程序中多变量读写时是否存在原子性违背错误；第15、16行主要是检测程序中不同优先级下，高优先级中断打断低优先级中断时，程序是否存在数据竞争的情况。

3.4.4. 控制执行机制

前文中我们已经介绍了针对多重中的DPOR偏序化简算法，如图3算法中第26行，此时控制执行

图4. UPDATEBACKTRACESETS算法描述

图5. 并发错误检测算法

器将控制目标机中的被测试程序执行的函数)，该函数可能是中断也可能是线程。

若，控制执行器阻塞除线程函数之外的所有的线程并关闭所有的内部中断，则线程函数可由VXWORKS系统调度为执行状态。

若，控制执行器通知中断发生器触发中断服务函数，并关闭所有的内部中断。

图6中所描述的共享变量读写流程图也就是表1中插装函数Instrument_obj_write (&X)以及Instrument_obj_read (&X)所完成的功能。

4. 实验平台和实验结果

4.1. 实验平台

实验平台的具体硬件配置见表4。

被测试程序方面，我们在ARM平台上选用了通讯加密编码程序，在PPC平台上选用了无人飞行器控制程序。为了通过实验验证控制系统并发程序错误检测算法的执行效率，我们对目标程序的线程、中断数量进行了修改。具体的实验结果如表5所示。

图6. 控制执行机制

表4. 测试软硬件平台

表5. 实验结果1

表6. 实验结果2

4.2. 实验结果

在以上的表格中，我们用“/”表示程序无法在48小时(172,800秒)内测试完成。从图中可以看出，在被测程序包含中断数、搜索迁移数、检测时间等三个比较指标上，在使用了偏序化简算法以后，执行时间大大缩短，提高了检测效率。

表6我们分别使用了类线程测试的方法[2] [3] 与我们的测试工具进行对比。由于中断服务函数和线程函数在执行方面存在着本质上的区别，因此在测试过程中类线程测试工具产生了误报的情况，另外由于verisoft采用了无状态的动态偏序化简算法，因此执行效率较低，而且本测试工具还有对中断服务函数和线程函数优先级的判断，可以进一步的缩减被测试程序并发模型的状态空间，所以在执行效率上有了进一步的提升。

5. 结束语

本文根据实时嵌入式系统中并发C语言程序的相关特点，使用LTS模型对并发程序进行建模，在DPOR算法的基础上，对中断服务函数进行了功能扩展，实现了对包含多线程、多重中断状态空间的化简。本文根据常见的三种并发错误的经典定义，给出了在标记迁移系统中的形式化描述和具体的检测算法，最终实现了对于包含多线程、多重中断的C语言并发错误检测。

参考文献 (References)