Skip to main content

Weak atomicity under the x86 memory consistency model

Amitabha Roy, Steven Hand, Tim Harris

DOI 10.1145/1941553.1941594 dblp BibTeX

Abstract

We consider the problem of building a weakly atomic Software Transactional Memory (STM), that provides Single (Global) Lock Atomicity (SLA) while adhering to the x86 memory consistency model (x86-MM).

Related papers

Making weak memory models fair OOPSLA 2021
RELINCHE: Automatically Checking Linearizability under Relaxed Memory Consistency POPL 2025
How Hard Is Weak-Memory Testing? POPL 2024
Sequential reasoning for optimizing compilers under weak memory concurrency PLDI 2022
Dartagnan: Bounded Model Checking for Weak Memory Models (Competition Contribution) TACAS 2020
Strong Logic for Weak Memory: Reasoning About Release-Acquire Consistency in Iris ECOOP 2017
On library correctness under weak memory consistency: specifying and verifying concurrent libraries under declarative consistency models POPL 2019
The semantics of x86-CC multiprocessor machine code POPL 2009