Authors
Yuting Wang
Ling Zhang
Zhong Shao
Jérémie Koenig
Abstract
Memory models play an important role in verified compilation of
imperative programming languages. A representative one is the
block-based memory model of CompCert, the state-of-the-art verified C
compiler. Despite its success, the abstraction over memory space
provided by CompCert's memory model is still primitive and
inflexible. In essence, it uses a fixed representation for identifying
memory blocks in a global memory space and uses a globally shared
state for distinguishing between used and unused blocks. Therefore,
any reasoning about memory must work uniformly for the global memory;
it is impossible to individually reason about different sub-regions of
memory (i.e., the stack and global definitions). This does not only
incur unnecessarily complexity in compiler verification, but also pose
significant difficulty for supporting verified compilation of open or
concurrent programs that need to work with contextual memory, as
manifested in many previous extensions of CompCert.
To remove the above limitations, we propose an enhancement to the
block-based memory model based on nominal techniques;
we call it the nominal memory model. By adopting the key
concepts of nominal techniques such as atomic names and
supports to model the memory space, we are able to (1)
generalize the representation of memory blocks to any types satisfying
the properties of atomic names and (2) remove the global
constraints for managing memory blocks, enabling flexible memory
structures for open and concurrent programs.
To demonstrate the effectiveness of the nominal memory model, we
develop a series of extensions of CompCert based on it. These
extensions show that the nominal memory model (1) supports a
general framework for verified compilation of C programs, (2)
enables concise and intuitive reasoning of compiler transformations on
partial memory; and (3) enables modular reasoning about programs
working with contextual memory. We also demonstrate that these
extensions require limited changes to the original CompCert, making
the verification techniques based on the nominal memory model easy to
adopt.
Published
In
Proc. 49th
ACM SIGPLAN-SIGACT Symposium on Principles of Programming
Languages (POPL'22), Philadelphia, PA, January 2022.
Published as
Proceedings of the ACM on Programming Languages (PACMPL), Volume 6, Number POPL, Article 25 (January 2022), 31 pages.