Verifying Sequential Consistency under Bounded Preemptions

TL;DR

This paper investigates the complexity of verifying sequential consistency in multi-threaded programs under bounded preemptions, revealing a complexity trichotomy based on the number of writers and preemptions.

Contribution

It introduces a complexity classification for the problem under bounded preemptions, including polynomial-time algorithms and hardness results for different program classes.

Findings

Polynomial-time algorithm for single-writer programs.

NP-hardness for two-writer programs.

Conditional lower bound for three-writer programs.

Abstract

Gibbons and Korach studied a fundamental problem in 1997: given an observed sequence of reads and writes of a multi-threaded program, does there exist an interleaving which is sequentially consistent? Apart from applications in testing shared memory implementations, a procedure for this problem is employed in Dynamic Partial-Order-Reduction (DPOR) algorithms. The problem is known to be NP-hard even when different syntactic parameters are kept bounded. In this paper, we consider a restriction on the kind of interleaving required: does there exist a sequentially-consistent interleaving with at most {\pi} preemptions? Empirical evidence suggests that several bugs manifest within a few preemptive switches. This motivates us to investigate the problem under bounded preemptions. Our results exhibit a trichotomy: the problem lends to a polynomial-time algorithm for the class of single-writer programs where for each variable, there is a single thread writing to it; it becomes NP-hard for two-writer programs and finally, for three-writer programs, we get a conditional lower bound under the Exponential-Time-Hypothesis. When the number of preemptions {\pi} is not bounded, we show the problem to be W[1]-hard, and hence unlikely to be fixed-parameter-tractable with parameter {\pi}.