（计算机软件与理论专业论文）使用事务内存同步机制的并行程序验证的研究.pdf

摘要 摘要 近年来，随着超线程、多核体系结构等多线程技术的发展和广泛应用，计 算机硬件已经提供了越来越高效的软件运行平台。但是要更好地利用这些平台 的并行优势，计算机软件就需要具备更好地并行性，以充分利用多个处理器的 性能。并行程序已经成为了软件开发的主流。然而要确保顺序程序的正确性已 经是非常困难的了，要保证并行程序的正确性难度更甚。这是因为在并行程序 中，程序员还需要处理共享数据的并发存取问题，确保数据在不同线程中的有 效性。传统上，程序员使用锁的方式来管理并行程序中共享数据的并发存取。 但是锁方式不仅难于推理，而且还容易出现死锁等导致程序进入异常执行状态 的隐患。为减轻程序员开发并行程序的负担，提高软件开发的效率，近年的研 究提出了使用事务内存同步机制来管理共享数据的并发存取。提供了事务内存 同步机制的系统通过自动地管理数据的并发访问，免除了程序员在这方面的负 担，也避免了死锁等锁机制的致命隐患。但是近年来围绕着事务内存同步机制 的研究主要集中于提供事务内存同步机制的系统的各种实现策略及其性能的提 高上，而对该同步机制在程序推理、形式验证及易于推理方面的研究甚少。 针对事务内存同步机制相关研究的现状，基于程序推理验证的研究成果， 本文提出了一种推理方法以推理使用了事务内存同步机制的实现系统所提供的 编程结构的程序。该推理方法基于众所周知的不变式证明( i n v a r i a n c ep r o o f ) 方法并对h o a r e 逻辑进行了扩展，通过指明共享数据上的不变式来约束多个线 程间的并发访问，可靠、可行，并具备模块化验证的特点。同时，本文还专注 于事务内存同步机制的语义研究，在携带证明的代码的研究的基础上，将所 提出的推理方法形式化到遵循事务内存同步机制语义的h o a r e 风格的验证框架 中，并证明了推理方法遵循事务内存同步机制的语义的可靠性。此外，本文还 给出了推理验证的应用实例，展示了本文所提出的推理方法和验证框架的有效 性。最后，本文通过详尽的比较，阐明了事务内存同步机制相对于传统的锁同 步机制易推理的优点，展示了事务内存同步机制对程序推理的简化。 7 本文的主要特色和贡献为： 本文提出了一种h o a r e 风格的推理方法，用于在事务内存同步机制的语义 的高层抽象上推理源语言级的并行程序。 本文也提出了一个携带证明的代码( p r o o f - c a r r y i n gc o d e ) 风格的验证框 架，用于在事务内存同步机制的语义的底层实现上验证汇编级的并行程 序，并证明了验证框架遵循事务内存同步机制的语义的可靠性。该验证框 架的提出，填补了携带证明的代码的研究在事务内存同步机制方面的空 白。 摘要 本文在c o q 定理证明辅助工具中完成了所提出的验汪框架的可靠性证明， 从而将验证框架中的验证推理系统从受信任计算基础中排除出去，使得本 文的验证框架具有更高的可靠性。 本文还通过详细的比较阐述了事务内存同步机制相对于锁同步机制的易推 理的优势。 关键字：软件安全，并行程序验证，汇编语言，受信任计算基础，携带证明的 代码，事务内存同步机制 1 工 a b s t r a c t a b s tr a c t t h em u l t i c o r ea r c h i t e c t u r e w h i c hh a sp r o v i d e di n f r a s t r u c t u r e so fb e t t e rp e r - f o r m a n c e ，h a sb e c o m ep o p u l a r t ob e n e f i tf r o mt h i sg r o w t hi np e r f o r m a n c e ， p r o g r a m m e r sa r er e q u i r e dt od e v e l o pm u l t i t h r e a d e dp r o g r a m s w h e r e a si ti s d i f f i c u l tt oe n s u r ec o r r e c t n e s sf o rs e q u e n t i a lp r o g r a m s ，i ti se v e nm o r es of o rc o n c u r r e n tp r o g r a m sd u et ot h ei n t e r a c t i o nb e t w e e nm u l t i p l et h r e a d s t r a d i t i o n - a n y , p r o g r a m m e r su s el o c k st oa c h i e v em u t u a le x c l u s i o no nc o n c u r r e n ta c c e s st o s h a r e dr e s o u r c e s b u tl o c k - b a s e dp r o g r a m m i n gi sd i f f i c u l tt or e a s o na b o u ta n d m a yl e a dt op r o b l e m ss u c ha sd e a d l o c k t r a n s a c t i o n a lm e m o r y ( t m ) i sp r o p o s e d a sa na l t e r n a t ec o n c u r r e n c y - c o n t r o lm e c h a n i s mt oa v o i dm a n yo ft h ep i t f a l l so f t h el o c k - b a s e do n e t ms y s t e m sm a n a g ed a t ar a c e sb e t w e e nt h r e a d sa u t o m a t i - c a l l ys ot h a tp r o g r a m m e r sd on o th a v et or e a s o na b o u tt h ei n t e r a c t i o no ft h r e a d s m a n u a l l y t mp r o v i d e sap r o g r a m m i n gm o d e lt h a tm a ym a k et h ed e v e l o p m e n to f m u l t i t h r e a d e dp r o g r a m se a s i e r m u c hw o r kh a sb e e nd o n et oe x p l o r et h ev a r i o u s i m p l e m e n t a t i o ns t r a t e g i e so ft ms y s t e m sa n dt oa c h i e v eb e t t e rp e r f o r m a n c e ，b u t l i t t l eh a sb e e nd o n eo nh o wt of o r m a l l yr e a s o na b o u tp r o g r a m su s i n gt ma n dh o w t om a k es u r et h a ts u c hr e a s o n i n gi ss o u n d t h i sd i s s e r t a t i o np r e s e n t sar e a s o n i n gm e t h o df o rp r o g r a m su s i n gt ma n d f o r m a l i z e si ti n t oah o a r e - s t y l ev e r i f i c a t i o nf r a m e w o r k t h er e a s o n i n gm e t h o d i sb a s e do ni n v a r i a n c ep r o o fa n dh o a r e - s t y l er e a s o n i n ga n ds u p p o r t sm o d u l a r v e r i f i c a t i o n t h ep r o o f - c a r r y i n gc o d e ( p c c ) s t y l ef r a m e w o r ki sp r o v e ds o u n dw i t h r e s p e c tt ot h et ms e m a n t i c s a n dac o m p a r i s o nb e t w e e nl o c k b a s e dr e a s o n i n g a n dt m b a s e dr e a s o n i n gi sp r e s e n t e da n ds h o w st h ec o n v e n i e n c eo ft h el a t t e r t h i sd i s s e r t a t i o nm a k e st h ef o l l o w i n gc o n t r i b u t i o n s ： i tp r e s e n t sah o a r e - s t y l er e a s o n i n gm e t h o dt or e a s o na b o u ts o u r c e - l e v e l p r o g r a m su s i n gt m e v e nt h o u g hp r o g r a m m i n gu s i n gt r a n s a c t i o n si ss u p - p o s e dt or e a s o na b o u te a s i l y , t h e r ea r es u b t l ep r o p e r t i e se x p e c t e db ym u l t i - t h r e a d e dp r o g r a m s t oe n s u r es u c hp r o p e r t i e sa r ec o r r e c t l ye n f o r c e di n ac o n c u r r e n tp r o g r a m ，p r o g r a m m e r sm u s tr e a s o na b o u tt h eb e h a v i o r so f t h e i rp r o g r a m st h o r o u g h l y t h i sd i s s e r t a t i o np r e s e n t sam e t h o dt op e r f o r m s u c ht m b a s e dr e a s o n i n g a n dt h ep r e s e n t e dr e a s o n i n gi sb a s e do nt h e s a m ei n t e n d e ds e m a n t i c so fd i f f e r e n tt ms y s t e m s ：t op r o v i d eap r o g r a m - m i n gs t r u c t u r et h a te x e c u t e sa t o m i c a l l ya n di ni s o l a t i o n ，t h i sm a k e st h e i l l a b s t r a c t p r e s e n t e dr e a s o n i n gc o m p a t i b l ew i t hv a r i o u st ms y s t e m st h a tr e s p e c tt h e s a m ei n t e n d e ds e m a n t i c s i ta l s op r e s e n t sap r o o f - c a r r y i n gc o d es t y l ef r a m e w o r kt oc e r t i f yt h ep r o p e r - t i e so fa s s e m b l yl e v e lp r o g r a m su s i n gt m t h ep r e s e n t e df r a m e w o r kb r i n g s p c ci n t ot h eb r a n d - n e wt ma r e a t h ei n f e r e n c er u l e so ft h ef r a m e w o r k a r ep r o v e ds o u n dw i t hr e s p e c tt ot h et ms e m a n t i c s a n de x a m p l e sa r e a l s og i v e nt oi l l u s t r a t et h ec o n s t r u c t i o no ft h ep r o o f sf o rp r o g r a m si nt h e f r a m e w o r k ，d e m o n s t r a t i n gt h ee f f e c t i v e n e s so ft h ef r a m e w o r k t h ep r e s e n t e df r a m e w o r ka d d r e s s e ss a f e t yi s s u e sa ta s s e m b l y 1 e v e ld i r e c t l y a sp c c s y s t e m sd o s ot h ec o m p l i c a t e da n de r r o r p r o n ec o m p i l a t i o na n do p - t i m i z a t i o nd on o tn e e dt ob et r u s t e d a n dt h ep r e s e n t e dr e a s o n i n gm e t h o d i sf o r m a l i z ei n t of r a m e w o r ka n di ss o u n dd u et ot h es o u n d n e s so ft h ef r a m e - w o r k a l lt h ew o r ko nt h ef r a m e w o r k ，i n c l u d i n gi t ss o u n d n e s sp r o o fa n d e x a m p l e s ，i sm e c h a n i z e di np r o o fa s s i s t a n tc o q t h i sm a k e so u rw o r km o r e r e l i a b l e t h r o u g ht h o r o u g hc o m p a r i s o n ，i ts h o w st h ec o n v e n i e n c eo ft m - b a s e dr e a - s o n i n go v e rl o c k - b a s e dr e a s o n i n g k e yw o r d s ： s o f t w a r es a f e t y , c o n c u r r e n c y v e r i f i c a t i o n ，a s s e m b l yl a n g u a g e ， t r u s t e dc o m p u t i n gb a s e ，p r o o f - c a r r y i n gc o d e ，t r a n s a c t i o n a lm e m o r y 中国科学技术大学学位论文原创性和授权使用声明 本人声明所呈交的学位论文，是本人在导师指导下进行研究工作 所取得的成果。除已特别加以标注和致谢的地方外，论文中不包含 任何他人已经发表或撰写过的研究成果。与我一同工作的同志对本 研究所做的贡献均已在论文中作了明确的说明。 本人授权中国科学技术大学拥有学位论文的部分使用权，即： 学校有权按有关规定向国家有关部门或机构送交论文的复印件和电 子版，允许论文被查阅和借阅，可以将学位论文编入有关数据库进 行检索，可以采用影印、缩印或扫描等复制手段保存、汇编学位论 文。 保密的学位论文在解密后也遵守此规定。 作者签名：盎垒 2 郴年石月堋 绪论 1 1 研究背景 第l 章绪论 随着计算机技术的广泛应用，社会生活的方方面面对计算机的依赖程度与 日俱增，从个人的利益和生命安全到国家的利益和安全都紧密地与计算机系统 联系在了一起，计算机系统的可靠性和安全性已经成为了人们关注的焦点。而 其中，人们对软件的安全性更为关切，因为相比硬件而言，软件应用才使得人 们真正获得了各种功能需求，而且它也更自由，更开放。但是随着应用需求的 增长，软件、包括操作系统已经变得越来越复杂和容易出错，要确保其正确性 己非常困难。而在许多领域，如核电站、飞机、医疗系统等等，其上所运行的 软件所产生的任何错误和异常都会给人们带来难以承受的损失。 近年来，随着多线程技术和多核体系结构的发展，计算机硬件已经提供了 越来越高效的软件运行平台毫但是要从体系结构持续的性能提升中不断获益， 就要求计算机软件能够更好地利用这些平台的多线程特性。并行程序已经成为 了软件开发的主流。然而要确保顺序程序的正确性已经是非常困难的了，要保 证并行程序的正确性困难更甚。这是因为在并行程序中，程序员还需要处理多 个线程之间的数据交互，这使得并行程序性质的推理变得十分困难，并行程序 中潜在的错误也更多更难以发现。并行程序的开发和维护因而也更为困难。 1 1 1 程序与安全 为了解决日趋严峻的程序安全闯题，人们研究了许多方法来改善程序的安 全性，尽可能地减少软件中存在的错误。程序测试是最常见的一种方法，测试 人员对程序进行大量的测试以试图发现程序中存在的安全性问题( b u g ) ，从 而提高程序的安全性。但是程序测试并不能有效地解决程序的安全性问题。首 先，程序测试难以覆盖程序所有可能的执行方式，它不能保证程序在所有可能 的执行状态下的安全性。其次，程序测试发现错误并对这些错误进行修改后， 并不能保证程序变得更安全了，这是因为统计表明修改一处错误往往会引入更 多的错误，程序测试无法保证对错误的修改不会引入新的错误。再次，大规模 复杂程序的测试成本往往都很高，重复的测试还使得错误检查的效率低下。 1 绪论 程序分析也是用于改善程序安全性的一种方法。分析人员利用辅助工具对 程序进行的静态分析，如数据流分析、控制流分析等，来检查程序的安全性。 虽然程序分析也可以查出程序中的一些错误，但是由于辅助分析工具往往无法 正确理解程序的语义，其自身也存在不完备不可靠的缺点，程序分析的结果常 会出现对程序错误的误报与漏报。因而它也不能很好地确保程序的安全性。 此外，还可以通过监视器监控计算机系统，在系统出现破坏行为时及时采 取恢复措施将系统恢复。但是这种方法也同样存在问题：首先，监视器也是运 行在计算机上的软件系统，其自身就存在安全性的问题，整个系统的安全性首 先依赖于监视器自身的安全性。其次，监视器无法预测整个复杂系统中可能出 现的各种错误，对其不理解的错误，监视器无法作出及时的恢复响应。 1 1 2 形式程序验证 程序测试、程序分析和系统监控之所以都不能够有效地解决程序的安全性 问题，关键在于它们都不能在理解程序语义的基础上查找程序中隐藏的问题。 无法明白程序行为的含义因而也就无法找出其中潜在的错误。于是就有了许多 帮助表达和理解程序语义的方法，程序注释就是最常见的一种帮助程序员开发 和维护程序的程序语义描述方法。但是程序注释通常都是用具有模糊性和二义 性的自然语言来编写的，使用它来描述确定的程序语义常常会不准确甚至会出 现对程序语义的错误描述。因此许多研究转而关注程序规范的形式描述( b o w e n ， 1 9 9 6 ；b o w e ne ta 1 ，1 9 9 3 ；c l a r k ea n dw i n g ，1 9 9 6 ) ，然而仅仅是形式的描述并无 法保证程序对象确实满足了程序规范，需要采用分析程序语义的方法去验证。 形式验证是一种静态的程序行为的检查，它虽然增加了构造安全程序所需要 的开销，但并没有增加程序在运行时的负担，因为所有的验证工作都在程序 运行前完成。程序语义形式描述及程序正确性证明的研究可以追溯到指称语 义( t e n n e n t ，1 9 9 7 ) ，h o a r e 逻辑( a p t ，1 9 8 1 ；h o a r e ，1 9 6 9 ) 等等。 形式验证的一种常用方法就是模型检查，它是对数学模型系统进行的详尽 的探测。但是由于模型检查作用在程序的抽象模型上，而从程序构造抽象模型 的过程往往是非平凡的，于是一个被验证了的模型并不一定能保证其对应的可 执行程序也是已被验证了的。 形式验证的另一种常用方法就是在程序上进行逻辑推导，它是对整个程序 进行的形式的数学推理。通常这种方法需要使用定理证明辅助工具来帮助其完 成形式推导。h o a r e 逻辑就是逻辑推导方法的一个实例。各种类型系统也是逻 辑推导方法的应用实例，只是其表达能力有限，所能推导的性质已经大为减少 了。 2 绪论 形式验证虽然可以提供安全性的可靠证明，但是其构造可靠证明的开销和 代价也是庞大的。这是因为形式验证过程不可能完全地由计算机程序自动地完 成，因为人们无法开发出可以理解所有程序语义的程序。而同时，形式验证过 程也不可能完全依靠人工完成。这是因为一方面程序员对程序的理解并不完全 可靠；另一方面软件规模和复杂度的增加，也使得程序员对整体系统的行为的 理解和把握变得更为困难。于是我们需要将尽可能多的验证工作交由计算机完 成，而当计算机无法自动完成时再交由人工完成。作为验证系统的一个特例的 类型系统之所以能够实现自动地验证其所关注的属性，是因为它所能验证的属 性的范围非常有限，并不支持通用属性的验证。但是它很好地说明了计算机系 统是可以自动完成某些性质的证明的。 1 1 3受信任计算基础 任何对程序正确性的研究，都是基于一个受信任计算基础( t r u s t e dc o m - p u t i n gb a s e ，简称t c b ) 之上的，它是指系统中不得不无条件给予信任的部 分。比如在讨论软件安全性的时候，所有的计算机硬件就都在t c b 之内。因为 如果计算机硬件不能正常工作，其上的软件执行就没有任何依据可以遵循，正 确性无从谈起。在通常的计算机系统中，操纵系统内核也属于t c b 的一部分。 t c b 通常可以用来评价一个系统的可靠程度。这是因为t c b 内部也是可 能存在漏洞的，而t c b 越大，产生漏洞的潜在可能也就越多，遭受的威胁也更 广。t c b 越小，相对的可能破坏整个系统安全性的潜在威胁也就越少。因而软 件安全性研究的一个重要的研究内容就是如何减小安全系统的t c b 。但是，无 论如何努力减小t c b ，t c b 也总是会存在的，因为系统所借助的任何工具、 方法都会在t c b 之内。因此，所能做的只是尽力减小t c b ，把复杂、易出错 的部分排除出t c b 。 1 1 4并行程序的安全性 以往已经有许多令人失望的经验表明：并行程序很难经受住非常仔细的检 查而没有在其中发现错误。因此，要确保并行程序执行了它所被期待的操作， 最为可靠的办法就是严格的证明并行程序确实这么做了。虽然已经有许多方法 被研究用来推理验证顺序和并行程序的性质( a p t ，1 9 8 1 ；f l o y d ，n d ；h o a r e ，1 9 6 9 ； l a m p o r t ，1 9 9 4 ；l a m p o r ta n ds c h n e i d e r ，1 9 8 4 ；o w i c k ia n dg r i e s ，1 9 7 6 ) ，但是这 并未使得确保并行程序的安全性变得简单，并行程序中的交互和干扰反而使得 推理过程变得非常复杂，也影响了其模块化验证的实现。而无法模块化验证将 使得应用于并行程序的验证方法缺乏实用价值。 3 绪论 在f r a n c e z 和p n u e l i ( f r a n c e za n dp n u e l i ，1 9 7 8 ) 开发了第一个用于模块化 验证并行程序的方法后，许多不同的方法也被提出用来处理并行程序模块 化验证的问题。这其中最具代表性的就是m i s r a 和c h a n d y 为消息传递系统 开发的a s s u m p t i o n c o m m i t m e n t 方法( m i s r aa n dc h a n d y ，1 9 8 1 ) 和j o n e s 为共享 内存程序开发的r e l y g u a r a n t e e 方法( j o n e s ，1 9 8 3 ) 。这两种方法在提出后即被 进行了更详细的研究( a b a d ia n dl a m p o r t ，1 9 9 3 ，1 9 9 5 ；c a ua n dc o l l e t t e ，1 9 9 6 ； f l a n a g a ne ta 1 ，2 0 0 2 ；h e n z i n g e re ta 1 ，2 0 0 2 ；o s s e f o r t ，1 9 8 3 ；p n u e l i ，1 9 8 5 ；s t a r k ， 1 9 8 5 ；s t i r l i n g ，1 9 8 8 ；x ue ta 1 ，1 9 9 4 ) 并常被统称为a s s u m e g u a r a n t e e 方法。 许多模型检查 器( c h a k ie ta 1 ， 2 0 0 4 ；d e m a r t i n ie ta 1 ， 1 9 9 9 ； f l a n a g a na n dq a d e e r ， 2 0 0 3 a ；g i a n n a k o p o u l o ue ta 1 ，2 0 0 2 ； h a v e l u n da n dp r e s s b u r g e r ，2 0 0 0 ；h o l z m a n n ，1 9 9 5 ) 也被研究用来验证并行程 序，但是它们都只能检查有限固定线程数的程序。c i r c 算法( h e n z i n g e re ta 1 ， 2 0 0 4 ) 虽然支持线程数目无限制的并行程序的检查，但它并没有模拟动态线程创 建的线程环境改变。3 v m c ( y a h a v ，2 0 0 1 ) 支持线程数目无限制且线程动态创建 的检查，但它并不是基于a s s u m e g u a r a n t e e 的方法，不支持模块化验证。 许多类型系统( f l a n a g a na n da b a d i ，1 9 9 9 a b ；f l a n a g a na n dq a d e e r ，2 0 0 3 b ； g r o s s m a n ，2 0 0 3 ) 也被研究用来推理并行程序。它们使用高阶逻辑来验证并行程 序的某些特定属性，如竞争、死锁、原子性等等。 近年来，o h e a r n 等( b o r n a te ta 1 ，2 0 0 5 ；b r o o k e s ，2 0 0 7 ；? ) 也开始使用分离 逻辑( s e p a r a t i o nl o g i c ) ( r e y n o l d s ，2 0 0 2 ) 来推理验证并行程序。 在这些研究当中，模型检查对程序的抽象使得实际运行的程序并未真正被 进行了验证；而类型系统一方面要通过限制自身的表达能力来确保其自动性， 另一方面类型系统所验证的程序属性的复杂度也决定了它实现的复杂度。因而 这两种方法在并行程序验证上的应用都受到了限制。 值得注意的是，虽然并行程序可以使用不同的方式进行多个线程间的交 互，如锁、原子区、条件变量等等，但是这些不同的交互方式都可以使用类似 锁方式的推理来进行推理验证。这是因为原子区可以被视为在全局资源上的加 锁和解锁，包括c p u 、内存、i o 外设等等。而条件变量本身就是锁或者锁的 一种细化。锁方式的验证推理方法在做出较小的改动后就可以直接应用于使用 原子区和条件变量的并行程序的验证推理。 虽然并行程序形式验证的研究已经给出了在存在交互和干扰下的程序的推 理方法，但这些方法对于一般的软件开发人员而言仍是非常难以掌握的，而且 实际应用中的负担开销也很大。而其他的方法在面对并行程序时，其作用和有 效性也都在下降。比如程序测试的方法，由于并行程序交互的不确定性，测试 中的错误并不总是在相同的外部测试条件下可再现的，这就给确定错误的来源 4 绪论 tcb 图1 1 ：p c c 框架 带来了极大的困难。程序分析同样因为并行交互的不确定性使得所需要分析的 信息呈指数增长，分析的成本代价大幅度提升。确保并行程序安全性的代价依 然高昂。 1 2携带证明的代码( p c c ) 携带证明的代码( p r o o f - c a r r y i n gc o d e ，简称p c c ) ( n e c u l a ，1 9 9 7 ) 是一个 通用框架，它允许代码生产者发布带有形式安全性证明的程序。携带证明的代 码要求其所携带的证明能够保障代码消费者所需求的安全策略，并且这些证明 可以被代码消费者自动地检查。这样，代码消费者就能够不需要信任代码生产 者而安全地运行其所发布的程序了。图l l 给出了p c c 的框架。p c c 代码包中 的可执行代码只需要在最初执行前被代码消费者进行一次检查，就可以在随后 的执行中和普通的代码样被调用，不再需要额外的检查，代码的执行效率并 没有任何损失。 与通常的代码不同的是，p c c 代码还携带了一个形式的安全性证明。该安 全性证明描述了程序语义的实现细节，执行代码的本地系统只需要检查证明与 代码是否匹配就可以知道代码是否值得信赖。代码生产者，往往也就是程序开 发人员，负责构造程序的安全性证明，安全性证明的构造过程就是程序语义的 理解过程，这虽然增加了程序员的负担，但却可以帮助程序员明确所表达的程 5 绪论 tcb 图1 2 - f p c c 框架 序语义，减小开发过程中出现错误的可能。同时，程序的安全性证明可以通过 计算机辅助半自动甚至是部分全自动地生成，一定程度上减轻了由构造安全性 证明带来的开发负担。 而代码消费者要安全地执行p c c 代码，就要通过安全策略描述本地的安全 需求，约束程序在本地系统上运行时的操作行为，确保本地系统的安全性不会 被代码生产者所提供的代码破坏。安全策略可以是对程序占用内存的大小的限 制，可以是对程序不修改本地系统某些环境的要求，或者是对程序行为必须满 足某些规范的约束等等。安全策略也必须由形式语言严格定义，这样才能够被 检查器用于检查其能否被代码生产者所提供的程序安全性证明所满足。 理论上，p c c 可以用于验证所有程序上的所有属性。而且它不需要加密、 认证等机制确保发布传输过程的安全性。被篡改的代码由于无法导出其自身的 证明而被代码消费者丢弃：仅篡改安全性证明也同样会由于无法通过检查而被 丢弃；面即便代码和安全性证明都遭到了篡改，如果用户的安全策略得不到满 足，代码依然会被丢弃。p c c 框架使得代码消费者仅需维持较小的t c b 就可 以获得较高安全性的可执行代码。 为进一步减小p c c 系统的t c b ，基础p c c ( f o u n d a t i o n a lp c c ，简 称f p c c ) ( a p p e l ，2 0 0 1 ；a p p e la n df e l t y ，2 0 0 0 ；c h e ne ta 1 ，2 0 0 3 ；h a m i de t8 l 1 ， 2 0 0 2 ；y ue ta 1 ，2 0 0 4 ) 的研究将安全策略中的验证推理系统排除出t c b ，同时 使用与检查器相同的基础逻辑搭建验证推理系统，并在基础逻辑上证明其可靠 性。图1 2 给出了f p c c 框架的概况。 6 绪论 由此，f p c c 可执行代码的安全性依赖于：1 ) 安全策略；2 ) 检查器；3 ) 执行代码的机器。这里安全策略要能够正确定义用户需求的安全性，否 则p c c 代码包中的证明就没有任何意义。而检查器则必须能够正确工作， 其所依赖的基础逻辑也必须正确。否则如果检查器的结果不准确，那依赖于它 的所有证明和安全策略就毫无意义了；而如果基础逻辑有错误，那么整个系统 就更没有什么安全性可言了。最后就是执行代码的机器要确保能够正常工作， 不会出现硬件故障以及操作系统错误等等。在t c b 之外的框架的其余部分，都 不再需要被信任。 在p c c 的相关研究中，s h a o 等人的f p c c 框架( f e n ga n ds h a o ，2 0 0 5 ； f e n ge ta 1 ，2 0 0 6 ；n ia n ds h a o ，2 0 0 6 ；y ua n ds h a o ，2 0 0 4 ；y ue ta 1 ，2 0 0 4 ) 采用 了逻辑语言作为程序规范，从而可以描述更为灵活和复杂的程序行为。他们使 用c a p ( c e r t i f i e da s s e m b l yp r o g r a m m i n g ) ( y ue ta 1 ，2 0 0 4 ) 和s c a p ( s t a c k - b a s e dc a p ) ( f e n ge ta 1 ，2 0 0 6 ) 完成了动态内存分配函数( m a l l o c f r e e ) 的安 全性证明( x i a n ge ta 1 ，2 0 0 6 ；y ue ta 1 ，2 0 0 4 ) 。在后继的研究中更使用s c a p 完 成了复杂的垃圾收集的验证( l i ne ta 1 ，2 0 0 7 ；m c c r e i g h te ta 1 ，2 0 0 7 ) 。最近，他 们还实现了用于验证带有硬件中断的抢占式线程模型的验证框架( f e n ge ta l l ， 2 0 0 8 ) 。 此外，c c a p ( c o n c u r r e n tc a p ) ( y ua n ds h a o ，2 0 0 4 ) 还支持多线 程程序的验证。c m a p ( c e r t i f i e dm u l t i - t h r e a d e da s s e m b l yp r o g r a m - r u i n g ) ( f e n ga n ds h a o ，2 0 0 5 ) 贝j j 在c c a p 的基础上支持线程动态创建的验证。 为将这些不同的验证框架统一到一个开放的平台中，s h a o 等人还开发 了o c a p ( o p e nc a p ) ( f e n ge ta 1 ，2 0 0 7 b ) ，进一步增强了f p c c 框架的实用 性。 1 3事务内存同步机制 事务( t r a n s a c t i o n ) ( g r a ya n dr e u t e r ，1 9 9 2 ) 是数据库系统中界定数据处理 逻辑单元的控制抽象，事务在允许共享数据并发存取的同时保证其自身满足 “a c i d ”语义； a t o m i c i t y ( 原子性) ：一个事务就是一个原子执行的操作序列，它要么 被完整地执行，要么完全不执行。如果一个事务成功地完成了它的所有操 作，它就提交( c o m m i t ) ，否则它就终止( a b o r t ) ，并且不产生任何效 果( e f f e c t ) 。 i s o l a t i o n ( 隔离性) ：事务在其提交之前不应让其他事务观察到它的执行 7 绪论 线程l线程2线程膏优先曩 线程鼍优先曩 i l o c ka i ：lock c - i !lockb i 1 0 c kc ： ii z 蚕 i i 一 i ：lock a j - 矗 l fi ： u n l o c kcl l o c kb ： ii 死锁优先级反转 图1 3 ：锁机制的隐患 效果。隔离性使得并发的事务执行变得可串行化( s e r i a l i z a b l e ) ，如同是 个一个顺序执行的。 c o n s i s t e n c y ( 一致性，) ：事务的原子性和隔离性确保了事务的正确执行 会将共享数据从一个一致的( c o n s i s t e n t ) 状态( 由具体的应用语义定 义) 转化到另一个一致的状态。 d u r a b i l i t y ( ，持久性) ：事务提交之后，其效果在随后的系统错误中也能 保留下来。 随着近年来并行程序需求的增长，管理并行程序中共享数据交互所使用 的传统的锁机制的缺陷已越来越突出：关联庞大数据结构的粗粒度( c o a r s e - g r a i n e d ) 的锁虽然使用简单，但通常会阻碍程序更好地利用多处理器优势，这 是因为线程在彼此间并无干扰的情况下也会相互阻塞( 如分别访问庞大数据结 构中的不同数据单元) ；而关联单个数据的细粒度( f i n e g r a i n e d ) 的锁虽然改 善了无干扰线程间相互阻塞的情况，但却极易引入死锁等导致程序执行进入异 常状态的隐患。 图1 3 说明了死锁和优先级反转这两种极易出现在锁机制中的问题给程序 执行带来的危害。如果线程1 和2 都需要锁a 和b 来执行操作，那么如图所示， 在线程1 获得锁a ，线程2 获得锁b 之后，两个线程都无法再获得所需要的另一 个锁来继续执行，死锁使得程序的执行陷于停滞。而优先级反转则使得高优先 级的线程不得不等待低优先级的线程先完成其操作，在低优先级的线程释放了 它所需要的锁之后才能够继续执行，严重地违反了关于优先级的定义。 在死锁等锁机制的隐患持续地困扰着程序员的同时，锁机制还严重地阻碍 8 绪论 初始 删除 插入 哈希表t l 哈希表t 2 二 二至 图1 4 ：锁机制程序合成的问题 了代码的合成( c o m p o s i t i o n ) 。能够正确交互的多个子程序所访问的数据如果 存在交集，那么这些子程序合成后，往往无法保证合成的程序是能够正确交互 的。而在程序合成中，子程序访问的数据存在交集的情况非常普遍。 一个简单的合成例子如图1 4 所示。对拥有线程安全的插入、删除操作的 哈希表，如果把项a 从表t 1 中删除，并将其插入到表t 2 中，那么就需要保证这 个操作的中间状态不被其他线程观测到，否则就会出现项a 既不在表t 1 中也不 在表t 2 中的情况。但是除非哈希表的实现者预料到了这种情况，否则这种中间 状态往往都能被其他线程所察觉。然而即便这种情况被预料到了，哈希表的设 计者所能做的也只是将哈希表内部对表进行加锁和解锁的操作公开出来，这样 不仅会破坏哈希表的抽象，还会引入死锁等隐患。因而无法由安全的插入、删 除操作合成出更复杂的安全操作。 于是并发控制机制的研究者们就开始借鉴数据库系统中事务的概念，提出 了崭新的并发控制机制：事务内存( t r a n s a c t i o n a lm e m o r y ) 同步机制。 1 3 1事务内存系统的系统实现的相关研究 提供事务内存同步机制的系统( 本文的剩余章节中将简称为“事务内存系 统”) 需要为程序员提供相应的编程结构( 事务) 编写并行程序代码，并自动 地管理编程结构中所包含的共享数据的交互。 h e r l i h y i g lm o s s 最早在硬件上实现了事务内存系统( h e r l i h ya n dm o s s ， 1 9 9 3 ) 。他们的事务内存系统强调事务是具有可串行性( s e r i a l i z a b i l i t y ) 和原 9 绪论 子性( a t o m i c i t y ) 的有限机器指令序列。可串行性是指并发事务仿佛是串行执 行的，一个事务绝不会与另一个事务交错执行，已提交的事务绝不会在不同的 处理器上呈现出不同的执行顺序。原子性的定义则和数据库系统的原子性定义 相同。 为了能够更加灵活地选择不同的同步机制，s h a v i t 和t o u i t o u 随后通 过软件的方法实现了事务内存系统( s h a v i ta n dt o u i t o u ，1 9 9 5 ) 。他们依循 了h e r l i h y 和m o s s 对事务可串行性和原子性的定义。 之后，许多研究相继探讨了事务内存系统在硬件中( a n a n i a ne ta 1 ， 2 0 0 5 ；h a m m o n de ta 1 ，2 0 0 4 ；m o o r ee ta 1 ，2 0 0 6 ) ，在软件中( h a r r i sa n df r a s e r ， 2 0 0 3 ；h a r r i se ta 1 ，2 0 0 5 ；h e r l i h ye ta 1 ，2 0 0 3 ) ，甚至是在软硬件结合的方法 中( d a m r o ne ta i ，2 0 0 6 ；s a h ae ta l ，2 0 0 6 ) 的各种实现策略。而事务内存系统 对事务的性质的定义也逐渐转化为了现在的原子性( a t o m i c i t y ) 和隔离性 ( i s o l a t i o n ) 。数据库系统“a c i d ”