A consistency model determines which result values are permissible for a read access.
Arm has developed its own consistency model for two main reasons. First, to allow users to get an understanding of the working of the Arm consistency model. Without the model tool, this can be complex and hard to understand. The Arm consistency model tells a user which results values are permitted for a read by the Arm architecture. This information is useful to Software developers, compiler writers, verification engineers and others.
Second, to make a precise, formal statement of the Arm consistency model: the Arm consistency model is a machine-readable, executable, and formal artefact, given as a "cat" file - the model is written in the cat domain specific language. It can be run using the herd7 tool – the following link is for the herd7 tool’s web interface.
The herd7 tool allows the user to execute the model with a specific question about the possible final states of the program. More specifically it can run the model over litmus tests - small programs written in Arm assembly. Using this tool allows users to probe the model with a specific question captured as a litmus test, or to develop an intuitive understanding of the model through experimentation.
The description of the memory model in the Arm Architecture Reference Manual is based on an English transliteration of the formal executable cat model - as such they should be completely consistent for the areas that the cat file supports - please report any discrepancies found to firstname.lastname@example.org.
We periodically release updates to the Arm consistency model, to include new features, or existing features which have been captured formally more recently. The current known areas of limitations of the model are described in the comments of the cat file and Arm is working to address these in the future.
Arm puts in reasonable efforts to ensure that any such changes do not invalidate existing hardware implementations or normal software usage. Arm distributes a configuration file "forbidden.conf". to drive the diy testing tool to generate vast numbers of litmus tests which allow to compare the Arm model against hardware for example. If any update that Arm makes causes problems with existing hardware or software, please report the problem, citing the versions of the model that have been changed, and explaining the impact to software to email@example.com.
Note: Arm is aware of external efforts to model the Arm architecture, and welcomes and fosters engagement to avoid errors and discrepancies - please contact Arm at firstname.lastname@example.org. However Arm does not endorse any model other than that this cat file, as well as its English rendition in the Arm ARM, as being authoritative. This applies to models which cover areas not yet covered by the Arm model, including those models that have been developed in the context of a collaboration with Arm.
A working example of how to use the herd7 Memory Model Tool
Read our blog exploring a working example of how to use the herd7 Memory Model Tool.
How to generate litmus tests automatically with the diy7 tool
Read our blog on how to generate litmus tests automatically using the diy7 tool.