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
41 - Share models
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
An important application of separation algebras is to model Hoare logics of programming languages with mutable memory. We generate an appropriate separation logic by choosing the correct semantic model, that is, the correct separation algebra. A natural choice is to simply take the program heaps as the elements of the separation algebra together with some appropriate join relation.
In most of the early work in this direction, heaps were modeled as partial functions from addresses to values. In those models, two heaps join iff their domains are disjoint, the result being the union of the two heaps. However, this simple model is too restrictive, especially when one considers concurrency. It rules out useful and interesting protocols where two or more threads agree to share read permission to an area of memory.
There are a number of different ways to do the necessary permission accounting. Bornat et al. [27] present two different methods; one based on fractional permissions, and another based on token counting. Parkinson, in chapter 5 of his thesis [74], presents a more sophisticated system capable of handling both methods. However, this model has some drawbacks, which we shall address below.
Fractional permissions are used to handle the sorts of accounting situations that arise from concurrent divide-and-conquer algorithms. In such algorithms, a worker thread has read-only permission to the dataset and it needs to divide this permission among various child threads.
- Type
- Chapter
- Information
- Program Logics for Certified Compilers , pp. 374 - 384Publisher: Cambridge University PressPrint publication year: 2014