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 is very 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. It can be run using the herd tool - we provide a link to the herd tool's web interface below.
The herd 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 should allow 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.
We periodically release updates to the Arm consistency model, to include new features, or existing features which have been captured formally more recently.
Access the Memory Model Tool
How to use the Memory Model Tool
Read our blog exploring a working example of how to use the Memory Model Tool.