Arm Community
Arm Community
  • Site
  • User
  • Site
  • Search
  • User
  • Groups
    • Arm Research
    • DesignStart
    • Education Hub
    • Innovation
    • Open Source Software and Platforms
  • Forums
    • AI and ML forum
    • Architectures and Processors forum
    • Arm Development Platforms forum
    • Arm Development Studio forum
    • Arm Virtual Hardware forum
    • Automotive forum
    • Compilers and Libraries forum
    • Graphics, Gaming, and VR forum
    • High Performance Computing (HPC) forum
    • Infrastructure Solutions forum
    • Internet of Things (IoT) forum
    • Keil forum
    • Morello Forum
    • Operating Systems forum
    • SoC Design and Simulation forum
    • 中文社区论区
  • Blogs
    • AI and ML blog
    • Announcements
    • Architectures and Processors blog
    • Automotive blog
    • Graphics, Gaming, and VR blog
    • High Performance Computing (HPC) blog
    • Infrastructure Solutions blog
    • Innovation blog
    • Internet of Things (IoT) blog
    • Mobile blog
    • Operating Systems blog
    • Research Articles
    • SoC Design and Simulation blog
    • Smart Homes
    • Tools, Software and IDEs blog
    • Works on Arm blog
    • 中文社区博客
  • Support
    • Open a support case
    • Documentation
    • Downloads
    • Training
    • Arm Approved program
    • Arm Design Reviews
  • Community Help
  • More
  • Cancel
Arm Research
Arm Research
Research Articles The Semantics of Transactions and Weak Memory in x86, Power, Arm, and C++
  • Research Articles
  • Leaderboard
  • Resources
  • Arm Research Events
  • Members
  • Mentions
  • Sub-Groups
  • Tags
  • Jump...
  • Cancel
Arm Research requires membership for participation - click to join
More blogs in Arm Research
  • Research Articles

Tags
  • Arm Research
  • Architecture
  • Security
  • Memory
  • Computer Architecture
Actions
  • RSS
  • More
  • Cancel
Related blog posts
Related forum threads

The Semantics of Transactions and Weak Memory in x86, Power, Arm, and C++

Nathan Chong
Nathan Chong
July 16, 2018

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.

Clarifying Concurrent Programs

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 Results

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:

  • Discover and generate tests to empirically validate the fidelity of our formal models; and
  • Perform bounded verification of metatheoretical properties, such as the sound compilation of C++ transactions

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.

Formalizing Transactions Axiomatically

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++.

Summary

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).

Find out more

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 .

Anonymous
Research Articles
  • How about a short walk?

    Ilias Vougioukas
    Ilias Vougioukas
    Current solutions to improve virtual to physical translation performance are impractical. We present an alternative, where a small change has a significant impact.
    • March 10, 2022
  • SpiNNaker: Next-level thinking

    Charlotte Christopherson
    Charlotte Christopherson
    SpiNNaker1 connected a million mobile phone processors, operating in some ways like a brain. SpiNNaker2 will drive the next generation of AI.
    • January 31, 2022
  • Sparking potential for community development: Arm Education Kits now available on GitHub

    Dipesh Patel
    Dipesh Patel
    University Program materials are now even easier to access via GitHub. Use our resources, tools and more to spark the potential of your students.
    • January 24, 2022