并发程序分离编译的验证

发布时间：2021-09-22 15:41

　　许多实用计算机程序是并发程序,且常由多个程序模块组成。分离编译对这样的程序十分重要,它将每个程序模块独立地编译之后链接成完整的可执行程序。将编译得到的目标模块链接成完整的目标程序之后,正确的编译过程应能确保目标程序与源程序的行为一致。这要求编译过程不仅正确地编译每个模块本身,还要确保目标模块间的交互与源程序模块一致。本文针对并发程序的分离编译场景,研究了编译正确性的形式化描述和验证技术,并作出了如下贡献。首先,本文提出了一个验证并发程序分离编译器的验证框架,它通过复用经过验证的串行程序编译来构建无数据竞争的并发程序的分离编译及其正确性证明。在该框架中,本文提出了一种保持内存印迹（执行中访问的内存地址集合）的模拟关系,并将这种源模块与目标模块间的模拟关系作为编译正确性的形式化描述。在外部函数调用点和线程间同步点处,该模拟关系刻画了模块与环境的相互影响,令这种模拟关系具有模块链接和非抢占式并发层面上的可组合性;通过在模拟关系中引入内存印迹的保持关系,本文将完整程序间无数据竞争性质的保持性分解成模块间的局部性质,实现了无数据竞争性的保持性的模块化验证。此外,通过对程序语言模型进行抽象,该验证... 

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

【文章页数】：181 页

【学位级别】：博士

【部分图文】：

图２．３验证框架的扩展??

?第５章验证框架的应用——ＣＡＳＣｏｍｐＣｅｒｔ编译器???引理?５．２（ｘ８６－ＳＣ是良定义的）ｗｄ（ｘ８６－ＳＣ）。??Ｘ８６－ＳＣ被编译器用作目标语言。在证明框架中的模拟关系反转引理（引??理４．８）中，需要以目标语言是确定性的为前提。为了能够应用该引理，我们证??明了?Ｘ８６－ＳＣ是确定性的。??引理?５．３?（ｘ８６＿ＳＣ是确定性的）ｄｅｔ（ｘ８６－ＳＣ）。??５．２?ＣｏｍｐＣｅｒｔ?的验证??Ｉ?１??

尽管ＣｏｍｐＣｅｒｔ不包含内存印迹概念及相关的定义，在其编译器证明中许多??中间定义、引理和证明脚本可以通过少量修改来支持内存印迹的保持性。例如，??图５．５给出了?Ｓｅｌｅｃｔｉｏｎ编译趟的证明中的一个关键引理ｓｅｌ＿ｅｘｐｒ＿ｃｏｒｒｅｃｔ，其??高亮部分是我们对该引理做的修改。该引理的含义是经指令选择得到的新表达??式的求值结果是原表达式求值结果的精化。我们对该引理作的修改只是增加对??内存印迹的约束，即在扩展（Ｍｅｍ．ｅｘｔｅｎｄｓ）的内存上，指令选择得到的新表达??式比原表达式有更小（ｆＰ．ｓｕ／ｊｓｅｔ）的内存印迹。??在复用ＣｏｍｐＣｅｒｔ模拟关系不变式（ｍａｔｃｈ＿ｓｔａｔｅ关系）时，添加对内存印??迹保持性的支持相对直接．例如图５．６中给出的Ｓｅｌｅｃｔｉｏｎ编译趟证明中的模拟??关系不变式，我们只需要在原ＣｏｍｐＣｅｒｔ的ｍａｔｃｈ＿ｓｔａｔｅ关系中加入内存印迹相??关的约束（高亮部分）即可。??５．３?Ｃｏｑ中的验证工作量??本节我们介绍本文Ｃｏｑ实现的验证工作量。??


本文编号：3404001