导读:本文包含了编译验证论文开题报告文献综述及选题提纲参考文献，主要关键词:并发,编译器验证,无数据竞争,模拟关系
编译验证论文文献综述
蒋瀚如[1]（2019）在《并发程序分离编译的验证》一文中研究指出许多实用计算机程序是并发程序,且常由多个程序模块组成。分离编译对这样的程序十分重要,它将每个程序模块独立地编译之后链接成完整的可执行程序。将编译得到的目标模块链接成完整的目标程序之后,正确的编译过程应能确保目标程序与源程序的行为一致。这要求编译过程不仅正确地编译每个模块本身,还要确保目标模块间的交互与源程序模块一致。本文针对并发程序的分离编译场景,研究了编译正确性的形式化描述和验证技术,并作出了如下贡献。首先,本文提出了一个验证并发程序分离编译器的验证框架,它通过复用经过验证的串行程序编译来构建无数据竞争的并发程序的分离编译及其正确性证明。在该框架中,本文提出了一种保持内存印迹(执行中访问的内存地址集合)的模拟关系,并将这种源模块与目标模块间的模拟关系作为编译正确性的形式化描述。在外部函数调用点和线程间同步点处,该模拟关系刻画了模块与环境的相互影响,令这种模拟关系具有模块链接和非抢占式并发层面上的可组合性;通过在模拟关系中引入内存印迹的保持关系,本文将完整程序间无数据竞争性质的保持性分解成模块间的局部性质,实现了无数据竞争性的保持性的模块化验证。此外,通过对程序语言模型进行抽象,该验证框架不与特定的并发原语或内存操作绑定。于是当把抽象语言实例化为多种真实程序语言时,验证框架中的引理可以被复用。其次,本文扩展了上述验证框架,使之支持以x86-TSO机器作为编译器的目标机器,并支持目标程序与类似Linux中自旋锁的、x86-TSO模型下带数据竞争的高效并发对象实现链接。在验证框架的扩展中,本文提出了x86-TSO模型下对象实现的正确性描述,并证明了x86-TSO模型下一种更强的DRF-guarantee,确保了该正确性描述的可靠性。最后,本文应用该验证框架开发了经过验证的CASCompCert编译器,它将实用C语言编译器CompCert的正确性证明扩展到了并发程序的分离编译场景。作为该验证框架扩展的应用,本文还验证了一种x86-TSO模型下的高效自旋锁实现满足本文提出的对象正确性描述,使得用CASCompCert编译的无数据竞争程序可以与该自旋锁链接,实现高效的线程间同步。以上验证结果均已在定理证明工具Coq中实现。(本文来源于《中国科学技术大学》期刊2019-05-01）
张晓曈[2]（2017）在《一种面向多线程的编译验证模型》一文中研究指出如何保证软件的执行与预期一致,在软件规模不断扩张的今天愈发成为摆在软件开发者与研究人员面前的一个难题。由于编译器在计算机软件系统中的特殊位置,使得保证编译器的可信性成为了保障软件正确执行的关键环节。保证编译器的可信性一般采取形式化验证方法,在形式化定义源语言、目标语言和编译过程的基础上,证明源语言程序与目标语言语义等同。本文针对Java语言的特点,提出了一种支持多线程的编译验证模型,具体研究内容如下:一、定义了一种适于证明的语言Jmin,并形式化定义其语义。Jmin语言是Java语言的一个子集,支持Java的核心语法:它是面向对象的,可以抛出和处理异常及执行部分线程操作。在目标语言一端,本文也提出了 Jmin虚拟机模型,并依据Java虚拟机指令给出了其指令集。二、形式化描述了编译过程,并使用定理证明工具Isabelle/HOL证明了编译过程的正确性。叁、在正确性证明的基础上,给出了 Jmin可信编译器的实现框架。(本文来源于《武汉大学》期刊2017-05-01）
江南,何炎祥,张晓瞳[3]（2016）在《_mJava到Micro-Dalvik虚拟机的编译验证》一文中研究指出针对类Java的面向对象语言mJava到类Dalvik的寄存器架构虚拟机Micro-Dalvik的编译验证,给出了mJava语言和Micro-Dalvik的操作语义.从mJava语言程序到Micro-Dalvik虚拟机指令的编译分为两步,首先将mJava语言程序中的本地变量名转换为相应的序号,得到一个中间语言程序,再将该中间语言程序翻译成Micro-Dalvik虚拟机指令程序.在给出中间语言的操作语义后,构造了mJava语言程序与编译后的中间语言程序的语义保持定理并证明,以及构造了中间语言程序的语义与编译后的Micro-Dalvik虚拟机程序的语义保持定理并证明.整个形式化编译验证在定理证明助手Isabelle/HOL中进行了机器检测.mJava语言和Micro-Dalvik虚拟机分别对Java语言和Dalvik虚拟机进行了抽象,是我们兼顾语言的真实性和形式化的清晰性的结果.但是,所有形式化的语义严格遵从语言规范中的定义,并与Dalvik VM的实现保持一致,从这种意义上讲,该编译器并不是一个实验性质的假想编译器,而是有其实用意义的.(本文来源于《电子学报》期刊2016年07期）
郭连伟[4]（2015）在《BWDSP译码器自动验证及编译向量化的研究与实现》一文中研究指出BWDSP是一款高性能数字信号处理器,同时兼容16位和32位定点数据格式,采用超长指令字架构,具有强大的并行处理能力,能较好的满足高速实时信号处理的应用要求。BWDSP具有多个执行簇,每个执行簇上有多个运算部件,同时提供了多种类型的向量化指令,为SIMD编译优化提供了大量的机会和支持。本文的主要工作包括两点。其一,设计并实现了BWDSP指令译码器的自动化验证平台；其二,在Open64编译基础设施的基础上研究并实现了基于高层WHIRL表示的支持BWDSP程序SIMD优化的编译算法。DSP译码器自动化验证平台是在BWDSP译码器的基础上,为了验证不断变动的指令集译码器的正确性,基于面向对象的理念设计的一套译码器验证工具。平台的设计首次使用了面向对象的思想。自动化译码器验证方案能够很好的支持重用和扩展,针对指令集的变动和扩展,能够在极短的时间内完成对应的测试版本。本文在OPEN64编译基础设施的基础之上,提出并实现了基于高层WHIRL表示的SIMD向量化算法。算法主要在OPEN64的中间语言高层WHIRL上进行,以最内层循环为主要优化对象,通过一系列的分析和变换工作,发现并利用程序循环潜在的指令并行,将该类操作进行SIMD优化处理。此外,BWDSP指令集还包括一些特殊的向量化指令,针对这些指令,算法也增加了对应的SIMD替换过程,通过对特殊向量化机会的识别,找到并替换成特殊SIMD操作,从而在WHIRL树层次上完成特殊指令SIMD变换。特殊SIMD操作替换算法已经实现了BWDSP指令集中的所有特殊向量化指令的替换优化算法。最终的实验结果表明,基于高层WHIRL表示的SIMD优化算法在BWDSP上针对可合成单字和双字的循环程序能够分别取得平均6.30倍和4.15倍的加速比。这表明,基于树匹配的SIMD优化算法对循环程序的效率提高是非常可观的。(本文来源于《中国科学技术大学》期刊2015-04-20）
徐超,何炎祥,吴伟,陈勇,刘健博[5]（2012）在《基于模拟关系的编译优化实现正确性验证方法》一文中研究指出编译器中通常采用各种优化方法来提高目标代码的质量,为了实现较好的效果,一些编译优化算法通常十分复杂,很容易给可靠性和安全性带来隐患.现有的编译器缺陷大部分是由优化阶段引起的.传统的编译优化正确性研究大部分只关注优化算法的正确性,但是只有该算法被正确的实现了才能确保实际运行的优化过程是正确的.本文提出一种基于模拟关系的方法来验证编译优化实现的正确性.在每次优化结束后,我们通过建立优化前代码和优化后代码之间的模拟关系生成优化正确应满足的逻辑条件,然后验证逻辑条件是否成立从而判定编译优化的实现是否正确性.以优化编译中的常量折迭优化和变量替换的验证作为示例显示了本方法的有效性和可靠性.(本文来源于《电子学报》期刊2012年11期）
陈旭超[6]（2012）在《基于增量编译的DSP内核IP的FPGA验证》一文中研究指出FPGA原型验证的出现极大地提高了芯片验证的效率。使得设计人员能够在短时间内测试大量的程序，及早的发现设计中的错误。但同时这种大规模芯片的验证使得软件编译时间越来越长，即使小的改动，也要连同没有修改的部分一起重新编译，浪费了时间，降低了验证效率。本文在对XXX DSP内核IP验证的过程中，引入了增量式设计，将设计按照不同功能、关键时序路径等进行了设计分区，每次修改设计后，再次编译时，软件会根据设计人员指定的分区网表类型，继承上一次编译的结果，只重新编译修改过的设计分区，极大地缩短了再次编译的时间，提高了FPGA验证的效率。本文具体工作如下：首先，通过研究增量编译的原理和设计方法，确定了通过Quartus II软件导出IP的方法以及使用IP的方法。其次，完成了ASIC设计到FPGA设计的代码转换工作，并通过功能验证的方法，保证了代码转换在行为级的正确性。接着，在成功导出DSP内核IP的基础上，采用增量式设计基于LMB总线搭建了IP验证环境，包括时钟模块、IP模块以及外部指令存储体模块。其中外部指令存储体模块又包含了从设备接口逻辑和存储体逻辑。从设备接口逻辑除了Split传输外，支持LMB总线的所有传输类型，如字节传输、半字传输、字传输、双字传输、读改写以及2、4、8节拍块传输。存储体逻辑实际上是一个ROM，宽度64bits，深度2048，是使用可综合的RTL编写的。最后，采用应用程序测试的方法，在XXX型高性能DSP IP FPGA性能评估系统硬件平台上，验证了XXX DSP内核IP的功能，并在验证过程中充分展现了增量编译的优势，提高了FPGA的验证效率。(本文来源于《西安电子科技大学》期刊2012-01-01）
陈晖,陈意云,茹祥民[7]（2005）在《一种用于Java程序验证编译的标签类型》一文中研究指出在基于语言考虑代码安全性的工作中,往往需要将高级语言程序翻译成类型化低级语言的程序进行类型检查.许多高级语言具有类型调度结构,在向低级语言的编译过程中需要用标签机制来实现.针对具有多继承接口的 Java 程序包含的一种特殊的类型调度结构,提出了一种新的标签类型.包含这种标签类型的低级语言能够有效地实现 Java 程序中的接口调用.这种对接口调用的编译方法被用在一个以类型化低级语言为验证语言的 Java 字节码即时编译器中.(本文来源于《软件学报》期刊2005年03期）
刘晓建,陈平[8]（2003）在《RETE网络中的优化编译模式及其PVS形式验证》一文中研究指出1.引言基于RETE算法的规则系统是实现指挥控制系统中的高性能战场态势监视与文电路由转发的核心计算模型。传统的规则系统,如OPS5,CLIPS等都是自封闭的规则系统,很难和常用的程序设计语言,如C/C~(++)互操作。iLog Rules虽然可以满足规则语言与C~(++)语言互操作的要求,但是由于不提供源码,不能满足“可信软件工程技术”项目所需要的“开放源码与文档以备安全审查”的基本要求。因此,我们在CLIPS的基础上,参考iLog Rules设计和开发了满足指控(本文来源于《计算机科学》期刊2003年06期）
编译验证论文开题报告
（1）论文研究背景及目的
此处内容要求：
首先简单简介论文所研究问题的基本概念和背景，再而简单明了地指出论文所要研究解决的具体问题，并提出你的论文准备的观点或解决方法。
写法范例：
如何保证软件的执行与预期一致,在软件规模不断扩张的今天愈发成为摆在软件开发者与研究人员面前的一个难题。由于编译器在计算机软件系统中的特殊位置,使得保证编译器的可信性成为了保障软件正确执行的关键环节。保证编译器的可信性一般采取形式化验证方法,在形式化定义源语言、目标语言和编译过程的基础上,证明源语言程序与目标语言语义等同。本文针对Java语言的特点,提出了一种支持多线程的编译验证模型,具体研究内容如下:一、定义了一种适于证明的语言Jmin,并形式化定义其语义。Jmin语言是Java语言的一个子集,支持Java的核心语法:它是面向对象的,可以抛出和处理异常及执行部分线程操作。在目标语言一端,本文也提出了 Jmin虚拟机模型,并依据Java虚拟机指令给出了其指令集。二、形式化描述了编译过程,并使用定理证明工具Isabelle/HOL证明了编译过程的正确性。叁、在正确性证明的基础上,给出了 Jmin可信编译器的实现框架。
（2）本文研究方法
调查法：该方法是有目的、有系统的搜集有关研究对象的具体信息。
观察法：用自己的感官和辅助工具直接观察研究对象从而得到有关信息。
实验法：通过主支变革、控制研究对象来发现与确认事物间的因果关系。
文献研究法：通过调查文献来获得资料，从而全面的、正确的了解掌握研究方法。
实证研究法：依据现有的科学理论和实践的需要提出设计。
定性分析法：对研究对象进行“质”的方面的研究，这个方法需要计算的数据较少。
定量分析法：通过具体的数字，使人们对研究对象的认识进一步精确化。
跨学科研究法：运用多学科的理论、方法和成果从整体上对某一课题进行研究。
功能分析法：这是社会科学用来分析社会现象的一种方法，从某一功能出发研究多个方面的影响。
模拟法：通过创设一个与原型相似的模型来间接研究原型某种特性的一种形容方法。
编译验证论文参考文献
[1].蒋瀚如.并发程序分离编译的验证[D].中国科学技术大学.2019
[2].张晓曈.一种面向多线程的编译验证模型[D].武汉大学.2017
[3].江南,何炎祥,张晓瞳._mJava到Micro-Dalvik虚拟机的编译验证[J].电子学报.2016
[4].郭连伟.BWDSP译码器自动验证及编译向量化的研究与实现[D].中国科学技术大学.2015
[5].徐超,何炎祥,吴伟,陈勇,刘健博.基于模拟关系的编译优化实现正确性验证方法[J].电子学报.2012
[6].陈旭超.基于增量编译的DSP内核IP的FPGA验证[D].西安电子科技大学.2012
[7].陈晖,陈意云,茹祥民.一种用于Java程序验证编译的标签类型[J].软件学报.2005
[8].刘晓建,陈平.RETE网络中的优化编译模式及其PVS形式验证[J].计算机科学.2003