Thaïs Baudon presents a compilation technique for custom, low-level memory representations of algebraic data types using bit-stealing.
Bit-Stealing Made Legal: Compilation for Custom Memory Representations of Algebraic Data Types (Video, ICFP 2023)
Thaïs Baudon, Gabriel Radanne, and Laure Gonnord
(University of Lyon, France / ENS Lyon, France / UCBL, France / CNRS, France / Inria, France / LIP, France; Inria, France / ENS Lyon, France / UCBL, France / CNRS, France / LIP, France; University Grenoble Alpes, France / Grenoble INP, France / LCIS, France / LIP, France)
Abstract: Initially present only in functional languages such as OCaml and Haskell, Algebraic Data Types (ADTs) have now become pervasive in mainstream languages, providing nice data abstractions and an elegant way to express functions through pattern matching. Unfortunately, ADTs remain seldom used in low-level programming. One reason is that their increased convenience comes at the cost of abstracting away the exact memory layout of values. Even Rust, which tries to optimize data layout, severely limits control over memory representation. In this article, we present a new approach to specify the data layout of rich data types based on a dual view: a source type, providing a high-level description available in the rest of the code, along with a memory type, providing full control over the memory layout. This dual view allows for better reasoning about memory layout, both for correctness, with dedicated validity criteria linking the two views, and for optimizations that manipulate the memory view. We then provide algorithms to compile constructors and destructors, including pattern matching, to their low-level memory representation. We prove our compilation algorithms correct, implement them in a tool called ribbit that compiles to LLVM IR, and show some early experimental results.
Article:
doi.org/10.1145/3607858
Supplementary archive:
doi.org/10.5281/zenodo.8099902 (Badges: Artifacts Available, Artifacts Evaluated — Reusable)
Supplementary web page:
gitlab.inria.fr/ribbit/ribbit
ORCID:
orcid.org/0000-0002-9368-651X,
orcid.org/0000-0002-2107-7678,
orcid.org/0000-0002-8013-1611
Video Tags: Algebraic Data Types, Pattern Matching, Compilation, Data Layouts, icfp23main-p134-p, doi:10.1145/3607858, doi:10.5281/zenodo.8099902, orcid:0000-0002-9368-651X, orcid:0000-0002-2107-7678, orcid:0000-0002-8013-1611, Artifacts Available, Artifacts Evaluated — Reusable
Presentation at the ICFP 2023 conference, September 4–9, 2023,
icfp23.sigplan.org/
Sponsored by ACM SIGPLAN,
sigplan.org/