（计算机软件与理论专业论文）低级并行代码中几种同步机制的验证.pdf

中国科学技术大学博士学位论文 摘要 摘要 多核多处理器等以共享存储为特征的新一代系统结构的出现，加速了对快速 研发基于共享资源的并行软件的需求，这给基于共享资源的高可信并行软件构造 带来许多挑战性研究课题。在基于共享资源的并行软件构造中，线程间的交互和 通信主要通过访问共享资源来实现，对共享资源访问的同步控制是保证并行程序 正确执行的关键所在。 目前用于共享变量的访问控制的同步机制主要有锁和事务内存两种。传统的 同步机制通过锁保护的临界区来管理并行程序中的共享资源的并发存取，使用锁 的方式不仅限制了程序在多核处理器上的执行效率，而且容易出现死锁等导致程 序进入异常执行状态的隐患。读写锁和可重入锁是锁同步机制的优化实现，其中 读写锁允许多个线程对共享数据进行并发只读访问，而可重入锁则通过允许线程 再次获得所持有的锁来避免自死锁。事务内存是近年来为发挥多核多处理等系统 结构的优势而开展的新型同步技术研究，它试图通过允许一组存取共享内存的指 令( 称为事务) 原子且隔离地执行来简化并行编程。 本课题小组的研究方向是验证使用多种同步机制的并行程序正确性，本论文 则重点关注如何验证使用读写锁和可重入锁这两种同步机制的低级并行代码的 正确性，并探讨同时使用锁和事务内存混合同步机制的并行程序的形式化验证方 法。已有的形式化验证框架及程序逻辑在推理使用锁的并行程序的正确性时，多 数只考虑语义简单的不可重入互斥锁，而不考虑读写锁和可重入锁，这些优化同 步机制无疑可以提高并行程序的性能和易编程性，但由于其语义复杂，导致现有 逻辑系统不能直接应用于推理它们。另外，锁和事务内存同步机制都有各自的优 缺点，未来高性能并行软件可能需要同时使用它们而获得最大的性能收益，相应 的高可信软件则要求设计程序逻辑保证同时使用它们的并行程序的正确性，而设 计一种同时反映锁和事务内存同步机制特征的中间语言是推理混合同步机制的 前提，而目前很少有研究工作考虑同时支持锁和事务内存同步机制的编程语言和 程序逻辑的设计。 针对锁和事务内存同步机制的研究现状以及已有程序验证方面的成果，本文 的主要工作分为以下两个方面： 一方面，在汇编语言级通过扩展邵中教授等提出的并发的经过证明的汇编编 中国科学技术大学博士学位论文 摘要 程( c c a p ) 验证框架，设计支持使用读写锁和可重入锁同步机制的并行程序正 确性验证的h o a r e格专用程序逻辑，达到构造携带基础证明的程序( f p c c ) 的 目标。我们选择模块性较好且适合于推理互斥临界区的并发分离逻辑作为所提出 的验证框架的基础逻辑，并针对其在推理验证读写锁和可重入锁时的局限性分别 进行了如下扩展： 通过扩展并发分离逻辑来支持以读写锁为基本同步原语的并行程序的推理， 将并发分离逻辑中的分离扩展为“强分离”和“弱分离刀两类，利用表示资 源不相交的强分离描述写写和读写线程间对共享资源的划分，利用允许资 源相交的弱分离描述读一读线程间对共享资源的划分，从而弥补并发分离逻 辑中要求共享资源在多个并行线程间进行不相交的划分的不足。 在并发分离逻辑的基础上设计一种推理规则同时支持推理线程首次获得锁 和再次获得锁的情况，避免资源被线程重复获得，从而使得并发分离逻辑 能正确推理使用可重入锁的并行程序。 我们用c o q 定理证明辅助工具实现了所提出的验证框架及其可靠性证明，从而将 验证框架中的验证推理系统从受信任计算基础中排除出去，使得本文的验证框架 具有更高的可靠性。 另一方面，提出一种新颖的语言构造“r e v c 一用于描述与事务内存实现特 点密切相关的可逆代码块，得到一种中间语言将锁和事务融合在一个统一的编程 模型中，并讨论了验证可逆代码块的困难及方法，为进一步深入研究可逆代码块 的推理验证打下基础。通过实例说明该语法结构的表达能力，并阐述能安全执行 的可逆代码块应该满足的基本安全属性 关键词：并行程序验证，读写锁，可重入锁，汇编语言，事务内存同步机制，并发 分离逻辑。 中国科学技术大学博士学位论文英文摘要 a b s t r a c t 。i h ea d v e n to fm u l t i - c o r ep r o c e s s o r sc h a r a c t e r i z e db ys h a r e dm e m o r ya c c e l e r - a r e st h er e q u i r e m e u to nf l e e t l yd e v e l o p i n gs h a r e d - r e s o u r c e - b a s e dp a r a l l e ls o f t w a r e i tb r i n g so u tm a n y c h a l l e n g i n gr e s e a r c ht o p i c so nb u i l d i n gh i g hc o n f i d e n t i a lp a r a l l e l s o f t w a r e s i nt h ep r o c e s so fb u i l d i n gp a r a l l e ls o f t w a r e s ，t h et h r e a d sm a k ei n t e r a c - t i o na n dc o m m u n i c a t i o nt h r o u g ha c c e s s i n gs h a r e dr e s o u r c e s ，a n dt h es y n c h r o n i z a - t i o nm e c h a n i s mf o ra c c e s s i n gs h a r e dr e s o u r c e si sk e yt oe n s u r et h ec o r r e c t n e s so f p a r a l l e lp r o g r a m s a tp r e s e n t ，t h e r em a i n l ye x i s tt w od i f f e r e n tk i n d so fs y n c h r o n i z a t i o nm e c h a - n i s m sf o rs h a r e dv a r i a b l ea c c e s sc o n t r 0 1 o n ei sl o c k i n ga n dt h eo t h e ri st r a n s a c - t i o n a lm e m o r y t h et r a d i t i o n a ll o c k i n gs y n c h r o n i z a t m nm e c h a n i s mm a n a g e st h e c o n c u r r e n ts t o r ea n dl o a do v e rs h a r e dr e s o u r c e sb yl o c k - p r o t e c t e dc r i t i c a ls e c t i o n h o w e v e r ，t h el o c k i n gw a y n o to n l yl i m i t st h ee x e c u t i o ne f f i c i e n c yr u n n i n go nm u l t i - c o r ep r o c e s s o r s ，b u ta l s oe a s i l yl e a d st od e a d l o c ka n dm a k e st h er u n n i n gp r o g r a m t oe n t e rt h ea b n o r m a ls t a t e r e a d - w r i t el o c k sa n dr e e u t r a n tl o c k sa r et h el o c k - b a s e ds y n c h r o n i z a t i o nm e c h a n i s m sf o ra c h i e v i n gt h eo p t i m i z a t i o n t h er e a d - w r i t e l o c k sa l l o wm u l t i p l et h r e a d st or e a dt h es h a r e dr e s o u r c e sc o n c u r r e n t l y , a n dt h e r e e n t r a n tl o c k sp e r m i tt h r e a d st or e a c q u i r et h es e l f - o w n e dl o c k st oa v o i dd e a d l o c k o ni t s e l f t r a n s a c t i o n a lm e m o r y ( t m ) i san e wr e s e a r c ht o p i co ns y n c h r o n i z a t i o n t e c h n o l o g yf o rb r i n g i n gt h ea d v a n t a g e so fm u l t i - c o r ep r o c e s s i n gs y s t e mi n t op l 矗y i ta t t e m p t st ou t i l i z eas e q u e n c eo fg r o u p e di n s t r u c t i o n st h 8 te x e c u t ea t o m i c a l l y a n di ni s o l a t i o nt os i m p l i f yp a r a l l e lp r o g r a m m i n g o u rg r o u p sr e s e a r c ht o p i ci sv e r i f i c a t i o no fc o n c u r r e n tp r o g r a m su s i n gd i v e r s e s y n c h r o n i z a t i o nm e c h a n i s m s t h i sd i s s e r t a t i o nm a i n l yf o c u s e 8o nt h ev e r i f i c a t i o n o fl o w - l e v e lc o n c u r r e n tp r o g r a m su s m gr e a d - w r i t el o c k sa n dr e e n t r a n tl o c k s t h e e x i s t i n gf o r m a lv e r i f i c a t i o nf r a m e w o r ka n dp r o g r a ml o g i cf o rr e a s o n i n ga b o u tt h e l o c k - b a s e dp a r a l l e lp r o g r a m so n l yc o n s i d e rt h en o n - r e e n t r a n te x c l u s i v el o c k sw i t h s i m p l es e m a n t i c sa n di g n o 地r e a d - w r i t el o c k sa n dr e e n t r a n tl o c k s t h e s ei m p r o v e d s y n c h r o n i z a t i o nm e c h a n i s i i i bc a ni m p r o v et h ep e r f o r m a n c eo fp a r a l l e lp r o g r a m sa n d e a s ep a r a l l e lp r o g r a m m i n g ，b u tw ec a n n o td i r e c t l ya p p l yt h ee x i t i n gt e c h n o l o g y 中国科学技术大学博士学位论文 英文摘要 t or e a s o na b o u tt h e md u et ot h e i rc o m p l e xs e m a n t i c s i na d d i t i o n ，b o t hl o c k i n g a n dt mh a v et h e i rs t r e n g t h e na n dw e a k n e s s ，a n dt h ef u t u r eh i g hp e r f o r m a n c e p a r a l l e ls o f t w a r ep r o b a b l yn e e dt ou s eb o t ho ft h e mt oo b t a i nt h em o s tb e n e f i t s ， a n dt h ep r o g r a ml o g i cf o rr e a s o n i n gt h ec o n c u r r e n tp r o g r a m sw i t hb o t hl o c k i n g a n dt ma r er e q u i r e dt oe n s u r et h ec o r r e c t n e s so ft h ec o r r e s p o n d i n gh i g hc o n f i - d e n t i a ls o f t w a r e s t h ed e s i g n m e n to fa na p p r o p r i a t ei n t e r m e d i a t el a n g u a g ei st h e p r e m i s eo fr e a s o n i n ga b o u tt h em i x i n gs y n c h r o n i z a t i o nm e c h a n i s m s h o w e v e r ，f e w r e s e a r c hw o r k sc o n c e r no nt h el a n g u a g ea n dp r o g r a ml o g i cd e s i g nf o rs u p p o r t i n g b o t hl o c k i n ga n dt ms y n c h r o n i z a t i o nm e c h a n i s m s a c c o r d i n gt ot h er e s e a r c hb a c k g r o u n do fl o c k i n ga n dt m ，a sw e l la st h ee x - i s t i n gr e s e a r c hr e s u l t so np r o g r a mv e r i f i c a t i o n ，t h em a j o rw o r ko ft h i sd i s s e r t a t i o n i sd i v i d e di n t ot h ef o l l o w i n gt w oa s p e c t s ： o nt h eo n eh a n d ，w ea t t e m p tt oe x t e n dt h ec e r t i f i e dc o n c u r r e n ta s s e m b l ea r o - g r a m ( c c a p ) f r a m e w o r kt h a tp r o p o s e db yp r o ls h a oa n dd e s i g nt h ee x c l u s i v e h o a r e - s t y l ep r o g r a ml o g i cf o rr e a s o n i n gc o n c u r r e n ta s s e m b l ep r o g r a m su s i n gr e a d - w r i t el o c k sa n dr e e n t r a n tl o c k si no r d e rt oc o n s t r u c tf o u n d a t i o n a lp r o o fc a r r y i n g c o d e ( f p c c ) w ec h o o s ec o n c u r r e n ts e p a r a t i o nl o g i c ( c s l ) w h i c hi sf i tf o rr e a s o n - i n gc o n c u r r e n tp r o g r a m w i t he x c l u s i v ec r i t i c a ls e c t i o n sa n ds u p p o r t sm o d u l a r i t y 蠲 0 1 1 1 b a s i cl o g i c ，a n dd u et oi t sl i m i t a t i o nw ee x t e n di tt os u p p o r tr e a s o n i n ga b o u t r e a d - w r i t el o c k sa n dr e e n t r a n ti o c ka sf o l l o w s ： w ee x t e n dc s lt or e a s o na b o u tc o n c u r r e n tp r o g r a m su s i n gr e a d - w r i t el o c k s p r i m i t i v e s ，a n dt h es e p a r a t i o nc o n j u n c t i o ni nc s li sd i v i d e di n t o s t r o n g s e p a r a t i o n a n d w e a ks e p a r a t i o n t h ef o r m e rw h i c hd on o ta l l o w sr e s o u r c e o v e r l a p si su s e dt od e s c r i b et h er e s o u r c ep a r t i t i o na m o n gr e a d - w r i t ea n dr e a d - r e a dt h r e a d s ，a n dt h el a t t e rw h i c ha l l o w sr e s o u r c eo v e r l a p si su s et od e p i c t t h er e s o u r c ep a r t i t i o na m o n gr e a d - r e a dt h r e a d s o u re x t e n s i o nm a k e su pt h e l i m i t a t i o no fc s lw h i c ho n l ya l l o w ss t r o n gs e p a r a t i o no v e rr e s o u r c e 8 w bd e s i g na ni n f e r e n c er u l e sf o rt h ef i r s te n t r ya n dr e e n t r yo fa c q u i r i n g r e e n t r a n tl o c k sb a s e do nc s l ，t h er 髑o u r c eo w n e r s h i pt r a n s f e ri nt h ea d a p t e d c s la v o i d sr e a c q u i r i n gt h eb a l er e s o u r c e s t h e nt h ee x t e n d e dc s lc a nb e a p p l i e dt or e a s o na b o u tc o n c u r r e n tp r o g r a m su s i n gr e e n t r a n tl o c k s 中国科学技术大学博士学位论文 英文摘要 w eu s ec o q p r o o f a s s i s t a n tt oi m p l e m e n tt h ep r o p o s e dv e r i f i c a t i o nf r a m e w o r k s a n dg i v et h e i rs o u n d n e s sp r o o f , t h i sm a k e so u rr e a s o n i n gs y s t e mm o r er e l i a b l e o nt h eo t h e rh a n d ，w ep r e s e n tan o v e ls y n t a xc o n s t r u c t ”，e ” c ) ”t od e s c r i b e t h er e v e r s i b l ec o d eb l o c k sw h i c hi sc l o s e l yr e l a t e dt ot m w i t ht h eh e l po ft h i s c o n s t r u c tw eo b t a i na ni n t e r m e d i a t el a n g u a g et oc o m b i n eb o t hl o c k i n ga n dt m i n t oau n i f i e dp r o g r a m m i n gm o d e l w ea l s od i s c u s st h ed i f f i c u l t i e so nr e a s o n i n g a b o u tt h er e v e r s i b l eb l o c k s ，a n dt h i sp r e l i m i n a r yw o r kg i v e st h eb a s i sf o rf u r t h e r s t u d yo ff o r m a lv e r i f i c a t i o no fr e v e r s i b l ec o d eb l o c k s a ne x a m p l ei sg i v e n t o d e m o n s t r a t et h ee x p r e s s i v ep o w e ro ft h ep r o p o s e dl a n g u a g e ，a n dt h er e q u i r e m e n t s f o rs a f e l ye x e c u t i n gr e v e r s i b l ec o d eb l o c k sa r ea l s od i s c u s s e d k e yw o r d s ：c o n c u r r e n c yv e r i f i c a t i o n ，r e a d - w r i t el o c k s ，r e e n t r a n tl o c k s ，a s s e m b l y c o d e ，t r a n s a c t i o n a lm e m o r y , c o n c u r r e n ts e p a r a t i o nl o g i c - v - 中国科学技术大学学位论文原创性和授权使用声明 本人声明所呈交的学位论文，是本人在导师指导下进行研究工作 所取得的成果。除已特别加以标注和致谢的地方外，论文中不包含任 何他人已经发表或撰写过的研究成果。与我一同工作的同志对本研究 所做的贡献均已在论文中作了明确的说明。 本人授权中国科学技术大学拥有学位论文的部分使用权，即：学 校有权按有关规定向国家有关部门或机构送交论文的复印件和电子 版，允许论文被查阅和借阅，可以将学位论文编入有关数据库进行检 索，可以采用影印、缩印或扫描等复制手段保存、汇编学位论文。 保密的学位论文在解密后也遵守此规定。 作者签名：拉! 途 矽7 年，月；1 日 中国科学技术大学博士学位论文第一章绪论 第一章绪论 随着计算机应用的不断发展，软件已渗透到国民经济和国防建设的各个领 域，在信息社会中发挥着至关重要的作用。因而软件一旦出现错误就可能会导致 巨额的财产损失，甚至威胁到生命安全，安全机密系统中的软件错误还可能会导 致国家机密的泄露。在当今的互联网环境中，软件缺陷与漏洞的问题更加突出 越来越多的软件基于网络环境进行开发、传播和运行，其安全性( s a f e t y ) 、可靠 性( r e l i a b i l i t y ) 、保密性( s e c u r i t y ) 面临着更加严峻的挑战。由此可见，软件质量 的问题关系到社会进步与经济发展，高可信软件相关的理论与技术问题在全球得 到了极大的重视，并且在研究领域取得了一些进展f l ，2 】。例如，有关携带证明的 代码( p r o o f - c a r r y i n gc o d e ，p c c ) 【3 】的研究为高可信软件的构造提供一种新的思 路：传统的软件加上软件的安全性证明就能够提高软件的可信度。 另一方面，近年来多核多处理器等以共享存储为特征的新一代系统结构的出 现，加速了对快速研发基于共享资源的并行软件的需求，这给基于共享资源的高 可信并行软件构造带来许多挑战性研究课题。然而保证并行程序的正确性远比保 证串行程序的正确性困难的多，这是由于并行程序中多线程之间交叠执行的不确 定性和干扰性，它使得推理并行程序的性质十分困难。在基于共享资源的并行软 件构造中，线程间的交互和通信主要通过访问共享资源来实现，对访问共享资源 的同步控制是保证并行程序正确执行的关键所在。因此为提高并行软件的生产率 和可信度，需要提供有效的方法验证使用各种同步机制的并行程序的正确性 1 1 研究背景及相关工作 本文关注的焦点是验证使用读写锁和可重入锁的低级并行代码的正确性，而 程序的正确性是指给定程序规范，判断该程序是否依照程序规范指示的方式执 行。这里程序规范不仅指明了程序在功能上的要求，同时还给出了程序在行为上 应受到的限制。程序验证是保证软件正确性的重要手段，它研究如何使用数学方 法严格证明一个程序是否满足指定的程序规范。具体实现过程是：在程序中用形 式化方法给出程序的规范，然后通过一些推理规则对这些规范以及相关代码进行 验证。常用的验证手段主要是模型检查和定理证明。 在本节中首先概述当前并行编程实践中所采用的主要同步机制，并分析它们 的优缺点；然后介绍目前用于并行程序正确性验证的逻辑系统和验证框架；最后 - 1 中国科学技术大学博士学位论文 1 1 研究背景及相关工作 分析已有的逻辑系统和验证框架在推理使用读写锁和可重入锁的并行程序时存 在的问题。 1 1 1 同步机制 现在流行的并行编程实践大都采用锁等较低级的同步设施用于共享变量的 访问控制，编程难、易出错( 如出现数据竞争、死锁等) 且不易组织能发挥多核多 处理优势的编程。为了提高锁同步机制的易编程性及使用锁编写的并行程序的并 发度，通过对语义简单的互斥锁进行优化改进得到读写锁和可重入锁。读写锁通 过允许多个线程同时并发只读访问共享资源而提高线程并发度；而可重入锁则 通过允许线程再次获得已经持有的锁而避免自死锁，同时也提高了易编程性。但 是，无论是读写锁还是可重入锁仍需要程序员手动分配锁保证并发线程在访问共 享资源时无数据竞争，而且无法彻底避免死锁现象的发生。 在共享变量访问控制的实现方面，除使用锁等低级方式外，近年来主要研究 的是事务内存( t r a n s a c t i o n a lm e m o r y ) 技术。粗略地说，事务内存是一种编程抽 象【4 1 ，它试图通过允许一组存取共享内存的指令( 称为事务) 原子且隔离地执行来 简化并行编程。它是一种允许事务乐观地投机并行执行并在发现冲突时部分事务 回滚到初始状态的、类似数据库事务的并发控制机制。事务虽具有其代码全都执 行或全不执行的原子性和不受其他事务干扰的隔离性，但是事务的概念及其语义 的具体设计必须考虑与现有操作系统、编程语言和程序代码等构成的丰富且复杂 的开放世界的衔接【4 】，因此尚存一些问题有待解决。例如，事务与( 也访问共享变 量的) 非事务代码之间的交互语义尚待明确睁- 8 】，是否可以将系统调用和i o 等 很难或不可能恢复原先状态的操作包容到事务中【4 ，9 ，l o 。用硬件实现的事务内 存在性能上有较大优势但是对现有硬件结构有较大改动且难以支持任意大小的 事务；而用软件实现的事务内存则存在运行开销大、语义不明等问题【4 】。 一些特殊的共享变量访问控制可以通过无锁编程来实现低级代码上无锁 编程的目标是在不使用l o c k 指令的前提下进行线程同步，安全地管理共享数据， 其主要实现基础是c a s ( c o m p a r ea n ds w a p ) 指令或者l l s c ( l o a d - l i n k s t o r e - c o n d i t i o n a l ) 指令。无锁代码虽效率高但很难编写和维护【1 l ，1 2 】 1 1 2 并行程序正确性验证 在并行程序的正确性验证方面，由于多线程的交叠执行和干扰性，保证并 行程序的正确性比保证串行程序的正确性要困难得多。虽然已经有许多方法 - 2 - 中国科学技术大学博士学位论文第一章绪论 f l z s 被研究用来推理验证顺序和并行程序的性质，但是由于并行程序中各种复 杂的行为，例如：线程的创建、复杂多样的线程间同步机制等，导致并行程序正 确性验证依然十分复杂。并行程序间的交互和干扰使得推理过程变得非常复杂， 同时也制约了实现模块化验证，而无法实现模块化验证的验证方法将缺乏实用价 值。 一些模型检查器【1 9 - 2 4 1 被研究用来验证并行程序的正确性，但是它们大 都只能检查有限固定线程数的程序。c i r c 【2 5 】算法虽然支持线程数目无限制 的并行程序检查，但它并没有考虑动态线程创建对环境的改变。3 v m c 【2 6 1 支 持线程数目无限制且线程动态创建的检查，但它不支持模块化验证。另外，许 多的类型系统【2 7 - 3 0 1 也被研究用来推理并行程序的性质，它们使用高阶逻辑 和特殊的类型标识来验证并行程序的一些特殊的性质，譬如无数据竞争、无 死锁、原子性等。目前基于逻辑方法的验证框架主要有p c c ( p r o o f - c a r r y i n g c o d e ) f 3 】和f p c c ( f o u n d a t i o n a lp r o o f - c a r r y i n gc o d e ) f 3 1 1 框架。p c c 的基 本思想是把二进制代码和此份代码的证明放在一起一并交给用户，使得 用户能够容易的验证该代码的正确性。f p c c 是在p c c 的基础上，采用高 阶逻辑来同时描述机器指令的操作语义和用户所需要的安全策略，使得 在f p c c 中可以验证程序的部分正确性。z h o n gs h a o ( 邵中) 所领导的f l i n t 采 用语法方式的f p c c ，提出了几种使用h o a r e 【1 5 】风格的汇编代码验证框架，诸 如c a p 3 2 、c c a p 3 3 、c m a p 3 4 1 、s c a p 3 5 、a i m 3 6 等项目，这些项目分别实 现了内存管理、单核上的多线程程序、基于栈的控制函数、中断处理程序等内容 的验证。 一些支持模块化验证的程序逻辑( 即描述和证明程序行为的逻辑) 被用来推理 并行程序的正确性，其中最有影响的是r e l y - g u a r a n t e e 方法( 简称r g 方法，也 称a s s u m e - g u a r a n t e e 方法) 【3 7 ，3 8 1 。在该方法中，程序的验证分为两步，首先检 验线程间的无干扰性：每个线程的假设r 由任何其他线程的保证g 蕴涵；然后分 离地验证每个线程在它的r 得到满足时履行它的g 不变式证明技术 3 9 】是一种 最简单的推理并行程序的方法，它通过一个全局不变式描述所有线程访问的共 享资源所满足的要求。p e t e ro h e a m 提出了并发分离逻辑【4 0 ，4 1 1 ，它把分离逻 辑 4 2 ，4 3 ( s e p a r a t i o n1 0 9 i c ) 的思想用到共享内存下带内存指针的并行程序的验 证上v a f e i a d i s 等提出另一种将r - g 方法和分离逻辑相结合的形式m ，x i n y u f e n g ( 冯新宇) 则将局部推理和信息隐藏引入到并行推理1 4 5 1 3 - 中国科学技术大学博士学位论文 1 2 存在的问题 国内在并行程序验证方面的主要工作有：张兆庆等曾经探讨基于消息传递 机制的p v m ( p a r a l l e lv i r t u a lm a c h i n e ) 程序到p e t r i 的自动转换和验证方法【4 6 】。 蒋昌俊等曾经引用时序p e t r i 网描述并行程序的时序p e t r i 网建模方法f 4 7 l 。另外， 本实验室的课题小组最近将f p c c 风格的验证框架应用于推理使用事务内存同 步机制的并行汇编程序的正确性【4 8 】，文中设计的抽象机器模型引入了一些标识 事务代码段开始和结束的粗粒度原语s t a r t r a n s 、c o m m i t ，并修改读写指令的语 义使得与事务读写语义一致，然后基于该事务语义模型利用不变式证明技术设计 推理规则。 1 。2 存在的问题 由于同步机制的语义的复杂性和多样性，导致上述程序验证技术很难直接应 用在推理使用各种同步机制的并行程序中。其中读写锁和可重入锁是使用低级的 锁同步设施实现的高级同步机制，这些基于锁同步机制的优化无疑可以提高易编 程性和程序的性能，但是同时也给推理它们带来了新的挑战，已有的验证框架或 逻辑系统多数只考虑如何推理语义最简单的互斥锁，而忽略了语义较为复杂的读 写锁以及可重入锁的推理。 事务内存作为一种复杂的高级同步控制机制被引入到并行编程语言中。分析 一些高效的软件事务内存系统( t l 2 、t i n y s t m ) 【4 9 ，5 0 1 的实现，可以发现它们 对外提供的编程接口都采用互斥锁或读写锁进行共享数据的同步访问控制。因 此，推理使用事务内存同步机制的并行程序，要求对使用锁同步的并行程序的推 理技术有全面和深入的理解。另一方面，锁和事务内存同步机制都有各自的优缺 点，并且已有的大量使用锁同步的代码导致事务内存不可能完全取代锁。高性能 的并行软件可能需要同时发挥两种同步机制的优势，所以需要提供一种有效的方 法将事务代码正确安全的融合到锁代码中，这种正确性则需要通过严格的程序逻 辑来提供保证。因此要求设计一种能用于实现锁同步原语以及反映事务同步机制 特征的中间语言，为推理验证使用混合同机制的并行程序提供一个基础平台。指 导高层同步抽象的设计和实现，为构造高性能高可信的并行软件奠定基础。目前 围绕着事务内存同步机制的研究主要集中于事务内存系统的各种实现策略及其 性能的提高上，而对使用事务内存同步机制的并行程序形式验证的研究很少，主 要考虑的都是事务内存系统的形式语义描述【8 ，5 1 - 5 3 1 。而考虑如何推理同时使用 锁和事务内存同步机制的并行程序的工作则更少，仅文献1 5 4 1 通过分析锁和事务 4 中国科学技术大学博士学位论文第一章绪论 内存两种同步机制的优缺点提出未来并行编程语言应该是以锁为主导而事务内 存辅助的编程方式。 针对各种同步机制和并行程序验证技术的研究现状，本文主要探索如何 将f p c c 【3 1 】风格的验证框架应用于推理使用读写锁和可重入锁同步机制的并行 程序；如何设计一种中间语言能同时用于实现底层的锁同步原语以及显式反映事 务同步机制的可恢复性。 1 3 本文的主要工作及贡献 本文首先分析研究了目前主要的并行程序验证技术，包括分离逻辑【4 2 】、 并发分离逻辑r e l y - g u a r a n t e e 3 t l 、结合r - g 和分离逻辑的逻辑系统r g s e p 阻】及s a g l 5 5 1 、和最新的支持局部推理的研究成果l r g 【4 5 】。针对具体的优 化同步机制一读写锁和可重入锁，选择模块性较好的并发分离逻辑进行扩 展，使其支持对使用这两种优化同步机制的并行程序的推理。我们通过扩展基 于f p c c 验证框架构建的汇编并行代码验证框架c c a p 将读写锁和可重入锁的 推理方法形式化到f p c c 验证框架中，选择该验证框架的原因是它在汇编级上探 讨程序安全属性，因而不需要信任复杂、易出错的编译和优化过程，能够使用较 小的t c b 构造p c c f p c c 代码包。同时，验证框架对读写锁和可重入锁同步机 制的抽象与高层的描述相似，验证框架所采用的推理方法也可以应用到相对高层 的使用这两种同步机制的并行程序中。在验证框架的构造过程中，我们首先将读 写锁和可重入锁同步原语添加到抽象机器模型中，并给出了这些同步原语的语义 描述，然后根据读写锁和可重入锁得语义特点设计适合推理它们的程序逻辑，并 给出推理规则用于验证在抽象机器上执行的程序。在证明这些推理规则遵循读写 锁和重入锁同步机制的语义的可靠性之后，给出验证实例说明验证框架的有效性 以及验证框架中构造程序证明的过程。另外本文还设计了一种支持可逆代码块的 中间语言能同时用于实现锁和事务内存同步机制，利用显式的可逆代码块的标识 反映事务操作的可恢复性，尝试设计推理规则禁止不可逆的操作出现在可逆代码 块中，为推理同时使用锁和事务内存同步机制的并行程序的正确性提供一个基础 平台。 本文工作主要的贡献是： 本文通过扩展c c a p 验证框架得到一个推理使用读写锁的并行汇编程序的 验证框架。通过扩展并发分离逻辑来支持以读写锁为基本同步原语的并行 5 - 中国科学技术大学博士学位论文1 4 章节安排 程序的推理，将并发分离逻辑中分离的含义扩展为 强分离”和”弱分离”两 类，利用表示资源不相交的强分离描述写写和读一写线程间对共享资源的划 分，利用允许资源相交的弱分离描述读读线程间对共享资源的划分，从而 弥补并发分离逻辑中要求共享资源在多个并行线程间进行不相交的划分的 不足。 本文通过扩展c c a p 验证框架得到了一个推理使用可重入锁的并行汇编程 序的验证框架。由于在并发分离逻辑中推理互斥锁同步原语的推理规则在 推理可重入互斥锁时不区分线程首次获得锁和再次获得锁，而统一利用所 有权转移的推理方法将锁保护共享资源转移到线程私有部分，导致共享资 源被线程重复获得而产生推理错误。我们设计了两种不同的推理规则来推 理线程首次获得锁和再次获得锁的情况，从而避免资源被线程重复获得， 使得并发分离逻辑能正确推理使用可重入锁的并行程序。 笔者对上述两个验证框架都使用c o q 定理证明辅助工具【5 6 】进行了实现， 并对验证框架中各个组成部分的c o q 实现方法进行了总结，包括抽象机 器、程序规范、推理规则的定义和可靠性定理的证明这四个部分。通过 与c o q 的交互，构造生成了机器可检查的证明。从而使得所提出的验证框 架更为可靠。本文工作的所有c o q 实现都可以从网上下载【5 7 】。 本文提出了一种新颖的语法结构“r e v c 用于描述与事务内存实现特点 密切相关的可逆代码块，它要求代码c 的执行对整个程序状态产生的效果 总是可以通过某种机制进行恢复的。文中讨论了推理这类代码块的困难及 方法，并结合实例说明该语法结构的表达能力，并阐述安全执行的可逆代 码块应该满足的性质。为进一步的深入研究可逆代码块的推理验证和混合 同步机制的并行编程语言设计打下基础。 1 4 章节安排 本文剩余的章节组织如下： 第2 章详细介绍了当前与并行程序验证相关的概念和技术背景，以一个简单 的并行编程语言s p p l 为平台，对目前主要的并行程序的推理验证技术做了详细 的介绍，并对各种并行程序的推理验证技术进行了分析比较。最后介绍了展开各 种同步机制的推理验证工作的基础框架一c c a p 。 一6 - 中国科学技术大学博士学位论文第一章绪论 第3 、4 章分别给出了一个推理使用读写锁和可重入锁的并行程序的f p c c 风 格的验证框架，在给出构成该验证框架的抽象机器、程序规范和推理规则后，并 证明了验证框架遵守读写语义的可靠性，并通过例子说明了验证框架的有效性。 第5 章中介绍使用c o q 定理证明辅助工具 5 6 1 进行实现本文给出的验证框架 的技术和方法。 第6 章中介绍了一种新颖的语法结构“r e v c ，用它描述事务代码中的可 逆代码块，并非形式化的描述可逆代码块的语义及推理可逆代码块的方法，通过 具体的例子说明“r e v c 的表达能力，并说明验证可逆代码块存在的问题和难 点。 - 7 - 中国科学技术大学博士学位论文第二章相关理论与技术基础 第二章相关理论与技术基础 本章主要介绍与并行程序验证相关的理论和技术基础，为开展