一句话：提出 Dargent 数据布局描述语言与精化框架，为 Cogent 生成带形式正确性证明的 C 代码，消除 marshalling 复制开销。
系统程序员需要对数据结构内存布局进行细粒度控制，以生成高性能代码并兼容现有代码、标准协议或硬件，但操作低级内存表示既困难又易错。传统做法是编写繁琐的 marshalling 代码，在编译器表示与紧凑格式间转换，既易错又因复制带来显著运行时开销；已有自动化或验证 marshalling 的方案仍未消除该开销。本文提出 Dargent：一种数据布局描述语言与数据精化框架，允许程序员声明式指定代数数据类型在内存中的布局。作者将其应用于 Cogent 语言，但方法具有通用性。Dargent 生成直接按目标内存布局操作数据的 C 代码，并保留该 C 代码相对于函数式语义的正确性形式证明。由此，程序员无需实现和验证 marshalling 代码，消除了复制，改善了与周边系统的互操作，并提升整体可信度。
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.
@article{paperbot2091,
title = {Dargent: A Silver Bullet for Verified Data Layout Refinement},
author = {Zilin Chen and Ambroise Lafont and Liam O'Connor and Gabriele Keller and Craig McLaughlin and Vincent Jackson and Christine Rizkallah},
journal = {Proceedings of the ACM on Programming Languages},
volume = {7},
number = {POPL},
year = {2023},
doi = {10.1145/3571240}
}