机械化验证一个高效的迭代数据流求解算法
作者:
作者单位:

作者简介:

江南(1976-),女,博士,副教授,CCF专业会员,主要研究领域为可信软件,机器证明,编程语言;张晓瞳(1989-),男,硕士,主要研究领域为可信软件,可信编译,软件缺陷预测;汪吕蒙(1988-),男,硕士,主要研究领域为CPU+GPU异质系统架构,GPGPU功耗优化;何炎祥(1952-),男,博士,教授,博士生导师,CCF会士,主要研究领域为可信软件,分布式并行处理,高性能计算

通讯作者:

何炎祥,E-mail:yxhe@whu.edu.cn

中图分类号:

TP311

基金项目:

国家自然科学基金(61972293);国家留学基金委地方合作项目(201808420414)


Mechanized Verification of Efficient Iterative Data-flow Algorithm
Author:
Affiliation:

Fund Project:

  • 摘要
  • |
  • 图/表
  • |
  • 访问统计
  • |
  • 参考文献
  • |
  • 相似文献
  • |
  • 引证文献
  • |
  • 资源附件
  • |
  • 文章评论
    摘要:

    迭代计算数据流等式的解,是数据流分析的常用方法.计算支配节点,从而识别自然循环,是许多现代编译器优化分析的重要组成部分.机械化验证高效的求解支配节点的算法通常是获得一个实际的“验证编译器”不可或缺的一部分.为了形式化证明一个高效的迭代求解严格支配节点的算法(CHK),首先建立了值域是逆序列表集合的半格结构,逆序列表中的元素是控制流图中节点的逆后序遍历次序,并证明了它是一个半格,其偏序满足上升链条件.然后使用半格结构,实现了一个基于工作表的Kildall迭代算法,计算严格支配节点.接下来,首先给出了控制流图中支配节点的定义性规范和相关性质定理,然后构造并证明了迭代求解算法所满足的重要性质.利用这些性质定理,相对于定义性规范,证明了该迭代求解算法的正确性和完备性.最后进行总结,并讨论未来工作.整个形式化开发使用的是定理证明助手Isabelle/HOL.

    Abstract:

    The common way of performing data-flow analysis of programs is by solving the data-flow equations using an iterative algorithm. Finding dominators, thus identifying natural loops, is central to numerous modern compiler optimization. Basically, mechanized verification of an efficient algorithm of computing dominators is intergral part of a verified compiler. In order to prove an efficient algorithm of computing strict dominators formally, first, a semilattice structure whose domain is a set of all descending lists in which nodes in a control flow graph are represented by its reverse post order (rPO) number is constructed and proved to be a semilattice whose ordering satisfies the ascending chain condition. Then, using the semilattice structure, a worklist-based Kildall's algorithm that computes strict dominators is implemented. Next, a specification of dominators on a control flow graph is defined; key properties of the specification and the iterative algorithm are established, and the correctness and completeness of the algorithm are proved with respect to the definitional specification. Finally, the work is summarized and future research is presented. The whole development is carried out in Isabelle/HOL.

    参考文献
    相似文献
    引证文献
引用本文

江南,汪吕蒙,张晓瞳,何炎祥.机械化验证一个高效的迭代数据流求解算法.软件学报,2022,33(6):2115-2126

复制
分享
文章指标
  • 点击次数:
  • 下载次数:
  • HTML阅读次数:
  • 引用次数:
历史
  • 收稿日期:2021-08-16
  • 最后修改日期:2021-10-14
  • 录用日期:
  • 在线发布日期: 2022-01-28
  • 出版日期: 2022-06-06
您是第位访问者
版权所有:中国科学院软件研究所 京ICP备05046678号-3
地址:北京市海淀区中关村南四街4号,邮政编码:100190
电话:010-62562563 传真:010-62562533 Email:jos@iscas.ac.cn
技术支持:北京勤云科技发展有限公司

京公网安备 11040202500063号