| 摘要 | 第1-6页 |
| ABSTRACT | 第6-10页 |
| 插图索引 | 第10-12页 |
| 主要符号对照表 | 第12-13页 |
| 第一章 绪论 | 第13-23页 |
| ·弱内存模型的设计 | 第15-17页 |
| ·运用于弱内存模型的程序逻辑设计 | 第17-23页 |
| 第二章 背景知识介绍 | 第23-31页 |
| ·顺序一致性模型 | 第23-24页 |
| ·弱内存模型 | 第24-28页 |
| ·TSO弱内存模型 | 第24-25页 |
| ·Happens-Before弱内存模型 | 第25-28页 |
| ·程序逻辑 | 第28-31页 |
| 第三章 基于操作语义的Happens-Before弱内存模型 | 第31-67页 |
| ·OHMM非形式化的描述 | 第32-42页 |
| ·OHMM语言 | 第32-33页 |
| ·OHMM抽象机 | 第33-35页 |
| ·事件执行顺序 | 第35-37页 |
| ·历史记录和内存访问 | 第37-39页 |
| ·重放事件 | 第39-42页 |
| ·OHMM形式化定义 | 第42-45页 |
| ·一些简单的例子 | 第45-50页 |
| ·JMM中不允许但OHMM中允许 | 第46-48页 |
| ·OHMM中禁止JMM中违反直观的例子出现 | 第48-50页 |
| ·DRF-Guarantee性质证明 | 第50-57页 |
| ·无数据竞争 | 第51-54页 |
| ·带标签的弱操作语义 | 第54页 |
| ·模拟关系(Simulation) | 第54-57页 |
| ·程序变换算法的正确性 | 第57-62页 |
| ·程序变换 | 第58-61页 |
| ·变换的正确性 | 第61-62页 |
| ·相关工作 | 第62-64页 |
| ·总结和弱点探讨 | 第64-67页 |
| 第四章 从OHMM到TSO弱内存模型 | 第67-71页 |
| ·OHMM-TSO模型 | 第67-71页 |
| 第五章 用于TSO模型局部推理的程序逻辑 | 第71-99页 |
| ·语言 | 第71-78页 |
| ·TSO标准模型 | 第72页 |
| ·ATSO内存模型 | 第72-78页 |
| ·断言定义 | 第78-83页 |
| ·逻辑系统 | 第83-86页 |
| ·一些例子 | 第86-91页 |
| ·Optimzed Implementation of Locks算法 | 第86-87页 |
| ·Peterson's Lock算法 | 第87-88页 |
| ·Simpson's Four Slot算法 | 第88-91页 |
| ·Concurrent GCD算法 | 第91页 |
| ·逻辑可靠性证明 | 第91-97页 |
| ·TSO是ATSO的精化 | 第93-94页 |
| ·逻辑系统在ATSO上的可靠性 | 第94-97页 |
| ·相关工作和总结 | 第97-99页 |
| 第六章 结论 | 第99-101页 |
| 参考文献 | 第101-105页 |
| 附录A Simulation引理证明 | 第105-113页 |
| 附录B 程序变换的正确性证明 | 第113-123页 |
| B.1 E-WAR的正确性 | 第113-115页 |
| B.2 E-WBW和E-IR正确性 | 第115页 |
| B.3 E-RAR和E-RAW正确性 | 第115-117页 |
| B.4 调序变换的正确性 | 第117-120页 |
| B.5 I-IR的正确性 | 第120-123页 |
| 附录C TSO和ATSO精化关系证明 | 第123-125页 |
| 附录D 逻辑在ATSO上可靠性主引理的证明 | 第125-129页 |
| 致谢 | 第129-131页 |
| 在读期间发表的学术论文与取得的研究成果 | 第131页 |