Mécanisation du modèle RC11 et de la propriété DRF-SC - Inria - Institut national de recherche en sciences et technologies du numérique Accéder directement au contenu
Communication Dans Un Congrès Année : 2021

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.
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
Origine : Fichiers produits par l'(les) auteur(s)

Dates et versions

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

Identifiants

  • HAL Id : hal-03081928 , version 1

Citer

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⟩
72 Consultations
106 Téléchargements

Partager

Gmail Facebook X LinkedIn More