面向程序验证的并行程序状态空间态约简技术综述

Reducing Concurrent Program State Space for Program Verification: A Survey

程序验证是保证程序安全性的重要手段。随着采用多核技术的硬件环境日渐普及,越来越多的软件正通过转向基于共享内存的并行程序模型来充分利用现有的计算资源。各线程在并行执行时通过共享内存的访问互相干扰执行状态,导致可能执行路径数成几何级数增长,进而产生可达状态空间爆炸问题。由于验证并行程序安全性主要通过分析程序可达状态来实现,因此,对并行程序可达状态空间的约简是决定并行程序验证效率的关键因素。首先对面向并行程序验证的并行程序可达状态空间约简方法进行了分类,然后对各类可达状态空间约简方法分别进行了分析和总结,最后指出了当前存在的问题和未来解决这些问题的研究方向。

Program verification is the critical means to ensure the program safety.During the maturity of multi-core hardware,there have been many programs which utilize the existed computing resources by adopting the memory shared concurrent program model.The concurrent threads interference with each other via the shared variables,which makes the reachable states increase with exponent factors.As a result,it results in the problem of combination explosion.Because the program verification relies on the reachable states,reducing the reachable state space is the key to the efficiency of program verification.In this paper,the reachable state reduction methods for concurrent program verification are classified,and the different kinds of reducing reachable states are analyzed and summarized.In the end,the issues which are still open are summarized and the future research directions to address these issues are also discussed.