收缩候选回溯集的有状态动态偏序归约方法  

Stateful Dynamic Partial- order Reduction Method of Shrinking Candidate Backtrack Set

作　　者：赵璐[1] 张健沛[1] 杨静[1] 

机构地区：[1]哈尔滨工程大学计算机科学与技术学院,哈尔滨150001

出　　处：《计算机工程》2015年第5期70-76,共7页Computer Engineering

基　　金：国家自然科学基金资助项目(61370083;61073043;61073041);教育部高等学校博士学科点专项科研基金资助项目(20112304110011;20122304110012);哈尔滨市科技创新人才研究专项基金资助项目(2011RFXXG015)

摘　　要：在验证多线程并发程序时,将基于无状态或有状态搜索的软件模型检测与动态偏序归约方法相结合,能大幅缩减待验证程序的状态空间,而动态偏序归约需不断利用当前候选回溯集更新相应回溯集,导致更新回溯集的计算成本过高。为此,形式化定义收缩候选回溯集,消除原候选回溯集中满足同一回溯条件的冗余迁移。针对各交织的回溯点,使用当前收缩候选回溯集更新相应回溯集,实现基于有状态动态偏序归约方法的并发多线程程序验证。实验结果表明,与现有动态偏序归约方法相比,该方法能减少遍历迁移数,加速回溯集更新,提高动态软件模型检测效率。To verify multithreaded concurrent programs, combine stateless or stateful search based software model checking methods with Dynamic Partial-order Reduction（ DPOR） so as to significantly reduce the state space of programs explored. DPOR uses current candidate backtrack set to refine corresponding backtrack set, however, the former computation cost actually exceeds the latter refinement demand. To solve the problem, a stateful DPOR method of shrinking candidate backtrack set is presented. The shrinking candidate set is formally defined, which can delete the redundant transitions for the same backtrack condition. For every interleaving backtrack state, the proposed method exploits current shrinking candidate set to refine corresponding backtrack set. Consequently, the method performs the stateful DPOR method to verify concurrent programs. Experimental results show that the method reduces the number of transitions explored,speeds up the refinement process and increases the efficiency of dynamic model checking compared with existing DPOR method.

关 键 词：软件模型检测 动态偏序归约 有状态搜索 回溯集 收缩候选集 

分 类 号：TP301[自动化与计算机技术—计算机系统结构]