Recherches
Laboratoire de langages et outils de programmation
Memory Fairness
Comment une exécution infinie peut-elle être limitée dans le contexte de la mémoire faible ? Quand est-ce qu'un programme concurrent se termine avec ce paramètre ?C'est à ce genre de questions que notre projet vise à répondre.
Les propriétés de vivacité, telles que la terminaison, des programmes concurrents de mémoire partagée les plus simples avec cohérence séquentielle nécessitent généralement au moins une hypothèse d'équité concernant le planificateur. Dans les modèles de mémoire faible, les notions standards d'équité des threads sont insuffisantes et une propriété d'équité supplémentaire, memory fairness, est nécessaire. Dans le cadre de ce projet, nous avançons des définitions de l'égalité de la mémoire dans le cadre de modèles de mémoire opérationnels et déclaratifs, tels que SC, x86-TSO, RA et StrongCOH, et explorons leur utilisation pour les vérifications de modèles et de terminaison des programmes concurrents avec une synchronisation à bas niveau.