内核源码里
READ_ONCE、smp_mb()、smp_store_release()
到处都是——它们不是装饰,是
正确性的基石。LKMM(Linux Kernel Memory
Model)是理解这些原语的钥匙。
一、先看图
flowchart TD
CODE[内核并发代码] --> MARKED[Marked Access<br/>READ_ONCE / WRITE_ONCE]
CODE --> BARRIER[显式屏障<br/>smp_mb / smp_rmb / smp_wmb]
CODE --> ACQ_REL[Acquire / Release<br/>smp_load_acquire<br/>smp_store_release]
MARKED --> LKMM[LKMM 语义<br/>herd7 形式化]
BARRIER --> LKMM
ACQ_REL --> LKMM
LKMM --> LITMUS[Litmus Test<br/>验证正确性]
classDef prim fill:#388bfd22,stroke:#388bfd,color:#adbac7;
classDef model fill:#a371f722,stroke:#a371f7,color:#adbac7;
class MARKED,BARRIER,ACQ_REL prim
class CODE,LKMM,LITMUS model
二、为什么需要内存模型
2.1 编译器重排
a = 1;
b = 2;
// 编译器可能先写 b 再写 a2.2 CPU 重排
x86(TSO):store-store 不重排,但 store-load 可以。 ARM/RISC-V(弱序):几乎任意重排。
没有屏障 → 多核并发代码看到乱序 → bug。
三、Marked Access
3.1 READ_ONCE / WRITE_ONCE
int x = READ_ONCE(shared_var); // 防止编译器优化/拆分读
WRITE_ONCE(shared_var, 42); // 防止编译器优化/拆分写不是屏障——只保证单次访问的原子性和不被优化。
3.2 Plain Access
普通 C 读写 → 编译器可能合并、拆分、缓存到寄存器。并发场景 → 未定义行为。
规则:共享变量的并发访问必须用 marked access。
四、屏障原语
| 原语 | 语义 |
|---|---|
smp_mb() |
全屏障:前面的读写都在后面的读写之前 |
smp_rmb() |
读屏障:前面的读在后面的读之前 |
smp_wmb() |
写屏障:前面的写在后面的写之前 |
smp_load_acquire() |
读 + acquire:后续读写不会提前 |
smp_store_release() |
写 + release:之前读写不会延后 |
4.1 Acquire/Release 配对
// CPU 0
WRITE_ONCE(data, 42);
smp_store_release(&flag, 1);
// CPU 1
if (smp_load_acquire(&flag))
assert(READ_ONCE(data) == 42); // 保证成立五、依赖关系
5.1 Address Dependency
int *p = READ_ONCE(ptr);
int val = READ_ONCE(*p); // 地址依赖:p 来自上一行硬件天然保证顺序(所有架构)。
5.2 Data Dependency
int idx = READ_ONCE(index);
WRITE_ONCE(array[idx], 1); // 数据依赖5.3 Control Dependency
int r = READ_ONCE(flag);
if (r)
WRITE_ONCE(data, 1); // 控制依赖控制依赖 + WRITE_ONCE → 提供写后序。但不提供读后序。
六、Cumulativity
屏障的传递性:A 的 release 被 B acquire → B 之后的 release 被 C acquire → A 对 C 可见。
这是多线程通信的核心保证。
七、volatile 的误用
volatile int x; // 不要在内核中用 volatile 做同步volatile 只防编译器优化,不提供 CPU 屏障。内核用
READ_ONCE/WRITE_ONCE 替代。
八、LKMM 形式化
LKMM 用 cat 语言 描述,工具 herd7 执行:
// tools/memory-model/linux-kernel.cat
开发者写 litmus test → herd7 枚举所有可能的执行序 → 判断是否存在违反。
C test
{
int x = 0; int y = 0;
}
P0(int *x, int *y) {
WRITE_ONCE(*x, 1);
smp_wmb();
WRITE_ONCE(*y, 1);
}
P1(int *x, int *y) {
int r0 = READ_ONCE(*y);
smp_rmb();
int r1 = READ_ONCE(*x);
}
exists (1:r0=1 /\ 1:r1=0)
九、观察
# 内核 litmus tests
ls tools/memory-model/litmus-tests/
# 运行 herd7
herd7 -conf linux-kernel.cfg test.litmus
# Documentation
Documentation/memory-barriers.txt
Documentation/litmus-tests/十、小结
- LKMM 定义了内核并发的内存序语义
- READ_ONCE/WRITE_ONCE 是最基本要求
- 屏障和 acquire/release 建立线程间可见性
- litmus test + herd7 可形式化验证正确性
- volatile 不是同步原语
参考文献
tools/memory-model/(LKMM 源码)Documentation/memory-barriers.txt- Paul McKenney, “A formal kernel memory-ordering model.” LWN 2017
- linux/memory-barriers-war-story(旧文延伸阅读)
- linux/access_once(旧文延伸阅读)
工具
- herd7(diy 工具套件)
tools/memory-model/scripts/- klitmus7
延伸阅读
上一篇:异步通知 benchmark 下一篇:原子 RMW
同主题继续阅读
把当前热点继续串成多页阅读,而不是停在单篇消费。
【操作系统百科】内核并发的形式化验证
用 herd7 跑 litmus test、用 CBMC 检查有界模型、用 TLA+ 验证协议——内核并发代码的形式化验证实践。本文讲工具链、实际 bug 案例、与传统测试的权衡。
EEVDF 调度器:Linux 6.6 为什么换掉了 CFS
Linux 6.6 用 EEVDF 取代了 CFS 的 SCHED_NORMAL 选取逻辑。从 1995 年原始论文的 lag、eligibility、virtual deadline,到 commit 147f3ef 只重写 placement/pick/preempt,再到本机内核 6.6 上读 sched/debug 把每个任务的 vruntime、eligible 标志、deadline 一一对上 vd=ve+r/w,外加 nice 带宽与 base_slice 抢占两组实测,讲清换的是哪一块、延迟敏感任务凭什么先跑。
【操作系统百科】Windows 内核与 Linux 的关键差异
NT Executive/Kernel/HAL 分层、Object Manager 与 handle、IRP 驱动栈、IOCP 完成端口 vs epoll/io_uring、EPROCESS/KTHREAD vs task_struct、Registry vs 文件配置,以及 WSL2 为何选择 Hyper-V 轻量 VM。
【操作系统百科】实时 OS 巡礼
硬实时与软实时的可调度性边界、VxWorks/QNX/Zephyr 机制对照、Linux PREEMPT_RT 与主线合入、DO-178C/ISO 26262 认证语境,以及选型决策树。