On the Complexity of 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.
Shared memory concurrency
safety verification
fixed-parameter tractability
exponential time hypothesis
bounded context switching
27:1-27:15
Regular Paper
Peter
Chini
Peter Chini
Jonathan
Kolberg
Jonathan Kolberg
Andreas
Krebs
Andreas Krebs
Roland
Meyer
Roland Meyer
Prakash
Saivasan
Prakash Saivasan
10.4230/LIPIcs.ESA.2017.27
M. F. Atig. Global model checking of ordered multi-pushdown systems. In FSTTCS, volume 8 of LIPIcs, pages 216-227. Schloss Dagstuhl, 2010.
M. F. Atig, A. Bouajjani, K. N. Kumar, and P. Saivasan. On bounded reachability analysis of shared memory systems. In FSTTCS, volume 29 of LIPIcs, pages 611-623. Schloss Dagstuhl, 2014.
M. F. Atig, A. Bouajjani, and T. Touili. Analyzing asynchronous programs with preemption. In FSTTCS, volume 2 of LIPIcs, pages 37-48. Schloss Dagstuhl, 2008.
M. F. Atig, A. Bouajjani, and T. Touili. On the reachability analysis of acyclic networks of pushdown systems. In CONCUR, volume 5201 of LNCS, pages 356-371. Springer, 2008.
M.F. Atig, A. Bouajjani, and S. Qadeer. Context-bounded analysis for concurrent programs with dynamic creation of threads. LMCS, 7(4), 2011.
J. Barnat, L. Brim, I. Cerná, P. Moravec, P. Rockai, and O. Simecek. Divine - A tool for distributed verification. In CAV, volume 4144 of LNCS, pages 278-281. Springer, 2006.
A. Björklund, T. Husfeldt, P. Kaski, and M. Koivisto. Fourier meets Möbius: fast subset convolution. In STOC, pages 67-74. ACM, 2007.
A. Björklund, P. Kaski, and L. Kowalik. Constrained multilinear detection and generalized graph motifs. Algorithmica, 74(2):947-967, 2016.
H. L. Bodlaender, R. G. Downey, M. R. Fellows, and D. Hermelin. On problems without polynomial kernels. JCSS, 75(8):423-434, 2009.
A. Bouajjani, M. Emmi, and G. Parlato. On sequentializing concurrent programs. In SAS, volume 6887 of LNCS, pages 129-145. Springer, 2011.
C. Calabro, R. Impagliazzo, and R. Paturi. The complexity of satisfiability of small depth circuits. In IWPEC, volume 5917 of LNCS, pages 75-85. Springer, 2009.
J.F. Cantin, M.H. Lipasti, and J.E. Smith. The complexity of verifying memory coherence and consistency. TPDS, 16(7):663-671, 2005.
J. Chen, X. Huang, I. A. Kanj, and G. Xia. Strong computational lower bounds via parameterized complexity. JCSS, 72(8):1346-1367, 2006.
P. Chini, J. Kolberg, A. Krebs, R. Meyer, and P. Saivasan. On the complexity of bounded context switching. CoRR, abs/1609.09728, 2017. URL: https://arxiv.org/abs/1609.09728.
https://arxiv.org/abs/1609.09728
M. Cygan, H. Dell, D. Lokshtanov, D. Marx, J. Nederlof, Y. Okamoto, R. Paturi, S. Saurabh, and M. Wahlström. On problems as hard as CNF-SAT. ACM TALG, 12(3):41:1-41:24, 2016.
M. Cygan, F. V. Fomin, Ł. Kowalik, D. Lokshtanov, D. Marx, M. Pilipczuk, M. Pilipczuk, and S. Saurabh. Parameterized algorithms. Springer, 2015.
M. Cygan, J. Nederlof, M. Pilipczuk, M. Pilipczuk, J. M. M. van Rooij, and J. O. Wojtaszczyk. Solving connectivity problems parameterized by treewidth in single exponential time. In FOCS, pages 150-159. IEEE, 2011.
S. Demri, F. Laroussinie, and P. Schnoebelen. A parametric analysis of the state explosion problem in model checking. In STACS, volume 2285 of LNCS, pages 620-631. Springer, 2002.
R. G. Downey and M. R. Fellows. Fundamentals of Parameterized Complexity. Springer, 2013.
A. Durand-Gasselin, J. Esparza, P. Ganty, and R. Majumdar. Model checking parameterized asynchronous shared-memory systems. In CAV, volume 9206 of LNCS, pages 67-84. Springer, 2015.
C. Enea and A. Farzan. On atomicity in presence of non-atomic writes. In TACAS, volume 9636 of LNCS, pages 497-514. Springer, 2016.
J. Esparza, P. Ganty, and R. Majumdar. Parameterized verification of asynchronous shared-memory systems. In CAV, volume 8044 of LNCS, pages 124-140. Springer, 2013.
J. Esparza, P. Ganty, and T. Poch. Pattern-based verification for multithreaded programs. ACM TOPLAS, 36(3):9:1-9:29, 2014.
A. Farzan and P. Madhusudan. The complexity of predicting atomicity violations. In TACAS, volume 5505 of LNCS, pages 155-169. Springer, 2009.
H. Fernau, P. Heggernes, and Y. Villanger. A multi-parameter analysis of hard problems on deterministic finite automata. JCSS, 81(4):747-765, 2015.
H. Fernau and A. Krebs. Problems on finite automata and the exponential time hypothesis. In CIAA, volume 9705 of LNCS, pages 89-100. Springer, 2016.
J. Flum and M. Grohe. Parameterized Complexity Theory. Springer, 2006.
F. V. Fomin, D. Kratsch, and G. J. Woeginger. Exact (exponential) algorithms for the dominating set problem. In WG, volume 3353 of LNCS, pages 245-256. Springer, 2004.
M. Fortin, A. Muscholl, and I. Walukiewicz. On parametrized verification of asynchronous, shared-memory pushdown systems. CoRR, abs/1606.08707, 2016.
L. Fortnow and R. Santhanam. Infeasibility of instance compression and succinct PCPs for NP. JCSS, 77(1):91-106, 2011.
F. Furbach, R. Meyer, K. Schneider, and M. Senftleben. Memory-model-aware testing: A unified complexity analysis. ACM TECS, 14(4):63:1-63:25, 2015.
M. Fürer. Faster integer multiplication. SICOMP, 39(3):979-1005, 2009.
P. B. Gibbons and E. Korach. Testing shared memories. SICOMP, 26(4):1208-1244, 1997.
M. Hague. Parameterised pushdown systems with non-atomic writes. In FSTTCS, volume 13 of LIPIcs, pages 457-468. Schloss Dagstuhl, 2011.
D. Harvey, J. van der Hoeven, and G. Lecerf. Even faster integer multiplication. Journal of Complexity, 36:1-30, 2016.
R. Impagliazzo and R. Paturi. On the complexity of k-sat. JCSS, 62(2):367-375, 2001.
S. La Torre, P. Madhusudan, and G. Parlato. A robust class of context-sensitive languages. In LICS, pages 161-170. IEEE, 2007.
S. La Torre, P. Madhusudan, and G. Parlato. Model-checking parameterized concurrent programs using linear interfaces. In CAV, volume 6174 of LNCS, pages 629-644. Springer, 2010.
S. La Torre and M. Napoli. Reachability of multistack pushdown systems with scope-bounded matching relations. In CONCUR, volume 6901 of LNCS, pages 203-218. Springer, 2011.
A. Lal and T. W. Reps. Reducing concurrent analysis under a context bound to sequential analysis. In CAV, volume 5123 of LNCS, pages 37-51. Springer, 2008.
D. Lokshtanov, D. Marx, and S. Saurabh. Slightly superexponential parameterized problems. In SODA, pages 760-776. SIAM, 2011.
D. Lokshtanov, N. Misra, and S. Saurabh. Kernelization - preprocessing with a guarantee. In The Multivariate Algorithmic Revolution and Beyond - Essays Dedicated to Michael R. Fellows on the Occasion of His 60th Birthday, volume 7370 of LNCS, pages 129-161. Springer, 2012.
S. Lu, S. Park, E. Seo, and Y. Zhou. Learning from mistakes: A comprehensive study on real world concurrency bug characteristics. In ASPLOS, pages 329-339. ACM, 2008.
D. Marx. Can you beat treewidth? In FOCS, pages 169-179. IEEE, 2007.
D. Marx. Can you beat treewidth? TOC, 6(1):85-112, 2010.
M. Musuvathi and S. Qadeer. Iterative context bounding for systematic testing of multithreaded programs. In PLDI, pages 446-455. ACM, 2007.
H. Ponce de León, F. Furbach, K. Heljanko, and R. Meyer. Portability analysis for axiomatic memory models. PORTHOS: one tool for all models. To appear at SAS, 2017.
S. Qadeer and J. Rehof. Context-bounded model checking of concurrent software. In TACAS, volume 3440 of LNCS, pages 93-107. Springer, 2005.
J. M. M. van Rooij, H. L. Bodlaender, and P. Rossmanith. Dynamic programming on tree decompositions using generalised fast subset convolution. In ESA, volume 5757 of LNCS, pages 566-577. Springer, 2009.
T. Wareham. The parameterized complexity of intersection and composition operations on sets of finite-state automata. In CIAA, volume 2088 of LNCS, pages 302-310. Springer, 2000.
C. K. Yap. Some consequences of non-uniform conditions on uniform classes. TCS, 26:287-300, 1983.
Creative Commons Attribution 3.0 Unported license
https://creativecommons.org/licenses/by/3.0/legalcode