Formally Verified Superblock Scheduling

International audience; Necula [2000] and Tristan et al. [2011] established that symbolic execution combined with rewriting is effective in validating the code produced by state-of-the-art compilers applying various optimizations. In the meantime, Tristan and Leroy [2008] used formally-verified symbolic execution to certify the schedules produced by untrusted oracles-optimizing pipeline usage-within the CompCert compiler. Alas, their formally-verified checker had exponential complexity and was thus never integrated into mainline CompCert. Recently, Six et al. [2020] solved this performance issue with formally-verified hash-consing within the symbolic execution. Our paper extends these approaches to superblocks (where instructions move across branches) and enables translation validation of instruction rewritings (changing instructions for "better" ones) modulo register liveness (e.g. with introduction of "fresh" registers): a significant step forward for certifying compilers from symbolic executions.