Mécanisation du modèle RC11 et de la propriété DRF-SC - Archive ouverte HAL Access content directly
Conference Papers Year :

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

(1)
1

Abstract

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.
Fichier principal
Vignette du fichier
ladeveze_21_mecanisation_du_modele_rc11_et_de_la_propriete_drf_sc.pdf (600.64 Ko) Télécharger le fichier
Origin : Files produced by the author(s)

Dates and versions

hal-03081928 , version 1 (18-12-2020)

Identifiers

  • HAL Id : hal-03081928 , version 1

Cite

Quentin Ladeveze. Mécanisation du modèle RC11 et de la propriété DRF-SC. JFLA 2021 - 32es Journées Francophones des Langages Applicatifs, Apr 2021, Saint Médard d’Excideuil, France. ⟨hal-03081928⟩
57 View
98 Download

Share

Gmail Facebook Twitter LinkedIn More