基于操作语义的弱内存模型描述及程序逻辑研究

声明

摘要

插图索引

主要符号对照表

第一章 绪论

1．1 弱内存模型的设计

1．2 运用于弱内存模型的程序逻辑设计

第二章 背景知识介绍

2．1 顺序一致性模型

2．2 弱内存模型

2．2．1 TSO弱内存模型

2．2．2 Happens-Before弱内存模型

2．3 程序逻辑

第三章 基于操作语义的Happens-Before弱内存模型

3．1 OHMM非形式化的描述

3．1．1 OHMM语言

3．1．2 OHMM抽象机

3．1．3 事件执行顺序

3．1．4 历史记录和内存访问

3．1．5 重放事件

3．2 OHMM形式化定义

3．3 一些简单的例子

3．3．1 JMM中不允许但OHMM中允许

3．3．2 OHMM中禁止JMM中违反直观的例子出现

3．4 DRF-Guarantee性质证明

3．4．1 无数据竞争

3．4．2 带标签的弱操作语义

3．4．3 模拟关系(Simulation)

3．5 程序变换算法的正确性

3．5．1 程序变换

3．5．2 变换的正确性

3．6 相关工作

3．7 总结和弱点探讨

第四章 从OHMM到TSO弱内存模型

4．1 OHMM-TSO模型

第五章 用于TSO模型局部推理的程序逻辑

5．1 语言

5．1．1 TSO标准模型

5．1．2 ATSO内存模型

5．2 断言定义

5．3 逻辑系统

5．4 一些例子

5．4．1 Optimzed Implementation of Locks算法

5．4．2 Peterson’s Lock算法

5．4．3 Simpson’s Four Slot算法

5．4．4 Concurrent GCD算法

5．5 逻辑可靠性证明

5．5．1 TSO是ATSO的精化

5．5．2 逻辑系统在ATSO上的可靠性

5．6 相关工作和总结

第六章 结论

参考文献

附录

致谢

在读期间发表的学术论文与取得的研究成果