Formally verified superblock scheduling
Cyril Six, Léo Gourdin, Sylvain Boulmé, David Monniaux, Justus Fasse, Nicolas Nardino
Abstract
On in-order processors, without dynamic instruction scheduling, program running times may be significantly reduced by compile-time instruction scheduling. We present here the first effective certified instruction scheduler that operates over superblocks (it may move instructions across branches), along with its performance evaluation. It is integrated within the CompCert C compiler, providing a complete machine-checked proof of semantic preservation from C to assembly.
Topics & Concepts
Computer scienceCompilerInstruction schedulingParallel computingScheduling (production processes)Compile timeProcessor schedulingProgramming languageDynamic priority schedulingOperating systemTwo-level schedulingScheduleOperations managementEconomicsParallel Computing and Optimization TechniquesDistributed systems and fault toleranceLogic, programming, and type systems