The CompCert memory model
Andrew W. Appel · Cambridge University Press eBooks · 2014
The imperative programming paradigm views programs as sequences of commands that update a memory state . A memory model specifies memory states and operations such as reads and writes. Such a memory model is a prerequisite to giving formal semantics to imperative programming languages, verifying properties of programs, and proving the correctness of program transformations. For high-level, type-safe languages such as ML or the sequential fragment of Java, the memory model is simple and amounts to a finite map from abstract memory locations to the values they contain. At the other end of the complexity spectrum, we find memory models for shared-memory concurrent programs with data races and relaxed (non sequentially consistent) memory, where much effort is needed to capture the relaxations ( e.g . reorderings of reads and writes) that are allowed and those that are guaranteed never to happen [1]. For CompCert we focus on memory models for the C language and for compiler intermediate languages, in the sequential case and with extensions to data race-free concurrency. C and our intermediate languages feature both low-level aspects such as pointers, pointer arithmetic, and nested objects, and high-level aspects such as separation and freshness guarantees. For instance, pointer arithmetic can result in aliasing or partial overlap between the memory areas referenced by two pointers; yet, it is guaranteed that the memory areas corresponding to two distinct variables or two successive calls to malloc are disjoint.