基于Petri网展开的多线程程序数据竞争检测与重演.pdf
《基于Petri网展开的多线程程序数据竞争检测与重演.pdf》由会员分享,可在线阅读,更多相关《基于Petri网展开的多线程程序数据竞争检测与重演.pdf(19页珍藏版)》请在咨信网上搜索。
1、基于 Petri 网展开的多线程程序数据竞争检测与重演*鲁法明1,黄莹1,2,曾庆田1,包云霞1,唐梦凡11(山东科技大学计算机科学与工程学院,山东青岛266590)2(中国科学院深圳先进技术研究院,广东深圳518055)通信作者:黄莹,E-mail:;包云霞,E-mail:摘要:数据竞争是多线程程序的常见漏洞之一,传统的数据竞争分析方法在查全率和准确率方面难以两全,而且所生成检测报告难以定位漏洞的根源.鉴于 Petri 网在并发系统建模和分析方面具有行为描述精确、分析工具丰富的优点,提出一种基于 Petri 网展开的新型数据竞争检测方法.首先,对程序的某一运行轨迹进行分析和挖掘,构建程序的一
2、个 Petri 网模型,它由单一轨迹挖掘得到,却可隐含程序的多个不同运行轨迹,由此可在保证效率的同时降低传统动态分析方法的漏报率;其次,提出基于 Petri 网展开的潜在数据竞争检测方法,相比静态分析方法在有效性上有较大提升,而且能明确给出数据竞争的产生路径;最后,对上一阶段检测到的潜在数据竞争,给出基于CalFuzzer 平台的潜在死锁重演调度方法,可剔除误报,保证数据竞争检测结果的真实性.开发相应的原型系统,结合公开的程序实例验证了所提方法的有效性.关键词:数据竞争;Petri 网;网展开;动态程序分析中图法分类号:TP311中文引用格式:鲁法明,黄莹,曾庆田,包云霞,唐梦凡.基于Petr
3、i网展开的多线程程序数据竞争检测与重演.软件学报,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
4、(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.Duetotheadv
5、antagesofPetrinetsintermsofaccuratebehavior description and rich analysis tools in the modeling and analysis of concurrent systems,this study proposes a new data racedetectionmethodbasedonPetrinetunfoldingtechnology.First,aPetrinetmodeloftheprogramisestablishedbyanalyzingandminingaprogramrunningtrac
6、e.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 t
7、he 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 en
8、sure theauthenticity of detection results.In addition,the corresponding prototype system is developed,and the effectiveness of the proposed*基金项目:国家自然科学基金(61602279);山东省泰山学者工程专项基金(ts20190936);山东省高等学校青创科技支持计划(2019KJN024);山东省博士后创新专项基金(201603056);国家海洋局海洋遥测工程技术研究中心开放基金(2018002);山东科技大学教学名师培育计划(MS20211102)本
9、文由“形式化方法与应用”专题特约编辑陈立前副教授、孙猛教授推荐.收稿时间: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:+86-10-62562563methodisverifiedbyopenprograminstanc
10、es.Key words:datarace;Petrinet;netunfolding;dynamicprogramanalysis大数据时代,随着对计算性能要求的不断提高,云计算和多线程程序等并行计算技术越来越受到人们的重视1,2.在多线程程序中,由于线程调度的时序不确定性以及共享内存空间访问控制的复杂性,如果设计不当,程序会存在诸多并发缺陷,进而导致运算结果出错甚至程序崩溃3.这些并发缺陷的检测和排除是多线程程序设计的一大挑战,而数据竞争4就是引起广泛关注的并发缺陷之一.数据竞争是指对同一块内存空间存在并发访问,并且至少有一个访问是写操作.数据竞争通常会对程序的正确性产生恶劣影响.但是,数
11、据竞争的产生场景往往难以检测,不仅需要特定的输入,还需要特定的线程调度顺序,这造成了数据竞争检测的困难.当前,数据竞争检测方法一般分为静态检测、动态检测和动静结合的数据竞争检测方法 3 类5.静态检测方法针对程序源代码进行分析,主要结合锁集对潜在的数据竞争缺陷进行检测,常见的静态检测工具包括 RacerX6、RELAY7和 locksmith8等.该类方法通过静态代码分析程序的完整行为,存在查全率高的优点.不过,由于静态分析方法不实际执行程序,它以源代码为输入直接进行程序分析,难以准确获取程序的运行时信息,从而导致了较高的误报率.此外,对程序全部行为进行分析使得静态分析方法时间效率偏低.动态检
12、测方法监视程序执行过程中的行为,收集必要的信息来判断哪些操作构成数据竞争.常见的动态数据竞争检测算法分为基于 lockset的算法911,基于 happens-before关系的算法1217,以及两者混合的 hybrid算法1820这 3 种.基于 lockset 的方法维护程序执行过程中每个线程的当前持有锁信息,同时更新共享变量持有的锁信息,当共享变量不再受到锁保护的时候,报告数据竞争;基于 happens-before关系的方法借助逻辑时钟识别两个操作之间因为同属于一个线程、因为锁的释放和申请,以及因为线程的 fork 或 join 而导致的因果关系,将不具备上述因果关系的两个操作识别为并
13、发.如果同一个共享变量的读写/写写操作之间是并发的,则认定两者构成数据竞争;hybrid 算法通常先基于 lockset 找到可疑的数据竞争,然后借助逻辑时钟等方法对可疑竞争的真实性进行验证.受限于线程执行交错的不确定性以及所收集信息的不完整性,动态竞争方法会有较多的漏检,但是数据竞争的动态分析方法一般比静态方法有更高的准确度.动静结合的数据竞争检测方法通常先通过静态方法检测潜在的数据竞争,然后,在程序动态执行过程中对线程的调度进行干预,以此增加数据竞争发生的概率,重演成功的数据竞争均为真实的并发缺陷.例如,文献 21 从一个已有的动态分析技术中获得的潜在数据竞争的相关信息,并据此控制线程的随
14、机调度程序,以提高真实数据竞争发生条件的出现概率,以此提高数据竞争重演成功的概率;文献 22 首先使用静态分析方法识别潜在的并发错误,然后使用静态程序切片来针对潜在的并发错误获取较小的程序,最后,动态控制线程的调度以便多个线程同时访问同一内存位置,以此验证并发错误是否会导致程序失败.文献 23 以有害数据竞争的检测为目标,首先综合考虑 happens-before 关系与 ad-hoc 类型的同步来精简需验证的数据竞争数量,然后,将相互之间不存在干扰的潜在数据竞争划分到同一组中,再借助线程调度器以组为单位对潜在数据竞争进行重演.动静结合的数据竞争检测方法综合两种方法的优点,在数据竞争的查全率、
15、准确度方面均有一定保证,不过,前期静态分析仍然耗时,后期动态重演通常是一些随机性的调度方法,重演成功率有待进一步提高.综上所述,目前的数据竞争检测方法在查全率、准确率方面难以两全,而且数据竞争检测的效率也有待提高.此外,如文献 5 所述,现有方法所产生的数据竞争报告使得开发者难以理解并据此追溯漏洞产生根源.针对上述问题,考虑到 Petri 网在并发系统建模和行为分析方面的优点,本文拟提出一种基于 Petri 网展开2430的新型数据竞争检测方法.首先,与动态检测方法类似,所提方法也是从多线程程序某次具体的运行轨迹出发进行分析,不过,从该轨迹出发,本文能构造出一个蕴含多种运行轨迹的程序 Petr
16、i 网模型,从该模型出发进行数据竞争检测能降低传统动态分析方法的漏报率,提高查全率;然后,与静态分析方法类似,通过对前述程序 Petri 网模型的分析检测潜在的数据竞争缺陷,本文将数据竞争检测问题转化为 Petri 网展开30中共享变量访问操作的并发关系识别,可有效提高数据竞争的检测效率;与此同时,潜在数据竞争对应的出现网片段可以很好地展示数据竞争产生的根源和具体路径;最后,由于程序运行轨迹中捕获的程序行为信息不够完备,由此挖掘到的 Petri 网模型可能与源程序在行鲁法明等:基于 Petri 网展开的多线程程序数据竞争检测与重演3727为上不一致,从而导致数据竞争误报的现象,为解决此问题,本
17、文给出一种数据竞争重演方法,重演成功的数据竞争可保证真实性,从而可提高检测准确率.就性能而言,本文从单一运行轨迹出发构造仅包含程序部分行为的Petri 网模型,相比静态分析方法构造反映程序全部行为的模型而言,所提方法简化了模型构建和分析的复杂度,在一定程度上可提升数据竞争检测方法的效率.1 实例与动机分析与经典的数据竞争动态分析方法类似,本文假设程序由有限个线程构成,这些线程通过共享对象的加锁/解锁以及读写进行同步和交互.在程序的一次运行过程中,将线程的启动/终止/阻塞、锁的获取和释放,以及共享对象读写等操作所构成的操作序列称为一条多线程程序运行轨迹,其形式化定义如下.定义 1.多线程程序运行
18、轨迹.多线程程序的运行轨迹,记作,是满足如下条件的一个操作序列: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,
19、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,获取成功
20、后读取共享变量 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 也存在一些
21、运行轨迹不会呈现上述并发缺陷,例如表 1 中的操作序列.当中,线程threadA 首先获得锁对象 lock 的使用权,并将共享变量 flag 的值设为 true;然后,线程 threadB 获得 lock 使用权,并将共享变量 x 的取值最终设置为 2.若程序按照表 1 中的轨迹执行,则前述数据竞争不会触发.对于图 1 中的 Program1,首先,基于 lockset 的数据竞争检测方法19不适用,因为该方法要求所有的共享变量在执行读写操作时都必须通过锁来保护,而 Program1 对共享变量 x 的访问操作均未加锁保护;其次,基于happens-before 关系的数据竞争检测方法,若以表
22、 1 中的运行轨迹为输入进行检测,也无法检测到实际存在的竞争.以得到广泛认可的 VerifiedFT17数据竞争检测算法为例,基于 happens-before 关系的数据竞争方法认为运行轨迹中一个锁释放操作与其后首次执行的该锁的申请操作间存在必然的因果关系.例如,表 1 的执行轨迹中,由于线程 threadA 释放锁对象 lock 的操作后,threadB 首次申请 lock,故 VerifiedFT 等基于 happens-before 关系的方法会假设在锁对象 lock 的使用权上,线程 threadA 一定先于 threadB,从而在两个操作之间加上一个错误的时序约束关系.而原本的程序
23、行为并不存在这一约束,线程 threadB 完全可以先获得 lock 的使用权,然后对变量 x 进行写操作,进而导致与 threadA 写 x 时的数据竞争.由此可见,传统的 happens-before 关系对程序行为人3728软件学报2023 年第 34 卷第 8 期为添加了更多的约束,从而导致数据竞争的漏报.lockset 与 happens-before 两者混合的 hybrid算法同时存在上述两个问题.123456789101112131415161718192021222324252627282930313233public class DataRaceTest static bo
24、oleanpublic 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;s
25、ynchronized(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
- 配套讲稿:
如PPT文件的首页显示word图标,表示该PPT已包含配套word讲稿。双击word图标可打开word文档。
- 特殊限制:
部分文档作品中含有的国旗、国徽等图片,仅作为作品整体效果示例展示,禁止商用。设计者仅对作品中独创性部分享有著作权。
- 关 键 词:
- 基于 Petri 展开 多线程 程序 数据 竞争 检测 重演
1、咨信平台为文档C2C交易模式,即用户上传的文档直接被用户下载,收益归上传人(含作者)所有;本站仅是提供信息存储空间和展示预览,仅对用户上传内容的表现方式做保护处理,对上载内容不做任何修改或编辑。所展示的作品文档包括内容和图片全部来源于网络用户和作者上传投稿,我们不确定上传用户享有完全著作权,根据《信息网络传播权保护条例》,如果侵犯了您的版权、权益或隐私,请联系我们,核实后会尽快下架及时删除,并可随时和客服了解处理情况,尊重保护知识产权我们共同努力。
2、文档的总页数、文档格式和文档大小以系统显示为准(内容中显示的页数不一定正确),网站客服只以系统显示的页数、文件格式、文档大小作为仲裁依据,平台无法对文档的真实性、完整性、权威性、准确性、专业性及其观点立场做任何保证或承诺,下载前须认真查看,确认无误后再购买,务必慎重购买;若有违法违纪将进行移交司法处理,若涉侵权平台将进行基本处罚并下架。
3、本站所有内容均由用户上传,付费前请自行鉴别,如您付费,意味着您已接受本站规则且自行承担风险,本站不进行额外附加服务,虚拟产品一经售出概不退款(未进行购买下载可退充值款),文档一经付费(服务费)、不意味着购买了该文档的版权,仅供个人/单位学习、研究之用,不得用于商业用途,未经授权,严禁复制、发行、汇编、翻译或者网络传播等,侵权必究。
4、如你看到网页展示的文档有www.zixin.com.cn水印,是因预览和防盗链等技术需要对页面进行转换压缩成图而已,我们并不对上传的文档进行任何编辑或修改,文档下载后都不会有水印标识(原文档上传前个别存留的除外),下载后原文更清晰;试题试卷类文档,如果标题没有明确说明有答案则都视为没有答案,请知晓;PPT和DOC文档可被视为“模板”,允许上传人保留章节、目录结构的情况下删减部份的内容;PDF文档不管是原文档转换或图片扫描而得,本站不作要求视为允许,下载前自行私信或留言给上传者【自信****多点】。
5、本文档所展示的图片、画像、字体、音乐的版权可能需版权方额外授权,请谨慎使用;网站提供的党政主题相关内容(国旗、国徽、党徽--等)目的在于配合国家政策宣传,仅限个人学习分享使用,禁止用于任何广告和商用目的。
6、文档遇到问题,请及时私信或留言给本站上传会员【自信****多点】,需本站解决可联系【 微信客服】、【 QQ客服】,若有其他问题请点击或扫码反馈【 服务填表】;文档侵犯商业秘密、侵犯著作权、侵犯人身权等,请点击“【 版权申诉】”(推荐),意见反馈和侵权处理邮箱:1219186828@qq.com;也可以拔打客服电话:4008-655-100;投诉/维权电话:4009-655-100。