学位论文 > 优秀研究生学位论文题录展示

使用事务内存同步机制的并行程序验证的研究

作　者: 李隆
导　师: 陈意云
学　校: 中国科学技术大学
专　业: 计算机软件与理论
关键词: 软件安全并行程序验证汇编语言受信任计算基础携带证明的代码事务内存同步机制
分类号: TP311.11
类　型: 博士论文
年　份: 2008年
下　载: 169次
引　用: 1次
阅　读: 论文下载

内容摘要

近年来,随着超线程、多核体系结构等多线程技术的发展和广泛应用,计算机硬件已经提供了越来越高效的软件运行平台。但是要更好地利用这些平台的并行优势,计算机软件就需要具备更好地并行性,以充分利用多个处理器的性能。并行程序已经成为了软件开发的主流。然而要确保顺序程序的正确性已经是非常困难的了,要保证并行程序的正确性难度更甚。这是因为在并行程序中,程序员还需要处理共享数据的并发存取问题,确保数据在不同线程中的有效性。传统上,程序员使用锁的方式来管理并行程序中共享数据的并发存取。但是锁方式不仅难于推理,而且还容易出现死锁等导致程序进入异常执行状态的隐患。为减轻程序员开发并行程序的负担,提高软件开发的效率,近年的研究提出了使用事务内存同步机制来管理共享数据的并发存取。提供了事务内存同步机制的系统通过自动地管理数据的并发访问,免除了程序员在这方面的负担,也避免了死锁等锁机制的致命隐患。但是近年来围绕着事务内存同步机制的研究主要集中于提供事务内存同步机制的系统的各种实现策略及其性能的提高上,而对该同步机制在程序推理、形式验证及易于推理方面的研究甚少。针对事务内存同步机制相关研究的现状,基于程序推理验证的研究成果,本文提出了一种推理方法以推理使用了事务内存同步机制的实现系统所提供的编程结构的程序。该推理方法基于众所周知的不变式证明(Invariance Proof)方法并对Hoare逻辑进行了扩展,通过指明共享数据上的不变式来约束多个线程间的并发访问,可靠、可行,并具备模块化验证的特点。同时,本文还专注于事务内存同步机制的语义研究,在携带证明的代码的研究的基础上,将所提出的推理方法形式化到遵循事务内存同步机制语义的Hoare风格的验证框架中,并证明了推理方法遵循事务内存同步机制的语义的可靠性。此外,本文还给出了推理验证的应用实例,展示了本文所提出的推理方法和验证框架的有效性。最后,本文通过详尽的比较,阐明了事务内存同步机制相对于传统的锁同步机制易推理的优点,展示了事务内存同步机制对程序推理的简化。本文的主要特色和贡献为:·本文提出了一种Hoare风格的推理方法,用于在事务内存同步机制的语义的高层抽象上推理源语言级的并行程序。·本文也提出了一个携带证明的代码(Proof-Carrying Code)风格的验证框架,用于在事务内存同步机制的语义的底层实现上验证汇编级的并行程序,并证明了验证框架遵循事务内存同步机制的语义的可靠性。该验证框架的提出,填补了携带证明的代码的研究在事务内存同步机制方面的空白。·本文在Coq定理证明辅助工具中完成了所提出的验证框架的可靠性证明,从而将验证框架中的验证推理系统从受信任计算基础中排除出去,使得本文的验证框架具有更高的可靠性。·本文还通过详细的比较阐述了事务内存同步机制相对于锁同步机制的易推理的优势。

全文目录

摘要  5-7
Abstract  7-12
第1章绪论  12-25
  1.1 研究背景  12-16
    1.1.1 程序与安全  12-13
    1.1.2 形式程序验证  13-14
    1.1.3 受信任计算基础  14
    1.1.4 并行程序的安全性  14-16
  1.2 携带证明的代码(PCC)  16-18
  1.3 事务内存同步机制  18-22
    1.3.1 事务内存系统的系统实现的相关研究  20-21
    1.3.2 事务内存系统的语义描述的相关研究  21-22
  1.4 存在的问题  22-23
  1.5 本文概述  23-25
    1.5.1 研究工作  23
    1.5.2 主要创新和贡献  23-24
    1.5.3 章节安排  24-25
第2章事务内存程序的推理方法  25-41
  2.1 事务内存同步机制  25-28
    2.1.1 语义及编程结构  25-26
    2.1.2 实现策略  26-27
    2.1.3 技术困难  27-28
  2.2 事务内存程序的推理方法的背景研究  28-30
    2.2.1 Hoare风格的推理  28-29
    2.2.2 不变式证明  29-30
  2.3 事务内存程序的推理方法  30-32
    2.3.1 推理方法  30-31
    2.3.2 推理方法可靠性  31-32
  2.4 推理方法实例  32-40
    2.4.1 哲学家就餐问题  32-37
    2.4.2 生产者-消费者问题  37-40
  2.5 本章小结  40-41
第3章事务内存程序的验证框架  41-84
  3.1 抽象机器  42-46
  3.2 程序规范  46-47
  3.3 分离逻辑  47-48
  3.4 推理规则  48-52
  3.5 验证框架可靠性  52-59
  3.6 验证框架的应用  59-71
    3.6.1 哲学家就餐问题  59-67
    3.6.2 生产者-消费者问题  67-71
  3.7 Coq实现  71-83
    3.7.1 抽象机器  72-74
    3.7.2 程序规范  74
    3.7.3 分离逻辑  74-75
    3.7.4 推理规则  75-78
    3.7.5 框架可靠性  78-79
    3.7.6 验证的例子  79-83
  3.8 本章小结  83-84
第4章事务内存同步机制的推理优势  84-90
  4.1 锁同步方式的推理方法  84-85
  4.2 锁与事务内存同步机制的推理比较  85-89
    4.2.1 非抢占式线程模型的A-G推理  86-88
    4.2.2 抢占式线程控制A-G推理  88-89
  4.3 本章小结  89-90
第5章结束语  90-92
  5.1 论文工作总结  90-91
  5.2 进一步的工作  91-92
参考文献  92-100
致谢  100-101
在读期间发表的学术论文与取得的研究成果  101

使用事务内存同步机制的并行程序验证的研究

内容摘要

全文目录

相似论文