Abstract
We study the fine-grained complexity of Leader Contributor Reachability ($${\textsf {LCR}} $$
LCR
) and Bounded-Stage Reachability ($${\textsf {BSR}} $$
BSR
), two variants of the safety verification problem for shared memory concurrent programs. For both problems, the memory is a single variable over a finite data domain. Our contributions are new verification algorithms and lower bounds. The latter are based on the Exponential Time Hypothesis ($${\textsf {ETH}} $$
ETH
), the problem $${\textsf {Set~Cover}} $$
Set
Cover
, and cross-compositions. $${\textsf {LCR}} $$
LCR
is the question whether a designated leader thread can reach an unsafe state when interacting with a certain number of equal contributor threads. We suggest two parameterizations: (1) By the size of the data domain $${\texttt {D}}$$
D
and the size of the leader $${\texttt {L}}$$
L
, and (2) by the size of the contributors $${\texttt {C}}$$
C
. We present algorithms for both cases. The key techniques are compact witnesses and dynamic programming. The algorithms run in $${\mathcal {O}}^*(({\texttt {L}}\cdot ({\texttt {D}}+1))^{{\texttt {L}}\cdot {\texttt {D}}} \cdot {\texttt {D}}^{{\texttt {D}}})$$
O
∗
(
(
L
·
(
D
+
1
)
)
L
·
D
·
D
D
)
and $${\mathcal {O}}^*(2^{{\texttt {C}}})$$
O
∗
(
2
C
)
time, showing that both parameterizations are fixed-parameter tractable. We complement the upper bounds by (matching) lower bounds based on $${\textsf {ETH}} $$
ETH
and $${\textsf {Set~Cover}} $$
Set
Cover
. Moreover, we prove the absence of polynomial kernels. For $${\textsf {BSR}} $$
BSR
, we consider programs involving $${\texttt {t}}$$
t
different threads. We restrict the analysis to computations where the write permission changes $${\texttt {s}}$$
s
times between the threads. $${\textsf {BSR}} $$
BSR
asks whether a given configuration is reachable via such an $${\texttt {s}}$$
s
-stage computation. When parameterized by $${\texttt {P}}$$
P
, the maximum size of a thread, and $${\texttt {t}}$$
t
, the interesting observation is that the problem has a large number of difficult instances. Formally, we show that there is no polynomial kernel, no compression algorithm that reduces the size of the data domain $${\texttt {D}}$$
D
or the number of stages $${\texttt {s}}$$
s
to a polynomial dependence on $${\texttt {P}}$$
P
and $${\texttt {t}}$$
t
. This indicates that symbolic methods may be harder to find for this problem.
Fine-Grained Complexity of Safety Verification
