（计算机软件与理论专业论文）用形式化方法构建安全的线程机制.pdf

摘要 摘要 并发系统的安全性随着其流行程度的增加，显得日益重要。以往在这方面大 多数研究的重点是，在并发机制的实现( o s ，线程库) 已经安全的假定下，如何 保证并发程序本身的安全性。对于如何保证并发机制本身的安全性，目前的解决 方案不是不完整，就是非常复杂。到了如今，大多数并发机制的实现者仍然主要 依赖传统的动态测试方法来保证代码的安全性。 为了探索如何用形式化验证的方法来保证并发机制本身的安全，本文中设计 了一个类似g n up t hl i b r a r y 的用户级别线程库，并用类m i p s 的汇编语言编写了 它的一个实现。与通常的线程库不同的是，该线程库携带了安全规范及其证明。 这些规范与证明保证，如果用户程序对该线程库a p i 的调用始终满足规范，那么 线程库的代码必然可以安全执行。更重要的是，从这些规范与证明不仅能得到线 程库本身的安全性，还能得到线程库和用户程序交互的安全性。为了让本文的验 证方法可以用于更复杂的代码，文中还提出了一些简化程序规范和降低证明代价 的方法。 本文中的所有形式化工作，都是在证明辅助工具c o q 上完成的。对于本文提 出的线程库，其安全性证明可以用机器检查。而该线程库的安全性，仅仅依赖于 证明检查工具的正确性，这意味着它是一个携带证明代码包( p c cp a c k a g e ) ，可以 直接用于对安全性要求非常高的场合。 关键词：软件安全、并行系统、线程库、携带证明代码、形式化证明方法 a b s t r a c t a st h ea p p l i c a t i o no fc o n c u r r e n c ts y s t e m si s w i d e l ya c c e p t e d ，t h e i rs a 士e t y 1 s g r o w m gm o r ea n dm o r ei m p o r t a n t m o s t o ff o r m e rr e s e a r c hf o c u s e do nh o wt o g u a r 拟e et h et h es a f e t yo fc o n c u r r e n tp r o g r a m sw i t h t h es a f e t yo ft h ei m p l e m e n t a t l o n f o rc o n c u r r e t a tm e c h a n i s m s t r u s t e d r e s e a r c ho nt h es a f e t y o ft h ec o n c u r 。e n t m e c h a n i s m st h e m s e l v e sw a se i t h e r b a s e do n a no v e r - a b s t r a c t e dm o d e it o m a k et h e r e a s o n i n gi m p r a c t i c a i o rr a t h e rc o m p l e x a n dn e e dv e r yt e d i o u sp r o o t h i s1 sw h yw e s t i l lu s et h ep r a c t i c a ld y n a m i ct e s t i n ga st h em a j o rw a y t oe n s u r et h es a f e t yo fo p e r a t i n g s y s t e m so rt h r e a dl i b r a r i e s w ea r ee a g e rt os e et h a tt h ef o r m a lr e a s o n i n gc a nb eu s e dm o r em r e a l 。w o r l d c o n c u f r e n ts y s t e m s ，a n dt h i sp a p e ri s as o li ds t e pt o w a r d so u rg o a l i nt h i sp a p e r ，w e p r o p o s ea v e r i f i c a t i o nf r a m e w o r kf o rl o w - l e v e lc o d er e a s o n i n g ，a n du s e 1 tt op r o v et h e s a f e t vo fat h r e a dl i b r a 哕。t h el i b r a r yi s r u n n a b l eo nr e a lp h y s i c a lm a c h l l i e s a n dt h e c o m p l e x i t yo fp r o o f o n o u rf r a m e w o r ki sm u c hl e s st h a nt h a to f o t h e s i m i l a rf r a m w o k s m o r ei m p o r t a n t l y ，w ep r o v en o tj u s tt h es a f e t yo f t h el i b r a r yi t s e l f , b u ta l s ot h es a f e t yo f t h ei n t e r a c t i o nb e t w e e nt h el i b r a r y a n di t sc l i e n t s t om a k eo u rf r a m e w o r km o 。e a p p l i c a b l e o nm o r ec o m p l i c a t e dc o d e ，w e a l s od om u c hw o r ko ns l m p l i f y i n gt h e p r o g r a ms p e c i f i c a t i o na n dr e d u c i n g t h ec o s to fp r o o f ： a i lf o r m a lw o r ki nt h i sp a p e ri si m p l e m e n t e di nt h ec o q p r o o fa s s l s t a n t i tm e a n s t h a tt h es o u n d n e s sp r o o fo fo u rf r a m e w o r k a n dt h es a f e t yp r o o fo ft h e1 i b a r yi sm a c h l n e c h e c k a b l e t h e i rs a f e t ya l s od o e sn o tr e l yo na n yc o m p i l e r s ，m a k i n g o u rt h r e a dh b a r ya p r o o f - c a r r y i n gc o d ep a c k a g e ，w h i c hc a n b ed i r e c t l yu s e di nt h es y s t e m sw h e r e t h es a f e t y p r o p e r t yi sv e r yc r i t i c a l k e y w o r d s ：s 。脚a r es a f e t y ，c 。n c u r r e n t s y s t e m s ，t h r e a dl i b r a 哦p r o o f - c a r 巧i n g c 。d e f o r m a lm e t h o d i i i 中国科学技术大学学位论文原创性声明 本人声明所呈交的学位论文，是本人在导师指导下进行研究工作所取得的 成果。除已特别加以标注和致谢的地方外，论文中不包含任何他人已经发表或 撰写过的研究成果。与我一周工作的同志对本研究所傲的贡献均已在论文中作 了明确的说明。 作者签名：矗i 童i签字目期：至翌兰墨：上 中国科学技术大学学位论文授权使用声明 作为申请学位的条件之一，学位论文著作权拥有者授权中国科学技术大学 拥有学位论文的部分使用权，即：学校有权按有关规定向国家有关部门或机构 送交论文的复印件和电子版，允许论文被查阅和借阅，可以将学位论文编入有 关数据库进行检索，可以采用影印、缩印或扫描等复制手段保存、汇编学位论 文。本人提交的皂子文档的内容和纸质论文的内容相一致。 保密的学位论文在解密后也遵守此规定。 出开口保密( 年) 作者签名：堑重量 签字日期：兰竺里! ：2 导师魏匿主雪 婵日期：亟卜 第l 章绪论 第1 章绪论 1 。1 研究背景和意义 并发执行的代码在目前的软件工业中占据了越来越大的比例。并发代码的安 全性，比起顺序代码来更加重要，也更加难以保证。并发系统里的某个进程或线 程一旦出错，很可能影响其他的进程或线程，甚至破坏整个系统。并发系统里往 往会出现一些顺序执行的程序里不存在的错误，例如数据共享造成的同步错误。 这类错误相对于来说更难查找和排除，因为并发系统里各个程序的执行结果一般 都依赖于其执行顺序，某些错误很有可能在较长时间内无法重现，以至于无法有 效调试! 人们希望从根本上提高并发代码的安全性，而不是仅仅依赖人工的调试排错 手段。在这方面，学术界和工业界已经提出了很多解决方案，例如消息传递模型， 事务内存，模型检查等等。然而对于并发系统的基本单元，即进程或线程，一般 采取的方法是将其操作抽象成一组a p i ，如创建，销毁，同步原语，并假定这些 a p i 已经符合相应规范。这种假定一旦不成立，即进程或者线程机制本身出了问题， 那么就算建立在它们之上的应用程序已被确定是安全的，整个系统也不安全。 总体来说，保证进程或者线程机制本身的安全性，有两种方法：类型系统和 程序验证。前者的主要问题是底层的很多性质很难纳入类型系统能推理的范畴。 后者的主要问题是它需要程序员来书写安全规范，并且通常对这些规范的证明也 难以自动完成，这增加了程序员的负担。下面对这两种方法的主要相关研究现状 进行一些简要分析，并指出它们各自的优点和不足。 1 2 研究现状 本节将分两部分介绍现今国内外基于类型系统和程序验证来提高底层并发程 序的安全性的相关研究工作。通过这些工作的调研和比较，提出目前这些领域存 在的问题以及未来的发展方向。 对于如何保证并发机制的实现的安全性，已经有一些很有意义的研究。远在 8 0 年代，b e v i e r 就使用b o y e r - m o o r e 逻辑验证了一个叫做k i t l 】的操作系统内核， 该操作系统和现代的操作系统差别较大。德国的v e r i s o f t 项目为验证操作系统建立 了一个完整的框架，称为c v m 【2 】。然而到目前为止，该项目的论文没有明确提到 如何保证在c v m 之上运行的应用程序和操作系统内核连接在一起之后，整个系统 仍然安全。微软研究院的s i n g u l a r i t y 项目致力于用安全的编程语言( c 群的变种) 第l 章绪论 来开发系统，然而该操作系统仍然有很大部分依赖于c 拌的不安全特性。n i 证明了 一个用户级线程库的安全性。由于在证明过程中用到了对通用代码的指针的推理， 并且采用了很复杂的方式来编码非直谓多态和递归谓词，整个线程库的规范和证 明花费了很大的代价，从而让这种方法不适合用于验证较大的系统。 1 2 1 基于类型系统的并发系统安全研究 近年来，基于类型系统的安全并发系统主要是微软研究院的s i n g u l a r i t y 项目， 以及其他一些用类型安全的高级语言来编写操作系统的项目。使用类型系统的主 要优点是类型检查一般是全自动的，程序员需要为安全性付出的额外代价较小。 其主要问题是类型系统的表达能力有限，其安全规范就是类型本身。另外类型安 全的语言通常不能用于编码操作系统的所有部分，其中内存的显式管理和硬件相 关的代码，仍然需要用c 和汇编这样的不安全语言来编写。 1 s i n g u l a r i t y 微软研究院的s i n g u l a r i t y t 3 是一个微内核的操作系统，其内核的 主要部分的实现语言是c 撑的一个扩展版本s i n g # ，s i n g # 是一个并发编程语言，它 在c 撑的基础上增加了信道( c h a n n e l ) 和低级语言的一些特性，使操作系统的一部分 最底层代码也可以用它实现。s i n g # 是类型安全的，并且其消息传递原语的语义是 形式化的协议定义好的。 s i n g u l a r i t y 的进程都运行于同一地址空间，它们之间不通过硬件机制隔离，而 通过加载进程之前的静态检查事先保证互不干扰。s i n g u l a r i t y 仍然包含一定的汇编 和c c + + 代码，用于中断处理和硬件抽象层。这些代码的安全性并没有保证，整 个系统建立在这些代码没有错误的假定上。 2 其他类似项目：j n o d e t 4 和j x 5 】是两个基于j a v a 的操作系统，和s i n g u l a r i t y 类似，它们的主要部分都是用类型安全的高级语言编写的。它们也依赖于一定的 非类型安全语言所编写的代码。s i n g u l a r i t y 、j n o d e 和j x 不使用硬件保护，而使用 语言层次的安全机制来达到保护内核数据和进程间隔离的目的，这类项目统称为 基于语言的系统( 1 a n g u a g e b a s e ds y s t e m ) 。 o s k e r l 6 】是一个l 4 微内核实现，其主体部分用h a s k e l l 编写。o s k e r 不是基于 语言的系统，它的保护仍然通过隔离地址空间来实现。o s k e r 依赖于h a s k e l l 的 r u n t i m e 以及很多用c 编写的底层支持代码。o s k e r 用一个叫p 1 0 9 i c 的断言语言为 其h a s k e l l 代码写上了注释和规范，但是其论文上没有提到如何证明它们。h o u s e r l 是o s k e r 的一个演示版本，它不是微内核结构，并依赖更多的h a s k e l lr u n t i m e ，比 如其多线程支持。 1 2 2 基于程序验证的并发系统安全研究 用基于程序验证的手段提高并发系统的安全性，其基本思路是使用原本并非类 2 第l 章绪论 型安全的语言，如c 和汇编等来实现并发系统，然后用某种程序逻辑来证明用这 些不安全语言编写的代码本身是安全的。k i t 操作系统在8 0 年代就在这方面做出 了最初的尝试。目前，基于程序验证的安全研究项目主要是v e r i s o f tx t 8 1 ，f l i n t 【9 l 和a u s t r a l i an a t i o n a li c t 1 们。 1 k i t - k i t 由b r b e v i e r 提出，实现并验证。它是一个小型的多任务操作系统， 用汇编语言实现。其内核提供如下功能：进程调度，错误处理，消息传递，以及 异步设备接口。以上模块的安全性，例如普通用户无法修改这些模块的数据，也 无法通过这些模块进入特权级别等，均通过b o y e r - m o o r e 逻辑验证，其证明用 b o y e r - m o o r e 定理证明器检查正确。k i t 与现代的操作系统的基本概念和结构相差 较大，并且作者没有明确说明是否验证了其他一些重要性质，例如内存分配和同 步机制是否安全。 2 v e r i s o f l 项目：该项目提出一整套的验证框架，来验证一个可实际运行的操 作系统原型。该操作系统的所有进程都运行在一组叫c v m ( c o m m u n i c a t i n gv i r t u a l m a c h i n e s ) 的抽象机器上。操作系统的主要部分用c 的子集c 0 1 i 】编写，其验证框架 证明了c o 上的程序逻辑( h o a r el o g i c ) 可以翻译成编译之后的汇编语言上的程序逻 辑。然而到目前为止，该项目的论文尚未明确提到如何保证在c v m 之上运行的应 用程序和操作系统内核连接在一起之后，整个系统仍然安全。 3 m t h ：f l i n t 项目组用基于p r o p x 的汇编语言验证框架【1 2 】( p r o p x b a s e dc e r t i f i e d a s s e m b l yp r o g r a m m i n g ，简称x c a p ) 证明了一个用户级线程库m t h ( m i n i t h r e a d l i b r a r y ) 1 1 3 】的安全性。该线程库和g n up t ht h r e a dl i b r a r y t l 4 】类似，可分为两层，下 层提供上下文切换，创建和销毁的接口，上层使用这些接口实现线程的切换，创 建和销毁。m t h 的所有代码的安全性证明都通过了机器检查。x c a p 为了支持通用 代码指针的模块性验证，使用了很复杂的方式来编码非直谓多态和递归谓词，使 得整个线程库的规范和证明需要花费很大的代价。对于较大的系统，这种方法由 于代价过高而不够实用。 4 n a t i o n a li c t 的l 4 1 1 5 j 验证项目：澳大利亚的n a t i o n a li c t 试图用i s a b e l l e t l 6 】 验证他们的一个l 4 实现，其硬件平台是a r m ，实现语言是c c + + 和汇编。其规 范和证明已经基本完成。它的主要特点是机器内存和实现语言的模型精确，并对 中断和分页机制也做了验证。目前该项目的代码和技术细节没有公开，开发者的 论文上也没有提到详细的底层代码的形式化验证过程。 1 3 本文工作与贡献 为了探索如何用形式化验证的方法来保证并行机制本身的安全，笔者在本文 中设计了一个类似g n up t hl i b r a r y 的用户级别线程库，并用类m i p s 的汇编语言 第1 章绪论 编写了它的一个实现。与通常的线程库不同的是，该线程库携带了安全规范及其 证明。这些规范与证明保证：如果用户程序对该线程库a p i 的调用始终满足规范， 那么线程库的代码必然可以安全执行。更重要的是，从这些规范与证明不仅能得 到线程库本身的安全性，还能得到线程库和用户程序交互的安全性。为了让本文 的验证方法可以用于更复杂的代码，文中还提出了降低证明代价的一些方法。 本文的主要贡献有： 1 本文设计、实现并验证了一个可以实际运行的线程库，本文中线程库的线 程模型与f l i n t 项目组的m t h 类似，其安全性在本质上也与m t h 的安全性是类似的。 然而本文对安全规范的形式化与m t h 完全不同。m t h 只使用一个程序逻辑，该程 序逻辑既被用来证明线程库本身的安全性，又被用来证明线程库与用户程序交互 的安全性。这导致程序逻辑过于一般化，因而给规范与证明带来很多不必要的复 杂性。本文对使用两个不同的程序逻辑分别证明线程库的安全性以及交互的安全 性。本文的两个程序逻辑和m t h 采用的程序逻辑一样，都能完整地表达线程库及 它与用户程序交互的正确性，然而在这两个程序逻辑之上的规范编写与证明构造 却比m t h 的做法简单得多。 2 和通常对算法正确性或程序性质的验证不同，本文的证明相当严格。本文 的证明基于归纳构造演算，只使用了归纳构造演算【1 7 】所提供的推理规则。本文的 证明最终以证明项的形式保存起来，并且通过了证明辅助工具c o q t 博】的证明检查。 如果信任归纳构造演算的一致性与c o q 提供的证明检查工具的正确性，那么可以 认为本文的证明不存在任何错误。 3 由于本文的证明在汇编层次完成，线程库的安全性并不依赖于编译器是否 正确。用户在使用该线程库时，只需要将代码及其携带的规范证明送给证明检查 工具。若证明通过了检查，那么该线程库必然是安全的。代码若在传输过程中被 篡改而不符合规范，其证明将无法通过最终的检查。因而该线程库本质上是一个 典型的携带i , y n 男代码包【 9 ( p c cp a c k a g e ) ，它可以用于对安全性要求非常高的场合。 4 本文提出对汇编代码的形式化证明的简化方法。该方法原则上不限于线程 库或调用线程库的用户程序，而是一个对于简化验证汇编代码的通用方法。该方 法稍加修改即可用于简化许多其它的验证工作，例如c 的内存管理库与垃圾收集 器等。 5 本文对线程库的验证过程，实际上就是将线程库的行为形式化的过程。将 线程库的行为形式化，除了向用户保证了线程库的安全性，还为程序员理解线程 库的工作过程提供了帮助。众所周知，在实现如线程库这类底层系统程序时，程 序员始终需要对系统的整个运行过程有相当透彻的理解，而目前这种理解通常是 经验的积累。笔者认为，总结出如何将运行过程形式化并将其用于教学，可以加 快和加深新系统程序员对系统程序的理解。因此本文的工作成果不仅有利于系统 4 第l 章绪论 程序的安全性，还有利于程序员对系统程序的认识。 1 4 章节安排 第二章介绍本文工作所需的基本设定和主要技术。这一章的介绍主要分为四个 部分：一是关于归纳构造演算( c a l c u l u so f i n d u c t i v ec o n s t r u c t i o n ，简称c i c ) 及其对 应的证明工具c o q ，c i c 用于形式化本文中的所有工作，c o q 用于实现这些形式化 的逻辑表达式，并用于证明本文中的所有定理，包括框架的可靠性，线程库本身 的安全性以及线程库与调用者交互的安全性。二是基于m i p s 体系结构1 2 0 】的抽象 机器模型，包括对内存和c p u 的抽象。三是关于并发程序的形式化方法的介绍， 其中包括假设一保证推理方法 2 q ( r e l y - g u a r a n t e er e a s o n i n g ) 以及并发分离逻辑 2 2 1 ( c o n c u r r e n ts e p a r a t i o nl o g i c ) ，并比较了两者在抽象层次，表达能力和推理代价 上的优劣。四是关于基于语法的基础携带证明代码技术【2 3 ( s y n t a c t i ca p p r o a c ht o f o u n d a t i o n a lp r o o fc a r r y i n gc o d e ) ，本文介绍其基本思想，如何将控制栈抽象成数 学模型，如何实现假设保证推理方法以及如何将用不同的f p c c 框架验证的代码 模块连接在一起，并保证整个代码的安全性。 第三章描述一个简单的线程库，该线程库基于g n up t hl i b r a r y ，并对其作出一 些必要的简化。这一章包含线程库的a p i ，线程模型与核心数据结构，及其实现简 要。 第四章描述该线程库的规范与证明。线程库的规范可以分为两层：接口规范 与实现规范。该章节详细讨论两种规范的区别，以及如何通过实现规范来证明接 口规范。本章还包括笔者在实现本文工作时发现的简化证明的方法。该方法通过 限制规范形式的方法消除了证明中的重复部分，并给出对于汇编指令的通用证明 结构。 第五章是对本文实用价值的分析。在这一章讨论本文中所说的“安全性证明” 在实践上到底指什么，以及证明好的代码到底有多大的可信度。 第六章比较相关工作，第七章总结全文，并讨论本文的后续工作方向。 在研究过程中，笔者对大量相关研究文献进行了分析理解，学习了相关的程序 设计和逻辑知识。在实现过程中，笔者还对基于类型论的定理证明辅助工具及其 理论基础进行了学习和调研。 本文涵盖笔者的研究内容、研究过程和研究过程中积累的经验。笔者认为， 形式化验证方法在现实的并行系统中应该得到更多的应用，而本文介绍的工作正 是以此为目标。从已经取得的成果看来，本文的工作朝着该目标迈出了坚实的一 步。 第2 章基本设定与主要技术 第2 章基本设定与主要技术 这一章介绍本文采用的主要技术及其原理。首先介绍用于形式化本文所有工作 的归纳构造演算及证明辅助工具c o q ，然后介绍验证线程库所需的抽象机器模型。 本章还介绍程序的两种形式化方法：假设- 保证推理方法( r e l y - g u a r a m e er e a s o n i n g ) 以及并发分离逻辑( c o n c u r r e n ts e p a r a t i o nl o g i c ) 。最后本章介绍基于语法的基础携 带证明代码技术( s y n t a c t i ca p p r o a c ht of 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 ) 。 2 1 归纳构造演算与证明辅助工具c o q 本节介绍本文中所有形式化的基础：归纳构造演算，以及证明辅助工具c o q 。 c o q 实现了归纳构造演算，另外还提供了一套用于自动构造证明项的策略语言 ( t a c t i cl a n g u a g e ) 。 2 1 1 归纳构造演算 构造演算( c a l c u l u so f c o n s t r u c t i o n s ，简称c c ) 是类型化l a m b d a 演算的一种， 按照b a r e n d r e g t 的分类，它位于l a m b d a 方块的远端右上角。也就是说它的类型系 统中包含多态、类型算子、以及依赖类型。构造演算通过c u r r y h o w a r d 同构，可 以对应成高阶构造逻辑。公理集合论中的任何集合也都可以很容易地对应成构造 演算里的类型。构造演算本身是类型化l a m b d a 演算，因此同时也可以当成一种静 态强类型的函数式编程语言来使用。 归纳构造演算( c a l c u l u so f i n d u c t i v ec o n s t r u c t i o n s ，简称c i c ) 在构造演算的基 础上增加了对自定义归纳数据类型和受限的不动点算子的支持。归纳数据类型和 受限不动点算子均可以在构造演算里直接编码，但是其编码过程较为繁琐，并且 无法区分在传统函数式语言里同构但是不同名的归纳数据类型。归纳构造演算的 自定义归纳数据类型和受限不动点算子与传统函数式语言里的自定义数据类型和 通用不动点算子用法非常接近。而自定义归纳数据类型本身也可以通过 c u r r y h o w a r d 同构对应成归纳定义的逻辑表达式。 c i c 使用s e t 表示通常数据结构的全域，p r o p 表示命题的全域。这种划分是 人为的，其目的是为了c o q 的程序抽取( p r o g r a me x t r a c t i o n ) 不会出现问题。读 者可以粗略地认为s e t 与p r o p 同构，s e t 中的元素是平时编程使用的数据结构类 型，而p r o p 中的元素是命题。 本文使用归纳构造演算来形式化机器模型及其操作语义。本文还用把机器上 的汇编指令编码成机器状态上的转换函数的方法，将线程库的汇编实现也编码成 6 第2 章基本设定与主要技术 归纳构造演算的表达式。 c i c 和其它的l a m b d a 演算一样，使用fxy 来表示以参数x ，y ，对f 的调用。本文在使用归纳构造演算来编码机器模型、断言语言和程序逻辑时，使 用这种表示方法。但是在某些场合，本文为了将概念抽象化和一般化，而不仅仅 局限于c i c ，采用通常的数学表达式( x ，y ，) 。读者可以直接忽略这两种表达方 式的区别。 2 1 2 证明辅助工具c o q c o q 是一个证明辅助工具( p r o o f a s s i s t a n t ) ，目前版本为8 2 。c o q 内部包含一 个程序设计语言和一个策略语言。其程序设计语言称为g a l l i n a ，g a l l i n a 的核心即 归纳构造演算。g a l l i n a 在纯归纳构造演算的基础上增加了一套和o c a m l 类似的模 块系统。因为归纳构造演算中可以很容易地构造出存在类型，因此该模块系统并 没有像在o c a m l 里那样增加了整个语言的表达能力。但是由于g a l l i n a 提供了对模 块系统的语法支持，使用其内建的模块系统比手工打包和解包存在类型要更为方 便。使用g a l l i n a 编写的程序可以通过c o q 提供的程序抽取工具翻译成合法的 o c a m l 3 1 】或是h a s k e l l 【3 2 】程序，然后通过这些语言的编译器编译成高效的可执行代 码。 在c o q 中，证明一个定理等价于构造出该定理所对应的类型里的一个l a m b d a 项。为了构造该l a m b d a 项，有两种方法。第一种方法是直接用g a l l i n a 语言将l a m b d a 项写出，般来说这种方法仅限于证明简单的命题，因为手工构造l a m b d a 项对于 较复杂的类型，即使有可能，也非常困难。第二种方法是进入c o q 的交互证明模 式，c o q 显示出当前的类型上下文，以及当前需要证明的目标( g o a l ) 。程序员根据 c o q 给出的这些信息决定当前使用什么样的证明策略。输入证明策略后，c o q 根据 该策略构造出证明项的一部分，并输出新的上下文和目标。当整个证明项构造出 来之后，c o q 将其保存，然后离开交互证明模式。 c o q 内建的证明策略比较简单。其基本的自动化证明策略a u t o 和e a u t o 类似于 p r o l o g 的h o r n 子句消解，只能处理简单的证明项。为了证明一个复杂的定理，其 证明策略的序列也会较长。更严重的问题是，由于每条证明策略和当前证明目标 密切相关，其他人无法通过只阅读证明策略序列的方法来理解证明过程。当命题 被修改时，其证明的修改与维护也相当困难。 为了解决该问题，通常采用的方法是类似自动定理证明器采用的决策过程 ( d e c i s i o np r o c e d u r e ) 。决策过程是根据命题的形式来自动构造证明的算法。程序员 可以通过阅读该算法来理解证明方法。除了g a l l i n a 外，c o q 还提供了让程序员编 写决策过程的语言，称为策略语言l t a c 。l t a c 是一个动态类型语言，允许程序员 按照写平常的算法的方法来编写决策过程，而不需要受g a l l i n a 里关于终止性和类 7 第2 章基本设定与主要技术 型系统的限制。由于l t a c 只在构造证明项时用到，其是否终止或者是否会出现运 行时错误并不影响c o q 进行定理证明时的可靠性。l t a c 并不保证一定会终止或者 一定不出现运行时错误，因为构造出来的证明项最终要在g a l l i n a 里通过类型检查。 只要证明项通过了类型检查，那么无论它是手工编写，通过策略序列产生，还是 用l t a c 自动构造出来，都可以认为它是可靠的。这一点对于c o q 的可靠性非常重 要，因为通常的自动定理证明器只会根据输入的命题输出“正确 、“错误或是 “无法证明 ，或是以证明步骤的方式输出证明过程，而并不构造证明项。对于 这些自动定理证明工具，用户必须信任其所有决策过程的算法与实现，其决策过 程越多越复杂，可靠程度越低。在c o q 里，l t a e 编写的决策过程是否出错没有关 系，用户之需要信任其类型检查器即可。因此程序员可以任意扩展c o q 的决策过 程，而无须担心证明的可靠性。 a g d a p 3 - 与c o q 非常类似，也基于类型化l a m b d a 演算与c u r r y h o w a r d 同构。 a g d a 对程序开发和规范编写的支持比c o q 强大，然而对自定义决策过程的支持则 不够。本文的线程库证明较为复杂，需要自定义大量的决策过程，因而采用c o q 作为主要开发工具。 2 2 抽象机器模型 本文的抽象机器是在r i s c 体系结构的m i p s 3 2 的基础上的简化模型。抽象机 器包含c p u 与内存。c p u 有3 2 个通用寄存器r ，一r 3 2 ，以及指令地址寄存器p c 。 遵循m i p s 命名规则，r 。又称为z e r o ，r ，称为a t ，r ：一r ，分别称为v 。一v 。，r 4 - r ， 分别称为a o - a ，r , - r 。分别称为t o - t ，r ，；到r z 3 分别称为s 0 - s 7 ，r 2 4 - r ：；分别 称为t 。一t ，r ：；一r ：，分别称为k o - k 。，r 2 , 称为g p ，r ：，称为s p ，r ，。称为s 。，r ，。 称为r a 。为简单起见，用c i c 的无穷精度自然数表示机器字，内存地址按l 对齐。 每个寄存器在c i c 里被编码为一个机器字，内存在c i c 里则编码为地址到机 器字的有限部分映射。在实际机器中，机器指令本身也存放在内存里。指令使用 机器字来编码。由于不考虑自修改代码，存放代码的内存块视为只读。机器指令 是m i p s 指令的一个子集，包含基本的加减，内存读写，以及控制流指令。图1 中的指令足以用来编写本文的线程库。本文将存放指令的内存块编码为机器字到 指令的部分映射，即代码堆。这可以让验证过程忽略指令是如何编码成机器字的。 整个抽象机器p 表示为二元组( c ，s ) ，其中c 表示代码堆，s 表示机器状态。 s 表示为三元组( h ，r ，p c ) ，其中h 表示可变内存，即数据堆，r 表示寄存器文件， 即从3 2 个寄存器号到3 2 个寄存器的完全映射，p c 表示代码指针。 第2 章基本设定与主要技术 ( p r o g r a m ) p ：= ( c s ) ( c o d e h e a p ) c ：= f 1 r ( s t a t e ) s ：= ( 盈：程，p c ) ( m e n u ) r y ) 匿 ：= 1 w ) ( r e g f i l e ) 交 ：= rmw 。 ( r e g i s t e r ) r ：= 磁产 o 叫 ( l a b e l s ) 士，1 p e ：= _ r l ( n a t 聆l f m s ) ( w o r d ) w ：= i ( b i t e g e r s ) ( 1 n s t r ) t：= a d d ur d r sr tla d d i ur dr s w ls u b u r d k r tis u b i u r dr s w l m o v er dr jll ir d 譬 | 1 wr tw ) l 8 wr tw ( r s ) lb e ql sr tf | b g t zr sf ijf | j a l 士| j r 瓦 f i g 2 1e l t c o d m go f t h ea b s t r a c tm a c l m t e 代码堆的抽象层次仍然较低，里面存放的是单独的指令，在汇编层次，程序员 通常会有“指令序列”的概念。这里将指令序列表达为一串以无条件跳转结尾的 连续存放的指令。用c ( f ) 表示从代码堆的地址f 处取出一串指令序列。 在该抽象机器p 上，将操作语义定义为以指令为参数的，两个状态之间的转 换关系。本文用p 一 p ，表示单步转换，p 一 。p ，表示k 步转换，p 。p ，表示转换 的自反和传递闭包。 机器模型的部分操作语义可见下表，其中h ( 1 ) 代表从内存h 的l 地址取出的 值，r ( r ) 代表从寄存器文件r 的第r 号寄存器取出的值。h 1 一 v ) 表示将内存h 里1 地址的值换成v 后得到的新内存。r r 。 v ) 表示将寄存器文件的r 号寄存器 里的值换成v 后得到的新的寄存器文件。其c o q 实现见本实验室项目组的主页1 2 8 1 。 9 第2 章基本设定与主要技术 ( c ，( h ，r ，p c ) ) h ( c ，n e x t c c 昨j ( h ，r ，p c ) ) 全 i ft = c ( p ct h e nn e x t t ( h ，r ，p c ) = a d d ur dr s ( h ，r r d r ( r s ) + i v r t ) ) ，p c + l w i t ，w ( r s )( h ，r r t - - h ( r ( r o + w ) ) ，p c 4 1 wi t ，w ( r s ) ( h r ( r s ) + 坩r ( r t ) ) ，r ，p c + l b e qr s ，r t ，f( h ，r ，p c + 1 ) i f r ( r , ) r ( n ) ( h ，r ，0 i fr ( r s ) = r ( n ) j a lf( h ，r r a - p c + 1 ) ，f ) j rr( h ，r ，r ( f ) ) 对于不熟悉m i p s 体系结构的读者，在这里略微说明：m i p s 没有硬件直接支 持的堆栈操作。其函数调用般通过j a l 指令进行。j a l 指令将下一条指令的p c 保存在寄存器r a ，而不是堆栈里。函数返回一般通过j rr a 来实现。对于嵌套的 函数调用，需要程序员自己维护一个软件堆栈，来保存函数参数与r a 的值。 2 3 并发代码的推理方法 本节介绍两种并发代码的推理方法，即假设保证推理方法和并发分离逻辑。 本文主要采用第一种推理方法。 2 3 1 假设一保证推理方法 假设保证是一种常见的验证并发程序间共享数据的方法。在这种方法里，每 个线程的规范需要描述它对共享数据的期望( 即假设条件) ，说明它认为其他所有 线程应该对这些共享数据作出什么样的改动。每个线程的规范还描述线程本身对 共享数据作出什么样的改动( 即保证条件) 。验证过程也就是对每个线程，证明其 他所有线程的保证条件均能蕴含该线程的假设条件。非形式化地说，对于任意一 个线程，若所有其他线程作出的保证都能满足该线程对它们行为的期望，那么就 可以认为所有线程的并发执行时安全的。由于任何一个线程的假设条件都是对于 除开该线程之外的所有线程的描述，因此需要验证的规范数量只和线程数量成正 比。 然而，假设条件和保证条件在现实中往往很难写出。这是因为它们需要包含 1 0 第2 章基本设定与主要技术 在整个程序执行过程中关于全局的程序状态的不变式。更具体一点，假设保证推 理方法的模块性和实用性制约于以下因素： 1 整个程序状态在使用该方法验证时，都被看成共享数据，并且所有的假 设条件和保证条件都需要描述其性质。如果其中一部分数据是某个线程 私有的，这种方法要求其他线程描述该线程的私有信息。这对验证的模 块化不利。 2 该方法假设共享数据都是静态可知，这给验证在动态分配的共享数据的 操作带来很大问题。因为何时分配一般来说都不是静态可知的。 3 有些数据可能只被并发执行的所有线程中的一部分线程共享，没有办法 将这些数据的信息对其他线程隐藏起来。 本文中的线程库接口规范基于假设保证推理方法。并发分离逻辑方法更简单， 但是限制更多，下面对其进行简要介绍。 2 3 2 并发分离逻辑 并发分离逻辑是另一种验证程序间共享数据的方法，它的基本思路是所有线程 均不能操作共享数据，除非它将共享数据变成私有数据。一般而言，可以将线程 为某个共享数据单元的加锁操作形式化为把该共享数据单元拿来变为私有数据单 元的过程，而将解锁操作形式化为将私有数据单元还回去变为共享数据单元的过 程。 并发分离逻辑是分离逻辑【2 4 】的扩展。这里首先简要介绍分离逻辑。分离逻辑在 传统的h o a r e 逻辑的基础上，为程序前后条件的逻辑语言增加了分离合取的连接 词。分离合取和合取一样，都要求其两边的逻辑表达式成立。不同的是，合取连 接词两边的逻辑表达式都是对全局数据的描述，而连接之后的表达式仍然是对全 局数据的描述。而分离合取连接词两边的逻辑表达式是对两块不相交的局部数据 的描述，连接之后的表达式是对这两块局部数据的总和的描述。分离逻辑大大简 化了对内存中存放的各种数据结构的底层表示的规范和证明。 本文第五章使用了较多的分离逻辑概念，在这里定义分离逻辑的些基本表达 式： 显i f - a 全a 銎 a i , a 2 会九登j 匿l ，至互2 匿l 列殁2 = 醒鹜li f a la h 2i i - a 2 t o p 兰九嚣t r u e ，11 、 1 一w 全丸嚣1 n u l l 嚣： 1 m w _ ， 1 卜垒久醒刍v ( 嚣i - l 卜w ) 1 一w l ，嘞兰1 一w l 宰l + lhw 2 枣唪l + ( 玎一1 ) h 其中，h j j a 表示内存h 满足分离逻辑断言a 。a l * a 2 描述内存块，该内存块 第2 章基本设定与主要技术 可以分为两个不相交的部分，这两部分分别满足a i 和a 2 。t o p 描述任意内存块。 l - w 描述一个内存单元，其地址为l ，存放的值为w 。1 1 - 描述任意一个地址为i 的单元。l - w i ，w n 描述一块连续地址空间，其大小为n ，起始地址为l ，里面存 放的值按地址增加的顺序分别为w l w n 。 并发分离逻辑将分离逻辑里对局部数据单独推理的思想应用在并发程序的验 证里。并发分离逻辑用分离合取来分隔每个线程的私有数据，以保证它们没有交 集。在这里，“私有 的概念仅仅是逻辑上的，而不是软件或硬件实现的保护。任 何线程只能访问它自己的私有数据，该线程若对某个共享单元加锁，那么在逻辑 上认为它的私有数据中增加了该单元，而