基于TL2软件事务内存机制的并发程序的精化验证
| 摘要 | 第1-6页 |
| Abstract | 第6-10页 |
| 第1章 绪论 | 第10-18页 |
| ·研究背景及意义 | 第10-15页 |
| ·软件事务内存及TL2算法 | 第10-13页 |
| ·STM的正确性标准及精化关系 | 第13-14页 |
| ·并发程序验证技术 | 第14-15页 |
| ·本文概述 | 第15-18页 |
| 第2章 技术基础 | 第18-26页 |
| ·本章导读 | 第18页 |
| ·TL2算法细节 | 第18-21页 |
| ·TL2算法实例 | 第19-21页 |
| ·基于依赖保证的模拟技术 | 第21-24页 |
| ·验证示例 | 第23-24页 |
| ·基于依赖保证的向前向后模拟技术 | 第24-25页 |
| ·本章小结 | 第25-26页 |
| 第3章 语言模型和精化关系的验证 | 第26-40页 |
| ·本章导读 | 第26页 |
| ·验证工作的难点 | 第26-27页 |
| ·线性化点难以确定 | 第26-27页 |
| ·不变式难以指定 | 第27页 |
| ·相关规范 | 第27-32页 |
| ·高层语言 | 第27-29页 |
| ·底层语言 | 第29-31页 |
| ·精化关系的定义 | 第31-32页 |
| ·中间层语言 | 第32-33页 |
| ·证明的分解 | 第33-34页 |
| ·高层和中间层精华关系的验证 | 第34-35页 |
| ·中间层和底层精化关系的验证 | 第35-38页 |
| ·本章小结 | 第38-40页 |
| 第4章 具体事务底层实现的验证 | 第40-54页 |
| ·本章导读 | 第40页 |
| ·读写事务底层实现的验证 | 第40-46页 |
| ·用中间层语言转换事务 | 第42页 |
| ·高层和中间层的验证 | 第42-43页 |
| ·中间层和底层的验证 | 第43-46页 |
| ·只读事务的验证 | 第46-52页 |
| ·用中间层语言转换事务 | 第48-49页 |
| ·高层和中间层的验证 | 第49-50页 |
| ·中间层和底层的验证 | 第50-52页 |
| ·本章小结 | 第52-54页 |
| 第5章 总结及进一步工作 | 第54-56页 |
| ·本文总结 | 第54页 |
| ·进一步研究工作 | 第54-56页 |
| 参考文献 | 第56-58页 |
| 致谢 | 第58页 |
