BBB : Room access code 756979
25 February 2021 - 14h00
Certified Superblock Scheduling for the CompCert Compiler
by Cyril SIX from Kalray / Verimag
Abstract: CompCert is a C to assembly compiler, with a formal proof of semantic preservation written in Coq.
It already features a number of simple optimizations such as constant propagation or common subexpression elimination, however to this day it lacks more advanced optimizations such as instruction scheduling, loop invariant code motion or strength reduction.
We previously introduced postpass list scheduling in CompCert, an optimization reordering the instructions at the Asm level within basicblocks (after register allocation).
I will present in this talk our newest optimization: prepass superblock scheduling, a second scheduling pass with the scope of superblocks, at the RTL level (before register allocation).
Combined with loop invariant code motion (not presented here) and loop unrolling, we achieve performance close to GCC -O2 on in-order processors.
