土法炼钢兴趣小组的算法知识备份

【操作系统百科】Linux 内核内存模型

文章导航

分类入口
os
标签入口
#lkmm#memory-model#memory-barrier#read-once#litmus-test

目录

内核源码里 READ_ONCEsmp_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 再写 a

2.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/

十、小结


参考文献

工具


延伸阅读


上一篇异步通知 benchmark 下一篇原子 RMW

同主题继续阅读

把当前热点继续串成多页阅读,而不是停在单篇消费。

2026-06-02 · os

【操作系统百科】内核并发的形式化验证

用 herd7 跑 litmus test、用 CBMC 检查有界模型、用 TLA+ 验证协议——内核并发代码的形式化验证实践。本文讲工具链、实际 bug 案例、与传统测试的权衡。

2026-05-06 · os

【操作系统百科】内核内存调试

内核内存 bug 是最难追的:UAF、OOB、double free、leak 都可能沉默数月。本文讲 KASAN 三种模式、KFENCE 生产采样、kmemleak、SLUB_DEBUG、UBSAN/KCSAN 联动。

2026-05-08 · os

【操作系统百科】VFS 四层抽象

Linux 的一切皆文件靠 VFS 实现——superblock、inode、dentry、file 四层抽象加 ops 表。本文讲 VFS 核心数据结构、dcache、inode cache、RCU lookup,以及文件系统如何插入 VFS。

2026-04-22 · os

操作系统百科

Linux 6.x 视角下的操作系统系列索引:110 篇覆盖调度、虚拟内存、文件系统与 I/O、并发、隔离、可观测性,按主题、阅读路径与关键问题三种入口组织。


By .