Wed 18 Jan 2023 17:35 - 18:00 at Avenue34 - Verified Compilation Chair(s): Ralf Jung

Systems programmers need fine-grained control over the memory
layout of data structures, both to produce performant code and to comply with well-defined interfaces imposed by existing code, standardised protocols or hardware. Code that manipulates these low-level representations in memory is hard to get right. Traditionally, this problem is addressed by the implementation of tedious marshalling code to convert between compiler-selected data representations and the desired compact data formats. Such marshalling code is error-prone and can lead to a significant runtime overhead due to
excessive copying. While there are many languages and systems that address the correctness issue, by automating the generation and, in some cases, the verification of the marshalling code, the performance overhead introduced by the marshalling code remains.
In particular for systems code, this overhead can be prohibitive.
In this work, we address both the correctness and the performance problems.

We present a data layout description language and data refinement framework,
called Dargent, which allows programmers to declaratively specify
how algebraic data types are laid out in memory.
Our solution is applied to the Cogent language,
but the general ideas behind our solution are applicable to other settings.
The Dargent framework generates C code that manipulates data directly with the desired memory layout,
while retaining the formal proof that this generated C code is correct
with respect to the \cogent functional semantics.
This added expressivity removes the need for implementing and verifying marshalling code,
which eliminates copying, smoothens interoperability with surrounding systems,
and increases the trustworthiness of the overall system.

Wed 18 Jan

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

16:45 - 18:00
Verified CompilationPOPL at Avenue34
Chair(s): Ralf Jung ETH Zürich
DimSum: A Decentralized Approach to Multi-language Semantics and VerificationDistinguished Paper
Michael Sammler MPI-SWS, Simon Spies MPI-SWS, Youngju Song Seoul National University; MPI-SWS, Emanuele D’Osualdo MPI-SWS, Robbert Krebbers Radboud University Nijmegen, Deepak Garg MPI-SWS, Derek Dreyer MPI-SWS
Formally Verified Native Code Generation in an Effectful JIT: Turning the CompCert Backend into a Formally Verified JIT Compiler
Aurèle Barrière University of Rennes; Inria; CNRS; IRISA, Sandrine Blazy University of Rennes; Inria; CNRS; IRISA, David Pichardie Meta
DOI Pre-print
Dargent: A Silver Bullet for Verified Data Layout Refinement
Zilin Chen UNSW, Ambroise Lafont University of Cambridge, Liam O'Connor University of Edinburgh, Gabriele Keller Utrecht University, Craig McLaughlin UNSW, Vincent Jackson University of Melbourne, Christine Rizkallah University of Melbourne