Guardado en:
| Autores principales: | , , , |
|---|---|
| Formato: | Preprint |
| Publicado: |
2026
|
| Materias: | |
| Acceso en línea: | https://arxiv.org/abs/2605.10625 |
| Etiquetas: |
Agregar Etiqueta
Sin Etiquetas, Sea el primero en etiquetar este registro!
|
| _version_ | 1866914554102939648 |
|---|---|
| author | Govind, R. Krishna, S. Sil, Sanchari Srivathsan, B. |
| author_facet | Govind, R. Krishna, S. Sil, Sanchari Srivathsan, B. |
| contents | 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 π 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 π is not bounded, we show the problem to be W[1]-hard, and hence unlikely to be fixed-parameter-tractable with parameter π. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2605_10625 |
| institution | arXiv |
| publishDate | 2026 |
| record_format | arxiv |
| spellingShingle | Verifying Sequential Consistency under Bounded Preemptions Govind, R. Krishna, S. Sil, Sanchari Srivathsan, B. Programming Languages 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 π 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 π is not bounded, we show the problem to be W[1]-hard, and hence unlikely to be fixed-parameter-tractable with parameter π. |
| title | Verifying Sequential Consistency under Bounded Preemptions |
| topic | Programming Languages |
| url | https://arxiv.org/abs/2605.10625 |