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...

Descripción completa

Detalles Bibliográficos
Autor principal: Krebbers, Robbert
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