Operational Aspects of C/C++ Concurrency

TL;DR

This paper introduces a comprehensive operational semantics framework for C/C++11 concurrency, capturing various memory models and synchronization primitives, and provides an executable implementation for testing and debugging concurrent programs.

Contribution

It presents the first formal, executable operational semantics for C11 that encompasses all key concurrent features, including relaxed atomics, while avoiding common issues like Out-of-Thin-Air behaviors.

Findings

Successfully models all essential concurrent aspects of C11

Provides an executable semantics in PLT Redex

Demonstrates practical application through a large case study

Abstract

In this work, we present a family of operational semantics that gradually approximates the realistic program behaviors in the C/C++11 memory model. Each semantics in our framework is built by elaborating and combining two simple ingredients: viewfronts and operation buffers. Viewfronts allow us to express the spatial aspect of thread interaction, i.e., which values a thread can read, while operation buffers enable manipulation with the temporal execution aspect, i.e., determining the order in which the results of certain operations can be observed by concurrently running threads. Starting from a simple abstract state machine, through a series of gradual refinements of the abstract state, we capture such language aspects and synchronization primitives as release/acquire atomics, sequentially-consistent and non-atomic memory accesses, also providing a semantics for relaxed atomics, while avoiding the Out-of-Thin-Air problem. To the best of our knowledge, this is the first formal and executable operational semantics of C11 capable of expressing all essential concurrent aspects of the standard. We illustrate our approach via a number of characteristic examples, relating the observed behaviors to those of standard litmus test programs from the literature. We provide an executable implementation of the semantics in PLT Redex, along with a number of implemented litmus tests and examples, and showcase our prototype on a large case study: randomized testing and debugging of a realistic Read-Copy-Update data structure.