从 SC 到 TSO 的优化可移植性

人们普遍认识到，在并发上下文中编译器优化的安全性面临风险。现有方法主要依赖于上下文无关的线程局部保证，并禁止引入数据竞争的优化。然而，编译器会利用全局的上下文特定信息，从而暴露出可能违反此类保证并引入竞争的安全优化。此类优化需要针对每种语言模型逐一证明其安全性。另一种替代方法是先在直观模型（如交错语义）中证明其安全性，然后确定其在其他并发模型中的可移植性。在本文中，我们解决了跨并发模型移植的问题。我们首先确定了一个关于从顺序一致性（SC）到完全存储定序（TSO）可移植优化的全局保证。我们的保证以约束的形式给出，规定了优化不得引起的语法变更。然后我们证明，这些约束与禁止引入三角竞争（与 TSO 相关的数据竞争的子集）相关联。最后，我们展示了此类引发竞争的优化如何与跨强释放获取（SRA）（一种已知的因果一致内存模型）的移植相关联。