一句话：为 Linux 内核内存一致性提供可执行的 cat 形式模型，并用 herd 验证，形式化并证明 RCU 定律。
Linux 内核中的并发行为及其一致性模型长期存在争议：内核支持 30 多种 CPU 架构，程序应如何表现、在外来硬件上是否正确，需要精确规范。本文提出一个用 cat 语言编写的 Linux 内核内存一致性形式模型，该模型不仅形式化，还可由 herd 模拟器执行，便于程序员实验和建立直觉。作者将模型与真实硬件行为对照测试，并与内核维护者协商精化模型。最后，他们形式化了 Read-Copy-Update（RCU）同步机制的基本定律，并证明其中一种实现满足该定律。
Concurrency in the Linux kernel can be a contentious topic. The Linux kernel mailing list features numerous discussions related to consistency models, including those of the more than 30 CPU architectures supported by the kernel and that of the kernel itself. How are Linux programs supposed to behave? Do they behave correctly on exotic hardware? A formal model can help address such questions. Better yet, an executable model allows programmers to experiment with the model to develop their intuition. Thus we offer a model written in the cat language, making it not only formal, but also executable by the herd simulator. We tested our model against hardware and refined it in consultation with maintainers. Finally, we formalised the fundamental law of the Read-Copy-Update synchronisation mechanism, and proved that one of its implementations satisfies this law.