Asynchronous Wait-Free Runtime Verification and Enforcement of Linearizability

TL;DR

This paper tackles the problem of runtime verification of linearizability in fully asynchronous wait-free shared-memory systems and proves a general impossibility for direct verification on common objects. It then introduces a predictive verification route through the class DRV by transforming any implementation A into a DRV-compatible A* that produces a sketch of its execution via views, enabling predictive checks using only read/write objects. It further shows that GenLin objects (including linearizability and its generalizations) admit self-enforced implementations that produce verifiable histories, allowing modular design with forensic guarantees. The approach yields a simple, generic methodology for instrumenting concurrent objects to be self-verifiable at runtime without requiring consensus, with broad implications for modular, accountable system design and potential extensions to other correctness conditions and computation models.

Abstract

This paper presents a {theoretical study} of the problem of verifying linearizability at runtime, where one seeks for a concurrent algorithm for verifying that the current execution of a given concurrent shared object implementation is linearizable. It shows that it is impossible to runtime verify linearizability for some common sequential objects, regardless of the consensus power of base objects. Then, it argues that a variant of the problem, which we call predictive verification, can be solved, if linearizability is verified indirectly. Namely, it shows that (1) linearizability of a class of concurrent implementations can be predictively verified using only read/write base objects (i.e. without the need of consensus), and (2) any implementation can be transformed to its counterpart in the class using only read/write objects. As far as we know, this is the first runtime verification algorithm for any correctness condition that is fully asynchronous and fault-tolerant. As a by-product, it is obtained a simple and generic methodology for deriving linearizable implementations that runtime verify their responses, and are able to produce a history certifying this, properties that allows the design of concurrent systems in a modular manner with accountable and forensic guarantees. We call such implementations self-enforced linearizable. The results hold not only for linearizability but for a correctness condition that includes generalizations of it such as set-linearizability and interval-linearizability.

Figures (11)

• Figure 1: Two executions of a stack where the two processes have the same partial views, i.e. sequence of invocations and responses; while the execution at the top is linearizable, the execution at the bottom is not. Real-time, unaccessible to the processes, is what ultimately defines the executions.
• Figure 2: Generic structure of a verifier $\mathcal{V}\xspace_\mathcal{O}\xspace$ for correctness condition ${\sf P}_\mathcal{O}\xspace$ (code of process $p_i$).
• Figure 3: Two 3-process histories of a stack implementations are depicted. Time goes from left to right, and operations are denoted with a double-ended arrows. For clarity, each operation ${\sf Apply}\xspace(\hbox{\sl op})$ is simply denoted $\hbox{\sl op}$. The execution at the top is linearizable with respect to the usual sequential specification of a stack; a linearization of it is: $\sf \langle Push(2): true \rangle \langle Push(1): true \rangle \langle Pop(): 1 \rangle \langle Pop(): 2 \rangle$. The execution at the bottom is not linearizable because the stack cannot be empty when the operation $\sf \langle Pop(): empty \rangle$ starts.
• Figure 5: Due to asynchrony, processes in a verifier might detect histories where operations of $\mathcal{A}\xspace$ are "stretched". This phenomenon is exemplified with two examples of a queue implementation where an operation ${\sf Apply}\xspace(\hbox{\sl op})$ is simply denoted $\hbox{\sl op}$. At the top, both histories, the actual one $E$ and the detected one $E'$, are linearizable. At the bottom, the actual history $E$ is not linearizable, but the detected history $E'$ is linearizable due to a long delay between the event that announces the operation of $\mathcal{A}$ that $p_1$ is going to call next (Line \ref{['L05']}) and the actual moment when the operation is called (Line \ref{['L06']}).
• Figure 6: The operations of any execution $E^*$ of $\mathcal{A}\xspace^*$ might "shrink" in the detected history $E'$. Two executions of $\mathcal{A}\xspace^*$ where $\mathcal{A}\xspace$ is a queue implementation are shown; an operation ${\sf Apply}\xspace(\hbox{\sl op})$ is simply denoted $\hbox{\sl op}$. In the example at the top, the actual history of $\mathcal{A}\xspace^*$ is linearizable but the history detected inside $\mathcal{A}\xspace^*$ is not. In contrast, in the example at the bottom, the actual history of $\mathcal{A}\xspace^*$ is not linearizable, which implies that the detected history is not linearizable either.

Theorems & Definitions (26)

• Definition 3.1: Distributed Runtime Verification
• Definition 4.1: Sequential Specifications
• Definition 4.2: Linearizability
• Theorem 5.1: Impossibility for Distributed Runtime Verification of Linearizability
• Definition 6.1: Distributed Runtime Predictive Verification
• Remark 7.1: Linearizability as abstract objects
• Definition 7.1: Similarity between histories
• Definition 7.2: The class GenLin
• Lemma 7.1: Linearizability is contained in GenLin
• Definition 7.3: The snapshot object AADGMS93