基于Petri网展开的多线程程序数据竞争检测与重演.pdf

基于 Petri 网展开的多线程程序数据竞争检测与重演*鲁法明1,黄莹1,2,曾庆田1,包云霞1,唐梦凡11(山东科技大学计算机科学与工程学院,山东青岛266590)2(中国科学院深圳先进技术研究院,广东深圳518055)通信作者:黄莹,E-mail:;包云霞,E-mail:摘要:数据竞争是多线程程序的常见漏洞之一,传统的数据竞争分析方法在查全率和准确率方面难以两全,而且所生成检测报告难以定位漏洞的根源.鉴于 Petri 网在并发系统建模和分析方面具有行为描述精确、分析工具丰富的优点,提出一种基于 Petri 网展开的新型数据竞争检测方法.首先,对程序的某一运行轨迹进行分析和挖掘,构建程序的一个 Petri 网模型,它由单一轨迹挖掘得到,却可隐含程序的多个不同运行轨迹,由此可在保证效率的同时降低传统动态分析方法的漏报率;其次,提出基于 Petri 网展开的潜在数据竞争检测方法,相比静态分析方法在有效性上有较大提升,而且能明确给出数据竞争的产生路径;最后,对上一阶段检测到的潜在数据竞争,给出基于CalFuzzer 平台的潜在死锁重演调度方法,可剔除误报,保证数据竞争检测结果的真实性.开发相应的原型系统,结合公开的程序实例验证了所提方法的有效性.关键词:数据竞争;Petri 网;网展开;动态程序分析中图法分类号:TP311中文引用格式:鲁法明,黄莹,曾庆田,包云霞,唐梦凡.基于Petri网展开的多线程程序数据竞争检测与重演.软件学报,2023,34(8):37263744.http:/ Race Detection and Replay of Multi-threaded Programs Based on Petri Net UnfoldingLUFa-Ming1,HUANGYing1,2,ZENGQing-Tian1,BAOYun-Xia1,TANGMeng-Fan11(CollegeofComputerScienceandEngineering,ShandongUniversityofScienceandTechnology,Qingdao266590,China)2(ShenzhenInstitutesofAdvancedTechnology,ChineseAcademyofSciences,Shenzhen518055,China)Abstract:Data races are common defects in multi-threaded programs.Traditional data race analysis methods fail to achieve both recallandprecision,andtheirdetectionreportscannotlocatetherootcauseofdefects.DuetotheadvantagesofPetrinetsintermsofaccuratebehavior description and rich analysis tools in the modeling and analysis of concurrent systems,this study proposes a new data racedetectionmethodbasedonPetrinetunfoldingtechnology.First,aPetrinetmodeloftheprogramisestablishedbyanalyzingandminingaprogramrunningtrace.Themodelimpliesdifferenttracesoftheprogrameventhoughitisminedfromasingletrace,whichcanreducethe false negative rate of traditional dynamic analysis methods while ensuring performance.After that,a Petri net unfolding-baseddetection method of program potential data races is proposed,which improves the efficiency significantly compared with static analysismethodsandcanclearlyshowthetriggeringpathofdataracedefects.Finally,forthepotentialdataracedetectedinthepreviousstage,ascheduling schema is designed to replay the defect based on the CalFuzzer platform,which can eliminate false positives and ensure theauthenticity of detection results.In addition,the corresponding prototype system is developed,and the effectiveness of the proposed*基金项目:国家自然科学基金(61602279);山东省泰山学者工程专项基金(ts20190936);山东省高等学校青创科技支持计划(2019KJN024);山东省博士后创新专项基金(201603056);国家海洋局海洋遥测工程技术研究中心开放基金(2018002);山东科技大学教学名师培育计划(MS20211102)本文由“形式化方法与应用”专题特约编辑陈立前副教授、孙猛教授推荐.收稿时间:2021-09-05;修改时间:2021-10-14;采用时间:2022-01-10;jos 在线出版时间:2022-01-28CNKI 网络首发时间:2023-02-23软件学报ISSN1000-9825,CODENRUXUEWE-mail:Journal of Software,2023,34(8):37263744doi:10.13328/ki.jos.006618http:/中国科学院软件研究所版权所有.Tel:[phone]methodisverifiedbyopenprograminstances.Key words:datarace;Petrinet;netunfolding;dynamicprogramanalysis大数据时代,随着对计算性能要求的不断提高,云计算和多线程程序等并行计算技术越来越受到人们的重视1,2.在多线程程序中,由于线程调度的时序不确定性以及共享内存空间访问控制的复杂性,如果设计不当,程序会存在诸多并发缺陷,进而导致运算结果出错甚至程序崩溃3.这些并发缺陷的检测和排除是多线程程序设计的一大挑战,而数据竞争4就是引起广泛关注的并发缺陷之一.数据竞争是指对同一块内存空间存在并发访问,并且至少有一个访问是写操作.数据竞争通常会对程序的正确性产生恶劣影响.但是,数据竞争的产生场景往往难以检测,不仅需要特定的输入,还需要特定的线程调度顺序,这造成了数据竞争检测的困难.当前,数据竞争检测方法一般分为静态检测、动态检测和动静结合的数据竞争检测方法 3 类5.静态检测方法针对程序源代码进行分析,主要结合锁集对潜在的数据竞争缺陷进行检测,常见的静态检测工具包括 RacerX6、RELAY7和 locksmith8等.该类方法通过静态代码分析程序的完整行为,存在查全率高的优点.不过,由于静态分析方法不实际执行程序,它以源代码为输入直接进行程序分析,难以准确获取程序的运行时信息,从而导致了较高的误报率.此外,对程序全部行为进行分析使得静态分析方法时间效率偏低.动态检测方法监视程序执行过程中的行为,收集必要的信息来判断哪些操作构成数据竞争.常见的动态数据竞争检测算法分为基于 lockset的算法911,基于 happens-before关系的算法1217,以及两者混合的 hybrid算法1820这 3 种.基于 lockset 的方法维护程序执行过程中每个线程的当前持有锁信息,同时更新共享变量持有的锁信息,当共享变量不再受到锁保护的时候,报告数据竞争;基于 happens-before关系的方法借助逻辑时钟识别两个操作之间因为同属于一个线程、因为锁的释放和申请,以及因为线程的 fork 或 join 而导致的因果关系,将不具备上述因果关系的两个操作识别为并发.如果同一个共享变量的读写/写写操作之间是并发的,则认定两者构成数据竞争;hybrid 算法通常先基于 lockset 找到可疑的数据竞争,然后借助逻辑时钟等方法对可疑竞争的真实性进行验证.受限于线程执行交错的不确定性以及所收集信息的不完整性,动态竞争方法会有较多的漏检,但是数据竞争的动态分析方法一般比静态方法有更高的准确度.动静结合的数据竞争检测方法通常先通过静态方法检测潜在的数据竞争,然后,在程序动态执行过程中对线程的调度进行干预,以此增加数据竞争发生的概率,重演成功的数据竞争均为真实的并发缺陷.例如,文献 21 从一个已有的动态分析技术中获得的潜在数据竞争的相关信息,并据此控制线程的随机调度程序,以提高真实数据竞争发生条件的出现概率,以此提高数据竞争重演成功的概率;文献 22 首先使用静态分析方法识别潜在的并发错误,然后使用静态程序切片来针对潜在的并发错误获取较小的程序,最后,动态控制线程的调度以便多个线程同时访问同一内存位置,以此验证并发错误是否会导致程序失败.文献 23 以有害数据竞争的检测为目标,首先综合考虑 happens-before 关系与 ad-hoc 类型的同步来精简需验证的数据竞争数量,然后,将相互之间不存在干扰的潜在数据竞争划分到同一组中,再借助线程调度器以组为单位对潜在数据竞争进行重演.动静结合的数据竞争检测方法综合两种方法的优点,在数据竞争的查全率、准确度方面均有一定保证,不过,前期静态分析仍然耗时,后期动态重演通常是一些随机性的调度方法,重演成功率有待进一步提高.综上所述,目前的数据竞争检测方法在查全率、准确率方面难以两全,而且数据竞争检测的效率也有待提高.此外,如文献 5 所述,现有方法所产生的数据竞争报告使得开发者难以理解并据此追溯漏洞产生根源.针对上述问题,考虑到 Petri 网在并发系统建模和行为分析方面的优点,本文拟提出一种基于 Petri 网展开2430的新型数据竞争检测方法.首先,与动态检测方法类似,所提方法也是从多线程程序某次具体的运行轨迹出发进行分析,不过,从该轨迹出发,本文能构造出一个蕴含多种运行轨迹的程序 Petri 网模型,从该模型出发进行数据竞争检测能降低传统动态分析方法的漏报率,提高查全率;然后,与静态分析方法类似,通过对前述程序 Petri 网模型的分析检测潜在的数据竞争缺陷,本文将数据竞争检测问题转化为 Petri 网展开30中共享变量访问操作的并发关系识别,可有效提高数据竞争的检测效率;与此同时,潜在数据竞争对应的出现网片段可以很好地展示数据竞争产生的根源和具体路径;最后,由于程序运行轨迹中捕获的程序行为信息不够完备,由此挖掘到的 Petri 网模型可能与源程序在行鲁法明等:基于 Petri 网展开的多线程程序数据竞争检测与重演3727为上不一致,从而导致数据竞争误报的现象,为解决此问题,本文给出一种数据竞争重演方法,重演成功的数据竞争可保证真实性,从而可提高检测准确率.就性能而言,本文从单一运行轨迹出发构造仅包含程序部分行为的Petri 网模型,相比静态分析方法构造反映程序全部行为的模型而言,所提方法简化了模型构建和分析的复杂度,在一定程度上可提升数据竞争检测方法的效率.1 实例与动机分析与经典的数据竞争动态分析方法类似,本文假设程序由有限个线程构成,这些线程通过共享对象的加锁/解锁以及读写进行同步和交互.在程序的一次运行过程中,将线程的启动/终止/阻塞、锁的获取和释放,以及共享对象读写等操作所构成的操作序列称为一条多线程程序运行轨迹,其形式化定义如下.定义 1.多线程程序运行轨迹.多线程程序的运行轨迹,记作,是满足如下条件的一个操作序列:Trace:=OperationOperation:=c:fork(u,v)|c:join(u,v)|c:stop(u)|c:acq(u,l)|c:rel(u,l)|c:rd(u,x)|c:wr(u,x)其中,u,v 表示线程,l 表示锁,x 表示一个共享变量,c 表示程序语句的标签(例如行号、列号等);fork(u,v)表示线程 u 启动线程 v;join(u,v)表示线程 u 阻塞直到线程 v 终止;stop(u)表示线程 u 停止;acq(u,l)表示线程 u 获取锁 l;rel(u,l)表示线程 u 释放锁 l;rd(u,x)表示线程 u 读共享变量 x;wr(u,x)表示线程 u 写共享变量 x.以图 1 中的 Java 多线程程序为例,它包括主线程、threadA 和 threadB 这 3 个线程、两个共享变量 x 与 flag、一个锁对象 lock.主线程首先为共享变量 flag 指派一个随机值,然后依次启动线程 threadA 和 theadB;待两个线程都结束后,主线程终止.线程 threadA 启动后,首先将共享变量 x 的值设置为 1,然后尝试获取锁对象 lock;获取lock 成功后将共享变量 flag 的值设置为 true.线程 threadB 启动后,首先尝试获取锁对象 lock,获取成功后读取共享变量 flag 并将其值赋予私有变量 new_flag;若 new_flag 之后的取值为 true 则将 x 的取值设置为 2.程序 Program1 存在两处关于共享变量 x 的数据竞争.具体而言,若线程 threadB 首先获得 lock 的使用权,当主线程为 flag 指派的初值为 true 时,第 22 行 threadB 对 x 的写操作与 threadA 对 x 的写操作构成数据竞争;当主线程为 flag 指派的初值为 false 时,第 24 行 threadB 对 x 的写操作与 threadA 对 x 的写操作构成数据竞争.然而,程序 Program1 也存在一些运行轨迹不会呈现上述并发缺陷,例如表 1 中的操作序列.当中,线程threadA 首先获得锁对象 lock 的使用权,并将共享变量 flag 的值设为 true;然后,线程 threadB 获得 lock 使用权,并将共享变量 x 的取值最终设置为 2.若程序按照表 1 中的轨迹执行,则前述数据竞争不会触发.对于图 1 中的 Program1,首先,基于 lockset 的数据竞争检测方法19不适用,因为该方法要求所有的共享变量在执行读写操作时都必须通过锁来保护,而 Program1 对共享变量 x 的访问操作均未加锁保护;其次,基于happens-before 关系的数据竞争检测方法,若以表 1 中的运行轨迹为输入进行检测,也无法检测到实际存在的竞争.以得到广泛认可的 VerifiedFT17数据竞争检测算法为例,基于 happens-before 关系的数据竞争方法认为运行轨迹中一个锁释放操作与其后首次执行的该锁的申请操作间存在必然的因果关系.例如,表 1 的执行轨迹中,由于线程 threadA 释放锁对象 lock 的操作后,threadB 首次申请 lock,故 VerifiedFT 等基于 happens-before 关系的方法会假设在锁对象 lock 的使用权上,线程 threadA 一定先于 threadB,从而在两个操作之间加上一个错误的时序约束关系.而原本的程序行为并不存在这一约束,线程 threadB 完全可以先获得 lock 的使用权,然后对变量 x 进行写操作,进而导致与 threadA 写 x 时的数据竞争.由此可见,传统的 happens-before 关系对程序行为人3728软件学报2023 年第 34 卷第 8 期为添加了更多的约束,从而导致数据竞争的漏报.lockset 与 happens-before 两者混合的 hybrid算法同时存在上述两个问题.123456789101112131415161718192021222324252627282930313233public class DataRaceTest static booleanpublic static void main(String args)throws InterruptedException Thread threadA=new Thread()public void run();Thread threadB=new Thread()public void run()booleanelse;threadA.start();threadB.start();threadA.join();threadB.join();static int x=0;flag=true;static final Object lock=new Object();x=1;synchronized(lock)flag=(new Random().flag=truenew_flag=false;synchronized(lock)new_flag=flag;if(new_flag)x=2;x=3;System.out.println(The value of x is+x);nextBoolean();图1多线程程序实例Program1表1程序 Program1 的一个可能的操作执行序列序号主线程mainThread线程threadA线程threadB16:wr(mainThread,flag)227:fork(mainThread,threadA)328:fork(mainThread,threadB)49:wr(threadA,x)510:acq(threadA,lock)611:wr(threadA,flag)712:rel(threadA,lock)818:acq(threadB,lock)919:rd(threadB,flag)1020:rel(threadB,lock)1122:wr(threadB,x)1229:join(mainThread,threadA)1330:join(mainThread,threadB)1431:rd(mainThread,x)1532:stop(mainThread)为解决上述问题,本文不对共享变量的访问做锁保护的限定,并从给定的程序运行轨迹出发挖掘能尽量准确反映程序行为的 Petri 网模型.所挖掘模型中,仅在如下情况下建立操作语句之间的因果关系:(1)同一线程内相继执行的两个操作语句;(2)线程的启动操作 fork 与被启动线程的第 1 个操作语句;(3)线程的 join 操作与等待线程鲁法明等:基于 Petri 网展开的多线程程序数据竞争检测与重演3729的最后一个语句.此外,对于锁对象竞争导致的运行轨迹多样化的问题,本文通过 Petri 网中的冲突结构来刻画这种行为的多样性.如此一来,前述动态分析方法中错误添加的因果关系便可以消除,而且,所挖掘模型中蕴含了多种潜在的程序运行轨迹,这为本文方法更准确地、检测出更多的潜在数据竞争缺陷提供了可能.此外,由于定义 1 中的程序运行轨迹捕获的程序行为有限,由此导致由其挖掘得到的 Petri 网模型对程序行为的刻画并不完全准确,而且 Petri 网的运行原理与并发程序的执行语义不完全一致,这导致网模型可能蕴含一些虚假的可执行操作序列,进而导致数据竞争的误报.针对这一问题,本文将给出潜在数据竞争的重演方法,以此保证本文方法所检测数据竞争的真实性.最后,需要指出的是,由于动态分析以程序的运行轨迹为漏洞检测依据,而线程执行交错的不确定性和程序控制逻辑与数据流交互的复杂性使得程序各类不同的运行轨迹难以完整捕获,丢失的运行轨迹可能会导致数据竞争动态检测的漏报.以图 1 中的程序为例,若仅以表 1 中的运行轨迹为检测依据,包括本文方法在内的动态分析方法无法检测到第 9 行对 x 的写语句与第 24 行对 x 的写语句间存在的数据竞争,因为该轨迹中第 24 行语句对应的操作并未出现.解决这一问题的关键在于生成尽量多的测试用例以尽可能地覆盖程序执行路径,文献 31 提出了一种用于多线程程序数据竞争检测的测试用例自动生成技术,其生成的测试用例覆盖率经评估可达 94%,虽然能覆盖大多数程序执行路径,但丢失的路径信息都可能导致数据竞争的漏报.2 基于运行轨迹的多线程程序 Petri 网模型挖掘Petri 网24,25是一种广泛应用于并发系统建模和分析的工具,其相关定义如下.=(P,T;F,M0)P=p1,p2,.,pnT=t1,t2,.,tmPT=PT,F (PT)(T P)M0:P 0,1,2,.定义 2.Petri 网.Petri 网是一个四元组,其中,为库所集,为变迁集,并且,称为网的流关系,为的初始标识.x PTx y PT|(y,x)Fx y PT|(x,y)FMt M定义 3.变迁使能与执行规则.对,称为 x 的前集,为 x 的后集.在标识 M 下,若变迁 t 的每个前驱中都含有至少一个标记,则称 t 是使能的.使能的变迁可以执行从而引发系统状态标识发生改变.T 执行后的标识 M满足如下条件,并记之为.M(p)=M(p)1,ifp ttM(p)+1,ifp ttM(p),otherwise.TM01 M12 M23.Mk1k MR()对,若,则称为一个可引发变迁序列,并称 M 为系统的一个可达标识,的所有可达标识的集合记为.进行系统建模时,Petri 网的库所通常表示某种状态或者资源,变迁通常表示某种动作,流关系通常用以刻画动作执行的前提条件和导致的后继状态,标识用于建模网系统的状态.本文使用 Petri 网对多线程程序的行为进行建模时,每个变迁对应程序执行过程中的一个操作;库所分为两类,控制库所用于建模线程的控制流状态,资源库所用于建模程序中的锁对象;Petri 网中的标识表示程序的运行状态.程序运行之初,仅有主线程的初始控制流库所和各个锁对象对应的资源库所含有一个标记,其余库所标记数为 0.M0(p0)=1 M0(plock)=1 p Pp0,plock:M0(p)=0图 2 就是根据表 1 的程序运行轨迹挖掘到的一个能反映图 1 程序部分行为的 Petri 网模型(具体挖掘方法稍后给出).模型中,每个变迁(用小矩形表示)对应一个程序操作,变迁同时标注了其变迁 ID 和对应的程序操作;黑色边线的库所(用圆表示)为某个线程的控制库所,建模控制流状态;红色边线的库所为一个资源库所,建模一个锁对象.控制流库所中的 token(用黑点表示)表示线程的当前控制流状态处于激活态,资源库所中的 token 表示当前锁对象处于可用状态.初始状态下主线程的就绪态被激活,各个锁对象可用,故它们对应的库所各自有一个 token,相应地,图 2 中的系统初始标识满足,当中 p0是一个控制流库所,对应主线程的就绪状态;plock是一个资源库所,对应程序中的锁对象 lock.就程序 Petri 网模型的挖掘方法而言,当给定多线程程序的某个运行轨迹后,可以按照表 2 所示的网模型构建规则构造程序本次运行对应的 Petri 网模型.具体而言,首先为主线程的就绪状态和各个锁对象分别构建一个含有 token 的库所;然后,针对运行轨迹中各个操作的种类,按照表 2 中给出的规则添加相应的变迁及其输入、输出库所和流关系即可.具体地说,每个共享变3730软件学报2023 年第 34 卷第 8 期量的读/写操作所对应变迁仅有唯一的前驱库所和唯一的后继库所,分别对应该操作所属线程的两个控制流状态;每个线程 fork 操作所对应变迁有一个输入库所对应该操作所在线程的上一个控制流状态,两个输出库所分别对应该操作所在线程的下一个控制流状态,以及被启动线程的就绪状态;每个线程 join 操作所对应变迁有两个输入库所分别对应该操作所在线程的上一个控制流状态,以及被 join 线程的结束状态,有唯一的输出库所对应该操作所在线程的下一个控制流状态;对于锁对象的获取操作而言,它对应的变迁有两个输入库所,其一对应该操作的前驱控制流状态,另一个对应申请访问的锁对象;对于锁对象的释放操作而言,它对应变迁有两个输出库所,其一对应该操作的后继控制流状态,另一个对应释放的锁对象.此外,为直观起见,表 2 为每个共享变量的读写操作额外添加了共享对量对应的一个红色圆圈,需要指出,该元素并不属于 Petri 网的库所,仅起到对共享变量读写的提示作用,进行 Petri 网行为分析时完全可以忽略这些变量标记.图 2 中的 Petri 网就省略了这些变量标记.p0BtB0pB1tB1pB2tB2pB3tB3pB4pA4pA3pA2pA1pA0tA0tA1tA2tA3t0t1t2t4t3t5t6p1p0p2p3p4p5p6p7plock主线程准备就绪wr(mainThread,flag)fork(mainThread,threadA)wr(threadA,x)acq(threadA,lock)fork(mainThread,threadB)threadB准备就绪acq(threadB,lock)rd(threadB,flag)rel(threadB,lock)wr(threadB,x)wr(threadA,flag)join(mainThread,threadA)join(mainThread,threadB)rd(mainThread,x)stop(mainThread)threadA准备就绪rel(threadA,lock)图2由表 1 运行轨迹挖掘得到的程序 Petri 网模型以表 1 中程序 Program1 的运行轨迹为例,结合前述 Petri 网模型挖掘方法和表 2 中的 Petri 网模型构造规则,可得图 2 所示的 Petri 网模型.初始标识下,该模型仅有变迁 t0可以执行,它对应源程序中主线程的首条可执行语句,即对共享变量 flag 的写操作;t0执行完毕后,状态库所 p1被输入一个 token,代表主线程的下一个控制流状态被激活;在这一新的状态下,变迁 t1使能,代表启动线程 threadA 的操作可以执行;t1的执行将同时向库所 p2和pA0各输入一个 token 以激活他们,前者对应主线程该操作执行后的后继状态,后者对应线程 threadA 的就绪状态,鲁法明等:基于 Petri 网展开的多线程程序数据竞争检测与重演3731=t0t1t2tA0tA1tA2tA3tB0tB1tB2tB3t3t4t5t6之后的操作依次类推.实际上,表 1 中的程序运行轨迹对应着图 2Petri 网的可执行变迁序列,该变迁序列执行完毕后,主线程的终止状态库所和锁对象 lock 对应的库所各自含有一个 token,这对应着程序 Program1 的终止状态.表2程序锁对象、初始状态以及操作所对应的 Petri 网模型程序对象及其操作对应的Petri网模型片段说明主线程就绪状态p0该库所表示主线程的就绪状态,初始标识下它包含一个token,表示初始状态下主线程处于就绪状态锁对象pi锁 i该库所对应一个锁对象,初始标识它包含一个token,表示初始状态下锁对象处于可用状态fork(u,v)p1t1p2fork(u,v)pv0变迁t1对应fork操作,其前驱库所p1表示线程u中fork操作的前驱控制流状态,后继库所p2表示线程u中fork操作的后继控制流状态,后继库所pv0表示线程v的就绪状态join(u,v)p1t1p2pv1join(u,v)变迁t1对应join操作,其前驱库所p1表示线程u中join操作的前驱控制流状态,前驱库所pv1表示线程v的结束状态;后继库所p2表示线程u中join操作的后继控制流状态acq(u,l)p1plt1p2acq(u,l)变迁t1对应锁对象l的acq操作,其前驱库所p1表示线程u中acq操作的前驱控制流状态,前驱库所pl表示锁对象l;后继库所p2表示线程u中acq操作的后继控制流状态rel(u,l)plp1t1p2rel(u,l)变迁t1对应锁对象l的rel操作,其前驱库所p1表示线程u中rel操作的前驱控制流状态;后继库所p2表示线程u中rel操作的后继控制流状态,后继库所pl表示锁对象lrd(u,x)p1t1p2var:xrd(u,x)变迁t1对应共享变量x的读操作,其前驱库所p1表示线程u中该操作的前驱控制流状态;后继库所p2表示线程u中该操作的后继控制流状态.红色圆圈表示的是一个共享变量,它不属于Petri网的元素,仅用来描述此操作执行了某个变量的读操作wr(u,x)p1t1p2var:xwr(u,x)变迁t1对应共享变量x的写操作,其前驱库所p1表示线程u中该操作的前驱控制流状态;后继库所p2表示线程u中该操作的后继控制流状态.红色圆圈表示的是一个共享变量,它不属于Petri网的元素,仅用来描述此操作执行了某个变量的写操作stop(u)p1t1p2stop(u)变迁t1对应线程u的终止操作,其前驱库所p1表示线程u中该操作的前驱控制流状态;后继库所p2表示线程u中该操作的后继控制流状态需要强调的是,虽然上述 Petri 网是由程序的单一运行轨迹挖掘得到,但它实际隐含了原程序多个不同的可执行操作序列.究其原因,虽然某个具体的程序运行轨迹中,不同线程的锁获取操作对同一个锁对象有固定的先后顺序,但根据运行轨迹构造 Petri 网模型时并没有强加上这种因果依赖关系.3732软件学报2023 年第 34 卷第 8 期M=p3,pA0,pB0,plock=t0t1t2tB0tB1tB2tB3tA0tA1tA2tA3t3t4t5t6仍然以图 2 中的 Petri 网为例,锁对象 lock 对应的资源库所 plock有两个后继变迁 tA1与 tB0,它们构成一种冲突结构,从而带来了多种不同的可执行变迁序列:一种情景是变迁 tA0先引发,对应着线程 threaA 首先获得锁对象lock 的使用权;另一种情景是变迁 tB1先引发,对应着线程 threaB 首先获得锁对象 lock 的使用权.具体来说,当网系统在初始状态执行完毕变迁序列 t0t1t2后,Petri 网的标识为当前状态下,若 tA1先执行则得到前述可执行变迁序列,它对应表 1 中的程序运行轨迹;若 tB0先执行,则得到另一个可执行变迁,它对应着表 3 中的程序运行轨迹.显然,表 1 的运行轨迹未触发数据竞争,而表 3中第 7、8 行的两个操作则触发了数据竞争.接下来借助网展开等 Petri 网分析工具对不同执行情景下共享变量读写操作之间可能的并发关系进行检测,每个可能并发的共享变量读写操作都对应着源程序的一个潜在数据竞争.表3程序 Program1 的另一个操作执行序列序号主线程线程threadA线程threadB16:wr(mainThread,flag)227:fork(mainThread,threadA)328:fork(mainThread,threadB)418:acq(threadB,lock)519:rd(threadB,flag)620:rel(threadB,lock)722:wr(threadB,x)89:wr(threadA,x)910:acq(threadA,lock)1011:wr(threadA,flag)1112:rel(threadA,lock)1229:join(mainThread,threadA)1330:join(mainThread,threadB)1431:rd(mainThread,x)1532:stop(mainThread)3 基于 Petri 网展开的潜在数据竞争检测要检测源程序中某共享变量的读写/写写操作间是否存在数据竞争,实际只需分析前述所挖掘 Petri 网模型中这两个操作对应的变迁间是否可并发即可.在诸多 Petri 网分析工具中,Petri 网的展开技术24,30可以对变迁之间是否存在并发作出有效判断,为此,本文将基于 Petri 网的展开进行程序潜在数据竞争的检测.Petri 网展开技术基于出现网对系统行为进行分析,下面简单介绍相关概念,更多内容见文献 24,26,30.N=(P,T;F)y,y PTt,t Ttt,(t,y)F(t,y)FFyy#y(y,y)F+yy y(y,y)F(y,y)(F1)(y#y)yy|ytB0#tA1t2|tA0t4#t4首先,对于无标识网中的任意节点,若存在变迁使得(当中,指流关系 F 的自反传递闭包),则称节点 y 与冲突,记作;若则称 y 与具有因果关系,记作;若,则称 y 与并发,记作.例如,若忽略图 2 中的token,将其视作一个网,则我们有、特殊的,节点自身与自身冲突的情况称为自冲突,如.b B:|b|1ON=(B,E;G)b B:|b|1G+(G1)+=y BE:(y#y)y BEx|x BE(x,y)G+出现网(本文出现网的定义与文献 25 不同.文献 25 要求,这意味着网中不允许有冲突,本文允许不同节点间存在冲突)是一个三元组,当中 B 为库所集,又称条件集;E 为变迁集,又称事件集,它们满足(1);(2),即网中不含有向圈;(3),即网中不存在自冲突;(4),集合是有限的,即任意节点的前驱节点都是有限的.Petri 网展开利用出现网描述系统行为的基本思想如下:用出现网中的一个事件表示 Petri 网系统中某个变迁的一次执行,用出现网中的一个条件表示网系统运行中涉及的某个 token,出现网中的流关系用以刻画原始 Petri网中变迁执行对 token 的消耗和产生情况,Petri 网初始标识下的各个 token 分别对应出现网中一个没有前驱的条件.例如,图 3 中的出现网就是图 2Petri 网系统的一个有限展开.当中,各节点旁标有两个标签,节点内部的标签是出现网中该节点的唯一 ID,节点外的标签是该节点对应的原 Petri 网系统中库所或者变迁节点的 ID,双边框表示鲁法明等:基于 Petri 网展开的多线程程序数据竞争检测与重演3733ee|(e2e)G的事件为截断事件.Petri 网的展开中,一个事件 e 的局部配置定义为,局部配置对应的 Petri 网可达标识是指从初始状态执行 e 中各个事件后到达的原 Petri 网系统标识.若事件 e 局部配置对应的可达标识与某已经存在之事件局部配置对应的可达标识相等,则称 e 为截断事件.例如,图 3 给出的就是一个出现网,它用以描述图 2 中 Petri 网的行为.p0c0e1p1p2t0tB0p0BpB1tA1pA2tA2pA3tA3pA4pB3pB2pB3pB4tB1tB2tB3t1t2p3c2e2c4e4c7p4c26e20e19p5p6t4t3t5t6p7c27e21c28e22c29c9e8c6e6c20e17c17e15e12c11e10c15c14plockplockc22c23tB0pB1tB1pB2tB2c21e18c18e16e13c24tA0pA1pA0tA1pA2pA3tA2c8e7c5c3e5e3c10tA3pA4t3p4c13e14e9c19c12c25plockplockc1plocke11c16图3图 2 中程序 Petri 网模型的展开c0,c1文献 30 已指出,对于任意一个有界的 Petri 网系统,可以构造一个有限的出现网来刻画网系统的行为,称该出现网为原 Petri 网的有限完全展开.例如,图 3 所示的 Petri 网展开中,前驱为空的条件集合为,它对应原3734软件学报2023 年第 34 卷第 8 期p0,plockc24,c25,c13,c7pB3,plock,pA4,p