SPLASH 2020
Sun 15 - Sat 21 November 2020 Online Conference
Fri 20 Nov 2020 13:00 - 13:20 at SPLASH-III - F-4B Chair(s): Aviral Goel, Ton Chanh Le
Sat 21 Nov 2020 01:00 - 01:20 at SPLASH-III - F-4B

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.

We present here a CompCert backend for a VLIW core (\textit{i.e.} with explicit parallelism at the instruction level), the first CompCert backend providing scalable and efficient instruction scheduling. Furthermore, its highly modular implementation can be easily adapted to other VLIW or non-VLIW pipelined processors.

Conference Day
Fri 20 Nov

Displayed time zone: Central Time (US & Canada) change

Conference Day
Sat 21 Nov

Displayed time zone: Central Time (US & Canada) change