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.

Fri 20 Nov
Times are displayed in time zone: Central Time (US & Canada) change

13:00 - 14:20: F-4BOOPSLA at SPLASH-III +12h
Chair(s): Aviral GoelNortheastern University, Ton Chanh LeStevens Institute of Technology
13:00 - 13:20
Talk
OOPSLA
Cyril SixKalray / Grenoble Alps University / CNRS / Grenoble INP / VERIMAG, Sylvain BoulméGrenoble Alps University / CNRS / Grenoble INP / VERIMAG, David MonniauxGrenoble Alps University / CNRS / Grenoble INP / VERIMAG
Link to publication DOI Media Attached
13:20 - 13:40
Talk
OOPSLA
Christoph SprengerETH Zurich, Tobias KlenzeETH Zurich, Marco EilersETH Zurich, Felix A. WolfETH Zurich, Peter MüllerETH Zurich, Martin ClochardETH Zurich, David BasinETH Zurich
Link to publication DOI Media Attached
13:40 - 14:00
Talk
OOPSLA
Yaniv DavidTechnion, Uri AlonTechnion, Eran YahavTechnion
Link to publication DOI Pre-print Media Attached
14:00 - 14:20
Talk
OOPSLA
Fei HeTsinghua University, Jitao HanTsinghua University
Link to publication DOI Media Attached

Sat 21 Nov
Times are displayed in time zone: Central Time (US & Canada) change