Verification under TSO with an infinite Data Domain

TL;DR

This paper studies safety verification for concurrent programs under Total Store Ordering (TSO) when data domains are infinite. It shows that control-state reachability is undecidable in general via a reduction from Lossy Channel Systems with Data (DLCS), motivating the use of context-bounded analysis as a tractable under-approximation. The authors develop a two-step abstraction, AB$(\mathsf{Prog},k)$ to handle unbounded buffers and a domain abstraction using relational information to collapse the infinite data domain, establishing that CB($k$)-Reach[$\mathtt{D}$, $\mathsf{Rl}_{\leq n}$] is PSPACE-complete. This work delineates the boundary between undecidability and practical decidability for verifying weak-memory concurrent programs with unbounded data, and outlines future directions for broader under-approximations and more expressive relations.

Abstract

We examine verification of concurrent programs under the total store ordering (TSO) semantics used by the x86 architecture. In our model, threads manipulate variables over infinite domains and they can check whether variables are related for a range of relations. We show that, in general, the control state reachability problem is undecidable. This result is derived through a reduction from the state reachability problem of lossy channel systems with data (which is known to be undecidable). In the light of this undecidability, we turn our attention to a more tractable variant of the reachability problem. Specifically, we study context bounded runs, which provide an under-approximation of the program behavior by limiting the possible interactions between processes. A run consists of a number of contexts, with each context representing a sequence of steps where a only single designated thread is active. We prove that the control state reachability problem under bounded context switching is PSPACE complete.

Figures (5)

• Figure 1: The transition relation of TSO. We assume that $\mathsf{St}(t)=q$.
• Figure 2: The transition relation of DLCS
• Figure 3: $\mathsf{Prog}(\mathcal{L})$ with threads $t$ (pink states) and $t_{\mathsf{ch}}$ (yellow states).
• Figure 4: The transition relation $\Delta_{\mathtt{AB}}$ of $\mathtt{AB}(\mathsf{Prog},k )$. Let $\delta=\langle q_a, op, q_b \rangle\in \Delta_{t}$ and $q_\mathtt{AB}=(\mathsf{St},act,j,c,u)$ with $\mathsf{St}(t)=q_a$ and $act(j)=t$.
• Figure 5: The transition relation of $\mathsf{Rl}_{<}{-}\mathtt{AB}(\mathsf{Prog},k )$. Sets $\mathsf{Rl}$ and $\mathsf{Rl}'$ satisfy (i) equality is an equivalence relation; (ii) disequality holds iff equality does not hold; (iii) $"<"$ is a total order on variables that are not equal.

Theorems & Definitions (14)

• theorem thmcountertheorem
• theorem thmcountertheorem: 10.1145/2933575.2934535
• lemma thmcounterlemma
• theorem thmcountertheorem
• lemma thmcounterlemma
• lemma thmcounterlemma
• proof
• lemma thmcounterlemma
• theorem thmcountertheorem
• proof