GC-MCR:有向图约束指导的并发缺陷检测方法
作者:
作者简介:

李硕川(1999-),男,硕士生,CCF学生会员,主要研究领域为并发缺陷检测,系统软件分析;赵英全(1994-),男,博士生,主要研究领域为编译器测试,JVM测试,并发测试;王赞(1979-),男,博士,副教授,CCF专业会员,主要研究领域为软件测试,机器学习;王海弛(1996-),男,博士生,主要研究领域为系统软件分析;马明旭(1999-),男,学士,主要研究领域为并发测试;王昊宇(1999-),男,硕士生,CCF学生会员,主要研究领域为并发缺陷检测,编译器测试;陈翔(1980-),男,博士,副教授,CCF高级会员,主要研究领域为智能软件工程,软件仓库挖掘,软件测试与维护.

通讯作者:

王赞,E-mail:wangzan@tju.edu.cn

基金项目:

国家自然科学基金(61872263);天津市智能制造专项资金(20201180)


GC-MCR: Directed Graph Constraint-guided Concurrent Bug Detection Method
Author:
  • 摘要
  • | |
  • 访问统计
  • |
  • 参考文献 [61]
  • |
  • 相似文献 [20]
  • | | |
  • 文章评论
    摘要:

    约束求解应用到程序分析的多个领域,在并发程序分析方面也得到了深入的应用.并发程序随着多核处理器的快速发展而得到广泛使用,然而并发缺陷对并发程序的安全性和可靠性造成了严重的影响,因此,针对并发缺陷的检测尤为重要.并发程序线程运行的不确定性导致的线程交织爆炸问题,给并发缺陷的检测带来了一定挑战.已有并发缺陷检测算法通过约减无效线程交织,以降低在并发程序状态空间内的探索开销.比如,最大因果模型算法把并发程序状态空间的探索问题转换成约束求解问题.然而,其在约束构建过程中会产生大量冗余和冲突的约束,大幅度增加了约束求解的时间以及约束求解器的调用次数,降低了并发程序状态空间的探索效率.针对上述问题,提出了一种有向图约束指导的并发缺陷检测方法GC-MCR (directed graph constraint-guided maximal causality reduction).该方法旨在通过使用有向图对约束进行过滤和约减,从而提高约束求解速度,并进一步提高并发程序状态空间的探索效率.实验结果表明:GC-MCR方法构建的有向图可以有效优化约束的表达式,从而提高约束求解器的求解速度并减少求解器的调用次数.与现有的J-MCR方法相比,GC-MCR的并发程序缺陷检测效率可以取得显著提升,且不会降低并发缺陷的检测能力,在现有研究方法广泛使用的38组并发测试程序上的测试时间可以平均减少34.01%.

    Abstract:

    Constraint solving has been applied to many domains of program analysis, and deeply applied in concurrent program analysis. Concurrent programs are specific domain software that has been widely used with the rapid development of multi-core processors. However, concurrent defects threaten the security and robustness of concurrent programs, thus it is of great importance to test concurrent programs. Due to the non-deterministic thread scheduling, one of the key challenges for concurrent program testing is how to reduce the thread interleaving space with exponential growth. The state-of-the-art approaches (i.e., J-MCR) tackle the challenge through constraint solving. However, it is found that there exist conflicts and redundancies inside constraints (i.e., the conflict of constraint clauses makes constraints unsatisfiable), solving those unsatisfiable constraints results in lower efficiency. Thus, a directed graph constraint-guided method called GC-MCR (directed graph constraint-guided maximal causality reduction) is proposed. By removing conflictive constraints and simplify redundant constraints, the times of constraint solving are reduced thereby further improving the efficiency. Comparing with state-of-the-art approach J-MCR, GC-MCR reduces the times of constraint solving by 19.36% on average and reduces the testing time on average by 34.01% on 38 concurrent programs.

    参考文献
    [1] Jiang YY, Xu C, Ma XX, et al.Approaches to obtaining shared memory dependences for dynamic analysis of concurrent programs:A survey.Ruan Jian Xue Bao/Journal of Software, 2017, 28(4):747-763(in Chinese with English abstract).http://www.jos.org.cn/1000-9825/5193.htm[doi:10.13328/j.cnki.jos.005193]
    [2] Bo LL, Jiang SJ, Zhang UM, et al.Research progress on techniques for concurrency bug detection.Computer Science, 2019, 46(5):13-20(in Chinese with English abstract).
    [3] Su XH, Yu Z, Wang TT, et al.A survey on exposing, detectingand avoiding concurrency bugs.Chinese Journal of Computers, 2015, 38(11):2215-2233(in Chinese with English abstract).
    [4] Putchala MK, Bryant AR.Synchron-ITS:An interactive tutoring system to teach process synchronization and shared memory concepts in an operating systems course.In:Proc.of the 2016 Int'l Conf.on Collaboration Technologies and Systems (CTS 2016).2016.180-187.
    [5] Huang J, Meredith PO, Rosu G.Maximal sound predictive race detection with control flow abstraction.In:Proc.of the ACM SIGPLAN Conf.on Programming Language Design and Implementation (PLDI 2014).2014.337-348.
    [6] Park S, Vuduc RW, Harrold MJ.Falcon:Fault localization in concurrent programs.In:Proc.of the 32nd ACM/IEEE Int'l Conf.on Software Engineering (ICSE 2010).2010.245-254.
    [7] Lu GZ, Xu L, Yang YB, Xu BW.Predictive analysis for race detection in software-defined networks.Science China Information Sciences, 2019, 62(6):062101:1-062101:20.
    [8] Cai Y, Lu Q.Dynamic testing for deadlocks via constraints.IEEE Trans.on Software Engineering, 2016, 42(9):825-842.
    [9] Engler DR, Ashcraft K.RacerX:Effective, static detection of race conditions and deadlocks.In:Proc.of the 19th ACM Symp.on Operating Systems Principles (SOSP 2003).2003.237-252.
    [10] Letko Z, Vojnar T, Krena B.AtomRace:Data race and atomicity violation detector and healer.In:Proc.of the 6th Workshop on Parallel and Distributed Systems:Testing, Analysis, and Debugging (PADTAD 2008), Held in Conjunction with the ACM SIGSOFT Int'l Symp.on Software Testing and Analysis (ISSTA 2008).2008.
    [11] Huang J, Zhang C, Dolby J.CLAP:Recording local executions to reproduce concurrency failures.In:Proc.of the ACM SIGPLAN Conf.on Programming Language Design and Implementation (PLDI 2013).2013.141-152.
    [12] Lu S, Tucek J, Qin F, Zhou YY.AVIO:Detecting atomicity violations via access-interleaving invariants.IEEE Micro, 2007, 27(1):26-35.
    [13] Clarke EM, Grumberg O, Minea M, Peled D.State space reduction using partial order techniques.Int'l Journal on Software Tools for Technology Transfer, 1999, 2(3):279-287.
    [14] Flanagan C, Godefroid P.Dynamic partial-order reduction for model checking software.In:Proc.of the 32nd ACM SIGPLAN-SIGACT Symp.on Principles of Programming Languages (POPL 2005).2005.110-121.
    [15] Godefroid P.Partial-order Methods for the Verification of Concurrent Systems-An Approach to the State-explosion Problem.Springer, 1996.
    [16] Mazurkiewicz A.Trace Theory.Petri Nets:Applications and Relationships to Other Models of Concurrency.Berlin, Heidelberg, 1987.278-324.
    [17] Lamport L.Time, clocks, and the ordering of events in a distributed system.Communications of the ACM, 1978, 21(7):558-565.
    [18] Huang J.Stateless model checking concurrent programs with maximal causality reduction.In:Proc.of the 36th ACM SIGPLAN Conf.on Programming Language Design and Implementation.2015.165-174.
    [19] Serbanuta TF, Chen F, Rosu G.Maximal causal models for sequentially consistent systems.In:Proc.of the 3rd Int'l Conf.on Runtime Verification (RV 2012).Revised Selected Papers, 2012.136-150.
    [20] de Moura LM, Bjørner N.Z3:An efficient SMT solver.In:Proc.of the 14th Int'l Conf.on Tools and Algorithms for the Construction and Analysis of Systems (TACAS 2008), Held as Part of the Joint European Conf.on Theory and Practice of Software (ETAPS 2008).2008.337-340.
    [21] Zhao YQ, Wang Z, Liu S, et al.Achieving high MAP-coverage through pattern constraint reduction.IEEE Trans.on Software Engineering, 2022.[doi:10.1109/TSE.2022.3144480]
    [22] Wang Z, Zhao YQ, Liu S, et al.MAP-coverage:A novel coverage criterion for testing thread-safe classes.In:Proc.of the 34th IEEE/ACM Int'l Conf.on Automated Software Engineering (ASE 2019).2019.722-734.
    [23] Cai Y, Yun H, Wang JQ, et al.Sound and efficient concurrency bug prediction.In:Proc.of the 29th ACM Joint European Software Engineering Conf.and Symp.on the Foundations of Software Engineering (ESEC/FSE 2021).2021.255-267.
    [24] ASM bytecode analysis framework.http://asm.ow2.org/
    [25] Choudhary A, Lu S, Pradel M.Efficient detection of thread safety violations via coverage-guided generation of concurrent tests.In:Proc.of the 39th Int'l Conf.on Software Engineering (ICSE 2017).2017.266-277.
    [26] Yu J, Narayanasamy S, Pereira C, et al.Maple:A coverage-driven testing tool for multithreaded programs.In:Proc.of the ACM Int'l Conf.on Object Oriented Programming Systems Languages and Applications.2012.485-502.
    [27] Yue H, Wu P, Chen TY, et al.Input-driven active testing of multi-threaded programs.In:Proc.of the 2015 Asia-Pacific Software Engineering Conf.(APSEC).2015.246-253.
    [28] He F, Sun ZH, Fan HY.Satisfiability modulo ordering consistency theory for multi-threaded program verification.In:Proc.of the 42nd ACM SIGPLAN Int'l Conf.on Programming Language Design and Implementation (PLDI 2021).2021.1264-1279.[doi:10.1145/3453483.3454108]
    [29] Alglave J, Kroening D, Tautschnig M.Partial orders for efficient bounded model checking of concurrent software.In:Proc.of the 25th Int'l Conf.on Computer Aided Verification (CAV 2013).2013.141-157.
    [30] Yin L, Dong W, Liu WW, et al.On scheduling constraint abstraction for multi-threaded program verification.IEEE Trans.on Software Engineering, 2020, 46(5):549-565.
    [31] Wang C, Said M, Gupta A.Coverage guided systematic concurrency testing.In:Proc.of the 33rd Int'l Conf.on Software Engineering (ICSE 2011).2011.221-230.
    [32] Hong S, Ahn J, Park S, et al.Testing concurrent programs to achieve high synchronization coverage.In:Proc.of the Int'l Symp.on Software Testing and Analysis (ISSTA 2012).2012.210-220.
    [33] Steenbuck S, Fraser G.Generating unit tests for concurrent classes.In:Proc.of the 6th IEEE Int'l Conf.on Software Testing, Verification and Validation (ICST 2013).2013.144-153.[doi:10.1109/ICST.2013.33]
    [34] Terragni V, Cheung SC.Coverage-driven test code generation for concurrent classes.In:Proc.of the 38th Int'l Conf.on Software Engineering (ICSE 2016).2016.1121-1132.[doi:10.1145/2884781.2884876]
    [35] Yang CD, Souter AL, Pollock LL.All-du-path coverage for parallel programs.In:Proc.of the ACM SIGSOFT Int'l Symp.on Software Testing and Analysis (ISSTA'98).1998.153-162.
    [36] Krena B, Letko Z, Vojnar T.Coverage metrics for saturation-based and search-based testing of concurrent software.In:Proc.of the 2nd Int'l Conf.on Runtime Verification (RV 2011).LNCS 7186, 2012.177-192.
    [37] Savage S, Burrows M, Nelson G, et al.Eraser:A dynamic data race detector for multithreaded programs.ACM Trans.on Computer Systems, 1997, 15(4):391-411.
    [38] Choi JD, Lee K, Loginov A, et al.Efficient and precise datarace detection for multithreaded object-oriented programs.In:Proc.of the 2002 ACM SIGPLAN Conf.on Programming Language Design and Implementation (PLDI).2002.258-269.[doi:10.1145/512529.512560]
    [39] Musuvathi M, Qadeer S, Ball T, et al.Finding and reproducing heisenbugs in concurrent programs.In:Proc.of the 8th USENIX Symp.on Operating Systems Design and Implementation (OSDI 2008).2008.267-280.
    [40] Shacham O, Sagiv M, Schuster A.Scaling model checking of dataraces using dynamic informatio.Journal of Parallel and Distributed Computing, 2007, 67(5):536-550.
    [41] Khurshid S, Pasareanu CS, Visser W.Test input generation with Java PathFinder:Then and now (invited talk abstract).In:Proc.of the 27th ACM SIGSOFT Int'l Symp.on Software Testing and Analysis (ISSTA 2018).2018.1-2.
    [42] Musuvathi M, Qadeer S.Iterative context bounding for systematic testing of multithreaded programs.In:Proc.of the ACM SIGPLAN 2007 Conf.on Programming Language Design and Implementation.2007.446-455.
    [43] Engler D, Ashcraft K.RacerX:Effective, static detection of race conditions and deadlocks.In:Proc.of the 19th ACM Symp.on Operating Systems Principles (SOSP 2003).2003.237-252.
    [44] Nishiyama H.Detecting data races using dynamic escape analysis based on read barrier.In:Proc.of the 3rd Virtual Machine Research and Technology Symp.2004.127-138.
    [45] Elmas T, Qadeer S, Tasiran S.Precise race detection and efficient model checking using locksets.Technical Report, MSR-TR-2005-118, Microsoft Research Microsoft Corporation, 2005.
    [46] Lahiri SK, Qadeer S, Rakamaric Z.Static and precise detection of concurrency errors in systems code using SMT solvers.In:Proc.of the 21st Int'l Conf.on Computer Aided Verification (CAV 2009).2009.509-524.
    [47] Wang F, Rompf T.From gameplay to symbolic reasoning:Learning SAT solver heuristics in the style of Alpha (Go) zero.arXiv:1802.05340v1, 2018.
    [48] Bello I, Pham H, Le QV, et al.Neural combinatorial optimization with reinforcement learning.In:Proc.of the 5th Int'l Conf.on Learning Representations (ICLR 2017).2017.
    [49] Xu L, Hoos H, Leyton-Brown K.Predicting satisfiability at the phase transition.In:Proc.of the 26th AAAI Conf.on Artificial Intelligence.2012.
    [50] Lu K, Wu Z, Wang XP, et al.RaceChecker:Efficient identification of harmful data races.In:Proc.of the 23rd Euromicro Int'l Conf.on Parallel, Distributed, and Network-based Processing (PDP 2015).2015.78-85.
    [51] Perkovic D, Keleher PJ.Online data-race detection via coherency guarantees.In:Proc.of the 2nd USENIX Symp.on Operating Systems Design and Implementation (OSDI).1996.47-57.
    [52] von Praun C, Gross TR.Object race detection.In:Proc.of the 2001 ACM SIGPLAN Conf.on Object-oriented Programming Systems, Languages and Applications (OOPSLA 2001).2001.70-82.
    [53] Yu Y, Rodeheffer T, Chen W.RaceTrack:Efficient detection of data race conditions via adaptive tracking.In:Proc.of the 20th ACM Symp.on Operating Systems Principles (SOSP 2005).2005.221-234.
    [54] von Praun C, Gross TR.Static conflict analysis for multi-threaded object-oriented programs.In:Proc.of the ACM SIGPLAN 2003 Conf.on Programming Language Design and Implementation.2003.115-128.
    [55] Elmas T, Qadeer S, Tasiran S.Goldilocks:A race and transaction-aware Java runtime.In:Proc.of the ACM SIGPLAN 2007 Conf.on Programming Language Design and Implementation.2007.245-255.
    [56] Pozniansky E, Schuster A.MultiRace:Efficient on-the-fly data race detection in multithreaded C++ programs.Concurrency and Computation Practice and Experience, 2007, 19(3):327-340.
    [57] Zhang Y, Liu H, Qiao L.Context-sensitive data race detection for concurrent programs.IEEE Access, 2021, 9:20861-20867.
    附中文参考文献
    [1] 蒋炎岩, 许畅, 马晓星, 等.获取访存依赖:并发程序动态分析基础技术综述.软件学报, 2017, 28(4):745-763.http://www.jos.org.cn/1000-9825/5193.htm[doi:10.13328/j.cnki.jos.005193]
    [2] 薄莉莉, 姜淑娟, 张艳梅, 等.并发缺陷检测技术研究进展.计算机科学, 2019, 46(5):13-20.
    [3] 苏小红, 禹振, 王甜甜, 等.并发缺陷暴露、检测与规避研究综述.计算机学报, 2015, 38(11):2215-2233.
    引证文献
    网友评论
    网友评论
    分享到微博
    发 布
引用本文

李硕川,王赞,马明旭,陈翔,赵英全,王海弛,王昊宇. GC-MCR:有向图约束指导的并发缺陷检测方法.软件学报,2023,34(8):3485-3506

复制
分享
文章指标
  • 点击次数:1228
  • 下载次数: 3558
  • HTML阅读次数: 1993
  • 引用次数: 0
历史
  • 收稿日期:2022-09-04
  • 最后修改日期:2022-10-13
  • 在线发布日期: 2022-12-30
  • 出版日期: 2023-08-06
文章二维码
您是第19700992位访问者
版权所有:中国科学院软件研究所 京ICP备05046678号-3
地址:北京市海淀区中关村南四街4号,邮政编码:100190
电话:010-62562563 传真:010-62562533 Email:jos@iscas.ac.cn
技术支持:北京勤云科技发展有限公司

京公网安备 11040202500063号