面向程序验证的并行程序状态空间态约简的几个

　　0引 言
　　多核硬件环境的日益普及使得能够深度挖掘计算资源的并行化软件已然成为软件行业的主流，进而即刻不断满足日渐提高的性能需求和功能需求。其中，基于共享内存的并行程序模型在和基于消息通讯的并行程序相较候可知，该模型具有访问便捷、信息交换开销低廉等优势特点，足可堪称当前主要的并行程序通讯模型，并在航天、武器、交通、核电、医疗和金融等安全攸关领域有着极为广泛且重要的应用。毫无疑问，并行软件的安全性就是影响其应用的关键因素。而程序验证则是保证程序安全性的重要手段， 一般情况下是由描述验证条件的规格说明和计算程序可达状态的分析算法组合构成。程序验证的目的就是旨在通过程序分析来判断程序的可达状态是否满足验证条件。然而，各线程在并行执行时通过共享内存的访问互相干扰执行状态，就将导致可能执行路径数成几何量级增长，进而产生可达状态空间组合爆炸问题，也为验证并行程序安全性制造了攻克难点与挑战。
　　在此，并行程序可达状态空间约简可表述为：通过一定规则来合并具有相同或相似可达程序状态路径的搜索策略，由此即可缓解来自组合爆炸导致的复杂计算压力。同时，对并行程序可达状态空间的约简效果还将直接决定对并行程序验证的可实现效率及可应用规模。当前的并行程序可达状态空间约简方法即是从不同角度出发、并采取多样的规则对并行程序中的路径进行明确划分，有效地解决或缓解研究环境中面临的问题，但是，其约简方法却仍将受到其他条件制约。所以，如何进一步整合并行程序可达状态空间的各种约简方法的优点并克服其各自缺点就依然是目前一个亟需深入探讨与解决的开放性问题。
　　本文首先对当前的并行程序可达状态空间的约简方法进行介绍，而后又分别就其优点和不足展开相应分析，并基于此再次给出这对这些不足的研究方向综述。
　　1并行程序可达状态空间约简方法分类
　　并行程序可达状态空间约简的目标是如何有效缓解由交叠执行所导致的状态空间组合爆炸问题。但由于对程序并行性的不同视角则决定了在搜索可达状态空间时的不同约简策略，为此即根据消除并行程序空间状态冗余的不同出发点而将并行程序可达状态空间约简方法具体分为以下四类：偏序关系约简方法、模块性约简方法、对称性约简方法和并行干扰约简方法。下面对这四类约简方法进行逐一的阐述与介绍。
　　1.1 偏序关系约简方法
　　偏序关系约简是从踪迹的独立性出发，而只搜索可能产生不同程序状态的踪迹。Godefroid就研究了独立变迁的等价关系[1]。两个变迁若称为独立，当且仅当在一条踪迹中这两个临近的变迁调换执行顺序后该踪迹的可达状态不变。鉴于该方法只是分析并行线程交叠执行等价类中的代表踪迹，因而避免了交叠执行等价类内其它踪迹的冗余分析。
　近期研究则主要集中在如何提高交叠执行等价类的划分精度。已有研究可知，通过静态分析的方法计算踪迹等价类中的可调度变迁却将占据较大时空开销。为了解决这一问题，Flanagan等即相应提出了动态偏序关系约简[2]，通过动态跟踪线程间交叠执行位置来分析发生冲突的回溯点。然而，该方法仍然存在重复访问等价踪迹类内的其他并行状态的可能。为了避免重复访问并行状态问题，分别由Gueta等提出了笛卡儿偏序关系约简[3]和Yang等提出的含有状态的动态偏序关系约简[4]，其主要思想是通过识别变迁间的依赖关系来区分可达状态。同时，又依次由Kahlon等提出了单调偏序关系约简[5]和由Abdulla等进一步提出的优化动态偏序关系约简[6]，其主要成果则是通过对调度赋予权重来优化遍历次序。而且，Kusano等[7]又采用了动态分析和静态分析相结合的偏序关系约简策略，具体结合点则是利用提出的谓词依赖关系而将并行程序状态空间抽象为可能导致断言失败或死锁的冲突内存访问对，其实现过程是将目标程序插桩，同时再通过依赖算子分析并行操作间的依赖关系，而后又以此为依据在动态分析已插桩的目标程序时采用动态偏序约简策略来对冗余的交叠踪迹完成剪枝处理。
　　1.2 并行程序模块化验证
　　并行程序模块化约简是从线程内局部操作和全局操作的差别出发，通过分别推理线程内程序状态和线程间作用状态来降低搜索空间。具体地，依赖保证约简（Rely-Guarantee，RG）即是典型代表，如文献[8-13]。该方法首先假设外界线程对本地线程的影响，作为依赖（Rely），由此推理线程内局部状态，再分析本地线程施加于远端并行线程对的影响，作为保证（Guarantee）。其后则迭代分析可达状态，直到状态空间稳定。
　　归纳数据流图（Inductive Data Flow Graph， iDFG）方法[14-15]同样利用了线程间交互的模块性特点，即通过迭代分析共享变量在线程间的数据流图来搜索状态空间。而与此迭代分析不同的是，本文方法是在保证目标属性仍然安全的条件下通过泛化当前可达状态，以此来实现状态空间的约简。
　　1.3 对称性约简方法  
　　对称性约简就是利用相似线程间状态变迁相似的特点来简化并行程序状态空间的方法。传统约简方法[16]中将对称性定义为变迁等价类。对称关系则是在程序状态空间上的一个双射关系π，且满足如下约束：即（s，s’）是一个变迁时，当且仅当存在对应的另一个变迁（π（s）， π（s’））。但是该类定义却假设并行线程都是无法区分，这将极大限制了在该定义下的应用范围。基于此，如何将对称关系的约束拓宽至非对称关系的约束也随即成为近期研究的主要方向。相应地，文献[17]提出了近似对称和粗糙对称结定义，继而由文献[18]推广到虚拟对称。虚拟对称就是满足互模拟对称商的最通用的条件。只是互模拟对称商很难获得，而且该类验证的属性也仅只局限于对称属性。文献[19]则提出了“超级结构”，并通过向该结构增加辅助变迁来表达任意对称关系，由此构造保护标记商。但是在验证过程中却要通过频繁地检测是否满足实际对称关系来弥补由于辅助变迁导致的精度缺失。另有，文献[20]又提出了懒惰约简策略，在分析程序前不假设任何对称关系，而在搜索过程中对每个可达状态也只是标记其如何违反了对称关系，主要依据就是：进程的相似度越高，其所获压缩表示的程度将越深。该方法采用了 自顶向下压缩方式，并利用语法相似性来标记进程间对称性，再通过虚拟结点表示构成对称关系的实际状态结点集合，以此建立了约简结构。而当模型检测时，即将虚拟结点转换为实际结点进行分别验证。此外，文献[21]提出了利用克雷格插值技术以自底向上来发掘对称性。具体实现时，由于计算克雷格插值时采用的是后向学习策略，这就在保证合并后状态的同时，又进一步保证了断言的安全性，而且也避免了逐项展开的额外开销。
　　1.4 并行程序干扰分析
　　由共享变量传递的并行干扰是导致并行程序交叠执行下可行踪迹组合爆炸的直接原因，第三类约简方法即是从待验证的目标属性出发，却只分析了与目标属性相关的交叠执行踪迹和可达状态。而并行干扰抽象方法[22-23]则是将交叠执行转化为共享变量读写匹配对的可满足性问题而展开其实现研究的。该方法以有限模型检测为基础、而且以不同并行线程对共享内存的访问为分析目标，在将读系匹配对编码为一阶谓词命题形式后，利用约束求解器（Satisfiability Modulo Theory，SMT）进行了计算，继而又利用关联变量上近似和下近似来控制查询规模，同时也利用上下近似修正规则来指导迭代的下一轮查询，该过程中将基于不动点理论判知该过程收敛至对验证条件的证明或者发现真实反例。研究可知，对于发现并行程序缺陷，该方法可以在精度与效率方面得到良好平衡。
　　2 现有并行程序状态空间约简方法的不足
　　综上论述可知，基于偏序关系的约简方法流程是分析了可能的交叠执行划分，再计算对共享变量的影响。而在共享内存模型下，通过共享变量间数据流关系相较控制流则更易分析共享变量和线程内局部变量的可达状态。但是，该类方法却因在独立踪迹实际可达状态间的关系方面缺乏充足考虑，这就使得即便彼此独立的代表踪迹也仍有可能具有相同的可达状态集合。
　　并行程序模块化验证方法具有迭代分析特点，但在迭代过程会产生虚假踪迹的问题，针对该错误即需进行修正而产生了额外时空开销。这是由于估计状态与实际状态差异及其传播，由此而延迟了对线程内可达状态的修正，致使部分时空开销将无可避免地耗费在对不可行全局交叠执行路径的分析上。
　　在对称性约简方法中，利用插值策略来约简并行线程间对称性的技术拓展了对称性的限制，而且在没有先验知识的条件下，又利用了弱对称关系来实现了并行线程间相似的交叠执行踪迹和状态的有效约简。但是该方法在应用插值蕴含操作时对后续交叠执行情况的要求却过于严格，导致可被蕴含的踪迹相应地出现了延迟，因而产生额外的分析开销。
　基于并行干扰的并行程序状态空间约简方法，因其依赖于有界模型检测，即其输入是执行序列的有限展开，就使得并行干扰抽象是借助下近似策略来截断无限循环类语句，由此导致对验证条件的安全性证明将存在不完备的可能。
　　3 结束语
　　现有的并行程序状态空间约简方法主要从相对独立的视角出发对其中冗余状态或路径进行合并，但由于并行程序特点的不同，实现的代码与分析视角的契合程度并不相同，因此现有方法只能适用于具有一定特点的某一类并行程序。如果能够根据并行程序内部的实际特点而分别采取某几种方法来分析将会克服单一视角的不足，但是如何融合不同视角间不同类型并行信息的表达将是进一步研究的方向。此外，如何将静态分析结果与动态分析观测值相结合来进一步提高搜索效率也是需要深入探讨的研究方向之一。
　　参考文献：
　　[1]GODEFROID P. Partial-Order Methods for the Verification of Concurrent Systems： An Approach to the State-Explosion Problem[M]. Secaucus， NJ， USA： Springer-Verlag New York， Inc.， 1996.
　　//ACM Sigplan Notices. New York： ACM Press， 2005：110-121.
　　[3]GUETA G， FLANAGAN C， YAHAV E， et al. Cartesian partial-order reduction[C]//Proceedings of the 14th International SPIN Conference on Model Checking Software. Berlin， Heidelberg： Springer-Verlag， 2007：95–112.
　　[4]YANG Y， CHEN X， GOPALAKRISHNAN G， et al. Efficient stateful dynamic partial order reduction[C]//Model Checking Software： 15th International SPIN Workshop， Los Angeles， CA， USA， August 10-12， 2008， Proceedings. Berlin： Springer-Verlag， 2008：156：288.
　　
　　[6]ABDULLA P， ARONIS S， JONSSON B， et al. Optimal dynamic partial order reduction[C]//Proceedings of the 41th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages. 2014. New York： ACM， POPL ’14.
　　//Proceedings of the 29th ACM/IEEE international conference on Automated software engineering. ACM， 2014： 175-186.
　　[8]GUPTA A， POPEEA C， RYBALCHENKO A. Threader： a constraint-based verifier for multi-threaded programs[C]//Computer Aided Verification. Berlin： Springer， 2011：412–417.
　　[9] GUPTA A， POPEEA C， RYBALCHENKO A. Predicate abstraction and refinement for verifying multi-threaded programs[C]//ACM SIGPLAN Notices. New York： ACM， 2011：331–344.
　　[10]VAFEIADIS V. RGSep action inference[C]//Verification， Model Checking， and Abstract Interpretation. New York： Springer， 2010：345–361.
　　[11]VAFEIADIS V， PARKINSON M. A marriage of rely/guarantee and separation logic[C]//CONCUR 2007 Concurrency Theory. Berlin： Springer， 2007：256–271.