Recently, the research team led by Wang Yuting, tenure-track associate professor of John Hopcroft Center for Computer Science at School of Electronic Information and Electrical Engineering, Shanghai Jiao Tong University, has made important progress in verified compilation of C-programs. The research findings "Verified Compilation of C Programs with a Nominal Memory Model" has been accepted by ACM SIGPLAN Symposium on Principles of Programming Languages (POPL 2022). The project was jointly completed by SJTU and Yale University, with SJTU as the first affiliation and Wang Yuting as the first author. In this research, the concepts of atomic names and supports in Nominal Techniques are innovatively introduced into the traditional block-based memory model, and a new memory model called Nominal Memory Model is proposed, which is successfully applied to the verified compilation of C-programs.
POPL is an international conference with the longest history and of the highest level in the field of programming languages, and it is also a Class-A conference recommended by China Computer Federation (CCF). POPL accepts only 1-3 papers with the participation of Chinese research institutions every year, and the papers with Chinese institutions as the first affiliation are even rarer. Only 65 papers were accepted worldwide by POPL 2022.
The team implemented the nominal memory model in the state-of-the-art verified C compiler CompCert, and based on this completed the proof of all the compilation processes in CompCert, and obtained the first CompCert extension that supports abstract memory space, namely NominalCompCert. Building on this, several CompCert extensions were further developed, which respectively simplified the verification difficulty of key compilation steps and provided better support for concurrent program semantics and modular verification (as shown in the figure). These works have laid a solid foundation for flexible and extensible verified compilation of modular concurrent programs, which are expected to improve a wider range of work based on traditional memory model in the field of program verification.
Paper Link:
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 \emph{nominal techniques}; we call it the \emph{nominal memory model}. By adopting the key concepts of nominal techniques such as \emph{atomic names} and \emph{supports} to model the memory space, we are able to \emph{1)} generalize the representation of memory blocks to any types satisfying the properties of atomic names and \emph{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 \emph{1)} supports a general framework for verified compilation of C programs, \emph{2)} enables concise and intuitive reasoning of compiler transformations on partial memory; and \emph{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.
Source: School of Electronic Information and Electrical Engineering, SJTU
Translated by Zhou Rong
Proofread by Xiao Yangning