（计算机科学与技术专业论文）cache一致性协议模型检验的抽象研究.pdf

国防科学技术大学研究生院硕士学位论文 摘要 随着高性能计算机性能的不断提升、规模不断增大，c a c h e 一致性协议变得异 常复杂，协议的状态数随系统规模成指数级增长，导致状态空间爆炸。为了缓解 状态空间爆炸问题对c a c h e 一致性协议模型检验的影响，迫切需要研究模型检验 优化技术。 本文深入剖析了模型检验工具m u r p h i ，介绍了m u r p h i 的语法、模型检验的流 程、执行模式和采用的优化技术。通过对简单协议进行验证，分析并总结出模型 检验中状态数目与状态分量的值域之间的关系，并归纳出m u r p h i 中状态空间分配 规律，找出状态空间爆炸现象出现的原因。 抽象是缓解状态空间爆炸问题的重要技术之一，它借助等价关系将原始模型 映射到一个简化的抽象模型。抽象模型相对于原始模型大大化简，从而减少了模 型检验时需要遍历的状态数目。本文提出了一种基于s m t 求解器的谓词抽象技术。 首先对高级描述语言m u r p h i 进行b d d 建模，将m u r p h i 描述转换成相应的b d d 公式；然后结合给定的谓词，将抽象问题转换成可满足性模型理论问题，并利用 最新的s m t 求解器进行求解；最后利用模型检验工具对抽象模型进行验证。实验 表明，基于s m t 求解器的谓词抽象能够在保证验证结果正确的同时显著减少对状 态空间的需求。 文章对谓词抽象的关键算法进行了分析，采用非递归方式实现下一抽象状态 的计算，提高了谓词抽象的效率。详细分析了经典的c a c h e 一致性协议，给出了 共享读、独占写和数据写回三种处理流程的消息传递规则。对谓词抽象前后的 c a c h e 协议进行模型检验，比较了两种方法在验证时间和空间上的差别。实验结果 表明基于谓词抽象的模型检验能够减少验证所需的状态空间，满足更大规模系统 的验证需求。 主题词：c a c h e 一致性协议，模型检验，状态空间爆炸，谓词抽象，s m t ，b d d 第i 页 国防科学技术大学研究生院硕士学位论文 a b s t r a c t w i t ht h eq u i c ki n c r e a s eo fc o m p u t e r sp e r f o r m a n c ea n dt h er a p i dg r o w t ho fs c a l e ， c a c h ec o h e r e n c ep r o t o c o lb e c o m e sm o r ea n dm o r ec o m p l e x t h en u m b e ro fs t a t e si n c a c h ec o h e r e n c ep r o t o c o lg r o w se x p o n e n t i a l l y ，w h i c hl e a d st os t a t e ss p a c ee x p l o s i o n i no r d e rt or e l a xi t si n f l u e n c et ot h ec a c h ec o h e r e n c ep r o t o c o lv e r i f i c a t i o n , i tc r i e sf o r t h eo p t i m i z a t i o nr e s e a r c ho i lm o d e lc h e c k i n g t b j sp a p e ri n t r o d u c e saf a m o u sm o d e lc h e c k i n gt o o l m u r p h i w ep r e s e n ti t s s y n t a x ，e x e c u t i o nm o d e l ，t h ep r o c e s so fm o d e lc h e c k i n ga n dt e c h n i q u e st or e d u c et h e m e m o r yr e q u i r e m e n t sd u r i n gv e r i f i c a t i o n w eu s em u r p h it oc h e c k t h ev a l i d i t yo fs o m e s i m p l ep r o t o c o l s ，a n a l y z ea n ds u m m a r i z et h ef u n c t i o nr e l a t i o nb e t w e e nt h e s t a t e v a r i a b l e ss t r u c t u r ea n dt h en u m b e ro fs t a t e sw h i c hi n v o l v e di nt h em o d e lc h e c k i n g p r o c e s s a n dw eg e tt h er e a s o na b o u ts t a t es p a c ee x p l o s i o n a b s t r a c ti sa l li m p o r t a n tt e c h n i q u et or e l a xt h es t a t ee x p l o s i o n o na b s t r a c tt h e o r y ， i tg e t so n ea b s t r a c ts y s t e mb ys c i s s o r i n go u t l y i n gv a r i a b l e sf r o mt h ec o n c r e t es y s t e m a n dm a p p i n gac o n c r e t es t a t es e tt oa na b s t r a c ts t a t e b e c a u s et h ea b s t r a c ts y s t e mi s m u c hs i m p l e rt h a nt h ec o n c r e t eo n e t h en u m b e ro fs t a t e si nm o d e lc h e c k i n gi sm u c h s m a l l e r t h i sp a p e rp r e s e n t st h ep r e d i c a t ea b s t r a c t i o nb a s e do ns m t s o l v e r f i r s t l y i t c o n v e r t se a c hp a r to ft h em u r p h ii n t ob d d f o r m u l a s e c o n d l y ，i tc o n v e r t st h ep r e d i c a t e a b s t r a c t i o np r o b l e mi n t ot h es a t i s f i a b i l i t ym o d u l op r o b l e mw h i c hc a nb es o l v e db vs m t s o l v e r l a s t l y ，i tc h e c k st h ev a l i d i t yo ft h ea b s t r a c ts y s t e ma n dc o m p a r e st h er e s u l t sw i t h t 1 1 a tm o d e lc h e c k i n gw i t h o u tp r e d i c a t ea b s t r a c t i o n e x p e r i m e n t a lr e s u l t ss h o wt h a t p r e d i c a t ea b s t r a c t i o nb a s e do ns m ts o l v e rc a l l n o to n l ye n s u r et h ec o r r e c t n e s so f v a l i d i t yc h e c k i n gb u ta l s or e d u c et h es t a t es p a c eg r e a t l y ，w h i c hm a k e si tf i tp r o t o c o l s v a l i d i t yc h e c k i n gi nl a r g e rs c a l e t 1 1 i sp a p e ra n a l y z e st h ee f f i c i e n c yo ft h em o d e lc h e c k i n gb a s e do np r e d i c a t e a b s t r a c t i o n a n di m p r o v e st h eb o t t l e n e c ka r i t h m e t i c i ta l s oa n a l y z e sa nf a m o u sc a c h e c o h e r e n c ep r o t o c o la n dp r e s e n t st h ep r o t o c o lf l o w si n c l u d i n gs h a r e dr e a d ，e x c l u s i v e w r i t ea n dd a t e w r i t e - b a c k l a s t l y ，w ea p p l ym o d e lc h e c k i n gb a s e do np r e d i c a t e a b s t r a c t i o nt oc h e c kt h ev a l i d i t yo fc a c h ec o h e r e n c ep r o t o c o l s ，a n dc o m p a r et h er e s u l t s w i t ht h o s ew i t h o u tp r e d i c a t ea b s t r a c t i o n t h er e s u l t sa r ee n c o u r a g i n g k e yw o r d s ：c a c h ec o h e r e n c ep r o t o c o 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 ， p r e d i c a t ea b s t r a c t 。s a t i s f i a b i l i t ym o d u l ot h e o r i e s ，b i n a r yd e c i s i o nd i a g r a m 第i i 页 国防科学技术大学研究生院硕士学位论文 表目录 表2 1 采用不同编译方式对经典协议进行测试的结果比较1 8 表3 1经典协议谓词抽象前后状态数比较2 8 表3 2 经典协议谓词抽象前后模型检验的一致性比较2 9 表4 1递归实现与非递归实现所用时间比较3 3 表4 2c a c h e 一致性协议的目录项对应的状态3 6 表4 3c a c h e 一致性协议的消息及其含义3 6 表4 4g e r m a n 协议的模型检验测试结果4 4 表4 5 两种模型检验技术对g e r m a n 协议进行验证的结果比较4 5 第l i i 页 国防科学技术大学研究生院硕士学位论文 图1 1 图1 2 图2 1 图2 3 图3 1 图3 2 图3 3 图3 4 图3 5 图3 6 图3 7 图4 1 图4 2 图4 3 图4 4 图4 5 图4 6 图4 7 图4 8 图4 9 图4 1 0 图4 1l 图4 1 2 图4 1 3 图4 1 4 图4 1 5 图4 1 6 图4 1 7 图4 1 8 图4 1 9 图目录 多处理机系统结构。2 模型检验过程示意图5 具有单个变量的状态机l5 三种方式的状态空间分配比较17 谓词抽象算法2 2 原始系统的m u r p h i 描述2 2 原始系统状态机2 3 抽象系统状态机2 3 c v c 3 的结构图2 4 基于s m t 求解器的谓词抽象的过程2 6 基于s m t 求解器的谓词抽象算法2 7 计算下一抽象状态算法递归实现3 0 计算下一抽象状态算法的一种改进3 l 递归和非递归实现f i b o n a c c i ( n ) 3 3 h 函数的非递归实现3 5 h o m e 结点共享读请求状态机3 7 h o m e 结点共享读m u r p h i 实现3 8 本地结点共享读请求的状态机3 8 结点p ( 本地结点) 共享读m u r p h i 实现3 9 h o m e 结点独占写请求状态机4 0 h o m e 结点独占写请求状态机4 0 本地结点独占写请求状态机4 l 本地结点独占写m u r p h i 实现4 l 独占结点数据写回状态机4 2 独占结点数据写回m u r p h i 实现4 2 属性c a c h e s t a t e p r o p 4 3 属性c a c h e d a t a p r o p 4 3 属1 生m e m d a t a p r o p 4 3 g e r m a n 协议要满足的属性之一4 4 g e r m a n 协议的谓词抽象结果4 5 第1 v 页 独创性声明 本人声明所呈交的学位论文是我本人在导师指导下进行的研究工作及取得的研 究成果尽我所知，除了文中特别加以标注和致谢的地方外，论文中不包含其他人已 经发表和撰写过的研究成果，也不包含为获得国防科学技术大学或其它教育机构的学 位或证书而使用过的材料与我一同工作的同志对本研究所做的任何贡献均已在论文 中作了明确的说明并表示谢意 学位论文作者签名：二出暑l 日期：7 年7 2 月7 日 学位论文版权使用授权书 本人完全了解国防科学技术大学有关保留、使用学位论文的规定本人授权国 防科学技术大学可以保留并向国家有关部门或机构送交论文的复印件和电子文档，允 许论文被查阅和借阅；可以将学位论文的全部或部分内容编入有关数据库进行检索， 可以采用影印、缩印或扫描等复制手段保存、汇编学位论文 ( 保密学位论文在解密后适用本授权书) 学位论文题目：垒q 照曼= 熬性边邀搓型拴验数抽鏊盈窒 学位论文作者签名：主蜜坚 作者指导教师签名：幸亟竺丛二 日期：川年i 2 月刃日 日期：m 叶年1 2 - 月2 ，日 国防科学技术大学研究生院硕士学位论文 第一章绪论 随着科学技术的全面发展，人们探索未知的能力和需求不断增强，开发的系 统规模不断增大、需要解决问题的复杂度不断提高，对计算机的处理能力也提出 了更高的要求。为了满足人们日益增长的实际需要，必须不断开发具有更高性能 的高性能计算机。高性能计算机的研制是高性能计算的重要内容，其发展水平是 衡量一个国家综合实力的重要标志。国务院在2 0 0 6 年2 月发布的国家中长期科 学和技术发展规划纲要( 2 0 0 6 2 0 2 0 ) 中指出：“加速发展高性能计算对提高我 国国防建设与国家安全、国家经济建设、国家重点工程和基础科学研究等尖端科 技领域的核心竞争力，具有十分重要的战略意义。 高性能计算机的研制面临很多的问题，2 0 0 8 年发布的高性能计算技术现状 及发展白皮书指出高性能计算机主要存在以下关键问题：内存与f o 墙、功耗墙、 编程墙、复杂度和可靠性墙、扩展性墙等，内存与u o 墙包括内存墙和f o 墙两部 分，其中内存墙是指存储器性能和处理器性能差距越来越大、本地带宽及延迟和 全局带宽及延迟发展不一致所形成的差距影响系统整体性能的提高。c a c h e 一致性 协议是解决高性能计算机中内存墙的一种非常有效的技术，而验证c a c h e 一致性 协议的正确性和有效性尤为重要。 本文的研究围绕验证c a c h e 一致性协议展开，模型检验是验证c a c h e 一致性 协议的种常用方法，但是在验证大规模系统的c a c h e 一致性协议时受状态空间 爆炸问题的限制。作者首先分析了模型检验中状态空间爆炸问题存在的原因，并 试图寻找对模型检验技术进行一定程度上的优化，减少状态空间爆炸问题对模型 检验技术的影响，最后将优化后的模型检验技术应用于c a c h e 一致性协议的验证， 满足更大规模系统c a c h e 一致性协议的验证需求。 1 1 研究背景 1 1 1c a c h e 一致性协议是实现多处理机系统的关键 随着计算机硬件技术的迅速发展，c p u 计算能力不断增强、主频不断提高， 造成了慢速存储器不能匹配高速c p u 处理能力的情况。为了解决处理器和存储器 之间的速度不匹配的问题，人们引入高速缓存c a c h e 技术。c a c h e 是位于c p u 与 主存之间一种容量较小、但速度极高的缓冲存储器。由于c p u 在进行运算时，所 需的指令和数据都是从主存中提取的，因此访存速度对整个系统的性能影响非常 大。引入c a c h e 技术之后，c p u 通过访问c a c h e 获得需要的指令和数据，不必 等待主存数据而保持高速操作。此外，还能够减少处理器对远程结点局部存储器 第1 页 国防科学技术大学研究生院硕士学位论文 的访问，降低对系统带宽的要求。 但是c a c h e 的使用带来了一致性的问题。在多处理机系统中，存在多个处理 单元对同一个c a c h e 块进行操作的情况，如共享读、独占写、失效c a c h e 块等操 作。例如图1 1 所示，当一个c a c h e 块同时在多个处理单元p l ，p 2 ，p i 中有拷贝 时，如果有处理单元p i + l 对该c a c h e 块进行修改，问题就出来了：p 1 ，p 2 ，p i 中 ( i n 1 ) 的一个处理单元再请求读自己缓存中的该c a c h e 块时将发生错误，因为 这时该c a c h e 块已经不是最新的。那么如何保证多个处理单元可以采用共享方式 访问c a c h e 块，并且各个处理单元还能正确的读取到最新数据，这就是c a c h e 一 致性问题。 图1 1多处理机系统结构 c a c h e 一致性协议是实现共享数据访问的一致性、定义处理器对共享主存访问 行为操作的机制。实现c a c h e 一致性的关键是跟踪共享c a c h e 块的状态，目前有 两种不同的共享数据状态跟踪技术：基于总线监听的c a c h e 一致性协议和基于目 录的c a c h e 一致性协议。监听一致性协议是基于监视总线活动并在需要时执行相 应一致性命令的协议，全局存储器以块为单位进行移动，每一块有一个与其相关 的状态，该状态指示该块内容发生的变化。该协议实现简单，但受系统总线带宽 的限制，可扩展性差，处理器数目越大其整体性能越差，因此该协议只适合在小 规模的系统中采用。基于目录的c a c h e 一致性协议将共享c a c h e 块的状态及相关 控制信息保存在目录中，当有处理器请求对共享c a c h e 块进行修改时，只需要根 据目录查找本地处理器有无该c a c h e 块的拷贝并进行相应的作废操作。目录甚至 可以和各个局部存储器分布在系统中，从而对不同目录内容的访问可以在不同的 结点进行。基于目录的c a c h e 一致性协议的可扩展性好，很适合在高速互连网络 连接的大规模系统中使用，是大规模高性能计算机c a c h e 一致性协议的常用实现 第2 页 国防科学技术大学研究生院硕士学位论文 方式。 1 1 2c a c h e 一致性协议验证 c a c h e 一致性协议是实现共享数据访问的一致性、保持共享数据块在若干个局 部c a c h e 和主存储器中一致性、提供共享存储编程接口所采用的处理机制，不仅 直接决定整个系统的正确性，而且对系统的规模和性能有着重要影响，是实现多 处理机系统的关键。在系统研制过程中，必须对c a c h e 一致性协议的正确性和有 效性进行验证。 c a c h e 一致性协议验证先对c a c h e 协议进行建模，然后验证该模型是否满足 给定的属性。c a c h e 一致性协议的验证很长一段时间为人们所忽视，很多协议从提 出到实现的整个过程中，都没有得到完备的验证，主要原因是当时的c a c h e 一致 性协议都是相对简单的基于总线监听的协议，然而随着计算机性能的提高和可扩 展性的增强，c a c h e 协议越来越复杂，人工验证不能确保其正确性，需要借助计算 机对大规模系统中的c a c h e 协议进行验证。 目前c a c h e 一致性协议的验证方法主要有两种：模拟验证和形式化验证【l 】【2 】。 模拟验证通过在系统输入端施加激励，通过观察输出是否与原始设计意图一致来 判断设计的正确性，其特点是简单和有效，但不能确保验证的完备性。形式化验 证借助具有形式语义的符号和工具，明确地表达系统的设计要求，通过给出系统 规范，从数学上完备地证明系统是否实现了设计者的要求，是对模拟验证的重要 补充。 形式化验证一般可分为等价性验证( e q u i v a l e n c ec h e c k i n g ) 、定理证明( t h e o r e m p r o v i n g ) 和模型检验( m o d e lc h e c k i n g ) 。等价性验证的基本思想是建立两个要进 行比较的模型，然后依据数学的定理和公理以及标准单元库判断两个模型之间的 等价性；等价性验证是不需要用户的输入，使用简单，但不能进行功能验证，并 且需要设计一个参考模型并保证参考模型的正确性，在处理大规模集成电路的验 证时存在指数级复杂度。定理证明的原理是将系统及其属性描述成形式化系统的 公式，利用该形式化系统的公理和推导规则，逐步推导出表达属性的公式，借助 定理证明器证明该公式的正确性。定理证明可以处理大规模的设计并且不需要很 大的存储空间，但是不能指出产生错误的原因，而且验证过程需要专家指导，使 用该方法的工作量很大，在实际应用中很少采用这种验证方法，它主要被用来做 一些关键的安全协议验证。模型检验与其它的形式化方法相比，有其自身的优势1 3 】， 例如能快速地进行验证、不需要用户进行手工校验、能够自动诊断出反例、允许 验证和设计同时进行、模型检验中提供的时态逻辑可以很方便的对同步系统中的 性质进行描述。因此人们主要采用模型检验技术对c a c h e 一致性协议进行验证。 第3 页 国防科学技术大学研究生院硕士学位论文 1 2 1 模型检验的发展历程 1 2 模型检验 上世纪8 0 年代初，美国的c l a r k e 等人提出了基于计算树逻辑( c o m p u t a t i o n a l t r e el o g i c ，c t l 1 】【9 1 ) 和有限状态机( f i n i t es t a t em a c h i n e ，f s m ) 的模型检验技术 1 3 】【4 】【5 】，其基本思想是用c t l 公式表达系统的性质，用f s m 表示系统的状态迁移 的抽象系统，然后通过遍历f s m 来验证c t l 的正确性。这时的模型检验算法都是 通过显式地枚举状态空间的可达状态来验证性质，通常所能处理的状态数在几百 万左右。随着程序和系统规模的不断增大，状态数呈指数上升的状况和显式模型 检验有限的处理能力之间存在难以克服的矛盾，这就是状态空间爆炸问题。 19 8 6 年，b r y a n t 将传统的二叉决策图( b i n a r yd e c i s i o nd i a g r a m ，b d d ) 6 j 技术 加以改进，利用b d d 来表示布尔表达式。m c m i l l a n 在1 9 8 7 年将b d d 技术引入 到模型检验中，用b d d 公式来表示系统的状态、迁移规则和系统规范，使得模型 检验中的所有运算都可以通过对b d d 公式进行计算来完成。b d d 的引入取得了 巨大的成功，使模型检验的发展再度复兴。基于b d d 的模型检验称为符号模型检 验【7 】【引( s y m b o l i cm o d e lc h e c k i n g ) 。符号模型检验的基本原理是用一个布尔公式表 示使它满足的所有状态，而这个布尔公式则可以以压缩方式在b d d 中，在遍历过 程中已经标识的状态也用布尔函数的b d d 表示，通过用o b d d ( 有序二叉决策图 o r d e r e db i n a r yd e c i s i o nd i a g r a m ) 来隐式地表示有限状态机的状态和状态之间的 迁移。符号模型检验的优点是能够表示一组而不是单个的状态和状态之间的迁移 关系，因此大幅度减小了空间需求，从而缓解了状态空间爆炸问题。实验表明符 号模型检验方法能处理的状态数达1 0 2 0 量级，进一步改进的算法所能处理的状态 数甚至可以达到1 0 1 2 0 数量级。但是符号模型检验并没有彻底地解决状态空间爆炸 问题，其最大瓶颈仍然是：存储和操作b d d 时对内存要求过大。 由b i e r e ，c i m a t t i 和c l a r k e 等人于1 9 9 9 年提出的定界模型检验( b o u n d e dm o d e l c h e c k i n g ，b m c ) 1 9 】技术是继符号模型检验后的又一重要进展。定界模型检验是基 于s a t ( b o o l e a ns a t i s f i a b i l i t yp r o b l e m ) 的模型检验，主要思想是：首先将状态迁 移关系在初始状态上迭代一定的次数k ，考察系统运行的情况，确定待验证的性质 是否满足。若不能确定性质是否满足，则加大k 的值，重新进行验证。在每一个 检验周期内，定界模型检验问题被转化成s a t 问题，再利用s a t 求解器进行求解。 s a t 问题虽然已证明是n p 完全问题，在实际应用中却很有效。s a t 求解比b d d 求解的优势在于状态空间爆炸问题远没有那么严重。i n t e l 的研究报告显示：在对 p e n t i u m 4 芯片中抽取的典型设计进行验证中，定界模型检验在验证能力和效率上 都比符号模型检验有优势。 第4 页 国防科学技术大学研究生院硕士学位论文 定界模型检验只验证用户给定的属性，验证过程不完备。针对定界模型检验 不完备的缺点，k l m c m i l l a n 于2 0 0 2 年提出了基于s a t 的无界模型检验 ( u n b o u n d e dm o d e lc h e c k i n g ，u m c ) 【l o 】技术。u m c 的基本思想是采用合取范式 表示状态集合及其状态迁移规则，在遍历过程中利用s a t 求解器计算出所有使合 取范式为真的赋值，每求出一组可满足的赋值，就对其进行量化处理，直到最后 得出的合取范式是不可满足的，然后压缩所有解，并利用s a t 求解器求解有限状 态机的不动点。一旦能够确定出不动点，完备性即获得保证，因为不动点对应了 所有可达状态的集合。 1 2 2 模型检验的过程 假设m 表示系统模型，逻辑公式表示有待验证的性质，模型检验就是判定 m 是否满足性质u ( 记为mi _ ) 的过程。在系统建模时，一般使用有穷状态自动 机( f s m ) 描述模型m ，将系统规范描述成c t l 公式的形式。整个模型检验的过 程就是不断的遍历有穷状态机的同时检验c t l 公式的正确性。如果不能验证公式 的正确，系统将给出一个反例，用户可以根据反例找出性质不成立的原因，从而 进一步优化模型，直至构建满足所有给定规范的系统模型。 模型检验的整个过程如图1 2 所示： 图1 2 模型检验过程示意图 完成一 在对系统进行模型检验时，首先需要对系统建模，即对实际系统进行形式化 描述，通常是用k r i p k e 结构描述验证模型。 定义1 1 ( k r i k p e 结构) k r i p k e 结构是一个五元组k = ，其中： 1 、s 是有限状态集合； s 。cs 是初始状态集合； 气) r 冬s xs 是状态迁移关系，即v s s ，了s t s 满足( s ，s 0 r ； 4 ) 彳p 是所有原子命题和它们否定命题的集合； 第5 页 国防科学技术大学研究生院硕士学位论文 5 ) ：s 专2 舻是标记函数，2 艘表示所有4 尸的子集的集合，三将状态s s 映 射到一个原子命题集合，该集合包含在状态s 中为真的所有原子命题。 目前，在模型检验中用于对实际系统进行建模的描述语言很多，例如美国卡 内基梅隆大学开发的m a g i c t l l l 、加州大学伯克利分校设计的b l a s t t l 3 】、斯坦 福大学的d a v i dl d i l l 等开发的m u r p h i 1 5 】等工具采用类c 语言描述，c a d e n c e 和 b e r k e l e y 联合开发的s m v 1 2 1 、美国科罗拉多州立大学开发的v i s t l 4 】系统、意大 利特兰托大学的n u s m v l l 6 】、英国爱丁堡大学和美国北卡罗来纳州立大学相继开发 的c w b t l 刀以及贝尔实验室设计的s p i n t l8 】等工具则采用专门的系统描述语言。 模型检验中的系统规范包括设计者对系统的一些要求和系统必须满足的属性 等，通常采用时序逻辑( 如分支时态逻辑( c o m p u t a t i o nt r e el o g i c ，c t l i n i i9 】) ) 描述。分支时态逻辑是时态逻辑的一种，它是在线性时态逻辑l t l 的基础上引入 分支。c t l 公式包括两部分，路径量词和时态运算符。路径量词有全称量词a ( 对 应所有的路径) 和存在量词e ( 存在某条路径) 两种。c t l 有四种基本的时态运 算符：g ( g l o b a l ) ，x ( n e x t ) ，f ( f u t u r e ) ，u ( u n t i l ) ，各种运算的含义如 下： ( 1 ) g o ：如果公式在一条路径中所有的状态都为真，则g o 对该路径为 真； ( 2 ) x ：如果在某路径的当前状态的下一状态中为真，则x 对该路径 为真； ( 3 ) f ：如果在某路径中的某个状态为真，则f 中对该路径为真； ( 4 ) u1 l r ：如果1 l r 在某路径中的某个状态为真，而中在这个状态之前的所 有状态都为真，则u1 l r 对该路径为真。 c t l 公式的结构归纳定义如下： 定义1 2 ( c t l 公式) ( 1 ) 如果p a p ，则p 是c t l 公式； ( 2 ) 如果厂，g 是c t l 公式，则了、( f vg ) 、a x f 、彤歹、a ( j u g ) 、e ( f u g ) 都是c t l 公式： ( 3 ) 每个c t l 都可以通过有限次使用( 1 ) ，( 2 ) 得到。 1 - 2 3 模型检验的优化技术 在实际的模型检验过程中，常常采用优化技术进一步缩小验证所需的状态空 间，以扩大可验证系统的规模。常用的优化技术有等价和模拟、抽象和精化、对 称【2 0 】【2 1 1 等几种。 第6 页 国防科学技术大学研究生院硕士学位论文 1 ) 等价( e q u i v a l e n c e ) 和模拟( s i m u l a t i o n ) 模型检验中采用等价关系能够建立不同模型之间行为比较的标准。引入等价 关系的目的是对逻辑和结构m ，试图找到一个更小的结构m + ，使得m + 与m 在 逻辑上具有满足相同的公式集合。为了定义结构之间的等价关系，d p a r k 提出 了互模拟等价关系【2 2 1 ，当两个结构互模拟等价时，它们满足相同的c t l 公式集。 有时候互模拟等价关系并不能使模型状态数目得到显著的缩减，通过限制逻辑和 降低两个结构必须满足恰好相同公式集的要求，有可能获得显著的压缩，为此引 入了模拟关系i 矧。模拟和互模拟的区别在于：互模拟保证两个结构有相同的行为， 而模拟使一个结构成为另一个结构的抽象。抽象可以隐藏原结构的部分细节，使 得抽象结构中的状态数目更少。 2 ) 抽象( a b s t r a c t i o n ) 和精化( r e f i n e m e n t ) 抽象是缓解状态空间爆炸问题的一种重要技术。抽象的原理是通过删除不影 响原始模型性质的变量，将原始模型中的数据值集合映射到一个较小的抽象数据 的集合，同时保持与原始模型对应的迁移关系，得到一个简化的抽象模型。验证 工作在抽象模型中进行。如果得到的抽象模型过于简单，以至于无法验证给定的 性质，这就需要重新定义抽象算子，对原始模型进行更加细致的等价划分，然后 在新得到的抽象模型中进行验证，这个过程称为抽象精化。将抽象过程与组合推 理结合，可能得到比较好的效果1 2 4 1 。 3 ) 对称( s y m m e t r y ) 对称技术的主要思想是如果原始模型中存在大量重复的结构，就可以利用这 些结构上的对称来压缩状态空间。实现压缩的基本原理是模型中包含对称就意味 着保持状态标记和迁移关系的非平凡置换群【2 5 】的存在，这样的群在模型状态空间 上定义一个等价关系1 r b i t 关系。这种关系引出的商模型比原始模型更小，而 且与原始模型互模拟等价。因此可以用来验证验证原始模型中的c t l 性质。 1 3c a c h e 一致性协议模型检验研究现状及存在的问题 协议设计正确性的验证问题受到工业界和学术界越来越多的关注，相关课题 的研究集中了世界上最优秀的数学家和计算机科学家，他们广泛分布于世界最著 名的高校、科研机构和公司；在工业界，几乎所有的世界顶尖i t 公司都投入大量 的人力和物力来开发它们的验证和测试工具。以c a c h e 一致性协议为代表的模型 检验成为计算机硬件设计领域非常重要的研究内容。对c a c h e 一致性协议的模型 检验研究始于2 0 世纪九十年代，主要集中在美国几所著名大学和研究所，国内相 关研究相对较少。 上世纪九十年代，u t a h 大学的m p v 研究小组开发的m u r p h i 是一个非常成功 第7 页 国防科学技术大学研究生院硕士学位论文 的显式模型检验系统。m u r p h i 非常适于描述异步并发系统的性质违背、错误语句、 断言违背和死锁等系统规范。m u r p h i 首先由d a v i dl d i l l 开发，随后u t a h 大学开 发了很多的后续版本以支持各种不同的应用，包括支持验证活性的r e lm u r p h i ， 支持磁盘扩展验证的d i s km u r p h i ，支持c a c h e 缓存的c a c h e ，支持概率验murphi 证的m u r p h i ，支持并行验证的m u r p h i 以及可以在6 4 位操作系统上运行并且可以 达到给定精度的m u r p h i 系统等等。m u r p h i 已经成功应用到c a c h e 一致性协议的验 证中，例如h a ls 1 系统的c a c h e 一致性协议【2 6 j 验证，被证明是发现问题的快速 有效的途径；m u r p h i 还被用于斯坦福大学的d a s h 和f l a s h 多机系统的c a c h e 的一致性验证、s u n 公司的s 3 m p 多机系统的链接层协议和c a c h e 一致性协议、 s u n 公司的u l t r a s p a r c 1 系统的c a c h e 一致性协议，均得到较好的效果。 另一个显式模型检验工具s s m ( s y m b o l i cs t a t em o d e l ) 【27 1 ，可以在行为级和 消息传递级验证释放一致性模型下的c a c h e 一致性协议。f o n gp o n g 等人同时采用 m u r p h i 和s s m 在存储一致性模型、c a c h e 一致性协议和实现三个抽象层次上对 s u n 的s 3 m p 系统的存储子系统进行了验证【2 引，提出了模型检验和模拟验证相结 合进行验证的建议。m a r t i n 分析了共享主存多处理机系统的c a c h e 一致性协议实 现对协议形式化验证的影响【2 纠，建议将c a c h e 一致性和m e m o r y 一致性分开，使 协议更多关注数据的一致性，将协议和互联网络实现分开，不依赖于网络的路由 顺序，将有助于降低协议验证过程的复杂度，同时提高协议的可重用性。 此外，m c l a r k 应用符号模型检验工具s 对i e e ef u t u r e b u s + 标准中的c a c h e 一致性协议验证时，发现之前未发现的错误【3 0 1 。n u s m v 同时支持基于b d d 和基 于s a t 两种验证方式，并且引入了启发式策略，在提高求解效率的同时缓解了状 态空间爆炸问题，m c m i l l a n 等人还采用n u s m v 对c a c h e 协议进行形式化验证【3 1 1 。 c h i n g t s u nc h o u 等人在采用循环推理的方式对g e r m a n ，f l a s h 协议化简之后用 模型检验工具对协议的一致性进行了验证【3 2 】。r a j e e vj o s h i 等人采用t l a + 和t l c 验证了c a c h e 一致性协议【3 3 】。u t a h 大学的x i a o f a n gc h e n 采用模型检验工具m u r p h i 对多处理机系统中的多级c a c h e 一致性协议进行验证【3 4 1 。 在国内，也有部分研究单位验证c a c h e 一致性协议的正确性。清华大学的李 崇民等采用模型检验的方法验证了c m p 中c a c h e 一致性协议的正确性【3 5 】：江南计 算机研究所高剑刚等人采用s m v 对基于广播的c a c h e 一致协议进行验证【3 6 】，尹飞 则分别采用了经典模型检验工具m u r p h i 和符号模型检验的典型工具n u s m v 对神 州i v 系统的c a c h e 一致性协议进行形式化验证【3 7 】；中国科学院软件研究所潘宏、 林惠民、吕毅等人利用自行开发的基于一阶逻辑的模型检验工具发现了著名的 c a c h e 一致性协议g e r m a n 2 0 0 4 协议中数据一致性存在的问题【3 8 j 。 状态空间爆炸然仍是阻碍大规模系统c a c h e 一致性模型检验的主要问题。虽 第8 页 国防科学技术大学研究生院硕士学位论文 然人们采用了对称、抽象、分解和其他各种简化方法试图来解决这一问题，但如 果要对大规模的设计进行全面的验证，现有的符号模型检验仍然不能完全胜任。 此外，验证工具本身也存在一些不足之处，例如验证策略比较单一，使得验证效 率低。尽管在给定的硬件条件下，可以对较简单的小规模系统进行验证。但是， 当需要验证的系统达到一定的规模时，其c a c h e 一致性协议异常的复杂，现有的 机器配置就将很难再满足验证的需求。 因此迫切需要从理论上研究新的验证技术，找出现有验证技术的不足，并对 其进行合理的改进，缓解状态空间爆炸问题，提高验证效率。同时对现有验证工 具中验证策略进行分析和改进，提高验证工具的效率。使得在给定硬件配置的验 证平台下能够对更大规模的c a c h e 一致性协议进行验证，进而满足实际系统设计 功能验证的需要。 1 4 本文主要工作 c a c h e 一致性协议模型检验通过遍历状态空间自动地判断一个有限状态系统 是否满足某些属性。由于状态空间大小与系统规模成指数关系，状态空间爆炸问 题严重影响了模型检验的进一步发展与应用，成为大规模c a c h e 一致性协议模型检 验的瓶颈。为了支持多处理机c a c h e 一致性协议的模型检验，我们在模型检验过 程结合抽象技术，剔除原始系统中的冗余信息。抽象的主要思想是将原始模型的 多个状态进行分组，通过状态集合之间的映射得到一个保留了部分原始模型行为、 规模更小的抽象模型，属性验证工作在抽象模型中进行。由于状态空间较小，验 证效率大大提高。本课题研究的正是基于谓词抽象的模型检验。 本文的主要工作如下： 首先剖析了