深入解析 Linux 内核内存一致性模型LKMM从 Litmus 测试到公理验证【免费下载链接】linuxLinux kernel source tree项目地址: https://gitcode.com/GitHub_Trending/li/linux导读Linux 内核运行在多核、多架构的硬件之上内存访问的重排序memory reordering问题既是并发编程的难点也是内核正确性的基石。Linux 内核内存一致性模型Linux Kernel Memory Consistency Model简称 LKMM是内核官方维护的、用 cat 语言编写的正式化内存模型配合外部的herd7/klitmus7工具可以穷举验证小型并发测试litmus tests的所有可能执行结果。本文以 Documentation/dev-tools/lkmm/index.rst 所指向的文档体系为主线结合tools/memory-model/目录下的模型源码带你掌握 LKMM 的定位、工具链安装、litmus 测试编写、输出解读以及模型公理背后的实现原理。LKMM 是什么内核并发正确性的形式化证明器在 Documentation/dev-tools/lkmm/index.rst 中明确指出这一章节直接渲染tools/memory-model/与tools/memory-model/Documentation/目录下的纯文本文档这些文档以pure plain text形式维护。也就是说LKMM 的全部灵魂都存放在内核源码树的tools/memory-model/目录中。根据 tools/memory-model/README 的引言LKMM 是Linux 内核的内存一致性模型简称 memory model使用 cat 语言编写可由外部提供的herd7模拟器执行该模拟器会穷举探索小型 litmus 测试的状态空间。这意味着 LKMM 不是一个玩具实验而是可执行的、形式化的并发语义规范herd7对 litmus 测试做穷举式状态空间搜索判定某个坏结果是否可能发生属于离线形式化验证klitmus7把同一个 litmus 测试转换成 Linux 内核模块加载后在真实硬件上运行用实证方式检验结果。二者配合让内核开发者既能从数学上证明某个并发模式的安全性又能在具体硬件上观察真实的统计行为。LKMM 本身也是学术成果的产物——tools/memory-model/linux-kernel.cat 的文件头注明其早期版本发表于 ASPLOS 2018 论文Frightening small children and disconcerting grown-ups: Concurrency in the Linux kernel。环境准备herd7 / klitmus7 的版本要求LKMM 模型文件本身随内核源码一起发布但执行它的herd7与klitmus7工具需要单独下载。根据 tools/memory-model/README 的 REQUIREMENTS 章节必须使用7.58 或更高版本的herd7和klitmus7工具来自 herdtools7 项目安装说明见其INSTALL.md尽管这些工具通常提供向后兼容但并不绝对保证——未来版本的 herd7 可能无法与本版本的模型协同工作届时通常会随后续内核版本提供兼容的模型klitmus7独立于本仓库提供的模型它依赖目标内核版本进行构建与执行内核 API 的变更会要求 klitmus7 同步升级。README 还给出了 klitmus7 与目标内核、herdtools7 的兼容性对照表目标内核版本herdtools7 版本-- 4.147.48 --4.15 -- 4.197.49 --4.20 -- 5.57.54 --5.6 -- 5.167.56 --5.17 --7.56.1 --快速上手用 herd7 跑第一个 litmus 测试命令行与输出逐行解读litmus-tests.txt 强调运行命令必须在tools/memory-model目录下执行。以仓库自带的 SBfencembonceonces.litmus 为例cd $LINUX_SOURCE_TREE/tools/memory-model herd7 -conf linux-kernel.cfg litmus-tests/SBfencembonceonces.litmus其中linux-kernel.cfg是收集了常见命令行参数的便捷配置文件见下文模型文件架构。对应的输出为Test SBfencembonceonces Allowed States 3 0:r00; 1:r01; 0:r01; 1:r00; 0:r01; 1:r01; No Witnesses Positive: 0 Negative: 3 Condition exists (0:r00 /\ 1:r00) Observation SBfencembonceonces Never 0 3 Time SBfencembonceonces 0.01 Hashd66d99523e2cac6b06e66f4c995ebb48这段输出的核心解读见 tools/memory-model/READMEPositive: 0 Negative: 3与Never 0 3均表示本测试的exists子句0:r00 /\ 1:r00即两个进程都读到对方尚未写入的值在任何执行中都无法满足末尾的两个数字分别表示满足与不满足exists子句的最终状态数量。在 litmus-tests.txt 中Observation一行的三种可能取值被解释得更清楚Never坏结果在任何执行中都不会出现Sometimes坏结果在部分执行中出现Always坏结果在所有执行中出现。注意herd7本身不评判好坏exists子句表示坏结果只是 LKMM 的使用约定——把exists条件取反再运行你会得到相反的解释。用 klitmus7 在真实硬件上验证同一个 litmus 测试可以通过klitmus7转换为内核模块并真实运行tools/memory-model/READMEmkdir mymodules klitmus7 -o mymodules litmus-tests/SBfencembonceonces.litmus cd mymodules; make sudo sh run.sh真实硬件上的输出与 herd7 的穷举结果形成了互证Test SBfencembonceonces Allowed Histogram (3 states) 644580 :0:r01; 1:r00; 644328 :0:r00; 1:r01; 711092 :0:r01; 1:r01; No Witnesses Positive: 0, Negative: 2000000 Condition exists (0:r00 /\ 1:r00) is NOT validated Observation SBfencembonceonces Never 0 2000000 Time SBfencembonceonces 0.16Positive: 0 Negative: 2000000表明在两百万次试验中exists子句指定的状态从未出现——与 herd7 的穷举结论Never完全一致。这也验证了 SBfencembonceonces.litmus 头注释中的论断全内存屏障足以排序 store-buffering 模式每个进程写入前一个进程读取的变量而锁与 RCU 也可以做到但其他手段不行。模型文件架构五个核心文件的分工tools/memory-model/目录下的模型本体由五个关键文件组成tools/memory-model/README 的 DESCRIPTION OF FILES 章节它们各司其职文件职责linux-kernel.bell对相关指令进行分类包括内存引用、内存屏障、原子读-改-写RMW操作、锁获取/释放以及 RCU 操作形式上它列出模型使用的各种事件类型的子类型并执行 RCU 读侧临界区嵌套分析linux-kernel.cat规定内存引用、内存屏障、原子 RMW 与 RCU 所禁止的重排序形式上规定模型所禁止的执行。允许的执行是满足模型在文件中定义的coherence、atomic、happens-before、propagation与rcu五条公理的执行linux-kernel.cfg收集常见 herd7 命令行参数的便捷配置文件linux-kernel.def把 C 风格语法映射到 herd7 内部的 litmus 测试指令集体系结构ISA即哪些内核 API 可以被 litmus 测试调用的清单lock.cat提供锁获取与释放的前端分析例如把一次锁获取与之前/之后的释放关联起来并检查自死锁形式上定义了锁原语上可能的 reads-from 与 coherence order 关系的性能增强生成方案此外litmus-tests/ 目录存放代表性 litmus 测试其选取标准见 litmus-tests/README是简单simple线程数量少每个线程函数相对简单正交orthogonal不存在两个描述模型同一方面的测试教科书式textbook开发者可以轻松复制-粘贴-修改把这些模式用到自己的代码上。深入模型公理从 linux-kernel.cat 看验证原理linux-kernel.cat用 cat 语言把 LKMM 的验证规则写成可执行代码。阅读 tools/memory-model/linux-kernel.cat 可以看到模型的骨架基本关系L23-L30 附近定义了 acquire/release 的程序序关系let acq-po [Acquire] ; po ; [M] let po-rel [M] ; po ; [Release]围栏fences定义了rmb、wmb、mb等屏障其中mb全屏障还包含了成功的 cmpxchg()、xchg() 等全屏障 RMW 操作如同被 smp_mb() 包裹的语义L36-L49以及smp_mb__after_spinlock()After-spinlock等特化围栏。五大公理对应 tools/memory-model/README 对linux-kernel.cat的说明coherence每个变量的顺序一致性let com rf | co | fracyclic po-loc | com as coherenceL79-L80——要求同一变量上的读写关系reads-from、coherence order、from-reads与程序序合起来必须无环atomic原子 RMWempty rmw (fre ; coe) as atomicL83——禁止读-改-写操作在读取与写入之间被其他写插入happens-beforehappens-before 公理let hb [Marked] ; (ppo | rfe | ((prop \ id) int)) ; [Marked]acyclic hb as happens-beforeL109-L110——要求 happens-before 关系无环propagation传播公理let pb prop ; strong-fence ; hb* ; [Marked]acyclic pb as propagationL117-L118——每次非 rf 的传播链都需要强围栏这一公理正是 IRIWfencembonceoncesOnceOnce.litmus 这类测试被判定 forbidden 的依据rcuRCU 公理位于文件的 RCU 部分约束 RCU 读侧临界区与宽限期之间的关系。模型还区分了preserved program order (ppo)L89-L95把地址依赖、数据依赖、控制依赖等纳入了进程内的保序关系。可以看到linux-kernel.cat是 LKMM 能证明什么的最终裁决者而linux-kernel.bell负责把每个事件打上Acquire、Release、Once、Marked等标签供 cat 文件中的关系计算使用。Litmus 测试格式详解消息传递示例逐行拆解litmus-tests.txt 用消息传递Message PassingMP模式完整讲解了 litmus 测试的格式。该模式在内核中非常常见一个标志变量y表示缓冲区x已填充完毕如果消费者看到标志被置位却读到缓冲区的旧值就是灾难。示例测试MPpooncereleasepoacquireonce要回答的问题是smp_store_release()与smp_load_acquire()是否足以避免这种坏结果C MPpooncereleasepoacquireonce {} P0(int *x, int *y) { WRITE_ONCE(*x, 1); smp_store_release(y, 1); } P1(int *x, int *y) { int r0; int r1; r0 smp_load_acquire(y); r1 READ_ONCE(*x); } exists (1:r01 /\ 1:r10)逐行要点litmus-tests.txt 的 Examples and Format 章节第 1 行C表明该文件采用 LKMM 的 C 语言格式完整 C 语言的一个小片段MPpooncereleasepoacquireonce是测试名按惯例为去掉.litmus后缀的文件名初始化区{}表示使用默认零初始化需要非默认值时在花括号内显式赋值如x42; y42;此时exists子句中的1:r10也要相应改为1:r142进程定义每个进程对应一个内核任务task/kthread/workqueue/threadLKMM 语境中这些术语可互换。进程名必须是单个P加连续数字P0、P1...。形参是指向全局共享变量的指针且名字有意义——P0与P1都声明int *x表示二者操作同一个全局变量x。全局变量永远按引用传递绝不写P0(int x, int y)局部变量约定俗成用r加数字命名。一个常见 bug 是忘了把全局变量加进进程的形参列表——这有时会报错但也可能让本意是全局的变量被静默当成未声明的局部变量可用的内核 API进程代码可用内核的原子操作、部分排他锁函数、部分 RCU/SRCU 函数完整清单见 linux-kernel.defexists断言在尘埃落定两个进程都完成、所有内存引用与屏障都已传播到全系统之后评估。局部变量引用必须加进程前缀如1:r0。注意断言表达式是 litmus 语言而非 C是相等比较、/\表示与、\/表示或、~表示逻辑非对应 C 的!不是C 的按位取反可用括号改变优先级。本测试的 herd7 输出中Observation MPpooncereleasepoacquireonce Never 0 3证明release-acquire 链确实阻断了读到标志但读到旧缓冲区的坏结果。三个可达终态为1:r00; 1:r10;、1:r00; 1:r11;、1:r01; 1:r11;被exists标记的1:r01; 1:r10;不在其中。控制结构if 与 Load-BufferingLKMM 支持 C 的if语句可用于建模条件分支但条件分支只有在非常小心时才能提供保序编译器很容易优化掉条件分支。LBfencembonceoncectrlonceonce.litmus 演示了内核中用于环形缓冲区生产者/消费者同步的 load-buffering 场景C LBfencembonceoncectrlonceonce {} P0(int *x, int *y) { int r0; r0 READ_ONCE(*x); if (r0) WRITE_ONCE(*y, 1); } P1(int *x, int *y) { int r0; r0 READ_ONCE(*y); smp_mb(); WRITE_ONCE(*x, 1); } exists (0:r01 /\ 1:r01)if (r0)让 P0 只在读到非零值后才写y由于 P1 的写发生在读之后直觉上exists子句两个 r0 都为 1不可满足LKMM 的Never 0 2证实了这一点。但注意没有while语句因为全状态空间搜索难以处理迭代——特殊情况可用下文提到的技巧模拟循环也可用手工展开sparingly谨慎使用。实战技巧Tricks and Trapslitmus-tests.txt 的 Tricks and Traps 章节提供了调试与建模的高级技巧是排查复杂问题的利器。调试输出locations 子句默认情况下herd7 只输出exists子句中出现的变量。以 SBrfionceonce-poonceonces.litmus 为例它探测的是硬件内存排序的隐秘角落该测试的输出Sometimes 1 3表明CPU 被允许窥探自己的存储缓冲区snoop their own store buffers——除 s390 外所有 Linux 支持的 CPU 家族都会这样做导致不同 CPU 对来自不同 CPU 的存储顺序产生分歧。若想同时看到0:r1、1:r3、x、y的值可加入locations [0:r1; 1:r3; x; y]locations子句让 herd7 在终态输出中显示额外的寄存器与位置。注意如果想看某个全局变量在进程执行中途的值可以READ_ONCE()到新局部变量再加入locations但要小心——在某些 litmus 测试中加一个READ_ONCE()会改变结果。模拟自旋锁filter 子句herd7 的状态空间搜索是指数级复杂度的潜在无限循环如等待锁显然不可行。解决办法是用filter子句丢弃那些未成功获取锁的执行而不是用自旋循环filter (0:r20 /\ 1:r20) exists (0:r10 /\ 1:r10)该技巧用xchg_acquire()模拟锁获取成功写r20、用smp_store_release()模拟锁释放filter保留两个进程都成功获取锁的执行。其输出Never 0 2证明这种用法确实正确模拟了锁。要点filter子句保留使其表达式为真的执行说什么要保留而非丢弃什么它比把同样条件塞进exists更快因为 herd7 能在表达式一旦不满足时立即放弃该执行而exists只在最后评估一个反直觉的细节filter只在被检查变量的最后一次赋值时评估——若某变量中途被赋成不满足条件的值、之后又改了并不会提前被过滤。链表建模地址依赖LKMM 只能处理每个节点只含一个指向下一节点的指针的链表但足够模拟 RCU 指针发布场景。MPonceassignderefonce.litmus 演示了rcu_assign_pointer()/rcu_dereference()模式。其初始化区的yz; z0;值得特别注意yz不是把z的值赋给y而是把y设为z的地址——这创建了一个链表y指向zz是空指针。exists子句中的1:r0x同样是比较地址测试 P1 是否读到 P0 新发布的指针却看到旧值。输出Never 0 2表明 RCU 读者不可能在访问新插入节点时看到初始化前的旧值。注释语法C 与 Ocaml 混用litmus 测试的不同部分由不同解析器处理因此注释语法也不同C 语法部分用 C 注释/* */或//其余部分用 Ocaml 注释(* *)。如果不喜欢混用可以用 C 预处理器统一处理。模拟异步 RCU 宽限期call_rcu()未被 LKMM 直接建模但可以通过增加一个进程来模拟该进程先做 acquire 加载c对应 call_rcu 请求、然后调用synchronize_rcu()等待一个宽限期、最后执行回调体模拟kfree()。由于该进程可能过早启动用filter (2:r01)拒绝2:r0不为 1 的执行。性能优化-speedcheck true状态空间搜索的代价是指数级的。实用建议litmus-tests.txt 的 Performance 章节从小开始逐步增大尽量把代码拆成小块每块代表一个核心并发需求使用-speedcheck true让 herd7 不再生成所有可能终态只关注exists子句是否可满足。文档给出的实测数据某个 10 进程 RCU 测试在普通 x86 笔记本上约 6 秒完成开启该选项后约300 毫秒一个数量级以上的提升16 进程测试从 15 分钟降到约 40 秒19 进程测试从 2 小时 40 分钟降到约 8 分钟——代价是放弃额外的数十万个状态例如 16 进程测试会少 65,535 个状态不想要命令行参数时可以在 litmus 测试里加一个与exists表达式完全相同的filter子句获得类似加速但在开发和调试 litmus 测试时查看完整状态集通常极有帮助。LKMM 的边界已知局限litmus-tests.txt 的 LIMITATIONS 章节如实列出了模型不做的事情编译器优化未被精确建模READ_ONCE()/WRITE_ONCE()限制了编译器优化但某些情况下编译器仍可能破坏模型假设详见 explanation.txt 的 THE PROGRAM ORDER RELATION: po AND po-loc 与 A WARNING 小节。例如编译器若能推断出依赖所携带变量的值就可能用常量替换来切断依赖。反过来LKMM 有时会高估可重排序程度做出比架构更弱的保证这并非坏事——它给编译器留出了优化空间单一变量的多种访问宽度、未对齐或部分重叠访问不支持异常与中断未建模可通过额外进程模拟MMIO、DMA 等 I/O 不支持自修改代码alternatives 机制、函数跟踪、BPF JIT、模块加载器不支持原子 RMW、锁、RCU 的完整建模未提供但支持面已相当大见 linux-kernel.def。具体限制包括rcu_assign_pointer()传入 NULL 时内核不提供保序但 LKMM 按 store-release 建模atomic_long_add_unless()等 unless RMW 未建模可用atomic_cmpxchg()模拟例外是atomic_add_unless()由 herd7 直接提供call_rcu()、rcu_barrier()未建模可用额外进程 release-acquire 模拟读写锁未建模可用原子 RMW 模拟。同时litmus 测试支持的 C 语言片段相当受限无自动 C 预处理可手动运行除Pn()进程函数外不能定义其他函数形参必须是指向全局共享变量的指针不能按值传参只能调用 herd7 内建函数或 linux-kernel.def 中定义的函数switch、do、for、while、goto均不支持switch可用if模拟循环可手工展开或借助预处理器herd7 只理解int与指针类型无浮点、枚举、字符、字符串、数组、结构体变量声明解析非常宽松几乎没有类型检查初始化器与 C 语义不同初始化器中的共享变量名表示指向该变量的指针int x y相当于 C 的int x y不支持动态内存分配可预分配多个静态变量变通。文档最后提醒随着硬件、用例与编译器的演进LKMM 本身也在不断变化——这正是它随内核版本发布的原因。Litmus 测试命名规范看名字就知道测什么litmus-tests/README 介绍了命名约定。litmus 测试通常按内容命名格式为测试类 每个进程的访问描述串以分隔.litmus后缀。测试类定义了访问模式与访问的变量例如经典的MP消息传递类——一个进程写两个变量、另一个进程读这两个变量其他常见类别还有LBload buffering、SBstore buffering、IRIWindependent reads of independent writes、WRCwrite-read-combined、S、Z6.0等litmus-tests/README 对仓库内每个测试都有一句话说明例如IRIWfencembonceoncesOnceOnce.litmus测试两个读进程是否能在写之间用smp_mb()对一对写达成一致顺序而 LKMM 的 propagation 规则正是该测试 forbidden 的原因。进程访问描述串由Rfi、Po、Fre、Once、Release、Acquire等描述符构成连接关系描述符来自 herd7 工具或 linux-kernel.bellOnce、Release、Acquire等。例如SBrfionceonce-poonceonces中的rfi表示进程内部 reads-frompo表示程序序Once表示READ_ONCE()/WRITE_ONCE()类无序访问。生成/检查这些名字可用norm7 -bell linux-kernel.bell \ Rfi Once PodRR Once Fre Once Rfi Once PodRR Once Fre Once | \ sed -e s/:.*//g # 输出: SBrfionceonce-poonceonces查看完整描述符列表可运行diyone7 -bell linux-kernel.bell -show edges。按图索骥根据你的水平选择阅读路线LKMM 文档集面向从新手到专家的全谱系读者。Documentation/README 给出了按知识水平递进的阅读路线后文假定读者已理解前文内容术语困惑时可查 glossary.txt刚接触内核并发simple.txt熟悉内核并发、想总览底层原语ordering.txt熟悉原语、想上手 litmus 测试litmus-tests.txt需要无锁访问锁保护的共享变量locking.txt想要多线程场景的直觉理解recipes.txt想深究编译器对控制依赖的影响control-dependencies.txt需要标注有意的并发访问以回应 KCSAN 报告access-marking.txt想要快速参考cheatsheet.txt想了解 LKMM 的需求、原理与实现explanation.txt 与 herd-representation.txt对相关文献感兴趣硬件手册、学术论文、标准委员会工作论文等references.txt。附给初学者的简单并发之道simple.txt 提醒我们LKMM 虽复杂但大多数场景有更简单的选择按复杂度递增依次是单线程代码code locking用全局锁把整段代码包成单线程执行适用于稀有路径内核曾为移除大内核锁付出巨大努力请谨慎添加小内核锁打包代码packaged code把并发交给库函数如lib/目录、include/linux/list.h的链表宏、工作队列、smp_call_function()、哈希表与搜索树等数据锁data locking锁与具体数据结构实例绑定如每个哈希桶一把锁可随桶数量自然扩展Per-CPU 处理每个 CPU 各自单线程化代价是内存占用增加percpu_counter与 RCU 的DEFINE_PER_CPU*()都是范例打包原语顺序锁读侧不要写、RCU读侧不要写、不要更新读者可见的数据、用锁保护更新、原子操作注意_relaxed/_acquire/_release后缀的有限保序语义cmpxchg()只在成功时提供全序无锁全序访问需要无锁访问共享变量时只使用全序操作无锁统计与启发式atomic_read()、atomic_set()、READ_ONCE()、WRITE_ONCE()不提供保序但能阻止编译器做破坏性优化——无序真的意味着无序别想当然。最后务必警惕现代优化编译器早已不是带语法的汇编器普通 C 赋值会惨遭重写务必使用READ_ONCE()/WRITE_ONCE()等显式原语。若以上都不满足需求再进入 recipes.txt 深入内存排序的下一层。小结LKMM 是 Linux 内核并发正确性的形式化基石linux-kernel.bell给事件分类打标签linux-kernel.cat以五条公理裁决执行合法性herd7穷举验证 litmus 测试klitmus7在真实硬件上复核。理解并善用这套工具链——从仓库自带的 litmus-tests/ 出发按命名规范复制-粘贴-修改借助locations、filter、-speedcheck true等技巧调试与提速同时清醒认识模型的边界——你将能把内存序是否正确从玄学变成可证明、可复现的工程实践。【免费下载链接】linuxLinux kernel source tree项目地址: https://gitcode.com/GitHub_Trending/li/linux创作声明：本文部分内容由AI辅助生成（AIGC），仅供参考