2026-08-16T14:53:42Z https://drops.dagstuhl.de/oai

oai:drops-oai.dagstuhl.de:7873 2024-03-06T10:41:18Z ddc:004 open_access

On the Complexity of Bounded Context Switching Chini, Peter Kolberg, Jonathan Krebs, Andreas Meyer, Roland Saivasan, Prakash Shared memory concurrency safety verification fixed-parameter tractability exponential time hypothesis bounded context switching 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. Schloss Dagstuhl – Leibniz-Zentrum für Informatik Peter Chini and Jonathan Kolberg and Andreas Krebs and Roland Meyer and Prakash Saivasan 2017 Is Part Of LIPIcs, Volume 87, 25th Annual European Symposium on Algorithms (ESA 2017) InProceedings Text doc-type:ResearchArticle publishedVersion application/pdf doi:10.4230/LIPIcs.ESA.2017.27 urn:nbn:de:0030-drops-78730 https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ESA.2017.27 eng https://creativecommons.org/licenses/by/3.0/legalcode