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 modelLKMM位于 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。二、事件与链接图例Legendherd-representation.txt开篇即给出全部事件类型与关系链接的速查图例记号含义RLoad 事件读WStore 事件写FFence 事件屏障LKRLock-Read 事件spin_lock()或成功spin_trylock()的读部分LKWLock-Write 事件对应 RMW 的写部分ULUnlock 事件spin_unlock()LFLock-Fail 事件失败的spin_trylock()RLRead-Locked 事件spin_is_locked()返回 TrueRURead-Unlocked 事件spin_is_locked()返回 FalseR*包含在 RMW 中的 Load 事件W*包含在 RMW 中的 Store 事件SRCUSleepable-Read-Copy-Update 事件可睡眠 RCU 相关事件poProgram-Order 链接程序顺序rmwRead-Modify-Write 链接每个 rmw 链接同时也是 po 链接约定表格单元格中的空行表示与前一行相同。例如下表中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部分的完整内容空单元格表示与前一行相同C 宏事件READ_ONCER[ONCE]atomic_readWRITE_ONCEW[ONCE]atomic_setsmp_load_acquireR[ACQUIRE]atomic_read_acquiresmp_store_releaseW[RELEASE]atomic_set_releasesmp_store_mbW[ONCE] -po F[MB]smp_mbF[MB]smp_rmbF[rmb]smp_wmbF[wmb]smp_mb__before_atomicF[before-atomic]smp_mb__after_atomicF[after-atomic]spin_unlockULspin_is_locked成功RL失败RUsmp_mb__after_spinlockF[after-spinlock]smp_mb__after_unlock_lockF[after-unlock-lock]rcu_read_lockF[rcu-lock]rcu_read_unlockF[rcu-unlock]synchronize_rcuF[sync-rcu]rcu_dereferenceR[ONCE]rcu_assign_pointerW[RELEASE]srcu_read_lockR[srcu-lock]srcu_down_readsrcu_read_unlockW[srcu-unlock]srcu_up_readsynchronize_srcuSRCU[sync-srcu]smp_mb__after_srcu_read_unlockF[after-srcu-read-unlock]源码印证这些映射全部能在 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部分完整内容C 宏事件atomic_addR*[NORETURN] -rmw W*[NORETURN]atomic_andspin_lockLKR -po LKWatomic_add/atomic_and这类不返回新值的原子操作被表示为一次完整的 RMWR*[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部分完整内容C 宏事件atomic_add_returnR*[MB] -rmw W*[MB]atomic_fetch_addatomic_fetch_andatomic_xchgxchgatomic_add_negativeatomic_add_return_relaxedR*[ONCE] -rmw W*[ONCE]atomic_fetch_add_relaxedatomic_fetch_and_relaxedatomic_xchg_relaxedxchg_relaxedatomic_add_negative_relaxedatomic_add_return_acquireR*[ACQUIRE] -rmw W*[ACQUIRE]atomic_fetch_add_acquireatomic_fetch_and_acquireatomic_xchg_acquirexchg_acquireatomic_add_negative_acquireatomic_add_return_releaseR*[RELEASE] -rmw W*[RELEASE]atomic_fetch_add_releaseatomic_fetch_and_releaseatomic_xchg_releasexchg_releaseatomic_add_negative_release这一整族操作对应 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部分完整内容C 宏事件atomic_cmpxchg成功R*[MB] -rmw W*[MB]失败R*[MB]cmpxchgatomic_add_unlessatomic_cmpxchg_relaxed成功R*[ONCE] -rmw W*[ONCE]失败R*[ONCE]atomic_cmpxchg_acquire成功R*[ACQUIRE] -rmw W*[ACQUIRE]失败R*[ACQUIRE]atomic_cmpxchg_release成功R*[RELEASE] -rmw W*[RELEASE]失败R*[RELEASE]spin_trylock成功LKR -po LKW失败LF条件 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失败时产生单个LFLock-Fail事件LF事件的 reads-from 候选边由 lock.cat 中的possible-rfe-noncrit-lf与all-possible-rfe-lf生成。八、从表示到模型四个核心文件的分工要真正看懂这张表示表需要理解 LKMM 四个核心文件的流水线分工tools/memory-model/README 中的 DESCRIPTION OF FILES 一节有官方说明linux-kernel.def把 C 风格原语调用翻译成 herd7 内部指令集ISA例如READ_ONCE(X) __load{ONCE}(X)。这是表示表最直接的机器可读版本。linux-kernel.bell对指令分类——列出各事件类型的子类型enum Accesses、enum Barriers、enum SRCU做 RCU/SRCU 读侧临界区的嵌套配对分析并过滤掉不提供语义排序的语法标注Acquire、Release、Mb、Noreturn的重定义。linux-kernel.cat规定哪些重排被禁止即定义coherence、atomic、happens-before、propagation、rcu等公理其中的mb、ppo、hb、pb、rb等关系全部建立在上层事件集合之上。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/MPpooncereleasepoacquireonce.litmus测试 MPpooncereleasepoacquireonce.litmus 演示经典的消息传递模式生产者WRITE_ONCE(*buf, 1)后smp_store_release(flag, 1)消费者smp_load_acquire(flag)后READ_ONCE(*buf)exists (1:r01 /\ 1:r10)为坏结局。结合本文的表示表smp_store_release→W[RELEASE]、smp_load_acquire→R[ACQUIRE]Release/ Acquire 配对提供了po-rel/acq-po排序从而禁止坏结局herd7 输出Never。其他可直接运行的示例分布在 tools/memory-model/litmus-tests/如SBfencembonceonces.litmus、LBpoonceonces.litmus、MPpolocks.litmus、Z6.0pooncelockpooncelockpombonce.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创作声明：本文部分内容由AI辅助生成（AIGC），仅供参考