Herding Cats: Modelling, Simulation, Testing, and Data Mining for Weak Memory

Abstract : We propose an axiomatic generic framework for modelling weak memory. We show how to instantiate this framework for Sequential Consistency (SC), Total Store Order (TSO), C++ restricted to release-acquire atomics, and Power. For Power, we compare our model to a preceding operational model in which we found a flaw. To do so, we define an operational model that we show equivalent to our axiomatic model. We also propose a model for ARM. Our testing on this architecture revealed a behaviour later acknowl-edged as a bug by ARM, and more recently, 31 additional anomalies. We offer a new simulation tool, called herd, which allows the user to specify the model of his choice in a concise way. Given a specification of a model, the tool becomes a simulator for that model. The tool relies on an axiomatic description; this choice allows us to outperform all previous simulation tools. Additionally, we confirm that verification time is vastly improved, in the case of bounded model checking. Finally, we put our models in perspective, in the light of empirical data obtained by analysing the C and C++ code of a Debian Linux distribution. We present our new analysis tool, called mole, which explores a piece of code to find the weak memory idioms that it uses. ACM Reference Format: Jade Alglave, Luc Maranget, and Michael Tautschnig. 2014. Herding cats: Modelling, simulation, testing, and data mining for weak memory.
Type de document :
Article dans une revue
ACM Transactions on Programming Languages and Systems (TOPLAS), ACM, 2014, 36 (2), pp.7:1--7:74. <10.1145/2627752>
Liste complète des métadonnées


https://hal.inria.fr/hal-01081364
Contributeur : Luc Maranget <>
Soumis le : vendredi 7 novembre 2014 - 16:45:29
Dernière modification le : lundi 5 octobre 2015 - 17:01:12
Document(s) archivé(s) le : dimanche 8 février 2015 - 10:50:22

Fichier

a7-alglave.pdf
Fichiers éditeurs autorisés sur une archive ouverte

Identifiants

Collections

Citation

Jade Alglave, Luc Maranget, Michael Tautschnig. Herding Cats: Modelling, Simulation, Testing, and Data Mining for Weak Memory. ACM Transactions on Programming Languages and Systems (TOPLAS), ACM, 2014, 36 (2), pp.7:1--7:74. <10.1145/2627752>. <hal-01081364>

Partager

Métriques

Consultations de
la notice

287

Téléchargements du document

170