A Demo of ConfigFix: Semantic Abstraction of Kconfig, SAT-based Configuration, and DIMACS Export

The Linux kernel's applicability in many different computing environments—ranging from small Android devices to large scale supercomputer clusters—has contributed to making it one of the world's largest software development projects [8]. Designed as a highly configurable system [50] it boasts 28 million lines of code [26] and over 15,000 configuration options (a.k.a. features [5, 7, 40]). To this end, it has a configurable build system [6], preprocessor-based variation points [7], a model of its features (Kconfig model) and constraints [7, 34], and an interactive configurator tool (xconfig) [50].

A plethora of academic studies and techniques on the kernel's variability and its configuration space exist, ranging from variability anomaly detection [2, 31, 35, 52], techniques to identify, extract, and analyze configuration constraints [29, 34, 49, 50, 55], as well as automated support for reviewing and testing patches [27, 28]. In addition to that, many studies have also been conducted on the kernel's evolution [4, 19, 41, 43] and maintenance [1, 18, 20, 56], analyzing its feature model [7, 47], the modeling language (Kconfig), the evolution of the model [29], the co-evolution and consistency of its variation points [22, 36, 37, 41, 42, 54], and the representation of feature constraints in its codebase [34]. Many of the results have inspired software configurator tools [13, 15]. Various other tools [51, 58] and techniques [32, 33, 44], including the synthesis of feature models from code or feature constraints [23, 30, 48], have also drawn inspiration from the Linux kernel and its configurator, by borrowing from or directly extending its capabilities.

The kernel's main configurator xconfig, however, lacks behind the state of the art. Kernel users have faced challenges when manually creating their desired configurations, given the kernel's vast configuration space and intricate feature constraints. Furthermore, there is limited support for choice propagation and a lack of intelligent configurator support for resolving configuration conflicts. These challenges are common, because enabling a feature often requires transitively changing many others. Consequently, achieving a desired configuration can in turn be laborious and error-prone. A survey  [17] revealed that kernel users commonly struggle with conflict resolution, with 20 % of the respondents needing at least “a few dozen minutes” to do so. Despite this, insofar as we know, no configuration technique stemming from academia, has been specifically developed for the Linux kernel such that it can be officially integrated into the Linux kernel mainline.

In 2015, with the Kconfig-sat initiative [24] kernel developers recognized the need for such a solution. They got in touch with researchers working on kernel configuration studies, to integrate such techniques back into the kernel configurator. Indeed, implementing a sound translation of the kernel's variability model to propositional logic, given the expressiveness and intricate nature of the Kconfig language semantics (explained shortly), has long been an open problem in the community. Multiple translation attempts have been proposed to remedy this [10, 21, 46, 53], but none of them have been without limitations [9].

We present a demo of ConfigFix  [11, 12], which offers intelligent configuration support integrated into the Linux kernel configurator xconfig. It is completely implemented in C, extends xconfig’s graphical user interface, and comes with a testing framework. Since researchers can draw value from the DIMACS export, we also discuss the Kconfig's semantics and the implementation details of our semantic abstraction. In contrast to our previous work [11], this paper is a demo, showcasing enhancements in the user interface, test infrastructure, code quality, and presents the DIMACS export functionality. The current version also integrates feedback from the kernel community. Our efforts have led to a stable version of ConfigFix and its test infrastructure [12], that is currently in the process of being integrated in the kernel's source tree (patches submitted and discussed).

Figure 1 shows the main components of ConfigFix: translation of the Kconfig model into a propositional formula, translation into conjunctive normal form (CNF), conflict resolution algorithm, test infrastructure, and DIMACS export. When invoked, ConfigFix takes the current configuration and the user's configuration goal as input. It then creates a single formula that is a conjunction of all constraints and then queries the SAT solver for satisfiability. In case of a configuration conflict (i.e., the user's goal is not applicable), it triggers our C-based, RangeFix-inspired implementation (discussed shortly) to calculate fixes [11, 59].

Linux Kernel Configuration. The kernel has three different configurators: make xconfig, make menuconfig, and make config. The xconfig provides a graphical user interface, while the others are tailored towards shell users. Via them, correct configurations of kernel features (which come with many different characteristics defined in the Kconfig model) that adhere to constraints (e.g., types and dependencies) can be created and modified. The underlying DSL [3] Kconfig provides feature-modeling concepts [7, 47]. It declares features (called symbols there) of different types (i.e., bool, tristate, string, hex, and int) [45, 46]. Tristate features are often used to control the binding modes of features via three states: "Yes" (compile feature into kernel), "No" (do not compile feature), or "Module" (compile feature as dynamically loadable kernel feature), where constraint semantics follow Kleene's rules for three-state logic [25]. A persistent challenge has been obtaining a sound logical representation (mainly due to its complexity) of the main semantics of Kconfig, as a prerequisite to develop analysis and configuration techniques [11]. After we were the first to formalize its semantics [45, 46] (reverse-engineered from xconfig’s behavior), many others followed up [9, 24, 38, 45, 61] with their own translations. These works demonstrated that the semantics of Kconfig can indeed be abstracted into propositional logic, to be used by SAT solvers.

Translation. Given Kconfig’s expressiveness beyond propositional logic, an abstraction is required. Specifically, ConfigFix translates each feature (called symbol in Kconfig) into a set of variables that represent the possibility of the feature assuming a specific value. For example, any arbitrary Boolean feature (i.e., symbol) will be translated to a single variable S which is either true or false. Tristate features may only assume the values “Yes,” “Module,” or “No.” For such features (i.e., S_TRISTATE), the constraint set variables C and C_m would be created, where C is true if and only if C is “Yes.” and C_m is true if and only if C is “Module”. In theory, in case of an integer feature (i.e., C_INT), with default value of 5 and a constraint 2 ≤ C ≤ 8, it would be translated into six variables in the propositional formula (which are indeed named as described): C=0, C=1, C=2, C=5, C=8 and C=n. C=0, C=1 and C=n are created for every feature by default with C=n handling the case that C is hidden and has no value (i.e., S_UNKNOWN). C=2, C=5 and C=8 are “known values,” which could be values that are either default for the feature or part of a range constraint. The propositional formula is then constructed based on these variables and subsequently translated into CNF using Tseitin transformation [57]. It is noteworthy that this aspect of implementing the ConfigFix translation is the most complicated, given that most features are mainly tristate. Thus, the sheer scale of everything (i.e., features, values, types and especially the CNF conversion), was challenging.

Fix Generation. The ConfigFix GUI is responsible for displaying calculated fixes for configuration conflicts received from users as configuration goals that are not applicable in the current configurator. To calculate and generate fixes from conflicts, a suitable conflict-resolution is required. Various conflict-resolution algorithms exist [16], but many were not applicable to the scope of ConfigFix. They either produce just a single fix, suggest a long list of fixes or only offer limited support for non-Boolean constraints [39]. However, our conflict-resolution algorithm of choice, a rangefix-inspired conflict resolver, produces fixes that offer a range of values for features, supports non-Boolean features and constraints, adheres to correctness, contains a maximum range in the event of overlapping ranges and requires minimal feature set changes [11]. In our implementation, it takes a CNF model where features are represented by variables and generates minimal sets of features (refered to as diagnoses) that must be changed. Next, it calculates new values for each variable in a diagnosis. All unchanged variables are then replaced by their current values and any violated constraints are minimized via heuristic rules defined and split into minimal clauses to generate the fixes. In summary, with those RangeFix capabilities, when there are infinitely many possible solutions available, the user is only presented with the minimal set of these [60].

We now demonstrate ConfigFix’s conflict resolution workflows and DIMACS export functionality. We show the xconfig  UI, the specification of the configuration goal (the assignment of values for a set of features to be configured), the calculation of adequate fixes, and their application.

Workflows. Figure 2 presents the complete workflow of ConfigFix. Upon launch, Xconfig  provides a view that presents a dependency-based hierarchy of nested menus containing features and allows feature value changes when the requirements for the target values are met (as shown in ①). The Kconfig language allows specifying conditions for when a feature should be visible in the view. Users can add any tristate feature to the set of features that should be changed by selecting it in this view and clicking the “Add symbol” button (as shown in ②). The set of features that a user wants to change, but that cannot be changed is also called conflict. The features that are currently added to the conflict are displayed in the menu on the bottom left. The desired value of a feature in the conflict can be set by selecting it in the menu on the bottom left and using one of the buttons “Y”, “M”, or “N” to set it to “Yes”, “Module”, or “No,” respectively. Alternatively, users can cycle through the three values by clicking on the corresponding cell in the column “Wanted Value.” The difference between “Yes” and “Module” is that with the former, a feature will be statically linked into the kernel, whereas with the latter it will be built as a dynamically loadable kernel module. If a feature cannot be built as a kernel module, the button “M” is grayed out. A feature (symbol) can be removed from the conflict by selecting it in the menu on the bottom left and clicking the button “Remove Symbol.”

Once the desired feature values have been set, fixes can be calculated by clicking “Calculate Fixes.” The fixes are then displayed in the table on the bottom right (as shown in ③). Users can switch between different fixes with a dropdown menu. The fixes associate each feature in the conflict with a new value, and ideally, there is an order of the changes the fix presents in which they can be applied such that after applying all changes, the desired changes would have been achieved. The changes can be made manually, or by clicking on “Apply Selected Solution”, the values can be applied automatically, in which case the user is informed via a dialog when the fix has been applied successfully (as shown in ④). ConfigFix  supports the

DIMACS Export. ConfigFix allows Kconfig model exports in DIMACS notation, using “make cfoutconfig”. The DIMACS output file offers users the Kconfig model in CNF form (see 1 ). This export functionality supports further research on the kernel's feature model and variability mechanisms. For example, given a configuration with 934872 variables that can be true or false and 2764895 constraints where a user wants to enforce functionalities such as automated isolation testing, build integrity and preprocessor validation via the UAPI_HEADER_TEST (32131) feature, 1 indicates that when 32131 is set to false, its dependant 51181 (UAPI_HEADER_TEST_NPC) must also be set to false. Such DIMACS exports could be potentially useful in logical inference scenarios where system based conclusions can be drawn from known configuration constraints, using algorithms that verify the satisfiability (SAT) of the underlying propositional logic statements.

We evaluated ConfigFix  based on the number of conflicts it resolves and the quality of fixes. We created a test infrastructure that generates random configuration samples, introduces conflicts, executes ConfigFix, and then validates the fixes. The cftestconfig module (invoked by the command “make cftestconfig”) is split into two submodules i.e., the ConflictFrameworkSetup responsible for initializing system parameters and the (ConflictFramework), which handles the generation of configurations and conflicts.

Specifically, the test infrastructure works as follows. Cftestconfig can be used to generate configurations and conflicts in three different modes. mode=“single” gives the user the option to generate several conflicts from an existing configuration. When these conflicts are resolved, the data is saved in a results file. In this mode, “make cftestgenconfig” can be called as many times as required. mode=“multi” provides the option to generate multiple random configurations while simultaneously generating for every configuration, a random set of conflicts for a given architecture. The conflicts are solved and the data is subsequently saved in the results file. In its order of execution, “make randconfig” is called first, followed by “make cftestgenconfig”. mode=“multi_arch” gives users the option to generate multiple random configurations and then generate for each, a random set of conflicts for multiple architectures.

First, it samples the configuration space. Samples should provide enough coverage of the features contained therein [14]. This requires all important features (such as hardware architecture) in the configuration space to be considered [14]. Our test infrastructure uses randconfig (an existing tool in the build system) to generate random configurations. Second, it introduces conflicts. For each of the generated configurations, it generates random conflicts containing a specific number of changes requested (i.e., the conflict size, which is configurable).

It then generate a base configuration using randconfig with a probability of 100 % of a feature being set with all conflicts chosen as subsets of the base configuration. Third, it executes the fix generation for each conflict. The generated configuration sample and conflict become inputs to the test algorithm, which will either produce a single or several configuration fixes, or provide feedback that the conflict cannot be resolved. Conflicts are generated by repeatedly choosing a random Boolean or tristate feature with at least one value to which it cannot be set to, due to unmet dependencies. The conflict then requires this option to be set to one of its blocked values (chosen at random). ConfigFix generates a maximum of three fixes that satisfy the set of violated constraints and can accommodate overlapping ranges using defined heuristics to minimise the number of features value changes. Fourth, it validates the fixes. A fix may include some additional features subject to change, in order to set them to their new, desired state. Such features typically bear configuration conflict properties, which may be too hard to reconfigure manually. As such, for every fix returned by the algorithm, it is applied to the sample configuration and verified to ensure that the configuration goal is satisfied, the resultant configuration after applying the fix is valid (via the xconfig configurator), as well as no unnecessary changes have been made to the product configuration.

For the actual evaluation, we generated configurations (i.e., in the multi_arch mode) for three different architectures (x86_64, arm64, and openrisc), and for nine different probabilities for a feature to be selected, ranging from $10\,\%$ to $90\,\%$. In total, the infrastructure evaluated 27 different configurations. We set it to generate conflict sizes between 1–10 features. Table 1 shows the results. It generated 1350 conflicts. For each of the 27 configurations, and each of the 10 conflict sizes, 5 conflicts were generated. ConfigFix  successfully resolved 1,150 conflicts (85.2%) and produced 2,645 fixes in total. Almost all fixes (99.9%) resolved the conflicts, with only 2 fixes (0.1%) failing to do so. Of the fixes, 1,116 (42.2%) were fully applicable (i.e., all the specified values in the fix can be applied) and resolved the conflict, while 1,527 (57.7%) resolved the conflict despite not being fully applicable (i.e., some of the values specified in the fix cannot be applied). Further evaluation details are provided in the ConfigFix repository [12].

Note, a fix could still not resolve a conflict, since our translations abstract the Kconfig model into a propositional formula, which may not be able to capture all the constraints of the original model. Consequently, a fix can be fully inapplicable, but still resolve the conflict, since the fix may change the value of a variable that is not directly involved in the conflict, but is a dependency of a variable that is involved in the conflict.

We presented a demo of ConfigFix. It helps to configure the Linux kernel by offering automated conflict resolution support. While details are in our preceding conference paper [11], herein we focus on demonstrating capabilities and showing improvements since then.

The results from our evaluation indicates the level of accuracy with which ConfigFix is capable of resolving the conflicts it encounters. Thus, reinforcing the notion that at least one fix is produced in almost 85% of the examples generated. And in those examples, fixes generated resolved the conflict correctly in about 100% of the cases presented. However, despite this impressive level of correctness, ConfigFix has some minor limitations.

For starters, ConfigFix does not explicitly handle string and integer constraints due to how relatively rare they are compared to boolean and tristate constraints. Often, the Linux kernel's features are constrained such that they can be enabled, disabled or set as a loadable kernel. Another slight restriction comes from our choice to use a SAT solver instead of an SMT solver, requiring translation from Kconfig to propositional formulas. This means some assignments with integer or string variables are missed by ConfigFix. An SMT solver could handle more complex value sets, like ranges, while ConfigFix  only suggests specific integer values. Furthermore, RangeFix was designed for SMT, however based on mailing list discussions with SAT experts, performance was paramount. Additionally, the translation is not perfectly accurate, even excluding strings and integers. This results in smaller constraint sets and faster runtimes. While this could lead to invalid fixes, irrelevant changes, and missed existing fixes, our validation of ConfigFix shows that this is not a problem at all.

Finally, based on mailing-list interactions, a future direction could be to provide a command-line configuration completion tool where users give a partial configuration, and ConfigFix completes it. We hope the C-based integration developed by discussion with Linux developers contributes research results back to the Linux kernel community, supporting users to configure their desired kernel.