A Two-Phase Infinite/Finite Low-Level Memory Model

TL;DR

This paper introduces a two-phase memory model that bridges infinite and finite memory semantics, enabling better program optimization and correctness proofs for low-level features in LLVM IR.

Contribution

It proposes a novel two-phase memory model with explicit refinement, improving the justification of program transformations involving low-level memory features.

Findings

The model supports optimizations like dead-alloca-elimination.

It provides provably correct refinements to executable interpreters.

The approach clarifies the boundary between idealized semantics and hardware implementation.

Abstract

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.