A Two-Phase Infinite/Finite Low-Level Memory Model
arxiv(2024)
摘要
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.
更多查看译文
AI 理解论文
溯源树
样例
生成溯源树,研究论文发展脉络
Chat Paper
正在生成论文摘要