The CompCert Memory Model, Version 2

Xavier Leroy 1, * Andrew Appel 2 Sandrine Blazy 3 Gordon Stewart 2
* Corresponding author
3 CELTIQUE - Software certification with semantic analysis
Inria Rennes – Bretagne Atlantique , IRISA-D4 - LANGAGE ET GÉNIE LOGICIEL
Abstract : A memory model is an important component of the formal semantics of imperative programming languages: it specifies the behavior of operations over memory states, such as reads and writes. The formally verified CompCert C compiler uses a sophisticated memory model that is shared between the semantics of its source language (the CompCert subset of C) and intermediate languages. The algebraic properties of this memory model play an important role in the proofs of semantic preservation for the compiler. The initial design of the CompCert memory model is described in an article by Leroy and Blazy (J. Autom. Reasoning 2008). The present research report describes version 2 of this memory model, improving over the main limitations of version 1. The first improvement is to expose the byte-level, in-memory representation of integers and floats, while preserving desirable opaqueness properties of pointer values. The second improvement is the integration of a fine-grained mechanism of permissions (access rights), which supports more aggressive optimizations over read-only data, and paves the way towards shared-memory, data-race-free concurrency in the style of Appel's Verified Software Toolchain project.
Document type :
Reports
Complete list of metadatas

https://hal.inria.fr/hal-00703441
Contributor : Xavier Leroy <>
Submitted on : Friday, June 1, 2012 - 6:38:18 PM
Last modification on : Thursday, November 15, 2018 - 11:57:40 AM
Long-term archiving on : Friday, November 30, 2012 - 1:10:22 PM

File

RR-7987.pdf
Files produced by the author(s)

Identifiers

  • HAL Id : hal-00703441, version 1

Citation

Xavier Leroy, Andrew Appel, Sandrine Blazy, Gordon Stewart. The CompCert Memory Model, Version 2. [Research Report] RR-7987, INRIA. 2012, pp.26. ⟨hal-00703441⟩

Share

Metrics

Record views

3119

Files downloads

1891