Book contents
- Frontmatter
- Dedication
- Contents
- Road map
- Acknowledgments
- 1 Introduction
- I Generic separation logic
- II Higher order separation logic
- III Separation logic for CompCert
- IV Operational semantics of CompCert
- V Higher-order semantic models
- VI Semantic model and soundness of Verifiable C
- 40 Separation algebra for CompCert
- 41 Share models
- 42 Juicy memories
- 43 Modeling the Hoare judgment
- 44 Semantic model of CSL
- 45 Modular structure of the development
- VII Applications
- Bibliography
- Index
40 - Separation algebra for CompCert
from VI - Semantic model and soundness of Verifiable C
Published online by Cambridge University Press: 05 August 2014
- Frontmatter
- Dedication
- Contents
- Road map
- Acknowledgments
- 1 Introduction
- I Generic separation logic
- II Higher order separation logic
- III Separation logic for CompCert
- IV Operational semantics of CompCert
- V Higher-order semantic models
- VI Semantic model and soundness of Verifiable C
- 40 Separation algebra for CompCert
- 41 Share models
- 42 Juicy memories
- 43 Modeling the Hoare judgment
- 44 Semantic model of CSL
- 45 Modular structure of the development
- VII Applications
- Bibliography
- Index
Summary
In building a Hoare logic over a language specified by an operational semantics, we can view the assertions of the Hoare logic as predicates on the states of the operational semantics. But we do this in two layers: first, relate the operational states into semantic worlds; then, apply the Hoare assertions to the worlds. We do this for several reasons: The operational states may contain information that we want to hide from the Hoare assertions, particularly control information (program counter, control stack) that is not supposed to be visible to a Hoare-logic assertion. The semantic worlds may contain information that we want to hide from the operational semantics, such as step-indexes, ghost variables, predicates in the heap (for modeling first-class functions or mutex locks), and permission-shares. For convenience in reasoning, we require Liebniz equality on worlds—equivalent worlds should be equal—but operational states do not generally satisfy Liebniz equality. In our two different toy examples (Chapter 9 and Chapter 39) we have separated operational states from semantic worlds, and we do so for the VST Separation Logic for CompCert C light.
Some components of the world are subject to separating conjunction (*), and others are not. Generally, to “heap” or “memory” or any other addressable component of the world, we apply separation in order to reason about antialiasing. Nonaddressable local variables (and the addresses of addressable local variables) do not require separation, because there is no aliasing to worry about.
- Type
- Chapter
- Information
- Program Logics for Certified Compilers , pp. 363 - 373Publisher: Cambridge University PressPrint publication year: 2014