ICFP 2024
Mon 2 - Sat 7 September 2024 Milan, Italy

The Rust programming language continues to rise in popularity, and as such, warrants the close attention of the programming languages community. In this work, we present a new foundational contribution towards the theoretical understanding of Rust’s semantics. We prove that LLBC, a high-level, borrow-centric model previously proposed for Rust’s semantics and execution, is sound with regards to a low-level pointer-based language \emph{à la} CompCert. Specifically, we prove the following: that LLBC is a correct view over a traditional model of execution; that LLBC’s symbolic semantics are a correct abstraction of LLBC programs; and that LLBC’s symbolic semantics act as a borrow-checker for LLBC, i.e. that symbolically-checked LLBC programs do not get stuck when executed on a heap-and-addresses model of execution.

To prove these results, we introduce a new proof style that considerably simplifies our proofs of simulation, which relies on a notion of hybrid states. Equipped with this reasoning framework, we show that a new addition to LLBC’s symbolic semantics, namely a join operation, preserves the abstraction and borrow-checking properties. This in turn allows us to add support for loops to the Aeneas framework; we show, using a series of examples and case studies, that this unlocks new expressive power for Aeneas.

Thu 5 Sep

Displayed time zone: Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change

13:30 - 15:00
Memory Models / Memory Management / Low-Level LanguagesICFP Papers and Events at Green 1-2-3
Chair(s): Stefan Monnier Université de Montréal
13:30
18m
Talk
Oxidizing OCaml with Modal Memory Management
ICFP Papers and Events
Anton Lorenzen University of Edinburgh, Leo White Jane Street, Stephen Dolan Jane Street, Richard A. Eisenberg Jane Street, Sam Lindley University of Edinburgh
DOI Pre-print
13:48
18m
Talk
A Two-Phase Infinite/Finite Low-Level Memory Model: Reconciling Integer–Pointer Casts, Finite Space, and undef at the LLVM IR Level of Abstraction
ICFP Papers and Events
Calvin Beck University of Pennsylvania, Irene Yoon Inria, Hanxi Chen University of Pennsylvania, Yannick Zakowski Inria, Steve Zdancewic University of Pennsylvania
DOI
14:06
18m
Talk
Double-Ended Bit-Stealing for Algebraic Data Types
ICFP Papers and Events
Martin Elsman University of Copenhagen
Link to publication DOI
14:24
18m
Talk
Beyond Trees: Calculating Graph-Based Compilers (Functional Pearl)Functional Pearl
ICFP Papers and Events
Patrick Bahr IT University of Copenhagen, Graham Hutton University of Nottingham
DOI Pre-print
14:42
18m
Talk
Sound Borrow-Checking for Rust via Symbolic Semantics
ICFP Papers and Events
Son Ho Inria, Aymeric Fromherz Inria, Jonathan Protzenko Microsoft Azure Research
DOI