This is the second in a two-part post from Arm Principal Researcher Dr Nathan Chong on his joint research with Tyler Sorensen (Imperial College London) and Dr John Wickerson (Research Fellow, Imperial College London), and published as a PLDI 2018 Distinguished Paper: "The Semantics of Transactions and Weak Memory in x86, Power, Arm, and C++". You can read the first part of the blog here.
Effective programmers need clear mental models of how their programs will behave because mismatches between programmer intent and actual program behavior are potential bugs. This need is even greater in the face of concurrency since a concurrent program can have many behaviors due to subtle interactions between multiple components. Our work offers formal semantics that clarify the behavior of concurrent programs using transactions and weak memory for several architectures; and hence, gives programmers clearer models for using these features together.
Transactions and weak memory are potential features of the concurrency model of a computer's architecture: the foundational contract between hardware and software. A transaction is a sequence of program instructions guaranteed to behave like a single indivisible instruction, similar to a transaction in a database. Weak memory (or memory consistency) is the specification that governs the ordering requirements of load and store instructions, which may differ from the order specified by the programmer.
"Weak memory models provide a complex, system-centric semantics for concurrent programs, while transactional memory (TM) provides a simpler, programmer-centric semantics. Both have been studied in detail, but their combined semantics is not well understood. This is problematic because such widely-used architectures and languages as x86, Power, and C++ all support TM, and all have weak memory models."
Our formal semantics, in axiomatic style, precisely capture the interaction of transactions and weak memory for x86, Power, Arm, and C++. In contrast to informal semantics, such as prose documentation, formal semantics are amenable to automated reasoning: we can make the computer an ally that can aid and amplify our understanding. The tools we developed can:
Formal semantics and automated reasoning are powerful lenses for viewing this problem: they helped us discover several ambiguities and unexpected interactions, including a counterexample for lock elision (Rajwar and Goodman, MICRO 2001) that has been lying dormant, waiting to be discovered, for 17 years. The details are in the paper and my talk.
At a high-level, the purpose of a semantics is to rigorously define what program behaviors are allowed or disallowed. In the case of weak memory, this involves defining how threads interact with shared memory by accounting for the relaxed ordering between loads and stores. Or, more simply, to determine the possible values that each load instruction of a program can observe.
In an axiomatic style semantics, a program's possible behaviors are captured as a set of candidate executions. An execution represents a single, complete run of the program as a graph structure: the nodes are memory events, such as reads, writes and fences; and the labelled directed edges are ordering relations, such as program order and coherence. The set of candidate executions is constructed to be an over-approximation of the program's behaviors (Section 2 of our paper). An axiomatic memory model is a set of constraints, such as acyclicity, that determine whether a given candidate execution is consistent or inconsistent (Alglave et al., TOPLAS 2014). In other words, we apply the constraints as a filter on the set of candidate executions. The remaining set of consistent executions, which satisfy the constraints, are the allowed behaviors of the program.
Hence, to formalize transactions in this setting, we need a representation of a transaction in an execution. We introduce a partial equivalence relation (i.e., symmetric and transitive) to bind together memory events of the same, successfully committed, transaction. In our paper, we call this relation stxn (Section 3.1 of our paper). Intuitively, the memory events joined by stxn are indivisible because a committed transaction is atomic. We formalize this intuition by lifting relations over events, to transactions (Section 3.3 of our paper). This enables us to express constraints over transactions as well as over individual memory events and is a key first step to capturing the semantics of transactions in x86, Power, Arm, and C++.
In summary, our work provides clearer models for programmers using transactions and weak memory in concurrent programs. Using formal semantics we can tame the complexity of these two features, use automated tooling to amplify our reasoning about their interactions, and uncover surprising results and counterexamples.
This work was presented at the ACM SIGPLAN Conference on Programming Language Design and Implementation and awarded a 'Distinguished Paper Award'. Our paper is released under a Creative Commons Attribution-ShareAlike 4.0 International (CC BY-SA 4.0).
Use the links below to download the full paper, "The Semantics of Transactions and Weak Memory in x86, Power, Arm, and C++", to watch my PLDI presentation, or to view my talk slides.
Read the full paper Watch the talk Read the talk slides .