https://research.swtch.com/hwmm
顺序一致性
要求遵守这一一致性的处理器的 任意一种实际执行 都满足等价于 所有处理器按照一个全局顺序执行，并且每个处理器中的操作按照其程序指定的顺序出现在该序列
共享内存可以一次服务一个线程的读取或写入请求
Litmus Test
测试模型是否允许特定的执行。结果只有两种，可能或不可能
很难做出完全通用的陈述来比较不同的内存模型。相反，专注于特定的测试案例，如果两个内存模型对给定的测试允许不同的行为，这证明它们是不同的
Litmus Test: Message Passing
Can this program seer1=1,r2=0?
// Thread 1 // Thread 2
x = 1 r1 = y
y = 1 r2 = x
On sequentially consistent hardware: no.
On x86 (or other TSO): no.
Litmus Test: Write Queue (also called Store Buffer)
Can this program seer1=0,r2=0?
// Thread 1 // Thread 2
x = 1 y = 1
r1 = y r2 = x
On sequentially consistent hardware: no.
On x86 (or other TSO):yes!
为了修复这一点，可以使用内存屏障，保证在读取之前将本地（？）写入刷新到共享内存
Litmus Test: Independent Reads of Independent Writes (IRIW)
Can this program seer1=1,r2=0,r3=1,r4=0?
(Can Threads 3 and 4 seexandychange in different orders?)
// Thread 1 // Thread 2 // Thread 3 // Thread 4
x = 1 y = 1 r1 = x r3 = y
r2 = y r4 = x
On sequentially consistent hardware: no.
On x86 (or other TSO): no.
Litmus Test: Coherence
Can this program seer1=1,r2=2,r3=2,r4=1?
(Can Thread 3 seex=1beforex=2while Thread 4 sees the reverse?)
// Thread 1 // Thread 2 // Thread 3 // Thread 4
x = 1 x = 2 r1 = x r3 = x
r2 = x r4 = x
On sequentially consistent hardware: no.
On x86 (or other TSO): no.
On ARM/POWER: no.
In any modern compiled language using ordinary variables: yes!
x86 TSO
处理器将写入加入到本地写队列，然后继续执行新指令
处理器读时会先考虑本地写队列，再考虑共享内存。其他处理器的写队列不可见
所有处理器都同意 写入到达共享内存的（总）顺序
Relaxed Memory Model
系统中的线程必须就写入单个内存位置的总顺序达成一致
Weak Ordering and Data-Race-Free Sequential Consistency
硬件的这些内存模型细节太复杂了，我们更喜欢一些简单的规则，通过遵守这些规则来保证顺序一致
weak order
用 同步模型 来约束内存访问
is weakly ordered by DRF
同步操作
结果：如果软件避免了数据竞争，那么硬件就好像它是顺序一致的一样
https://research.swtch.com/plmm
编程语言的内存模型回答了并行程序可以依赖哪些行为来共享线程之间的内存
原子操作，同步原子
利用同步指令创建happens-before关系
现代语言采用DRF-SC
编译器允许重排序，只要这种重排序不会改变单线程代码的执行被观察的结果，这导致了编译程序的内存模型可以被认为比relaxed更弱（如连贯性测试 yes）
java内存模型
所有锁、解锁和 volatile 变量访问的行为有全局顺序，这个全局顺序定义了subsequent的含义
同步操作
线程的创建发生在线程的第一个动作之前。
互斥量 m 的解锁发生在任何subsequent锁定 m 之前。
一个对易失性变量 v 的写操作发生在任何subsequent读操作 v 之前。
也就是说，subsequent进一步定义了happens-before关系。通过检查happens-before，我们可以进一步确定有没有数据竞争
竞态程序的语义
java内存模型仍有一些疑点（？）