| 摘要 | 第1-9页 |
| ABSTRACT | 第9-10页 |
| 第一章 绪论 | 第10-16页 |
| ·课题研究背景 | 第10-11页 |
| ·问题描述 | 第11-12页 |
| ·课题研究思路与内容 | 第12-13页 |
| ·课题创新点 | 第13-14页 |
| ·论文结构 | 第14-16页 |
| 第二章 数据竞争及原子性问题的相关技术 | 第16-30页 |
| ·原子性问题的研究现状 | 第16-19页 |
| ·基于Reduction 的原子性检查技术 | 第16-18页 |
| ·commit-atomicity 原子性检查方法 | 第18页 |
| ·一种静态分析检测原子性技术 | 第18-19页 |
| ·数据竞争的相关技术 | 第19-27页 |
| ·LOCKSMITH 基于类型流的分析 | 第21-23页 |
| ·CoBE 的Bootstrapping 方法 | 第23-24页 |
| ·RELAY 相关锁集合算法 | 第24-27页 |
| ·数据竞争与原子性的区别及联系 | 第27-28页 |
| ·本章小结 | 第28-30页 |
| 第三章 基于抽象解释的数据竞争和原子性分析方法 | 第30-46页 |
| ·抽象解释理论简介 | 第30-34页 |
| ·抽象解释理论的基本思想和主要应用 | 第30-31页 |
| ·抽象解释相关预备知识 | 第31页 |
| ·顺序程序的抽象解释简介 | 第31-34页 |
| ·多级中断程序的语法和语义 | 第34-40页 |
| ·多级中断程序的抽象解释语法 | 第34-36页 |
| ·多级中断程序的语义 | 第36-38页 |
| ·多级中断程序的静态语义 | 第38-39页 |
| ·数据竞争及原子性的形式化描述 | 第39-40页 |
| ·多级中断程序的抽象解释 | 第40-43页 |
| ·只考虑中断优先级的抽象解释 | 第41-42页 |
| ·采取优化措施的抽象解释 | 第42-43页 |
| ·本章小结 | 第43-46页 |
| 第四章 数据竞争及原子性分析工具的实现及实验结果 | 第46-66页 |
| ·数据竞争及原子性分析工具的实现 | 第46-60页 |
| ·程序控制流图的构建 | 第46-50页 |
| ·函数指针参数的别名分析 | 第50-54页 |
| ·控制流图上组合状态的遍历算法 | 第54-57页 |
| ·函数摘要的构建与使用 | 第57-60页 |
| ·实验结果 | 第60-63页 |
| ·MIDAC 的实际应用 | 第60-61页 |
| ·使用函数摘要与未使用函数摘要时空开销对比 | 第61-63页 |
| ·与数据竞争检查工具goblint 的时间及结果对比 | 第63页 |
| ·本章小结 | 第63-66页 |
| 第五章 结束语 | 第66-68页 |
| ·本文工作总结 | 第66页 |
| ·下一步工作 | 第66-68页 |
| 致谢 | 第68-69页 |
| 参考文献 | 第69-73页 |
| 作者在学期间取得的学术成果 | 第73页 |