Soutenance mémoire
Les problématiques liées à la sémantique des programmes concurrents sur des architectures parallèles à mémoire partagée constituent un problème ancien. En 1979, Leslie Lamport propose que ces architectures se comportent de manière séquentiellement cohérente (sequential consistency, SC) : “le résultat de toute exécution est le même que si les opérations de tous les processus étaient exécutées dans un ordre séquentiel quelconque, tel que les opérations de chaque processus apparaissent dans cette séquence dans l’ordre spécifié par leur programme” [102].
Si cette notion de cohérence séquentielle paraît naturelle et permet de raisonner aisément sur des programmes concurrents, il s’agit toutefois d’une notion trop forte, qui limite fortement les possibilités d’optimisation et les performances potentielles des programmes concurrents. Ainsi la recherche va plutôt s’orienter vers des modèles dans lesquels l’ordre des instructions ne suit pas un ordre séquentiel – on parle alors de modèle mémoire faible, ou relâché. En 1986, Dubois et al. s’intéressent aux multiprocesseurs ayant recours à des tampons de lecture et d’écriture afin de limiter les latences dues aux accès mémoires, et proposent le modèle de cohérence faible (weak ordering) [71]. En 1990, Adve et Hill [16] introduisent un modèle de synchronisation sans situation de compétition (datarace free model, DRF). Ce modèle logiciel garantit à tout programme qui le respecte un comportement en apparence séquentiellement cohérent, même si l’architecture matérielle sous-jacente expose un modèle de cohérence faible. Par la suite, de nombreux modèles verront le jour (cohérence PRAM (PRAM consistency) [107], cohérence cache (cache consistency) [82], cohérence processeur (processor consistency) [82, 18], cohérence lente (slow consistency) [92], cohérence au relâchement (release consistency) [78], cohérence causale (causal consistency) [17], …), et plusieurs architectures matérielles implémenteront de tels modèles au niveau du processeur.
Etat de l’art
Lorsque l’on souhaite s’assurer qu’un programme s’exécutant sur un modèle mémoire faible soit correct, on peut avoir recours à différentes approches. La première consiste à s’assurer que tout programme se comporte comme s’il était exécuté sur un modèle SC (pour une certaine notion de comportement). La seconde consiste à vérifier que le programme, exécuté sur un modèle mémoire faible donné, respecte les propriétés de sûreté que l’on attend de ce programme, même s’il montre à l’exécution plus de comportements que sur un modèle SC. En général, les outils permettant de vérifier ces propriétés permettent également d’ajouter des primitives de synchronisation afin de s’assurer que la propriété soit respectée.
La quasi-totalité de ces outils analysent des programmes pour un nombre fixe (et généralement petit) de processus. Une exception notable est l’outil Dual-TSO, qui permet la vérification de propriétés de sûreté pour une certaine forme de programmes paramétrés.
Restriction aux comportements SC
Une bonne façon de s’assurer qu’un programme s’exécutant sur un modèle mémoire faible soit correct consiste à restreindre ses comportements à ceux effectivement possibles sur un modèle SC. Cette approche est en général plus simple que de vérifier des propriétés de sûreté d’un programme s’exécutant directement sur un modèle mémoire faible. Grâce à cette garantie, on peut alors utiliser tout l’éventail des techniques de vérification utilisables en SC. Il existe différentes façons de caractériser les comportements d’un programme. Certaines sont basées sur l’utilisation de traces d’exécution, d’autres sur des états concrets. De même, il existe différentes façons de vérifier et d’imposer qu’un programme ne présente que des comportements SC. L’approche générale consiste à détecter les comportements potentiellement non réalisables en SC et à ajouter judicieusement des primitives de synchronisation (barrières mémoires, instructions de lecture modification-écriture atomiques) afin d’interdire ces comportements. Toutefois, il est important de ne pas utiliser trop de ces primitives, au risque d’impacter négativement la performance des programmes. La plus simple des approches consiste simplement à s’assurer que le programme ne comporte aucune situation de compétition ou data race. Cette approche est en général simple à mettre en œuvre mais génère un nombre important de synchronisations. Partant du constat que certaines situations de compétition sont bénignes, une approche un peu moins stricte consiste à n’interdire que les situations de compétition dites “triangulaires” [115], c’est-à-dire celles dans lesquelles la lecture est précédée d’une écriture, sans qu’aucune primitive de synchronisation ne les sépare. Là aussi, l’approche est relativement simple à mettre en œuvre, et génère moins de primitives de synchronisation que l’approche précédente. Enfin, d’autres approches plus précises étudient plus finement les comportements des programmes de façon à interdire spécifiquement certaines traces d’exécution non-SC (on parle alors de stabilité, ou robustesse, mais également de persistence). Beaucoup de ces travaux reposent sur l’utilisation des notions de trace, de cycle critique, et d’analyse de délais, telles que définies par Shasha et Snir dans [127].
Pensieve Java Compiler [73, 128] (introuvable) est un compilateur expérimental pour le langage Java, conçu pour analyser l’effet des modèles mémoires faibles (i.e. x86 et Power). Il implémente l’algorithme décrit dans [103], basé sur l’analyse de délais et de cycles critiques de Shasha et Snir. Différentes stratégies d’insertion de barrières mémoires sont mises en œuvre, comparées et évaluées. La connaissance des garanties offertes par le modèle sous-jacent est utilisée pour réduire le nombre d’instructions de synchronisation utilisées.
Checkfence [50] (http://checkfence.sourceforge.net) analyse des programmes écrits en C (CIL) et s’exécutant sur un modèle mémoire ad-hoc appelé Relaxed [49], qui capture l’essentiel des modèles TSO, PSO, RMO et Alpha. Il encode le programme C en un problème SAT, qu’il décharge sur un solveur SAT, qui construit un contre-exemple s’il existe une exécution qui diffère de SC. Dans ce cas, des barrières mémoires sont ajoutées afin de rendre cette exécution irréalisable.
Sober [51] (introuvable) analyse des programmes en C# et s’exécutant sur le modèle TSO. Il utilise un algorithme de moniteur pour détecter des exécutions dites “limites”, c’est-à-dire des exécutions SC pouvant être prolongées en une exécution non-SC en ajoutant une seule instruction à la séquence. Cet algorithme s’appuie sur le model checker CHESS [113]. L’outil n’ajoute toutefois pas de primitives de synchronisation pour restaurer un comportement SC.
Offence [24] (http://offence.inria.fr) permet d’analyser des programmes écrits en langage d’assemblage x86 et Power et s’exécutant sur leurs modèles respectifs. Il est également basé sur les travaux de Shasha et Snir, adaptés aux modèles modernes, et permet l’ajout de barrières mémoires, d’instructions atomiques et de verrous, afin de garantir la stabilité. Différentes solutions sont générées, et leur coût est évalué, de façon à choisir la solution la plus efficace.
DFence [108] (https://github.com/eth-srl/DFENCE) analyse des programmes C (LLVM) sur les modèles TSO et PSO. Il utilise un ordonnanceur dit “démoniaque”, qui tente de générer des exécutions non-SC. Si une telle exécution est rencontrée, des primitives de synchronisation sont ajoutées et une nouvelle analyse est lancée.
Trencher [44] (https://tcs.cs.tu-bs.de/trencher.html) analyse des systèmes de transitions sur le modèle TSO. Basé sur des travaux précédents [46], il réduit le problème de robustesse au problème d’atteignabilité sur SC, en instrumentant le programme source de différentes façons afin de détecter toutes les exécutions non-SC. Il cherche pour cela des violations minimales (cycles) dans les exécutions, puis énumère toutes les solutions permettant de rétablir la robustesse. Ces solutions sont encodées sous forme de problème ILP (Integer Linear Programming), et un solveur se charge de déduire la moins chère.
Musketeer [26, 27] (www.cprover.org/wmm/fence13) analyse des programmes écrits en C et supporte les sémantiques x86-TSO, Power et ARM. Il utilise un modèle axiomatique pour exprimer la sémantique des programmes, et recherche la présence de cycles critiques (au sens de Shasha et Snir) pour déterminer comment placer les diverses primitives de synchronisation permettant de rétablir la “stabilité” du programme analysé.
Persist [2] (https://github.com/PhongNgo/persistence) analyse des systèmes de transitions sur le modèle TSO (en utilisant le langage d’entrée de Trencher). Le critère utilisé pour s’assurer qu’un programme n’expose que des comportements SC est celui de la persistance, une notion qui diffère de la robustesse (ou stabilité). Cette notion s’appuie sur des traces représentant l’ordre des opérations par processus et l’ordre dans lequel les écritures sont propagées en mémoire. Un programme sera considéré comme persistant s’il génère les mêmes traces en SC et en TSO. Dans ce cas les états atteignables seront les mêmes en SC et en TSO. Si un programme n’est pas persistant, un algorithme guidé par les contre-exemples permet d’ajouter un nombre minimal de primitives de synchronisation pour rétablir la persistance.
|
Table des matières
1 Introduction
2 Etat de l’art
2.1 Restriction aux comportements SC
2.2 Vérification de propriétés de sûreté
2.3 Vérification paramétrée de propriétés de sûreté : Dual-TSO
3 Présentation de Cubicle-W
3.1 Rappels sur Cubicle
3.1.1 Des tableaux paramétrés
3.1.2 Langage d’entrée
3.1.3 Exemple 1 : Mutex Naïf
3.1.4 Exemple 2 : Protocole MESI
3.1.5 Exemple 3 : Two-Phase Commit
3.1.6 Analyse d’atteignabilité de Cubicle
3.2 Des compteurs de processus
3.2.1 Expression des compteurs sous Cubicle
3.2.2 Exemple de système à compteurs : Sense-Reversing Barrier
3.3 Modèle mémoire opérationnel de Cubicle-W
3.4 Extensions et restrictions du langage d’entrée
3.5 Exemples
3.5.1 Mutex Naïf
3.5.2 Spinlock Linux
3.5.3 L’Arbitre
4 Model checking modulo mémoire faible
4.1 Expérimentation : modélisation directe des tampons TSO
4.2 Modèle mémoire axiomatique de Cubicle-W
4.2.1 Modèle mémoire axiomatique original de TSO
4.2.2 Prise en compte de l’ordonnancement dans le modèle TSO axiomatique
4.2.3 Prise en compte des opérations atomiques
4.2.4 Stratégie de construction de ghb en arrière
4.3 Théorie des tableaux faibles
4.3.1 Langage à événements
4.3.2 Sémantique des formules logiques
4.3.3 Etats
4.4 Systèmes de transitions à tableaux faibles
4.4.1 Langage de description
4.4.2 Etats initiaux
4.4.3 Etats dangereux
4.4.4 Transitions
4.5 Analyse d’atteignabilité
4.5.1 Algorithme d’atteignabilité arrière
4.5.2 Calcul de préimage
4.5.3 Exemple d’exploration arrière
4.6 Résultats et comparaison avec d’autres outils
5 Traduction de programmes x86 vers Cubicle-W
5.1 Langage source
5.1.1 Syntaxe
5.1.2 Représentation des états x86-TSO
5.1.3 Notations pour manipuler les tampons TSO
5.1.4 Sémantique des programmes
5.1.5 Sémantique des instructions
5.1.6 Synchronisation Tampon / Mémoire
5.2 Schéma de traduction
5.2.1 Traduction des instructions x86-TSO
5.2.2 Traduction des opérations sur les compteurs
5.2.3 Traduction des programmes
5.3 Correction
5.4 Exemples
5.4.1 Mutex avec lock xchg
5.4.2 Spinlock Linux
5.4.3 Sense-Reversing Barrier
5.5 Résultats
6 Conclusion
