Page 122 - 《软件学报》2024年第6期

2698 软件学报 2024 年第 35 卷第 6 期

该方法在实现中断异常检测的同时消除了不必要的开销.

3.4 内存一致性保证
根据处理器对内存模型的支持情况可以分为 3 类: 顺序性内存模型 (sequentially consistent, SC)、强内存模型
(total store order, TSO) 和弱内存模型 (weak memory order, WMO). 表 4 列出了主流处理器架构在硬件层面对并发
程序中数据访问顺序一致性的保证情况. 可以看出不同处理器硬件对内存模型支持存在很大差异.

表 4 主流处理器硬件对并发程序中存储数据访问顺序一致性保证

RISC-V
执行操作 Alpha ARMv7 POWER x86 AMD64
WMO TSO
读后读 × × × √ × √ √
读后写 × × × √ × √ √
写后写 × × × √ × √ √
写后读 × × × × × × ×
注: 部分旧的x86和AMD处理器采用弱内存模型

表 5 给出了同一并发程序在 TSO 和 WMO 两种不同内存模型的处理器中执行的结果. 假设初始状态为 A=0,
B=0, 在场景 1 中, TSO 模型不允许输出 a=0, b=1, 而 WMO 模型允许. 在场景 2 中, TSO 模型不允许输出 a=0, b=0,
而 WMO 模型允许. 出现不同输出结果的原因是 TSO 模型通过硬件隐式保证访存的时序性, 而 WMO 模型的硬件
并没有进行该操作, 代码执行时访问数据的顺序可以重排.

表 5 程序在 TSO 和 WMO 内存模型的执行结果

场景 线程0 线程1 TSO内存模型输出 WMO内存模型输出
A=1 a=A
场景1 (a=0, b=1) × (a=0, b=1) √
B=1 b=B
A=1 B=1
场景2 (a=0, b=0) × (a=0, b=0) √
b=B a=A

模型的硬件无法保证内存的访问顺序. 如果想要将
TSO 模型通过硬件保证访存的先后顺序, 而 [41] TSO 模
WMO
型的应用迁移到 WMO 模型, 需要额外加入同步栅栏指令来避免指令发生重排序. 然而, 在二进制代码中无论是寻
找待同步点还是添加栅栏指令均会带来较高的性能开销. 针对 TSO-to-WMO 并发程序的翻译, Natarajan 等人 [94]
量化分析了插入同步栅栏指令和基于事务内存一致性处理两种方法带来的性能开销, 发现对于事务冲突较少且事
务足够大的并发程序, 基于事务的内存一致性处理性能较好. 对于事务开销较高的并发程序, 插入内存同步栅栏指
令的效果更好. 然而, 相比于使用单一方法, 两种方法混合使用效果更优.
栅栏指令的插入会显著影响程序执行效率, 选择合适的插入时机就变得极其重要. Chakraborty 等人 [100] 提出
强化弱内存模型变换的鲁棒性, 当发现违反鲁棒性时再插入适当的内存栅栏指令. 文献 [101] 在 Coq 工具上设计
公理化的宽松内存模型实现内存读写操作的局部重排序, 完成从 SC 内存模型向 WMO 内存模型的变换. Lustig 等
人 [102] 提出内存一致性框架 ArMOR, 构建内存顺序约束表以确定 load→load、load→store、store→load 以及
store→store 是否需要保序, 辅助指导翻译程序动态的注入栅栏同步指令. Cota 等人 [15] 证明了插入内存栅栏指令对
保证多核程序访存顺序的有效性. Rocha 等人 提出的 Lasagne 通过构建语句一致性和访存原子约束条件来保证
程序全局访问的内存顺序, 扩展 LLVM IR 并发原语确定内存栅栏指令的插入位置, 实现由强到弱内存模型翻译
的 LIMM (LLVM IR memory model) 并发模型, 之后基于 LIMM 模型实现从 x86 平台到 LLVM IR 再到 ARM 平台
的转换. Lasagne 很好解决了静态翻译在不同内存模型的硬件平台之间正确翻译并发程序难题. QEMU 引入多线
程 MTTCG (multi-threaded TCG) 来支持不同内存一致性模型并发程序的翻译. 最近, Gouicem 等人 [61] 研究发现
QEMU 对并发程序的翻译存在多个翻译错误, 对此, Gouicem 等人提出了名为 Risotto 的并发程序翻译方法.
Risotto 形式化了基于 TCG IR 中间表示的内存模型转换过程, 并使用被形式化的 TCG IR 实现强内存模型到弱内