Fine-Grained Complexity of Safety Verification
- PDF / 580,510 Bytes
- 26 Pages / 439.37 x 666.142 pts Page_size
- 71 Downloads / 212 Views
Fine-Grained Complexity of Safety Verification Peter Chini1 · Roland Meyer1 · Prakash Saivasan1 Received: 19 June 2020 / Accepted: 26 June 2020 © The Author(s) 2020
Abstract We study the fine-grained complexity of Leader Contributor Reachability (LCR) and BoundedStage Reachability (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 (ETH), the problem Set Cover, and crosscompositions. 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 D and the size of the leader L, and (2) by the size of the contributors C. We present algorithms for both cases. The key techniques are compact witnesses and dynamic programming. The algorithms run in O∗ ((L · (D + 1))L·D · DD ) and O∗ (2C ) time, showing that both parameterizations are fixed-parameter tractable. We complement the upper bounds by (matching) lower bounds based on ETH and Set Cover. Moreover, we prove the absence of polynomial kernels. For BSR, we consider programs involving t different threads. We restrict the analysis to computations where the write permission changes s times between the threads. BSR asks whether a given configuration is reachable via such an s-stage computation. When parameterized by P, the maximum size of a thread, and 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 D or the number of stages s to a polynomial dependence on P and t. This indicates that symbolic methods may be harder to find for this problem. Keywords Parameterized verification · Parameterized complexity · Fine-grained complexity · Safety verification
B
Peter Chini [email protected] Roland Meyer [email protected] Prakash Saivasan [email protected]
1
TU Braunschweig, Brunswick, Germany
123
P. Chini et al.
1 Introduction We study the fine-grained complexity of two safety verification problems [1,18,32] for shared memory concurrent programs. The motivation to reconsider these problems are recent developments in fine-grained complexity theory [7,12,35,39]. They suggest that classifications such as NP or even FPT are too coarse to explain the success of verification methods. Instead, it should be possible to identify the precise influence that parameters of the input have on the verification time. Our contribution confirms this idea. We give new verification algorithms for the two problems that, for the first time, can be proven optimal in the sense of fine-grained complexity theory. To state the results, we need some background. As we proceed, we explain the development of fine-grained complexity theory. Ther
Data Loading...
