企业官网建设流程全解析

Linux 内核内存一致性模型（LKMM）并发原语 herd 事件表示完全指南

【免费下载链接】linuxLinux kernel source tree项目地址: https://gitcode.com/GitHub_Trending/li/linux

本指南以 Linux 内核源码树中的tools/memory-model/Documentation/herd-representation.txt（由 Documentation/dev-tools/lkmm/docs/herd-representation.rst 以字面量方式包含）为核心，系统讲解内核各类并发原语（READ_ONCE、smp_mb、原子 RMW 操作、自旋锁、RCU/SRCU 等）在 herdtools7 的 cat 语言模型中如何被抽象为事件（events）与链接（links）。读完本文，你将能够读懂 herd7 的输入/输出事件流，理解linux-kernel.def、linux-kernel.bell、linux-kernel.cat、lock.cat四个模型文件的协作关系，并能借助herd7命令验证真实 litmus 测试。

一、背景：LKMM 与 herd 事件表示

Linux 内核内存一致性模型（Linux-kernel memory consistency model，LKMM）位于 tools/memory-model/ 目录，使用 cat（*.cat）语言编写，由外部工具herd7执行——herd7 会穷举搜索小型 litmus 测试的状态空间；配套的klitmus7可将 litmus 测试转换成内核模块并在真实硬件上运行（tools/memory-model/README）。

为了让模型可计算，herd7 需要先把 C 风格的并发原语调用"翻译"成一种抽象指令表示，这正是 herd-representation.txt 所定义的映射表：每个内核并发原语对应什么样的事件（或事件序列），以及事件之间由什么链接（po、rmw）相连。该文档位于内核文档站点的 Documentation/dev-tools/lkmm/ 目录下，与 explanation.txt 一起被官方定位为"深入了解 LKMM 需求、原理与实现"的进阶阅读材料（见 tools/memory-model/Documentation/README）。

二、事件与链接图例（Legend）

herd-representation.txt开篇即给出全部事件类型与关系链接的速查图例：

约定：表格单元格中的空行表示"与前一行相同"。例如下表中atomic_read与READ_ONCE的事件表示相同，故后者单元格留空。

这些事件类型在 lock.cat 中有精确定义——LKR/LKW 总是成对出现（所有 RMW 事件序列皆如此）；LKR、LF、RL、RU 是读事件，其中 LKR 带 Acquire 排序；LKW 与 UL 是写事件，其中 UL 带 Release 排序；LKW、LF、RL、RU 本身没有排序属性。

三、重要：语法表示与语义集合并不总是一一对应

原文档专门给出了一条极易踩坑的说明：

语法（syntactic）表示并不总是与linux-kernel.cat中的集合与关系一致，因为linux-kernel.bell与lock.cat中做了重定义。例如：LKR 与 LKW 之间的po链接会被升级为rmw链接；W[ACQUIRE]不会被包含进 Acquire 集合。

这两个例子都能在源码中找到直接证据：

• po升级为rmw：在 lock.cat 中，let lk-rmw = ([LKR] ; po-loc ; [LKW]) \ (po ; po)先把 LKR 与其 RMW 搭档 LKW 按地址配对，随后let rmw = rmw | lk-rmw将其并入全局rmw关系——这正是"语法上只是po，语义上却是rmw"的根源。
• W[ACQUIRE]不在 Acquire 集合：在 linux-kernel.bell 中，let FailedRMW = RMW \ (domain(rmw) | range(rmw))先剔除失败的 RMW，然后：

let Acquire = ACQUIRE \ W \ FailedRMW let Release = RELEASE \ R \ FailedRMW let Mb = MB \ FailedRMW let Noreturn = NORETURN \ W

即：落在写事件上的 ACQUIRE 标注、落在读事件上的 RELEASE 标注、以及失败 RMW 上的各类标注，都会被"过滤"掉，因为它们不提供相应的语义排序。这与表中smp_store_release映射为W[RELEASE]、而xchg_acquire映射为R*[ACQUIRE] ->rmw W*[ACQUIRE]的语法表示形成了鲜明对照——读表时一定要区分"herd7 看到的事件标签"与"模型最终使用的语义集合"。

另外原文档声明：表格仅展示add与and两种运算的表示；sub、inc、dec、or、xor、andnot的表示与之对应/相同，故省略。

四、非 RMW 操作的事件表示

下表是原文档"Non-RMW ops"部分的完整内容（空单元格表示与前一行相同）：

源码印证

这些映射全部能在 linux-kernel.def 中找到逐条对应：

READ_ONCE(X) __load{ONCE}(X) WRITE_ONCE(X,V) { __store{ONCE}(X,V); } smp_store_release(X,V) { __store{RELEASE}(*X,V); } smp_load_acquire(X) __load{ACQUIRE}(*X) rcu_assign_pointer(X,V) { __store{RELEASE}(X,V); } rcu_dereference(X) __load{ONCE}(X) smp_store_mb(X,V) { __store{ONCE}(X,V); __fence{MB}; } smp_mb() { __fence{MB}; } rcu_read_lock() { __fence{rcu-lock}; } rcu_read_unlock() { __fence{rcu-unlock}; } synchronize_rcu() { __fence{sync-rcu}; } synchronize_rcu_expedited() { __fence{sync-rcu}; } srcu_read_lock(X) __load{srcu-lock}(*X) srcu_read_unlock(X,Y) { __store{srcu-unlock}(*X,Y); } synchronize_srcu(X) { __srcu{sync-srcu}(X); }

几个值得注意的实现细节：

• smp_store_mb被翻译为"W[ONCE]后跟一条po链接指向F[MB]"，即"带全屏障的存储"= 普通 ONCE 存储 + 程序顺序的全屏障。
• synchronize_rcu()与其快速路径变体synchronize_rcu_expedited()都映射为F[sync-rcu]；synchronize_srcu()与其变体则映射为独立的SRCU[sync-srcu]事件（见 linux-kernel.def）。
• spin_is_locked的两种结果分别对应RL/RU事件，且 lock.cat 中let LF = LF | RL会把RL视作一种"无排序属性的读"（LF 的同类）；同文件还定义了critical = ([LKW] ; po-loc ; [UL]) \ ...来把 LKW 与其对应的 UL 配对。
• 屏障标签的完整枚举定义在 linux-kernel.bell 的enum Barriers中：wmb、rmb、MB、barrier、rcu-lock、rcu-unlock、sync-rcu、before-atomic、after-atomic、after-spinlock、after-unlock-lock、after-srcu-read-unlock，统一声明为instructions F[Barriers]。

五、无返回值 RMW 操作

原文档"RMW ops w/o return value"部分完整内容：

• atomic_add/atomic_and这类"不返回新值"的原子操作，被表示为一次完整的 RMW：R*[NORETURN] ->rmw W*[NORETURN]。NORETURN标注的含义在 linux-kernel.bell 中注释为"non-return RMW 的 R 部分"；在 linux-kernel.def 中atomic_add(V,X) { __atomic_op{NORETURN}(X,+,V); }，atomic_sub、atomic_and、atomic_or、atomic_xor、atomic_inc、atomic_dec、atomic_andnot等同样走__atomic_op{NORETURN}模板。
• 注意spin_lock在语法表示中只是LKR ->po LKW（程序顺序），但如第三节所述，lock.cat 会通过lk-rmw与let rmw = rmw | lk-rmw把它升级为rmw链接——自旋锁获取在语义上就是一次原子的读-改-写。

六、有返回值 RMW 操作

原文档"RMW ops w/ return value"部分完整内容：

这一整族操作对应 linux-kernel.def 中的三类模板：

__atomic_op_return{MB|ONCE|ACQUIRE|RELEASE}(X,op,V) __atomic_fetch_op{MB|ONCE|ACQUIRE|RELEASE}(X,op,V) __xchg{MB|ONCE|ACQUIRE|RELEASE}(X,V)

• 默认（不带后缀）的返回值原子操作使用MB标注，即"全屏障 RMW"；*_relaxed用ONCE，*_acquire用ACQUIRE，*_release用RELEASE。同一行的多个宏（如atomic_xchg与xchg、atomic_fetch_and与atomic_fetch_add）共享相同的事件形态。
• atomic_add_negative系列在 linux-kernel.def 中实现为__atomic_op_return{...}(X,+,V) < 0，即"有返回值的 RMW + 结果判断"，因此同样归入此类。
• 从语法上看R*[MB] ->rmw W*[MB]的读与写都打了MB标签。在 linux-kernel.cat 的mb定义中有专门注释说明这一设计的动机："全屏障 RMW（成功的cmpxchg()、xchg()等）行为上如同被smp_mb()包围"，其效果通过给读、写加上Mb标签并补充相应的po边来形式化：

([M] ; po ; [Mb & R]) | ([Mb & W] ; po ; [M]) |

这正是"默认 RMW = 全屏障"这一语义在 cat 模型中的落点。

七、条件 RMW 操作

原文档"Conditional RMW ops"部分完整内容：

条件 RMW 的关键语义是成败两种路径产生不同的事件形态：

• 成功：完整的R*[...] ->rmw W*[...]读写对；
• 失败：只有一次读R*[...]，没有写入、也没有rmw链接——这正是 linux-kernel.bell 中FailedRMW（不在任何rmw链接定义域/值域内的 RMW 事件）所要筛除的对象；而Mb = MB \ FailedRMW则保证失败路径上的MB标注不会提供全屏障语义。
• atomic_add_unless在 linux-kernel.def 中映射为__atomic_add_unless{MB}(X,V,W)，与其他条件 RMW 一样走 MB（全屏障）路径。
• spin_trylock成功时与spin_lock相同（LKR ->po LKW，语义上升级为rmw），失败时产生单个LF（Lock-Fail）事件；LF事件的 reads-from 候选边由 lock.cat 中的possible-rfe-noncrit-lf与all-possible-rfe-lf生成。

八、从表示到模型：四个核心文件的分工

要真正"看懂"这张表示表，需要理解 LKMM 四个核心文件的流水线分工（tools/memory-model/README 中的 DESCRIPTION OF FILES 一节有官方说明）：

1. linux-kernel.def：把 C 风格原语调用翻译成 herd7 内部指令集（ISA），例如READ_ONCE(X) __load{ONCE}(X)。这是"表示表"最直接的机器可读版本。
2. linux-kernel.bell：对指令分类——列出各事件类型的子类型（enum Accesses、enum Barriers、enum SRCU），做 RCU/SRCU 读侧临界区的嵌套配对分析，并过滤掉不提供语义排序的语法标注（Acquire、Release、Mb、Noreturn的重定义）。
3. linux-kernel.cat：规定哪些重排被禁止，即定义coherence、atomic、happens-before、propagation、rcu等公理；其中的mb、ppo、hb、pb、rb等关系全部建立在上层事件集合之上。
4. lock.cat：锁操作的前端分析——把LKR/LKW配对为rmw、把UL并入写集合、把LKR并入 Acquire、生成锁的rf/co关系，并检查自死锁（lock-nest）、未配对锁事件等合法性约束。

因此，表示表是"观察窗口"，而.bell/.cat才是"语义裁决者"：同一个R[ACQUIRE]标注，经过Acquire = ACQUIRE \ W \ FailedRMW过滤后是否真正参与 Acquire 集合，取决于事件的具体类型与成败路径。

九、实操验证：用 herd7 跑一个 litmus 测试

理解了表示之后，可以立刻用仓库自带的 litmus 测试验证（需自行安装 herd7，官方要求版本 7.58 及以上，见 tools/memory-model/README）：

$ cd tools/memory-model $ herd7 -conf linux-kernel.cfg litmus-tests/MP+pooncerelease+poacquireonce.litmus

测试 MP+pooncerelease+poacquireonce.litmus 演示经典的"消息传递"模式：生产者WRITE_ONCE(*buf, 1)后smp_store_release(flag, 1)，消费者smp_load_acquire(flag)后READ_ONCE(*buf)，exists (1:r0=1 /\ 1:r1=0)为坏结局。结合本文的表示表：smp_store_release→W[RELEASE]、smp_load_acquire→R[ACQUIRE]，Release/ Acquire 配对提供了po-rel/acq-po排序，从而禁止坏结局（herd7 输出Never）。

其他可直接运行的示例分布在 tools/memory-model/litmus-tests/（如SB+fencembonceonces.litmus、LB+poonceonces.litmus、MP+polocks.litmus、Z6.0+pooncelock+pooncelock+pombonce.litmus等）。linux-kernel.cfg中还设置了macros linux-kernel.def、bell linux-kernel.bell、model linux-kernel.cat与variant lkmmv2，说明 herd7 组合这几个文件的方式与本文所述一致；scripts/ 目录下的checklitmus.sh、judgelitmus.sh等脚本则可用于批量校验 litmus 测试。

十、小结

herd-representation.txt用一张精确的映射表把 Linux 内核的并发原语世界"投影"到 herd7 的事件空间：普通读写/屏障/锁/RCU/SRCU 被折叠为R、W、F、LKR、LKW、UL、LF、RL、RU、SRCU等事件，原子 RMW 被表达为R* ->rmw W*的读写对，条件 RMW 则依据成败路径分裂为"完整 RMW"或"仅读"两种形态。理解该表示是深入阅读 linux-kernel.cat 与 linux-kernel.bell 的前提，也是编写、调试 LKMM litmus 测试时判断"某个原语到底提供什么排序"的最快途径。需要快速回顾时，可配合 cheatsheet.txt 的排序矩阵一并使用；而 explanation.txt 提供了更完整的模型原理叙述。

【免费下载链接】linuxLinux kernel source tree项目地址: https://gitcode.com/GitHub_Trending/li/linux