Software Transactional Memory on Relaxed Memory Models
Software Transactional Memory on Relaxed Memory Models
复制标题
宽松内存模型上的软件事务内存
DOI：
--
复制
发表时间：
2009
期刊：
影响因子：
--
通讯作者：
Vasu Singh
中科院分区：
文献类型：
--
作者：
R. Guerraoui;T. Henzinger;Vasu Singh
STM的伪代码描述假定程序执行顺序一致，并且高级STM操作（如读、写和提交）具有原子性。这些假设在实际设置中经常被违背，因为STM实现运行在宽松的内存模型上，操作的原子性由硬件提供。本文提出了在具有32位加载和存储原子性以及读-修改-写操作的宽松内存模型下验证stm的第一种方法。RML是一种新的高级语言，用于表达具有硬件级指令原子性的并发算法，其语义由各种宽松内存模型参数化。然后，我们介绍了我们的工具FOIL，它将STM算法的RML描述和内存模型的描述作为输入，并自动确定篱笆的位置，如果插入篱笆，则确保给定内存模型下STM算法的正确性。我们使用FOIL在顺序一致性、总存储顺序、部分存储顺序和宽松存储顺序的内存模型下验证DSTM、TL2和McRT STM。
Pseudo-code descriptions of STMs assume sequentially consistent program execution and atomicity of high-level STM operations like read, write, and commit. These assumptions are often violated in realistic settings, as STM implementations run on relaxed memory models, with the atomicity of operations as provided by the hardware. This paper presents the first approach to verify STMs under relaxed memory models with atomicity of 32 bit loads and stores, and read-modify-write operations. We present RML, a new high-level language for expressing concurrent algorithms with a hardware-level atomicity of instructions, and whose semantics is parametrized by various relaxed memory models. We then present our tool, FOIL, which takes as input the RML description of an STM algorithm and the description of a memory model, and automatically determines the locations of fences, which if inserted, ensure the correctness of the STM algorithm under the given memory model. We use FOIL to verify DSTM, TL2, and McRT STM under the memory models of sequential consistency, total store order, partial store order, and relaxed memory order.