一句话：提出两阶段无限/有限内存模型，统一 LLVM IR 的整数指针转换、有限空间与 undef，并证明精化以支持优化。
低级语言语义中，整数–指针转换、有限地址空间与 undef 等特性使内存模型难以同时支持程序变换的正确性证明。本文提出“两阶段”内存模型：一个无限内存层配无限整数类型，另一个有限内存层对应真实硬件；两层之间通过显式精化关系连接，并处理内存耗尽行为。作者将该模型嵌入 LLVM IR 语义，得到无限与有限内存两版语言语义，并证明它们在内存耗尽行为上满足精化。每版语义均配有经过验证的可执行参考解释器。该工作使 dead-alloca-elimination 等此前难以或无法证明正确的优化得到语义学依据。
This paper provides a novel approach to reconciling complex low-level memory model features, such as pointerinteger casts, with desired refinements that are needed to justify the correctness of program transformations. The idea is to use a “two-phase” memory model, one with an unbounded memory and corresponding unbounded integer type, and one with a finite memory; the connection between the two levels is made explicit by a 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. The two-phase memory model has been incorporated into an LLVM IR semantics, demonstrating its utility in practice in the context of a low-level language with features like undef and bitcast. This yields infinite and finite memory versions of the language semantics that are proven to be in refinement with respect to out-of-memory behaviors. Each semantics is accompanied by a verified executable reference interpreter. The semantics justify optimizations, such as dead-alloca-elimination, that were previously impossible or difficult to prove correct.
DOI 原文 · arXiv · PDF（开放获取） · DBLP
@article{abs-2404-16143,
title = {A Two-Phase Infinite/Finite Low-Level Memory Model: Reconciling Integer–Pointer Casts, Finite Space, and undef at the LLVM IR Level of Abstraction},
author = {Calvin Beck and Irene Yoon and Hanxi Chen and Yannick Zakowski and Steve Zdancewic},
journal = {Proceedings of the ACM on Programming Languages},
volume = {8},
number = {ICFP},
year = {2024},
doi = {10.1145/3674652}
}