Le point-virgule qui fuit
Author
Venue
Actes de l'ACM sur les langages de programmation 2021
Abstract
La logique et la sémantique des programmes présentent une vision idyllique de la composition séquentielle : lors de l'exécution de (S1 ; S2), on exécute d'abord S1, puis S2. Cependant, pour améliorer les performances, les processeurs exécutent les instructions dans un ordre aléatoire, et les compilateurs réorganisent les programmes de manière encore plus radicale. De par leur conception, les systèmes monothread ne peuvent pas détecter ces réorganisations ; en revanche, les systèmes multithread le peuvent, ce qui rend la situation nettement moins idyllique. Une tentative formelle de comprendre le désordre qui en résulte est connue sous le nom de « modèle de mémoire assoupli ». Les modèles antérieurs soit ne traitent pas directement la composition séquentielle, soit restreignent excessivement les processeurs et les compilateurs, soit autorisent des comportements absurdes et fantaisistes qui sont inobservables dans la pratique. Afin de prendre en charge la composition séquentielle tout en ciblant le matériel moderne, nous enrichissons l'approche standard basée sur les événements avec des préconditions et des familles de transformateurs de prédicats. Lors du calcul de la signification de (S1;S2), le transformateur de prédicats appliqué à la condition préalable d’un événement e issu de S2 est choisi en fonction de l’ensemble des événements de S1 dont e dépend. Nous appliquons cette approche à deux modèles de mémoire existants.
