Herding Cats
- 1 July 2014
- journal article
- Published by Association for Computing Machinery (ACM) in ACM Transactions on Programming Languages and Systems
- Vol. 36 (2), 1-74
- https://doi.org/10.1145/2627752
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 acknowledged 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.Keywords
This publication has 45 references indexed in Scilit:
- Relaxed Operational Semantics of Concurrent Programming LanguagesElectronic Proceedings in Theoretical Computer Science, 2012
- You don't know jack about shared variables or memory modelsCommunications of the ACM, 2012
- Memory modelsCommunications of the ACM, 2010
- A unified theory of shared memory consistencyJournal of the ACM, 2004
- Information-flow models for shared memory with an application to the powerPC architectureIEEE Transactions on Parallel and Distributed Systems, 2003
- AlloyACM Transactions on Software Engineering and Methodology, 2002
- Relating Event and Trace Semantics of Hardware Description LanguagesThe Computer Journal, 2002
- Shared memory consistency models: a tutorialComputer, 1996
- Efficient and correct execution of parallel programs that share memoryACM Transactions on Programming Languages and Systems, 1988
- Enumeration of the Elementary Circuits of a Directed GraphSIAM Journal on Computing, 1973