Reasoning about the Implementation of Concurrency Abstractions on x86-TSO
Scott Owens · 2010
Abstract. With the rise of multi-core processors, shared-memory concurrency has become a widespread feature of computation, from hardware, to operating systems, to programming languages such as C++ and Java. However, none of these provide sequentially consistent shared memory; instead they have relaxed memory models, which make concurrent programs even more challenging to understand. Programming languages run atop hardware memory models, so VM and run-time system implementors must reason at both levels. Of particular interest are the low-level implementations of the abstractions that support languagelevel concurrency—especially because they invariably contain data races. In this paper, we develop a novel principle for reasoning about assembly programs on our previous x86-TSO memory model, and we use it to analyze five concurrency abstraction implementations: two spinlocks (from Linux); a non-blocking write protocol; the double-checked locking idiom; and a Parker (from java.util.concurrent). Our principle, called triangular-race freedom, generalizes the usual data-race freedom style of reasoning. 1