程序模型检测中的状态散列问题及解决方案

理论计算机科学电子笔记149（2006）51-69www.elsevier.com/locate/entcs程序模型检测Tilman Mehler1德国多特蒙德大学计算机科学系Stefan Edelkamp2德国多特蒙德大学计算机科学系摘要虽然在其他领域的计算是合法的，但状态散列可能成为软件模型检查中最昂贵的操作之一。 原因在于潜在的 程序公开的大型状态描述。在本文中，我们介绍了增量散列大型，动态变化的状态向量，自然出现在程序模型检查器中的软件验证过程中。我们利用的事实，只有一小部分的状态描述改变了一个单一的过渡。 根据前一状态的变化，新状态和可以高效地计算其散列值关键词：模型检测，状态空间搜索，哈希1介绍散列在状态空间搜索中是必不可少的，以避免冗余工作。在许多领域中，例如并发软件系统的模型检查[2]，生成的状态集表现出大量的重复。哈希表的使用提供了一种有效的方法来检测重复的状态，1电邮地址：tilman. cs.uni-dortmund.de2电 子 邮件：stefan. cs.uni-dortmund.de1571-0661 © 2006由Elsevier B. V.出版，CC BY-NC-ND许可下开放获取。doi：10.1016/j.entcs.2005.07.02652T. Mehler，S.Edelkamp/Electronic Notes in Theoretical Computer Science 149（2006）51搜索树的大部分。另一方面，如果相应的域表现出特别大的状态描述，则散列可能成为探索例如，新一代的软件模型检查器，如Java字节码模型检查器JPF [23]就是这种情况。与传统方法不同，JPF不依赖于抽象模型。相反，它为能够执行编程语言的编译代码的虚拟机定制了模型检查算法。通过使用未抽象的状态表示，模型检查器消除了遗漏错误的可能性，其原因被抽象所隐藏。换言之，抽象隐藏了行为。此外，用户将不会浪费时间调查不存在但由于抽象而报告的错误。显然，未抽象的软件模型检查的缺点在于潜在的大的状态描述，因为它们必须存储所有当前分配的内存块的内容这是一个普遍的观察，程序的大多数指令（转换）只改变状态的一小部分。模型检查器通过增量存储新生成的状态来利用这些知识。这是通过折叠压缩[15]或通过存储对前驱状态的组件的向后引用[16]来完成的考虑到在状态的增量存储上花费的大量精力，很少关注哈希码的高效计算。如果状态描述的大小变得很大，散列可以大大减缓探索。作为折衷，散列函数可以仅考虑所有状态分量的子集，并且冒着散列冲突数量增加的如果完整状态存储在哈希表中，则这可能是可接受的在最坏的情况下，可能会有大量具有相同散列值的生成状态，并且与新生成的状态进行比较可能会使探索甚至比使用完整散列函数更慢。更关键的是当使用压缩散列函数（如位状态散列[10]和散列压缩[24，22]）时的情况。它们的使用要求底层函数产生最少的哈希冲突，因为每个冲突都可能导致可能包含错误状态的未探索子树为了最小化冲突的数量，哈希函数必须考虑状态描述的所有组件。增量散列函数提供了两种功能：在大型状态描述上的快速计算和在可能的散列值集合上的良好分布先前的工作[6]考虑静态状态描述，涉及一个恒定大小的单个向量这使得该方法适用于AI探索问题，如解谜，约束满足和行动规划。在本文中，我们的目的是使该方法适用于软件模型检测中的由于非常大的状态空间，T. Mehler，S.Edelkamp/Electronic Notes in Theoretical Computer Science 149（2006）5153适合使用深度优先搜索的变体，如迭代深度优先和IDA* [13]以达到更大的搜索深度。增量哈希对于这种模式特别有效，因为我们只需要记住当前访问状态的全局哈希该值根据搜索算法所采取的状态转换和回溯步骤来更新。本文件的结构如下。在下一节中，我们将介绍程序模型检查，特别是在c++程序环境中的汇编级软件模型检查领域我们介绍了模型检查器StEAM，它使用虚拟机检查C++程序的目标代码级别。在此之后，我们研究了静态状态向量的增量哈希，然后，我们解决了如何增量哈希可以应用于某些类型的结构，并讨论了预期的运行时间相比，非增量的情况下。接下来，我们将这些见解用于散列结构化状态向量。我们提供了实验证据的有效性，我们的方法在我们的模型检查StEAM。最后，我们考虑相关的工作，并得出结论。2程序模型检查自动化验证的一个重要应用-例如模型检查-在于程序检查，因为它们可以帮助检测安全关键程序中的细微错误。抽象早期的程序模型检查方法[8]依赖于抽象模型，这些模型要么是手动构建的，要么是从被调查程序的源代码中生成的作为一个缺点，程序模型可能抽象出错误，或者报告实际程序中不存在的错误。模型检查机器代码新一代程序模型检查器建立在能够解释编译代码的体系结构上，以避免构建抽象模型。所使用的架构包括虚拟机[23，16]和调试器[18]。蒸汽c++程序模型检查器StEAM [17]代表了上述领域中较新的工具之一基于一个虚拟处理器，称为互联网54T. Mehler，S.Edelkamp/Electronic Notes in Theoretical Computer Science 149（2006）51Fig. 1. StEAM中的一个州。C虚拟机（ICVM）3该工具对从C++源代码编译的机器代码执行搜索。当前版本的ICVM已经能够高速运行复杂的程序，包括商业游戏《毁灭战士》。该软件包包括一个编译器，它将传统的c/c++代码转换为ICVM的机器代码编译后的代码以ELF格式存储，这是Linux二进制文件的通用对象文件格式。对于StEAM，虚拟机通过多线程进行了扩展，这使得模型检查并发c++程序也成为可能。StEAM为模型检测软件提供了新的可能性在设计阶段，我们可以检查我们的规格是否满足所需的属性。开发人员可以提供一个用与最终产品相同的编程语言编写的测试实现，而不是使用像SPIN [ 9 ]这样的模型检查器的输入语言编写的模型由于基本概念，原则上对可以由StEAM检查的程序没有语法或语义限制，只要它们是有效的c/c++程序。图1反映了StEAM中状态的组成部分StEAM中的状态基本上由运行线程的堆栈内容和机器寄存器、数据和bss部分以及锁和内存池组成。的3ICVM在ivm.sourceforge.net上作为开源公开提供T. Mehler，S.Edelkamp/Electronic Notes in Theoretical Computer Science 149（2006）5155j=IΣ数据段和BSS段包含程序图1中的描述看起来相当大，人们可以得出结论，由于存储访问状态所需的内存，模型检查机器代码是不可行的。然而，在实践中，一个程序的大多数状态与其直接的前一个状态仅略有对于新生成的状态，内存仅分配给已更改的组件。对于未更改的组件，StEAM仅在前驱状态中存储指向该组件内容的指针[16]。这使得在内存耗尽之前可以探索程序状态空间的大部分由状态大小引起的真正问题在于必须用于散列的e_ort事实上，这是探索过程中最昂贵的部分，如果我们跳过哈希码的计算，每秒生成的状态数量会急剧然而，并发程序的探索表现出大量的重复状态，这使得散列必不可少。本文的目标是设计一个增量哈希方案，即允许基于相应转换所做的更改快速计算状态3哈希静态向量为了清楚起见，我们将首先讨论具有恒定大小的状态向量的增量散列。之后，我们将该方法扩展到像StEAM那样的动态状态本文提出的哈希计算基于Rabin和Karp算法的扩展版本[11]。这里，使用散列计算来加速在文本串S =（s1，.， s n）∈ n，其中k 这样的单个语句只改变与var关联的存储单元的内容。设i∈{1，.，k}是改变的组件的位置。 考虑状态向量v =（v1，...， v n）。类似于根据Rabin和Karp的算法，我们将v的哈希值定义为：n（一）h（v）=vj·|Σ|Jmodqj=1因此，考虑后继vJ=（v1， . ，viJ， . ，vn）offv. WECAN在恒定时间内从h（v）递增地计算散列值h（v，J）Kh（vJ） = vj·|Σ|j−vi·|Σ|i+viJ·|Σ|imodqj=1=h（v）−vi·|Σ|i+ viJ·|Σ|imodq.我们可以将上述情况推广到状态转换更改多个组件的值的情况例如，如果声明多个指令以形成原子区域，则会发生这种情况。原子区域通常用于并发程序中，以防止在密码设I（v，vJ）={i|v i/= v iJ}是修改后的索引的集合，则nh（vJ） =vi·|Σ|i−vi·|Σ|i+viJ·|Σ|imodqi=1=h（v）−i∈I（v，vJ）i∈I（v，vJ）vi·|Σ |I+i∈I（v，vJ）i∈I（v，vJ）viJ·|Σ |imodq.已知选择q作为素数可以在可能的哈希码集合上提供良好的分布[12]。这个属性也被Lehmer生成器[14]用来生成伪随机数。定理3.1计算vJ的哈希值，给定v的哈希值在时间• 时间复杂度为O（i，v，J）;使用O（k）额外空间，其中I（v，v，J）是改变的索引的集合• 时间复杂度为O（k·|Σ|Imax=max（v，vJ）|I（v，vJ）|.上一篇：在第一种情况下，我们存储|Σ|im odq，对于所有1≤i≤k。在第二58T. Mehler，S.Edelkamp/Electronic Notes in Theoretical Computer Science 149（2006）51ImaxΣM2M我们预先计算j∈<$I（v，vJ）−vj| Σ |j+vjJ|Σ |jm odq对于所有可能的跃迁（v，vJ），其中最多有。 k·|Σ|Imax=O（（k·|Σ|我最多有两个。3.1分布一个好的哈希函数应该最小化地址冲突的数量给定一个大小为m的哈希表和序列k1，...，k n个要插入的密钥，我们可以定义X ij= 1，如果h（k i）= h（k j），否则为0。 那么X=i< jX ij是碰撞的总和。假设一个随机散列函数具有均匀分布，我们有E（X）= E.XI j=I j）=1I j=. 1.我们在一个大小为100的向量上对增量哈希的分布进行了经验测试，并将结果与随机生成的m= 10000019（大于1000000的最小素数）和n=1000000的数字进行了比较。对于随机生成的数字，我们得到了48，407次碰撞，而增量哈希则得到了50，304次碰撞，这是一个微不足道的增加。4哈希动态状态向量在上一节中，我们设计了一个静态状态向量的增量哈希方案这并不直接适用于程序模型检查器，因为它们对动态和结构化状态进行操作动态意味着向量的大小可能会改变。例如，程序可以动态地分配新的存储器区域。结构化意味着状态被分成几个子向量，而不是一个大向量。例如，在StEAM中，堆栈、机器、变量部分和锁/内存池构成子向量，它们一起形成全局状态向量。在下文中，我们将上一节中的增量哈希方案扩展为适用于动态和分布式状态。对于动态矢量，可以在任意位置插入分量我们将把动态向量看作是α- bet上的字符串的等价物.在下文中，对于两个向量a和b，a，b表示a和b的级联。例如，对于a=（0，8）和b=（15），我们定义a，b=（0，8，15）。IJIJT. Mehler，S.Edelkamp/Electronic Notes in Theoretical Computer Science 149（2006）5159| |{−}∈−||{∈ {−}|}·i=1i=1我们为上一节中等式1描述的散列函数h定义了四个一般引理引理4.1和4.2与插入有关，引理4.3和4.4与成分的删除有关然后，我们将引理应用于不同类型的数据结构，如堆栈和队列。我们使用|一|来表示向量a的大小。引理4.1对于a，b，c∈f，我们有h（a，b，c） =h（a，c）−h（c）·|Σ||+的|+h（b）·|Σ||+ h（c）·|Σ|一||B|莫德角|b|modq.校样：|一||c|h（a，c） =ai·|Σ|i+ci|Σ|I+|一|modq=h（a） +h（c）·|Σ||莫德角|modq.类似地，我们推断出以下结果。引理4.2对于alla，b，c∈H，我们有h（a，b，c）=（h（a，c）−h（a））·|Σ||+的|+h（a） +h（b）·|Σ||莫德角|modq.接下来，我们需要解决从向量中移除组件的问题。引理4.3和4.4展示了一种递增地计算结果向量的哈希值的方法。引理4.3对于a，b，c∈f，我们有h（a，c）=h（a，b，c）−h（b，c）·|Σ||+的|+h（c）|Σ||莫德角|modq.引理4.4对于所有a，b，c∈ H，我们有h（a，c）=（h（a，b，c）h（a，b））/H |B|+的h（a）mod q.引理4.3和4.4需要取逆矩阵|B|模q由于探索算法经常改变其哈希表的大小，因此q的值，乘法逆的计算必须以有效的方式在运行时执行这可以使用欧几里得算法的扩展版本来实现[21]，用于计算两个自然数a和b的最大公约数（gcd），其中a> b。它计算（d，x，y），其中d是a和b的最大公约数，d=ax+by。已知[2 1]，（Z<$q，modq）构成群当且仅当Z<$q=a1，.，q 1 gcd（a，q）= 1 .如果q是素数，则后者对Zq=1、 . . . . . . 、 Q1.一、 因此，通过计算ExtendedEuclid（a，q），我们得到一个三元组（d，x，y），其中d=gcd（a，q）= 1 =ax+qy。这意味着ax mod q= 1，这意味着x是a的乘法逆。4.1栈和队列如果动态向量表示堆栈或堆栈结构，则仅在开头和结尾添加或删除组件对于所有可能的情况，60T. Mehler，S.Edelkamp/Electronic Notes in Theoretical Computer Science 149（2006）51j=1j=I1{−}[我=我我1我=（我2N我1可以在恒定时间内递增地计算得到的散列地址h（v1， . ，vn，vn+1） =h（v） +vn+1·|Σ|n+1modqh（v1， . ，vn−1） =h（v）−vn·|Σ|nmodqh（v0， . ，vn） =v0·|Σ|+（h（v）·|Σ|）modqh（v， . . . ， v） =h（v）−v1·|Σ|modq=h（v）−vmodq|Σ ||Σ|第一个和第二个等式指的是载体末端的插入和删除第三个和第四个等式，解决了开头的插入和删除。4.2组件插入和取出如果可以在向量的任意位置插入或删除组件，则设向量v =（v1，.，v 1，.v n）be定义为pi（v）=ivj|Σ|jmodq和si（v）=nvj|Σ|我的天对于插入（单个）组件，我们有两种选择，计算前缀或后缀，直到向量中的相应位置（括号中应用的引理）：h（v，..，v，w，v，...，v（4. 1）h（v）−s（v） +w·|Σ|i+1+s（v）·|Σ|莫德奎h（v，..，v，w，v，...，v（4.（二）h（v）−p（v））·|Σ|+w·|Σ|i+1+p（v）模q类似地，对于移除组件，我们有两种选择：h（v，...，v，v，...，v（4. 第三章h（v）−s（v）−visi+1（v）·|Σ|+modq1i−1一期+1n）=i+1i|Σ|（4. 4）h（v）−pi−1（v）−vi·|Σ|我h（v1， . ，vi−1，vi+1， . ，vn）=|+ p i − 1（v）mo d q|+pi−1(v)modq显然，与非增量散列相比，所提出的方法不会改变O（n）的渐近运行时间然而，我们只需要访问mini，n i+ 1个组件，这意味着在最坏的情况下有n/4.3联合作战到目前为止，我们只讨论了任意数量的组件更改其值或插入或删除单个元素的情况。为了完整性，我们还希望涵盖任意数量的值更改以及插入/删除应用于状态向量的情况一种解决方案是应用给定的增量哈希计算，一期+1n）的一期+1n）的T. Mehler，S.Edelkamp/Electronic Notes in Theoretical Computer Science 149（2006）5161[2014-05-23]ΣΣ−{−}联系我们ΣΣk=1对于每组值更改和每次插入/移除元件，连续地创建多个站点然而，我们知道，为了去除动态向量中的一个分量，我们必须在最坏的情况下访问n/2个分量。如果我们必须执行几次这样的计算，增量哈希计算所需的时间将很快超过非增量哈希函数。一个折衷的办法是将向量的所有变化统一到一个sin中-n的角序列，使得vJ=a v1J， . ，vmJb，其中a，b是空序列或a = v1，.，v i是一个前缀，b = v k，. v n是v的子集。然后，Mh（vJ） =h（v）−si+1（v） +sk（v）·|Σ|m+vjJ·|Σ|j+imodqj=1m=（h（v）−pi（v））·|Σ|m+pi（v） +vjJ·|Σ|i+jmodq.j=1这意味着，对于一般情况，我们需要访问mini +m，n i+m个元素，在最坏的情况下，它等于vJ的长度，即m。如果m很小，i或n i也很小，我们可以期待改进-即如果vJ仅在靠近向量一侧的小序列中与v未来我们来看看如何实现O（n）。5哈希结构化状态向量一个结构化的状态向量u可以被看作是级联v1，.，子向量Vi=（Vi，1， . ，vi，ni）forri1、 . . . ，m。因此，v的划分可以自由选择，或者更自然地，它起源于所探索的底层状态空间。例如，计算机程序的状态由静态组件（如全局变量）和动态组件（如程序堆栈和动态分配内存池）组成。5.1线性方法给定子向量的顺序，我们可以单独对每个子向量进行哈希，并将结果整合以返回相同的全局哈希代码，就像我们直接对全局向量进行哈希一样。关于v= v1，...，v m是我h（v）=vi=1j =1i、j·|Σ|i−1nk+jmodq.62T. Mehler，S.Edelkamp/Electronic Notes in Theoretical Computer Science 149（2006）51--将子向量组合成全局哈希码所需的运行时根据状态转换所做的更改而变化。一个程序步骤--不管是一行代码还是一些原子块--通常在所有分配的内存区域的一个小子集内改变值因此，我们可以期望平均运行时间接近最佳情况（一个组件是受约束的），而不是最差情况（所有组件都是受约束的）。线性方法的一个弱点在于当子向量被插入到全局状态向量中或从全局状态向量中移除时的时间复杂度类似于4.2节，最坏情况下的运行时间是O（m），即使是一次插入或删除。如果与仅改变存储器单元的内容的指令相比，（解除）分配存储器区域的指令是不常见的，则该方法仍然有效5.2平衡树方法通过引入一个额外的数据结构，我们可以减少在每种情况下的渐近运行时间为O（logm）。为此目的，我们使用具有m个内部节点的平衡的例如AVL[1]树表示t-每个子向量vi，i∈ {1，.，m}。我们将t中节点N的哈希函数HJ定义如下：如果N是叶子，则HJ（N）= 0。否则，hJ（N）=hJ（N1） +h（v（N））·|Σ||+ h j（N r）·|Σ|N l||v（N）|莫德角|v(N)|modq.这里|N|表示具有根N的子树中的向量的累积长度，并且v（N）代表与N相关联的子向量，而Nl、Nr分别表示N的左子树和右子树。如果R是t的根，则hJ（R）给出与按顺序应用于所有子向量的级联的h相同的散列值图2显示了一组四个向量的例子，其中q = 1， 2， 3，q= 17。树中的节点用它们的hJ值注释，并且计算如下：h（3， 1）= 3· 3+1· 3mod 17 = 18mod 17 = 1h（1， 2）=hJ（N1，1）= 1· 3+2· 9mod 17 = 21mod 17 = 4h（2）=hJ（N2，1）= 2· 3mod 17 = 6mod 17 = 6h（2， 1， 2）= 2· 3+1· 9+2· 27mod 17 = 69mod 17 = 1hJ（N1，2）= h（2）+h（2，1，2）·3|（二）|mod 17 = 6+3 mod17 = 9hJ（R）= 13+9·3|（1、2、3、1）|mod 17 = 13 + 9·81 mod 17 = 11对于h（1，2，3，1，2，2，1，2），我们用线性方法得到同样的结果（即11）当子向量vi中的值改变时，我们必须首先重新计算T. Mehler，S.Edelkamp/Electronic Notes in Theoretical Computer Science 149（2006）5163Maxi=1i=1i=1我Maxi=1我Maxh’=11（3，1）h’=4（一、二）h’=9（二、一、二）h’=6（二）图二、用于计算结构化状态向量的哈希码的示例树h（vi）。然后，结果必须自底向上传播到根节点。由于平衡树的深度在数学上以节点数m为界，所以我们至多遍历O（logm）个节点，直到到达树的根节点此外，插入和删除一个元素在/从平衡树可以在O（logm）的时间通过恢复平衡树结构使用旋转（左或右）。更新执行旋转的两个节点的哈希值集可以在恒定时间内实现。我们在下面的结果中总结了观察结果。定理5.1结构化向量的动态增量哈希vJ=（v1J， . ，vmJ ）关于它的前一个v =（v1，...，（v m）假设组件i中的修改（组件内的更新、插入和删除分量），i ∈ {1，.，m}，其中I（v i，viJ）是索引的集合在c分量i和Ii=max（v，vJ）中变化|I（vi，viJ）|及时提供• O（|I（vi，viJ）|时间复杂度为O（m），时间复杂度为O（m）时间复杂度为O（m + max）• 时间复杂度：O（m+logni）时间复杂度：O（m + log n i）时间复杂度：O（m）时间复杂度O（m+n）|Σ|（Ii ）extras pa ce.• O（|I（vi，viJ）|时间复杂度为O（log m），时间复杂度为O（logm+logni），时间复杂度为O（m）时间复杂度为O（m + max）• 更新的时间复杂度为O（logm），插入的时间复杂度为O（logm +logni），时间复杂度为O（m+n）|Σ|（Ii）extras pa ce.证明：对于线性方法（第一种情况），我们有64T. Mehler，S.Edelkamp/Electronic Notes in Theoretical Computer Science 149（2006）51ΣΣΣk=1·12Mk=1算法的复杂度为O（m+1）Mi=1 ni）。案例）可通过预计算j∈I（v，vJ）（−vi，j|Σ|j+viJ，j|Σ|j）所有人的modq我我n1h（v）=vj=1i、jn2·|Σ|j+vj=12，jnk·|Σ|n1+j+. . . +vj=12个月·|Σ|m−1nk+jmodqm−1=h（v） +h（v）·|Σ|n1+. . . +h（v）·|Σ|kmodq，这样我们就可以减少对静态设置的更新，i−1nk|k =1 mo d q，其中a是经修正的comp one n t。|k=1modqwiththeaffectedcom pone nt. 另外更新这些日期存储的对象集，我们维护一个列表|Σ|njmodq，j∈{1， . ，m}。 对于插入，|必须重新计算NimodQ。|nimodqhastobenewlycomputed. 使用快速扩展，该值可以在时间O（logni）内确定。这两个表总共占用O（m）空间。在最坏的情况下，插入和删除向量分量额外需要O（m）的向量内的重构操作对于平衡树方法（第三种情况），插入和删除在时间O（logm）内可用，而更新日期需要O（|I（vi，viJ）|logm）时间。再一次，对于插入，我们还需要O（log n i）时间来计算|Σ|来自scrat c h的nimodq。由于二叉树消耗的空间li接近，与静态情况一样，改进的扩展因子|I（vi，viJ）|时间复杂度为O（1）可能的转变将Vi改变为ViJ并且i ∈ {1，.，m}。6实验结果我们在StEAM中对堆栈进行了增量散列实验。状态的其余部分仍然是非增量散列的，结果被组合为全局散列值。通过只递增地散列堆栈，我们强调了我们的方法的有效性，因为如果所有组件都用递增的方法散列，我们可以期望更高的运行时间增益对于每个正在运行的线程，程序堆栈以8 MB字节的字节向量给出通过连接n个正在运行的线程的堆栈，我们得到的向量大小为8· 10242n，必须进行散列。 由于可能会生成新的线程，因此向量可以动态增长。我们使用了一个Linux系统，CPU为1.8 GHz，时间限制为30分钟。图3比较了秒，直到发现错误，与非增量和增量散列计算的用餐哲学家，光学电报和领导人选举协议。一个输入O.T. 这意味着在发现错误之前已达到时间限制。所使用的算法是广度优先搜索（BFS）和贪婪最佳优先（GBF）。对于GBF，我们使用了最阻塞启发式算法[16]来加速哲学家和光电报协议中的死锁搜索对于包含断言冲突的leader election协议，我们使用T. Mehler，S.Edelkamp/Electronic Notes in Theoretical Computer Science 149（2006）5165BFSGBFnincIncincInc23456789101617181920253050100114257O.T.O.T.O.T.O.T.O.T.O.T.O.T.O.T.O.T.O.O.T.0125O.T.O.T.O.T.O.T.O.T.O.T.O.T.O.T.O.T.O.TO.T.00011122310131417203765279O.T.000000000011113419239BFSGBFnincIncincInc2O.T. O.T.103O.T. O.T304O.T. O.T.605O.T. O.T.11010O.T. O.T.79611O.T. O.T.105712O.T. O.T.135913O.T. O.T.1701214O.T. O.T.2141515O.T. O.T.2621916O.T. O.T.3162317O.T. O.T.3792718O.T. O.T44832BFSGBFnincIncincInc2345678910111213146263O.T.O.T.O.T.O.T.O.T.O.T.O.T.O.T.O.T.O.T.O.T.033O.T.O.T.O.T.O.T.O.T.O.T.O.T.O.T.O.T.O.T.O.T.015112755112232476936O.T.O.T.O.T.0101349173569244668O.T.图三.使用非增量和增量散列的运行时间（秒），用于用餐哲学家（左），用于光学电报（右）和用于领导者选举协议（下）。更合适的注意，即使对于非增量计算，我们也只需要考虑堆栈的部分，它位于当前堆栈指针之下。堆栈指针上方的所有存储单元都被视为零。结果令人鼓舞，因为与非增量散列相比，我们获得了10倍以上的加速，并且可以在时间限制内发现更多错误在不久的将来，我们的目标是验证更复杂的程序，这将不允许显式存储每个状态。这意味着需要压缩散列方案，例如位状态散列。如前所述，部分哈希不适合哈希压缩，因为哈希冲突的数量很66T. Mehler，S.Edelkamp/Electronic Notes in Theoretical Computer Science 149（2006）517相关工作散列可能成为探索的瓶颈，特别是当应用模式或抽象数据库时[4，5，20]。[ 7 ]中提供了一种在IDA* 中应用增量哈希的探索算法，该算法具有多个抽象数据库和位状态哈希，以及其在AI规划领域的应用。除了应用程序域之外，关于当前贡献的限制是所有状态描述符都是静态的，但是我们希望抽象数据库的增量散列也可以与动态变化的状态向量一起工作独立于我们的研究，Musuvathi和Dill [19]提出了一种相关的哈希方法，该方法解决了显式状态模型检查中的增量堆规范化（HC）。HC服务于获得用于所分配的存储器区域的堆的规范表示（CR）的目的，使得仅在堆对象的地址中不同的状态被检测为重复。Iosif之前提出了一个HC算法，它根据堆中的深度优先顺序连接堆对象作者指出了Iosif算法的两个缺点其次，根据作者的说法，堆中的小变化会导致CR中的大变化-即许多堆对象的位置发生变化。如果使用增量哈希，这可能会导致探索在本文中，增量散列被描述为每个堆对象维护散列单独的值，这些值被组合为整个堆的全局散列值在执行状态转换之后，仅为那些被转换改变或者其在CR中的位置已经改变的对象重新计算散列值。由于大多数转换仅改变所有堆对象的一小部分，因此在CR中维护大多数对象的部分的堆HC是有利的。增量HC解决了Iosif算法的两个缺点。 首先，对象o在CR中的位置通过堆图中的广度优先访问链和o的长度来确定。广度优先访问链被定义为路径边缘上的o集合标签列表。作者设计了一个递归重定位函数，它根据对象的BFS访问链和长度计算对象在CR中的位置。它表明，该函数总是重新定位具有相同的访问链和长度的对象在CR中的相同位置。第二个定理假设，重定位函数为两个等价堆创建相同的CR。该方法在工具CMC和Zing中实现。三个示例程序的实验结果表明，显着加速的探索。T. Mehler，S.Edelkamp/Electronic Notes in Theoretical Computer Science 149（2006）5167关于我们的方法，本文留下了一些悬而未决的问题.一个好的散列函数应该散列整个状态，以尽量减少冲突。只有当哈希冲突导致搜索树中未探索的路径（如果使用压缩哈希方案），或者解决哈希冲突的时间比哈希本身更长时，才是这样。事实上，当状态显式存储在哈希表中时，如果状态仅部分哈希，则探索可以更快一般来说，对于状态转换，不仅可能所有堆对象的一个小子集被改变，而且在这些对象中只有很小的改变提供的哈希函数要求，如果对象的内容发生了变化，则完全重新计算对象的部分哈希这里不使用增量哈希，尽管哈希函数会支持它。如果只有对象在CR中的位置发生了变化，所提出的增量哈希还需要重新计算部分哈希值。通过我们提出的一个适当的哈希函数，这可以在恒定的时间内完成。作者指出，一旦程序的数据结构被初始化，访问链的数量（以及堆的结构）就会这也意味着，在特定的搜索级别之后，堆的CR将不再改变。这种方法很可能会遇到问题的工作程序，不断改变其分配的内存区域集。8结论我们分析了开发有效的状态散列方法所花费的时间，因为在许多显式状态模型检查的领域中-例如在未抽象的软件验证中-状态描述可以变得非常大，并将散列函数变成探索的瓶颈。我们提出了增长/收缩和结构化状态向量的增量散列，并讨论了建立我们的方法的正式描述所需的基本属性它的目标是那些领域，其中ex-banded一个大的状态向量表示，而过渡只改变整个状态的一小部分我们还考虑了如何利用数据结构的属性（如堆栈或队列）来有效地增加哈希函数的计算。对于分布式状态，我们发现最坏情况下的时间插入和删除的子向量的规模与子组件的数量m线性。使用平衡二叉树，我们提出了一种替代方法，运行时对数m。我们先做了一些68T. Mehler，S.Edelkamp/Electronic Notes in Theoretical Computer Science 149（2006）51实验并观察到与非增量散列相比的显著加速。在当前的实现中，我们只对堆栈内容进行递增散列。我们选择栈，因为它们构成了状态描述的一部分，当递增地进行散列时，它们会产生最大的预期运行时间改进：首先，栈的数量随着运行进程的数量而增长（与data-/bss-section和pool相反）。此外，由于技术原因，ICVM将机器寄存器保留在堆栈上。因此，通过散列堆栈，我们也散列机器寄存器。此外，由于测试程序很少使用动态分配的内存，这里堆栈构成了状态描述的最大部分在未来，我们计划为状态描述的所有组件实现一个完整的增量哈希方案，以实现更高的运行时增益。完整的增量哈希计算将与位状态哈希结合使用，以使用StEAM检查更复杂的程序此外，我们将花一些时间考虑是否以及如何将增量散列与状态重建相结合。引用[1] Adelson-Velskii，G. M.和E. M. Landis，An algorithm for t