（计算机软件与理论专业论文）spin状态压缩：基于属性的状态向量优化.pdf

兰州大学硕士学位论文摘要 摘要 模型检测是保证程序正确性的一条重要途径，它最大的优点就是验证过程 完全自动化。然而，模型检测在规模大、复杂度高的系统的应用中却碰到了所 谓状态空间爆炸问题对很多系统来说，其运行过程中所产生的系统状态数 目往往随着系统规模的扩大和及其子模块数目的增加而呈现指数增长。这直接 导致很多系统的规模超出了当前验证工具的能力范围。 s p i n 是贝尔实验室开发的面向分布式软件系统的模型检测器。s p i n 在应 用过程中同样面临状态空间爆炸问题，它采用偏序归约策略来减少状态空间中 需要遍历及存储的状态数目。还有另一种完全不同的策略是减少每个系统状态 所需的存储空间，这属于内存压缩技术的范畴。 本文提出了一种基于s p i n 的无损压缩技术基于属性的状态向量优化 ( s o b p ) ，它利用系统属性的特点，以一个变量替换多个变量的方式对状态 向量进行优化，从而实现状态压缩。而且，当该算法与c o l l a p s ec o m p r e s s i o n 结合使用时，将使c o l l a p s ec o m p r e s s i o n 更加强大，从而进一步减少状态存储空 间。与s p i n 中其它无损压缩算法一样，该压缩算法在实现状态压缩的同时， 也是以增加运行时间作为代价的。 关键词：s p i n 基于属性的状态向量优化( s o b p ) 状态向量状态压缩 d f s ( n d f s ) b f s 逆向推导c o l l a p s ec o m p r e s s i o n 兰州大学硕士学位论文摘要 a b s t r a c t m o d e lc h e c k i n gi sa n i m p o r t a n ta p p r o a c h w h i c h g u a r a n t e e sp r o g r a m c o r r e c t n e s s ，w i t ht h e b e n e f i tt h a ti ti s c o m p l e t e l ya u t o m a t i c h o w e v e r ，i t s a p p l i c a t i o nt oe v e nl a r g e ra n dm o r ec o m p l e xs y s t e m si sl i m i t e db yt h es o c a l l e d s t a t es p a c ee x p l o s i o np r o b l e m ：f o rm a n yt y p e so fs y s t e m s ，t h en u m b e ro fp o s s i b l e s t a t e sd u r i n gs y s t e me x e c u t i o ng r o w se x p o n e n t i a l l yw i t ht h es i z eo ft h es y s t e ma n d t h en u m b e ro fi t sc o m p o n e n tp a r t s t h i sq u i c k l yl e a d st om o d e l sw h o s es i z e e x c e e d st h ec u r r e n tc a p a b i l i t i e so fv e r i f i c a t i o nt o o l s s p i ni sap o p u l a ro p e n s o u r c es o f t w a r et o o lt h a tc a nb eu s e df o rt h ef o r m a l v e r i f i c a t i o no fd i s t r i b u t e ds o f t w a r es y s t e m s s p i na d o p t st h ep a r t i a lo r d e rr e d u c t i o n s t r a t e g yt or e d u c et h en u m b e ro fs y s t e ms t a t e st h a tn e e d st ob ev i s i t e da n ds t o r e di n t h es t a t es p a c et os o l v et h em o d e lc h e c k i n gp r o b l e m a no r t h o g o n a ls t r a t e g yi st o r e d u c et h ea m o u n to fm e m o r yt h a ti sr e q u i r e dt os t o r ee a c hs y s t e ms t a t e t h i si st h e d o m a i no fm e m o r yc o m p r e s s i o nt e c h n i q u e s t h i st h e s i sp r e s e n t sak i n do fl o s s l e s sc o m p r e s s i o nt e c h n i q u ef o rs p i nn a m e d s t a t e v e c t o ro p t i m i z a t i o nb a s e do np r o p e r t y ，o rs o b pf o rs h o r t ，i tm a k e su s eo ft h e c h a r a c t e r i s t i c so fs y s t e mp r o p e r t y ，o p t i m i z e ss t a t e v e c t o rb ys u b s t i t u t i n gt w oo r m o r ev a r i a b l e si n p r o p e r t y w i t ho n ev a r i a b l e ，t h u sa c h i e v e ss t a t e v e c t o r c o m p r e s s i o n m o r e o v e r ，w h e ns o b pc o m b i n e dw i t hc o l l a p s ec o m p r e s s i o n ，i tw i l l m a k ec o l l a p s ec o m p r e s s i o n s t r o n g e r ，c o n s e q u e n t l yr e d u c i n gt h ea m o u n to fm e m o r y f u r t h e r s i m i l a rt oo t h e rl o s s l e s sc o m p r e s s i o nt e c h n i q u e si ns p i n ，s o b pi n c r e a s e s t h er u n - t i m er e q u i r e m e n t sw h i l er e d u c e st h em e m o r y r e q u i r e m e n t so fa ne x h a u s t i v e s e a r c h k e y w o r d s ：s p i n ；s t a t e v e c t o ro p t i m i z a t i o nb a s e do np r o p e r t y ( s o b p ) ； s t a t e - v e c t o r ；s t a t ec o m p r e s s i o n ；d f s ( n d f s ) ；b f s ； c o n t r a r yd e r i v a t i o n ；c o l l a p s ec o m p r e s s i o n 原创性声明 本人郑苇声明：本人所呈交的学位论文，是在导师的指导卜独 立进行研究所取得的成果。学位论文中凡引用她人已经发表域未发 表的成果、数据、观点等，均已明确注明出处。除文中已经注明引 用的内容外，不包含任何其他个人或集体已经发表或撰写过的科研 成果。对本文的磷究成果做出重要贡献韵个人和集体，均已在文中 以明确方式标明。 本声明的法律责任由本人承担。 论文作者签名：鑫期：坦! ：! 关于学位论文使用授权的声明 本人在导师指导下所完成的论文及相关的职务作品，知识产权 归属兰州大学。本人完全了解兰州大学有关保存、使用学位论文的 规定，同意学校保存或向国家有关部门或机构送交论文的纸质版和 电子版，允许论文被查阅和借阅；本人授权兰州大学可以将本学位 论文的全部或部分内容编入有关数据库进行检索，可以采用任何复 制手段保存和汇编本学位论文。本人离校后发表、使用学位论文或 与该论文直接相关的学术论文或成果时，第一署名单位仍然为兰州 大学。 保密论文在解密后应遵守此规定。 、 论文作者签名：二碴导师签名： 蓊庭一一渖一 兰州大学硕士学位论文s p i n 状态压缩：基于属性的状态向量优化 1 引言 1 1 研究背景口1 随着计算机技术及其应用的飞速发展，人们设计的系统日益复杂化，系统 的安全性要求也越来越严格。例如铁路信号、核电站、航空航天、国家安全和 大型通讯系统中的软件都是安全性第一的( s a f e t yc r i t i c a l ) ，任何一点差错将 导致灾难性的后果。因此，保证这些系统在任何情况下的正确性变得至关重要。 保证系统正确性的途径是多方面的。首先对系统的需求分析要全面而准 确，不能有任何实质性的漏洞，以产生正确的系统规范，建立正确的系统规范 的有效方法之一是快速原型法。建立系统准确的模型，进行反复的模拟和仿真 是目前进行硬件设计验证的主要途径。但是模拟只能用典型的情况对系统进行 考察。对系统进行穷尽的模拟是不可能的。在大型系统中，要模拟系统完全的 行为可能要连续运行多年时间，这显然是不实际的。 测试是保证系统正确性的一个手段，对硬件系统的测试是在加工后进行 的；对软件系统的测试是在编码后进行的，但是测试只能证明错误存在而不能 证明错误的不存在。对于复杂的系统，进行穷尽的测试也是不可能的，甚至设 计一个有效的测试方案和评价其故障的覆盖都是相当困难的。 形式化验证是保证设计正确性的另一条重要途径。它用数学方法表达系统 的规范或系统的性质，并且根据数学理论来证明所设计的系统满足系统的规范 或具有所期望的性质。在不能证明所期望的性质时，则可能发现设计错误。在 这一领域，模型检测( m o d e lc h e c k i n g ) 无疑是一种很成功的技术，它最大的 优点就是验证过程完全自动化。然而，模型检测在对规模大、复杂度高的系统 的应用中却碰到了一个棘手的问题状态空间爆炸( s t a t es p a c ee x p l o s i o n ) 。 所谓状态空间爆炸，是指对很多系统来说，其运行过程中所产生的系统状态数 目往往随着系统规模的扩大和及其子模块数目的增加而呈现指数增长。这直接 导致很多系统的规模超出了当前验证工具的能力范围。显然，如何解决状态空 第1 页 兰州大学硕：卜学位论文s p i n 状态压缩：基于属性的状态向量优化 问爆炸问题成了模型检测能否成功的关键所在。 1 2 本文的研究工作 s p i n 是贝尔实验室开发的面向分布式软件系统的模型检测器，它是目前 世界上最优秀的模型检测器之一。s p i n 在应用过程中同样面临状态空间爆炸 问题，它采用偏序归约( p a r t i a lo r d e rr e d u c t i o n ) 策略来减少状态空间中需要遍 历及存储的状态数目。另一种完全不同的策略是减少每个系统状态所需的存储 空间，这属于内存压缩技术的范畴。 s p i n 支持无损压缩和有损压缩：第一种类型的压缩减少穷尽遍历所需的 内存空间，代价是运行时间会变长；第二种类型的压缩是一种近似算法，它只 需要很小的内存，但不能保证穷尽遍历。 s p i n 支持两种无损压缩算法：c o l l a p s e 压缩模式采用分层索引方法来 达到压缩的目的：m a ( m i n i m i z e da u t o m a t o n ) 压缩模式通过建立和更新一个 最小化的有限自动机来存储状态描述符。 本文的工作除了研究s p i n 中的压缩算法外，重点在于提出了一种基于 s p i n 的无损压缩技术：基于属性的状态向量优化。该算法通过分析系统所需 验证的性质的特殊性，以一个变量替换多个变量的方式对状态向量进行优化， 从而实现状态的压缩。与其他无损压缩算法一样，该算法在实现状态压缩的同 时，也是以增加运行时间作为代价的。 1 3 本文的组织结构 本篇论文主要由五个部分构成，后续内容的组织如下：第2 章介绍了s p i n 的基础知识及其模型验证方法，并总结了s p i n 中实现的核心算法。第3 章介 绍了s p i n 中的状态压缩技术，包括无损压缩和有损压缩。第4 章提出了一个 新的无损状态压缩算法，是本文的重点。第5 章，结论与展望。 第2 页 兰州人学硕i 二学位论文s p i n 状态压缩：基于属性的状态向量优化 2s pln 模型检测器瞳1 2 1 概述 s p i n 是一个支持设计及验证异步进程系统( 分布式系统) 的模型检测器 【2 ，3 ，4 ，5 。s p i n 验证模型时注重于保证进程交互的正确性，并试图将异步系 统抽象成尽可能小的串行模型。在s p i n 中进程间的交互可以用多种方式来实 现：用r e n d e z v o u s 原语来描述进程交互、通过b u f f e r e dc h a n n e l s 来传递异步消 息、存取共享变量，或是以上这些方式的任意组合。s p i n 关注于软件系统中 的异步性，而不是硬件系统中的同步时序控制，这使得它有别于其他知名的模 型检测方法，如符号模型检测【6 。 作为形式化验证工具，s p i n 的目标是提供： 1 ) 一套直观的、类似于程序语言的符号来精确地描述系统设计，但不包 含实现的细节， 2 ) 一套强大而简练的符号来表达系统的正确性要求，以及 3 ) 一套能够检测1 ) 描述的模型是否具有逻辑一致性并且满足2 ) 描述的 属性的方法。 目前已经提出了很多形式化语言来解决前两个问题。s p i n 采用p r o m e l a 4 语言来描述系统规范，同时接受以标准的线性时态逻辑( l 1 几) 7 】描述的正 确性要求( 即属性要求) 。 对于无界的系统( u n b o u n d e ds y s t e m s ) 来说目前还没有一个通用的决策系 统( 类似于有限自动机) ，而且没有人能够保证一个无限增长的系统的可靠性。 因而，采用p r o m e l a 语言描述的模型必须是有界的，并且只能包含可数个不同 的行为。这意味着在模型检测器能够解决的问题规模内以及可满足的计算资源 的约束下，所有的正确性要求总是形式化上可决定的。当然，所有要验证的系 统都会有一些由于问题规模所导致的物理限制，如机器内存的大小，用户能够 接受或是能够忍受的运行时间等等。在形式化验证中，这些约束往往是被忽略 第3 页 兰州大学硕二b 学位论文s p i n 状态压缩：基于属性的状态向量优化 的问题。我们通常研究模型检测器本身的限制，并提供一些可靠的策略来解决 那些不能用常规的穷尽遍历的方法所证明的问题。 2 2s pin 的结构 图1s p l n t 奠拟和验证的结构 s p i n 模型检测器的基本结构如图1 所示。典型的工作模式通常从描述并 发系统或是分布式系统的抽象模型开始，一般采用s p i n 的图形化前端x s p i n 。 在修复完语法错误后，通常执行交互式的模拟来初步确定模型是否像我们想象 的那样子工作。然后，也就是第三步，s p i n 将通过模型的p r o m e l a 描述生成 一个优化后的o n t h e f l yv e r i f i e r 。v e r i f i e r 先经过编译，编译时可加上各种类型 的归约算法，然后运行。如果检测到不满足正确性要求的反例，这些错误将反 第4 页 兰州大学硕士学位论文 s p i n 状态压缩：基于属性的状态向量优化 馈给交互式模拟器，用户可重新运行模拟器来跟踪并排除错误。 2 3s p in 的基础 s p i n 最早源于8 0 年代初的基于o n t h e f l y 可达性分析的协议验证系统i s ， 9 ，1 0 1 。这些早期的验证器的目的是提供一些有效的方法来解决那些重要的实 际问题。由于受到所要解决的问题的计算复杂度的限制，这些验证工具只能验 证标准的安全性( s a f e t yp r o p e r t i e s ) 和小范围的活性( 1 i v e n e s s p r o p e r t i e s ) 。 逻辑模型检测技术的研究最早是从c l a r k e 、e m e r s o n ，、s i f a k i s 和q u e i l l e 开始的，他们为新一代的模型检测工具奠定了基础，这些工具能够验证较大规 模的系统。v a r d i 和w o l p e r 扩展了这一工作，他们提出的自动机理论模型成 为了s p i n 系统中时态逻辑模型检测技术的形式化基础。下面总结这一框架。 p r o m e l a 中描述的并发系统由一个或多个用户定义的进程模板组成( 由 p r o c t y p e 关键字定义) ，并且至少有一个进程被实例化。这些模板定义了各种 不同类型的进程的行为。任何运行中的进程可以根据进程模板进一步产生若干 个异步的进程。 s p i n 将每一个进程模板转换成一个自动机。并发系统的全局行为通过计 算异步积自动机( a s y n c h r o n o u si n t e r l e a v i n gp r o d u c to fa u t o m a t a ) 得到，每个自 动机对应一个异步的进程行为。而得到的全局系统行为本身也被表示为一个自 动机。这一异步积自动机通常就是指系统的状态空间，而且因为它可以很容易 地被描述为一个图，所以也常被称为全局状态图。 执行验证之前，s p i n 将正确性要求描述为一个时态逻辑公式，并将公式 转化成一个b i i c h i 自动机，然后计算出这属性自动机与表示全局状态空间的自 动机的同步积，结果仍然是一个b i i c h i 自动机。如果这个自动机接受的语言为 空，则晚明给定的系统不满足初始的属性要求。若不为空，则它精确的包含了 那些满足初始时态逻辑公式的行为。在s p i n 中，我们使用正确性声明和时态 逻辑公式来形式化描述系统错误的行为，例如不想要的行为。验证的过程要么 证明这样的行为是不可能发生的，要么给出匹配这一行为的详细的例子。 第5 页 兰州大学硕士学位论文s p i n 状态压缩：基于属性的状态向量优化 在最坏的情况下，全局可达状态图的大小是所有组件系统的笛卡尔积。建 模语言p r o m e l a 规定了每个组件必须是有限( 界) 的，具体来说，每个进程只 能有有限个控制状态，所有的局部变量和全局变量只能使用有限个不同的值， 所有的消息通道( m e s s a g ec h a n n e l ) 都由用户定义有界的容量。然而，实际上 全局可达图的大小从来不会出现最坏的情况，因为笛卡尔积的一部分很容易被 阻止作进一步的穷尽扩展和构造，很多内存管理技术已经被研究出来以解决这 一问题。下面有单独的一节来讲述s p i n 中实现的这一种技术。 2 3 1 时态逻辑属性 s p i n 接受由线性时态逻辑( l t l ) 表达的正确性属性。m 公式能够表 示安全性以及活性。一个u 1 l 公式f 可以包含若干小写的命题符号p ，并用一 元或二元运算符、布尔与或运算符、时态运算符将它们连接起来，使用的语 法如图2 所示。 图2l t l 语法 例如，l t l 属性 】o uq ) 表示p 始终为真直到q 变为真。类似的，口( ，p ) 第6 页 兰州大学硕士学位论文s p i n 状态压缩：基于属性的状态向量优化 表示不管在运行的任何时候p 最终将变为真且至少一次。 v a r d i 和w o l p e r 在1 9 8 3 年表示，任何l t l 公式都可以转换为一个b c l c h i 自动机 1 1 。s p i n 采用简单的o n t h e - f l y 构造技术自动地将l t l 公式转换为 b f i c h i 自动$ j l 1 2 。这一形式化后得到的自动机只接受那些满足对应的u l 公 式的系统运行。 正如前面提到的，我们利用正确性要求来形式化那些不该发生的系统行 为，即潜在的不满足正确性要求的行为。当然，任何“肯定的”u 1 l 公式可以 变成“否定的”，反之亦然，只需在公式前面加上一个逻辑否定运算符。 一个“肯定的”属性声明要求我们证明系统的语言( 即系统的行为) 包含 在属性的语言中。一个“否定的”属性声明则刚好相反，它要求我们证明系统 语言与属性语言的交集为空。该语言交集的状态空间的大小，最大为自动机表 示的系统和属性的笛卡尔积的大小，最小为它们的和的大小。最坏情况下证明 语言交集为空的状态空间大小仍然为系统与属性的笛卡尔积，但是，在最好的 情况下是零。注意，如果系统中没有属性声明表示的非法行为的部分，那么交 集包含零个状态。因而，s p i n 采用“否定的”正确性声明，并通过语言的交 集来解决验证问题。 一个b f i c h i 自动机接受一次系统的运行当且仅当运行强制使它无限经常 地一次或多次通过它的接受状态。我们把这种行为叫做a c c e p t a n c ec y c l e s 。( 注 意，一个有限系统上的无限运行必然是循环的。) 为了证明系统没有运行序列 满足“否定的”正确性声明，只需证明系统与b f i c h i 自动机表示的声明的联 合运行中不出现a c c e p t a n c ec y c l e s 。这一联合运行在形式化上是由系统与声明 的同步自动机定义的。 整个计算过程，从多个独立运行的并发组件和b f i c h i 自动机表示的正确性 声明开始，在s p i n 中只需一个程序即可完成，即嵌套的深度优先遍历算法 ( n e s t e dd e p t h f i r s ts e a r c ha l g o r i t h m ) 3 ，1 3 ，1 4 。算法在遇到a c c e p t a n c ec y c l e 时终止( 此时会产生违反正确性声明的一个反例) ，或者，在还没有发现反例 时，整个积自动机已经计算完毕。 第7 页 兰州大学硕士学位论文s p i n 状态压缩：基于属性的状态向量优化 2 4 核心算法 s p i n 的验证过程是基于一个优化后的深度优先遍历算法。我们在下面几 节来讨论用来优化这一搜索过程的核心算法。 2 4 1 嵌套的深度优先遍历( n d f s ) s p i n 中的环( c y c l e ) 发现算法可以说具有核心的重要性。它必须与各种 验证模式相兼容，包括e x h a u s t i v es e a r c h ，b i t s t a t eh a s h i n g ，p a r t i a lo r d e rr e d u c t i o n t e c h n i q u e s 。 在一个图中发现环的最经典算法是t a r j a n 的深度优先遍历算法【1 5 ，它通 过在每个可达状态上添加两个整数( t h ed 居n u m b e ra n dt h el o w l i n k n u m b e r ) ， 可以在线性时问内构造出一个强连通图。由于s p 矾生成的状态空间可能包含 数十亿个状态，那么每个整数至少需要3 2 位的存储空间。 如果可达状态图中的强连通图包含至少一个接受状态，则一个可达的 a c c e p t a n c ec y c l e 必然存在。t a r j a n 的算法依赖于整数( t h e 码詹- n u m b e ra n dt h e l o w l i n k n u m b e r ) 的精确性，而且与s p i n 中的b i t s t a t eh a s h i n gt e c h n i q u e s 并不 兼容。后来出现了另外一些有效的算法 4 ，1 3 ，1 6 】，使用这些算法，在执行嵌 套的深度优先遍历算法的时候可能会访问每个状态两次，但是每个状态只存储 一次。这种情况下，使用一种简单的编码方法【1 7 】就可实现嵌套的深度优先遍 历算法，且每个状态只需附加2b i t s 的开销，而不是t a r j a n 算法的6 4 b i t s 。 嵌套的深度优先遍历算法的原理如下所示。若在可达状态图中存在一个 a c c e p t a n c ec y c l e ，那么至少有一个接受状态必须从系统初始状态可达( 即状态 图的根) 且从自身可达。第一次深度优先遍历确定哪些接受状态从初始状态可 达。第二次( 嵌套的) 深度优先遍历从每个检测到的可达的接受状态开始，检 测该状态是否也从自身可达。如果从自身可达，那么一个包含a c c e p t a n c ec y c l e 的完整的运行序列就被构造出来：也就是两次深度优先遍历中所用到的栈的内 容的串联。对s p i n 模型检测器而言，这一运行序列就等同于用户定义的正确 第8 页 兰州大学硕士学位论文s p i n 状态压缩：基于属性的状态向量优化 性声明的反例，并且它可以被打印出来以证明指定的系统并不满足用户的正确 性声明。 嵌套的深度优先遍历算法并不能检测到可达状态图中所有的a c c e p t a n c e c y c l e 。然而，当存在一个以上的a c c e p t a n c ec y c l e 时，它至少能检测到一个【1 6 a 因为s p i n 中a c c e p t a n c ec y c l e 用来构造正确性声明的反例，能够确定它们存在 或不存在就已经能够满足验证的目的了。 使用c h o u e k a 的f l a g 构造算法【1 6 ，1 8 ，s p i n 中嵌套的深度优先遍历算法 便可扩展至满足一个可选的w e a kf a i r n e s sc o n s t r a i n t 的要求。在该w e a kf a i m e s s c o n s t r a i n t 下可以保证，每个包括一个以上在无限长的时间里保持e n a b l e d 状态 的转换( t r a n s i t i o n ) 的进程，必然可以在有限的时间内运行那个转换。 2 4 2 偏序规约( p a r t i a io r d e rr e d u c t i o n ) s p i n 使用偏序规约算法 1 9 ，2 0 ，2 1 来减少在验证过程中所需遍历及存储 的可达状态数目。该规约算法基于以下的观察：判断系统是否满足一个u 工 公式通常对深度优先遍历过程中并发事件的交叉执行的顺序并不敏感。因而， 在验证过程中并不需要生成包含所有运行序列的穷尽的状态空间，验证器可以 生成一个更小的状态空间，只需包含那些能够代表一类运行的序列，因为同属 一类的运行序列相对于给定的正确性属性而言没有什么区别。这一归约算法的 实现基于 1 4 】中描述的静态归约技术，即在实际的验证开始之前，先判断出偏 序归约技术可以被安全应用到验证过程中的一些情况。这一静态归约方法避免 了过去在验证过程中应用复杂的偏序归约技术造成的时间开销。 图3 描述了s p i n 在验证l e a d e re l e c t i o np r o t o c o l 【2 2 】( 参见附录) 时所产 生的可达状态数目的情况。它说明了偏序归约算法在最好情况下的性能，当协 议中进程的数量增加时系统状态的指数增长可降低至线性增长。在更多典型的 情况下，状态空间大小和内存需求的归约与模型的大小呈线性关系，从而可以 减少1 0 到9 0 的时间和空间需求 1 4 1 。 第9 页 兰州大学硕= i ：学位论文s p i n 状态压缩：基于属性的状态向量优化 可达状态数 l234567 问题规模( 进程数) 图3 偏序规约的效果 s p i n 中静态归约技术的一个重要特性是：相对于穷尽的搜索，它不会显 著地增加内存的需求。另外，该归约方法对于进程或是变量的顺序是不敏感的。 另一个基于二叉判定图的归约方法已被证明缺乏这两个重要的特性【2 3 。 归约算法本身的正确性( 保证安全性与活性) 已经单独地被定理证明器 h o l 【2 4 所验证。 第1 0 页 m， 一 一 删 ， 一 1 s ， 一 一 m m m m m m 兰州大学硕：b 学位论文 s p i n 状态压缩：基于属性的状态向量优化 3s pin 中的状态压缩技术 3 1 无损压缩 3 1 1c o ii a p s ec o m p r e s s i o n 3 2 5 1 乍一看，让我们感到很困惑的是模型检测器在验证( 搜索) 过程中产生的 系统状态数目会增长得如此迅速、如此庞大，尽管实际上每个进程只能产生很 少的状态，每个数据对象也只能存取少数的值。其实，系统可达状态数目的爆 炸仅仅是由于各个系统组件( 如进程和数据对象) 产生的局部状态之间往往可 以有相对庞大的组合方式。而且，在每个全局系统状态中复制一份组成全局状 态的各个组件的完整描述是一种潜在的浪费，尽管这样执行起来可能会很有 效。 s p i n 中的c o l l a p s ec o m p r e s s i o n 算法正是观察到了这一点，它把组成系统 状态的各个组件单独存储，并为每个组件分配一个唯一的索引号，将这些组件 的索引号码组合起来便可组成全局状态描述符。 将一个全局系统状态精确地分解成各个单独的组件可以有很多种方式，理 想的分解应该使组件之间的相关性尽可能的小。s p i n 的组件分配方式如图4 所示。 g l ：匿巫亟匦二 队匡亘堕二 雎匡互匦二二 s v ： 回 全局状态描述符( 状态向量) 图4c 0 1 l a p s ec o m p r e s s i o n 的状态组件 第1 1 页 兰州大学硕士学位论文s p i n 状态压缩：基于属性的状态向量优化 第一个组件是由模型中所有全局数据对象组成的，包括消息通道的内 容，不管它们被声明为局部的或是全局的。这一组件同时还有一个长 度域来记录压缩之前的状态向量的初始长度。 接下来，每个活动的进程都对应一个组件，它记录着进程的控制状态， 及所有局部变量的状态，但不包括局部消息通道的内容。 因为各个组件的状态数目是事先不知道的，算法就应该能够对索引号所需 的存储位数做出相应的调整。在s p i n 的实现中，c o l l a p s ec o m p r e s s i o n 为每个 索引号提供了4 个字节的空间，这样最多可以有2 3 2 个独立的组件状态。索引 长度表存储在全局变量组件中。全局变量组件本身的索引长度则存储在压缩后 的状态描述符的一个单独的字节中。为了不发生匹配错误，每个独立组件的长 度也和组件数据一样都被存储起来。 启用c o l l a p s ec o m p r e s s i o n 的方法是在对s p i n 生成的验证器( v e r i f i e r ) 源 码进行编译时附加一个运行时参数d c o u a p s e ，例如： $ s p i n am o d e l sc c d c o l l a p s e op a np a n c s p a n 除了运行时间可能会增加、内存需求会减少以外，验证器的输出结果应浚 没有其它的变化。 。为了看到c o l l a p s e 算法的效果，我们考虑标准的s p i n 发行包中自带的一 个例子：l e a d e re l e c t i o np r o t o c o l 。我们将进程的数量设置为7 个( 发行包中默 认为5 个) ，同时不采用偏序规约算法以增加状态空间的大小，这样可以得到 更有趣的结果，我们可以这样做： $ s p i n - al e a d e r sg c c d n o r e d u c e d m e m l i m = 1 2 8 一op a np a n c $ t i m e p a n ( s p i nv e r s i o n4 2 0 一一2 7j u n e2 0 0 4 ) f u l ls t a t e s p a c es e a r c hf o r ： n e v e rc l a i m 一( n o n es p e c i f i e d ) 第1 2 页 兰州大学硕= 学位论文s p i n 状态压缩：基于属性的状态向量优化 a s s e r t i o nv i o l a t i o n s + a c c e p t a n c ec y c l e s一( n o ts e l e c t e d ) i n v a l i de e ds t a t e s + s t a t e - v e c t o r2 0 0b y t e d e p t hr e a c h e d1 0 8 ，e r r o r s ：0 1 5 7 7 9s t a t e s ，s t o r e d 4 2 4 0 2s t a r e s m a r c h e d 5 8 1 8 1t r a n s i t i o n s ( = s t o r e d + m a t c h e d ) 1 2a t o m i cs t e p s h a s hc o n f l i c t s ：8 6 0 ( r e s o l v e d ) s t a t s 3 2 8 2 2 9 6 5 1 0 4 9 0 3 2 0 4 2 3 6 o nm e m o r yu s a g e ( i nm e g a b y t e s ) ： e q u i v a l e n tm e m o r yu s a g ef o rs t a t e s ( s t o r e d o ( s t a t e - v e c t o r + o v e r h e a d ) ) a c t u a lm e m o r yu s a g ef o rs t a t e s ( c o m p r e s s i o n ：9 0 3 5 ) s t a t e - v e c t o ra ss t o r e d = 1 8 0byte+8b y t eo v e r h e a d m e m o r yu s e df o rh a s ht a b l e ( 一w 1 8 ) m e m o r yu s e df o rd f ss t a c k ( 一m 1 0 0 0 0 ) t o t a la c t u a lm e m o r yu s a g e u n r e a c h e di np r o c t y p en o d e l i n e5 3 s t a t e2 8 ”o u t i t w o ，n r “ ( 1o f4 9s t a t e s ) u n r e a c h e di np r o c t y p e ：i n i t ： ( 0o fi is t a t e s ) r e a lo m 2 7 3 0 s u s e ro m o 3 0 0 s s y s o m o 0 7 0 s 在c p u 为1 7g h z 的p c 上运行，搜索过程花费了2 7 3 0s ，同时消耗了 4 2 3 6 m b y t e s 内存。在输出结果中还打印出了“e q u i v a l e n t m e m o r yu s a g e ”，它是 将存储的状态数乘以每个状态描述符的大小，再加上哈希查找表的开销计算得 到的。默认的搜索会比这次效果好一些，因为在状态描述符被存储之前可以采 用一些简单的字节掩码技术来去除状态向量中一部分冗余的信息。 下面，我们调整一下编译时的参数，同时也启用c o l l a p s ec o m p r e s s i o n 算法， 执行的结果如下： 第1 3 页 兰型查兰堡主兰些堡兰 ! ! ! ! 鉴查堡塑! 苎三旦堡竺鉴查塑里垡些 ss p i n - al e a d e r sg c c d n o r e d u c e d m e m l i m = 1 2 8 一d c o l l a p s e 。op a np a n c $ t i m e p a n ( s p i nv e r s i o n4 2 0 一2 7j u n e2 0 0 4 l + c o m p r e 8 s i o n f u l ls t a t e s p a c es e a r c hf o r ： n e v e rc l a i m一( n o n es p e c i f i e d ) a b 8 e r t i o nv i o l a t i o n s + a c c e p t a n c ec y c l e s 一( n o ts e l e c t e d ) i n v a l l de n ds t a t e s + s t a t e v e c t o r2 0 0b y t e d e p t hr e a c h e d1 0 8 ，e r r o r s ：0 1 5 7 7 9s t a r e s s t o r e d 4 2 4 0 2s t a t e s m a t c h e d 5 8 1 8 1t r a n s i t i o n s ( = s t o r e d + m a t c h e d ) 1 2a t o m i cs t e p s h a s hc o n f l i c t s ：9 5 1 ( r e s o l v e d ) s t a t s 3 3 4 5 0 7 1 1 o nm e m o r yu s a g e ( i nm e g a b y t e s ) ： e q u i v a l e n tm e m o r yu s a g ef o rs t a t e s ( s t o r e d ls t a t e v e c t o r + o v e r h e a d ) ) a c t u a lm e m o r yu s a g ef o rs t a t e s ( c o m p r e s s i o n ：2 1 2 5 ) s t a t e v e c t o ra ss t o r e d = 3 3byte+12b y t eo v e r h e a d 1 0 4 9m e m o r yu s e df o rh a s ht a b l e ( 一w 1 8 ) 0 3 2 0m e m o r yu s e df o rd f ss t a c k ( 一m 1 0 0 0 0 ) 1 9 8 3t o t a la c t u a lm e m o r yu s a g e n r o ft e m p l a t e s ：【g l o b a l sc h a n sp r o c s1 c o l l a p s ec o u n t s ；【3 1 89 32 】 u n r e a c h e di np r o c t y p en o d e l l n e5 3 ，s t a t e2 8 ”o u t l t w o ，n r ” ( 1o f4 9s t a t e s ) u n r e a c h e di np r o c t y p e ：i n i t ： ( 0o f1 1s t a t e s ) r e a l o m 2 9 8 8 s u s e r0 m 0 3 7 0 s s y s o m o 0 5 0 s 正如预料的那样，我们得到了相同的状态数，但是这次搜索花赞了2 9 8 8s 而内存降至1 9 8 3 m b y t e s 。c o l l a p s e 算法在这种情况下表z z 限好。 第1 4 页 兰州大学硕= b 学位论文s p i n 状态压缩：基于届性的状态向量优化 在输出结果中，一些附加的统计信息被打印出来，告诉我们在搜索过程中 各种类型的组件分别发现了多少个。组件在这个列表中被叫做t e m p l a t e s ，各个 类型的组件( 全局变量，消息通道，进程) 在哈希查找表中的“入口”数在这 里分别是：3 1 8 ，9 3 ，2 。 尽管压缩的效果看起来让人印象深刻，但是如果我们重新验证这个例子并 启用偏序规约算法时，状态空间的大小减少至仅9 7 个状态，运行时间减至 2 2 5 2s ，内存需求为1 5 7 3m b y t e s 。显然，状态压缩并不是偏序规约算法的替 代，但它们可以很有效地结合起来使用。 3 1 2m in i m i z e da u t o m a t o nr e p r e s e n t a t i o n 3 2 6 3 s p i n 支持的第二种无损压缩方法是m i n i m i z e da u t o m a t o n ，它不是将系统 可达状态存储在传统的哈希查找表中，而是将它们存储在一个最小化的确定性 有限状态自动机中，并通过建立和维护这个最小自动机来匹配状态。这个自动 机可以表示成一个有限图，在搜索过程中每遇到一个状