CPA-SEL: Collaborative Research: Trace-Driven Verification of Multithreaded Software

CCF-0811287/CCF-0810865协作研究：跟踪驱动的多线程软件验证杨子江和Karem Sakalla超线程的使用不断增加，以及廉价多处理器硬件的可用，为软件开发人员提供了巨大的机遇和严峻的挑战。为了让软件应用程序受益于多核处理器中持续的指数级吞吐量增长，应用程序必须是编写良好的多线程软件程序。不幸的是，编写能够充分释放当前和未来硬件系统潜力的多线程软件程序，在今天仍然像30年前一样具有挑战性。这项研究旨在开发实用的工具和方法，将测试/调试多线程程序的复杂性降低到与测试/调试顺序程序相当的水平。为此，必须使用强大的推理引擎来增强现有的调试工具，这些引擎允许它们隐式地分析指定测试输入下所有可能的线程交错。在这个项目的过程中，将研究实现这一目标的各种方法，包括一些从初步分析中似乎特别有希望的新想法：(1)多线程程序的有效符号编码，(2)跟踪驱动的抽象和精化它们的执行，以及(3)允许该方法扩展到实际程序大小的性能增强技术。

CCF-0811287/CCF-0810865Collaborative Research: Trace-Driven Verification of Multithreaded SoftwareZijiang Yang and Karem SakallahThe ever increasing use of hyper-threading and the availability of inexpensive multiprocessor hardware present tremendous opportunities as well as serious challenges for software developers. In order for software applications to benefit from the continued exponential throughput advances in multicore processors, the applications must be well-written multithreaded software programs. Unfortunately, writing multithreaded software programs that can unleash the full potential of present and future hardware systems remains as challenging today as it was thirty years ago. This research aims to develop practical tools and methodologies that can bring down the complexity of testing/debugging multithreaded programs to a level comparable to that of testing/debugging sequential programs. To this end, existing debugging tools have to be enhanced with powerful reasoning engines that allow them to implicitly analyze all possible thread interleavings under the specified test inputs. During the course of this project a variety of approaches to achieve this objective will be investigated, including some novel ideas that seem particularly promising from a preliminary analysis: (1) efficient symbolic encoding of multithreaded programs, (2) trace-driven abstraction and refinement of their execution, and (3) performance enhancement techniques that allow this approach to scale to realistic program sizes.