Johann Mortara
email: johann.mortara@univ-cotedazur.fr

Philippe Collet
email: philippe.collet@univ-cotedazur.fr

Capturing the diversity of analyses on the Linux kernel variability

Keywords: Linux, configuration, variability, build system, variability anomalies

As its variability management architecture is complex, the Linux kernel is a constant subject of study for analyzing different aspects of its variability. It relies on a configuration-aware build system, preprocessor directives in the code, and a configuration tool. While many studies have focused on detecting anomalies within these parts or between them, all concepts and denominations are different among contributions, with similar properties devised with varied formalisms, or with no easy relationship between them. This actually hampers the understanding of all variability issues and proposed analyses, as well as their application to other highly configurable systems. In this paper, we analyse the different properties that have been studied on the variability of the kernel and propose a formalism based on the generic concepts of configurator and derivator. We instantiate them to represent the Kconfig, the Kbuild, and CPP in a unified model that enables to represent all the consistency properties. With this model, we manage to categorize the main related studies, establishing their coverage on the defined properties, showing also overlapping and divergences between studies.

CCS CONCEPTS

• Software and its engineering → Software product lines.

INTRODUCTION

With impressive figures of over 15,000 configurable features, 28 million lines of code in more than 60K files, 900,000 commits from more than 2K authors [START_REF] Larabel | The Linux Kernel Enters 2020 At 27.8 Million Lines In Git But With Less Developers For[END_REF], the Linux kernel has been a constant subject of study for the software engineering community. Thanks to its open-source nature and its available history, software evolution [START_REF] Antoniol | Analyzing cloning evolution in the linux kernel[END_REF][START_REF] Israeli | The Linux kernel as a case study in software evolution[END_REF][START_REF] Padioleau | Documenting and automating collateral evolutions in Linux device drivers[END_REF] and maintenance [START_REF] Abal | 42 variability bugs in the linux kernel: a qualitative analysis[END_REF][START_REF] Jiang | Will my patch make it? and how fast? case study on the linux kernel[END_REF] issues have been extensively studied, but it is in the variability research community that it has become emblematic over the years [START_REF] Sincero | Is the Linux Kernel a Software Product Line?[END_REF].

Related work. The variability management architecture of the kernel is complex. It relies on a model-based configuration tool (Kconfig), CPP preprocessor directives in the code, and a configurationaware build system (Kbuild).

Naturally, variability management in the Kconfig part was deeply investigated. While Sincero and Schröder-Preikschat [START_REF] Sincero | The Linux Kernel Configurator as a Feature Modeling Tool[END_REF] established a first mapping between the Kconfig language and feature modelling concepts, She et al. [START_REF] She | The Variability Model of The Linux Kernel[END_REF] investigated the inverse mapping and built a model for the Kconfig language constructs. In [START_REF] She | Formal semantics of the Kconfig language[END_REF], She and Berger described the semantics of the Kconfig language, used as a basis for multiple tools [START_REF] El-Sharkawy | Analysing the Kconfig Semantics and Its Analysis Tools[END_REF][START_REF] Kästner | KconfigReader[END_REF][START_REF] She | Linux Variability Analysis Tools[END_REF][START_REF] Tartler | Feature consistency in compile-time-configurable system software: Facing the Linux 10,000 feature problem[END_REF]. Zengler and Küchlin [START_REF] Zengler | Encoding the Linux kernel configuration in propositional logic[END_REF] achieved a translation of Kconfig's constraints in a single logic formula, later reused with SAT-solving by Walch et al. [START_REF] Walch | Formal analysis of the Linux kernel configuration with SAT solving[END_REF] to analyze the consistency of Kconfig files. In his Master's thesis, Hengelein [START_REF] Hengelein | Analyzing the Internal Consistency of the Linux KConfig Model[END_REF] analyses defects in Kconfig. As it can be seen as a feature model [START_REF] She | The Variability Model of The Linux Kernel[END_REF], it can have its defects, i.e., dead features [START_REF] Kyo | Feature-oriented domain analysis (FODA) feasibility study[END_REF], or false optional features [START_REF] Zhang | A propositional logic-based method for verification of feature models[END_REF]. Besides, as the Linux kernel is a living ecosystem, the evolution of its variability model has also been extensively studied [START_REF] Dintzner | Analysing the Linux kernel feature model changes using FMDiff[END_REF][START_REF] Lotufo | Evolution of the Linux kernel variability model[END_REF][START_REF] Passos | Coevolution of variability models and related artifacts: A case study from the Linux kernel[END_REF][START_REF] Passos | A study of feature scattering in the linux kernel[END_REF].

Closer to the code, Sincero et al. [START_REF] Sincero | Efficient extraction and analysis of preprocessor-based variability[END_REF] defined presence conditions to identify inconsistencies in the constraints defined by ifdef directives in the kernel, and proposed an implementation with the Undertaker toolchain. While Tartler et al. introduced the problem of inconsistencies between Kconfig files and ifdef directives in [START_REF] Tartler | Dead or alive: Finding zombie features in the Linux kernel[END_REF], they extended Undertaker to add constraints from the Kconfig files and identify inconsistencies between the two spaces [START_REF] Tartler | Feature consistency in compile-time-configurable system software: Facing the Linux 10,000 feature problem[END_REF][START_REF] Tartler | Revealing and repairing configuration inconsistencies in large-scale system software[END_REF]. Other tools relying on presence conditions have been developed to reason on ifdef directives for type checking, such as TypeChef [START_REF] Kenner | Typechef: Toward type checking# ifdef variability in C[END_REF], and use the Linux code base as a robustness trial [START_REF] Kästner | Variability-aware parsing in the presence of lexical macros and conditional compilation[END_REF]. In [START_REF] Rodrigues | Do# ifdefbased Variation Points Realize Feature Model Constraints[END_REF] the authors identified more than 36,000 inconsistencies in the Linux code assets with their checking technique between FM concepts and their translation using ifdef directives.

Multiple tooled approaches have also been proposed to parse, analyze and reason on Kbuild Makefiles, as KbuildMiner [START_REF] Berger | Feature-to-Code Mapping in Two Large Product Lines[END_REF], Makex [START_REF] Nadi | The Linux kernel: A case study of build system variability[END_REF], Golem [START_REF] Dietrich | A robust approach for variability extraction from the Linux build system[END_REF] (and its extension MiniGolem [START_REF] Ruprecht | Lightweight Extraction of Variability Information from Linux Makefiles[END_REF]), and Kmax [START_REF] Gazzillo | Kmax: Finding all configurations of kbuild makefiles statically[END_REF]. Berger et al. [START_REF] Berger | Feature-to-Code Mapping in Two Large Product Lines[END_REF] analyzed the Kbuild Makefiles to extract a mapping between features and code assets in the shape of presence conditions on the features. Other tools for analyzing standard Makefiles have been applied to Kbuild files, as Makao [START_REF] Adams | Design recovery and maintenance of build systems[END_REF], which builds a dependency graph from them. This tool is used in more recent work on the identification of unspecified dependencies in make-based systems, also applied to Kbuild [START_REF] Bezemer | An empirical study of unspecified dependencies in make-based build systems[END_REF]. Finally, after studying the internal consistency of the Kbuild Makefiles through three types of defects [START_REF] Nadi | Make it or break it: Mining anomalies from Linux Kbuild[END_REF], Nadi and Holt built a third extension of Undertaker to add constraints from the Kbuild files and identify inconsistencies in the three spaces [START_REF] Nadi | Mining Kbuild to detect variability anomalies in Linux[END_REF].

Despite this large body of work, the variability of the Linux kernel is still a subject of new studies (e.g., translating configurations from the Kconfig to propositional logic [START_REF] Fernandez-Amoros | A Kconfig translation to logic with one-way validation system[END_REF], using symbolic execution to recover build conditions in Kbuild files [START_REF] Nguyen | Using Symbolic Execution to Analyze Linux KBuild Makefiles[END_REF]), tools (e.g., interactively resolving configuration conflict [START_REF] Franz | ConfigFix: Interactive Configuration Conflict Resolution for the Linux Kernel[END_REF]), and challenges (e.g., deriving a BDD [START_REF] Thüm | A BDD for Linux? the knowledge compilation challenge for variability[END_REF]). Problem statement. While many studies have focused on detecting anomalies in or between each part of the Linux build, all concepts and denominations are different among contributions, with the same properties being described with varied formalisms and sometimes different definitions, at different levels, or with no easy relationship between them.

For example, Sincero et al. [START_REF] Sincero | Efficient extraction and analysis of preprocessor-based variability[END_REF] presented a first implementation of Undertaker for CPP implementing their formalism on CPP. Tartler et al. [START_REF] Tartler | Feature consistency in compile-time-configurable system software: Facing the Linux 10,000 feature problem[END_REF] then improved it by adding a second level to Undertaker for reasoning over the Kconfig constraints, but the authors considered the constraints from CPP in the tool as a black box. Consequently the fine-grained comprehension of the link feature-block is then lost. The same issue can be found in the work from Nadi and Holt [START_REF] Nadi | Mining Kbuild to detect variability anomalies in Linux[END_REF] on the Kbuild space and the third extension they provide for Undertaker.

Moreover, several studies on the variability anomalies exhibit inconsistencies in and across the different parts of the Linux build system, making use of identical denominations (such as dead and undead) for different types of code assets (code block, file. . . ), with sometimes colliding definitions [START_REF] Nadi | Mining Kbuild to detect variability anomalies in Linux[END_REF][START_REF] Sincero | Efficient extraction and analysis of preprocessor-based variability[END_REF][START_REF] Tartler | Feature consistency in compile-time-configurable system software: Facing the Linux 10,000 feature problem[END_REF] (cf. section 3).

These issues and the lack of a uniform vision over the different analyses on the kernel variability hamper the understanding of both the issues and the proposed solutions, as well as their transfer in the future evolution of the build system. Furthermore a uniform and consistent model could be applied to other highly configurable systems, such as MozBuild [START_REF] Maudoux | Lessons and Pitfalls in Building Firefox with Tup[END_REF] from the Mozilla foundation.

Contributions. In this paper, after providing background information about variability in the Linux kernel (section 2), we tackle these issues by making the following contributions:

• We analyse the different terminologies and properties that have been studied on the variability elements of the kernel, taking as input the main related work on consistency inside Kconfig, Kbuild, and CPP, and between them (section 3). • We bring together existing formalizations in a single formalism that captures all relevant elements of the Linux kernel variability. Instead of extracting a partial representation to reason about it, our formalism first considers selectable entities of the entire build workflow, i.e., features, files and code blocks, to express properties. These properties are determined over two concepts: a configurator, which can represent the Kconfig, and a derivator, which can be instantiated differently to represent the Kbuild (to select files) and CPP (to select code blocks) (section 4). • We show the instantiated models and express the already identified defects from the main previous contributions, establishing their coverage on the defined properties (section 5).

Section 6 discusses the threats to the validity of this study while section 7 concludes this paper.

VARIABILITY IN THE LINUX KERNEL

The Linux build system is composed of three distinct stages (fig. 1): Kconfig space. Kconfig files are present in multiple directories of the codebase and define configuration options (also called symbols) representing features. Each configuration option is defined as a config entry and can be of six different types: bool, tristate, string, hex, or int. A default value for the feature can be set with the default entry. Features can be selected directly by the user via a prompt (present in an individual prompt entry or attached to the type of the feature), or by constraints on other features (defined in a depends on entry). Menus allow to group features. If a feature is defined within a menu item that itself has a depends on entry, this condition is appended by Kconfig to the depends on condition of the feature 1 . A feature can also force the selection of another feature with the select entry. For example, in the lib/Kconfig file presented in fig. 1, feature FOO (l.4) is a feature of type bool whose default value is y but which can be modified by the user via a prompt. To be selected, DEPS_A or DEPS_B need to be selected, and MENU_COND needs to be satisfied. The selection of FOO, will also force the selection of F_SEL. Kconfig checks for the consistency of the constraints between the selected features and outputs two files containing the list of selected features in two formats: .config will be read by the Kbuild Makefiles, and autoconf.h is a C header file that will be appended to every source file during compilation.

Make space. The Kbuild system is made of multiple Makefiles present in multiple directories throughout the project, which select objects for the compilation. Three types of objects exist: object files, directories and composite objects. Object files (such as file_c.o in lib/dir/Makefile) represent objects generated during the compilation from existing .c files in the codebase. Therefore, a file_c.c file should be present in the codebase. Added directories (such as dir/ in lib/Makefile) will have their Kbuild Makefile parsed to select files from this subtree. Composite objects associate multiple files in one single object. For example, foo.o in lib/dir/Makefile is a composite object defined at line 2 combining file_a.o and file_b.o and used at line 1.

Selection is done by adding the object files generated at the precompilation to lists. For example, in lib/dir/Makefile, the file_c.o object is added to the obj-y list. In this case, the object will always be selected. The selection of an object can also be conditioned by the value of a feature, as for the foo.o object. CONFIG_FOO refers to the FOO feature defined in the Kconfig file lib/Kconfig. FOO is a boolean feature, therefore if it has for value y, the object will be added to the obj-y list. The same mechanism applies for the dir directory in lib/Makefile, with the small difference that BAR is a tristate feature, allowing an extra m value. The object added to the obj-m list will be compiled as a module. If a feature is not defined, the name of the list becomes obj-and is ignored.

Code space. Variability in the source files is implemented using CPP directives. Code in conditional blocks declared with #if, #elif, #ifdef, or #ifndef directives (referred to as ifdef directives) is selected only if the condition of the directive is satisfied. For example, in lib/dir/foo.c, the selection of B1 implies that the condition line 1 is true. A nested block can only be selected if its parent block is selected (the selection of B1 implies that the condition line 3 is true and that B1 is also selected). Finally, code defined in a block declared with #elif or #else can only be selected if the ifdef blocks preceding it are not selected (the selection of B3 implies that the condition line 5 is true and that B2 is not selected, and the selection of B4 implies that neither B2 nor B3 are selected).

DIVERSITY OF ANALYSES

Facing the many research studies on the Linux kernel variability, we queried three major digital libraries (ACM Digital Library, IEEEXplore and Scopus) searching for papers related to the consistency, build or configuration of the Linux kernel, and clearly Figure 1: Sample Linux build process, inspired from [START_REF] Nadi | The Linux kernel: A case study of build system variability[END_REF] and [START_REF] Sincero | Efficient extraction and analysis of preprocessor-based variability[END_REF] evoking at least one of the three mechanisms of the build system (namely, Kconfig, Kbuild, and CPP). We then explored the references from the obtained papers to search for other work related to the topic. After manual inspection, we discarded work related to the analysis of tools to parse files from the build system [START_REF] El-Sharkawy | Analysing the Kconfig Semantics and Its Analysis Tools[END_REF], the tools themselves [START_REF] Kästner | KconfigReader[END_REF][START_REF] She | Linux Variability Analysis Tools[END_REF] and tooled approaches that do not characterize anomalies [START_REF] Adams | Design recovery and maintenance of build systems[END_REF][START_REF] Berger | Feature-to-Code Mapping in Two Large Product Lines[END_REF][START_REF] Dietrich | A robust approach for variability extraction from the Linux build system[END_REF][START_REF] Gazzillo | Kmax: Finding all configurations of kbuild makefiles statically[END_REF][START_REF] Ruprecht | Lightweight Extraction of Variability Information from Linux Makefiles[END_REF]. We also dismiss work on the formal semantics of the Kconfig files [START_REF] She | Formal semantics of the Kconfig language[END_REF][START_REF] Walch | Formal analysis of the Linux kernel configuration with SAT solving[END_REF][START_REF] Zengler | Encoding the Linux kernel configuration in propositional logic[END_REF] and translation to boolean logic [START_REF] Fernandez-Amoros | A Kconfig translation to logic with one-way validation system[END_REF], which do not report anomalies. Finally, we dismiss preliminary work completed by later publications of the same authors [START_REF] Tartler | Dead or alive: Finding zombie features in the Linux kernel[END_REF] and journal extensions [START_REF] Nadi | The Linux kernel: A case study of build system variability[END_REF][START_REF] Tartler | Revealing and repairing configuration inconsistencies in large-scale system software[END_REF]. In the following, we discuss five studies of anomalies in the kernel variability, definitions for anomalies being directly extracted from them. We mark with a ★ anomalies that are naturally inconsistent as they are directly extracted from papers. Characterizing these inconsistencies is done by instantiating the anomalies in our models (cf. section 5). However, some sentences may be added to reproduce the context of the definitions. For brevity's sake, some less important definitions are not given in this paper, but are detailed in a companion report that is covering all definitions of the analysed studies, the proposed models, and their application to the kernel [START_REF] Mortara | Capturing the diversity of analyses over the Linux kernel variability -Companion Technical Report[END_REF].

CPP internal consistency by Sincero et al. [44]

Sincero et al. [START_REF] Sincero | Efficient extraction and analysis of preprocessor-based variability[END_REF] formalize CPP directives using propositional logic and propose a framework, Undertaker, to automate the derivation of presence conditions from ifdef directives. They define lines of code in ifdef blocks as blocks and define for a block 𝑏 𝑖 the Presence Condition [START_REF] Sincero | Efficient extraction and analysis of preprocessor-based variability[END_REF]: The authors then give a definition of dead defect:

PC(𝑏 𝑖 ) = 𝑒𝑥𝑝𝑟𝑒𝑠𝑠𝑖𝑜𝑛(𝑏 𝑖 ) ∧ 𝑛𝑜𝑃𝑟𝑒𝑑𝑒𝑐𝑒𝑠𝑠𝑜𝑟𝑠 (𝑏 𝑖 ) ∧
Anomaly 1 (Dead block [START_REF] Sincero | Efficient extraction and analysis of preprocessor-based variability[END_REF]). A block is dead if:

¬𝑠𝑎𝑡𝑖𝑠 𝑓 𝑖𝑎𝑏𝑙𝑒 (K ∧ C ∧ 𝐵𝑙𝑜𝑐𝑘 𝑁 )
with K and C the propositional formulas representing the problem space constraints (i.e., Kconfig space) and solution space constraints (i.e., Make space) respectively. 𝑠𝑎𝑡𝑖𝑠 𝑓 𝑖𝑎𝑏𝑙𝑒 () represents the boolean satisfiability problem2 .

Relying on the expression of the presence condition, the authors finally define two levels of consistency to express this definition of dead defect. As these expressions have been simplified by the authors in later work [START_REF] Tartler | Feature consistency in compile-time-configurable system software: Facing the Linux 10,000 feature problem[END_REF], they are given in the companion report.

Anomaly 2 (Internal consistency [START_REF] Sincero | Efficient extraction and analysis of preprocessor-based variability[END_REF]). def. in companion report.

Anomaly 3 (External consistency [START_REF] Sincero | Efficient extraction and analysis of preprocessor-based variability[END_REF]). def. in companion report.

Kconfig internal consistency by

Hengelein [START_REF] Hengelein | Analyzing the Internal Consistency of the Linux KConfig Model[END_REF] In his Master's thesis Hengelein [START_REF] Hengelein | Analyzing the Internal Consistency of the Linux KConfig Model[END_REF] analyses the internal consistency of Kconfig and characterises six different types of anomalies.

While the first three are common anomalies resulting from conflicts between constraints on the features, the last three are related to the syntax of the Kconfig files, and given in the companion report.

Anomaly 4 (Dead feature [START_REF] Hengelein | Analyzing the Internal Consistency of the Linux KConfig Model[END_REF]). A feature is dead if there are contradictions in its dependencies.

Anomaly 5 (False optional (undead) feature ★ [START_REF] Hengelein | Analyzing the Internal Consistency of the Linux KConfig Model[END_REF]). A false optional feature in Kconfig is a feature that is selected by another feature that is always on or selected by a feature that is false optional itself.

Anomaly 6 (Missing dead feature [START_REF] Hengelein | Analyzing the Internal Consistency of the Linux KConfig Model[END_REF]). A feature is missing dead if features in the dependencies are not defined in Kconfig.

Anomaly 7 (Selects on Symbols with Dependencies [START_REF] Hengelein | Analyzing the Internal Consistency of the Linux KConfig Model[END_REF]). def. in companion report.

Anomaly 8 (Unreachable symbol [START_REF] Hengelein | Analyzing the Internal Consistency of the Linux KConfig Model[END_REF]). def. in companion report.

Anomaly 9 (Unnecessary Selects on Choice Values [START_REF] Hengelein | Analyzing the Internal Consistency of the Linux KConfig Model[END_REF]). def. in companion report.

Kbuild consistency by Nadi and Holt [30]

Nadi and Holt [START_REF] Nadi | Make it or break it: Mining anomalies from Linux Kbuild[END_REF] investigate both the internal and external consistencies of the Kbuild Makefiles by studying the (non-)use of composite objects, and the non-selection of a file because of a missing feature. The absence of files from the code base in the Makefiles is also studied (anom. {10}), but does not result from a conflict between constraints in the build system. Its definition and its instantiation in our model are thus given in the companion report.

Anomaly 10 (File Not Used (implementation-compilation consistency) [START_REF] Nadi | Mining Kbuild to detect variability anomalies in Linux[END_REF]). def. in companion report.

Anomaly 11 (Feature Not Defined (compilation-configuration consistency) [START_REF] Nadi | Mining Kbuild to detect variability anomalies in Linux[END_REF]). A .c file is referenced in the Makefile, and its presence is conditioned on a Kconfig feature being defined. However, this feature is not defined in any of the Kconfig files.

Anomaly 12 (Variable Not Used (compilation self-consistency) [START_REF] Nadi | Mining Kbuild to detect variability anomalies in Linux[END_REF]).

A .c file is referenced in the Makefile as part of a composite variable definition, but this variable is never used.

Kconfig-CPP consistency by Tartler et al. [45]

Tartler et al. [START_REF] Tartler | Feature consistency in compile-time-configurable system software: Facing the Linux 10,000 feature problem[END_REF] characterize defects issuing from conflicts between the Kconfig and the CPP space. They first give the following definition of dead and undead blocks.

Anomaly 13 (Configurability defect ★ [START_REF] Tartler | Feature consistency in compile-time-configurable system software: Facing the Linux 10,000 feature problem[END_REF]). A configurability defect (short: defect) is a configuration-conditional item that is either dead (never included) or undead (always included) under the precondition that its parent (enclosing item) is included:

dead: ¬𝑠𝑎𝑡 (C ∧ I ∧ 𝐵𝑙𝑜𝑐𝑘 𝑁 ) undead: ¬𝑠𝑎𝑡 (C ∧ I ∧ ¬𝐵𝑙𝑜𝑐𝑘 𝑁 ∧ 𝑝𝑎𝑟𝑒𝑛𝑡 (𝐵𝑙𝑜𝑐𝑘 𝑁 ))
with C and I the formulas representing the configuration (i.e., Kconfig) and implementation (i.e., Make) spaces respectively.

The authors then reuse the formalism proposed by Sincero et al. [START_REF] Sincero | Efficient extraction and analysis of preprocessor-based variability[END_REF] to simplify the defects with the two following definitions.

Anomaly 14 (Implementation-only defects [START_REF] Tartler | Feature consistency in compile-time-configurable system software: Facing the Linux 10,000 feature problem[END_REF], simplification of anom. {2}). def. in companion report.

Anomaly 15 (Configuration-implementation defects ★ [START_REF] Tartler | Feature consistency in compile-time-configurable system software: Facing the Linux 10,000 feature problem[END_REF], simplification of anom. {3}). Configuration-implementation defects occur when the rules from the configuration space contradict rules from the implementation space. We check for such defects by solving 𝑠𝑎𝑡 ((𝑏 𝑖 ↔ PC(𝑏 𝑖 )) ∧ V). We can infer the expressions for dead and undead configuration-implementation defects.

dead: ¬𝑠𝑎𝑡 ((𝑏 𝑖 ↔ PC(𝑏 𝑖 )) ∧ V) undead: ¬𝑠𝑎𝑡 (¬ (𝑏 𝑖 ↔ PC(𝑏 𝑖 )) ∧ V)
with V the propositional formula representing the configuration space (i.e., the feature model of Kconfig).

Since anom. {14} is a special case of anom. {15} which does not consider external constraints, we only detail the latter.

Anomaly 16 (Configuration-only defects [START_REF] Tartler | Feature consistency in compile-time-configurable system software: Facing the Linux 10,000 feature problem[END_REF]). Features are present in the configuration-space model but do not appear in any valid configuration of the model, which means that the presence condition of the feature is not satisfiable. We can check for such defects by solving: 𝑠𝑎𝑡 (𝑓 𝑒𝑎𝑡𝑢𝑟𝑒 → 𝑝𝑟𝑒𝑠𝑒𝑛𝑐𝑒𝐶𝑜𝑛𝑑𝑖𝑡𝑖𝑜𝑛(𝑓 𝑒𝑎𝑡𝑢𝑟𝑒)). However, no formal definition of 𝑝𝑟𝑒𝑠𝑒𝑛𝑐𝑒𝐶𝑜𝑛𝑑𝑖𝑡𝑖𝑜𝑛 was given.

Anomaly 17 (Referential defects [START_REF] Tartler | Feature consistency in compile-time-configurable system software: Facing the Linux 10,000 feature problem[END_REF]). Referential defects are caused by a missing feature (𝑚) that appears in either the configuration or the implementation space only. That is:

𝑠𝑎𝑡 ((𝑏 𝑖 ↔ PC(𝑏 𝑖 )) ∧ V ∧ ¬ (𝑚 1 ∨ • • • ∨ 𝑚 𝑛 ))
is unsatisfiable.

Kconfig-Kbuild-CPP consistency by Nadi

and Holt [START_REF] Nadi | Mining Kbuild to detect variability anomalies in Linux[END_REF] Nadi and Holt [START_REF] Nadi | Mining Kbuild to detect variability anomalies in Linux[END_REF] improve Undertaker [START_REF] Tartler | Feature consistency in compile-time-configurable system software: Facing the Linux 10,000 feature problem[END_REF] to add constraints from the Make space and identify dead and undead artifacts at both source file and code block levels, relying on constraints from the three spaces.

Anomaly 18 (Code anomalies [START_REF] Nadi | Mining Kbuild to detect variability anomalies in Linux[END_REF]). def. in companion report.

Anomaly 19 (Code-Kconfig ★ [START_REF] Nadi | Mining Kbuild to detect variability anomalies in Linux[END_REF]). Code-Kconfig anomalies are defined as "Code constraints are not consistent with constraints in Kconfig" and detected using the following formulas:

𝐷𝑒𝑎𝑑 𝐵 𝑁 = ¬𝑠𝑎𝑡 (𝐵𝑙𝑜𝑐𝑘 𝑁 ∧ 𝐶 ∧ 𝐾) 𝑈 𝑛𝑑𝑒𝑎𝑑 𝐵 𝑁 = ¬𝑠𝑎𝑡 (¬𝐵𝑙𝑜𝑐𝑘 𝑁 ∧ 𝑝𝑎𝑟𝑒𝑛𝑡 (𝐵𝑙𝑜𝑐𝑘 𝑁 ) ∧ 𝐶 ∧ 𝐾)
These formulas are strictly identical to anom. {15}, thus their expressiveness in our model will be checked together.

Anomaly 20 (Code-Kconfig missing [START_REF] Nadi | Mining Kbuild to detect variability anomalies in Linux[END_REF]). Such defects happen when Code constraints are not consistent with Kconfig constraints because certain features used in the code are not defined in the Kconfig files and are, therefore, always false.

Anomaly 21 (Code-Make ★ [START_REF] Nadi | Mining Kbuild to detect variability anomalies in Linux[END_REF]). def. in companion report.

Anomaly 22 (Code-Make-Kconfig ★ [START_REF] Nadi | Mining Kbuild to detect variability anomalies in Linux[END_REF]). Code-Make-Kconfig anomalies are defined as "The combination of constraints in the three spaces are conflicting" and detected using the following formulas:

𝐷𝑒𝑎𝑑 𝐵 𝑁 = ¬𝑠𝑎𝑡 (𝐵𝑙𝑜𝑐𝑘 𝑁 ∧ 𝐶 ∧ 𝑀 ∧ 𝐾) 𝑈 𝑛𝑑𝑒𝑎𝑑 𝐵 𝑁 = ¬𝑠𝑎𝑡 (¬𝐵𝑙𝑜𝑐𝑘 𝑁 ∧ 𝑝𝑎𝑟𝑒𝑛𝑡 (𝐵𝑙𝑜𝑐𝑘 𝑁 ) ∧ 𝐶 ∧ 𝑀 ∧ 𝐾)
Anomaly 23 (Code-Make-Kconfig missing [START_REF] Nadi | Mining Kbuild to detect variability anomalies in Linux[END_REF]). Such defects happen when "The combination of constraints in the three spaces are conflicting because certain features used in the compilation constraints are not defined in the Kconfig files, and are therefore always false".

Anomaly 24 (Make-Kconfig ★ [START_REF] Nadi | Mining Kbuild to detect variability anomalies in Linux[END_REF]). A file is dead "if it can never be present (i.e., will never get compiled) while satisfying the combination of constraints in the Make space and the Kconfig space". These anomalies are checked by checking these formulas.

𝐷𝑒𝑎𝑑 𝐹 𝑁 = ¬𝑠𝑎𝑡 (𝐹𝑖𝑙𝑒 𝑁 ∧ 𝑀 ∧ 𝐾) 𝑈 𝑛𝑑𝑒𝑎𝑑 𝐹 𝑁 = ¬𝑠𝑎𝑡 (¬𝐹𝑖𝑙𝑒 𝑁 ∧ 𝑀 ∧ 𝐾)
Anomaly 25 (Make-Kconfig missing [START_REF] Nadi | Mining Kbuild to detect variability anomalies in Linux[END_REF]). The definition of this type of defects is not written literally in the paper but we can derive the definition from anom. {20,23}. Such defects happen when the combination of constraints in the make and Kconfig spaces are conflicting because certain features used in the Makefiles are not defined in the Kconfig files, and are therefore always false.

Since anom. {18,19,21} and their missing variants anom. {20,25} encompass special cases of anom. {19} and anom. {23} by considering only some spaces, we only detail the instantiation of the latter.

Summary

While the studies on the Linux build system all present the three spaces (Kconfig, Kbuild and CPP) when they used them, no standard denomination is given to each of these spaces, leading to a profusion of names. The different denominations for the studied papers are listed in table 1 3 . Within just this subset, we can notice that every paper has its own terminology. To prevent the addition of yet another terminology to the state-of-the-art, we decided to reuse the terminology proposed by Nadi and Holt [START_REF] Nadi | Mining Kbuild to detect variability anomalies in Linux[END_REF], as it is the only study we kept that covers the three spaces.

By analysing the definitions of anomalies from the selected papers, we can pinpoint multiple elements bringing confusion. First, multiple definitions are redundant between papers, but their expression and their names differ. For example, Dead block defined by Sincero et al. [START_REF] Sincero | Efficient extraction and analysis of preprocessor-based variability[END_REF] in anom. {1}, Configurability defects defined by Tartler et al. [START_REF] Tartler | Feature consistency in compile-time-configurable system software: Facing the Linux 10,000 feature problem[END_REF] in anom. {13} and Code-Kconfig anomalies defined by Nadi and Holt [START_REF] Nadi | Mining Kbuild to detect variability anomalies in Linux[END_REF] in anom. {19} express the same formula. Moreover, spaces can also be named differently, sometimes with 3 Details of all the studies presented in the introduction are given in a complete table in the companion report [START_REF] Mortara | Capturing the diversity of analyses over the Linux kernel variability -Companion Technical Report[END_REF]. the same letter representing two different spaces in two definitions (𝐶 represents the CPP constraints in [START_REF] Nadi | Mining Kbuild to detect variability anomalies in Linux[END_REF][START_REF] Sincero | Efficient extraction and analysis of preprocessor-based variability[END_REF] and the Kconfig constraints in [START_REF] Tartler | Feature consistency in compile-time-configurable system software: Facing the Linux 10,000 feature problem[END_REF]). A summary of these differences is given in table 1.

On the opposite, some anomalies with identical names may not express the same type of defect. This is the case for the formulas to detect dead blocks in anom. {13} and anom. {15}, which are equivalent, while the characterizations of undead blocks are inconsistent. Let us take the following example:

1 #if defined A 2 //block 1 3 # if defined A 4 //block 2 5 # endif 6 #endif
Block 2 is undead according to anom. {13}, as the selection of its parent (Block 1) implies its selection. However, if the A variable is not defined, then Block 2 is not undead according to anom. {15} as it is not always included.

While encompassing the variability of the whole Linux kernel build system, the models presented in the next section will also help in obtaining a coherent set of consistency properties.

PROPOSED MODELS

In order to cover all three stages of the Linux kernel build system and to represent its variability mechanisms independently of their implementation, we design a model with the concepts of feature, asset, propositional formula, and presence condition. We add a concept of predecessor to handle the dependency between the three stages, as well as two additional concepts to be able to represent the stages themselves:

• a configurator defines presence conditions on features (i.e., the condition allowing an individual feature to be selected).

Presence conditions on features are propositional formulas on other features; • a derivator defines presence conditions on assets, (i.e., the condition allowing an individual asset to be selected). Presence conditions on assets are propositional formulas on both features and assets, which can be either of the same type or of another type. Some properties will also be defined on the internal and external consistency of the elements as to cover the different anomalies devised in the previous section. We could also have built our models on a more expressive theoretical background, such as the refinement theory, to potentially obtain for free some properties, but we decided to rely on a more simple but very explicit basis to clarify first all concepts and inconsistencies.

In the following, we will use these utility definitions:

𝑡𝑒𝑟𝑚𝑠 (𝜙) a helper function which, given a propositional formula, returns the terms in it (e.g., 𝑡𝑒𝑟𝑚𝑠 ((𝐴 ∧ 𝐵) ∨ 𝐶) = {𝐴, 𝐵, 𝐶}). 𝑒𝑥𝑝𝑎𝑛𝑑 (𝜙) a helper function which, given a propositional formula 𝜙, replaces every asset 𝑎 in 𝜙 by its presence condition, noted PC 𝐼𝑛𝑡 (𝑎) and defined in def. 2 (e.g., 𝑒𝑥𝑝𝑎𝑛𝑑 (𝑏

1 ∧ ¬𝑏 2 ) = PC 𝐼𝑛𝑡 (𝑏 1 ) ∧ ¬PC 𝐼𝑛𝑡 (𝑏 2 )
). 𝑠𝑙𝑖𝑐𝑒 (𝐶,𝑇 ) an operator which, given a set of boolean conditions on terms 𝐶 and a set of terms 𝑇 , returns the conjunction of all propositional formulas from 𝐶 containing terms from 𝑇 . The operator is recursively applied to the terms that appear in these formulas 4 .

Derivator Model

In this section, we introduce the concepts to form the derivator model and illustrate them with its application to CPP.

Definition 1 (Asset). An asset 𝑎 = ⟨𝜙 𝑠𝑒𝑙𝑒𝑐𝑡 , 𝜙 𝑝𝑟𝑒𝑑𝑠 , 𝜙 𝑑𝑒𝑝𝐼𝑛𝑡 , 𝜙 𝑑𝑒𝑝𝐸𝑥𝑡 ⟩ from a set of assets A 𝑋 is defined as follows:

• 𝜙 𝑠𝑒𝑙𝑒𝑐𝑡 is a propositional formula for the asset's selection ;

• 𝜙 𝑝𝑟𝑒𝑑𝑠 is a propositional formula on other assets that are evaluated before 𝑎. We call these assets predecessors ; • 𝜙 𝑑𝑒𝑝𝐼𝑛𝑡 is a propositional formula on assets on which 𝑎 is dependent ; • 𝜙 𝑑𝑒𝑝𝐸𝑥𝑡 is a propositional formula on assets from another context on which 𝑎 is dependent.

Application to CPP. An asset 𝑏 is a code block, with:

• 𝜙 𝑠𝑒𝑙𝑒𝑐𝑡 the condition of the #if surrounding the block ; Example. In fig. 1, the lib/foo/foo.c file and the blocks B1, B2, B3, and B4 it contains are represented by the following assets:

• 𝜙 𝑝𝑟𝑒𝑑𝑠 = ¬( 𝑖 𝑏 𝑖 ) if 𝑏
• 𝑓 𝑖𝑙𝑒 = ⟨𝑡𝑟𝑢𝑒, 𝑡𝑟𝑢𝑒, 𝑡𝑟𝑢𝑒, 𝑡𝑟𝑢𝑒⟩

• 𝑏 1 = ⟨𝐹𝑂𝑂 ∨ 𝐵𝐴𝑅 ∨ 𝐵𝐴𝑍, 𝑡𝑟𝑢𝑒, 𝑡𝑟𝑢𝑒, 𝑓 𝑖𝑙𝑒⟩ • 𝑏 2 = ⟨𝐹𝑂𝑂, 𝑡𝑟𝑢𝑒, 𝑏 1 , 𝑓 𝑖𝑙𝑒⟩ • 𝑏 3 = ⟨𝐵𝐴𝑅, ¬𝑏 2 , 𝑏 1 , 𝑓 𝑖𝑙𝑒⟩ • 𝑏 4 = ⟨𝑡𝑟𝑢𝑒, ¬(𝑏 2 ∨ 𝑏 3 ), 𝑏 1 , 𝑓 𝑖𝑙𝑒⟩
Definition 2 (Internal presence condition). The internal presence condition of an asset is the boolean formula that needs to be satisfiable for the asset to be selectable. It is defined as 4 The principle of slicing has already been applied to feature models [START_REF] Mathieu Acher | Slicing feature models[END_REF][START_REF] Krieter | Comparing algorithms for efficient feature-model slicing[END_REF] and its goal is to extract a subset of formulas equivalent to the whole space by keeping only formulas relevant to terms from 𝑇 .

PC 𝐼𝑛𝑡 (𝑎) = 𝜙 𝑠𝑒𝑙𝑒𝑐𝑡 𝑎 ∧ 𝑒𝑥𝑝𝑎𝑛𝑑 𝜙 𝑝𝑟𝑒𝑑𝑠 𝑎 ∧ 𝑒𝑥𝑝𝑎𝑛𝑑 𝜙 𝑑𝑒𝑝𝐼𝑛𝑡 𝑎
Note. An asset is selected if and only if its presence condition is satisfied: PC 𝐼𝑛𝑡 (𝑎) ↔ 𝑎 Application to CPP. Let us take again the previous example.

PC 𝐼𝑛𝑡 (𝑏 1 ) = 𝜙 𝑠𝑒𝑙𝑒𝑐𝑡 𝑏 1 ∧ 𝑒𝑥𝑝𝑎𝑛𝑑 𝜙 𝑝𝑟𝑒𝑑𝑠 𝑏 1 ∧ 𝑒𝑥𝑝𝑎𝑛𝑑 𝜙 𝑑𝑒𝑝𝐼𝑛𝑡 𝑏 1 = (𝐹𝑂𝑂 ∨ 𝐵𝐴𝑅 ∨ 𝐵𝐴𝑍 ) ∧ 𝑒𝑥𝑝𝑎𝑛𝑑 (𝑡𝑟𝑢𝑒) ∧ 𝑒𝑥𝑝𝑎𝑛𝑑 (𝑡𝑟𝑢𝑒) = (𝐹𝑂𝑂 ∨ 𝐵𝐴𝑅 ∨ 𝐵𝐴𝑍 ) PC 𝐼𝑛𝑡 (𝑏 2 ) = 𝜙 𝑠𝑒𝑙𝑒𝑐𝑡 𝑏 2 ∧ 𝑒𝑥𝑝𝑎𝑛𝑑 𝜙 𝑝𝑟𝑒𝑑𝑠 𝑏 2 ∧ 𝑒𝑥𝑝𝑎𝑛𝑑 𝜙 𝑑𝑒𝑝𝐼𝑛𝑡 𝑏 2 = (𝐹𝑂𝑂) ∧ 𝑡𝑟𝑢𝑒 ∧ 𝑒𝑥𝑝𝑎𝑛𝑑 (𝑏 1 ) = (𝐹𝑂𝑂) ∧ (𝐹𝑂𝑂 ∨ 𝐵𝐴𝑅 ∨ 𝐵𝐴𝑍 ) PC 𝐼𝑛𝑡 (𝑏 3 ) = 𝜙 𝑠𝑒𝑙𝑒𝑐𝑡 𝑏 3 ∧ 𝑒𝑥𝑝𝑎𝑛𝑑 𝜙 𝑝𝑟𝑒𝑑𝑠 𝑏 3 ∧ 𝑒𝑥𝑝𝑎𝑛𝑑 𝜙 𝑑𝑒𝑝𝐼𝑛𝑡 𝑏 3 = (𝐵𝐴𝑅) ∧ (¬PC 𝐼𝑛𝑡 (𝑏 2 )) ∧ PC 𝐼𝑛𝑡 (𝑏 1 ) PC 𝐼𝑛𝑡 (𝑏 4 ) = 𝜙 𝑠𝑒𝑙𝑒𝑐𝑡 𝑏 4 ∧ 𝑒𝑥𝑝𝑎𝑛𝑑 𝜙 𝑝𝑟𝑒𝑑𝑠 𝑏 4 ∧ 𝑒𝑥𝑝𝑎𝑛𝑑 𝜙 𝑑𝑒𝑝𝐼𝑛𝑡 𝑏 4 = (¬(PC 𝐼𝑛𝑡 (𝑏 2 ) ∨ PC 𝐼𝑛𝑡 (𝑏 3 ))) ∧ PC 𝐼𝑛𝑡 (𝑏 1 )
Note. Extracted presence conditions can be complex and may contain redundant terms (e.g., PC 𝐼𝑛𝑡 (𝑏 2 ) is equivalent to 𝐹𝑂𝑂). Approaches to simplify presence conditions have been proposed [START_REF] Von Rhein | Presence-condition simplification in highly configurable systems[END_REF] and are out of the scope of this paper.

Definition 3 (External presence condition). By evaluating PC 𝐼𝑛𝑡 , we check that the asset can be selected given the constraints of its space. However, other external constraints may prevent the selection the asset. We call context the set of these constraints. The external presence condition of an asset in a given context C is defined as

PC 𝐸𝑥𝑡 (𝑎) = PC 𝐼𝑛𝑡 (𝑎)∧𝑠𝑙𝑖𝑐𝑒 (C, 𝑡𝑒𝑟𝑚𝑠 (PC 𝐼𝑛𝑡 (𝑎))∪𝑡𝑒𝑟𝑚𝑠 (𝜙 𝑑𝑒𝑝𝐸𝑥𝑡 𝑎 ))
Application to CPP. In the Linux build system, the selection of a CPP block is conditioned by constraints on both the features used in the #if instructions (which are determined at the Kconfig level) and the file containing the block (which are determined at the Kbuild level). Thus, the context C to express the external presence condition of a block is the union of the Kconfig and Kbuild contexts C = C Kconfig ∪ C Kbuild . Let us take an example with

C Kconfig = {𝐹𝑂𝑂 → 𝐵𝐴𝑅, 𝐵𝐴𝑍 → (¬𝐹 1), 𝐹 1 → (¬𝐹𝑂𝑂), 𝐹 3 → 𝐹 4} C Kbuild = {𝑓 𝑖𝑙𝑒 ↔ 𝐹𝑂𝑂 } then P C 𝐸𝑥𝑡 (𝑏 1 ) = P C 𝐼𝑛𝑡 (𝑏 1 ) ∧ 𝑠𝑙𝑖𝑐𝑒 ( C, 𝑡𝑒𝑟𝑚𝑠 ( P C 𝐼𝑛𝑡 (𝑏 1 )) ∪ 𝑡𝑒𝑟𝑚𝑠 (𝜙 𝑑𝑒𝑝𝐸𝑥𝑡 𝑏 1
))

= P C 𝐼𝑛𝑡 (𝑏 1 ) ∧ 𝑠𝑙𝑖𝑐𝑒 ( C, {𝐹𝑂𝑂, 𝐵𝐴𝑅, 𝐵𝐴𝑍 } ∪ {𝑓 𝑖𝑙𝑒 }) = P C 𝐼𝑛𝑡 (𝑏 1 ) ∧ ( (𝐹𝑂𝑂 → 𝐵𝐴𝑅) ∧ (𝐵𝐴𝑍 → (¬𝐹 1)) ∧ (𝐹 1 → (¬𝐹𝑂𝑂)) ∧ ( 𝑓 𝑖𝑙𝑒 ↔ 𝐹𝑂𝑂))
4.1.1 Internal consistency. To express defects, we define dead, core, and full-mandatory assets, relying on definitions of dead and falseoptional features introduced by Benavides et al. [START_REF] Benavides | Automated analysis of feature models 20 years later: A literature review[END_REF], and full-mandatory features from Trinidad et al. [START_REF] Trinidad | Automated error analysis for the agilization of feature modeling[END_REF].

Definition 4 (Dead asset). An asset 𝑎 of A is dead if it can never be selected. The set of dead assets of A is noted 𝑑𝑒𝑎𝑑𝑠 (A).

𝑎 ∈ 𝑑𝑒𝑎𝑑𝑠 (A) ⇔ ¬𝑠𝑎𝑡 (PC 𝐼𝑛𝑡 (𝑎))

Note. This consistency check includes the more specific case where an asset is dead because of an inconsistency with the condition to select its internal dependencies (i.e., 𝑒𝑥𝑝𝑎𝑛𝑑 (𝜙 𝑑𝑒𝑝𝐼𝑛𝑡 𝑠 ) → ¬𝜙 𝑠𝑒𝑙𝑒𝑐𝑡 𝑠 ) as in this case PC 𝐼𝑛𝑡 (𝑎) is inconsistent.

Definition 5 (Core asset). An asset 𝑎 of A is a core asset if it is always selected. The set of core assets of A is noted 𝑐𝑜𝑟𝑒 (A).

𝑎 ∈ 𝑐𝑜𝑟𝑒 (A) ⇔ ¬𝑠𝑎𝑡 (¬(PC 𝐼𝑛𝑡 (𝑎)))

Configurator Model

The configurator represents the model element that checks the selection of features. It is represented by a set of features F . We will illustrate the formalization here with its application to the Kconfig. 𝐹 = ⟨𝜙 𝑒𝑛𝑎𝑏𝑙𝑒 , 𝜙 𝑑𝑒𝑝𝑠 , F 𝑠𝑒𝑙𝑒𝑐𝑡 ⟩ • 𝜙 𝑒𝑛𝑎𝑏𝑙𝑒 is a propositional formula representing the ability to select the feature ; • 𝜙 𝑑𝑒𝑝𝑠 is a propositional formula on features on which 𝐹 is dependent ; • F 𝑠𝑒𝑙𝑒𝑐𝑡 is a set of features automatically selecting 𝐹 . If a feature from F 𝑠𝑒𝑙𝑒𝑐𝑡 is selected, 𝐹 is also selected, regardless of the precedent conditions.

Application to Kconfig. A feature 𝐹 is a configuration option defined in a Kconfig file, with:

• 𝜙 𝑒𝑛𝑎𝑏𝑙𝑒 represents the ability to select the feature by user selection (prompt), or default value, as defined in table 2 ; • 𝜙 𝑑𝑒𝑝𝑠 represents the boolean formula on features defined in the depends on statement ; • F 𝑠𝑒𝑙𝑒𝑐𝑡 is a set of features selecting 𝐹 with a select statement ; In the Kconfig file presented in fig. 1, three features are defined: FOO, BAR and F_SEL. Existing work on the semantics of the Kconfig files [START_REF] She | Formal semantics of the Kconfig language[END_REF] inline the conditions from the menu items surrounding the definition of a feature in the depends on condition. These features can be represented by the following assets:

• 𝐹𝑂𝑂 = ⟨𝑡𝑟𝑢𝑒, (𝐷𝐸𝑃𝑆_𝐴 ∨ 𝐷𝐸𝑃𝑆_𝐵) ∧ 𝑀𝐸𝑁𝑈 _𝐶𝑂𝑁 𝐷, {}⟩ • 𝐵𝐴𝑅 = ⟨𝑡𝑟𝑢𝑒, 𝑀𝐸𝑁𝑈 _𝐶𝑂𝑁 𝐷, {}⟩ • 𝐹 _𝑆𝐸𝐿 = ⟨𝑓 𝑎𝑙𝑠𝑒, 𝑡𝑟𝑢𝑒, {𝐹𝑂𝑂 }⟩
Definition 10 (Presence condition). The presence condition of a feature 𝐹 ∈ F represents the boolean formula which needs to be satisfied for the feature to be selected.

PC(𝐹 ) = 𝜙 𝑒𝑛𝑎𝑏𝑙𝑒 ∧ 𝑒𝑥𝑝𝑎𝑛𝑑 (𝜙 𝑑𝑒𝑝𝑠 ) ∨ 𝑑𝑖𝑟𝑒𝑐𝑡𝑆𝑒𝑙𝑒𝑐𝑡 (𝐹 ) with 𝑑𝑖𝑟𝑒𝑐𝑡𝑆𝑒𝑙𝑒𝑐𝑡 (𝐹 ) = 𝐹 𝑠 ∈ F 𝑠𝑒𝑙𝑒𝑐𝑡 PC(𝐹 𝑠 ).
Note. The selection of a feature implies that its presence condition is satisfied: 𝐹 → PC(𝐹 ) There is no biimplication as we consider that a user can manually interfere in the selection. Therefore, the information extracted from the model can only express if a feature can be selected, and not its effective selection. Note. Due to the size and complexity of the Kconfig model, obtaining a sound and complete abstraction of its semantics is still a challenge. The latest studies on boolean translation are not able to represent the whole complexity of the language [START_REF] Fernandez-Amoros | A Kconfig translation to logic with one-way validation system[END_REF]. Because of these limitations, the accuracy of variability reasoning approaches is also limited and acknowledged by researchers [START_REF] Franz | ConfigFix: Interactive Configuration Conflict Resolution for the Linux Kernel[END_REF]. Therefore, we aim here to provide a model allowing us to synthesize the current work, and do not pretend to present a complete model of Kconfig5 .

Consistency.

Definition 11 (Dead feature). A feature 𝐹 of F is dead if it can never be selected. The set of dead features is noted 𝑑𝑒𝑎𝑑𝐹𝑒𝑎𝑡𝑢𝑟𝑒𝑠 ().

𝐹 ∈ 𝑑𝑒𝑎𝑑𝐹𝑒𝑎𝑡𝑢𝑟𝑒𝑠 () ⇔ ¬𝑠𝑎𝑡 (PC(𝐹 ))

Definition 12 (Core feature). A feature 𝐹 of F is a core feature if it is always selected. The set of core features is noted 𝑐𝑜𝑟𝑒𝐹𝑒𝑎𝑡𝑢𝑟𝑒𝑠 ().

𝐹 ∈ 𝑐𝑜𝑟𝑒𝐹𝑒𝑎𝑡𝑢𝑟𝑒𝑠 () ⇔ ¬𝑠𝑎𝑡 (¬PC(𝐹 ))

Note. If 𝐹 𝑆 ∈ F 𝑠𝑒𝑙𝑒𝑐𝑡 𝐹 is a core feature, then 𝐹 is also a core feature, as PC(𝐹 𝑆 ) → PC(𝐹 ).

Definition 13. (Missing dead feature) A feature 𝐹 is missing dead if a feature in its presence condition is not defined. The set of missing dead features is noted 𝑚𝑖𝑠𝑠𝑖𝑛𝑔𝐷𝑒𝑎𝑑𝐹𝑒𝑎𝑡𝑢𝑟𝑒𝑠 ().

𝐹 ∈ 𝑚𝑖𝑠𝑠𝑖𝑛𝑔𝐷𝑒𝑎𝑑𝐹𝑒𝑎𝑡𝑢𝑟𝑒𝑠 () ⇔ (𝑚 ∈ 𝑡𝑒𝑟𝑚𝑠 (PC(𝐹 )) ∧ (𝑚 ∉ F )

INSTANTIATION ON THE LINUX KERNEL

We now instantiate our model on the kernel build system. The configurator is used to model the Kconfig, while the derivator concept is used to model source files selected by the Kbuild Makefiles, with a form of positive variability [START_REF] Voelter | Product line implementation using aspectoriented and model-driven software development[END_REF]: the core is represented by the obj-y entries, where the additional parts are added in composite objects and feature dependent entries. The same derivator concept also represents the selection of code blocks from the source files by CPP, implementing this time negative variability [START_REF] Voelter | Product line implementation using aspectoriented and model-driven software development[END_REF].

Model on CPP

For CPP we have to describe the presence conditions and crossspace expressions for its related anomalies.

5.1.1

Compliance with presence conditions from Sincero et al. [START_REF] Sincero | Efficient extraction and analysis of preprocessor-based variability[END_REF].

For conciseness and to prevent confusion, we name this definition PC 𝑆𝑖𝑛 and use the more compact expression given in [START_REF] Tartler | Feature consistency in compile-time-configurable system software: Facing the Linux 10,000 feature problem[END_REF]:

PC 𝑆𝑖𝑛 (𝑏 𝑖 ) = 𝑒𝑥𝑝𝑟 (𝑏 𝑖 ) ∧ 𝑛𝑜𝑃𝑟𝑒𝑑𝑒𝑐𝑒𝑠𝑠𝑜𝑟𝑠 (𝑏 𝑖 ) ∧ 𝑝𝑎𝑟𝑒𝑛𝑡 (𝑏 𝑖 )
We can express PC 𝑆𝑖𝑛 using our definition of asset from def. 1. Let us apply PC 𝑆𝑖𝑛 on an asset 𝑏 as defined in section 4.1.

PC 𝑆𝑖𝑛 (𝑏) = 𝑒𝑥𝑝𝑟 (𝑏) ∧ 𝑛𝑜𝑃𝑟𝑒𝑑𝑒𝑐𝑒𝑠𝑠𝑜𝑟𝑠 (𝑏) ∧ 𝑝𝑎𝑟𝑒𝑛𝑡 (𝑏) = 𝜙 𝑠𝑒𝑙𝑒𝑐𝑡 𝑏 ∧ ¬ (𝑝𝑟𝑒𝑑 1 ∨ 𝑝𝑟𝑒𝑑 2 ∨ • • • ∨ 𝑝𝑟𝑒𝑑 𝑛 ) ∧ 𝜙 𝑑𝑒𝑝𝐼𝑛𝑡 𝑏 = 𝜙 𝑠𝑒𝑙𝑒𝑐𝑡 𝑏 ∧ 𝜙 𝑝𝑟𝑒𝑑𝑠 𝑏 ∧ 𝜙 𝑑𝑒𝑝𝐼𝑛𝑡 𝑏
𝜙 𝑝𝑟𝑒𝑑𝑠 𝑏 and 𝜙 𝑑𝑒𝑝𝐼𝑛𝑡 𝑏 are propositions on assets corresponding to the blocks themselves. However, to evaluate the presence condition, these assets have to be expanded to their logical expression.

PC 𝑆𝑖𝑛 (𝑏) = 𝜙 𝑠𝑒𝑙𝑒𝑐𝑡 𝑏 ∧ 𝑒𝑥𝑝𝑎𝑛𝑑 𝜙 𝑝𝑟𝑒𝑑𝑠 𝑏 ∧ 𝑒𝑥𝑝𝑎𝑛𝑑 (𝜙 𝑑𝑒𝑝𝐼𝑛𝑡 𝑏 )
The definition of PC 𝑆𝑖𝑛 is therefore compliant with our definition of PC 𝐼𝑛𝑡 given in def. 2. [START_REF] Nadi | Mining Kbuild to detect variability anomalies in Linux[END_REF] defined multiple anomalies (anom. {19,21,22,24}) using different terms, i.e., 𝐵 𝑁 , 𝐶, 𝑀, and 𝐾, which we now describe with our model. 𝐵 𝑁 ∧𝐶. 𝐵 𝑁 represents a block, and 𝐶 the constraints in the code space. This expression is true if and only if the block 𝐵 𝑁 is selected, thus it corresponds to 𝐵 𝑁 ↔ PC 𝑆𝑖𝑛 (𝐵 𝑁 ) using Tartler et al. [START_REF] Tartler | Feature consistency in compile-time-configurable system software: Facing the Linux 10,000 feature problem[END_REF]'s notation and PC 𝐼𝑛𝑡 (𝐵 𝑁 ) in our model. 𝑝𝑎𝑟𝑒𝑛𝑡 (𝐵 𝑁 ). 𝑝𝑎𝑟𝑒𝑛𝑡 (𝐵 𝑁 ) represents the selection of the parent of a block, i.e., its enclosing block. This expression corresponds to 𝑒𝑥𝑝𝑎𝑛𝑑 (𝜙 𝑑𝑒𝑝𝐼𝑛𝑡 𝐵 𝑁

Expressing cross-space formulas. Nadi and Holt

) in our model.

The Kconfig space 𝐾. 𝐾 represents the set of constraints in the Kconfig space, i.e., the constraints on features that allow them to be selected. Tartler et al. [START_REF] Tartler | Feature consistency in compile-time-configurable system software: Facing the Linux 10,000 feature problem[END_REF] do not use the whole feature model expression as the solving would not scale. They instead identify the features impacting the selection of a given code block using a slicing algorithm to build a minimal but sufficient subset of the configuration space through a recursive application on each new feature found in the presence condition expression.

The make space 𝑀. 𝑀 represents the set of constraints in the make space, i.e., the constraints on features that allow the selection of source files in the Makefiles. In her PhD thesis [START_REF] Nadi | Variability Anomalies in Software Product Lines[END_REF], Nadi states: since the conflicts in anom. {21} arise from looking at the block presence condition as well as the file's presence condition, we call this category of anomalies code-build anomalies. Thus, to detect defects involving the make space, it is only necessary to have the presence condition of the file containing the analyzed block.

In section 4.1, we instantiate on CPP the definition of external presence condition given in def. ))

⇔ ¬𝑠𝑎𝑡 ¬PC 𝐸𝑥𝑡 (𝐵 𝑁 ) ∧ 𝑒𝑥𝑝𝑎𝑛𝑑 (𝜙 𝑑𝑒𝑝𝐼𝑛𝑡 𝐵 𝑁 )

anom. {22} thus expresses dead (def. 6) and full-mandatory defects (def. 8).

Instantiation 2 (Expressing configurability defects {13}). Same as inst. 1 with C = C Kconfig .

Instantiation 3 (Expressing code-Kconfig {19}). Same as inst. 2.

Instantiation 4 (Expressing configuration-implementation defects {15}). V corresponds to the minimum but sufficient set of constraints from the configuration space. Thus:

𝑠𝑎𝑡 ((𝑏 𝑖 ↔ PC(𝑏 𝑖 )) ∧ V) ⇔ 𝑠𝑎𝑡 (PC 𝐼𝑛𝑡 (𝑏 𝑖 ) ∧ C Kconfig )
We can then express dead and undead configuration-implementation defects. Given B the set of blocks and C = C Kconfig :

¬𝑠𝑎𝑡 ((𝑏 𝑖 ↔ PC(𝑏 𝑖 )) ∧ V) ⇔ ¬𝑠𝑎𝑡 (PC 𝐼𝑛𝑡 (𝑏 𝑖 ) ∧ C) ⇔ ¬𝑠𝑎𝑡 (PC 𝐸𝑥𝑡 (𝑏 𝑖 )) (𝑑𝑒 𝑓 . 3) ¬𝑠𝑎𝑡 (¬ (𝑏 𝑖 ↔ PC(𝑏 𝑖 )) ∧ V) ⇔ ¬𝑠𝑎𝑡 (¬PC 𝐼𝑛𝑡 (𝑏 𝑖 ) ∧ C) ⇔ ¬𝑠𝑎𝑡 (¬PC 𝐸𝑥𝑡 (𝑏 𝑖 )) (𝑑𝑒 𝑓 . 3)
anom. {15} thus expresses dead (def. 6) and core defects (def. 7).

Instantiation 5 (Expressing code-Make-Kconfig missing defects {23}). We showed in inst. 1 that 𝐵 𝑁 ∧ 𝐶 ∧ 𝑀 ∧ 𝐾 |= PC 𝐸𝑥𝑡 (𝐵 𝑁 ). If a feature 𝑚 from the formula is not defined in the Kconfig files, it means that 𝑚 ∉ 𝑡𝑒𝑟𝑚𝑠 (𝐾) ∪ 𝑡𝑒𝑟𝑚𝑠 (𝑀), i.e., 𝑚 ∉ 𝑡𝑒𝑟𝑚𝑠 (C Kconfig ∪ C Kbuild ). Therefore: ∃𝑚 ∈ 𝑡𝑒𝑟𝑚𝑠 ( P C 𝐸𝑥𝑡 (𝐵 𝑁 )) | (𝑚 ∉ 𝑡𝑒𝑟𝑚𝑠 ( C)), thus 𝐵 𝑁 is dead by missing feature.

Instantiation 6 (Expressing code-Kconfig missing defects {20}). Same as inst. 5 with C = C Kconfig .

Instantiation 7 (Expressing referential defects {17}). If the feature is missing in the configuration space, then the definition corresponds def. 9 with C = C Kconfig as context. A feature missing in the implementation space can mean that the feature is used in the Make space only. It is characterized as a defect as [START_REF] Tartler | Feature consistency in compile-time-configurable system software: Facing the Linux 10,000 feature problem[END_REF] does not consider this space, but it is not a defect for us.

Model on Kbuild

At the Kbuild level, an asset 𝑠 = ⟨𝜙 𝑠𝑒𝑙𝑒𝑐𝑡 , 𝜙 𝑝𝑟𝑒𝑑𝑠 , 𝜙 𝑑𝑒𝑝𝐼𝑛𝑡 , 𝜙 𝑑𝑒𝑝𝐸𝑥𝑡 ⟩ can represent a C object file. We then express presence conditions and related anomalies with our model. As seen in section 2, an object is selected for compilation by being added to defined lists, with possible constraints on one or more features in case of multiple definitions. Before, objects can also be added to composite variables.

• 𝜙 𝑠𝑒𝑙𝑒𝑐𝑡 = 𝑓 𝑖 with 𝑓 𝑖 being features which at least one needs to be set for the source file to be selected. If the asset is always selected, 𝜙 𝑠𝑒𝑙𝑒𝑐𝑡 = 𝑡𝑟𝑢𝑒. If the asset is defined but never added to a list, 𝜙 𝑠𝑒𝑙𝑒𝑐𝑡 = 𝑓 𝑎𝑙𝑠𝑒 ;

• 𝜙 𝑝𝑟𝑒𝑑𝑠 = 𝑐𝑜𝑚𝑝 with 𝑐𝑜𝑚𝑝 the name of the composite variable if 𝑠 is part of a composite definition. 𝑐𝑜𝑚𝑝 must be selected ; • 𝜙 𝑑𝑒𝑝𝐼𝑛𝑡 = 𝑑𝑖𝑟 with 𝑑𝑖𝑟 the directory containing the source file represented by 𝑠 which also needs to be selected ; • 𝜙 𝑑𝑒𝑝𝐸𝑥𝑡 = 𝑡𝑟𝑢𝑒 as the selection of a source file only relies on its feature.

Expressing the assets from fig. 1.

• 𝑑𝑖𝑟 = ⟨𝐵𝐴𝑅, 𝑡𝑟𝑢𝑒, 𝑡𝑟𝑢𝑒, 𝑡𝑟𝑢𝑒⟩ • 𝑓 𝑜𝑜 = ⟨𝐹𝑂𝑂, 𝑡𝑟𝑢𝑒, 𝑑𝑖𝑟, 𝑡𝑟𝑢𝑒⟩ • 𝑓 𝑖𝑙𝑒_𝑎 = ⟨𝑡𝑟𝑢𝑒, 𝑓 𝑜𝑜, 𝑑𝑖𝑟, 𝑡𝑟𝑢𝑒⟩ • 𝑓 𝑖𝑙𝑒_𝑏 = ⟨𝑡𝑟𝑢𝑒, 𝑓 𝑜𝑜, 𝑑𝑖𝑟, 𝑡𝑟𝑢𝑒⟩ • 𝑓 𝑖𝑙𝑒_𝑐 = ⟨𝑡𝑟𝑢𝑒, 𝑡𝑟𝑢𝑒, 𝑑𝑖𝑟, 𝑡𝑟𝑢𝑒⟩
Expressing their presence conditions We can then express anom. {24} in our model:

P C 𝐼𝑛𝑡 (𝑑𝑖𝑟 ) = 𝜙 𝑠𝑒𝑙𝑒𝑐𝑡 𝑑𝑖𝑟 ∧ 𝑒𝑥𝑝𝑎𝑛𝑑 𝜙 𝑝𝑟𝑒𝑑𝑠 𝑑𝑖𝑟 ∧ 𝑒𝑥𝑝𝑎𝑛𝑑 𝜙 𝑑𝑒𝑝𝐼𝑛𝑡 𝑑𝑖𝑟 = 𝐵𝐴𝑅 ∧ 𝑡𝑟𝑢𝑒 ∧ 𝑡𝑟𝑢𝑒 = 𝐵𝐴𝑅 P C 𝐼𝑛𝑡 (𝑓 𝑜𝑜) = 𝐹𝑂𝑂 ∧ 𝑡𝑟𝑢𝑒 ∧ 𝑒𝑥𝑝𝑎𝑛𝑑 ( P C 𝐼𝑛𝑡 (𝑑𝑖𝑟 )) = 𝐹𝑂𝑂 ∧ 𝐵𝐴𝑅 P C 𝐼𝑛𝑡 (𝑓 𝑖𝑙𝑒_𝑎) = 𝑡𝑟𝑢𝑒 ∧ 𝑒𝑥𝑝𝑎𝑛𝑑 ( P C 𝐼𝑛𝑡 (𝑓 𝑜𝑜)) ∧ 𝑒𝑥𝑝𝑎𝑛𝑑 ( P C 𝐼𝑛𝑡 (𝑑𝑖𝑟 )) = (𝐹𝑂𝑂 ∧ 𝐵𝐴𝑅) ∧ 𝐵𝐴𝑅 P C 𝐼𝑛𝑡 (𝑓 𝑖𝑙𝑒_𝑏) = P C 𝐼𝑛𝑡 (𝑓 𝑖𝑙𝑒_𝑎) P C 𝐼𝑛𝑡 (𝑓 𝑖𝑙𝑒_𝑐) = 𝑡𝑟𝑢𝑒 ∧ 𝑡𝑟𝑢𝑒 ∧ 𝑒𝑥𝑝𝑎𝑛𝑑 ( P C 𝐼𝑛𝑡 (𝑑𝑖𝑟 )) = 𝐵𝐴𝑅
¬𝑠𝑎𝑡 (𝐹 𝑁 ∧ 𝑀 ∧ 𝐾) ⇔ ¬𝑠𝑎𝑡 (PC 𝐸𝑥𝑡 (𝑠)) ¬𝑠𝑎𝑡 (¬𝐹 𝑁 ∧ 𝑀 ∧ 𝐾) ⇔ ¬𝑠𝑎𝑡 (¬PC 𝐸𝑥𝑡 (𝑠))
anom. {24} thus expresses dead (def. 6) and core defects (def. 7).

Instantiation 11 (Expressing Make-Kconfig missing defects {25}). Same as inst. 5 with C = C Kconfig , and relying on formulas from inst. 10.

Model on Kconfig

Given the configurator model and the application example already given in section 4.2, we just have to instantiate the anomalies.

Instantiation 12 (Expressing dead feature {4}). Given 𝐹 a dead feature. The definition can be expressed in our model as ¬𝑠𝑎𝑡 (𝜙 𝑑𝑒𝑝𝑠 𝐹 ), which itself implies ¬𝑠𝑎𝑡 (PC(𝐹 )), hence 𝐹 is dead.

Instantiation 13 (Expressing false optional {5}). This definition corresponds to the note in def. 12, thus 𝐹 is a core feature.

Instantiation 14 (Expressing missing dead feature {6}). The definition limits the presence of an undefined feature in the dependencies:

(𝑚 ∈ 𝑡𝑒𝑟𝑚𝑠 (𝜙 𝑑𝑒𝑝𝑠 𝐹 )) ∧ (𝑚 ∉ F )
As 𝑡𝑒𝑟𝑚𝑠 (𝜙 𝑑𝑒𝑝𝑠 𝐹 ) ⊆ 𝑡𝑒𝑟𝑚𝑠 (PC(𝐹 )), every missing dead feature according to anom. {6} is also missing dead in our model.

Resulting coverage

From the instantiations of the configurator model on Kconfig and the derivator on both Kbuild and CPP, we obtain a complete expression of the different formulas and anomalies taken as input. A summary of the different anomalies for each paper and how they are expressed is presented in table 3. As expected, no existing proposal expresses defects in every space of the Linux build system. The table confirms the inconsistencies that we manually observed in section 3.6 between anom. {13} and anom. {15} from [START_REF] Tartler | Feature consistency in compile-time-configurable system software: Facing the Linux 10,000 feature problem[END_REF], with the first anomaly being characterized as a full-mandatory defect and the other as a core defect. Moreover, similar inconsistencies are exhibited in defects from [START_REF] Nadi | Mining Kbuild to detect variability anomalies in Linux[END_REF], as well as two anomalies that are described as dead defects but are not called as such (anom. {12,16}).

THREATS TO VALIDITY

Internal threats to validity. A first internal threat could be caused by the selection of papers made to devise the properties and the model. However, given the narrow focus of the subject and the fact that we sought additional work in the references of the obtained papers, we believe that the most important studies are included.

Another internal threat concerns the accuracy of the formalisms from the chosen studies, but their application to the kernel was demonstrated. Besides, while we provide a formalization, there is no proof of correctness of the formalism nor associated syntax and semantics given in a theorem prover. As future work, we plan to rather use modelling tools to extract representations of the different spaces in our model and reason on properties.

External threats to validity. While the application of the proposed models to the Linux build system is shown in the paper, there is no demonstration of the applicability of the configurator and derivator concepts to other build systems. A first demonstration of the derivator concept is nevertheless done through its double instantiation as the Kconfig and CPP preprocessor. Our future plan also includes building a generalized framework and applying it to other variability build systems [START_REF] Halin | Yo variability! JHipster: a playground for web-apps analyses[END_REF][START_REF] Kästner | A variabilityaware module system[END_REF][START_REF] Maudoux | Lessons and Pitfalls in Building Firefox with Tup[END_REF][START_REF] Mordahl | An empirical study of real-world variability bugs detected by variability-oblivious tools[END_REF].

CONCLUSION

The Linux kernel is a constant subject of study for the software variability research community. While many aspects of its build system have been studied, no uniform model encompassing all properties on the Kconfig, Kbuild, and CPP, has been proposed.

In this paper, we first examined the main studies on the kernel variability to propose a complete set of definitions for the analyzed properties. We exposed the differences in terminology and some inconsistencies in the interpretation of similar definitions in them. We then described a formalism based on the generic concepts of configurator and derivator to express the whole set of consistency properties. We showed that the configurator can be instantiated to represent the Kconfig, while the instantiated derivators can represent the Kbuild, selecting files, or CPP, selecting code blocks. The obtained model enables one to categorize the previous studies and to establish their coverage and divergences on the analyses.

As future work, we plan to implement a model-driven framework derived from the proposed models, in which one can plug extraction processes from software artifacts and consistency checking techniques related to some of the consistency properties. Then, we plan to apply the models on other complex variability build systems, such as Busybox [START_REF] Kästner | A variabilityaware module system[END_REF][START_REF] Mordahl | An empirical study of real-world variability bugs detected by variability-oblivious tools[END_REF], JHipster [START_REF] Halin | Yo variability! JHipster: a playground for web-apps analyses[END_REF], and MozBuild [START_REF] Maudoux | Lessons and Pitfalls in Building Firefox with Tup[END_REF], used on Firefox and other Mozilla projects. We expect the presented model and these extensions to enable practitioners, in the Linux community and in others, to incorporate the right consistency checking elements in their build system.

  Application to Kconfig. P C (𝐹𝑂𝑂) = 𝜙 𝑒𝑛𝑎𝑏𝑙𝑒 𝐹𝑂𝑂 ∧ 𝑒𝑥𝑝𝑎𝑛𝑑 (𝜙 𝑑𝑒𝑝𝑠 𝐹𝑂𝑂 ) ∨ 𝑑𝑖𝑟𝑒𝑐𝑡𝑆𝑒𝑙𝑒𝑐𝑡 (𝐹𝑂𝑂) = 𝑡𝑟𝑢𝑒 ∧ ( ( P C (𝐷𝐸𝑃𝑆_𝐴) ∨ P C (𝐷𝐸𝑃𝑆_𝐵)) ∧ P C (𝑀𝐸𝑁𝑈 _𝐶𝑂𝑁 𝐷)) = ( P C (𝐷𝐸𝑃𝑆_𝐴) ∨ P C (𝐷𝐸𝑃𝑆_𝐵)) ∧ P C (𝑀𝐸𝑁𝑈 _𝐶𝑂𝑁 𝐷) P C (𝐵𝐴𝑅) = 𝜙 𝑒𝑛𝑎𝑏𝑙𝑒 𝐵𝐴𝑅 ∧ 𝑒𝑥𝑝𝑎𝑛𝑑 (𝜙 𝑑𝑒𝑝𝑠 𝐵𝐴𝑅 ) ∨ 𝑑𝑖𝑟𝑒𝑐𝑡𝑆𝑒𝑙𝑒𝑐𝑡 (𝐵𝐴𝑅) = 𝑡𝑟𝑢𝑒 ∧ P C (𝑀𝐸𝑁𝑈 _𝐶𝑂𝑁 𝐷) = P C (𝑀𝐸𝑁𝑈 _𝐶𝑂𝑁 𝐷) P C (𝐹 _𝑆𝐸𝐿) = (𝑓 𝑎𝑙𝑠𝑒 ∧ 𝑡𝑟𝑢𝑒) ∨ P C (𝐹𝑂𝑂) = P C (𝐹𝑂𝑂)

  3, using for context C = C Kconfig ∪ C Kbuild . Thus, C Kconfig = 𝐾 and C Kbuild = 𝑀, and:𝑠𝑙𝑖𝑐𝑒 (C Kconfig , 𝑡𝑒𝑟𝑚𝑠 (PC 𝐼𝑛𝑡 (𝑎)) ∪ 𝑡𝑒𝑟𝑚𝑠 (𝜙 𝑑𝑒𝑝𝐸𝑥𝑡 𝑎 )) |= 𝐾 𝑠𝑙𝑖𝑐𝑒 (C Kbuild , 𝑡𝑒𝑟𝑚𝑠 (PC 𝐼𝑛𝑡 (𝑎)) ∪ 𝑡𝑒𝑟𝑚𝑠 (𝜙 𝑑𝑒𝑝𝐸𝑥𝑡 𝑎 )) |= 𝑀We can then express the different formulas in our model. Instantiation 1 (Expressing code-Make-Kconfig anomalies {22}). ¬𝑠𝑎𝑡 (𝐵 𝑁 ∧ 𝐶 ∧ 𝑀 ∧ 𝐾) ⇔ ¬𝑠𝑎𝑡 (PC 𝐼𝑛𝑡 (𝐵 𝑁 ) ∧ C) ⇔ ¬𝑠𝑎𝑡 (PC 𝐸𝑥𝑡 (𝐵 𝑁 )) (𝑑𝑒 𝑓 . 3) ¬𝑠𝑎𝑡 (¬𝐵 𝑁 ∧ 𝑝𝑎𝑟𝑒𝑛𝑡 (𝐵 𝑁 ) ∧ 𝐶 ∧ 𝑀 ∧ 𝐾) ⇔ ¬𝑠𝑎𝑡 (C ∧ ¬PC 𝐼𝑛𝑡 (𝐵 𝑁 ) ∧ 𝑒𝑥𝑝𝑎𝑛𝑑 (𝜙 𝑑𝑒𝑝𝐼𝑛𝑡 𝐵 𝑁

Instantiation 15 (

 15 Expressing configuration-only defects {16}). The function 𝑝𝑟𝑒𝑠𝑒𝑛𝑐𝑒𝐶𝑜𝑛𝑑𝑖𝑡𝑖𝑜𝑛(𝑓 𝑒𝑎𝑡𝑢𝑟𝑒) returns the presence implication of the feature and is defined by the authors as "the selection of the feature itself and the expression of the depends on option." This definition, expressed by our model, corresponds to 𝜙 𝑒𝑛𝑎𝑏𝑙𝑒 𝑓 ∧ 𝑒𝑥𝑝𝑎𝑛𝑑 (𝜙 𝑑𝑒𝑝𝑠 𝑓 ) = PC(𝑓 ). Thus¬𝑠𝑎𝑡 (𝑓 → 𝑝𝑟𝑒𝑠𝑒𝑛𝑐𝑒𝐶𝑜𝑛𝑑𝑖𝑡𝑖𝑜𝑛(𝑓 )) ⇔ ¬𝑠𝑎𝑡 (PC(𝑓 ))Therefore, 𝑓 is dead.

Table 1 :

 1 Notation and terminologies mapping for the three spaces in selected papers

	Paper	Kconfig files	Kbuild Makefiles	CPP / Source files
	[31]	Kconfig space	Make space	Code space
		K	M	C
	[15]	Feature Modeling Configuration	Build system	Generator Preprocessor
	[30]	Configuration space	Compilation space	Implementation space
	[44]	Problem space Model	/	Solution space Implementation
		K	/	C
	[45]	Configuration space C	/ /	Implementation space I

  𝜙 𝑑𝑒𝑝𝐼𝑛𝑡 = 𝑝 with 𝑝 the parent block of 𝑏 if 𝑏 is a nested block.• 𝜙 𝑑𝑒𝑝𝐸𝑥𝑡 = 𝑓 𝑖𝑙𝑒 the file containing 𝑏.

is an #elsif or #else block, 𝑏 𝑖 represents the corresponding #if block and the potential #elsif blocks before 𝑏 ; •

  Definition 6. (Externally dead asset) An asset 𝑎 is an externally dead asset if it is never selected due to inconsistencies with its context. The set of externally dead assets of A is noted 𝑑𝑒𝑎𝑑𝑠𝐸𝑥𝑡 (A).Definition 7 (Externally core asset). An asset 𝑎 of A is an externally core asset if it is always selected independently of the constraints of the context. The set of core assets of A is noted 𝑐𝑜𝑟𝑒𝐸𝑥𝑡 (A).

	4.1.2 External consistency.
	𝑎 ∈ 𝑑𝑒𝑎𝑑𝑠𝐸𝑥𝑡 (A) ⇔ ¬𝑠𝑎𝑡 (PC 𝐸𝑥𝑡 (𝑎))

𝑎 ∈ 𝑐𝑜𝑟𝑒𝐸𝑥𝑡 (A) ⇔ ¬𝑠𝑎𝑡 (¬(PC 𝐸𝑥𝑡 (𝑎))) Definition 8. (Externally full-mandatory asset) An asset 𝑎 is an externally full-mandatory asset if the selection of its parent dependencies implies its selection due to the formulas in its context. The set of externally full-mandatory assets of A is noted 𝑚𝑎𝑛𝑑𝐸𝑥𝑡 (A).

𝑎 ∈ 𝑚𝑎𝑛𝑑𝐸𝑥𝑡 (A) ⇔ 𝑒𝑥𝑝𝑎𝑛𝑑 (𝜙 𝑑𝑒𝑝𝐼𝑛𝑡 𝑎 ) → PC 𝐸𝑥𝑡 (𝑎) ⇔ ¬𝑠𝑎𝑡 (¬PC 𝐸𝑥𝑡 (𝑎) ∧ 𝑒𝑥𝑝𝑎𝑛𝑑 (𝜙 𝑑𝑒𝑝𝐼𝑛𝑡 𝑎 ))

Definition 9. (Missing dead asset) An asset 𝑎 is missing dead if a feature in its presence condition is not defined in the context C.

The set of assets of A with missing features is noted 𝑚𝑖𝑠𝑠𝑖𝑛𝑔(A).

𝑎 ∈ 𝑚𝑖𝑠𝑠𝑖𝑛𝑔(A) ⇔ ∃𝑚 ∈ 𝑡𝑒𝑟𝑚𝑠 (PC 𝐸𝑥𝑡 (𝑎)) | (𝑚 ∉ 𝑡𝑒𝑟𝑚𝑠 (C))

Table 2 :

 2 Truth table for 𝜙 𝑒𝑛𝑎𝑏𝑙𝑒 from a Kconfig feature Presence of prompt Presence of default 𝜙 𝑒𝑛𝑎𝑏𝑙𝑒

	yes	activated not activated	𝑡𝑟𝑢𝑒 𝑡𝑟𝑢𝑒
	no	activated not activated	𝑡𝑟𝑢𝑒 𝑓 𝑎𝑙𝑠𝑒

  Instantiation 8 (Expressing Feature Not Defined {11}). Given 𝑚 a feature not being defined in any Kconfig files, and 𝑎 a file referenced a Kbuild Makefile whose presence is conditioned by 𝑚.As 𝑡𝑒𝑟𝑚𝑠 (𝜙 𝑠𝑒𝑙𝑒𝑐𝑡𝑎 𝑖 ) ⊆ 𝑡𝑒𝑟𝑚𝑠 (PC 𝐸𝑥𝑡 (𝑎 𝑖 )), anom. {11} is a special case of def. 9, therefore 𝑎 is a missing dead file.Instantiation 9 (Expressing Variable Not Used {12}). Given 𝑎 an asset and 𝜙 𝑝𝑟𝑒𝑑𝑠 𝑎 = 𝑐𝑜𝑚𝑝. 𝑎 is an unused variable if ¬𝜙 𝑠𝑒𝑙𝑒𝑐𝑡 𝑐𝑜𝑚𝑝 , and ¬𝜙 𝑠𝑒𝑙𝑒𝑐𝑡𝑐𝑜𝑚𝑝 → ¬P C (𝑐𝑜𝑚𝑝) → ¬𝑒𝑥𝑝𝑎𝑛𝑑𝑠 (𝜙 𝑝𝑟𝑒𝑑𝑠𝑎 ) → ¬P C (𝑎). Thus, 𝑎 is a dead asset.Instantiation 10 (Expressing Make-Kconfig anomalies {24}). Let us consider 𝑠 the asset that represents the file 𝐹 𝑁 , and C = C Kconfig .PC 𝐼𝑛𝑡 (𝑠) = 𝜙 𝑠𝑒𝑙𝑒𝑐𝑡 𝑠 ∧ 𝑒𝑥𝑝𝑎𝑛𝑑 𝜙 𝑝𝑟𝑒𝑑𝑠 𝑠 ∧ 𝑒𝑥𝑝𝑎𝑛𝑑 𝜙 𝑑𝑒𝑝𝐼𝑛𝑡 𝑠 = 𝜙 𝑠𝑒𝑙𝑒𝑐𝑡 𝑠 ∧ PC 𝐼𝑛𝑡 (𝑐𝑜𝑚𝑝) ∧ PC 𝐼𝑛𝑡 (𝑑𝑖𝑟 )To build 𝑀 as it appears in anom. {24}, Nadi and Holt[START_REF] Nadi | Mining Kbuild to detect variability anomalies in Linux[END_REF] extract for every file a presence condition consisting of a conjunction of the features conditioning the selection of the file ( 𝑓 𝑖 = 𝜙 𝑠𝑒𝑙𝑒𝑐𝑡 𝑠 ), the composite object if present (PC 𝐼𝑛𝑡 (𝑐𝑜𝑚𝑝)) and its parent directory (PC 𝐼𝑛𝑡 (𝑑𝑖𝑟 )) in the corresponding Makefiles. Therefore, PC 𝐼𝑛𝑡 (𝑠) |= (𝐹 𝑁 ∧ 𝑀).

Thus, 𝑚 is present in 𝜙 𝑠𝑒𝑙𝑒𝑐𝑡 𝑎 , however is not present in the features defined in the Kconfig files, obtained with 𝑡𝑒𝑟𝑚𝑠 (C Kconfig ).

(𝑚 ∈ 𝑡𝑒𝑟𝑚𝑠 (𝜙 𝑠𝑒𝑙𝑒𝑐𝑡 𝑎 )) ∧ (𝑚 ∉ 𝑡𝑒𝑟𝑚𝑠 (C Kconfig )) P C 𝐸𝑥𝑡 (𝑠) = P C 𝐼𝑛𝑡 (𝑠) ∧ 𝑠𝑙𝑖𝑐𝑒 ( C, 𝑡𝑒𝑟𝑚𝑠 ( P C 𝐼𝑛𝑡 (𝑠)) ∪ 𝑡𝑒𝑟𝑚𝑠 (𝜙 𝑑𝑒𝑝𝐸𝑥𝑡𝑠 )) |= (𝐹 𝑁 ∧ 𝑀) ∧ 𝐾 (cf. 𝑠𝑒𝑐𝑡𝑖𝑜𝑛 5.1.2)

Table 3 :

 3 Anomalies covered by the model (defects defined as dead and undead according to the authors)

		Paper		Sincero et al. [44]	Tartler et al. [45]	Nadi and Holt [30]	Nadi and Holt [31]	Hengelein [15]
		Internal	Dead	anom. {2}	anom. {14}	anom. {12}	anom. {18}
		consistency	Core	anom. {2}	anom. {14}		anom. {18}
	Derivator	External	Dead	anom. {1,3}	anom. {13,15}		anom. {19,21,22,24}
		consistency	Core	anom. {3}	anom. {15}		anom. {24}
		Full-mandatory		anom. {13}		anom. {19,21,22}
		Missing feature		anom. {17}	anom. {11}	anom. {20,23,25}
		Dead			anom. {16}		anom. {4}
	Configurator	Core					anom. {5}
		Missing dead				anom. {6}
	Other properties (e.g., unreachable symbol, file not used)			anom. {10}	anom. {7,8,9}

https://www.kernel.org/doc/html/latest/kbuild/kconfig-language.html#menustructure

In the remainder of this paper, we will refer to it as 𝑠𝑎𝑡 ().

For example, although Kconfig's syntax allows adding conditions to select statements, no defect described in our model requires to express this behaviour.