VLIM: Verified Loop Interchange for Optimised Matrix Multiplication

Loop optimisations are essential for achieving high performance in modern computing, particularly for memoryintensive operations. However, while unverified optimisers achieve impressive speedups, their manual application is error-prone and challenging to verify, making them risky in high-assurance computing platforms. This paper introduces VLIM, a novel rewrite algebra, to overcome these difficulties, enabling the development and automatic verification of loop transformations within the Capla programming language, a formally defined front-end for the Compcert verified compiler. Our framework allows compiler developers to define rewrite rules, with correctness proofs automatically derived through rewrite composition, ensuring semantic preservation during optimisation. We demonstrate the effectiveness of our approach, VLIM, by implementing a loop interchange optimisation and evaluating its impact on matrix multiplication performance. Empirical analyses show significant performance improvements: for a 1000 × 1000 matrix, loop interchange using VLIM reduced runtime by 36.6% and 74.6%when compiled with Compcert and Clang, respectively. This workadvances the state-of-the-art in verified compilation, offering apromising direction for developing high-performance, formallyverified software.