The CompCert Memory Model, Version 2

Xavier Leroy 1, * Andrew Appel 2 Sandrine Blazy 3 Gordon Stewart 2
* Auteur correspondant
3 CELTIQUE - Software certification with semantic analysis
Inria Rennes – Bretagne Atlantique , IRISA-D4 - LANGAGE ET GÉNIE LOGICIEL
Résumé : Le modèle mémoire est un composant important de la sémantique formelle d'un langage impératif de programmation: il spécifie le comportement des opérations sur les états mémoire, tels que les lectures et les écritures. Le compilateur formellement vérifié CompCert C utilise un modèle mémoire élaboré, qu'il partage entre les sémantiques de son langage source (le sous-ensemble CompCert de C) et de ses langages intermédiaires. Les propriétés algébriques de ce modèle mémoire jouent un rôle important dans les preuves de préservation sémantique du compilateur. La première version du modèle mémoire CompCert est décrit dans un article de Leroy et Blazy (J. Autom. Reasoning 2008). Ce rapport de recherche décrit la version 2 de ce modèle mémoire, qui résout les principales limitations de la version 1. Première amélioration: il expose la représentation en mémoire, au niveau de l'octet, des entiers et des flottants, tout en préservant les propriétés utiles d'opacité des pointeurs. Seconde amélioration: il intègre un mécanisme de permissions (droits d'accès) à grain fin, qui autorise le compilateur à effectuer des optimisations plus agressives sur les données en lecture seule, et constitue un premier pas vers le parallélisme à mémoire partagée bien synchronisé, dans le style du projet Verified Software Toolchain d'Appel.
Type de document :
Rapport
[Research Report] RR-7987, INRIA. 2012, pp.26
Liste complète des métadonnées

https://hal.inria.fr/hal-00703441
Contributeur : Xavier Leroy <>
Soumis le : vendredi 1 juin 2012 - 18:38:18
Dernière modification le : jeudi 9 février 2017 - 16:05:41
Document(s) archivé(s) le : vendredi 30 novembre 2012 - 13:10:22

Fichier

RR-7987.pdf
Fichiers produits par l'(les) auteur(s)

Identifiants

  • HAL Id : hal-00703441, version 1

Citation

Xavier Leroy, Andrew Appel, Sandrine Blazy, Gordon Stewart. The CompCert Memory Model, Version 2. [Research Report] RR-7987, INRIA. 2012, pp.26. <hal-00703441>

Partager

Métriques

Consultations de
la notice

1788

Téléchargements du document

745