| 摘要 | 第1-7页 |
| ABSTRACT | 第7-13页 |
| 插图 | 第13-15页 |
| 表格 | 第15-16页 |
| 第1章 绪论 | 第16-24页 |
| ·关键问题与研究现状概述 | 第18-20页 |
| ·一般并发程序精化的验证 | 第18-19页 |
| ·并发对象实现的正确性刻画与验证 | 第19-20页 |
| ·本文的贡献与组织结构 | 第20-24页 |
| 第2章 验证并发程序精化的模拟关系RGSim | 第24-44页 |
| ·关键挑战与我们的解决方案 | 第24-29页 |
| ·串行环境下建立的精化关系缺少可组合性 | 第24-25页 |
| ·假设任意开放环境的精化关系缺乏实用性 | 第25-26页 |
| ·如何允许程序使用不同的编程语言和机器模型? | 第26页 |
| ·如何定义程序的行为? | 第26-27页 |
| ·我们的解决方案 | 第27-29页 |
| ·基本设定 | 第29-32页 |
| ·通用的并发程序语言 | 第29-30页 |
| ·精化关系 | 第30-32页 |
| ·RGSim的定义 | 第32-35页 |
| ·RGSim的可组合性 | 第35-39页 |
| ·一个简单的例子 | 第39-42页 |
| ·本章小结 | 第42-44页 |
| 第3章 RGSim的简单应用 | 第44-52页 |
| ·并发环境下程序优化的验证 | 第44-48页 |
| ·专为程序优化设计的推理规则 | 第44-46页 |
| ·应用举例一：循环不变代码外提 | 第46-47页 |
| ·应用举例二：强度削弱和归纳变量删除 | 第47-48页 |
| ·相关工作 | 第48页 |
| ·抽象操作的细粒度实现的验证 | 第48-52页 |
| ·应用举例：计算最大公约数的并发程序 | 第49-51页 |
| ·并发对象的验证 | 第51-52页 |
| 第4章 并发垃圾收集算法的验证 | 第52-78页 |
| ·并发垃圾收集算法的正确性 | 第52-53页 |
| ·基于RGSim的通用验证框架 | 第53-55页 |
| ·应用举例：Boehm等人提出的并发垃圾收集算法 | 第55-76页 |
| ·GC算法概述 | 第55-59页 |
| ·程序变换 | 第59-64页 |
| ·用户指令上的精化证明 | 第64-67页 |
| ·GC代码的验证 | 第67-76页 |
| ·相关工作 | 第76-78页 |
| 第5章 验证并发对象线性一致性的程序逻辑 | 第78-116页 |
| ·关键挑战与我们的解决方案 | 第78-83页 |
| ·验证LP固定的并发对象的程序逻辑 | 第78-80页 |
| ·帮助机制与Pending线程池 | 第80-81页 |
| ·依赖未来的LP与Try-Commit指令 | 第81-82页 |
| ·作为元理论的模拟关系 | 第82-83页 |
| ·基本设定 | 第83-90页 |
| ·支持并发对象的程序语言 | 第83-87页 |
| ·并发对象的规范与线性一致性 | 第87-89页 |
| ·与线性一致性等价的上下文精化关系 | 第89-90页 |
| ·验证线性一致性的程序逻辑 | 第90-99页 |
| ·辅助代码和状态 | 第90-91页 |
| ·断言 | 第91-93页 |
| ·推理规则 | 第93-97页 |
| ·语义和部分正确性 | 第97-99页 |
| ·保证程序逻辑可靠性的模拟关系 | 第99-102页 |
| ·应用举例 | 第102-113页 |
| ·一对数据的快照 | 第102-104页 |
| ·MS无锁队列 | 第104-110页 |
| ·CCAS算法 | 第110-113页 |
| ·本章小结与相关工作 | 第113-116页 |
| 第6章 刻画并发对象进展性的上下文精化框架 | 第116-128页 |
| ·并发对象的进展性性质与我们的上下文精化框架概述 | 第116-120页 |
| ·线性一致性与上下文精化 | 第116-117页 |
| ·进展性性质 | 第117-119页 |
| ·我们的上下文精化框架 | 第119-120页 |
| ·形式化进展性性质 | 第120-123页 |
| ·基于上下文精化的统一框架 | 第123-127页 |
| ·可观测行为 | 第123-124页 |
| ·新的上下文精化关系和等价结果 | 第124-127页 |
| ·本章小结与相关工作 | 第127-128页 |
| 第7章 结论 | 第128-132页 |
| 参考文献 | 第132-138页 |
| 附录A 与Herlihy和Shavit的无阻碍性定义的比较 | 第138-140页 |
| 附录B 各种等价结果的证明 | 第140-148页 |
| B.1 最泛化客户端程序 | 第140-141页 |
| B.2 定理5.6的证明 | 第141-145页 |
| B.3 定理6.3的证明 | 第145-148页 |
| 索引 | 第148-154页 |
| 致谢 | 第154-156页 |
| 在读期间发表的学术论文与取得的研究成果 | 第156页 |