2024/01/18 by Parosh Aziz Abdulla, Abdulla, Parosh Aziz, Mohamed Faouzi Atig +5
Computer Science · #Distributed systems and fault tolerance #FOS: Computer and information sciences #Formal Languages and Automata Theory (cs.FL) #Formal Methods in Verification #Parallel Computing and Optimization Techniques #Programming Languages (cs.PL)
paper · pdf · doi:10.48550/arxiv.2401.10423
openalex publication_date 2024/01/18 · openalex created_date 2025/10/10 · openalex updated_date 2026/07/28
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.