删除或更新信息,请邮件至freekaoyan#163.com(#换成@)

高精度的大规模程序数据竞争检测方法

本站小编 Free考研考试/2022-01-02

摘要:随着技术的不断发展,软件系统的非确定性(uncertainty)不断增强,数据竞争是并发系统这一类典型的非确定性软件系统中常见的缺陷.尽管数据竞争静态检测近年来取得了巨大进展,但其面临的重要问题仍然存在.先前的静态技术要么以分析精度为代价达到高扩展性,要么由于高精度分析而导致可扩展性问题.提出一种解决上述矛盾的分段分析方法——GUARD.它首先基于程序值流进行轻量级上下文敏感的数据访问分析,以识别出候选的数据竞争子路径而非完整的程序路径.接下来,进行可能并行执行(may-happen-in-parallel,即MHP)分析来确定程序中的两个数据访问操作是否可能会同时执行.MHP分析基于线程流图(TFG)将线程信息进行编码以便于高效地查询各个子路径之间的并发关系.最后,对于每条存在MHP数据访问的子路径,进行重量级路径敏感分析以确定数据竞争路径的可行性.针对12个开源项目的实验评估显示,GUARD能够在1 870s内完成对130万行代码的工业规模项目的检测,且平均误报率为16.0%.此外,GUARD的分析速度更快,比现有的前沿技术平均快了6.08倍,并且显著降低了误报率.除此之外,GUARD在其中还发现了12个数据竞争漏洞.将它们全部报告给了开发者,其中8个已得到了确认.



Abstract:With the development of techniques, the uncertainty in software systems is continuously increasing. Data race is a typical bug in current programs, which is a classic type of uncertainty programs. Despite significant progress in recent years, the important problem of practical static race detection remains open. Previous static techniques either suffer from a high false positive rate due to the compromise of precision, or scalability issues caused by a highly precise analysis. This paper presents GUARD, a staged approach to resolve this paradox. First, it performs a lightweight context-sensitive data access analysis, based on the value flow of a program, to identify the candidate data race subpaths instead of the whole program paths. Second, may-happen-in-parallel (MHP) analysis is employedto identify whether two data accesses in a program may execute concurrently. This stage is scalable, due to the design of the thread flow graph (TFG), which encodes thread information to query MHP relationship of the subpaths. Finally, for each subpath whose two data accesses are MHP, the heavyweight path-sensitive analysis is appliedto verify the feasibility of the data races. The evaluation demonstrates that GUARD can finish checking industrial-sized projects, up to 1.3MLoC, in 1 870s with an average false positive rate of 16.0%. Moreover, GUARD is faster than the state-of-the-art techniques with the average speedup 6.08X and significantly fewer false positives. Besides, GUARD has found 12 new race bugs in real-world programs. All of them are reportedtothe developers and 8 of them have been confirmed.



PDF全文下载地址:

http://jos.org.cn/jos/article/pdf/6260
相关话题/数据 程序 技术 系统 确认

  • 领限时大额优惠券,享本站正版考研考试资料!
    大额优惠券
    优惠券领取后72小时内有效,10万种最新考研考试考证类电子打印资料任你选。涵盖全国500余所院校考研专业课、200多种职业资格考试、1100多种经典教材,产品类型包含电子书、题库、全套资料以及视频,无论您是考研复习、考证刷题,还是考前冲刺等,不同类型的产品可满足您学习上的不同需求。 ...
    本站小编 Free壹佰分学习网 2022-09-19
  • 面向分布式图计算作业的容错技术研究综述
    摘要:随着图数据规模的日益庞大和图计算作业的日益复杂,图计算的分布化成为必然趋势.然而图计算作业在运行过程中面临着分布式图计算系统内外各种来源的非确定性所带来的严峻的可靠性问题.首先分析了分布式图计算框架中不确定性因素和不同类型图计算作业的鲁棒性,并提出了基于成本、效率和质量3个维度的面向分布式图计 ...
    本站小编 Free考研考试 2022-01-02
  • 自动驾驶智能系统测试研究综述
    摘要:随着人工智能技术的深入发展,自动驾驶已成为人工智能技术的典型应用,近十年来得到了长足的发展,作为一类非确定性系统,自动驾驶车辆的质量和安全性得到越来越多的关注.对自动驾驶系统,特别是自动驾驶智能系统(如感知模块、决策模块、综合功能及整车)的测试技术得到了业界和学界的深入研究.调研了56篇相关领 ...
    本站小编 Free考研考试 2022-01-02
  • 区块链系统中身份管理技术研究综述
    摘要:区块链技术是一种通过块链式结构、共识算法和智能合约来生成、存储、操作和验证数据的新型分布式基础架构和计算范式,其所构建的新型信任机制有助于推动互联网技术由信息互联网向价值互联网的转化.由于区块链中的账本数据采用公开交易记录、多节点共识确认的方式进行存储和验证,因此对系统中的身份管理及隐私保护提 ...
    本站小编 Free考研考试 2022-01-02
  • 基于分支标记的数据流模型的代码生成方法
    摘要:模型驱动开发以其低错误率、易仿真、易验证的特点,在嵌入式软件开发中被广泛应用.近年来,基于模型的嵌入式软件开发方法及相应工具也在逐渐发展和完善.数据流模型是各种建模工具中使用最为频繁的语义模型,然而,各种工具对于数据流模型的代码生成能力却参差不齐,特别是对于数据分支组件的支持,当前主流的建模工 ...
    本站小编 Free考研考试 2022-01-02
  • 面向SPARC处理器架构的操作系统异常管理验证
    摘要:航天器等安全关键系统是典型的嵌入式系统,具有多任务并发、中断频发等特点.操作系统是其最基础的软件,构建一个正确的操作系统是保障航天器系统高可信运行的关键.异常管理作为操作系统最底层的功能,负责引导系统控制流的突变来响应处理器状态中的某些变化,异常管理的正确性是整个操作系统正确性的基础.提出一种 ...
    本站小编 Free考研考试 2022-01-02
  • Petri网的反向展开及其在程序数据竞争检测的应用
    摘要:展开技术借助分支进程可在一定程度上缓解Petri网性质分析中的状态爆炸问题.但展开网中仍然包含了系统的所有状态信息.某些应用问题仅需对系统特定状态的可覆盖性进行判定,以此为目标,有望缩减网系统展开的规模.为此,针对安全Petri网的可覆盖性判定问题提出了一种目标导向的反向展开算法,结合启发式技 ...
    本站小编 Free考研考试 2022-01-02
  • 基于锁增广分段图的多线程程序死锁检测
    摘要:死锁是并行程序常见的缺陷之一,动态死锁分析方法根据程序运行轨迹构建锁图、分段图等模型来检测死锁.然而,锁图及其现有的各种变型无法区分同一循环中锁授权语句的多次执行,扩展锁图中记录的锁集无法捕捉线程曾经持有而又随后释放的锁信息,分段图无法刻画锁的获取和释放操作与线程启动操作耦合而导致的段间依赖关 ...
    本站小编 Free考研考试 2022-01-02
  • 面向数据流的ROS2数据分发服务形式建模与分析
    摘要:机器人操作系统(robotoperatingsystem,简称ROS)是一种开源的元操作系统,能够在异种计算簇上提供基于消息机制的结构化通信层.为改善ROS1中存在的数据分发实时性、可靠性问题,ROS2提出了面向数据流的数据分发服务机制.采用概率模型检验的方法,分析、验证ROS2系统数据分发机 ...
    本站小编 Free考研考试 2022-01-02
  • 面向持续软件工程的微服务架构技术专题前言
    摘要:随着软件互联网化和服务化的高度发展,持续性(continuity)成为现代软件系统的基本特性之一,覆盖从商业策划、软件开发、运维、演化的所有环节,使得软件系统在持续稳定提供功能和服务的同时,软件系统的边界和内部结构始终处于不断变化、持续更新和适应之中,持续软件工程(continuoussoft ...
    本站小编 Free考研考试 2022-01-02
  • 一种优化的数据流驱动的微服务化拆分方法
    摘要:近年来,微服务架构已经成为软件工程领域比较流行的架构风格,其天然支持DevOps和持续交付以及可伸缩性、可扩展性好等特性,驱动着业界实践者纷纷向微服务架构迁移.然而,采用微服务架构也面临诸多挑战,其中最关键的是缺乏自动化、一体化的解决方案来高效支持面向微服务的拆分设计以及候选微服务架构的评估. ...
    本站小编 Free考研考试 2022-01-02