On the Complexity of Bounded Context Switching

TL;DR

This paper provides a parameterized analysis of bounded context switching (BCS), introducing algorithms and bounds based on parameters like context switches, memory size, and scheduling dimension, advancing understanding of BCS complexity.

Contribution

It presents the first parameterized algorithms for BCS based on context switches and memory, establishes lower bounds, and introduces scheduling dimension as a new complexity measure.

Findings

Algorithm solving BCS with parameters cs and m in O*(m^(cs)2^(cs))

Lower bound of m^o(cs / log(cs)) based on exponential time hypothesis

BCS admits no polynomial kernel

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.