update memory barrier

Author: cch123

memory_barrier.md

@@ -126,7 +126,7 @@ mesi 协议解决了多核环境下，内存多层级带来的问题。使得 ca
 
 ## CPU 导致乱序
 
-使用 litmus 进行形式化验证:
+使用 litmus 进行验证:
 
 ```
 cat sb.litmus
@@ -181,6 +181,56 @@ Time SB 0.11
 
 在两个核心上运行汇编指令，意料之外的情况 100w 次中出现了 96 次。虽然很少，但确实是客观存在的情况。
 
+有文档提到，x86 体系的内存序本身比较严格，除了 store-load 以外不存在其它类型的重排，也可以用下列脚本验证:
+
+```
+X86 RW
+{ x=0; y=0; }
+ P0          | P1          ;
+ MOV EAX,[y] | MOV EAX,[x] ;
+ MOV [x],$1  | MOV [y],$1  ;
+locations [x;y;]
+exists (0:EAX=1 /\ 1:EAX=1)
+```
+
+```
+%%%%%%%%%%%%%%%%%%%%%%%%%
+% Results for sb.litmus %
+%%%%%%%%%%%%%%%%%%%%%%%%%
+X86 OOO
+
+{x=0; y=0;}
+
+ P0          | P1          ;
+ MOV EAX,[y] | MOV EAX,[x] ;
+ MOV [x],$1  | MOV [y],$1  ;
+
+locations [x; y;]
+exists (0:EAX=1 /\ 1:EAX=1)
+Generated assembler
+	##START _litmus_P0
+	movl	-4(%rsi,%rcx,4), %eax
+	movl	$1, -4(%rbx,%rcx,4)
+	##START _litmus_P1
+	movl	-4(%rbx,%rcx,4), %eax
+	movl	$1, -4(%rsi,%rcx,4)
+
+Test OOO Allowed
+Histogram (2 states)
+500000:>0:EAX=1; 1:EAX=0; x=1; y=1;
+500000:>0:EAX=0; 1:EAX=1; x=1; y=1;
+No
+
+Witnesses
+Positive: 0, Negative: 1000000
+Condition exists (0:EAX=1 /\ 1:EAX=1) is NOT validated
+Hash=7cdd62e8647b817c1615cf8eb9d2117b
+Observation OOO Never 0 1000000
+Time OOO 0.14
+```
+
+无论运行多少次，Positive 应该都是 0。
+
 ## barrier
 
 从功能上来讲，barrier 有四种: