Certified Compiler Backends for VLIW Processors Highly Modular Postpass-Scheduling in the CompCert Certified Compiler

CompCert is a C compiler with a formal, machine-checked, proof of correctness: after successful compilation, the object code has a behavior faithful to the source code. It is moderately optimizing; in particular, it does not reorder instructions. To get good performance for in-order and, more specifically, VLIW processors (processors with explicit parallelism at the instruction level), it is necessary to reorder instructions. Previous attempts at reordering instructions in CompCert did not scale. We present here a scalable, efficient approach for scheduling and reordering instructions in CompCert backends. We apply it to the VLIW assembly of the Kalray K1C processor, but our approach has wider scope