Poétique de la mémoire partagée
Institution:
Paris 7Disciplines:
Directors:
Abstract EN:
We examine here the behaviour of concurrent programs that execute on modem architectures. Such program do not execute according to the natural model, namely Sequential Consistency (defined by Leslie Lamport), where the result of an execution of such a program corresponds to an interleaving of the instructions involved. Indeed, modem multiprocessors feature weak memory models, for they propose several optimisations such as the write atomicity relaxation (store buffering being a particular case), or the reorderings of instructions. We propose here a generic Framework, implemented in the Coq proof assistant, which allows us to define and reason about weak memory models. Thereby, we define a hierarchy of these models, and prove formally that several existing models (Sequential Consistency, Sun TSO, PSO, RMO, and Alpha) belong to our framework. The documentations of these processors are written in natural language, hence lack the mathematical precision require to establish formal models for such architectures. To remedy this state of affairs, we adopt an empirical approach: we have developed a testing tool named diy (do it yourself), which allows us to test precisely which optimisations are exhibited by a given machine. We used this tool to test several Power machines intensively, which not only allowed us to design a fragment of a model for the Power architecture, but also to exhibit a bug in the implementation of barriers of Power 5 machines. Finally, we focus on the stability of an execution of a program from one architecture to another. We define an execution to be stable when its validity on a weak architecture entails its validity on a stronger one. To illustrate this definition, we study the semantics of several synchronisation primitives as defined in the Power documentation, and prove that they ensure stability. Then, we propose a characterisation of the executions that are stable from a weak architecture to sequential consistency.
Abstract FR:
Nous examinons ici le comportemement des programmes concurrents s'exécutant sur les architectures modernes. Contrairement a ce que l'on pourrait attendre, de tels programmes ne s'exécutent pas suivant le modèle naturel, a savoir Sequential Consistency (défini par Leslie Lamport), ou le résultat d'une exécution d'un programme concurrent correspond a un entrelacement des instructions intervenant sur les différents processeurs mis en partie. En effet, les processeurs modernes bénéficient de modèles de mémoire dits faibles, car ils proposent diverses optimisations tels que le relâchement de l'atomicité des écritures (dont le store buffering est un cas particulier), ou le reordonnancement d'instructions. Nous proposons donc ici un cadre de travail générique, mis en oeuvre au sein de l'assistant de preuve Coq, permettant de définir et de raisonner au sujet des modèles de mémoire faibles. Ainsi, nous définissons une hiérarchie des modèles de mémoire faibles, et nous démontrons formellement que plusieurs modèles existants (Sequential Consistency, Sun TSO, PSO, RMO, et Alpha) appartiennent a notre cadre. Les documentations de ces processeurs sont écrites en langue naturelle, et manque par conséquent de la rigueur mathématique nécessaire a l'établissement de modèles formels pour de telles architectures. Pour y remédier, nous adoptons une approche empirique: nous avons développe un outil de test nomme diy (do it yourself), qui permet de tester précisément quelles sont les optimisations proposées par une machine donnée. Nous avons utilise cet outil pour tester plusieurs machines Power de manière intensive, ce qui nous a permis non seulement de dresser un modèle pour un fragment de l'architecture Power, mais également de révéler une erreur dans la mise en oeuvre des barrières sur les machines de type Power 5. . Pour finir, nous nous concentrons sur le problème de la stabilité des exécutions d'un programme donne d'une architecture a un autre. Nous définissons une exécution comme étant stable quand sa validité sur une architecture faible entraine sa validité sur une architecture plus forte. Pour illustrer cette définition, nous étudions la sémantique de plusieurs primitives de synchronisation présentées dans la documentation de Power, et démontrons qu'elles garantissent la stabilité. Enfin, nous proposons une caracterisation des exécutions stables d'une architecture faible vers Sequential Consistency.