Recherches
Laboratoire de langages et outils de programmation
IMM: Compilation Correctness for Relaxed Memory Models
Le framework IMM simplifie la preuve de l'exactitude de la compilation à partir de modèles de mémoire de langage de programmation, tels que Promising et Weakestmo, vers des modèles de mémoire matérielle, tels que x86, Power, Arm et RISC-V. Le framework est mécanisé dans Coq.
Nous développons un modèle intermédiaire de mémoire faible, IMM, afin de modulariser les preuves de l'exactitude de la compilation à partir de langages de programmation concurrents avec une sémantique de cohérence de la mémoire faible sur les architectures standard à plusieurs cœurs, telles que POWER et ARM. Nous utilisons IMM pour prouver l'exactitude de la compilation à partir de nouveaux modèles de mémoire de langage de programmation (principalement ceux qui visent à résoudre le problème de création ex-nihilo) à des modèles de mémoire matériels, comme POWER, ARMv7, ARMv8, RISC-V, and x86-TSO. Nos résultats sont mécanisés dans Coq et, à notre connaissance, il s'agit des premiers résultats d'exactitude de la compilation vérifiés par machine pour les modèles qui sont plus faibles que x86-TSO.
