Cargando…
A Formal C Memory Model for Separation Logic
The core of a formal semantics of an imperative programming language is a memory model that describes the behavior of operations on the memory. Defining a memory model that matches the description of C in the C11 standard is challenging because C allows both high-level (by means of typed expressions...
Autor principal: | |
---|---|
Formato: | Online Artículo Texto |
Lenguaje: | English |
Publicado: |
Springer Netherlands
2016
|
Materias: | |
Acceso en línea: | https://www.ncbi.nlm.nih.gov/pmc/articles/PMC6109957/ https://www.ncbi.nlm.nih.gov/pubmed/30174361 http://dx.doi.org/10.1007/s10817-016-9369-1 |
_version_ | 1783350398283677696 |
---|---|
author | Krebbers, Robbert |
author_facet | Krebbers, Robbert |
author_sort | Krebbers, Robbert |
collection | PubMed |
description | The core of a formal semantics of an imperative programming language is a memory model that describes the behavior of operations on the memory. Defining a memory model that matches the description of C in the C11 standard is challenging because C allows both high-level (by means of typed expressions) and low-level (by means of bit manipulation) memory accesses. The C11 standard has restricted the interaction between these two levels to make more effective compiler optimizations possible, at the expense of making the memory model complicated. We describe a formal memory model of the (non-concurrent part of the) C11 standard that incorporates these restrictions, and at the same time describes low-level memory operations. This formal memory model includes a rich permission model to make it usable in separation logic and supports reasoning about program transformations. The memory model and essential properties of it have been fully formalized using the Coq proof assistant. |
format | Online Article Text |
id | pubmed-6109957 |
institution | National Center for Biotechnology Information |
language | English |
publishDate | 2016 |
publisher | Springer Netherlands |
record_format | MEDLINE/PubMed |
spelling | pubmed-61099572018-08-31 A Formal C Memory Model for Separation Logic Krebbers, Robbert J Autom Reason Article The core of a formal semantics of an imperative programming language is a memory model that describes the behavior of operations on the memory. Defining a memory model that matches the description of C in the C11 standard is challenging because C allows both high-level (by means of typed expressions) and low-level (by means of bit manipulation) memory accesses. The C11 standard has restricted the interaction between these two levels to make more effective compiler optimizations possible, at the expense of making the memory model complicated. We describe a formal memory model of the (non-concurrent part of the) C11 standard that incorporates these restrictions, and at the same time describes low-level memory operations. This formal memory model includes a rich permission model to make it usable in separation logic and supports reasoning about program transformations. The memory model and essential properties of it have been fully formalized using the Coq proof assistant. Springer Netherlands 2016-05-10 2016 /pmc/articles/PMC6109957/ /pubmed/30174361 http://dx.doi.org/10.1007/s10817-016-9369-1 Text en © The Author(s) 2016 Open AccessThis article is distributed under the terms of the Creative Commons Attribution 4.0 International License (http://creativecommons.org/licenses/by/4.0/), which permits unrestricted use, distribution, and reproduction in any medium, provided you give appropriate credit to the original author(s) and the source, provide a link to the Creative Commons license, and indicate if changes were made. |
spellingShingle | Article Krebbers, Robbert A Formal C Memory Model for Separation Logic |
title | A Formal C Memory Model for Separation Logic |
title_full | A Formal C Memory Model for Separation Logic |
title_fullStr | A Formal C Memory Model for Separation Logic |
title_full_unstemmed | A Formal C Memory Model for Separation Logic |
title_short | A Formal C Memory Model for Separation Logic |
title_sort | formal c memory model for separation logic |
topic | Article |
url | https://www.ncbi.nlm.nih.gov/pmc/articles/PMC6109957/ https://www.ncbi.nlm.nih.gov/pubmed/30174361 http://dx.doi.org/10.1007/s10817-016-9369-1 |
work_keys_str_mv | AT krebbersrobbert aformalcmemorymodelforseparationlogic AT krebbersrobbert formalcmemorymodelforseparationlogic |