Update SC.

Author: kneep

content/posts/memory-model/sequential-consistency/index.md

@@ -1,5 +1,5 @@
 +++
-title = '【内存模型】顺序一致性'
+title = '【内存模型】SC'
 series = '内存模型'
 date = '2024-05-10'
 keywords = ['计算机原理', '操作系统', '内存模型', '并发']
@@ -41,6 +41,11 @@ L1: r1 = y;
 S2: y = NEW;
 L2: r2 = x;
 ```
+说明如下：
+- x 和 y 是共享内存中的变量
+- 所有 r 是 CPU 本地变量（寄存器）
+- L 和 S 代表读（Load）和写（Store）
+- x、y 初始值都是 0
 
 另外，我们要约定一些定义和助记符：
 
@@ -63,7 +68,7 @@ L2: r2 = x;
 
 现在我们可以下结论：
 {{< alert "check" >}}
-场景一是符合 SC 的，运行结果是`(r1, r2)` == `(0, NEW)`
+场景一是符合 SC 的，运行结果是`(r1, r2) == (0, NEW)`
 {{< /alert >}}
 
 ### 场景二
@@ -72,7 +77,7 @@ L2: r2 = x;
 我们可以得出类似的结论：
 
 {{< alert "check" >}}
-场景二是符合 SC 的，运行结果是`(r1, r2)` == `(NEW, 0)`
+场景二是符合 SC 的，运行结果是`(r1, r2) == (NEW, 0)`
 {{< /alert >}}
 
 ### 场景三
@@ -81,15 +86,15 @@ L2: r2 = x;
 在这个例子中，在单个处理器上连续的指令，在实际执行的时候发生了交错（`S1`和`L1`之间隔着`S2`，`S2`和`L2`之间隔着`L1`），这在现实场景中很常见，但是如果我们对照 SC 的特性，依然可以得到以下结论：
 
 {{< alert "check" >}}
-场景三是符合 SC 的，运行结果是`(r1, r2)` == `(NEW, NEW)`
+场景三是符合 SC 的，运行结果是`(r1, r2) == (NEW, NEW)`
 {{< /alert >}}
 
 ### 场景四
 最后一个场景的执行如下图：
 ![](img/sc4.svg "场景4")
 这个场景就有点不一样了，因为`S2 <p L2`，但是同时`L2 <m S2`，所以我们可以得出结论：
 {{< alert "xmark" >}}
-场景四是**不符合 SC** 的，运行结果是`(r1, r2)` == `(0, 0)`
+场景四是**不符合 SC** 的，运行结果是`(r1, r2) == (0, 0)`
 {{< /alert >}}
 
 ## 形式化定义
@@ -102,9 +107,9 @@ L2: r2 = x;
   4. 如果 `S(a) <p L(b)`，则 `S(a) <m L(b)`（`Store -> Load`）
 - 针对同一内存地址，读（`Load`）总是能得到 `<m` 中最近一次写（`Store`）的值：
 ```
-          L(a) = Max<m { S(a) | S(a) <m L(a) }
+L(a) = Max<m { S(a) | S(a) <m L(a) }
 ```
-上面公式的意思是，对地址`a`的`Load`，读到的是在`<m`中最新（Max）的一个对`a`进行`Store`的效果。虽然看起来也像一句废话，但是，在缓存的作用下，这个结果并不是理所当然的。
+上面公式的意思是，对地址`a`的`Load`，读到的是在`<m`中最新（Max）的一个对`a`进行`Store`的效果。
 
 此外，这里除了`Load`和`Store`，我们要引入第三种读写指令——`RMW`。`RMW`代表`Read->Modify->Write`，它通常用于这样一种场景：基于内存中某个变量的当前值来更新这个变量，比如把某个变量`++`。通常，做这样的操作，需要三个步骤：
 1. 把内存的值读到寄存器中；