Room 206 (2nd floor, badged access)
22 octobre 2020 - 14h15
Certified and Efficient Instruction Scheduling. Application to Interlocked VLIW Processors.
par Cyril Six de Kalray - Verimag
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.
The talk will present two novel contributions on CompCert:
- scalable scheduling optimizations for multiple-issue pipelined cores, by embedding untrusted schedulers (greedy, ILP, etc), dynamically checked with verified symbolic execution.
- verified code generation for an interlocked VLIW processor, ie with explicit instruction parallelism in the assembly language.
This is a joint work with Sylvain Boulmé and David Monniaux.
This will be a training talk for our presentation at the OOPSLA'20 conference. For people who will not physically attend to the talk at Verimag, we will provide an online video (for OOPSLA'20 by early November).
