Operational semantics of relaxed memory models
Institution:
NiceDisciplines:
Directors:
Abstract EN:
Most current multiprocessor architectures and shared memory parallel programming languages are not sequentially consistent for parallel programs. Their possible behaviors are characterized by weak or relaxed memory models. A memory model describes the way in which parallel programs can interact by reading and writing the shared memory. Thus, a relaxed memory model exhibits more behaviors than sequential consistency (a “strong” memory model). The fact that most architectures have relaxed memory models has been known for decades, and yet few programmers understand which are the exact behaviors a parallel program can have in such architectures. We argue in this thesis that the problem stems from the difficulty in understanding the specification of these relaxed memory models. Firstly because few architectures or programming languages provide a formal definition of their memory model. And secondly because the majority of the existing formal definitions are axiomatic, which hinders their understandability and makes them unsuitable for language-based techniques such as static analysis or model checking. We propose an alternative characterization of relaxed memory models. Our characterization is operational, which we believe makes it simpler to understand for the programmer, and better suited to standard language-based techniques. Our first contribution in this thesis is the operational formalization of writebuffering architectures. Write-buffering is pervasive across multi-core architectures, and thus its understanding is fundamental for parallel programming in such architectures. By means of standard programming languages concepts, we prove that the standard DRF guarantee is satisfied by our formalization. Hence, reasoning about sequentially consistent computations is sound for programs free of simultaneous accesses on a single memory location. Our second contribution is a framework for the operational characterization of speculative computation techniques. This framework allows us to formally define the intuitive notion of valid speculation. For this framework two languages are considered; a high-level programming language that supports locks; and a low-level programming language, closer to the Instruction Set Architecture (ISA) of a machine, that only supports barriers and a simple compare-and-swap instruction. We identify properties for programs of both of these languages that are sufficient to guarantee that only sequentially consistent behaviors can be observed when the programs are executed speculatively. The final contribution is the instantiation of the write-buffering and speculative frameworks to formalize the TSO, PSO and RMO memory models of the Sparc architecture. In particular, we observe that the framework of write buffers is not well suited to formalize liberal relaxations as allowed by RMO. We prove a correspondence result between the formalizations of PSO and TSO I ii in both frameworks. The fact that RMO cannot be instantiated by means of write-buffers is a good indication that the speculative framework is more general than the one of write buffers.
Abstract FR:
La plupart des architectures multiprocesseurs et des langages de programmation parallèle `a mémoire partagée actuels ne sont pas séquentiellement consistant pour les programmes parallèles. Leurs comportements possibles sont caractérisés par des modèles mémoire faibles ou relâchés. Un modèle mémoire décrit la manière dont les programmes parallèles peuvent interagir par des lectures et des écritures dans la mémoire partagée. Ainsi, un modèle mémoire relâché présente plus de comportements que le modèle séquentiellement consistant (modèle mémoire “fort”). Le fait que la plupart des architectures ont des modèles mémoire relâchés est connu depuis des décennies, et peu de programmeurs comprennent quels sont les comportements exacts qu’un programme parallèle peut avoir dans de telles architectures. Nous soutenons dans cette thèse que le problème provient de la difficulté `a comprendre la spécification de ces modèles de mémoire. Ceci, d’abord car peu d’architectures ou de langages de programmation donnent une définition formelle de leur modèle mémoire, et, ensuite, parce que la plupart des définitions formelles existantes sont axiomatiques, ce qui les rendent difficiles `a comprendre et inadaptées `a des techniques basées sur le langage, telles que l’analyse statique ou le model checking. Notre première contribution dans cette thèse est la formalisation opérationnelle des architectures `a tampons d’écriture (write buffers). Les write buffers sont omniprésents dans les architectures multi-core, et donc leur compréhension est fondamentale pour la programmation parallèle dans de telles architectures. En utilisant des concepts standard des langages de programmation, nous démontrons que la classique “DRF guarantee” est satisfaite dans notre formalisation. Par conséquent, raisonner par des calculs séquentiellement consistant est correct pour les programmes libres d’accès simultanés sur une même case mémoire. Notre deuxième contribution est un framework pour la caractérisation opérationnelle des techniques de calcul spéculatif. Ce framework nous permet de définir formellement la notion intuitive de spéculation valide. Pour cette formalisation deux langues sont considérés, un langage de programmation de haut niveau avec un mécanisme d’exclusion mutuel par verrous, et un langage de programmation de bas niveau, plus proche de l’Instruction Set Architecture (ISA) d’une machine, avec des mécanismes de barrières mémoire et des instructions atomiques. Pour les programmes de ces deux langages, nous identifions les propriétés suffisantes pour garantir que seuls les comportements séquentiellement consistant peuvent être observés lorsque les programmes sont exécutés de manière spéculative. La dernière contribution est l’instanciation de ces deux frameworks sémantiques pour formaliser les modèles mémoire TSO, PSO et RMO de iii iv l’architecture Sparc. En particulier, nous observons que le framework des write buffers n’est pas bien adapté pour formaliser des relaxations trop libérales comme le permet RMO. Nous démontrons un résultat de correspondance entre les formalisations de PSO et TSO dans les deux frameworks. Le fait que RMO peut pas être instanciée par le framework des write buffers est une bonne indication que le framework spéculatif est plus générale que celui des write buffers.