| 摘要 | 第5-6页 |
| ABSTRACT | 第6页 |
| 第1章 绪论 | 第15-23页 |
| 1.1 关键问题和研究现状概述 | 第16-18页 |
| 1.2 本文的贡献 | 第18-20页 |
| 1.3 本文的组织结构 | 第20-23页 |
| 第2章 编译器验证概述 | 第23-33页 |
| 2.1 串行程序编译器验证:CompCert | 第23页 |
| 2.2 串行程序分离编译器验证:Compositional CompCert | 第23-26页 |
| 2.3 主要挑战和我们的解决方案 | 第26-28页 |
| 2.4 编译器验证框架概述 | 第28-29页 |
| 2.5 验证框架的扩展 | 第29-31页 |
| 2.6 本章小结 | 第31-33页 |
| 第3章 基本设定 | 第33-53页 |
| 3.1 抽象程序语言 | 第33-41页 |
| 3.1.1 模块局部语义 | 第34-36页 |
| 3.1.2 良定义的程序语言 | 第36-38页 |
| 3.1.3 完整程序的抢占式并发语义 | 第38-41页 |
| 3.2 事件路径的精化关系和等价关系 | 第41-43页 |
| 3.3 无数据竞争性 | 第43-44页 |
| 3.4 关于良定义的语言的进一步讨论 | 第44-50页 |
| 3.5 本章小结 | 第50-53页 |
| 第4章 编译器验证框架 | 第53-75页 |
| 4.1 非抢占式语义 | 第53-56页 |
| 4.1.1 完整程序的非抢占式并发语义 | 第53-55页 |
| 4.1.2 抢占式与非抢占式语义的等价性 | 第55-56页 |
| 4.2 NPDRF的定义 | 第56-57页 |
| 4.3 保持内存印迹的模拟关系 | 第57-65页 |
| 4.3.1 内存印迹一致性 | 第58-59页 |
| 4.3.2 依赖/保证条件 | 第59-60页 |
| 4.3.3 模拟关系 | 第60-64页 |
| 4.3.4 模拟关系的传递性 | 第64-65页 |
| 4.4 模拟关系的可组合性 | 第65-69页 |
| 4.4.1 完整程序的向下模拟关系 | 第65-67页 |
| 4.4.2 模块的Reach-Close性质 | 第67-68页 |
| 4.4.3 可组合性引理 | 第68-69页 |
| 4.5 模拟关系的可靠性和NPDRF的保持 | 第69-73页 |
| 4.5.1 完整程序的向上模拟关系 | 第69-72页 |
| 4.5.2 可靠性引理 | 第72页 |
| 4.5.3 NPDRF保持引理 | 第72-73页 |
| 4.6 验证框架的最终定理 | 第73-74页 |
| 4.7 本章小结 | 第74-75页 |
| 第5章 验证框架的应用-CASCompCert编译器 | 第75-89页 |
| 5.1 程序语言的实例化 | 第75-79页 |
| 5.1.1 Clight语言的实例化 | 第75-77页 |
| 5.1.2 x86-SC的实例化 | 第77-79页 |
| 5.2 CompCert的验证 | 第79-85页 |
| 5.2.1 内存模型的变换 | 第83-84页 |
| 5.2.2 内存印迹的保持性证明 | 第84-85页 |
| 5.3 Coq中的验证工作量 | 第85-89页 |
| 第6章 针对x86-TSO机器模型的验证框架扩展 | 第89-105页 |
| 6.1 验证框架扩展的最终目标 | 第89-92页 |
| 6.2 x86-TSO机器模型 | 第92-98页 |
| 6.3 对象模块源语言CImp | 第98-99页 |
| 6.3.1 对象内存与用户内存的隔离 | 第98-99页 |
| 6.4 对象正确性的定义 | 第99-101页 |
| 6.5 加强的DRF-guarantee | 第101-102页 |
| 6.6 自旋锁实现的验证 | 第102-105页 |
| 第7章 相关工作 | 第105-109页 |
| 7.1 编译器验证 | 第105-107页 |
| 7.2 编译确认 | 第107页 |
| 7.3 非抢占式语义和无数据竞争性 | 第107-109页 |
| 第8章 总结和未来工作 | 第109-111页 |
| 参考文献 | 第111-115页 |
| 附录A 定理6.1和相关引理的证明 | 第115-123页 |
| A.1 SC和TSO完整程序间的模拟关系 | 第116-117页 |
| A.2 用户模块的局部模拟关系 | 第117-119页 |
| A.3 x86-TSO程序不产生冲突的用户内存印迹 | 第119-122页 |
| A.4 x86用户模块满足模拟关系 | 第122-123页 |
| 附录B 支持栈地址逃逸的验证框架 | 第123-175页 |
| B.1 修改后的定义和重要引理 | 第123-131页 |
| B.1.1 状态模型 | 第123页 |
| B.1.2 模块局部的模拟关系 | 第123-127页 |
| B.1.3 可组合性和非抢占语义下完整程序的向下模拟关系 | 第127-129页 |
| B.1.4 完整程序模拟关系的反转 | 第129-130页 |
| B.1.5 NPDRF的保持性 | 第130-131页 |
| B.2 模拟关系传递性(引理B.1)的证明 | 第131-145页 |
| B.3 模拟关系可组合性(引理B.2)的证明 | 第145-160页 |
| B.4 模拟关系反转(引理B.3)的证明 | 第160-167页 |
| B.5 NPDRF保持性(引理B.4)的证明 | 第167-175页 |
| 附录C 支UnusedGlob的验证框架 | 第175-179页 |
| 致谢 | 第179-181页 |
| 在读期间发表的学术论文与取得的研究成果 | 第181页 |
