一句话：综述 Arm 用 cat 语言形式化并发一致性模型的工作，含混合大小访问扩展、等价表述及 x86 验证。
本文回顾 Arm 在形式化并发建模上的持续工作。Arm 最初用 cat 语言写成的架构一致性模型于 2017 年发布并上游到 herd+diy 工具链；此后模型被扩展，加入混合大小访问等特性，并给出两种可证明等价的替代表述。文章系统总结这些扩展与等价性结果，并通过大规模实验表明，其处理混合大小访问的原则也适用于 x86。作者还说明，这些替代表述可推广到任何采用与 Arm 类似风格的模型。
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.
@article{paperbot1216,
title = {Armed Cats},
author = {Jade Alglave and Will Deacon and Richard Grisenthwaite and Antoine Hacquard and Luc Maranget},
journal = {ACM Transactions on Programming Languages and Systems},
volume = {43},
number = {2},
year = {2021},
doi = {10.1145/3458926}
}