A version of the CompCert certified compiler with
- global common subexpression elimination
- loop-invariant code motion strength reduction
- pre-pass and post-pass instruction scheduling for pipelined processors and in particular for the Kalray VLIW core (with explicit instruction parallelism at the assembly level)
See the 5-minutes video by C. Six, presenting our certified efficient instruction scheduling for the KVX backend.
