汇编级顺序语句块的自动形式化规约及其验证

软件的形式化验证是保障软件可证明性、可靠性和安全性的重要手段,但传统形式化验证脚本的生成过程复杂且需要形式化验证专家的大量手工验证。为提高证明效率,构建一种自动证明模型,并在此基础上提出语义自动规约算法以及对所规约的语义自动生成证明脚本的算法。利用C++和Python并通过交互式定理证明器Isabelle 2017在基准数据中随机选择10个程序进行测试,结果表明,与完全人工操作相比,该算法具有较高的验证效率,可实现顺序语句块的自动化规约与验证。     

面向部分向量化的循环分布及聚合优化

大量循环中都存在着少数无法向量化的语句以及许多可向量化语句,循环分布通常可以将这些语句分离到不同的循环中,进而实现循环的部分向量化。目前主流的优化编译器仅支持简单激进的循环分布方法,因而导致向量化后的循环开销过大,且不利于寄存器和cache的重用。针对上述问题,提出了面向部分向量化的循环分布及聚合方法。首先,分析了一般循环分布的两个关键问题:语句集的划分和循环执行顺序的确定;其次,提出了面向最大聚合的凝聚图结点排序方法来指导循环合并,在不影响并行性的前提下减小了循环开销;最后,通过实验对提出的方法进行了验证。实验结果表明,对于测试用例,提出的方法能够生成正确的向量化代码,并且能够显著提高向量化程序的执行效率。     

基于KeY的程序分析和验证

可信性是各安全攸关领域软件的基础要求,例如航空航天飞行器控制软件、核电站控制软件和交通控制管理软件等,基于形式化方法的程序验证和分析是确保软件正确,具有可信性的重要手段。相比软件测试,基于定理证明的程序验证具有语法和语义的严格性,和属性相关的完备性。本文对程序形式化Hoare语义规约和相关的程序逻辑推理规则系统进行了详细的讨论。基于形式化验证平台Ke Y,采用完全自动化和交互式两种方法,对具有一定规模的,含有循环结构,并且具有实际意义的程序进行验证。研究证明过程的具体证明策略和方法,尤其是关于循环不变式的规约方法;对Ke Y的证明效率,先进性和局限性进行评估。     

面向自然语言需求的验证性质生成方法

安全关键系统和软件的安全性、可靠性需要形式化验证来保障,使用形式化验证的前提是从自然语言需求文本中提取相关验证性质并将其转化为形式化规约,这已成为当前形式化验证领域研究的热点和难点.当前的形式化规约提取工作大多针对英文需求,较少针对中文自然语言需求.此外,由于AADL具有强大的表达能力和完善的验证机制,已成为航空航天领域的主要建模语言之一,而现有的工作较少考虑如何从需求中提取AADL模型的验证性质.为了解决上述问题,本文提出一种面向自然语言需求的AADL模型验证性质自动生成方法,从自然语言需求中提取验证的相关性质,并将其转化为AADL模型验证工具AGREE可识别的形式化规约.首先,定义了模式定义语言(Contract Pattern Language, CPL),将需求划分为不同模式,并给出由固定句型和占位符组成的需求模板;其次,通过自然语言处理技术解析需求文本,获取替换需求模板中占位符的原子命题,以便生成完整的形式化规约;最后,设计并实现了相关工具,并将其用于工业界实际案例来说明该方法的可用性和有效性.     

若干算法程序的形式化推导与生成技术研究

PAR方法基于分划与递推、量词变换规则、循环不变式开发新策略和软件转换工具,实现了复杂算法问题的形式化开发.采用PAR方法形式化推导几个典型的算法问题.通过量词变换规则对程序规约进行形式化推导,可以得到具有数学引用透明性、易于形式化证明的求解算法问题的递推关系;并在此基础上,自然地导出循环不变式.在得到简短、易于理解、高可靠性的Apla算法程序之后,通过转换工具自动生成Java,C 等可执行程序.     

基于扩展逻辑变换系统_μTS证明循环优化正确性

循环优化对于提高Cache性能、发掘程序的并行性以及减少执行循环的开销都有着重要的作用,证明带循环优化功能的现代编译器的正确性已成为可信编译的一个挑战性的问题.形式化证明一个羽翼丰满的优化编译器本质上是不可行的,可以使用替代的方法,即不是证明优化编译器本身,而是形式化证明每一次循环变换前后编译对象的正确性.提出一种新颖的基于扩展逻辑变换系统μTS来证明循环优化正确性的方法.系统μTS在逻辑变换系统TS的基础上扩展了若干条派生规则,经谓词抽象将源程序与目标程序转换为形式化Radl语言后,使用μTS的派生规则能证明常见循环变换的正确性,如循环融合、循环分配、循环交换、循环反转、循环分裂、循环脱皮、循环调整、循环展开、循环铺盖、循环判断外提、循环不变代码外提等.循环优化可以看作一系列循环变换的组合,从而系统μTS能证明循环优化的正确性.为了支持自动化证明循环优化的正确性并出示证据,进一步提出了一个辅助证明算法.最后通过一个典型实例对这一方法进行了详细的阐述,实际效果表明了该方法的有效性.该方法对设计高可信优化编译器具有重要的指导意义.     

序列折半划分问题的形式化推导

形式化推导是在程序正确性证明理论下所进行的程序开发,最终得到完全正确的算法程序。针对序列折半划分问题,现有的形式化推导方法将推导与证明交替进行,推导过程繁琐且大多无法直接获得可执行程序。为解决上述问题,提出了一种新的序列折半划分问题的形式化推导方法。该方法基于分划递推的核心思想,应用规约变换技术对问题规约进行变换并严格保证一致性,使得在推导过程中无需交替证明,进而导出递推关系式并得到高可靠性抽象算法程序Apla,最终通过转换工具自动生成可执行程序。实现了从程序规约到具体可执行程序的完整程序求精过程。以2个序列算法为例,验证了该方法的有效性和可行性,对相关问题的形式化推导具有指导意义。     

循环条件的形式化推导在程序验证中的应用

提出了一种求解命令式程序中循环执行和终止条件的方法.该方法基于循环代码本身进行循环执行和终止条件的分析推导,可以定义一个原型工具进行自动化推导.现有的形式化方法依赖于形式化规范,而提出的方法适用于未被形式化的程序.提出的形式化方法可以在一个原型工具中实现,通过该工具来推导循环执行和终止条件,辅助程序验证和程序缺陷修正.     

自动向量化中基于数据依赖分析的循环分布算法

循环分布是开发向量化程序的一个有效的方法。但是由于程序中的数据相关性,当前的自动向量化编译器实现完全的循环分布非常困难。因此,当前的自动向量化编译器一般采用简单的循环分布方法。以数据依赖关系分析为基础,从有无依赖环的角度分析了程序中语句的向量化能力,提出了基于语句向量化识别的循环分布算法,并在自动向量化中加以实现。通过此方法,可以充分地分析语句或依赖环的向量化能力,最终采用循环分布,将可向量化的语句与不可向量化的语句分布在不同的循环中。该方法可以处理当前的自动向量化编译器无法向量化的循环,对一些语句间有依赖关系的循环可达到较好的效果。     

可信执行环境访问控制建模与安全性分析

可信执行环境(TEE)的安全问题一直受到国内外学者的关注. 利用内存标签技术可以在可信执行环境中实现更细粒度的内存隔离和访问控制机制, 但已有方案往往依赖于测试或者经验分析表明其有效性, 缺乏严格的正确性和安全性保证. 针对内存标签实现的访问控制提出通用的形式化模型框架, 并提出一种基于模型检测的访问控制安全性分析方法. 首先, 利用形式化方法构建基于内存标签的可信执行环境访问控制通用模型框架, 给出访问控制实体的形式化定义, 定义的规则包括访问控制规则和标签更新规则; 然后利用形式化语言B以递增的方式设计并实现该框架的抽象机模型, 通过不变式约束形式化描述模型的基本性质; 再次以可信执行环境的一个具体实现TIMBER-V为应用实例, 通过实例化抽象机模型构建TIMBER-V访问控制模型, 添加安全性质规约并运用模型检测验证模型的功能正确性和安全性; 最后模拟具体攻击场景并实现攻击检测, 评估结果表明提出的安全性分析方法的有效性.     

Validating More Loop Optimizations

Translation validation is a technique for ensuring that a translator, such as a compiler, produces correct results. Because complete verification of the translator itself is often infeasible, translation validation advocates coupling the verification task with the translation task, so that each run of the translator produces verification conditions which, if valid, prove the correctness of the translation. In previous work, the translation validation approach was used to give a framework for proving the correctness of a variety of compiler optimizations, with a recent focus on loop transformations. However, some of these ideas were preliminary and had not been implemented. Additionally, there were examples of common loop transformations which could not be handled by our previous approaches.This paper addresses these issues. We introduce a new rule Reduce for loop reduction transformations, and we generalize our previous rule Validate so that it can handle more transformations involving loops. We then describe how all of this (including some previous theoretical work) is implemented in our compiler validation tool TVOC.     

一种微控制器中零开销循环的实现方法

为扩展芯片的应用领域,增强芯片DSP的能力,提出一种用于MCU处理器支持零开销循环的设计方法。该方法依据在DSP程序中经常出现循环的特点,设计专门的硬件处理循环,用以消除循环转移造成的流水线等待,在分析MCU原有结构特别是指令单元的基础上,对循环指令采取与其他分支指令不同的处理方法。在尽量少改动原有MCU结构的前提下,支持零开销的循环。性能分析结果表明,改进后的MCU能有效减少循环执行周期。     

基于QBF的循环不变式构造技术

构造循环不变式是程序验证的核心问题之一。主流的循环不变式构造方法通常假设程序中的变量在无限数域上取值,然而程序执行过程中变量都是用有限长度的位向量来表示,无限数域上的循环不变式在有限数域的程序中可能不再是不变式,反之亦然。针对这一问题,本文给出一种基于QBF求解的构造有限数域上循环不变式的方法。该方法可用于构造类型丰富的不变式,包括线性(或多项式)等式(或不等式)不变式,支持加、减、乘、除、移位、位操作等,允许不变式中出现量词。本文也例证了该方法在程序终止性证明、循环上界分析、程序正确性证明等方面的应用价值。     

Integrated static code analysis and runtime verification

Static code analysis tools automatically generate alerts for potential software faults that can lead to failures. However, these tools usually generate a very large number of alerts, some of which are subject to false positives. Because of limited resources, it is usually hard to inspect all the alerts. As a complementary approach, runtime verification techniques verify dynamic system behavior with respect to a set of specifications. However, these specifications are usually created manually based on system requirements and constraints. In this paper, we introduce a noval approach and a toolchain for integrated static code analysis and runtime verification. Alerts that are generated by static code analysis tools are utilized for automatically generating runtime verification specifications. On the other hand, runtime verification results are used for automatically generating filters for static code analysis tools to eliminate false positives. The approach is illustrated for the static analysis and runtime verification of an open‐source bibliography reference manager software. Copyright © 2014 John Wiley & Sons, Ltd.     

DynaMICs: Comprehensive Support for Run-Time Monitoring

Software engineering strives to enable the economic construction of software systems that behave reliably, predictably, and safely. In other engineering disciplines, safety is assured in part by detailed monitoring of processes. In software, we may achieve some level of confidence in the operation of programs by monitoring their execution. DynaMICs is a software tool that facilitates the collection and use of constraints for software systems. In addition, it supports traceability by mapping constraints to system artifacts. Constraint specifications are stored separately from code; constraint-monitoring code is automatically generated from the specifications and inserted into the program at appropriate places; and constraints are verified at execution time. These constraint checks are triggered by changes made to variable values. We describe the architecture of DynaMICs, discuss alternative verification techniques, and outline research directions for the DynaMICs project.     

Loop Staggering,Loop Compacting:Restructuring Techniques for Thrashing Problem

Parallel loops account for the greatest amount of parallelism in numerical programs.Executing nested loops in parallel wit low run-time overhead is thus very important for achieving high performance in paralleo processing systems.However,in parallel processing systems with caches of local memories in memory hierarchies,“thrashing problemmay” may arise when data move back and forth frequently between the caches or local memories in different processors.The techniques associated with parallel compiler to solve the problem are not completely developed.In this paper,we present two restructuring techniques called loopg staggering,loop staggering and compacting,with which we can not only eliminate the cache or local memory thrashing phemomena significantly,but also exploit the potential parallelism existing in outer serial loop.Loop staggering benefits the dynamic loop scheduling strategies,whereas loop staggering and compacting is good for static loop scheduling strategies,Our method especially benefits parallel programs,in which a parallel loop is enclosed by a serial loop and array elements are repeatedly used in the different iterations of the parallel loop.     

一个有效的并行分析算法

并行分析在并行编译系统中有着很重要的作用,它的优劣直接影响到编译系统的成败,随着机群系统及其并行开发环境的发展,多数的并行系统可支持多重并行循环的运行。而对只支持一重并行循环的编程系统,选择并行运行效率最高的循环,也是很重要的。为此,本文提出了一个有效的循环并行分析方案,它不但能给出多层循环的并行性,而且能够处理绝大部分实际应用中的并行性问题,本文对传统的并行分析算法进行修改,并给出了一个有效的并     

降低指令存储器功耗的一种有效方法：循环缓冲

在超长指令字结构的数字信号处理器中,其指令存储器的功耗所占比重较大。但是,根据数字信号应用的特点,可以采用循环缓冲来减小指令存储器的功耗。本文提出了一种编译器控制的循环缓冲技术,由编译器选择合适的循环代码将其放入循环缓冲,从而减小了取指过程中指令存储器的功耗;给出了循环缓冲的体系结构设计、功耗分析以及有效利用循环缓冲的编译方法;最后用功能级功耗模型验证了该方法的有效性。     

3种提高软件流水有效性的算法:比较和结合

软件流水是开发循环程序指令级并行性的技术,它通过并行执行连续的多个循环体来加快循环的执行速度.在软件流水中,循环体的重叠增加了寄存器需求,导致寄存器压力增大,当目标处理机所提供的寄存器不足时,软件流水可能失败.在Itanium处理机上评估了NAS和SPEC2000基准程序中的软件流水循环的寄存器需求,发现静态寄存器不足是造成软件流水失败的主要原因,提出了3种增加软件流水个数、提高软件流水有效性的算法:限制循环展开因子的算法(register sensitive unrolling,简称RSU)、堆栈寄存器分配算法(stacked registerallocation,简称SRA)以及变量类型转换的算法(variabletype conversion,简称VTC).RSU根据静态寄存器需求确定一个合理的展开因子,增加了软件流水的成功率;SRA和VTC分别使用空闲的堆栈寄存器和旋转寄存器来充当静态寄存器,提高了寄存器的利用率.在面向Itanium处理器的开放源码编译器ORC(open research compiler)上实现了这3种算法,通过NAS程序的测试比较了这3种算法的有效性,同时对它们的结合应用进行了研究和实验.     

The Static Parallelization of Loops and Recursions

We demonstrate approaches to the static parallelization of loops and recursions on the example of the polynomial product. Phrased as a loop nest, the polynomial product can be parallelized automatically by applying a space-time mapping technique based on linear algebra and linear programming. One can choose a parallel program that is optimal with respect to some objective function like the number of execution steps, processors, channels, etc. However,at best,linear execution time complexity can be atained. Through phrasing the polynomial product as a divide-and-conquer recursion, one can obtain a parallel program with sublinear execution time. In this case, the target program is not derived by an automatic search but given as a program skeleton, which can be deduced by a sequence of equational program transformations. We discuss the use of such skeletons, compare and assess the models in which loops and divide-and-conquer resursions are parallelized and comment on the performance properties of the resulting parallel implementations.