Bounded context switching (BCS) is an under-approximate method for finding violations to safety properties in shared-memory concurrent programs. Technically, BCS is a reachability problem that is known to be NP-complete. Our contribution is a parameterized analysis of BCS. The first result is an algorithm that solves BCS when parameterized by the number of context switches (cs) and the size of the memory (m) in O*(m^(cs)2^(cs)). This is achieved by creating instances of the easier problem Shuff which we solve via fast subset convolution. We also present a lower bound for BCS of the form m^o(cs / log(cs)), based on the exponential time hypothesis. Interestingly, the gap is closely related to a conjecture that has been open since FOCS'07. Further, we prove that BCS admits no polynomial kernel. Next, we introduce a measure, called scheduling dimension, that captures the complexity of schedules. We study BCS parameterized by the scheduling dimension (sdim) and show that it can be solved in O*((2m)^(4sdim)4^t), where t is the number of threads. We consider variants of the problem for which we obtain (matching) upper and lower bounds.
@InProceedings{chini_et_al:LIPIcs.ESA.2017.27, author = {Chini, Peter and Kolberg, Jonathan and Krebs, Andreas and Meyer, Roland and Saivasan, Prakash}, title = {{On the Complexity of Bounded Context Switching}}, booktitle = {25th Annual European Symposium on Algorithms (ESA 2017)}, pages = {27:1--27:15}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-049-1}, ISSN = {1868-8969}, year = {2017}, volume = {87}, editor = {Pruhs, Kirk and Sohler, Christian}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ESA.2017.27}, URN = {urn:nbn:de:0030-drops-78730}, doi = {10.4230/LIPIcs.ESA.2017.27}, annote = {Keywords: Shared memory concurrency, safety verification, fixed-parameter tractability, exponential time hypothesis, bounded context switching} }
Feedback for Dagstuhl Publishing