Dargent: A Silver Bullet for Verified Data Layout Refinement

Zilin Chen, Ambroise Lafont, Liam O'Connor, Gabriele Keller, Craig McLaughlin, Vincent Jackson, Christine Rizkallah

Research output: Contribution to journalArticlepeer-review


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 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.
Original languageEnglish
Article number47
Number of pages27
JournalProceedings of the ACM on Programming Languages
Issue numberPOPL
Publication statusPublished - 9 Jan 2023
EventThe 50th ACM SIGPLAN Symposium on Principles of Programming Languages, 2023 - Boston, United States
Duration: 15 Jan 202321 Jan 2023
Conference number: 50


  • certifying compiler
  • data refinement
  • systems programming


Dive into the research topics of 'Dargent: A Silver Bullet for Verified Data Layout Refinement'. Together they form a unique fingerprint.

Cite this