Certified and efficient instruction scheduling: application to interlocked VLIW processors
Cyril Six, Sylvain Boulmé, David Monniaux
Abstract
CompCert is a moderately optimizing C compiler with a formal, machine-checked, proof of correctness: after successful compilation, the assembly code has a behavior faithful to the source code. Previously, it only supported target instruction sets with sequential semantics, and did not attempt reordering instructions for optimization. We present here a CompCert backend for a VLIW core ( i.e. with explicit parallelism at the instruction level), the first CompCert backend providing scalable and efficient instruction scheduling. Furthermore, its highly modular implementation can be easily adapted to other VLIW or non-VLIW pipelined processors.
Topics & Concepts
Very long instruction wordComputer scienceParallel computingCompilerInstruction-level parallelismScalabilityCorrectnessInstruction schedulingModular designProgramming languageInstruction setScheduling (production processes)Code generationComputer architectureOptimizing compilerParallelism (grammar)Operating systemDynamic priority schedulingTwo-level schedulingKey (lock)EconomicsOperations managementScheduleParallel Computing and Optimization TechniquesLogic, programming, and type systemsSoftware Testing and Debugging Techniques