企业官网建设流程全解析

Linux 内核内存一致性模型（LKMM）术语完全指南：从地址依赖到 Happens-Before

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

LKMM（Linux-kernel memory consistency model，Linux 内核内存一致性模型）是用cat语言编写、可被herd7模拟器穷举执行的形式化模型，用于预测多 CPU 并发代码中加载指令可能取得的取值。本指南以内核仓库中 tools/memory-model/Documentation/glossary.txt 的术语表为骨架，逐条解析 LKMM 的 13 个核心术语，并对照 linux-kernel.cat、linux-kernel.bell 与 linux-kernel.def 中的形式化定义展开原理级讲解。读完本文，你将能准确理解 RCU 读侧临界区、内存屏障配对、acquire/release 语义等并发原语在模型中的精确含义，并具备阅读 litmus 测试与 LKMM 相关文档的术语基础。

说明：Documentation/dev-tools/lkmm/docs/glossary.rst通过kernel-include指令字面包含本指南的主体来源 glossary.txt；后者又是 Documentation/dev-tools/lkmm/ 文档集的一部分。与大多数术语表一样，它不要求从头读到尾，而是供按需检索具体术语时使用。

依赖类术语：地址依赖、控制依赖与数据依赖

LKMM 把依赖（dependency）区分为三种：地址依赖、控制依赖和数据依赖。它们的共同点是：后续访问的执行或取值以某个先前加载的返回值为基础，从而在事件之间建立一条从加载到后续访问的依赖边（edge）。

地址依赖（Address Dependency）

当某个后续内存访问的地址由先前加载的返回值计算得出时，从该加载到该后续访问之间存在"地址依赖"。地址依赖在 RCU 读侧临界区中非常常见：

1 rcu_read_lock(); 2 p = rcu_dereference(gp); 3 do_something(p->a); 4 rcu_read_unlock();

因为第 3 行p->a的地址由第 2 行rcu_dereference()返回的p计算得出，地址依赖从rcu_dereference()延伸到p->a。在少数情况下，优化编译器可能破坏地址依赖，更多信息见 Documentation/RCU/rcu_dereference.rst。

在形式化模型中，地址依赖对应cat文件里的addr关系。值得注意的是，linux-kernel.bell 对依赖做了"透过普通（plain）访问传递"的增强处理：

let carry-dep = (data ; [~ Srcu-unlock] ; rfi)* let addr = carry-dep ; addr let ctrl = carry-dep ; ctrl let data = carry-dep ; data

也就是说，即使依赖经过一个普通 C 访问再继续传递，模型也会把依赖边延续下去，这是 LKMM 对编译器"依赖销毁"问题的一种保守对抗策略。

控制依赖（Control Dependency）

当后续存储的执行取决于对某个先前加载返回值所做的测试时，从该加载到该存储之间存在"控制依赖"。例如：

1 if (READ_ONCE(x)) 2 WRITE_ONCE(y, 1);

控制依赖从第 1 行的READ_ONCE()延伸到第 2 行的WRITE_ONCE()。控制依赖是脆弱的，很容易被优化编译器破坏——例如编译器可能把第 2 行提前执行、或者把第 1 行的条件判断变换为无法保留依赖关系的等价形式。详细讨论见 control-dependencies.txt，该文档专门讲解如何防止编译器优化破坏控制依赖（如使用barrier()或smp_store_release()等技巧）。

在模型中，控制依赖对应ctrl关系。在 linux-kernel.cat 中，它参与构成"保留的程序顺序"（preserved program order, ppo）：

let rwdep = (dep | ctrl) ; [W]

即dep（地址依赖与数据依赖的并集）或ctrl之后跟一个写事件，构成读写依赖rwdep，进而纳入ppo，参与 happens-before 关系推导。

数据依赖（Data Dependency）

当后续存储所写入的数据由先前加载的返回值计算得出时，从该加载到该存储之间存在"数据依赖"。例如：

1 r1 = READ_ONCE(x); 2 WRITE_ONCE(y, r1 + 1);

数据依赖从第 1 行的READ_ONCE()延伸到第 2 行的WRITE_ONCE()。与地址依赖、控制依赖一样，数据依赖也是脆弱的；而且由于优化编译器会花费大量精力推断整型变量的可能取值，当依赖经由整型变量传递时尤其容易被破坏。

在模型中，数据依赖对应data关系，同样通过dep = addr | data汇入ppo的构建。

Acquire / Release / Relaxed：带标记访问的三种排序强度

Acquire、Release与Relaxed描述的是标记访问（marked access）的排序语义，是 LKMM 中最常用的操作类别。

Acquire（获取）

对于锁而言，Acquire 指获取该锁（例如spin_lock()）。对于非锁的共享变量，Acquire 指包含一个加载、且将该加载排序到同一 CPU 后续内存引用之前的特殊操作。典型例子是smp_load_acquire()，此外atomic_read_acquire()与atomic_xchg_acquire()也包含获取型加载。

Acquire 的核心语义：当获取型加载读到的是某个释放型存储（release store）写入同一变量的值（即该获取加载"从"该释放存储"读取"，英文 reads-from），那么该存储之前的所有操作都"先发生于"（happen before）该加载之后的任何操作。这就是经典的 release-acquire 配对同步。

在 linux-kernel.bell 中可以看到它的形式化起点：

enum Accesses = 'ONCE (*READ_ONCE,WRITE_ONCE*) || 'RELEASE (*smp_store_release*) || 'ACQUIRE (*smp_load_acquire*) || 'NORETURN (* R of non-return RMW *) || 'MB (*xchg(),cmpxchg(),...*)

随后语法标注被过滤为真正具有语义的集合：

let Acquire = ACQUIRE \ W \ FailedRMW let Release = RELEASE \ R \ FailedRMW

即"获取"只对加载有效、"释放"只对存储有效，失败的读-改-写（如失败的cmpxchg()）不计入。在 linux-kernel.cat 中，获取/释放通过acq-po与po-rel参与排序：

let acq-po = [Acquire] ; po ; [M] let po-rel = [M] ; po ; [Release]

Release（释放）

对于锁而言，Release 指释放该锁（例如spin_unlock()）。对于非锁的共享变量，Release 指包含一个存储、且将该存储排序到同一 CPU 先前内存引用之后的特殊操作。典型例子是smp_store_release()，此外atomic_set_release()与atomic_cmpxchg_release()也包含释放型存储。

释放型存储与获取型加载天然配对：一个smp_store_release()与读到它所存值的smp_load_acquire()构成一对。全部相关操作的映射可在 linux-kernel.def 中查到，例如：

smp_store_release(X,V) { __store{RELEASE}(*X,V); } smp_load_acquire(X) __load{ACQUIRE}(*X) atomic_set_release(X,V) { smp_store_release(X,V); } atomic_read_acquire(X) smp_load_acquire(X)

Relaxed（宽松）

Relaxed 指不隐含任何排序的标记访问，例如READ_ONCE()、WRITE_ONCE()、不返回值读-改-写操作，以及名字以_relaxed结尾的返回值读-改-写操作（如atomic_add_return_relaxed()、atomic_fetch_add_relaxed()）。在 linux-kernel.def 中，这些操作被映射为ONCE标记的底层访问，例如：

READ_ONCE(X) __load{ONCE}(X) WRITE_ONCE(X,V) { __store{ONCE}(X,V); } atomic_add_return_relaxed(V,X) __atomic_op_return{ONCE}(X,+,V)

注意：READ_ONCE()/WRITE_ONCE()虽然名为 "ONCE"（保证单次访问、防止编译器合并或撕裂），但不提供跨 CPU 的排序保证，这正是它们属于 Relaxed 类别的原因。

标记访问与未标记访问（Marked / Unmarked Access）

• 标记访问：对变量使用特殊函数或宏的访问，如r1 = READ_ONCE(x)或smp_store_release(&a, 1)。
• 未标记访问：使用普通 C 语言语法对变量的访问，如a = b[2]。

在 linux-kernel.bell 中两者被精确地区分：

let Marked = (~M) | IW | ONCE | RELEASE | ACQUIRE | MB | RMW | LKR | LKW | UL | LF | RL | RU | Srcu-lock | Srcu-unlock let Plain = M \ Marked

Plain（即未标记访问）在 LKMM 中不参与 happens-before 等排序关系，只有受标记访问"界定"后才有意义；模型还在 linux-kernel.cat 中通过data-race标志检测未标记访问构成的数据竞争：

flag ~empty (ww-race | wr-race | rw-race) as contenteditable="false">【免费下载链接】linuxLinux kernel source tree项目地址: https://gitcode.com/GitHub_Trending/li/linux