On the Complexity of Bounded Context Switching.

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)

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.

Recommendations

Cites work

Cited in

(9)

Describes a project that uses

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)