内存顺序
如「指定原子指令的序」中所述：
每个原子指令都有两个位，aq 和 rl，用于指定其他 RISC-V 硬件线程（harts）所观察到的额外内存序约束。
而顺序约束会对程序执行结果具体产生什么样的影响，可以利用石蕊测试进行可视化的分析。
下面以自旋锁为例，分析添加 aq 和 rl 与否，程序执行有什么样的差异。
获取与释放
ISA03+SIMPLE.litmus 是一个简单的石蕊测试文件，可以从如下仓库处获取：
其完整内容为：
RISCV ISA03+SIMPLE
(* ISA V2.3, Fig 1.3, spinlock, adapt, test mutual exclusion *)
{
0:a0=lock; 0:a5=a;
1:a0=lock; 1:a5=a;
}
P0 | P1 ;
li t0,1 | li t0,1 ;
amoswap.w.aq t0,t0,(a0) | amoswap.w.aq t0,t0,(a0) ;
lw t1,0(a5) | lw t1,0(a5) ;
addi t1,t1,1 | addi t1,t1,1 ;
sw t1,0(a5) | sw t1,0(a5) ;
amoswap.w.rl x0,x0,(a0) | amoswap.w.rl x0,x0,(a0) ;
filter (0:t0=0 /\ 1:t0=0)
forall (a=2)
可以看到其中原子指令含有额外的内存排序约束：aq 和 rl。
使用「兽群」工具模拟内存模型，命令如下：
herd7 -through none -model riscv.cat -show prop \
-doshow addr,data,ctrl,fence,ppo,rf,fr -showevents mem -showinitwrites false \
-showthread true -squished true -graph columns -fixedsize false \
-fontname "SF Mono" -fontsize 14 -edgefontsizedelta 0 -penwidth 2 \
-arrowsize 1 -splines spline -pad 0.0 -showlegend true -showkind true \
-yscale 1.5 -xscale 5 -extrachars 0 -edgemerge true \
-o tests/non-mixed-size/HAND tests/non-mixed-size/HAND/ISA03+SIMPLE.litmus
其执行结果为：
Test ISA03+SIMPLE Required
States 1
[a]=2;
Ok
Witnesses
Positive: 2 Negative: 0
Condition forall ([a]=2)
Observation ISA03+SIMPLE Always 2 0
Time ISA03+SIMPLE 0.20
Hash=277646d28ce797552d4c6351515fb0f7
同时会生成一个 dot 文件：ISA03+SIMPLE.dot。
使用工具将其转换为可预览的 svg 文件，命令如下：
neato "-Gfontname=SF Pro Display" "-Nfontname=SF Pro Display" \
"-Efontname=SF Pro Display" \
-Tsvg:cairo tests/non-mixed-size/HAND/ISA03+SIMPLE.dot \
-o tests/non-mixed-size/HAND/ISA03+SIMPLE.svg
herd7 依据执行结果，生成的 dot 文件一般会包含多个图形，可以先进行切分，然后再利用 neato 转换每一个图形文件。
生成的可视化图形：
| Edge | Full Name (and explanation) |
|---|---|
| rf | Reads From (from each store to the loads that return a value written by that store) |
| co | Coherence (a total order on the stores to each address) |
| fr | From-Reads (from each load to co-successors of the store from which the load returned a value) |
| ppo | Preserved Program Order |
| fence | Orderings enforced by a FENCE instruction |
| addr | Address Dependency |
| ctrl | Control Dependency |
| data | Data Dependency |
绘制的石蕊测试图表的图例
边的全称（和解释）：
- rf：读自关系（从每个储存到返回该储存所写值的载入）
- co：一致性（对每个地址上储存的全序关系）
- fr：从读关系（从每个载入到载入返回值的储存的 co 后继）
- ppo：保留程序序
- fence：FENCE 指令强制的序关系
- addr：地址依赖
- ctrl：控制依赖
- data：数据依赖
在列出的关系中，硬件线程间的 rf 边、co 边、fr 边和 ppo 边直接约束全局内存序（fence、addr、data 和一些 ctrl 边也通过 ppo 来约束）。其他边（如硬件线程内的 rf 边）是信息性的，但不约束全局内存序。
可以看到图中 a,b c,d e,f g,h 4 组节点之间的边均含有 ppo 约束。
保留程序序（Preserved Program Order）表示必须在全局内存序中被遵守的程序序的子集。从概念上讲，来自同一硬件线程且由保留程序序排序的事件必须从其他硬件线程和/或观察者的角度以该顺序出现。另一方面，来自同一硬件线程但未由保留程序序排序的事件可能从其他硬件线程和/或观察者的角度看起来被重排序。
也就是说，程序只会按 a→b c→d e→f g→h 的顺序执行，结合其他的 ppo 以及其他约束。变量 a 的最终结果只能为 2。
宽松顺序
ISA03+SIMPLE+BIS.litmus 测试去除了 aq 和 rl，可以从如下仓库处获取：
其完整内容为：
RISCV ISA03+SIMPLE+BIS
(* ISA V2.3, Fig 1.3, spinlock, adapt, test mutual exclusion,
with relaxed swaps *)
{
0:a0=lock; 0:a5=a;
1:a0=lock; 1:a5=a;
}
P0 | P1 ;
li t0,1 | li t0,1 ;
amoswap.w t0,t0,(a0) | amoswap.w t0,t0,(a0) ;
lw t1,0(a5) | lw t1,0(a5) ;
addi t1,t1,1 | addi t1,t1,1 ;
sw t1,0(a5) | sw t1,0(a5) ;
amoswap.w x0,x0,(a0) | amoswap.w x0,x0,(a0) ;
filter (0:t0=0 /\ 1:t0=0)
exists ~(a = 2)
其执行结果为：
Test ISA03+SIMPLE+BIS Allowed
States 2
[a]=1;
[a]=2;
Ok
Witnesses
Positive: 4 Negative: 4
Condition exists (not ([a]=2))
Observation ISA03+SIMPLE+BIS Sometimes 4 4
Time ISA03+SIMPLE+BIS 0.20
Hash=01bf4938d5b4cdab1bd650dfc7a4fdf4
同样生成可视化图形：
可以看到图中 a,b c,d e,f g,h 4 组节点之间的边均无 ppo 约束，也就是说他们的顺序在其他线程看来可以发生改变。
最终结果 a 可能为 1 或 2。
任意无关
ISA03.litmus
RISCV ISA03
(* ISA V2.3, Fig 1.3, spinlock, adapt *)
{
uint64_t x;
uint64_t y;
uint64_t z;
uint64_t t;
0:a1=x; 0:a2=y; 0:a3=z; 0:a4=t; 0:a0=lock; 0:a5=a;
1:a1=x; 1:a2=y; 1:a3=z; 1:a4=t; 1:a0=lock; 1:a5=a;
}
P0 | P1 ;
li t1,1 | ;
sd t1,0(a1) | ;
ld t2,0(a2) | ;
li t0,1 | li t0,1 ;
amoswap.w.aq t0,t0,(a0) | amoswap.w.aq t0,t0,(a0) ;
lw t1,0(a5) | lw t1,0(a5) ;
addi t1,t1,1 | addi t1,t1,1 ;
sw t1,0(a5) | sw t1,0(a5) ;
li t3,1 | li t1,1 ;
sd t3,0(a3) | sd t1,0(a2) ;
ld t4,0(a4) | ld t2,0(a1) ;
amoswap.w.rl x0,x0,(a0) | amoswap.w.rl x0,x0,(a0) ;
| li t3,1 ;
| sd t3,0(a4) ;
| ld t4,0(a3) ;
locations [a;]
filter (0:t0=0 /\ 1:t0=0)
exists (0:t2=0 /\ 1:t2=0) /\ (0:t4=0 /\ 1:t4=0)
Test ISA03 Allowed
States 16
0:x7=0; 0:x29=0; 1:x7=0; 1:x29=0; [a]=2;
0:x7=0; 0:x29=0; 1:x7=0; 1:x29=1; [a]=2;
0:x7=0; 0:x29=0; 1:x7=1; 1:x29=0; [a]=2;
0:x7=0; 0:x29=0; 1:x7=1; 1:x29=1; [a]=2;
0:x7=0; 0:x29=1; 1:x7=0; 1:x29=0; [a]=2;
0:x7=0; 0:x29=1; 1:x7=0; 1:x29=1; [a]=2;
0:x7=0; 0:x29=1; 1:x7=1; 1:x29=0; [a]=2;
0:x7=0; 0:x29=1; 1:x7=1; 1:x29=1; [a]=2;
0:x7=1; 0:x29=0; 1:x7=0; 1:x29=0; [a]=2;
0:x7=1; 0:x29=0; 1:x7=0; 1:x29=1; [a]=2;
0:x7=1; 0:x29=0; 1:x7=1; 1:x29=0; [a]=2;
0:x7=1; 0:x29=0; 1:x7=1; 1:x29=1; [a]=2;
0:x7=1; 0:x29=1; 1:x7=0; 1:x29=0; [a]=2;
0:x7=1; 0:x29=1; 1:x7=0; 1:x29=1; [a]=2;
0:x7=1; 0:x29=1; 1:x7=1; 1:x29=0; [a]=2;
0:x7=1; 0:x29=1; 1:x7=1; 1:x29=1; [a]=2;
Ok
Witnesses
Positive: 1 Negative: 16
Condition exists (0:x7=0 /\ 1:x7=0 /\ 0:x29=0 /\ 1:x29=0)
Observation ISA03 Sometimes 1 16
Time ISA03 9.29
Hash=b6d3059467f1537d63dd512ee7686023
由于此示例使用 aq，临界区中的载入和储存保证在全局内存序中出现在用于获取锁的 AMOSWAP 之后。然而，假设 a0、a1 和 a2 指向不同的内存位置，临界区中的载入和储存在全局内存序中可能会也可能不会出现在示例开头的「任意无关载入」之后。
释放语义序的工作方式与获取语义序完全相同，只是方向相反。释放语义要求在程序序中先于释放语义操作的所有载入和储存也在全局内存序中先于释放语义操作。 使用相同的示例，临界区中的载入和储存与代码片段末尾的「任意无关储存」之间的序仅由 FENCE RW,W 强制执行，而不是由 rl 强制执行。