Reversibility for concurrent memory models
Pietro Lami · AMS Dottorato Institutional Doctoral Theses Repository (University of Bologna) · 2025
La notion de réversibilité a été bien étudiée pour des langages et systèmes concurrents à base d'échanges de messages, mais pas du tout dans le cas de langages concurrents à base de mémoire partagée. Nous explorons dans cette thèse une réversibilité causalement cohérente dans différents modèles de mémoire partagée, notamment des modèles mémoire faibles tels que l'on peut les trouver dans des langages concurrents récents comme Java. Nous procédons en deux étapes. Nous développons d'abord un méta-modèle pour la définition de langages concurrents à base de mémoire partagée sous la forme de produits de synchronisation de systèmes de transitions étiquetés comprenant trois composants principaux: des fils d'exécution, une mémoire et un ordonnanceur. Nous montrons comment définir comme instances de ce méta-modèle plusieurs modèles mémoire connus, notamment le classique modèle de mémoire séquentiellement cohérente, un modèle mémoire avec un buffer d'écriture, et une mémoire transactionnelle. Nous développons ensuite une théorie compositionnelle pour rendre réversible des produits de systèmes de transaitions étiquetés tout en en garantissant la cohérence causale. Nous appliquons cette théorie au modèle de mémoire séquentiellement cohérente en montron sur cet exemple que notre approche compositionnelle permet d'éviter d'introduire des dépendances causales indûes par rapport à une approche consistant à rendre réversible directement une sémantique opérationnelle monolithique d'un langage avec mémoire séquentiellement cohérente.