中国科学院软件研究所机构知识库
Advanced  
ISCAS OpenIR  > 软件所图书馆  > 期刊论文
Title:
基于扩展逻辑变换系统_μTS证明循环优化正确性
Alternative Title: Verifying the Correctness of Loop Optimization Based on Extended Logic Transformation System μTS
Author: 王昌晶
Keyword: 循环优化 ; 可信编译 ; 扩展逻辑变换系统 ; 循环变换 ; 辅助证明算法
Source: 计算机研究与发展
Issued Date: 2012
Volume: 49, Issue:9, Pages:1863-1873
Indexed Type: CNKI ; EI ; WANFANG
Department: 江西师范大学计算机信息工程学院;计算机科学国家重点实验室(中国科学院软件研究所);中国科学院研究生院;
Sponsorship: 江西省教育厅青年科学基金项目(GJJ09461)
Abstract: 循环优化对于提高Cache性能、发掘程序的并行性以及减少执行循环的开销都有着重要的作用,证明带循环优化功能的现代编译器的正确性已成为可信编译的一个挑战性的问题.形式化证明一个羽翼丰满的优化编译器本质上是不可行的,可以使用替代的方法,即不是证明优化编译器本身,而是形式化证明每一次循环变换前后编译对象的正确性.提出一种新颖的基于扩展逻辑变换系统μTS来证明循环优化正确性的方法.系统μTS在逻辑变换系统TS的基础上扩展了若干条派生规则,经谓词抽象将源程序与目标程序转换为形式化Radl语言后,使用μTS的派生规则能证明常见循环变换的正确性,如循环融合、循环分配、循环交换、循环反转、循环分裂、循环脱皮、循环调整、循环展开、循环铺盖、循环判断外提、循环不变代码外提等.循环优化可以看作一系列循环变换的组合,从而系统μTS能证明循环优化的正确性.为了支持自动化证明循环优化的正确性并出示证据,进一步提出了一个辅助证明算法.最后通过一个典型实例对这一方法进行了详细的阐述,实际效果表明了该方法的有效性.该方法对设计高可信优化编译器具有重要的指导意义.
English Abstract: Loop optimization plays an important role in improving cache performance, making effective use of parallel processing capabilities, and reducing overheads associated with executing loops. Verifying the correctness of modern compilers with loop optimization is a challenge of trustworthy compiling. Formally verifying a full-fledged optimizing compiler is not feasible in nature. Rather than verifying the compiler itself, after every run of the loop transformation, formally verifing the target code produced is a correct translation of the source program. A novel approach is proposed to verify the correctness of loop optimization based on extended logic transformation system μTS, which extends a number of derived rules from logic transformation TS. After converting source program and target code into formal language Radl by predicate abstracting, one can verify the correctness of common loop transformations using the derived rules of μTS, such as loop fusion, loop distribution, loop interchange, loop reversal, loop splitting, loop peeling, loop alignment, loop unrolling, loop tiling, loop unswitching, loop-invariant code motion, etc. Loop optimization can be regarded as a series of loop transformation composition so that μTS can verify the correctness of loop optimization. Furthermore, an aided certified algorithm is put forward in order to automatic verify the correctness of loop optimization and show its proof. Finally this approach is elaborated using one typical example. Practical effects manifest its effectiveness. This approach has important instructive significance in designing high-trusted optimization compiler.
Language: 中文
Content Type: 期刊论文
URI: http://ir.iscas.ac.cn/handle/311060/14983
Appears in Collections:软件所图书馆_期刊论文

Files in This Item:

There are no files associated with this item.


Recommended Citation:
王昌晶. 基于扩展逻辑变换系统_μTS证明循环优化正确性[J]. 计算机研究与发展,2012-01-01,49(9):1863-1873.
Service
Recommend this item
Sava as my favorate item
Show this item's statistics
Export Endnote File
Google Scholar
Similar articles in Google Scholar
[王昌晶]'s Articles
CSDL cross search
Similar articles in CSDL Cross Search
[王昌晶]‘s Articles
Related Copyright Policies
Null
Social Bookmarking
Add to CiteULike Add to Connotea Add to Del.icio.us Add to Digg Add to Reddit
所有评论 (0)
暂无评论
 
评注功能仅针对注册用户开放,请您登录
您对该条目有什么异议,请填写以下表单,管理员会尽快联系您。
内 容:
Email:  *
单位:
验证码:   刷新
您在IR的使用过程中有什么好的想法或者建议可以反馈给我们。
标 题:
 *
内 容:
Email:  *
验证码:   刷新

Items in IR are protected by copyright, with all rights reserved, unless otherwise indicated.

 

 

Valid XHTML 1.0!
Copyright © 2007-2019  中国科学院软件研究所 - Feedback
Powered by CSpace