使用事务内存同步机制的并行程序验证的研究
| 摘要 | 第1-7页 |
| Abstract | 第7-12页 |
| 第1章 绪论 | 第12-25页 |
| ·研究背景 | 第12-16页 |
| ·程序与安全 | 第12-13页 |
| ·形式程序验证 | 第13-14页 |
| ·受信任计算基础 | 第14页 |
| ·并行程序的安全性 | 第14-16页 |
| ·携带证明的代码(PCC) | 第16-18页 |
| ·事务内存同步机制 | 第18-22页 |
| ·事务内存系统的系统实现的相关研究 | 第20-21页 |
| ·事务内存系统的语义描述的相关研究 | 第21-22页 |
| ·存在的问题 | 第22-23页 |
| ·本文概述 | 第23-25页 |
| ·研究工作 | 第23页 |
| ·主要创新和贡献 | 第23-24页 |
| ·章节安排 | 第24-25页 |
| 第2章 事务内存程序的推理方法 | 第25-41页 |
| ·事务内存同步机制 | 第25-28页 |
| ·语义及编程结构 | 第25-26页 |
| ·实现策略 | 第26-27页 |
| ·技术困难 | 第27-28页 |
| ·事务内存程序的推理方法的背景研究 | 第28-30页 |
| ·Hoare风格的推理 | 第28-29页 |
| ·不变式证明 | 第29-30页 |
| ·事务内存程序的推理方法 | 第30-32页 |
| ·推理方法 | 第30-31页 |
| ·推理方法可靠性 | 第31-32页 |
| ·推理方法实例 | 第32-40页 |
| ·哲学家就餐问题 | 第32-37页 |
| ·生产者-消费者问题 | 第37-40页 |
| ·本章小结 | 第40-41页 |
| 第3章 事务内存程序的验证框架 | 第41-84页 |
| ·抽象机器 | 第42-46页 |
| ·程序规范 | 第46-47页 |
| ·分离逻辑 | 第47-48页 |
| ·推理规则 | 第48-52页 |
| ·验证框架可靠性 | 第52-59页 |
| ·验证框架的应用 | 第59-71页 |
| ·哲学家就餐问题 | 第59-67页 |
| ·生产者-消费者问题 | 第67-71页 |
| ·Coq实现 | 第71-83页 |
| ·抽象机器 | 第72-74页 |
| ·程序规范 | 第74页 |
| ·分离逻辑 | 第74-75页 |
| ·推理规则 | 第75-78页 |
| ·框架可靠性 | 第78-79页 |
| ·验证的例子 | 第79-83页 |
| ·本章小结 | 第83-84页 |
| 第4章 事务内存同步机制的推理优势 | 第84-90页 |
| ·锁同步方式的推理方法 | 第84-85页 |
| ·锁与事务内存同步机制的推理比较 | 第85-89页 |
| ·非抢占式线程模型的A-G推理 | 第86-88页 |
| ·抢占式线程控制A-G推理 | 第88-89页 |
| ·本章小结 | 第89-90页 |
| 第5章 结束语 | 第90-92页 |
| ·论文工作总结 | 第90-91页 |
| ·进一步的工作 | 第91-92页 |
| 参考文献 | 第92-100页 |
| 致谢 | 第100-101页 |
| 在读期间发表的学术论文与取得的研究成果 | 第101页 |
