Vous pouvez vous abonner à nos annonces de séminaires: http://cambium.inria.fr/seminar.html Nos séminaires sont accessibles en ligne en direct: https://webconf.math.cnrs.fr/b/fra-ryy-fjn S É M I N A I R E ______ __ _ / ____/___ _____ ___ / /_ (_)_ ______ ___ / / / __ `/ __ `__ \/ __ \/ / / / / __ `__ \ / /___/ /_/ / / / / / / /_/ / / /_/ / / / / / / \____/\__,_/_/ /_/ /_/_.___/_/\__,_/_/ /_/ /_/ I N R I A - Paris 2 rue Simone Iff (ou: 41 rue du Charolais) en ligne Lundi 29 mars, 10h30 ---------------- Quentin Ladeveze ---------------- Inria Paris =================================================== Preuve de la propriété DRF-SC du modèle RC11 en Coq =================================================== Un modèle mémoire décrit les comportements possibles d'un programme concurrent réalisant des accès à la mémoire partagée. Le modèle RC11 par exemple est un modèle mémoire formel qui définit le comportement des programmes C/C++11 concurrents, et en particulier des primitives de synchronisation que ce standard propose aux utilisateurs. Ce modèle est précis mais possiblement trop complexe pour le programmeur. Le modèle SC est au contraire proche de l'intuition du programmeur sur le comportement d'un programme concurrent. Dans ce modèle, le comportement d'un programme correspond à un entrelacement des instructions des différents threads exécuté séquentiellement. Ce modèle est simple, mais trop restrictif en termes de performances. Pour offrir les possibilités d'optimisations de RC11 et la simplicité de SC, le modèle RC11 vérifie la propriété DRF-SC. Cette propriété stipule que dans n'importe quel programme, si aucune exécution possible dans SC ne comporte de data-race, alors toutes les exécutions possibles dans le modèles RC11 auront un comportement conforme à celui d'une exécution SC. Nous présentons dans cet exposé cette preuve, et sa formalisation dans l'assistant de preuves Coq. Nous discuterons également les possibilités d'adapter cette preuve formelle à d'autres modèles mémoire et la pertinence du critère de l'absence de data-race pour faire coïncider les comportements dans le modèle mémoire d'un langage de programmation avec ceux possibles dans SC.