Scenario-Based Proofs for Concurrent Objects [Extended Version]

TL;DR

This work presents a novel proof technique for concurrent objects, based around identifying a small set of scenarios (representative, canonical interleavings), formalized as the commutativity quotient of a concurrent object, and gives an expression language for defining abstractions of the quotient in the form of regular or context-free languages that enable simple proofs of linearizability.

Abstract

Concurrent objects form the foundation of many applications that exploit multicore architectures and their importance has lead to informal correctness arguments, as well as formal proof systems. Correctness arguments (as found in the distributed computing literature) give intuitive descriptions of a few canonical executions or "scenarios" often each with only a few threads, yet it remains unknown as to whether these intuitive arguments have a formal grounding and extend to arbitrary interleavings over unboundedly many threads. We present a novel proof technique for concurrent objects, based around identifying a small set of scenarios (representative, canonical interleavings), formalized as the commutativity quotient of a concurrent object. We next give an expression language for defining abstractions of the quotient in the form of regular or context-free languages that enable simple proofs of linearizability. These quotient expressions organize unbounded interleavings into a form more amenable to reasoning and make explicit the relationship between implementation-level contention/interference and ADT-level transitions. We evaluate our work on numerous non-trivial concurrent objects from the literature (including the Michael-Scott queue, Elimination stack, SLS reservation queue, RDCSS and Herlihy-Wing queue). We show that quotients capture the diverse features/complexities of these algorithms, can be used even when linearization points are not straight-forward, correspond to original authors' correctness arguments, and provide some new scenario-based arguments. Finally, we show that discovery of some object's quotients reduces to two-thread reasoning and give an implementation that can derive candidate quotients expressions from source code.

Figures (12)

• Figure 1: Layer automaton for the Michael/Scott Queue.
• Figure 2: A concurrent counter.
• Figure 3: The steps of an execution with three increment-only threads whose actions are aligned horizontally. For readability, we rename the local variable c in thread $i$ to $\texttt{c}^i$. The curved blue arrows depict data-flow dependencies between reads/writes of ctr.
• Figure 4: An expression representing a quotient of the Counter. For readability we present it as four sub-expressions called "layers" whose composition with regular expression operators (concatenation, union, star) is represented using an automaton (all states are accepting). The full formal definitions of an example layer---from the quotient expression grammar---is given in Example \ref{['ex:layer']}. In this figure, for conciseness, we subscript the primitives to indicate whether they were from increment-vs-decrement. Layer 1 represents decrements acting alone and finding the counter to be 0, Layer 2 corresponds to the first successful increment, Layer 3 and Layer 4 represent successful increments and decrements. For Layers 2 -- 4, some number $x$ of threads begin to read then a single different thread performs its complete write path, and then all $x$ threads fail their CAS instructions. Technically, Layer 2 is a specialization of Layer 3, by letting $m=0$. However, treating them as separate layers provides a more refined representation.
• Figure 5: Layer automaton for the synchronous SLS queue. Layers' acronyms and their definitions are given in the lower half of the figure. States are depicted in dark boxes. For conciseness, layer definitions do not split the prefix/suffix of the read paths.

Theorems & Definitions (25)

• definition 1
• definition 2
• definition 3
• definition 4: Quotient
• theorem 1
• definition 5: Interpretation of an expression
• definition 6: Abstractions of quotients
• definition 7: Basic Layer Expressions
• definition 8
• theorem 2