On the Complexity of Bounded Context Switching.

DOI10.4230/LIPICS.ESA.2017.27zbMATH Open1442.68073arXiv1609.09728OpenAlexW2964098997MaRDI QIDQ5111714FDOQ5111714

Authors: Peter Chini, Jonathan Kolberg, A. Krebs, Roland Meyer, Prakash Saivasan 

Publication date: 27 May 2020

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, closing the gap means settling 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.

Full work available at URL: https://arxiv.org/abs/1609.09728

Recommendations

• scientific article
• Model checking with bounded context switching
• Bounded context switching for valence systems
• scientific article
• On Computation Complexity of the Concurrently Enabled Transition Set Problem
• scientific article; zbMATH DE number 17815
• On the complexity of verifying concurrent transition systems
• On the complexity of verifying concurrent transition systems
• Reducing Context-Bounded Concurrent Reachability to Sequential Reachability

zbMATH Keywords

exponential time hypothesisfixed-parameter tractabilitysafety verificationshared memory concurrencybounded context switching

Mathematics Subject Classification ID

Computational difficulty of problems (lower bounds, completeness, difficulty of approximation, etc.) (68Q17) Specification and verification (program logics, model checking, etc.) (68Q60) Models and methods for concurrent and distributed computing (process algebras, bisimulation, transition nets, etc.) (68Q85) Parameterized complexity, tractability and kernelization (68Q27)

Cites Work

• Fundamentals of parameterized complexity
• Faster integer multiplication
• On problems without polynomial kernels
• Parametrized complexity theory.
• Constrained multilinear detection and generalized graph motifs
• Kernelization -- preprocessing with a guarantee
• Can you beat treewidth?
• On Problems as Hard as CNF-SAT
• Complexity of pattern-based verification for multithreaded programs
• Solving Connectivity Problems Parameterized by Treewidth in Single Exponential Time
• Parameterized Algorithms
• On the complexity of \(k\)-SAT
• The complexity of satisfiability of small depth circuits
• Infeasibility of instance compression and succinct PCPs for NP
• Title not available (Why is that?)
• Dynamic Programming on Tree Decompositions Using Generalised Fast Subset Convolution
• Graph-Theoretic Concepts in Computer Science
• Some consequences of non-uniform conditions on uniform classes
• Even faster integer multiplication
• Strong computational lower bounds via parameterized complexity
• Fourier meets M\"{o}bius: fast subset convolution
• Reachability of multistack pushdown systems with scope-bounded matching relations
• Title not available (Why is that?)
• Title not available (Why is that?)
• Tools and Algorithms for the Construction and Analysis of Systems
• Reducing Concurrent Analysis Under a Context Bound to Sequential Analysis
• The Complexity of Predicting Atomicity Violations
• Model checking parameterized asynchronous shared-memory systems
• Global model checking of ordered multi-pushdown systems
• Testing Shared Memories
• On the Complexity of Bounded Context Switching.
• Title not available (Why is that?)
• A multi-parameter analysis of hard problems on deterministic finite automata
• Problems on Finite Automata and the Exponential Time Hypothesis
• Context-bounded analysis for concurrent programs with dynamic creation of threads
• On the Reachability Analysis of Acyclic Networks of Pushdown Systems
• Model-checking linear-time properties of parametrized asynchronous shared-memory pushdown systems
• On atomicity in presence of non-atomic writes
• Parameterised pushdown systems with non-atomic writes
• Analyzing Asynchronous Programs with Preemption

Cited In (8)

• Reachability of scope-bounded multistack pushdown systems
• Fine-grained complexity of safety verification
• Stateless model checking under a reads-value-from equivalence
• Model checking with bounded context switching
• Title not available (Why is that?)
• Bounded Context Switching for Valence Systems
• On the satisfiability of context-free string constraints with subword-ordering
• On the Complexity of Bounded Context Switching.

Uses Software

• DiVinE

This page was built for publication: On the Complexity of Bounded Context Switching.

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q5111714)