SHF: Small: New Algorithmic Paradigms in Dynamic Analysis of Multithreaded Software

SHF：Small：多线程软件动态分析中的新算法范式

• 批准号: 2007428
• 负责人: Mahesh Viswanathan
• 金额: $ 25万
• 依托单位: University of Illinois at Urbana-Champaign
• 依托单位国家: 美国
• 项目类别: Standard Grant
• 财政年份: 2020
• 资助国家: 美国
• 起止时间: 2020-07-01 至 2024-06-30
• 项目状态: 已结题
• 来源: https://www.nsf.gov/awardsearch/showAward?AWD_ID=2007428&HistoricalAwards=false
• 关键词: SHF; Small; New; Algorithmic; Paradigms

Building reliable, bug-free software is an important and challenging problem. Dynamic analysis of system traces is one among several facets of a multi-pronged strategy that tries to address this problem through scalable, automated analysis methods that identify bugs in software. Here one observes a deployed system or a component under test, to extract a trace of relevant events, which is then automatically analyzed to determine if the execution is symptomatic of a bug in the system. This project develops sound, predictive dynamic analysis techniques to detect races, atomicity violations, deadlocks, and other concurrency properties that scale to traces with a large number of events.This project focuses on offline dynamic analysis, wherein a stored trace of a program is examined. These traces are often very large to ensure that the trace exercises large parts of a production-scale software. Therefore, to minimize storage needs, these traces are compressed. This project develops algorithms to analyze such compressed traces directly without first uncompressing the trace and then analyzing it. Such an algorithm will be provably fast since they will run in time that is linear in the size of the compressed trace. The project develops instructional material to be used by the investigators in outreach activities for the local Girls Who Code chapter, and will be available on teacher forums throughout the country.This award reflects NSF's statutory mission and has been deemed worthy of support through evaluation using the Foundation's intellectual merit and broader impacts review criteria.

构建可靠、无错误的软件是一个重要且具有挑战性的问题。系统跟踪的动态分析是多管齐下策略的几个方面之一，该策略试图通过可扩展的、自动化的分析方法来识别软件中的错误来解决这个问题。在这里，人们观察已部署的系统或正在测试的组件，以提取相关事件的跟踪，然后自动分析该跟踪以确定执行是否是系统中错误的症状。 该项目开发完善的预测动态分析技术，以检测竞争、原子性违规、死锁和其他并发属性，这些属性可扩展到大量事件的跟踪。该项目专注于离线动态分析，其中检查程序的存储跟踪。这些跟踪通常非常大，以确保跟踪运行生产规模软件的大部分。因此，为了最大限度地减少存储需求，这些痕迹被压缩。该项目开发了直接分析此类压缩轨迹的算法，而无需先解压缩轨迹然后进行分析。这样的算法将被证明是快速的，因为它们的运行时间与压缩轨迹的大小成线性关系。该项目开发了指导材料，供调查人员在当地“编程女孩”分会的外展活动中使用，并将在全国各地的教师论坛上提供。该奖项反映了 NSF 的法定使命，并通过使用基金会的智力价值和更广泛的影响审查标准。

项目成果

Controller Synthesis for Linear System With Reach-Avoid Specifications

具有避免触及规格的线性系统的控制器综合

• DOI: 10.1109/tac.2021.3069723
• 发表时间: 2022-04
• 期刊: IEEE Transactions on Automatic Control
• 影响因子: 6.8
• 作者: Fan, Chuchu;Qin, Zengyi;Mathur, Umang;Ning, Qiang;Mitra, Sayan;Viswanathan, Mahesh
• 通讯作者: Viswanathan, Mahesh

A tree clock data structure for causal orderings in concurrent executions

用于并发执行中因果排序的树时钟数据结构

• DOI: 10.1145/3503222.3507734
• 发表时间: 2022-02
• 期刊: ACM International Conference on Architectural Support for Programming Languages and Operating Systems
• 作者: Mathur, Umang;Pavlogiannis, Andreas;Tunç, Hünkar Can;Viswanathan, Mahesh
• 通讯作者: Viswanathan, Mahesh

Checking LTL[F,G,X] on compressed traces in polynomial time

在多项式时间内检查压缩迹线上的 LTL[F,G,X]

• DOI: 10.1145/3468264.3468557
• 发表时间: 2021-08
• 期刊: ACM Joint European Software Engineering Conference and Symposium on the Foundations of Software Engineering
• 作者: Zhang, Minjian;Mathur, Umang;Viswanathan, Mahesh
• 通讯作者: Viswanathan, Mahesh

Atomicity Checking in Linear Time using Vector Clocks

使用矢量时钟进行线性时间原子性检查

• DOI: 10.1145/3373376.3378475
• 发表时间: 2020-03
• 期刊: International Conference on Architectural Support for Programming Languages and Operating Systems
• 作者: Mathur, Umang;Viswanathan, Mahesh
• 通讯作者: Viswanathan, Mahesh

Sound Dynamic Deadlock Prediction in Linear Time

线性时间内的可靠动态死锁预测

• DOI: 10.1145/3591291
• 发表时间: 2023-04-07
• 期刊: Proceedings of the ACM on Programming Languages
• 作者: Umang Mathur;Andreas Pavlogiannis;Hunkar Can Tuncc;Mahesh Viswanathan
• 通讯作者: Mahesh Viswanathan