Skip to Main content Skip to Navigation
Conference papers

Mécanisation du modèle RC11 et de la propriété DRF-SC

Résumé : Un modèle mémoire décrit les comportements possibles d'un programme concurrent réalisant des accès à la mémoire partagée. Dans le modèle mémoire SC, ces comportements sont ceux que l'on pourrait observer si l'on exécutait séquentiellement un entrelacement des instructions des différents $threads$ du programme. Ce modèle simple est généralement celui qui est attendu par le programmeur. Cependant, il exclut des comportements, dits relâchés, induits par les processeurs et les compilateurs lorsque ces derniers réalisent des optimisations. Pour que les utilisateurs puissent bénéficier de la simplicité de SC, tout en permettant de bonnes performances, on souhaite que les modèles mémoire de ces processeurs et de ces langages de programmation vérifient la propriété DRF-SC. Cette propriété garantit que si les exécutions conformes à SC d'un programme ne contiennent aucune race, le programme ne présentera aucune exécution non conforme à SC. Autrement dit, en respectant une condition simple, l'utilisateur peut ignorer le modèle mémoire de son langage et de son architecture. Le modèle RC11 est un modèle mémoire formel des programmes C/C++ respectant le standard C11. Les auteurs de ce modèle accompagnent ce dernier d'une preuve qu'il respecte la propriété DRF-SC. Nous présentons la mécanisation dans l'assistant de preuves Coq de ce modèle mémoire et de cette preuve. De plus, nous explorons les limites d'application de cette propriété dans le cadre des programmes C11. Enfin, nous discutons des façons dont cette preuve pourrait être adaptée à d'autres modèles et modifiée pour s'appliquer à une classe moins restreinte de programmes.
Complete list of metadatas

https://hal.inria.fr/hal-03081928
Contributor : Quentin Ladeveze <>
Submitted on : Friday, December 18, 2020 - 1:34:22 PM
Last modification on : Thursday, January 7, 2021 - 3:37:13 AM

File

ladeveze_21_mecanisation_du_mo...
Files produced by the author(s)

Identifiers

  • HAL Id : hal-03081928, version 1

Collections

Citation

Quentin Ladeveze. Mécanisation du modèle RC11 et de la propriété DRF-SC. JFLA 2021 -Trente-deuxièmes Journées Francophones des Langages Applicatifs, Feb 2021, Saint Médard d’Excideuil, France. ⟨hal-03081928⟩

Share

Metrics

Record views

32

Files downloads

84