Document Open Access Logo

The Complexity of Bounded Context Switching with Dynamic Thread Creation

Authors Pascal Baumann , Rupak Majumdar , Ramanathan S. Thinniyam , Georg Zetzsche

PDF
Thumbnail PDF

File

LIPIcs.ICALP.2020.111.pdf
  • Filesize: 0.63 MB
  • 16 pages

Document Identifiers

Author Details

Pascal Baumann
  • Max Planck Institute for Software Systems, Kaiserslautern, Germany
Rupak Majumdar
  • Max Planck Institute for Software Systems, Kaiserslautern, Germany
Ramanathan S. Thinniyam
  • Max Planck Institute for Software Systems, Kaiserslautern, Germany
Georg Zetzsche
  • Max Planck Institute for Software Systems, Kaiserslautern, Germany

Funding

This research was funded in part by the Deutsche Forschungsgemeinschaft project 389792660-TRR 248 (see https://perspicuous-computing.science) and by the European Research Council under the Grant Agreement 610150 (ERC Synergy Grant ImPACT).

Acknowledgements

We would like to thank Ranko Lazić, who made us aware of "counter systems with chained counters" from [Stéphane Demri et al., 2013] after submission of this work.

Cite AsGet BibTex

Pascal Baumann, Rupak Majumdar, Ramanathan S. Thinniyam, and Georg Zetzsche. The Complexity of Bounded Context Switching with Dynamic Thread Creation. In 47th International Colloquium on Automata, Languages, and Programming (ICALP 2020). Leibniz International Proceedings in Informatics (LIPIcs), Volume 168, pp. 111:1-111:16, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2020)
https://doi.org/10.4230/LIPIcs.ICALP.2020.111

Abstract

Dynamic networks of concurrent pushdown systems (DCPS) are a theoretical model for multi-threaded recursive programs with shared global state and dynamical creation of threads. The (global) state reachability problem for DCPS is undecidable in general, but Atig et al. (2009) showed that it becomes decidable, and is in 2EXPSPACE, when each thread is restricted to a fixed number of context switches. The best known lower bound for the problem is EXPSPACE-hard and this lower bound follows already when each thread is a finite-state machine and runs atomically to completion (i.e., does not switch contexts). In this paper, we close the gap by showing that state reachability is 2EXPSPACE-hard already with only one context switch. Interestingly, state reachability analysis is in EXPSPACE both for pushdown threads without context switches as well as for finite-state threads with arbitrary context switches. Thus, recursive threads together with a single context switch provide an exponential advantage. Our proof techniques are of independent interest for 2EXPSPACE-hardness results. We introduce transducer-defined Petri nets, a succinct representation for Petri nets, and show coverability is 2EXPSPACE-hard for this model. To show 2EXPSPACE-hardness, we present a modified version of Lipton’s simulation of counter machines by Petri nets, where the net programs can make explicit recursive procedure calls up to a bounded depth.

Subject Classification

ACM Subject Classification
  • Theory of computation → Distributed computing models
  • Theory of computation → Problems, reductions and completeness
Keywords
  • Dynamic thread creation
  • Bounded context switching
  • Asynchronous Programs
  • Safety verification
  • State reachability
  • Petri nets
  • Complexity
  • Succinctness
  • Counter Programs

Metrics

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

References

  1. Mohamed Faouzi Atig, Ahmed Bouajjani, and Shaz Qadeer. Context-bounded analysis for concurrent programs with dynamic creation of threads. In Tools and Algorithms for the Construction and Analysis of Systems, 15th International Conference, TACAS 2009, Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2009, York, UK, March 22-29, 2009. Proceedings, pages 107-123, 2009. Google Scholar
  2. Byron Cook, Daniel Kroening, and Natasha Sharygina. Verification of Boolean programs with unbounded thread creation. Theoretical Computer Science, 388(1-3):227-242, 2007. URL: https://doi.org/10.1016/j.tcs.2007.07.050.
  3. Stéphane Demri, Diego Figueira, and M. Praveen. Reasoning about data repetitions with counter systems. In 28th Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2013, New Orleans, LA, USA, June 25-28, 2013, pages 33-42, 2013. Google Scholar
  4. Emanuele D'Osualdo, Jonathan Kochems, and C.-H. Luke Ong. Automatic verification of Erlang-style concurrency. In Static Analysis - 20th International Symposium, SAS 2013, Seattle, WA, USA, June 20-22, 2013, Proceedings, volume 7935 of Lecture Notes in Computer Science, pages 454-476. Springer, 2013. Google Scholar
  5. Javier Esparza. Decidability and complexity of Petri net problems - an introduction. In G. Rozenberg and W. Reisig, editors, Lectures on Petri Nets I: Basic Models. Advances in Petri Nets, number 1491 in Lecture Notes in Computer Science, pages 374-428, 1998. Google Scholar
  6. Hana Galperin and Avi Wigderson. Succinct representations of graphs. Information and Control, 56(3):183-198, 1983. Google Scholar
  7. Pierre Ganty and Rupak Majumdar. Algorithmic verification of asynchronous programs. ACM Transactions on Programming Languages and Systems (TOPLAS), 34(1):6, 2012. Google Scholar
  8. Alexander Kaiser, Daniel Kroening, and Thomas Wahl. Dynamic cutoff detection in parameterized concurrent programs. In 22nd International Conference on Computer Aided Verification, CAV 2010, Edinburgh, UK, July 15-19, 2010, Proceedings, pages 645-659. Springer, 2010. Google Scholar
  9. Jonathan Kochems. Verification of asynchronous concurrency and the shaped stack constraint. PhD thesis, University of Oxford, UK, 2014. URL: http://ora.ox.ac.uk/objects/uuid:cd487639-0e7f-4248-9405-e05e8a8383d5.
  10. Salvatore La Torre, Parthasarathy Madhusudan, and Gennaro Parlato. The language theory of bounded context-switching. In LATIN 2010: Theoretical Informatics, 9th Latin American Symposium, Oaxaca, Mexico, April 19-23, 2010, Proceedings, volume 6034 of Lecture Notes in Computer Science, pages 96-107. Springer, 2010. Google Scholar
  11. Akash Lal and Thomas W. Reps. Reducing concurrent analysis under a context bound to sequential analysis. Formal Methods in System Design, 35(1):73-97, 2009. URL: https://doi.org/10.1007/s10703-009-0078-9.
  12. Ernst Leiss. Succinct representation of regular languages by Boolean automata. Theoretical Computer Science, 13(3):323-330, 1981. URL: https://doi.org/10.1016/S0304-3975(81)80005-9.
  13. Richard Lipton. The reachability problem is exponential-space hard. Yale University, Department of Computer Science, Report, 62, 1976. Google Scholar
  14. Madanlal Musuvathi and Shaz Qadeer. Iterative context bounding for systematic testing of multithreaded programs. In Proceedings of the ACM SIGPLAN 2007 Conference on Programming Language Design and Implementation, PLDI 2007, San Diego, CA, USA, June 10-13, 2007, pages 446-455. ACM, 2007. Google Scholar
  15. Christos H. Papadimitriou and Mihalis Yannakakis. A note on succinct representations of graphs. Information and Control, 71(3):181-185, 1986. Google Scholar
  16. Shaz Qadeer and Jakob Rehof. Context-bounded model checking of concurrent software. In Tools and Algorithms for the Construction and Analysis of Systems, 11th International Conference, TACAS 2005, Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2005, Edinburgh, UK, April 4-8, 2005, Proceedings, volume 3440 of Lecture Notes in Computer Science, pages 93-107. Springer, 2005. Google Scholar
  17. Charles Rackoff. The covering and boundedness problems for vector addition systems. Theoretical Computer Science, 6(2):223-231, 1978. 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 Imprint Privacy Contact