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

Loop Optimization Transformation Using CTL Specifications

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

Formal specification was required for implementation and correctness validate of loop optimization. TRANS, a specification language based on CTL for optimization transformations, adopts rewrite rule with side conditions to express program transformation. TRANS was macro-expanded and given temporal logic specification of loop nest, induction variable, loop dependence and direction vector. The reordering loop optimization transformation was investigated from the perspective of dependence analysis and specified, meanwhile the two examples loop reversal and loop interchange were given.