This program is tentative and subject to change.
This paper provides a novel approach to reconciling complex low-level memory model features, such as pointer–integer casts, with desired refinements that are needed to justify the correctness of program transformations. The idea is to use a ``two-phased'' memory model, one with and unbounded memory and corresponding unbounded integer type, and one with a finite memory; the connection between the two levels is made explicit by our notion of refinement that handles out-of-memory behaviors. This approach allows for more optimizations to be performed and establishes a clear boundary between the idealized semantics of a program and the implementation of that program on finite hardware.
To demonstrate the utility of this idea in practice, we instantiate the two-phase memory model in the context of Zakowski et al.’s VIR semantics, yielding infinite- and finite-memory models of LLVM IR, including low-level features like undef
and bitcast
. Both the infinite and finite models, which act as specifications, can provably be refined to executable reference interpreters. The semantics justify optimizations, such as dead-alloca-elimination, that were previously impossible or difficult to prove correct.
This program is tentative and subject to change.
Thu 5 SepDisplayed time zone: Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change
13:30 - 15:00 | Memory Models / Memory Management / Low-Level LanguagesICFP Papers and Events | ||
13:30 18mTalk | 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 18mTalk | A Two-Phase Infinite/Finite Low-Level Memory Model ICFP Papers and Events Calvin Beck University of Pennsylvania, Steve Zdancewic University of Pennsylvania, Irene Yoon INRIA Paris, Hanxi Chen University of Pennsylvania, Yannick Zakowski Inria | ||
14:06 18mTalk | Double-Ended Bit-Stealing for Algebraic Data Types ICFP Papers and Events Martin Elsman University of Copenhagen, Denmark Link to publication DOI | ||
14:24 18mTalk | Beyond Trees: Calculating Graph-Based Compilers ICFP Papers and Events Pre-print | ||
14:42 18mTalk | Sound Borrow-Checking for Rust via Symbolic Semantics ICFP Papers and Events |