CAREER: Automated Concurrency Debugging ? An Essential Ingredient for Safety-Critical Software Assurance and Security

检测和修复并发软件缺陷一直是劳动密集型的，由于固有的复杂性，在分析天文数字大量的线程交织。多核处理器的日益广泛使用加剧了这种情况，而多核处理器的计算能力只能通过并发软件来释放。这种检测和修复过程的自动化有望大幅减少调试此类系统所花费的时间，从而产生可靠和安全的软件以及充分利用的并行硬件。本研究的目标是通过自动化并发调试的创新来提高并发软件的可靠性和安全性。该项目将研究新的理论和算法进展，以及完全自动化大型并发软件的错误检测，诊断，修复和优化的关键过程的工具。这项研究的统一主题是明智的应用逻辑约束为基础的符号方法和自动线程干涉抽象。 符号化方法可以缓解并行软件分析、验证、综合和维护中的主要可扩展性瓶颈--交织爆炸。干扰抽象将使使用最经济的方法来分析系统的属性，通过下或过度近似的线程相互作用的建模。PI将把这项研究的结果纳入信息技术（IT）从业人员的本科计算课程和夏季再培训课程，目的是保持美国IT劳动力的竞争活力。

Detecting and repairing concurrent software defects has always been labor-intensive due to the inherent complexity in analyzing the astronomically large number of thread interleavings. The situation is exacerbated by the increasingly widespread use of multicore processors, whose computing power can only be unleashed by concurrent software. Automation of this detection and repair process promises to drastically reduce the time spent in debugging such systems, leading to reliable and secure software as well as fully utilized parallel hardware. The objective of this research is to improve the concurrent software reliability and security through innovations in automated concurrency debugging. This project will investigate new theoretical and algorithmic advances, and tools to fully automate the crucial process of bug detection, diagnosis, repair, and optimization for large concurrent software. The unifying theme of this research is the judicious application of logical constraint based symbolic methods and automated thread interference abstractions. Symbolic methods will mitigate interleaving explosion, which is the major scalability bottleneck in concurrent software analysis, verification, synthesis and maintenance. Interference abstraction will enable the use of the most economical methods to analyze properties of the system via under- or over-approximated modeling of thread interactions. The PI will incorporate the results from this research into the undergraduate computing curriculum and summer retraining courses for Information Technology (IT) practioners with the aim of maintaining the competitive vitality of the U.S. IT workforce.