The FLINT Project

Research

People

Publications

Software

Support

Links

Internal

Verified Compilation of C Programs with a Nominal Memory Model

Last modified: Tue Jan 25 15:12:52 2022 GMT.

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.
  • Conference Paper [PDF]
  • POPL22 Talk Slides [PDF] and [pptx]
  • POPL22 Talk Video[mp4]
  • Artifact [URL]

  • Copyright © 1996-2022 The FLINT Group <flint at cs dot yale dot edu>
    Yale University Department of Computer Science
    Validate this page
    colophon