Modern multiprocessors and microprocesseurs implement weak or relaxed memory models, in which the apparent order of memory operation does not follow the sequential consistency (SC) proposed by Leslie Lamport. Any concurrent program running on such architecture and designed with an SC model in mind may exhibit new behaviors during its execution, some of which may potentially be incorrect. For instance, a mutual exclusion algorithm, correct under an interleaving semantics, may no longer guarantee mutual exclusion when implemented on a weaker architecture. Reasoning about the semantics of such programs is a difficult task. Moreover, most concurrent algorithms are designed for an arbitrary number of processus. We would like to ensure the correctness of concurrent algorithms, regardless of the number of processes involved. For this purpose, we rely on the Model Checking Modulo Theories (MCMT) framework, developed by Ghilardi and Ranise, which allows for the verification of safety properties of parameterized concurrent programs, that is to say, programs involving an arbitrary number of processes. We extend this technology with a theory for reasoning about weak memory models. The result of this work is an extension of the Cubicle model checker called Cubicle-W, which allows the verification of safety properties of parameterized transition systems running under a weak memory model similar to TSO.

Les multiprocesseurs et microprocesseurs multicĹ“urs modernes mettent en oeuvre des modèles mĂ©moires dits faibles ou relâchĂ©s, dans dans lesquels l’ordre apparent des opĂ©rations mĂ©moire ne suit pas la cohĂ©rence sĂ©quentielle (SC) proposĂ©e par Leslie Lamport. Tout programme concurrent s’exĂ©cutant sur une telle architecture et conçu avec un modèle SC en tĂŞte risque de montrer Ă  l’exĂ©cution de nouveaux comportements, dont certains sont potentiellement des comportements incorrects. Par exemple, un algorithme d’exclusion mutuelle correct avec une sĂ©mantique par entrelacement pourrait ne plus garantir l’exclusion mutuelle lorsqu’il est mis en oeuvre sur une architecture plus relâchĂ©e. Raisonner sur la sĂ©mantique de tels programmes s’avère très difficile. Par ailleurs, bon nombre d’algorithmes concurrents sont conçus pour fonctionner indĂ©pendamment du nombre de processus mis en oeuvre. On voudrait donc pouvoir s’assurer de la correction d’algorithmes concurrents, quel que soit le nombre de processus impliquĂ©s. Pour ce faire, on s’appuie sur le cadre du Model Checking Modulo Theories (MCMT), dĂ©veloppĂ© par Ghilardi et Ranise, qui permet la vĂ©rification de propriĂ©tĂ©s de sĂ»retĂ© de programmes concurrents paramĂ©trĂ©s, c’est-Ă -dire mettant en oeuvre un nombre arbitraire de processus. On Ă©tend cette technologie avec une thĂ©orie permettant de raisonner sur des modèles mĂ©moires faibles. Le rĂ©sultat ce ces travaux est une extension du model checker Cubicle, appelĂ©e Cubicle-W, permettant de vĂ©rifier des propriĂ©tĂ©s de systèmes de transitions paramĂ©trĂ©s s’exĂ©cutant sur un modèle mĂ©moire faible similaire Ă  TSO.