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

点击翻译按钮获取中文摘要

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.