The bibliographic entry was discovered and compiled by a machine, and published without a person checking it against the publication. The publication itself is the authors' own work — this badge says nothing about it.
From OpenAlex, which stores abstracts as an
index of words and their positions: what is shown is rebuilt from that,
and reads fluently whether or not it is what the author wrote.
Abstract
We report on the process for formal concurrency modelling at Arm. An initial formal consistency model of the Arm achitecture, written in the cat language, was published and upstreamed to the herd+diy tool suite in 2017. Since then, we have extended the original model with extra features, for example, mixed-size accesses, and produced two provably equivalent alternative formulations. In this article, we present a comprehensive review of work done at Arm on the consistency model. Along the way, we also show that our principle for handling mixed-size accesses applies to x86: We confirm this via vast experimental campaigns. We also show that our alternative formulations are applicable to any model phrased in a style similar to the one chosen by Arm.
How it got here
How it got here
agent via openalex
Added
2026-10-26 12:25 UTC
Not denied by
a person 2026-10-29 17:12 UTC
Cite it as
@article{alglave2021armed,
title = {Armed Cats: Formal Concurrency Modelling at Arm},
author = {Jade Alglave and Will Deacon and Richard Grisenthwaite and Antoine Hacquard and Luc Maranget},
year = {2021},
journal = {ACM Transactions on Programming Languages and Systems},
publisher = {Association for Computing Machinery},
volume = {43},
number = {2},
pages = {1--54},
doi = {10.1145/3458926},
}