机械化验证一个高效的迭代数据流求解算法

Mechanized Verification of Efficient Iterative Data-flow Algorithm

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

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.