publications
2024
- TASE 2024Verified Validation for Affine Scheduling in Polyhedral CompilationXuyang Li, Hongjin Liang, and Xinyu FengIn Theoretical Aspects of Software Engineering, 2024
Structural nested loops can be abstracted into polyhedral models, based on which one can perform aggressive loop optimizations; however, the optimizations are often heuristic and complex, and therefore error-prone. Meanwhile, verified compilers, though rigorously correct, still miss powerful optimizing transformations and therefore produce less efficient code than industrial ones. To bridge this gap, this work provides a general verified validation framework based on Bernstein’s conditions for affine scheduling, the core component of polyhedral optimization techniques. It is parameterized over the concrete definitions and proofs of the instruction language to be reusable. As shown in our evaluation, the framework is flexible enough to support both existing verified compilers like CompCert and existing polyhedral compilers like Pluto. The result is fully mechanized in the Coq proof assistant.
@inproceedings{10.1007/978-3-031-64626-3_17, author = {Li, Xuyang and Liang, Hongjin and Feng, Xinyu}, editor = {Chin, Wei-Ngan and Xu, Zhiwu}, title = {Verified Validation for Affine Scheduling in Polyhedral Compilation}, booktitle = {Theoretical Aspects of Software Engineering}, year = {2024}, publisher = {Springer Nature Switzerland}, address = {Cham}, pages = {287--305}, isbn = {978-3-031-64626-3}, }