内存一致性模型深度剖析：从顺序一致到C++11内存排序的完整理论体系

一、为什么需要内存一致性模型

多核系统中每个核心拥有私有L1/L2缓存和写缓冲（Store Buffer、Load Buffer），同一内存位置在不同缓存中存在副本。缓存一致性协议保证单写入者多读取者场景下看到相同值，但Coherence不等于Consistency Model。

一致性协议解决"谁写入最新值可见"的微观问题。一致性模型解决"不同写入以什么顺序可见"的宏观问题。程序员需要的多核原子性保证，实际是顺序一致性（Sequential Consistency）与原子操作的组合保障。

然而，SC在现代多核处理器上代价极高：每次写入必须广播并等待所有核心确认，Store Buffer被禁用，重排优化失效。因此硬件实际提供的是更宽松的模型：x86的TSO、ARM的弱一致性模型、RISC-V的WMO。

二、Lamport的顺序一致性

Lamport 1979年定义：多处理器系统是顺序一致性的，如果任何执行的结果都与所有处理器的操作以某种顺序依次执行的结果相同，且每个处理器的操作按程序顺序出现。

形式化定义：对于任意执行，存在一个全序关系，使得每个线程内的操作保持程序顺序，读操作读到在它之前最近一次写操作的值。SC在结果上与单处理器并发执行等价。

然而SC禁止编译器重排和硬件重排，对现代乱序CPU意味着性能灾难。C++11在设计内存模型时必须在程序员正确性与优化间找到平衡。

三、TSO模型：x86的写缓冲诡计

x86实现引入Store Forwarding形成core-observable的有序错觉：

写操作：每个核心维护FIFO Store Buffer。写入先入Store Buffer即返回，后台异步广播给其他缓存。解决写入延迟问题但引入可见性延迟。

读操作：先检查Store Buffer中的待写项（Store Forwarding），命中则直接返回（即使该值尚未全局可见）。

TSO核心特性：StoreLoad重排允许；StoreStore重排禁止（FIFO保证）；LoadLoad和LoadStore重排禁止。

Dekker算法在TSO上的失败是经典证明：核心1写A=1读B；核心2写B=1读A。两者都读到0是可能的。

四、弱内存模型：ARM与RISC-V

ARMv8和RISC-V采用弱内存模型，理论上允许所有四种重排：

ARM Weakly-Ordered Memory Model：写入"multi-copy atomic"，一个核心的写入对所有其他核心不同步。ARMv8提供DMB/DSB/ISB三类内存屏障。

RISC-V WMO：FENCE指令提供全序关系，PPO算法精确描述保留顺序约束。AMO和LR/SC提供原子性保证。

实际硬件采用MESI一致性广播加Store Buffer加Invalidate Queue架构。写入时的invalidate命令在Queue中延迟处理是"弱"的本质来源。

五、C++11内存模型：六种内存排序

memory_order_relaxed：仅保证原子性，不保证顺序。计数器加法（fetch_add(1, relaxed)）适合纯统计。

memory_order_consume：数据依赖顺序。LLVM实际将consume实现为acquire。

memory_order_acquire：后续读写排在本读之后。开锁后的代码必须看到受保护数据的完整写入。ARM对应DMB ISH。

memory_order_release：前面读写排在本写之前。开锁前的写入必须对acquire者可见。

memory_order_acq_rel：同时具有acquire和release语义。读-改-写操作的默认屏障。

memory_order_seq_cst：全序一致性。所有seq_cst操作在全局总序中可排序。代价最高，每次写入刷新Store Buffer。

六、Compare-Swap与ABA问题

strong vs weak：strong保证不发生伪失败；weak允许伪失败（ARM/RISC-V的LL/SC对缓存行写失效spurious fail）。weak在while循环中更友好。

ABA问题：ptr从A变B再变A，CAS无法感知中间变化。解决方案：Tagged Pointer利用高位存储计数器；Hazard Pointer延迟释放；Epoch-Based Reclamation。

七、Lock-free编程的正确性模式

Michael-Scott Queue：head和tail用atomic管理，节点的next也用atomic。入队CAS tail->next为新节点，CAS tail为新节点。所有CAS用memory_order_acq_rel保证指针和数据写入的可见性。

Seqlock：写入侧解锁加写加解锁顺序保证，读侧读到偶数seq一致后重读。性能优于读写锁在写少读多场景。

八、硬件微架构中的顺序秘密

Invalidate Queue：处理器收到invalidate命令发送ack但不立即删除缓存行，放入Queue等待处理。内存屏障先等待Queue排空。

Store Forwarding：读操作优先检查Store Buffer，命中则绕过Cache Coherence直接返回Store Buffer的值。

九、形式化验证Litmus Tests

Litmus测试用Tiny Assembly描述线程执行轨迹，通过herd7加diy工具集生成所有可能的执行和coherence组合。sb.c（Store Buffering）在ARM上发生但x86-TSO上不发生。内存模型从编译器经验驱动进化到形式化建模加litmus验证的精确科学。

十、RISC-V WMO生态与未来

RISC-V的RVWMO是目前最严格弱内存模型的正式标准。Ztso扩展给RISC-V带来x86类似的TSO保证。LLVM/Rust/C++的一致性验证tooling链正在成熟。Linux kernel的barrier语义在SC-DRF保证下对C++、Java、Go透明。

并发编程从"使用锁保护一切"到"理解底层微架构语义、选择合适memory_order"的进化，是软件工程的正确性革命。