基于时序逻辑证明编译优化程序变换的保义性

基于时序逻辑CTL(computation tree logic)的一种扩展CTL-FV对优化编译中的语句交换和变量替换这两种常见变换的保义性条件给出了形式刻画,采用含条件重写规则定义了保义语句交换T_exch和保义变量替换T_sub,并基于一种归纳证明框架对它们的保义性进行了证明.此外,基于变换Texch对程序基本块内保依赖语句重排的保义性也给出了一种构造性的证明.     

基于线性表出的非奇异循环变换局部性优化方法

开发程序的局部性是当今并行编译优化研究的重点之一，而程序变换是开发程序时间局部性和空间局部性的重要手段之一．该文提出了一种新的利用非奇异循环变换来优化程序局部性的局部性优化方法，即基于线性表出的循环变换．该方法利用一组最少的线性无关向量组来线性表出数组访问的下标表达式，并据此构造非奇异变换矩阵来优化数组访问的时间局部性和空间局部性．该方法能充分开发数组访问的时间局部性，能简便地确定是否能对数组访问进行时间局部性或空间局部性优化，并能对给定的嵌套循环同时进行时间局部性和空间局部性优化．实验结果表明了该文所提出的基于线性表出的非奇异循环变换局部性优化方法是有效的．     

基于CTL的循环优化变换描述方法

TRANS是基于CTL的优化变换描述语言,对TRANS语言作了宏扩展,给出了循环嵌套、循环归纳变量、循环依赖及方向向量的时序逻辑描述.从依赖分析的角度对重排序循环优化变换加以考查,并以循环逆转和循环交换为例阐述了其形式化描述方法.     

基于重排序变换和循环分布的通信优化算法

针对现有通信优化算法无法使MPI自动并行化编译器生成加速比理想的消息传递程序问题,提出了一种基于重排序变换和循环分布的通信优化算法。该算法根据给出的过程间副作用集合和基于mpi_wait/mpi_irecv移动的重排序变换规则,有序地采用重排序变换和循环分布,尽可能安全地扩大点到点非阻塞通信中通信与计算的重叠窗口,使MPI自动并行化编译器生成具有更多计算重叠通信的消息传递代码。实验结果表明,该算法能够隐藏更多的点到点非阻塞通信开销,并且明显提升消息传递程序的加速比。     

基于分离逻辑的程序验证技术

介绍了分离逻辑的验证原理和特点及其在程序验证方面的应用实例,分析了为支持程序验证的若干分离逻辑研究进展,包括分离逻辑的自身属性、与其他逻辑的关系、对程序语言和设计模式的支持以及定理证明器等内容.指出了分离逻辑进一步深入应用所面临的问题和解决方向.     

基于DSA的扩展自证明签名方案

自证明签名对验证者来说一次仅验证了两个签名，而在PMI系统中，验证者除了要认证用户身份，其中包括两个验证：一个是验证用户的签名，另一个是验证CA颁发的公钥证书，还需要验证AA颁发的属性证书。针对此问题，该文对自证明签名做了一定的扩展，提出了扩展自证明签名ESCS方案，ESCS由验证两个签名扩展到可同时验证3个签名，此后又对ESCS方案做了进一步的扩展，扩展后的ESCS方案可以同时验证多个签名。     

Radl 形式规格说明相对正确性研究

在形式规格说明的获取任务中,一个重要问题是验证获取得到的形式规格说明的正确性.即给定一个问题需求P,往往可以获取多种不同形式的规格说明,如何验证这些不同形式的规格说明均正确?问题需求的非(半)形式化与形式规格说明的形式化两者之间差异的本性,使得该问题成为软件需求工程中一个具有挑战性的问题.提出一种基于形式化推导的方法来验证同一问题不同形式规格说明的相对正确性,通过证明不同形式规格说明与问题需求某个最为直截明了的形式规格说明Si等价来实现,而Si使用PAR方法和PAR平台转换为可执行程序,通过测试已经得到确认.为了支持该方法,进一步提出了扩展的逻辑系统和辅助证明算法.使用Radl语言作为形式规格说明语言,通过排序搜索、组合优化领域的两个典型实例对该方法进行了详细的阐述.实际使用效果表明,该方法不仅能够有效地验证Radl形式规格说明的正确性,还具备良好的可扩充性.该方法在规格说明的正确性验证、算法优化、程序等价性证明等研究领域具有潜在的理论意义与应用价值.     

通过程序变换对数字系统进行优化

在文章[10]中,我们详细地讨论了如何用函数式硬件描述语言对数字电路进行描述、综合和模拟验证的方法。本文将在此基础上,进一步研究函数或硬件描述语言的代数性质并通过程序变换对所描述的电路进行综合和优化,从而设计出正确的优化逻辑结构,在这种逻辑结构中去除了冗余,最大限度地重复使用各个子部件。文章中给出了变换规则和变换的算法及若干示例。     

一种基于HASH变换的循环散列分档排序算法

在数据排序问题中,各种分段快速排序算法[3～11]只有对特定的数据分布类型或者符合ΔM相似文献   

CC-NUMA并行系统通信优化的变换技术

减少通信开销是并行编译优化的主要目标之一.该文针对具有cache一致性的非一致存储访问并行系统(CC-NUMA)的特点,提出通过结合计算变换和数据变换,在统一的代数框架下对并行程序进行通信优化的策略和方法.通过实验测试,验证了此策略和方法是行之有效的.     

基于半扩展规则的定理证明方法

自动定理证明一直是人工智能领域中最重要的问题之一,基于归结的方法是通过推出空子句的方法来判定子句集的可满足性.基于扩展规则的定理证明方法在一定意义上是和归结原理对偶的方法,是通过子句集能否推导出所有极大项组成的子句集来判定可满足性.通过对扩展规则的研究给出了半扩展规则的概念,并提出了基于半扩展规则的定理证明算法SER.然后分析及证明了该算法的正确性、完备性和复杂性.实验结果表明,算法SER的执行效率较基于归结的有向归结算法DR和基于扩展规则算法IER,NER有明显的提高.     

使用扩展逻辑效力的逻辑路径尺寸优化方法

为解决集成电路物理设计中考虑互连线影响的逻辑路径延迟优化问题,提出一个计入互连线负载的扩展的逻辑效力(ELE),并针对ELE给出一个可同时优化逻辑路径中各个逻辑门尺寸及各段互连线长度的优化流程.ELE在保留原有逻辑效力参数的同时,使用互连寄生参数提取软件获得的Ⅱ型互连线参数,实现对带有互连线负载的逻辑门的传播延迟的描述和估计;逻辑路径优化流程采用效力延迟分配策略作为初始条件来表示各段互连线负载对总效力延迟的影响,将所用目标单元库和制造工艺的物理尺寸信息作为限制条件,以ELE表达式为核心展开优化计算,辅以动态规划办法,无需迭代运算,仅通过一轮计算即可求得全部结果.实验结果表明,该流程计算任务简单,资源耗费少,可以准确、快速地获得所需的逻辑门尺寸和互连线长度;结果清晰合理,与目标单元库和工艺库完全兼容.     

基于可信计算的企业云签证协议设计与证明

为解决当前企业云内部部门之间通信时缺乏身份认证的问题,提出基于可信计算的企业云签证方法与协议,并对其进行证明和分析。在可信云vTPM架构基础上,通过设计vAIK签证协议,建立vTPM与企业云部门终端之间的身份对应关系并保证了vTPM签名能力的合法性。通过设计vTPM远程证明协议使得企业云内部通信时的消息发送方身份可验。vAIK签证过程中的报告由云平台签名、远程证明过程中的报告由云平台和vTPM共同签名以保证消息发送方的身份真实性,并在vAIK签证和远程证明过程中加入随机数保证报告新鲜性。最后使用SVO逻辑对vTPM证书签证和远程证明协议进行了证明与分析,结果表明该设计能够达到理想目标。     

带测试动作的动态时序逻辑扩展

作为一种动态知识表示形式,动态时序逻辑(DLTL)尤适用于正规程序验证,然而它不直接支持测试动作,这使得其应用受到一定限制。为支持测试动作,提出一个DLTL扩展DLTL+和一个判定DLTL+公式可满足性的tableau算法,并给出了算法的正确性以及其时间复杂度为2O(n)的证明。分析表明,DLTL+提供了一种直接的、有效的测试动作支持方式,该方式比已知的其他方式更具有实际应用价值。     

基于DM6446的5/3小波变换优化方法

JPEG2000技术中对图像块进行的无损压缩采用5/3小波滤波作为变换方式,本文讨论嵌入式平台上针对5/3小波滤波器的优化技术.文章基于TI公司开发的DM6446(达芬奇)DSP平台,从理论上详细地阐述了几种典型的DSP程序优化方法,其中包括添加优化选项、循环分解、SPLOOP技术以及编排软件流水等.实验表明,通过将这些方法综合应用到整数滤波算法的优化过程中去,能够明显提升算法的执行效率,优化效果达到10倍左右.     

三值逻辑证明系统及正例与反例的提取

三值逻辑模型检验是对更高层的模型抽象验证的一种方法,对其验证中常常需要给出正例和反例.为此,讨论了三值逻辑模型检验以及正例和反例的提取,并在给出一套三值逻辑证明规则的基础上形成一个证明系统;运用该系统可以证明模型是否满足某个性质;在证明过程中为存在路径量词提取正例,为全称路径量词提取反例.正例和反例的提取可给模型的细化指明方向.最后通过实例给出了该证明系统在数字逻辑电路验证中的应用.     

基于Tree-SSA优化框架的高级循环优化

现代的计算机处理器和计算机系统实现了很多先进技术,要利用这些技术更需要编译器的支持以取得高性能。GCC中Tree-SSA优化框架提供了一个功能强大的程序分析框架。增强的数据依赖分析信息允许编译器变换一个算法以取得更大的局部性,提高资源的利用率以增大吞吐量,提高性能。该文对数据依赖、矩阵变换、循环变换进行了研究,分析了它们的特点,算法和性能,陈述了GCC中循环变换的现状,对以后的研究做出了一定的展望。     

面向SIMD扩展部件的循环优化研究

高性能微处理器中普遍采用SIMD向量扩展作为计算加速部件。在深入研究SIMD扩展部件数据依赖关系约束条件的基础上,提出一种基于依赖关系逆向图的Tarjan扩展算法,提高了SIMD并行性识别率,并结合传统向量化方法,实现了面向SIMD扩展部件的循环优化技术,消除了不可向量化语句对可向量化语句在数据重组中不必要的开销。实际程序测试结果显示,其在基于依赖关系的SIMD并行性判定方面优于ICC编译器,经过循环优化后,最终生成的SIMD代码其执行效率平均提高了12%。