3. 内核源码中的 LKMM

3.1 源码位置

linux/tools/memory-model/
|-- linux-kernel.cat      # 核心模型定义（cat 语言）
|-- linux-kernel.bell     # 事件类型分类
|-- linux-kernel.def      # C 语法到 herd7 指令的映射
|-- linux-kernel.cfg      # herd7 配置文件
|-- lock.cat              # 锁语义定义
|-- README                # 使用说明
|-- Documentation/        # 详细文档
|   |-- explanation.txt   # 26 章详细解释（2810 行）
|   |-- litmus-tests.txt  # Litmus test 格式教程
|   |-- simple.txt        # 简明指南
|-- litmus-tests/         # 官方 litmus tests
|-- scripts/              # 测试脚本

3.2 linux-kernel.cat 详解

这是 LKMM 的核心，用 cat 语言（由 Luc Maranget 设计）编写。主要部分：

Coherence（一致性）

let co0 = loc & (W * W)
let co = ...  (* 计算 coherence order *)
let com = co | rf | fr

co 是同一内存位置上所有写操作的全序。com (communication) 是 co、rf、fr 的并集。

Happens-Before（发生先于）

let hb = po | ... | rf | ...

hb 由 program order、各种屏障关系、reads-from 等组合而成。

Propagation（传播）

let pb = ...

pb 确保写操作能够传播到所有 CPU，是处理弱内存模型的关键。

RCU

let rb = ...
irreflexive rb as rcu

rb (RCU-before) 约束 RCU 读临界区和 grace period 的关系。

3.3 linux-kernel.bell 详解

定义了 herd7 需要识别的事件类型：

enum Accesses = 'once | 'acquire | 'release | 'noreturn | 'mb
enum Barriers = 'wmb | 'rmb | 'mb | 'release | 'acquire | ...

3.4 linux-kernel.def 详解

将 C 语言语法映射到 herd7 内部指令：

READ_ONCE(x)          -> R[once] x
WRITE_ONCE(x, v)      -> W[once] x v
smp_load_acquire(&x)   -> R[acquire] x
smp_store_release(&x,v) -> W[release] x v
smp_mb()              -> F[mb]
xchg(&x, v)           -> Rmw[mb] x v
atomic_inc(&x)        -> Rmw[once] x (Add 1)
rcu_read_lock()       -> F[rcu_lock]
rcu_read_unlock()     -> F[rcu_unlock]
synchronize_rcu()     -> F[sync]

3.5 lock.cat 详解

处理锁的获取和释放语义：

let lk-rf = ...  (* 锁的 reads-from 关系 *)
let lk-hb = ...  (* 锁的 happens-before *)

锁操作引入的 happens-before 关系是 LKMM 的重要组成部分。

4. Documentation/ 下的文档详解

内核 tools/memory-model/Documentation/ 目录下包含 13 个文档文件，总计约 7000 行。这些文档按照从入门到精通的顺序组织：

4.1 README — 文档导航

这是整个 Documentation 目录的入口。它不做技术讲解，而是根据读者的背景知识水平，推荐不同的阅读路径：

4.2 simple.txt — 简单并发入门（270 行）

目标读者：对内核并发完全陌生的开发者。

核心内容：

单线程代码

使用库函数

数据锁（Data Locking）

Per-CPU 处理

封装好的无锁原语

  1. Sequence Locking（顺序锁）
    • 简单规则：”不要在读端代码中写”
    • 复杂用法需要 LKMM 指导（LKMM 目前还不直接支持 seqlock，需要在 litmus tests 中手动展开）
  2. RCU
    • 简单规则：”读端不写入”、”不更新读者可见的数据”、”更新用锁保护”
  3. Atomic 操作
    • 三类：初始化/读取（atomic_set/atomic_read）、无返回值无序操作（atomic_inc）、有返回值全序操作（atomic_add_return）
    • 新内核增加了 _relaxed()、_acquire()、_release() 后缀的变体

无锁但全序访问

统计和启发式数据

不要让编译器坑了你

4.3 ordering.txt — 内存排序原语分类（556 行）

目标读者：了解内核并发基础，想看所有低级别排序原语的分类和说明。

核心内容按强度递减组织：

1. Barriers（屏障/栅栏）

2. Ordered Memory Accesses（有序内存访问）

3. Unordered Accesses（无序访问）

4.4 litmus-tests.txt — Litmus Test 格式与技巧（1083 行）

目标读者：熟悉内核并发原语，想写和运行 litmus tests。

核心内容：

Litmus Test 格式

高级特性

性能优化技巧

限制

4.5 locking.txt — 锁与无锁访问（303 行）

目标读者：需要在不持有锁的情况下访问锁保护的共享变量。

核心内容：

锁的基本规则

Double-Checked Locking（DCL）

锁对未持锁 CPU 的排序

No Roach-Motel Locking

4.6 recipes.txt — 常见内存排序模式（574 行）

目标读者：熟悉内核并发，想看实际代码中的常见模式。

核心内容：

Message Passing (MP)

Load Buffering (LB)

Release-Acquire Chains

Store Buffering (SB)

规则总结

4.7 control-dependencies.txt — 控制依赖（258 行）

目标读者：需要使用控制依赖进行排序的开发者。

核心内容：

控制依赖的基本形式

q = READ_ONCE(a);
if (q)
    WRITE_ONCE(b, 1);

关键限制

编译器优化破坏的例子

解决方案

4.8 access-marking.txt — 访问标记指南（624 行）

目标读者：需要标记有意的并发访问，特别是应对 KCSAN 报告的开发者。

核心内容：

访问标记选项

  1. Plain C-language accesses（a = b）
  2. data_race(a = b) — 标记有意数据竞争
  3. READ_ONCE() / WRITE_ONCE() — 阻止编译器优化
  4. __data_racy — 变量属性
  5. ASSERT_EXCLUSIVE_ACCESS() / ASSERT_EXCLUSIVE_WRITER() — KCSAN 断言

何时使用 data_race()

何时使用 Plain C Accesses

KCSAN 的特殊处理

4.9 cheatsheet.txt — 快速参考（35 行）

一个表格，总结了所有内存排序原语对不同类型访问的排序效果。

表格列：Prior Operation（Self, R, W, RMW）和 Subsequent Operation（Self, R, W, DR, DW, RMW, SV）

行：Relaxed store/load/RMW、rcu_dereference()、_acquire()、_release()、smp_rmb()、smp_wmb()、smp_mb()、full RMW、smp_mb__before_atomic()、smp_mb__after_atomic()

标记：C（累积排序）、P（传播）、R（读）、W（写）、Y（提供排序）、a（需要 intervening RMW）

4.10 glossary.txt — 术语表（178 行）

定义了 LKMM 相关术语：

4.11 explanation.txt — LKMM 详细解释（2810 行）

目标读者：熟悉内核并发和 LKMM，想了解模型的设计原理和实现。

这是 Documentation 下最长的文档，共 26 章：

  1. INTRODUCTION: LKMM 简介，目标读者
  2. BACKGROUND: 什么是内存一致性模型，多处理器系统的复杂性
  3. A SIMPLE EXAMPLE: 用设备驱动例子（中断处理程序和 read() 系统调用）引入 MP 模式
  4. A SELECTION OF MEMORY MODELS: Sequential Consistency、TSO、PSO、Weak Ordering 等模型对比
  5. ORDERING AND CYCLES: 排序和循环的概念
  6. EVENTS: LKMM 中的事件类型
  7. THE PROGRAM ORDER RELATION: po 和 po-loc（同一位置的 program order）
  8. A WARNING: 关于编译器优化的警告
  9. DEPENDENCY RELATIONS: data、addr、ctrl 依赖
  10. THE READS-FROM RELATION: rf、rfi（internal）、rfe（external）
  11. CACHE COHERENCE AND THE COHERENCE ORDER RELATION: co、coi、coe
  12. THE FROM-READS RELATION: fr、fri、fre
  13. AN OPERATIONAL MODEL: 操作模型视角
  14. PROPAGATION ORDER RELATION: cumul-fence 和传播
  15. DERIVATION OF THE LKMM FROM THE OPERATIONAL MODEL: 从操作模型推导 LKMM
  16. SEQUENTIAL CONSISTENCY PER VARIABLE: 每个变量的顺序一致性
  17. ATOMIC UPDATES: RMW 操作的原子性
  18. THE PRESERVED PROGRAM ORDER RELATION: ppo（保留的 program order）
  19. AND THEN THERE WAS ALPHA: Alpha 架构的特殊处理
  20. THE HAPPENS-BEFORE RELATION: hb 的详细定义
  21. THE PROPAGATES-BEFORE RELATION: pb 的详细定义
  22. RCU RELATIONS: rcu-link、rcu-gp、rcu-rscsi、rcu-order、rcu-fence、rb
  23. SRCU READ-SIDE CRITICAL SECTIONS: SRCU 的处理
  24. LOCKING: 锁的语义
  25. PLAIN ACCESSES AND DATA RACES: 普通访问和数据竞争
  26. ODDS AND ENDS: 杂项

4.12 herd-representation.txt — Herd7 表示（113 行）

目标读者：想了解内核并发原语在 herd7 中的抽象表示。

解释了 linux-kernel.def 如何将 C 代码映射到 herd7 内部的事件表示。例如：

4.13 references.txt — 参考资料（130 行）

列出了 LKMM 相关的论文、手册、标准委员会工作文件和 LWN 文章。

包括：

5. Litmus Test 详解

5.1 什么是 Litmus Test

Litmus Test 是一种小型并发程序，用于测试内存模型的某个特定属性。它通常包含：

5.2 Litmus Test 格式

C MP+pooncerelease+poacquireonce

(*
 * Result: Never
 *
 * Test that release/acquire prevents reordering.
 *)

{
  int x = 0;
  int y = 0;
}

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:r0=1 /\ 1:r1=0)

格式说明

部分 含义
C MP+... 测试名称
{ ... } 初始化代码
P0(...) / P1(...) 线程 0 / 线程 1
exists (...) 断言：描述 “坏结果”

Result 含义

结果 含义
Never 断言的结果永远不会出现（模型保证）
Sometimes 断言的结果可能出现（允许的行为）
Always 断言的结果总是出现

5.3 断言语法

exists (1:r0=1 /\ 1:r1=0)   (* P1 读到 y=1 但 x=0 *)
forall (1:r0=0 \/ 1:r1=1)   (* 总是满足某个条件 *)

6. 工具链使用指南

6.1 安装 herdtools7

从源码编译安装

# 依赖
git clone https://github.com/herd/herdtools7.git
cd herdtools7

# 需要 OCaml 环境
sudo dnf install opam
eval $(opam env)

# 编译安装
make all
make install

使用 opam 安装（推荐）

opam install herdtools7

验证安装

herd7 --version
klitmus7 --version

6.2 使用 herd7 运行 Litmus Test

基本用法

cd /path/to/kernel/tools/memory-model

# 运行单个测试
herd7 -conf linux-kernel.cfg litmus-tests/MP+pooncerelease+poacquireonce.litmus

# 运行多个测试
herd7 -conf linux-kernel.cfg litmus-tests/*.litmus

输出解读

Test MP+pooncerelease+poacquireonce Allowed
States 3
1:r0=0; 1:r1=0;
1:r0=0; 1:r1=1;
1:r0=1; 1:r1=1;
No
Witnesses
Positive: 0 Negative: 3
Condition exists (1:r0=1 /\ 1:r1=0)
Observation MP+pooncerelease+poacquireonce Never 0 3
Time MP+pooncerelease+poacquireonce 0.01
Hash=...

6.3 使用 klitmus7 生成内核模块

klitmus7 将 litmus test 转换为可在真实硬件上运行的内核模块：

# 生成内核模块
klitmus7 -o /tmp/litmus-test litmus-tests/SB+poonceonces.litmus

# 编译并加载
cd /tmp/litmus-test
make
sudo insmod litmus.ko

# 查看结果
dmesg | tail

6.4 批量测试脚本

内核提供了丰富的测试脚本：

cd tools/memory-model

# 运行所有 litmus tests，检查与预期结果
./scripts/checkalllitmus.sh

# 检查与 GitHub litmus archive 的兼容性
./scripts/checkghlitmus.sh

# 初始化/更新 litmus test 历史记录
./scripts/initlitmushist.sh --timeout 10m --procs 10
./scripts/newlitmushist.sh --timeout 10m --procs 10

# 比较两次运行结果
./scripts/checklitmushist.sh --timeout 10m --procs 10

测试 LKMM 修改的工作流程

# 1. 记录修改前的预期结果（约1小时）
scripts/initlitmushist.sh --timeout 10m --procs 10

# 2. 应用修改
git am -s -3 /path/to/patch

# 3. 快速冒烟测试（秒级）
scripts/checkalllitmus.sh

# 4. 与历史记录对比（约1小时）
scripts/checklitmushist.sh --timeout 10m --procs 10

# 5. 与 GitHub archive 对比（分钟级）
scripts/checkghlitmus.sh --timeout 10m --procs 10

7. 经典 Litmus Test 模式

7.1 MP (Message Passing)

P0:                    P1:
  WRITE_ONCE(x, 1);      r0 = READ_ONCE(y);
  WRITE_ONCE(y, 1);      r1 = READ_ONCE(x);

exists (1:r0=1 /\ 1:r1=0)

问题：P1 看到 y=1 但 x=0（消息未传递）。

无屏障：Sometimes（允许） 加 smp_mb()：Never（阻止） 用 release/acquire：Never（阻止）

7.2 SB (Store Buffering)

P0:                    P1:
  WRITE_ONCE(x, 1);      WRITE_ONCE(y, 1);
  r0 = READ_ONCE(y);     r1 = READ_ONCE(x);

exists (0:r0=0 /\ 1:r1=0)

问题：两个 CPU 都先写后读，但都没看到对方的写。

无屏障：Sometimes（x86 TSO 允许 store buffer） 加 smp_mb()：Never（阻止）

7.3 LB (Load Buffering)

P0:                    P1:
  r0 = READ_ONCE(x);     r1 = READ_ONCE(y);
  WRITE_ONCE(y, 1);      WRITE_ONCE(x, 1);

exists (0:r0=1 /\ 1:r1=1)

问题：两个 CPU 都先读后写，形成循环依赖。

7.4 IRIW (Independent Reads of Independent Writes)

P0:                    P1:                    P2:                    P3:
  WRITE_ONCE(x, 1);      WRITE_ONCE(y, 1);      r0 = READ_ONCE(x);     r2 = READ_ONCE(x);
                                                  r1 = READ_ONCE(y);     r3 = READ_ONCE(y);

exists (0:r0=1 /\ 0:r1=0 /\ 1:r2=0 /\ 1:r3=1)

问题：P2 和 P3 对两个写的观察顺序不一致（非全局一致性）。

x86 TSO：Never（TSO 保证全局一致性） ARM/Power：Sometimes（允许）

7.5 WRC (Write-to-Read Causality)

P0:                    P1:                    P2:
  WRITE_ONCE(x, 1);      r0 = READ_ONCE(x);      r1 = READ_ONCE(y);
                         WRITE_ONCE(y, 1);       r2 = READ_ONCE(x);

exists (1:r0=1 /\ 2:r1=1 /\ 2:r2=0)

问题：P2 通过 P1 间接知道 P0 的写，但没看到 x=1。

本站所有文章转发 CSDN 将按侵权追究法律责任，其它情况随意。