多线程程序约束构建、优化求解及其智能测试方法研究

项目名称： 多线程程序约束构建、优化求解及其智能测试方法研究

项目编号： No.61472318

项目类型： 面上项目

立项/批准年度： 2015

项目学科： 自动化技术、计算机技术

项目作者： 杨子江

作者单位： 西安理工大学

项目金额： 84万元

中文摘要： 随着多核技术在CPU中的广泛使用，串行程序已难以发挥现有CPU的全部能力，多线程程序成为当前计算机性能提升的核心技术。由于线程调度难以控制、执行过程难以复现和线程交织导致状态空间爆炸等问题，多线程程序的测试难度远超过串行程序，成为多线程程序质量提升的难题和应用发展的瓶颈。 本项目旨在研究多线程程序的约束建模和智能测试方法，将其测试难度降低到与串行程序相近水平。本项目提出一种结合测试用例的多线程程序约束模型，描述程序状态转移、线程控制、案例正确性和初始条件，将多线程程序测试问题转化为约束求解问题；通过研究多线程程序约束构建、求解优化和交织序列精炼方法，检测程序中是否存在违背测试用例的线程交织路径；设计多线程程序智能测试工具（IDEA），验证研究成果的有效性。本研究突破多线程程序测试面临的线程控制和状态爆炸等问题，显著降低多线程程序测试难度和复杂度，具有较高理论创新性和显著应用价值。

中文关键词： 多线程程序测试；线程交织；约束模型；约束求解；SMT求解器

英文摘要： Since the multicore hardware systems have become ubiquitous, sequential software can no longer benefit from the hardware improvement. Multithreaded programming is considered the key technology to solve the software crisis by providing a mechanism for more efficient use of multiple cores and improved concurrency. However, testing multithreaded programs is extremely difficult due to several reasons. First, thread scheduling is controlled by operating systems so it is nontrivial to test a particular thread interleaving. Second, faulty executions cannot be easily reproduced. Last but not the least, the number of thread-interleaving is astronomically large so it is impossible to perform an exhaustive testing. As a result, the challenges in testing multithreaded program remain an obstacle that hampers the development of such software. In this proposal, we propose a novel testing method based on constraint construction and solving. The approach has the potential to reduce the complexity of testing multithreaded programs to a level comparable to that of testing sequential programs. In particular, we model the execution driven by a testing vector as a first-order logic formula that consists of four components: program transition, thread scheduling, testcase validity and initialization. The satisfiability of the formula, solvable by constraint solvers, can indicate the correctness of a multithreaded program under various thread interleavings without the need of repeated executions. The algorithms of constraint construction, constraints solving optimization and thread interleaving refinement are to be investigated to make our approach feasible and scalable. We will develop an intelligent debugger, named as IDEA, to test Java and C/C++ multithreaded programs. Being able to address the challenges of multithreaded program testing and dramatically reduce its difficulty and complexity, we believe our proposed project processes high theoretical and practical values.

英文关键词： multithreaded program testing;thread-interleaving;constraint model;constraint solving;satisfiability modulo theory solver