Document Open Access Logo

On the Complexity of Bounded Context Switching

Authors Peter Chini, Jonathan Kolberg, Andreas Krebs, Roland Meyer, Prakash Saivasan

PDF
Thumbnail PDF

File

LIPIcs.ESA.2017.27.pdf
  • Filesize: 0.58 MB
  • 15 pages

Document Identifiers

Author Details

Peter Chini
Jonathan Kolberg
Andreas Krebs
Roland Meyer
Prakash Saivasan

Cite As Get BibTex

Peter Chini, Jonathan Kolberg, Andreas Krebs, Roland Meyer, and Prakash Saivasan. On the Complexity of Bounded Context Switching. In 25th Annual European Symposium on Algorithms (ESA 2017). Leibniz International Proceedings in Informatics (LIPIcs), Volume 87, pp. 27:1-27:15, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2017) https://doi.org/10.4230/LIPIcs.ESA.2017.27

Abstract

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.

Subject Classification

Keywords
  • Shared memory concurrency
  • safety verification
  • fixed-parameter tractability
  • exponential time hypothesis
  • bounded context switching

Metrics

  • Access Statistics
  • Total Accesses (updated on a weekly basis)
    0
    PDF Downloads
    0
    Metadata Views

References

  1. M. F. Atig. Global model checking of ordered multi-pushdown systems. In FSTTCS, volume 8 of LIPIcs, pages 216-227. Schloss Dagstuhl, 2010. Google Scholar
  2. 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. Google Scholar
  3. 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. Google Scholar
  4. 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. Google Scholar
  5. M.F. Atig, A. Bouajjani, and S. Qadeer. Context-bounded analysis for concurrent programs with dynamic creation of threads. LMCS, 7(4), 2011. Google Scholar
  6. 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. Google Scholar
  7. A. Björklund, T. Husfeldt, P. Kaski, and M. Koivisto. Fourier meets Möbius: fast subset convolution. In STOC, pages 67-74. ACM, 2007. Google Scholar
  8. A. Björklund, P. Kaski, and L. Kowalik. Constrained multilinear detection and generalized graph motifs. Algorithmica, 74(2):947-967, 2016. Google Scholar
  9. H. L. Bodlaender, R. G. Downey, M. R. Fellows, and D. Hermelin. On problems without polynomial kernels. JCSS, 75(8):423-434, 2009. Google Scholar
  10. A. Bouajjani, M. Emmi, and G. Parlato. On sequentializing concurrent programs. In SAS, volume 6887 of LNCS, pages 129-145. Springer, 2011. Google Scholar
  11. 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. Google Scholar
  12. J.F. Cantin, M.H. Lipasti, and J.E. Smith. The complexity of verifying memory coherence and consistency. TPDS, 16(7):663-671, 2005. Google Scholar
  13. J. Chen, X. Huang, I. A. Kanj, and G. Xia. Strong computational lower bounds via parameterized complexity. JCSS, 72(8):1346-1367, 2006. Google Scholar
  14. 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.
  15. 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. Google Scholar
  16. M. Cygan, F. V. Fomin, Ł. Kowalik, D. Lokshtanov, D. Marx, M. Pilipczuk, M. Pilipczuk, and S. Saurabh. Parameterized algorithms. Springer, 2015. Google Scholar
  17. 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. Google Scholar
  18. 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. Google Scholar
  19. R. G. Downey and M. R. Fellows. Fundamentals of Parameterized Complexity. Springer, 2013. Google Scholar
  20. 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. Google Scholar
  21. C. Enea and A. Farzan. On atomicity in presence of non-atomic writes. In TACAS, volume 9636 of LNCS, pages 497-514. Springer, 2016. Google Scholar
  22. 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. Google Scholar
  23. J. Esparza, P. Ganty, and T. Poch. Pattern-based verification for multithreaded programs. ACM TOPLAS, 36(3):9:1-9:29, 2014. Google Scholar
  24. A. Farzan and P. Madhusudan. The complexity of predicting atomicity violations. In TACAS, volume 5505 of LNCS, pages 155-169. Springer, 2009. Google Scholar
  25. H. Fernau, P. Heggernes, and Y. Villanger. A multi-parameter analysis of hard problems on deterministic finite automata. JCSS, 81(4):747-765, 2015. Google Scholar
  26. 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. Google Scholar
  27. J. Flum and M. Grohe. Parameterized Complexity Theory. Springer, 2006. Google Scholar
  28. 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. Google Scholar
  29. M. Fortin, A. Muscholl, and I. Walukiewicz. On parametrized verification of asynchronous, shared-memory pushdown systems. CoRR, abs/1606.08707, 2016. Google Scholar
  30. L. Fortnow and R. Santhanam. Infeasibility of instance compression and succinct PCPs for NP. JCSS, 77(1):91-106, 2011. Google Scholar
  31. 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. Google Scholar
  32. M. Fürer. Faster integer multiplication. SICOMP, 39(3):979-1005, 2009. Google Scholar
  33. P. B. Gibbons and E. Korach. Testing shared memories. SICOMP, 26(4):1208-1244, 1997. Google Scholar
  34. M. Hague. Parameterised pushdown systems with non-atomic writes. In FSTTCS, volume 13 of LIPIcs, pages 457-468. Schloss Dagstuhl, 2011. Google Scholar
  35. D. Harvey, J. van der Hoeven, and G. Lecerf. Even faster integer multiplication. Journal of Complexity, 36:1-30, 2016. Google Scholar
  36. R. Impagliazzo and R. Paturi. On the complexity of k-sat. JCSS, 62(2):367-375, 2001. Google Scholar
  37. S. La Torre, P. Madhusudan, and G. Parlato. A robust class of context-sensitive languages. In LICS, pages 161-170. IEEE, 2007. Google Scholar
  38. 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. Google Scholar
  39. 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. Google Scholar
  40. 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. Google Scholar
  41. D. Lokshtanov, D. Marx, and S. Saurabh. Slightly superexponential parameterized problems. In SODA, pages 760-776. SIAM, 2011. Google Scholar
  42. 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. Google Scholar
  43. 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. Google Scholar
  44. D. Marx. Can you beat treewidth? In FOCS, pages 169-179. IEEE, 2007. Google Scholar
  45. D. Marx. Can you beat treewidth? TOC, 6(1):85-112, 2010. Google Scholar
  46. M. Musuvathi and S. Qadeer. Iterative context bounding for systematic testing of multithreaded programs. In PLDI, pages 446-455. ACM, 2007. Google Scholar
  47. 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. Google Scholar
  48. S. Qadeer and J. Rehof. Context-bounded model checking of concurrent software. In TACAS, volume 3440 of LNCS, pages 93-107. Springer, 2005. Google Scholar
  49. 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. Google Scholar
  50. 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. Google Scholar
  51. C. K. Yap. Some consequences of non-uniform conditions on uniform classes. TCS, 26:287-300, 1983. Google Scholar
Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail
© 2023-2024 Schloss Dagstuhl – LZI GmbH About DROPS Imprint Privacy Contact