x86、Power、ARM 和 C++ 中事务与弱内存的语义
编程语言
2018-04-18 v2 分布式、并行与集群计算
摘要
弱内存模型为并发程序提供了以系统为中心的复杂语义，而事务内存 提供了以程序员为中心的更简单的语义。两者都已被详细研究，但它们的组合语义尚不清楚。这是有问题的，因为像 x86、Power 和 C++ 这样广泛使用的架构和语言都支持 TM，并且都有弱内存模型。我们的工作旨在通过用 TM 的新规则扩展现有的公理化弱内存模型（x86、Power、ARMv8 和 C++）来阐明弱内存与 TM 之间的相互作用。我们的形式化模型由自动化工具支持，该工具能够 (1) 合成测试以针对现有实现验证我们的模型，以及 (2) 对与 TM 相关的转换（如锁省略和将 C++ 事务编译为硬件）进行模型检查。一个关键发现是，ARM Research 目前正在考虑的向 ARMv8 提出的 TM 扩展在不牺牲可移植性或性能的情况下与锁省略不兼容。
引用
@article{arxiv.1710.04839,
title = {The Semantics of Transactions and Weak Memory in x86, Power, ARM, and C++},
author = {Nathan Chong and Tyler Sorensen and John Wickerson},
journal= {arXiv preprint arXiv:1710.04839},
year = {2018}
}