\[ \def\po{\mathsf{\textcolor{black}{po}}} \def\poto{\overset{\po}{\longrightarrow}} \def\so{\mathsf{\textcolor{purple}{so}}} \def\soto{\overset{\so}{\longrightarrow}} \def\sfwr{\mathsf{\textcolor{green}{wr}}} \def\wrto{\overset{\sfwr}{\longrightarrow}} \def\ww{\mathsf{\textcolor{orange}{ww}}} \def\wwto{\overset{\ww}{\longrightarrow}} \def\rw{\mathsf{\textcolor{red}{rw}}} \def\rwto{\overset{\rw}{\longrightarrow}} \def\vis{\mathsf{vis}} \def\co{\mathsf{\textcolor{orange}{co}}} \def\coto{\overset{\co}{\longrightarrow}} \def\rf{\mathsf{\textcolor{green}{rf}}} \def\mo{\mathsf{\textcolor{orange}{mo}}} \def\rb{\mathsf{\textcolor{red}{rb}}} \def\sc{\mathsf{\textcolor{purple}{sc}}} \]
摘要
Executions
Events 分为四种：Reads, Writes, Updates, Fences
事件间的关系有：
- \(\po\)：每个线程内的程序顺序，类似 \(\so\)
- \(\rf\)：写-读顺序，类似 \(\sfwr\)
- \(\mo\)：写-写顺序，类似 \(\ww\)
- \(\rb\)：读-写顺序，类似 \(\rw\)
Sequential consistency
the result of any execution is the same as if the operations of all the processors were executed in some sequential order, respecting the order specified by the program
[Lanport 1979]
Lamport 定义
SC 一致性类似数据库隔离级别中的 SER，要求存在一个全序 \(\sc. \po \cup \rf \subseteq \sc\)，且 \(\rf\) 意味着写-读之间没有其他的写。
Alternative 定义
\(\mo_x\) 是变量 \(x\) 上所有写事件的一个全序，类似数据库事务中的 \(\ww_x\) 关系。
\(\rb\) 类似数据库事务中的 \(\rw\) 关系。但上图中对 \(\rb\) 的定义似乎不明晰，应该限定在某个特定的变量上。
SC 的两个定义是等价的。
Coherence
SC 一致性的硬件实现成本太高，也限制了一些对于串行代码有意义的优化。
大多数硬件保证的、编译器保护的一致性是 SC-per-location，也叫 coherence。
定义
Alternative definition I
Alternative definition II
Release/acquire (RA) memory model
定义
Alternative definition
一致性强度
\[ COH < RA < SC \]
Happens-before
TODO：这一页完全看不明白
rlx 和 acq 是什么
C/C++11 memory model
Summary
- 弱）并发语义的声明式方法
- 统一且模块化地处理各种模型、
- 基于“不良模式”的替代公式对 SC（一致性，RA）的重要削弱
- C/C++11 内存模型简介
