Résumé
Depuis le quatrième cours, notre vision d'une exécution parallèle d'un programme est celle d'un entrelacement des actions élémentaires des processus constituant le programme. Ce modèle du parallélisme est appelé séquentiellement cohérent (SC). Un avantage de ce modèle est qu'il donne un sens précis aux courses critiques qui peuvent se produire pendant l'exécution, comme on en trouve dans certains algorithmes parallèles.
Malheureusement, le modèle SC est une fiction : les processeurs et les langages contemporains ne garantissent pas la cohérence séquentielle, et fournissent à l'utilisateur des modèles mémoires faiblement cohérents, avec davantage de comportements qu'explicables par des entrelacements. Ces relaxations de la cohérence séquentielle proviennent autant de dispositifs matériels (tampons d'écriture, exécution dans le désordre, etc.) que d'optimisations à la compilation (réordonnancements et factorisations de code). Divers mécanismes matériels (barrières) et linguistiques permettent de contrôler ces relaxations.
Comment vérifier les programmes parallèles dans ces conditions ? Pour une large classe de programmes, la logique de séparation concurrente « standard » suffit : les programmes vérifiables dans cette logique n'ayant pas de courses critiques, ils s'exécutent à l'identique dans le modèle SC et dans tout modèle relâché qui présente la garantie DRF (Data Race Freedom), ce qui est le cas de tous les modèles matériels et logiciels connus. Nous avons esquissé une démonstration dans le cas particulier du modèle TSO.
L'étape suivante est de raisonner sur les accès atomiques faiblement cohérents, comme ceux fournis par les standards C/C++ 2011. La logique FSL de Vafeiadis et Narayan ajoute à la logique de séparation concurrente de nouvelles assertions et des règles de déduction pour les accès atomiques de type release-acquire, utilisés pour le passage de messages. L'extension aux accès atomiques de type relaxé se heurte au problème des valeurs ex nihilo (values out of thin air) du modèle C/C++ 2011, problème que résout la sémantique « prometteuse » proposée par Kang et al. Cela débouche sur la logique SLR de Svensden et al., qui étend FSL avec un traitement des accès atomiques relaxés.
