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.ESA.2017.27
URN: urn:nbn:de:0030-drops-78730
URL: http://dagstuhl.sunsite.rwth-aachen.de/volltexte/2017/7873/
Go to the corresponding LIPIcs Volume Portal

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

On the Complexity of Bounded Context Switching

pdf-format:
LIPIcs-ESA-2017-27.pdf (0.6 MB)

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.

BibTeX - Entry

@InProceedings{chini_et_al:LIPIcs:2017:7873,
  author =	{Peter Chini and Jonathan Kolberg and Andreas Krebs and Roland Meyer and Prakash Saivasan},
  title =	{{On the Complexity of Bounded Context Switching}},
  booktitle =	{25th Annual European Symposium on Algorithms (ESA 2017)},
  pages =	{27:1--27:15},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-049-1},
  ISSN =	{1868-8969},
  year =	{2017},
  volume =	{87},
  editor =	{Kirk Pruhs and Christian Sohler},
  publisher =	{Schloss Dagstuhl--Leibniz-Zentrum fuer Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{http://drops.dagstuhl.de/opus/volltexte/2017/7873},
  URN =		{urn:nbn:de:0030-drops-78730},
  doi =		{10.4230/LIPIcs.ESA.2017.27},
  annote =	{Keywords: Shared memory concurrency, safety verification, fixed-parameter tractability, exponential time hypothesis, bounded context switching}
}

Keywords: Shared memory concurrency, safety verification, fixed-parameter tractability, exponential time hypothesis, bounded context switching
Collection: 25th Annual European Symposium on Algorithms (ESA 2017)
Issue Date: 2017
Date of publication: 01.09.2017

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