License: Creative Commons Attribution 3.0 Unported license (CC BY 3.0)
When quoting this document, please refer to the following
DOI: 10.4230/LIPIcs.ICALP.2020.111
URN: urn:nbn:de:0030-drops-125187
URL: http://dagstuhl.sunsite.rwth-aachen.de/volltexte/2020/12518/
Go to the corresponding LIPIcs Volume Portal

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

The Complexity of Bounded Context Switching with Dynamic Thread Creation

pdf-format:
LIPIcs-ICALP-2020-111.pdf (0.6 MB)

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.

BibTeX - Entry

@InProceedings{baumann_et_al:LIPIcs:2020:12518,
  author =	{Pascal Baumann and Rupak Majumdar and Ramanathan S. Thinniyam and Georg Zetzsche},
  title =	{{The Complexity of Bounded Context Switching with Dynamic Thread Creation}},
  booktitle =	{47th International Colloquium on Automata, Languages, and Programming (ICALP 2020)},
  pages =	{111:1--111:16},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-138-2},
  ISSN =	{1868-8969},
  year =	{2020},
  volume =	{168},
  editor =	{Artur Czumaj and Anuj Dawar and Emanuela Merelli},
  publisher =	{Schloss Dagstuhl--Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/opus/volltexte/2020/12518},
  URN =		{urn:nbn:de:0030-drops-125187},
  doi =		{10.4230/LIPIcs.ICALP.2020.111},
  annote =	{Keywords: Dynamic thread creation, Bounded context switching, Asynchronous Programs, Safety verification, State reachability, Petri nets, Complexity, Succinctness, Counter Programs}
}

Keywords: Dynamic thread creation, Bounded context switching, Asynchronous Programs, Safety verification, State reachability, Petri nets, Complexity, Succinctness, Counter Programs
Collection: 47th International Colloquium on Automata, Languages, and Programming (ICALP 2020)
Issue Date: 2020
Date of publication: 29.06.2020

DROPS-Home | Fulltext Search | Imprint | Privacy Published by LZI