Linux 内核 LKMM 原子测试Litmus Tests格式、herd7 状态空间分析与进阶技巧完全指南【免费下载链接】linuxLinux kernel source tree项目地址: https://gitcode.com/GitHub_Trending/li/linux本文围绕 Linux 内核内存一致性模型Linux-Kernel Memory Model简称 LKMM的原子测试litmus test展开从测试文件的完整格式消息传递示例逐行解析、初始化与控制结构到locations调试子句、filter自旋锁模拟、RCU 宽限期模拟等进阶技巧直至 LKMM 的已知局限。读完本文后你将能够直接编写、修改并运行 LKMM 原子测试理解 herd7 输出中Never / Sometimes / Always的判定语义并知道在遇到状态空间爆炸时如何取舍。一、资料来源先复制粘贴再从零开始与许多软件一样编写原子测试时改编一个已有测试通常比从零创建更好。内核源码树中自带了两组可直接使用的测试tools/memory-model/litmus-tests/一组教科书式的代表性测试。从 tools/memory-model/README 的说明看这些测试被刻意挑选为1) 简单进程数少、每进程代码少2) 正交没有两个测试描述内存模型的同一侧面3) 便于开发者复制-粘贴-修改后套用到自己的代码上。Documentation/litmus-tests/按内核 API 语义分类的测试集包含 atomic 子目录、locking 子目录如DCL-broken.litmus与DCL-fixed.litmus展示双重检查锁的错误与修复版本、rcu 子目录如RCUsyncfree.litmus。此外内核外部的 herdtools 社区还维护了数量更多的示例测试集原文档提到可在 github 及 kernel.org 的相关仓库中找到数千个示例此处不展开外部链接。使用git grep的-l和-L参数是快速找到与需求相似的已有测试的实用技巧# 在 litmus-tests 中按模式查找相似的测试 git grep -l smp_store_release -- tools/memory-model/litmus-tests git grep -L 20 -- tools/memory-model/litmus-tests即便如此理解原子测试格式本身仍然必不可少因为任何改编都需要你读懂每个子句。二、格式详解以消息传递Message-Passing测试为例下面这个示例是 LKMM 中最常见的消息传递用例一个标志y表示缓冲区x已填好可被消费。如果消费者看到标志已置位、却因内存乱序读到缓冲区的旧值就是严重错误。本示例验证smp_store_release()smp_load_acquire()组合是否足以避免这种坏结果1 C MPpooncereleasepoacquireonce 2 3 {} 4 5 P0(int *x, int *y) 6 { 7 WRITE_ONCE(*x, 1); 8 smp_store_release(y, 1); 9 } 10 11 P1(int *x, int *y) 12 { 13 int r0; 14 int r1; 15 16 r0 smp_load_acquire(y); 17 r1 READ_ONCE(*x); 18 } 19 20 exists (1:r01 /\ 1:r10)该测试实际位于 tools/memory-model/litmus-tests/MPpooncereleasepoacquireonce.litmus逐行解读如下第 1 行以C开头标识该文件采用 LKMM 的 C 语言格式完整 C 语言的一个小片段。行首之后是测试名按惯例为去掉.litmus后缀的文件名。第 2 行机器生成的测试常在此放一段双引号注释运行时被忽略。你也可以自己加注释但由于测试的不同部分由不同解析器处理注释规则并不统一见注释小节。C 代码部分可用/* */或//注释。第 3 行初始化段。本测试用默认的零初始化即可因此写成空的{}。需要非默认初始化时初始化段必须非空见下一节。第 5-9 行 / 11-18 行两个进程。每个进程对应一个 Linux 内核任务kthread、workqueue、线程等LKMM 讨论中这些术语常互换使用。进程名必须是P加从 0 开始连续编号如P0、P1——这一约束在实践中很有用一个.litmus文件若匹配^P1(但不匹配^P2(必然是一个双进程测试。参数列表每个函数的形参都是该进程用到的全局变量的指针。与普通 C 不同形参名字是有意义的P0和P1都声明了形参x意味着两个进程操作的是同一个名为x的全局变量。全局变量永远按引用传给进程所以必须是P0(int *x, int *y)绝不能写成P0(int x, int y)。局部变量P0没有局部变量P1声明了r0、r1。名字可自由选择但出于历史惯例用r加数字。一个常见 bug 是忘记把某全局变量加入进程参数列表——有时会报错但有时该全局变量会被静默地当作未声明的局部变量处理。进程代码接近 Linux 内核 C 风格可用内核的许多原子操作、部分互斥锁函数以及部分 RCU/SRCU 函数。当前受支持函数的近似清单见 tools/memory-model/linux-kernel.def。第 7 行WRITE_ONCE(*x, 1)是对全局x的无序存储第 8 行smp_store_release(y, 1)是对全局y的 release 存储第 16-17 行则是 acquire 加载与无序加载。第 20 行exists断言在所有尘埃落定之后两进程都结束、所有内存访问与内存屏障都已传播到系统各处评估终态。局部变量必须加进程前缀1:指明归属。注意断言表达式使用的是测试语言而非 C是相等不是赋值/\是与\/是或~是逻辑非对应 C 的!不要与 C 的按位取反~混淆括号可改变优先级。本例的exists子句在消费者看到y已置位、却把x当作未填好即1:r01且1:r10时成立——这正是我们要证明不会发生的坏结果。运行测试与解读输出运行命令必须且只能在tools/memory-model目录下执行cd tools/memory-model herd7 -conf linux-kernel.cfg litmus-tests/MPpooncereleasepoacquireonce.litmus其中-conf linux-kernel.cfg指向 tools/memory-model/linux-kernel.cfg该配置把常用参数集中起来从仓库文件内容看它声明了macros linux-kernel.def、bell linux-kernel.bell、model linux-kernel.cat、variant lkmmv2并附带一组图形化输出选项graph columns、showevents noregs、edgeattr hb,color,indigo等。对应的输出形如1 Test MPpooncereleasepoacquireonce Allowed 2 States 3 3 1:r00; 1:r10; 4 1:r00; 1:r11; 5 1:r01; 1:r11; 6 No 7 Witnesses 8 Positive: 0 Negative: 3 9 Condition exists (1:r01 /\ 1:r10) 10 Observation MPpooncereleasepoacquireonce Never 0 3 11 Time MPpooncereleasepoacquireonce 0.00 12 Hash579aaa14d8c35a39429b02e698241d09输出的解读要点第 10 行是最关键的一行Never 0 3表示exists子句标记的坏结果从未发生尾部数字为满足 exists 的终态数:不满足的终态数。也可能是Sometimes部分执行出现坏结果或Always所有执行都出现坏结果。需要强调herd7 本身不做价值判断exists 子句 坏结果只是 LKMM 的约定——把条件取反再跑一遍即可看到这一点。第 2-5 行States 3给出全部终态数量随后逐行列出如1:r00; 1:r10;表示 P1 的两次加载都读到 0。由于第 10 行是Never被exists标记的状态自然不在列表中。这份完整状态清单在调试新测试时非常有用。其余各行第 1 行回显测试名与Test/Allowed第 6 行No等价于第 10 行的Never第 8 行的Positive: 0 Negative: 3与第 10 行尾部数字同义第 9 行回显exists子句以免翻查源文件第 11 行给出分析耗时小测试通常几毫秒0.00很常见第 12 行是测试文件内容哈希供管理数千个测试及其输出的工具链使用帮助 LKMM 维护者判断某次模型改动影响了哪些测试。关于工具本身tools/memory-model/README 指出herd7与klitmus7需要外部单独安装要求 herdtools7 7.58 及以上版本模型本身是写在内核树linux-kernel.cat文件中的 cat 语言模型klitmus7则能把测试转换成内核模块在真实硬件上跑两百万次试验做统计验证输出中的Positive: 0 Negative: 2000000即两百万次试验均未命中坏状态。三、初始化空段、显式初始化与地址陷阱上面的示例依赖x、y的默认零初始化相同测试也可以显式初始化1 C MPpooncereleasepoacquireonce 2 3 { 4 x42; 5 y42; 6 } 7 8 P0(int *x, int *y) 9 { 10 WRITE_ONCE(*x, 1); 11 smp_store_release(y, 1); 12 } 13 14 P1(int *x, int *y) 15 { 16 int r0; 17 int r1; 18 19 r0 smp_load_acquire(y); 20 r1 READ_ONCE(*x); 21 } 22 23 exists (1:r01 /\ 1:r142)第 3-6 行把x、y都初始化为 42因此第 23 行的exists子句必须把1:r10改成1:r142。运行结果与之前整体相同只是 42 取代了 01 Test MPpooncereleasepoacquireonce Allowed 2 States 3 3 1:r01; 1:r11; 4 1:r042; 1:r11; 5 1:r042; 1:r142; 6 No 7 Witnesses 8 Positive: 0 Negative: 3 9 Condition exists (1:r01 /\ 1:r142) 10 Observation MPpooncereleasepoacquireonce Never 0 3 11 Time MPpooncereleasepoacquireonce 0.02 12 Hashab9a9b7940a75a792266be279a980156陷阱为了避免42到处硬编码一个诱人做法是定义全局变量initval42再把所有42替换成initval。这样做不会把x、y初始化为 42而是初始化为initval的地址可以实际试一试。理解这一点有助于看懂后面链表小节中yz的写法——在那里地址语义反而是被刻意利用的。四、极简的控制结构if 可用while 不可用LKMM 支持 C 的if语句从而可以建模条件分支但条件分支要影响排序必须非常小心——编译器优化掉条件分支的能力出人意料地强。下面的示例是 Linux 内核中用于环形缓冲区生产者/消费者同步的load bufferingLB用例P0检查操作能否进行P1完成其更新。测试文件对应 tools/memory-model/litmus-tests/LBfencembonceoncectrlonceonce.litmus1 C LBfencembonceoncectrlonceonce 2 3 {} 4 5 P0(int *x, int *y) 6 { 7 int r0; 8 9 r0 READ_ONCE(*x); 10 if (r0) 11 WRITE_ONCE(*y, 1); 12 } 13 14 P1(int *x, int *y) 15 { 16 int r0; 17 18 r0 READ_ONCE(*y); 19 smp_mb(); 20 WRITE_ONCE(*x, 1); 21 } 22 23 exists (0:r01 /\ 1:r01)P1第 10 行的if按预期工作只有第 9 行从x加载到非零值时第 11 行才执行。由于P1对x写 1 只发生在它从y读取之后直觉上exists子句不可能成立。LKMM 的结论一致1 Test LBfencembonceoncectrlonceonce Allowed 2 States 2 3 0:r00; 1:r00; 4 0:r01; 1:r00; 5 No 6 Witnesses 7 Positive: 0 Negative: 2 8 Condition exists (0:r01 /\ 1:r01) 9 Observation LBfencembonceoncectrlonceonce Never 0 2 10 Time LBfencembonceoncectrlonceonce 0.00 11 Hashe5260556f6de495fd39b556d1b831c3b而没有while语句——完整状态空间搜索对迭代有天然困难但有一些技巧可以处理特殊情形见下一节。此外也可以谨慎地使用循环展开loop-unrolling技巧。五、技巧与陷阱Tricks and Traps5.1 调试输出用locations子句显示更多变量herd7 默认只在输出中显示exists子句涉及的变量。调试时往往还需要看其他变量的值。考虑这个探测硬件内存排序冷门角落的测试对应仓库中的 tools/memory-model/litmus-tests/SBrfionceonce-poonceonces.litmus此处略有改动1 C SBrfionceonce-poonceonces 2 3 {} 4 5 P0(int *x, int *y) 6 { 7 int r1; 8 int r2; 9 10 WRITE_ONCE(*x, 1); 11 r1 READ_ONCE(*x); 12 r2 READ_ONCE(*y); 13 } 14 15 P1(int *x, int *y) 16 { 17 int r3; 18 int r4; 19 20 WRITE_ONCE(*y, 1); 21 r3 READ_ONCE(*y); 22 r4 READ_ONCE(*x); 23 } 24 25 exists (0:r20 /\ 1:r40)herd7 输出1 Test SBrfionceonce-poonceonces Allowed 2 States 4 3 0:r20; 1:r40; 4 0:r20; 1:r41; 5 0:r21; 1:r40; 6 0:r21; 1:r41; 7 Ok 8 Witnesses 9 Positive: 1 Negative: 3 10 Condition exists (0:r20 /\ 1:r40) 11 Observation SBrfionceonce-poonceonces Sometimes 1 3 12 Time SBrfionceonce-poonceonces 0.01 13 Hashc7f30fe0faebb7d565405d55b7318ada这个输出说明 CPU 被允许窥探自己的 store buffer除 s390 外的所有 Linux CPU 家族都会欣然这样做。这种窥探导致各 CPU 对其他 CPU 存储顺序的认知不一致但很少引发实际问题。输出只包含exists子句提到的两个变量。如果修改测试时还想知道x、y、0:r1、0:r3的值就在exists前加一行locations子句25 locations [0:r1; 1:r3; x; y] 26 exists (0:r20 /\ 1:r40)于是 herd7 会显示全部变量的值1 Test SBrfionceonce-poonceonces Allowed 2 States 4 3 0:r11; 0:r20; 1:r31; 1:r40; x1; y1; 4 0:r11; 0:r20; 1:r31; 1:r41; x1; y1; 5 0:r11; 0:r21; 1:r31; 1:r40; x1; y1; 6 0:r11; 0:r21; 1:r31; 1:r41; x1; y1; 7 Ok 8 Witnesses 9 Positive: 1 Negative: 3 10 Condition exists (0:r20 /\ 1:r40) 11 Observation SBrfionceonce-poonceonces Sometimes 1 3 12 Time SBrfionceonce-poonceonces 0.01 13 Hash40de8418c4b395388f6501cafd1ed38d若想知道某个全局变量在某进程执行某处的值一个办法是用READ_ONCE()把它加载进新的局部变量再把该局部变量加入locations子句。但要小心在某些测试中多加一个READ_ONCE()会改变结果——原文档特别提示有专门的一对测试用例C-READ_ONCE.litmus与C-READ_ONCE-omitted.litmus位于内核外部的 litmus 示例仓库中可以印证这一点。5.2 模拟自旋循环filter子句herd7 做的是完整状态空间搜索其时间复杂度至少是指数级的。增加进程数、增加每进程代码量都会显著拉长运行时间而等待锁的潜在无限循环则更加棘手。幸运的是可以用专门的建模技巧避免状态空间爆炸。下面的测试用xchg_acquire()模拟加锁但不把xchg_acquire()包进自旋循环而是用 herd7 的filter子句剔除那些未成功获取锁的执行。注意对于互斥锁直接使用 LKMM 原生建模的spin_lock()/spin_unlock()是更好的选择至少它们快得多但本节的技术可用于其他目的比如 LKMM 尚未建模的读写锁。1 C C-SBl-o-o-ul-o-o-u-X 2 3 { 4 } 5 6 P0(int *sl, int *x0, int *x1) 7 { 8 int r2; 9 int r1; 10 11 r2 xchg_acquire(sl, 1); 12 WRITE_ONCE(*x0, 1); 13 r1 READ_ONCE(*x1); 14 smp_store_release(sl, 0); 15 } 16 17 P1(int *sl, int *x0, int *x1) 18 { 19 int r2; 20 int r1; 21 22 r2 xchg_acquire(sl, 1); 23 WRITE_ONCE(*x1, 1); 24 r1 READ_ONCE(*x0); 25 smp_store_release(sl, 0); 26 } 27 28 filter (0:r20 /\ 1:r20) 29 exists (0:r10 /\ 1:r10)测试逻辑两个全局变量x1、x2源码中为x0/x1外加模拟的全局自旋锁sl——把sl从 0 改成 1 的进程持有锁改回 0 即释放。xchg_acquire()无条件向sl存 1并把旧值0 或 1存入r2分别对应加锁成功或失败。代码看似两种情况下都会进入临界区第 12-13 行第 28 行的filter子句负责兜底它保留其表达式为真的执行即只保留0:r2和1:r2都为 0两个锁都真正获取到的执行把那些假想地进入临界区的执行连同其副作用一并丢弃。请务必记住filter子句说的是保留什么而不是丢弃什么。运行结果1 Test C-SBl-o-o-ul-o-o-u-X Allowed 2 States 2 3 0:r10; 1:r11; 4 0:r11; 1:r10; 5 No 6 Witnesses 7 Positive: 0 Negative: 2 8 Condition exists (0:r10 /\ 1:r10) 9 Observation C-SBl-o-o-ul-o-o-u-X Never 0 2 10 Time C-SBl-o-o-ul-o-o-u-X 0.03第 9 行的Never表明这种xchg_acquire()smp_store_release()组合确实正确模拟了互斥锁。为什么不直接像内核那样用自旋循环处理加锁失败关键洞见是在无死锁的程序中自旋循环对exists子句可能出现的终态没有任何影响。给定高质量的加锁原语、无死锁程序与高质量硬件每次加锁最终都会成功而 herd7 本就在穷举所有可能的执行时长获取锁花多久并不重要。为什么不把filter表达式并进exists子句那样也能工作但更慢在常见情形下herd7 一旦发现filter表达式失败就可以立即放弃该执行而exists只在时间尽头全部执行结束后才评估herd7 会浪费时间在两个临界区并发执行的假想执行上。此外一些 LKMM 用户也喜欢filter与exists分工带来的关注点分离。filter的评估时机冷门但值得知道如果把修改后的测试中临时把0:r2置为非零会不会让 herd7 因filter提前不匹配而提前放弃执行直接看这个变体第 4 行引入初始化为 1 的全局x2第 23 行将其读入1:r2制造与filter的早期不匹配第 24 行用必然成立的if避免 herd7 的静态分析第 32 行把exists改为必然成立的条件1 C C-SBl-o-o-ul-o-o-u-X 2 3 { 4 x21; 5 } 6 7 P0(int *sl, int *x0, int *x1) 8 { 9 int r2; 10 int r1; 11 12 r2 xchg_acquire(sl, 1); 13 WRITE_ONCE(*x0, 1); 14 r1 READ_ONCE(*x1); 15 smp_store_release(sl, 0); 16 } 17 18 P1(int *sl, int *x0, int *x1, int *x2) 19 { 20 int r2; 21 int r1; 22 23 r2 READ_ONCE(*x2); 24 if (r2) 25 r2 xchg_acquire(sl, 1); 26 WRITE_ONCE(*x1, 1); 27 r1 READ_ONCE(*x0); 28 smp_store_release(sl, 0); 29 } 30 31 filter (0:r20 /\ 1:r20) 32 exists (x11)如果filter在每次赋值时都检查那么所有执行都会在第 23 行之后被过滤掉输出将没有任何执行。实际输出却是1 Test C-SBl-o-o-ul-o-o-u-X Allowed 2 States 1 3 x11; 4 Ok 5 Witnesses 6 Positive: 2 Negative: 0 7 Condition exists (x11) 8 Observation C-SBl-o-o-ul-o-o-u-X Always 2 0 9 Time C-SBl-o-o-ul-o-o-u-X 0.04 10 Hash080bc508da7f291e122c6de76c0088e3第 3 行显示有一个执行没被过滤掉——即filter子句只在其检查的变量最后一次赋值时评估。由于本例filter是析取disjunction它可能评估两次一次在0:r2的最后也是唯一一次赋值处一次在1:r2的最后赋值处。5.3 链表仅支持纯指针节点LKMM 可以处理链表但仅限于每个节点除了指向下一节点的指针外别无内容的链表。这个限制当然很严格但即便如此仍有不少可做参见 tools/memory-model/litmus-tests/MPonceassignderefonce.litmus1 C MPonceassignderefonce 2 3 { 4 yz; 5 z0; 6 } 7 8 P0(int *x, int **y) 9 { 10 WRITE_ONCE(*x, 1); 11 rcu_assign_pointer(*y, x); 12 } 13 14 P1(int *x, int **y) 15 { 16 int *r0; 17 int r1; 18 19 rcu_read_lock(); 20 r0 rcu_dereference(*y); 21 r1 READ_ONCE(*r0); 22 rcu_read_unlock(); 23 } 24 25 exists (1:r0x /\ 1:r10)第 4 行yz乍看奇怪——此时z还没初始化。但yz并不是把z的值赋给y而是把z的地址赋给y。于是第 4、5 行构造了一条简单链表y指向zz是 NULL 指针。想建更长的链表完全可以甚至可以建和操作单向循环链表。exists子句同理1:r0x比较的不是x的值而是其地址检验第 20 行从y加载的指针是否看到了第 11 行存储的值。P0第 10 行先把x置 1第 11 行再把x链入y顶替z。P1第 20 行从y加载指针、第 21 行解引用它第 19-22 行的 RCU 读侧临界区在此示例中纯粹是装饰性的。注意第 21 行加载的地址取决于本例中恰好等于第 20 行加载的值——这是一个地址依赖address dependency从第 20 行的加载延伸到第 21 行的加载它提供了一种弱形式的排序保证。运行结果1 Test MPonceassignderefonce Allowed 2 States 2 3 1:r0x; 1:r11; 4 1:r0z; 1:r10; 5 No 6 Witnesses 7 Positive: 0 Negative: 2 8 Condition exists (1:r0x /\ 1:r10) 9 Observation MPonceassignderefonce Never 0 2 10 Time MPonceassignderefonce 0.00 11 Hash49ef7a741563570102448a256a0c8568可能的结果只有两种要么P1加载到指向z内容为 0的指针要么加载到指向x内容为 1的指针。这令人安心RCU 读者访问新插入的链表节点时不会看到初始化之前的旧值——那种P1 加载到x的指针、解引用却拿到初始化前的 0的坏场景正是exists子句标记的目标而 LKMM 判定为Never。5.4 注释C 注释与 OCaml 注释各管一段测试的不同部分由不同解析器处理由此产生一个有趣的后果不同部分要用不同的注释语法。C 语法部分进程代码用 C 注释/* */或//其余部分用 OCaml 注释(* *)。下面的测试标出了每个语法单元对应的注释风格A-L1 C MPonceassignderefonce (* A *) 2 3 (* B *) 4 5 { 6 yz; (* C *) 7 z0; 8 } // D 9 10 // E 11 12 P0(int *x, int **y) // F 13 { 14 WRITE_ONCE(*x, 1); // G 15 rcu_assign_pointer(*y, x); 16 } 17 18 // H 19 20 P1(int *x, int **y) 21 { 22 int *r0; 23 int r1; 24 25 rcu_read_lock(); 26 r0 rcu_dereference(*y); 27 r1 READ_ONCE(*r0); 28 rcu_read_unlock(); 29 } 30 31 // I 32 33 exists (* J *) (1:r0x /\ (* K *) 1:r10) (* L *)一句话总结C 代码里用 C 注释其余部分用 OCaml 注释。若你偏好通篇 C 风格注释C 预处理器是你的朋友。5.5 模拟异步 RCU 宽限期call_rcu()的等价建模Documentation/litmus-tests/rcu/RCUsyncfree.litmus 演示了synchronize_rcu()的语义下面的版本则改造为模拟异步的call_rcu()1 C RCUsyncfree 2 3 { 4 int x 1; 5 int *y x; 6 int z 1; 7 } 8 9 P0(int *x, int *z, int **y) 10 { 11 int *r0; 12 int r1; 13 14 rcu_read_lock(); 15 r0 rcu_dereference(*y); 16 r1 READ_ONCE(*r0); 17 rcu_read_unlock(); 18 } 19 20 P1(int *z, int **y, int *c) 21 { 22 rcu_assign_pointer(*y, z); 23 smp_store_release(*c, 1); // Emulate call_rcu(). 24 } 25 26 P2(int *x, int *z, int **y, int *c) 27 { 28 int r0; 29 30 r0 smp_load_acquire(*c); // Note call_rcu() request. 31 synchronize_rcu(); // Wait one grace period. 32 WRITE_ONCE(*x, 0); // Emulate the RCU callback. 33 } 34 35 filter (2:r01) (* Reject too-early starts. *) 36 exists (0:r0x /\ 0:r10)各进程职责第 4-6 行初始化的链表由y带头初始含xz预先初始化供P1替换x使用。P0第 9-18 行进入 RCU 读侧临界区加载链表头y并解引用节点指针落入0:r0、节点值落入0:r1。P1第 20-24 行把链表头改为指向z然后通过对c做 release 存储来模拟call_rcu()。P2第 27-33 行模拟call_rcu()背后的机制第 30 行 acquire 加载c注意到回调请求第 31 行等待一个宽限期第 32 行模拟 RCU 回调进而模拟kfree()。P2完全可能启动得太早使2:r0为 0 而非要求的 1第 35 行的filter子句正是为此剔除所有2:r0 ! 1的执行。5.6 性能指数复杂度的代价与-speedcheck true完整状态空间探索极其有用但代价是对进程数、每进程平均语句数、测试中存储总数的指数级计算复杂度。最佳实践是从小开始逐步放大尽可能把代码拆成若干小片每片对应一个核心的并发需求。即便如此herd7 仍然很快。原文档记录了一组在普普通通的 x86 笔记本上测得的数据这些是原文档给出的实测数字反映的是当时机型10 进程的 RCU 测试约 6 秒完成全量分析。加上-speedcheck true选项同一测试约 300 毫秒完成提速一个数量级以上。该选项阻止 herd7 生成所有可能的终态只聚焦于exists子句能否被满足。16 进程测试通常需要 15 分钟加-speedcheck true后约 40 秒。公平地说关掉该选项你会额外得到 65535 个状态。19 进程测试不加该选项需 2 小时 40 分钟加上约 8 分钟多小时的运行比短运行多探索不少于 524287 个状态。不习惯命令行参数的话可以加一个与exists子句表达式完全相同的filter子句获得类似的加速。但请注意开发和调试测试期间看到完整状态集往往极其有帮助不要过早牺牲它。六、LKMM 的局限性Linux 内核内存模型LKMM的局限包括以下为原文档的完整清单编译器优化未被精确建模。当然READ_ONCE()/WRITE_ONCE()限制了编译器优化空间但某些情况下编译器仍可能破坏内存模型。更详细的信息见 Documentation/dev-tools/lkmm/docs/explanation.rst特别是 THE PROGRAM ORDER RELATION: po AND po-loc 与 A WARNING 两节。该局限连带限制了 LKMM 对地址、控制、数据依赖的精确建模能力。例如若编译器能推断出某个携带依赖的变量的值就可以用该常量替换从而打断依赖。反过来LKMM 有时也会高估编译器/CPU 能做的重排序从而漏掉一些相当明显的排序。一个简单例子r1 READ_ONCE(x); if (r1 0) smp_mb(); WRITE_ONCE(y, 1);WRITE_ONCE()并不依赖READ_ONCE()因此 LKMM 不主张二者之间有排序。但实际上WRITE_ONCE()不会先于READ_ONCE()执行原因有二其一分支中smp_mb()的存在阻止编译器把WRITE_ONCE()提到if之前编译器必须假定r1有时为 0其二CPU 不会把 store 执行到 po-earlier 的条件分支之前即使该 store 位于分支两臂汇合之后。对 LKMM 来说给出比架构更弱的保证完全没有危险甚至是有利的——这给编译器留出了优化空间。比如若r1为 0 会在别处触发未定义行为聪明的编译器可能推断出if条件中r1永不为 0进而安全地优化掉smp_mb()消除分支与架构本会保证的一切排序。不支持对同一变量的多种访问大小也不支持非对齐或部分重叠访问。不建模异常和中断。某些情况下可以用额外进程模拟中断或异常来绕过。不支持 MMIO、DMA 等 I/O。不支持自修改代码内核的 alternatives 机制、function tracer、BPF JIT 编译器、模块加载器中都有这类代码。原子读改写操作、锁原语和 RCU 的所有变体并未完整建模。例如call_rcu()和rcu_barrier()不受支持。不过 tools/memory-model/linux-kernel.def 显示这些操作已有相当可观的支持度。具体限制a.rcu_assign_pointer()传入 NULL 时内核不提供任何排序而 LKMM 把这种情况建模为 store release。b. unless 类 RMW 操作当前未建模atomic_long_add_unless()、atomic_inc_unless_negative()、atomic_dec_unless_positive()可以用atomic_cmpxchg()模拟。例外是atomic_add_unless()它由 herd7 直接提供可以在测试中直接使用。c.call_rcu()未建模可用额外进程 synchronize_rcu() 回调体 release-acquire 链模拟见 5.5 节。d.rcu_barrier()未建模可以仿照call_rcu()的模拟方式用 release-acquire 从各模拟进程末端连到rcu_barrier()模拟点。e. 读写锁未建模可用原子读改写操作模拟。测试所用的 C 语言片段本身也相当有限、且有些非标准没有自动的 C 预处理可以自己手动跑。除了Pn()进程函数外不能创建其他函数。Pn()的形参必须是指向全局共享变量的指针不能按值传参。只能调用 herd7 内置或 linux-kernel.def 中定义的函数。不支持switch、do、for、while、goto。switch可用if模拟do/for/while往往可手动展开循环模拟必要时请 C 预处理器帮忙减少代码重复部分goto可用if或展开模拟。变量声明可以使用多种类型但herd7 只真正理解 int 和指针类型——不支持浮点、枚举、字符、字符串、数组、结构体。变量声明的解析非常宽松几乎没有类型检查。初始化器与 C 不同初始化器中出现共享变量名时表示指向该变量的指针而非其当前值。例如int x y按int x y解释。不支持动态内存分配某些场景下可用多个静态变量绕过。部分限制未来可能解决其他限制更可能通过把 LKMM 整合进其他工具来应对。最后请记住随着硬件、用例与编译器演化LKMM 本身也在持续变化。七、延伸阅读内核树内的配套文档本指南基于 tools/memory-model/Documentation/litmus-tests.txt由 Documentation/dev-tools/lkmm/docs/litmus-tests.rst 直接引入。围绕它仓库内还有以下文档可构成完整学习路径见 tools/memory-model/Documentation/README 的阅读顺序建议Documentation/dev-tools/lkmm/docs/simple.rst零基础入门 Linux 内核并发Documentation/dev-tools/lkmm/docs/ordering.rst内核提供的底层并发原语总览Documentation/dev-tools/lkmm/docs/locking.rst对锁保护之外共享变量的无锁访问Documentation/dev-tools/lkmm/docs/recipes.rst多线程场景下 LKMM 的直觉式详解Documentation/dev-tools/lkmm/docs/control-dependencies.rst编译器对控制依赖能做什么、不能做什么Documentation/dev-tools/lkmm/docs/glossary.rst 与 cheatsheet.rst术语表与速查表。模型实现本身也值得翻看linux-kernel.cat 以 cat 语言定义了被允许的/被禁止的执行coherence、atomic、happens-before、propagation、rcu 公理linux-kernel.bell 对指令做分类并完成 RCU 读侧临界区嵌套分析lock.cat 则在前端把锁获取/释放关联起来并检查自死锁。配合herd7状态空间穷举与klitmus7转内核模块在硬件上统计验证双工具就构成了 Linux 内核内存模型验证的完整闭环。【免费下载链接】linuxLinux kernel source tree项目地址: https://gitcode.com/GitHub_Trending/li/linux创作声明：本文部分内容由AI辅助生成（AIGC），仅供参考