高飞 武淑红 王耀力

摘  要： 并发模型分析主要用于业务流程逻辑验证，并不能很好支持多线程程序建模。目前大部分研究主要针对Java程序的死锁检测，对于使用POSIX线程库开发的C语言程序研究并不多。为了检测POSIX线程库开发的C语言程序是否存在死锁问题，提出一种对多线程程序进行自动建模与死锁检测的形式化验证方法。首先，根据C++CSP框架和源程序之间的联系，实现源程序到C++CSP框架的语义转换;然后，对C++CSP框架建立通信顺序进程（CSP）模型，并通过过程分析工具（PAT）对建立的模型进行死锁检测;最后，通过实例验证了本文中自动建模与死锁检测方法的可行性与有效性。

关键词： 多线程建模; 死锁检测; 语义转换; 形式化验证; 通信顺序进程; 过程分析

中图分类号： TN911.23?34; TP311.5             文献标识码： A                  文章编号： 1004?373X（2019）12?0057?05

Abstract： Concurrency model analysis is mainly used for logic verification of business process， but cannot support multithreaded program modeling well. Since most of current researches are mainly aiming at the deadlock detection of Java programs， researches on C language program developed with the POSIX thread library are still in small amount. Therefore， a formal verification method for automatic modeling and deadlock detection of multithreaded programs is proposed to detect whether there exists the deadlock phenomenon in the C language program developed with the POSIX thread library. The semantic transformation from the source program to the C++CSP framework is realized according to the relationship between the C++CSP framework and source program. The communication sequence process （CSP） model is established for the C++CSP framework. The deadlock detection for the established model is conducted by using the process analysis tool （PAT）. The feasibility and effectiveness of the automatic modeling and deadlock detection method proposed in this paper are verified by examples.

Keywords： multithreaded modeling; deadlock detection; semantic transformation; formal verification; communication sequence process; process analysis

0  引  言

随着多核和异构多处理器的广泛应用，计算机因有硬件的支持而能够在同一时间执行一个或多个线程，进而提升了整体处理性能。如今，多线程已经应用于各类复杂系统[1?2]，然而多线程也导致线程资源竞争或线程推进顺序不合适而产生死锁的问题[3]。Lu S等人针对MySQL，FireFox，Apache，OpenOffice这4款开源软件进行了统计，发现接近30%的并行程序缺陷与死锁有关[4]。死锁造成了系统的不稳定，对于安全性较高的行业，一旦软件系统發生死锁将会产生灾难性的后果。

国内外针对并发模型分析大多用于业务流程系统，对于多线程程序形式化验证研究较少。马莉等人针对物联网系统进行了形式化建模与验证[5];李凯宁等人基于模型驱动框架（MDA）实现了业务流程（BPMN）面向对象的建模，并对模型进行了死锁检测分析[6];中国科技大学的黄理提出了一种基于Petri网的多线程死锁检测方法[7]。

现有方法针对业务流程和多线程死锁形式化验证主要通过Petri网进行建模，由于Petri网适用于表示过程关系，并不能很好地对数据的流向进行描述，所以对于程序中的复杂过程并不适合。为了对源程序建立合适的模型，提高死锁检测精度，本文从肯特大学Neil BROWN和Peter WELCH等人开发的C++CSP框架受到启发[8?9]，使用C++CSP框架语言作为中介，提出一种多线程自动建模及死锁检测方法，实现了多线程程序的形式化验证。多线程程序到CSP建模和检测流程如图1所示。

图1  多线程程序建模和检测流程

1  多线程程序到C++CSP框架转换

C++CSP作为C++语言的一个多线程库，符合编程语言的逻辑与语义，可以实现源程序到C++CSP框架的等价语义转换。同时，该框架的通信方式是对CSP通道行为的模拟，为下一步C++CSP转换为CSP模型奠定了基础。因此，使用C++CSP作为中介可以精确地对源程序进行CSP建模。

下面将针对图2分析在POSIX多线程程序中，如何将通信结构转换为具有等效语义的消息传递结构。

1.1  共享内存通道转换

在C语言中，共享内存中数据的读/写通过赋值运算“=”，而在C++CSP中，则通过通道末端实现对共享内存的读写。C++CSP中存在两种通道类型：一个是允许正常写入数据的[chanout]通道;另一个是允许正常读取数据的[chanin]通道。共享变量通道在C++CSP中的声明如下：

1.2  互斥锁通道转换

对共享内存并发读/写时，互斥锁保证了非原子操作可以不受干扰的发生。使用POSIX线程库编写C语言程序中，通过对互斥量进行加锁和解锁的操作保证并发系统发生。多个线程可能拥有一个共同的互斥量，但只存在一个线程可对互斥量进行加锁操作，并且只有该线程进行互斥量解锁操作。多线程程序示例如下：

互斥量加锁和解锁过程如图2所示。在C++CSP中，互斥锁是通过互斥锁通道（[LockChannel]）进行模拟的，[LockChannel]由输入通道和输出通道两部分组成。声明互斥量时，需要对互斥量通道初始化，向[Chanin]通道输入一个互斥标记值表明当前为可加锁状态。当加锁时，从[Chanin]通道中读出标记值，互斥锁通道中没有标记完成加锁过程。同样，在解锁时向[Chanout]通道写入标记，使互斥锁通道中重新拥有标记值完成了解锁过程。互斥量加锁与解锁操作表示如下：

[Chanin mutex_in;Chanout mutex_out;mutex_out.read（lcl_mutex）;mutex_in.write（lcl_mutex）;]

图2  互斥量加锁和解锁过程

1.3  等待條件与信号量通道转换

POSIX线程库中提供了一种使线程等待来自其他线程信号的方法。当一个线程处于等待状态时，直到收到另一个线程发来的唤醒信号时，等待线程中才会被唤醒。该线程库中提供了[pthread_cond_wait（）]函数供用户使用等待操作，而在C++CSP中将该操作分为解开互斥锁、等待信号量、锁定互斥锁3个过程进行描述。信号量的产生与释放在C++CSP中通过[flush（）]和[fallinto（）]方法描述，描述方法如下：

[csp：：Bucket cond;cond.flush（）;cond.fallinto（）;]

在多线程程序中，[pthread_cond_wait（）]函数在C++CSP中描述如下：

[mutex_out.write（lcl_mutex）cond.fallinto（）mutex_in.read（lcl_mutex）]

1.4  线程逻辑主体到C++CSP的转换

[pthread_create（*thr，NULL，*start，*arg）]函数是POSIX线程库供用户进行线程创建的方法，该方法的第3个参数是创建线程主体的入口。由于在C++CSP中，线程之间使用通道方式进行通信，因此将线程主体中的逻辑关系转换为C++CSP，需要把线程主体中对共享内存的操作转换为通道通信形式。多线程程序中，[thr1]，[thr2]线程主体在C++CSP中，通过创建[run（）]方法实现对共享内存操作，对于每一个共享变量[X]，对应的局部变量[lcl_X]都会在[run（）]方法中创建，同时[run（）]方法还包含了线程中逻辑主体的行为过程，该方法在执行[delete  thr]方法后线程将被终止。

2  面向C++CSP框架的抽象建模

C++CSP框架线程之间通信是以CSP为理论基础进行开发的，所以C++CSP在通信行为上和CSP基本保持一致。而CSP作为一门可以有效描述并发结构和进程间交互的过程语言，CSP同样具有其语法规则和逻辑。下面将分析如何对由源程序转换而成的C++CSP框架语言进行抽象建模。

2.1  进程代数CSP

通信顺序进程（Communication Sequence Process，CSP）是描述并发系统中通信实体进行消息交换而设计的一种进程代数方法[10]。基于POSIX线程库开发的多线程程序是一种并发系统，本文采用CSP对多线程程序进行形式化建模与分析。

针对CSP中的符号约定，设大写字母[P]，[Q]，[R]表示进程，小写字母[x]，[y]表示事件。CSP中进程由事件和算子构成，它有顺序算子“->”和非确定选择算子“|”两种基本算子运算符。例如：进程[P]可表示为[x->Q]，表示事件[x]发生后流向进程[Q];进程的选择可表示为[（x->Q|x->R）]。此外，CSP中还定义了进程的复合操作，例如确定性选择进程（[P[]Q]）、或进程（[P?Q]）、并发进程（[P||Q]）、穿插进程（[P|||Q]）、顺序进程（[P;Q]）。