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

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.

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

本项目旨在研究多线程程序的约束建模和智能测试方法，将其测试难度降低到与串行程序相近水平。本项目提出一种结合测试用例的多线程程序约束模型，描述程序状态转移、线程控制、案例正确性和初始条件，将多线程程序测试问题转化为约束求解问题；通过研究多线程程序约束构建、求解优化和交织序列精炼方法，检测程序中是否存在违背测试用例的线程交织路径；设计多线程程序智能测试工具（IDEA），验证研究成果的有效性。本项目发表论文20余篇，其中CCF A期刊会议12篇（包括IEEE ICSE 、IEEE TSE、IEEE TIFS等）；申请专利11项，获得授权5项，包括美国专利1项；主持CCF A类会议ASE 2016多线程程序分会1次；培养博士研究生4人，硕士研究生10人。各项指标均超额完成预期任务。