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

发布时间：2017-03-25 01:00

  本文关键词：基于操作语义的弱内存模型描述及程序逻辑研究，由笔耕文化传播整理发布。

【摘要】：程序语言的内存模型规定了在程序执行的过程中内存访问是如何发生的。它作为桥梁将为程序员和语言实现连接起来,帮助程序员写出正确的并发程序。在现实世界中,大多数的硬件和编译系统都是基于弱内存模型的假设,即内存访问并不是严格按照程序顺序执行,以用来支持各类优化。本文研究了弱内存模型的设计,并提出了可以支持在弱内存模型上进行程序验证的程序逻辑。具体来说,本文在弱内存模型和程序逻辑方面做出了如下的贡献： 首先,本文提出一种新的弱内存模型OHMM,这是Happens-before内存模型(HMM)的变种。这个模型通过对一个简单语言赋予具体的操作语义,并通过它在抽象机上的程序行为来模拟HMM。由于OHMM所允许的程序行为是通过操作语义自然生成的,所以它自然而然的避免了所谓的凭空出现(out-of-thin-air)的程序行为。另外一方面,OHMM使用一种我们称之为重放的机制来允许某些符合一定条件的指令在抽象机上能够多次执行,来模拟现实世界中编译器和处理器优化中的投机执行和优化。总的来说,我们的模型对于无锁程序的约束会比Java内存模型(JMM)更加弱一些,因此我们将会允许更多的编译器优化算法在我们的模型上能够使用。同时,在OHMM上,程序行为在直观上会比JMM更加自然。许多在JMM上可能出现但是明显违反直观认识的程序,在我们的模型上就不再合法。我们希望OHMM可以成为可供类Java语言选择的一种新内存模型。 其次,本文提出一种新的用于验证并发程序在TSO(Total Store Order)弱内存模型下正确性的程序逻辑。TSO模型所允许的弱行为是OHMM的子集。我们知道,TSO模型已经被用作X86和SPARC-TSO处理器族的模型基础,并且在一些高级语言中也正在被提案作为其内存模型的基础。我们的逻辑对LRG(Local Rely-Guarantee)进行扩展,对其加入了关于TSO写缓存的断言,这可以让我们对TSO模型中对外部线程不可见的局部的写缓存的状态进行描述。如同LRG一样,我们的程序逻辑支持对细粒度并发具有表达力强的rely/guarantee推理以及分离逻辑中的局部推理。同时,我们在逻辑上对TSO模型进行进一步抽象,把TSO共享内存分为local和shared两部分,这可以允许我们可以将那些在访问时只有单个线程能够访问的内存单元(逻辑上等同于local单元)的写操作直接写入内存,不需要经过写缓存。我们使用这个逻辑证明了一些具有代表性的并发算法在TSO上的正确性,包括Peterson's lock算法,Simpson's four slot算法,concurrent GCD算法以及lock的优化实现算法。
【关键词】：弱内存模型 程序验证 并发 程序逻辑
【学位授予单位】：中国科学技术大学
【学位级别】：博士
【学位授予年份】：2015
【分类号】：TP311.1
【目录】：

• 摘要5-6
• ABSTRACT6-10
• 插图索引10-12
• 主要符号对照表12-13
• 第一章 绪论13-23
• 1.1 弱内存模型的设计15-17
• 1.2 运用于弱内存模型的程序逻辑设计17-23
• 第二章 背景知识介绍23-31
• 2.1 顺序一致性模型23-24
• 2.2 弱内存模型24-28
• 2.2.1 TSO弱内存模型24-25
• 2.2.2 Happens-Before弱内存模型25-28
• 2.3 程序逻辑28-31
• 第三章 基于操作语义的Happens-Before弱内存模型31-67
• 3.1 OHMM非形式化的描述32-42
• 3.1.1 OHMM语言32-33
• 3.1.2 OHMM抽象机33-35
• 3.1.3 事件执行顺序35-37
• 3.1.4 历史记录和内存访问37-39
• 3.1.5 重放事件39-42
• 3.2 OHMM形式化定义42-45
• 3.3 一些简单的例子45-50
• 3.3.1 JMM中不允许但OHMM中允许46-48
• 3.3.2 OHMM中禁止JMM中违反直观的例子出现48-50
• 3.4 DRF-Guarantee性质证明50-57
• 3.4.1 无数据竞争51-54
• 3.4.2 带标签的弱操作语义54
• 3.4.3 模拟关系(Simulation)54-57
• 3.5 程序变换算法的正确性57-62
• 3.5.1 程序变换58-61
• 3.5.2 变换的正确性61-62
• 3.6 相关工作62-64
• 3.7 总结和弱点探讨64-67
• 第四章 从OHMM到TSO弱内存模型67-71
• 4.1 OHMM-TSO模型67-71
• 第五章 用于TSO模型局部推理的程序逻辑71-99
• 5.1 语言71-78
• 5.1.1 TSO标准模型72
• 5.1.2 ATSO内存模型72-78
• 5.2 断言定义78-83
• 5.3 逻辑系统83-86
• 5.4 一些例子86-91
• 5.4.1 Optimzed Implementation of Locks算法86-87
• 5.4.2 Peterson's Lock算法87-88
• 5.4.3 Simpson's Four Slot算法88-91
• 5.4.4 Concurrent GCD算法91
• 5.5 逻辑可靠性证明91-97
• 5.5.1 TSO是ATSO的精化93-94
• 5.5.2 逻辑系统在ATSO上的可靠性94-97
• 5.6 相关工作和总结97-99
• 第六章 结论99-101
• 参考文献101-105
• 附录A Simulation引理证明105-113
• 附录B 程序变换的正确性证明113-123
• B.1 E-WAR的正确性113-115
• B.2 E-WBW和E-IR正确性115
• B.3 E-RAR和E-RAW正确性115-117
• B.4 调序变换的正确性117-120
• B.5 I-IR的正确性120-123
• 附录C TSO和ATSO精化关系证明123-125
• 附录D 逻辑在ATSO上可靠性主引理的证明125-129
• 致谢129-131
• 在读期间发表的学术论文与取得的研究成果131

【共引文献】

中国期刊全文数据库 前10条

1 余伟;;基于消元法生成非线性循环不变式[J];电子技术与软件工程;2014年16期

2 万良;石文昌;冯慧;;基于分离逻辑的并行程序性质验证方法[J];计算机科学;2013年10期

3 罗军;王宏;李文生;;基于向量时钟模型的NoSQL最终一致性的研究[J];计算机工程与应用;2013年23期

4 张晶;潘有顺;;嵌入式系统同步进程的竞态条件分析与推理学习方法[J];计算机科学;2014年02期

5 万良;;基于隔离逻辑的并行程序可靠性验证方法[J];计算机工程;2014年02期

6 SHEN YuPing;ZHAO XiShun;;Proof systems for planning under 0-approximation semantics[J];Science China(Information Sciences);2014年07期

7 刘恒;李美安;苏萌;;基于重复数的最短循环请求集生成算法[J];计算机应用;2014年05期

8 张展;左德承;黄友富;何辉;;一种基于准同步检查点的虚拟机卷回恢复算法[J];计算机科学;2014年05期

9 余伟;;循环不变式在程序设计教学中的应用[J];科技风;2014年14期

10 林菲;孙勇;丁宏;任一支;;自稳定的分布式事务内存模型及算法[J];计算机研究与发展;2014年09期

中国博士学位论文全文数据库 前9条

1 朱素霞;面向多核处理器确定性重演的内存竞争记录机制研究[D];哈尔滨工业大学;2013年

2 刘洋;网络式软件需求验证的形式化方法研究[D];电子科技大学;2013年

3 毛华坚;云环境中的移动文件存储和时空数据分析关键技术研究[D];国防科学技术大学;2013年

4 刘光辉;高效处理器容错技术研究与实现[D];国防科学技术大学;2013年

5 吴晓峰;面向无线网络的形式化方法研究[D];华东师范大学;2014年

6 杨哲a\;Java语言的程序漏洞检测与诊断技术[D];复旦大学;2012年

7 王涛;任务关键系统的软件行为建模与检测技术研究[D];燕山大学;2014年

8 周宁;代数化符号模拟验证的应用研究[D];北京交通大学;2015年

9 陈艳文;分布式系统的时间化通信行为模型[D];华东师范大学;2014年

中国硕士学位论文全文数据库 前10条

1 刘恒;并发数据结构及其在动态内存管理中的应用[D];重庆大学;2013年

2 张越;铁路信号联锁系统安全规范的形式化描述与验证方法[D];北京交通大学;2013年

3 顾飞;基于SPARC架构面向确定性重演的多核访存竞争记录方法的研究[D];哈尔滨工业大学;2013年

4 王勇;动态可重构的DSM语义研究[D];哈尔滨工业大学;2012年

5 齐蓓;基于软件体系结构的软件可靠性验证测评方法研究[D];东华大学;2013年

6 刘彦武;综合信息系统的开发与建设[D];天津大学;2012年

7 刘曼霞;基于XYZ/SE的C/S体系结构风格研究[D];湖南大学;2013年

8 王文苑;分布式缓存可用性相关问题研究[D];华中科技大学;2013年

9 孙建良;分布式存储系统可用性与一致性研究[D];华中科技大学;2013年

10 曹粟;基于非即停调试模式的嵌入式应用级调试系统[D];华中科技大学;2013年

  本文关键词：基于操作语义的弱内存模型描述及程序逻辑研究，，由笔耕文化传播整理发布。

本文编号：266401