无数据竞争并发程序的语义等价性研究

发布时间：2021-03-08 10:35

　　多核处理器已经成为目前主流的处理器,相应的多线程并发编程也成为了目前主流的编程。多线程并发程序在充分利用多核处理器带来的高运行效率的同时,相比于串行程序也带来了更多线程交错的不确定性。线程的交错执行让程序员对并发程序的理解更加困难,使并发程序存在着比串行程序更多的错误和缺陷。因此,并发程序的正确性成为了研究热点,而对并发程序正确性的验证,也成为了当下程序验证领域的热门话题。并发程序正确性的验证工作非常困难,其中一个严重的阻碍在于:并发程序的线程交互具有不确定性,可能的交错执行顺序随着程序长度几乎呈指数级的增长。为了减少对并发程序推理的难度,本文考虑在非抢占语义下研究并发程序的行为。非抢占语义下,只有当线程主动让出执行权,其他线程才能开始执行。这样将线程交互限制在特定程序点,大大降低了需要考虑的执行过程的数量,简化了验证过程。本文对无数据竞争并发程序在非抢占语义和抢占语义下的等价性进行研究,通过对非抢占语义定义的讨论,提出了形式化定义的非抢占语义,并严格证明了对于无数据竞争的并发程序,它进行非抢占执行和抢占执行将得到一样的结果。具体地说,本文的主要贡献有以下几点:·我们提出了一种简单的并... 

【文章来源】：中国科学技术大学安徽省 211工程院校 985工程院校

【文章页数】：70 页

【学位级别】：硕士

【文章目录】：
摘要
ABSTRACT
第1章 绪论
    1.1 研究背景与研究意义
        1.1.1 软件正确性与形式化验证
        1.1.2 并发程序验证与非抢占语义
    1.2 相关研究概况
    1.3 本文贡献与结构
第2章 背景知识介绍
    2.1 数据竞争
    2.2 精化关系与程序验证
    2.3 非抢占语义
第3章 并发程序语法及语义
    3.1 程序语法
    3.2 带内存印迹的线程执行语义
    3.3 全局执行语义
    3.4 多步执行的定义
    3.5 事件路径和程序行为
    3.6 数据竞争的定义
第4章 非抢占语义
    4.1 对非抢占语义的讨论
    4.2 非抢占语义的具体定义
    4.3 多步执行与事件路径的定义
    4.4 非抢占语义下数据竞争的定义
    4.5 本章小结
第5章 非抢占语义和抢占语义的等价性
    5.1 无冲突的线程交换过程
    5.2 内存印迹冲突与数据竞争
    5.3 事件路径的一致性
    5.4 无数据竞争的等价性
    5.5 本章小结
第6章 语义等价性在编译验证中的应用
    6.1 编译器的正确性
    6.2 实际验证工作
    6.3 证明工作量
第7章 结论
参考文献
致谢
在读期间发表的学术论文与取得的研究成果



本文编号：3070907