Verifying the Correctness of Loop Optimization Based on Extended Logic Transformation System μTS

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.