A Case Study of Interactive Conflict-Resolution Support in Software Configuration

Abstract

The Linux kernel is one of the largest highly configurable systems, with more than 13,000 configuration options. Although a description is provided for many of the configuration options, configuring the kernel has been identified as troublesome by both users and developers. To assist the user in satisfying unmet dependencies when configuring a system, an algorithm for resolving configuration conflicts called RangeFix has been proposed by academia. In this case study, we explore how RangeFix can be integrated with the Linux kernel configurator xconfig. We develop a prototype based on xconfig, where an existing Scala implementation of RangeFix is integrated to generate fixes and help the user resolve unmet dependencies. The workflow for configuring the kernel, supported by this prototype, is evaluated with Linux users through a survey. We find that the prototype is promising and can be useful in certain scenarios. We also evaluate the existing Scala implementation of RangeFix in terms of correctness and performance. Although the correctness is found to be good, it is much slower than the users’ expectation. How RangeFix can be implemented to comply with the Linux kernel community’s requirements is also explored in this case study. The result is a partial C implementation of RangeFix, based on a SAT solver. This C implementation is also evaluated in terms of correctness and performance. Even if our C implementation is incomplete, we find that this is a feasible way to implement the algorithm. When finished, it might perform well enough to provide interactive conflict-resolution support in the Linux kernel configurators.