Johann Mortara

Philippe Collet

Capturing the diversity of analyses on the Linux kernel variability Companion

published or not. The documents may come

Fig. 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] 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

Alongside the selected studies characterizing anomalies in the Linux build system, plethora of work describe it as they study some aspects of the Linux kernel (such as the evolution of its model [START_REF] Passos | Coevolution of variability models and related artifacts: A case study from the Linux kernel[END_REF]), or use it as a case study [START_REF] Abal | 42 variability bugs in the linux kernel: a qualitative analysis[END_REF] or a benchmark for tools [START_REF] El-Sharkawy | An Empirical Study of Configuration Mismatches in Linux[END_REF]. Table 1 summarizes, for the papers found by our query, the different terminologies used to refer to the different parts of the build system (namely, Kconfig and its files, Kbuild and its Makefiles, and CPP directives in source files). Except for a journal extension [START_REF] Nadi | Variability Anomalies in Software Product Lines[END_REF] and a PhD thesis [START_REF] Tartler | Mastering variability challenges in Linux and related highly-configurable system software[END_REF], every paper has its own terminology, and some of them even use multiple terminologies ( [START_REF] Abal | 42 variability bugs in the linux kernel: a qualitative analysis[END_REF][START_REF] Hengelein | Analyzing the Internal Consistency of the Linux KConfig Model[END_REF][START_REF] Tartler | Mastering variability challenges in Linux and related highly-configurable system software[END_REF][START_REF] Tartler | Feature consistency in compile-time-configurable system software: Facing the Linux 10,000 feature problem[END_REF]). One paper [START_REF] El-Sharkawy | An Empirical Study of Configuration Mismatches in Linux[END_REF] groups the Kbuild and CPP in a single Solution space, denomination used by Abal et al. [START_REF] Abal | 42 variability bugs in the linux kernel: a qualitative analysis[END_REF] and Sincero et al. [START_REF] Sincero | Efficient extraction and analysis of preprocessor-based variability[END_REF] to refer only to the CPP constraints.

In the papers we selected for study, we noticed redundant expressions of anomalies. However, the variables used to represent the different spaces diverge, hampering the comprehension of the expressed defects between the work. A summary of the different notations encountered is showed in table 2.

MODEL

As presented in the paper, deriving a variant of the Linux build system is done in three stages. First, a subset of the features defined in the Kconfig files are selected, either by the user or by constraints, and form a valid configuration of

Paper

Properties CPP Make Kconfig Sincero et al. [START_REF] Sincero | Efficient extraction and analysis of preprocessor-based variability[END_REF] anom. {1} C / K Tartler et al. [START_REF] Tartler | Feature consistency in compile-time-configurable system software: Facing the Linux 10,000 feature problem[END_REF] anom. {13} I / C Nadi and Holt [START_REF] Nadi | Mining Kbuild to detect variability anomalies in Linux[END_REF] anom. {19,21,22,24} C M K the Linux kernel. These features are then used in the Kbuild Makefiles to select the files from the code base which will be added for compilation, and by the C preprocessor (CPP) to select parts of these files.

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 ; • 𝜙 𝑑𝑒𝑝𝐸𝑥𝑡 = 𝑓 𝑖𝑙𝑒 the file containing 𝑏.

• 𝜙 𝑝𝑟𝑒𝑑𝑠 = ¬( 𝑖 𝑏 𝑖 ) if 𝑏
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:

• 𝑓 𝑖𝑙𝑒 = ⟨𝑡𝑟𝑢𝑒, 𝑡𝑟𝑢𝑒, 𝑡𝑟𝑢𝑒, 𝑡𝑟𝑢𝑒⟩

• 𝑏 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

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 → (¬𝐹𝑂𝑂)) ∧ ( 𝑓 𝑖𝑙𝑒 ↔ 𝐹𝑂𝑂))
3.1.1 Internal consistency. To express defects, we define dead, core, and full-mandatory assets, relying on definitions of dead and false-optional 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 𝐼𝑛𝑡 (𝑎)))
3.1.2 External consistency.

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).

𝑎 ∈ 𝑑𝑒𝑎𝑑𝑠𝐸𝑥𝑡 (A) ⇔ ¬𝑠𝑎𝑡 (PC 𝐸𝑥𝑡 (𝑎))
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).

𝑎 ∈ 𝑐𝑜𝑟𝑒𝐸𝑥𝑡 (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))
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 1, 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

P C 𝐼𝑛𝑡 (𝑑𝑖𝑟 ) = 𝜙 𝑠𝑒𝑙𝑒𝑐𝑡 𝑑𝑖𝑟 ∧ 𝑒𝑥𝑝𝑎𝑛𝑑 𝜙 𝑝𝑟𝑒𝑑𝑠 𝑑𝑖𝑟 ∧ 𝑒𝑥𝑝𝑎𝑛𝑑 𝜙 𝑑𝑒𝑝𝐼𝑛𝑡 𝑑𝑖𝑟 = 𝐵𝐴𝑅 ∧ 𝑡𝑟𝑢𝑒 ∧ 𝑡𝑟𝑢𝑒 = 𝐵𝐴𝑅 P C 𝐼𝑛𝑡 (𝑓 𝑜𝑜) = 𝐹𝑂𝑂 ∧ 𝑡𝑟𝑢𝑒 ∧ 𝑒𝑥𝑝𝑎𝑛𝑑 ( P C 𝐼𝑛𝑡 (𝑑𝑖𝑟 )) = 𝐹𝑂𝑂 ∧ 𝐵𝐴𝑅 P C 𝐼𝑛𝑡 (𝑓 𝑖𝑙𝑒_𝑎) = 𝑡𝑟𝑢𝑒 ∧ 𝑒𝑥𝑝𝑎𝑛𝑑 ( P C 𝐼𝑛𝑡 (𝑓 𝑜𝑜)) ∧ 𝑒𝑥𝑝𝑎𝑛𝑑 ( P C 𝐼𝑛𝑡 (𝑑𝑖𝑟 )) = (𝐹𝑂𝑂 ∧ 𝐵𝐴𝑅) ∧ 𝐵𝐴𝑅 P C 𝐼𝑛𝑡 ( 𝑓 𝑖𝑙𝑒_𝑏) = P C 𝐼𝑛𝑡 (𝑓 𝑖𝑙𝑒_𝑎) P C 𝐼𝑛𝑡 (𝑓 𝑖𝑙𝑒_𝑐) = 𝑡𝑟𝑢𝑒 ∧ 𝑡𝑟𝑢𝑒 ∧ 𝑒𝑥𝑝𝑎𝑛𝑑 ( P C 𝐼𝑛𝑡 (𝑑𝑖𝑟 )) = 𝐵𝐴𝑅

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 3 ; • 𝜙 𝑑𝑒𝑝𝑠 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.

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 (𝐹𝑂𝑂)
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 Kconfig2 .

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 ) 3.2.2 Expressing cross-space formulas. Nadi and Holt [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 𝑒𝑥𝑝𝑎𝑛𝑑 (𝜙 𝑑𝑒𝑝𝐼𝑛𝑡 𝐵 𝑁

) 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. 𝑛𝑜𝑃𝑟𝑒𝑑𝑒𝑐𝑒𝑠𝑠𝑜𝑟𝑠 (𝑏 𝑖 ) Given 𝑏 𝑖 , 𝑛𝑜𝑃𝑟𝑒𝑑𝑒𝑐𝑒𝑠𝑠𝑜𝑟𝑠 (𝑏 𝑖 ) returns the negation of the disjunction of all its predecessors (logical variables representing blocks) in an if-group. Example: For the block B4 of fig. 1 𝑛𝑜𝑃𝑟𝑒𝑑𝑒𝑐𝑒𝑠𝑠𝑜𝑟𝑠 (𝑏 4 )

returns ¬(𝑏 2 ∨ 𝑏 3 ).

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 3.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.

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 problem 3 .

Instantiation 1 (Dead block {1}). Same as inst. 13.

Anomaly 2 (Internal consistency [START_REF] Sincero | Efficient extraction and analysis of preprocessor-based variability[END_REF]). Internal consistency is defined as checking for each block of a compilation unit if it is selectable by at least one valid configuration. This property is checked with 𝑠𝑎𝑡𝑖𝑠 𝑓 𝑖𝑎𝑏𝑙𝑒 (𝐶 𝑢 ∧ 𝑏 𝑖 ) which, expanded using the definition of 𝐶 𝑢 , gives: 𝑠𝑎𝑡𝑖𝑠 𝑓 𝑖𝑎𝑏𝑙𝑒 as done 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. {14}. Thus, anom. {2} ⇔ anom. {14}.

Anomaly 3 (External consistency [START_REF] Sincero | Efficient extraction and analysis of preprocessor-based variability[END_REF]). External consistency is defined as checking for each block of a compilation unit if it is selectable by at least one valid configuration. This property is checked with 𝑠𝑎𝑡𝑖𝑠 𝑓 𝑖𝑎𝑏𝑙𝑒 (𝐶 𝑢 ∧ 𝑏 𝑖 ∧ 𝐹 𝑀) (with 𝐹 𝑀 the representation of the feature model in a boolean formula) which, expanded using the definition of 𝐶 𝑢 , gives:

𝑠𝑎𝑡𝑖𝑠 𝑓 𝑖𝑎𝑏𝑙𝑒 𝑖=1..𝑚 𝑏 𝑖 ↔ PC(𝑏 𝑖 ) ∧ 𝑏 𝑖 ∧ 𝐹 𝑀
Instantiation 3 (Expressing External consistency {3}). In inst. 2, we showed:

𝑖=1..𝑚 𝑏 𝑖 ↔ PC(𝑏 𝑖 ) ∧ 𝑏 𝑖 ⇔ (𝑏 𝑖 ↔ PC(𝑏 𝑖 ))
𝐹 𝑀 in anom. {3} and V in anom. {15} both represent the Kconfig space constraints. Therefore:

𝑠𝑎𝑡𝑖𝑠 𝑓 𝑖𝑎𝑏𝑙𝑒 𝑖=1..𝑚 𝑏 𝑖 ↔ PC(𝑏 𝑖 ) ∧ 𝑏 𝑖 ∧ 𝐹 𝑀 ⇔ 𝑠𝑎𝑡 ((𝑏 𝑖 ↔ PC(𝑏 𝑖 )) ∧ V)
i.e., anom. {3} ⇔ anom. {15}.

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.

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

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.

Instantiation 5 (Expressing false optional {5}

). This definition corresponds to the note in def. 12, thus 𝐹 is a core feature.

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.

Instantiation 6 (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.

Anomaly 7 (Selects on Symbols with Dependencies [START_REF] Hengelein | Analyzing the Internal Consistency of the Linux KConfig Model[END_REF]). select statements should not be used to select symbols matching the following conditions:

• The Symbol has dependencies

• The Symbol is selected by another symbol Instantiation 7 (Expressing selects on symbols with dependencies {7}).

(𝑡𝑒𝑟𝑚𝑠 (𝜙 𝑑𝑒𝑝𝑠 𝐹 ) ≠ ∅) ∧ 𝑑𝑖𝑟𝑒𝑐𝑡𝑆𝑒𝑙𝑒𝑐𝑡 (𝐹 )
Anomaly 8 (Unreachable symbol [START_REF] Hengelein | Analyzing the Internal Consistency of the Linux KConfig Model[END_REF]). A symbol is unreachable if:

• The symbol is invisible (does not have a prompt)

• The symbol is not selected by another symbol

• The symbol does not have a default value (or just default values with the value "n") Instantiation 8 (Expressing unreachable symbol {8}). Given 𝐹 a symbol. If the symbol does not have a prompt neither a default value allowing its selection, then ¬𝑠𝑎𝑡 (𝜙 𝑒𝑛𝑎𝑏𝑙𝑒 𝐹 ). Selection by another feature is modeled with 𝑑𝑖𝑟𝑒𝑐𝑡𝑆𝑒𝑙𝑒𝑐𝑡 (𝐹 ).

Thus: ¬𝑠𝑎𝑡 (𝜙 𝑒𝑛𝑎𝑏𝑙𝑒 𝐹 ) ∧ ¬𝑑𝑖𝑟𝑒𝑐𝑡𝑆𝑒𝑙𝑒𝑐𝑡 (𝐹 )

Anomaly 9 (Unnecessary Selects on Choice Values [START_REF] Hengelein | Analyzing the Internal Consistency of the Linux KConfig Model[END_REF]). select statements are unnecessary on symbols matching the following conditions:

• The Symbol is a choice value

• The Symbol is selected by another symbol Instantiation 9 (Expressing unnecessary selects on choice values {9}). To express this defect, we need to add an extra 𝑡𝑦𝑝𝑒 attribute to the feature. 𝑡𝑦𝑝𝑒 ∈ {𝑐𝑜𝑛𝑓 𝑖𝑔, 𝑐ℎ𝑜𝑖𝑐𝑒} represents the way 𝐹 is defined in the Kconfig model, either as a simple 𝑐𝑜𝑛𝑓 𝑖𝑔 element or in a 𝑐ℎ𝑜𝑖𝑐𝑒 statement.

(𝑡𝑦𝑝𝑒 𝐹 = 𝑐ℎ𝑜𝑖𝑐𝑒) ∧ 𝑑𝑖𝑟𝑒𝑐𝑡𝑆𝑒𝑙𝑒𝑐𝑡 (𝐹 )
Anomaly 10 (File Not Used (implementation-compilation consistency) [START_REF] Nadi | Mining Kbuild to detect variability anomalies in Linux[END_REF]). A .c file exists in the directory but is not used in the Makefile of that directory.

Instantiation 10 (Expressing File Not Used {10}). This definition may not be valid anymore, since the syntax of Kbuild Makefiles allows them to explore subdirectories too 4 . However, we can generalise this definition with: A .c file exists in the codebase but is not used in any Makefile.

Given 𝑆 the set of source files of the Linux kernel code base, and A Kbuild the set of assets representing source files in the Kbuild Makefiles. A file 𝑠 ∈ 𝑆 is a file not used if no asset in A Kbuild corresponds to 𝑠:

𝑎 𝑖 ∈ A Kbuild | 𝑠 ≡ 𝑎 𝑖
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.

Instantiation 11 (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 𝑚. Thus, 𝑚 is present in 𝜙 𝑠𝑒𝑙𝑒𝑐𝑡 𝑎 , however is not present in the features defined in the Kconfig files, obtained with 𝑡𝑒𝑟𝑚𝑠 (C Kconfig ).

(𝑚 ∈ 𝑡𝑒𝑟𝑚𝑠 (𝜙 𝑠𝑒𝑙𝑒𝑐𝑡 𝑎 )) ∧ (𝑚 ∉ 𝑡𝑒𝑟𝑚𝑠 (C Kconfig ))

As 𝑡𝑒𝑟𝑚𝑠 (𝜙 𝑠𝑒𝑙𝑒𝑐𝑡𝑎 𝑖 ) ⊆ 𝑡𝑒𝑟𝑚𝑠 (PC 𝐸𝑥𝑡 (𝑎 𝑖 )), anom. {11} is a special case of def. 9, therefore 𝑎 is a missing dead file.

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.

Instantiation 12 (Expressing Variable Not Used {12}). Given 𝑎 an asset and 𝜙 𝑝𝑟𝑒𝑑𝑠 𝑎 = 𝑐𝑜𝑚𝑝. 𝑎 is an unused variable if ¬𝜙 𝑠𝑒𝑙𝑒𝑐𝑡 𝑐𝑜𝑚𝑝 , and ¬𝜙 𝑠𝑒𝑙𝑒𝑐𝑡𝑐𝑜𝑚𝑝 → ¬P C (𝑐𝑜𝑚𝑝) → ¬𝑒𝑥𝑝𝑎𝑛𝑑𝑠 (𝜙 𝑝𝑟𝑒𝑑𝑠𝑎 ) → ¬P C (𝑎). Thus, 𝑎 is a dead asset.

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.

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

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}). Implementation-only defects [. . . ] represent code blocks that cannot be selected regardless of the systems' selected features; the structure of the source file itself contains contradictions that impede the selection of a block. This can be determined by checking the satisfiability of the formula 𝑠𝑎𝑡 (𝑏 𝑖 ↔ PC(𝑏 𝑖 )). We can infer the expressions for dead and undead implementation-only defects.

dead: ¬𝑠𝑎𝑡 (𝑏 𝑖 ↔ PC(𝑏 𝑖 ))

undead: ¬𝑠𝑎𝑡 (¬ (𝑏 𝑖 ↔ PC(𝑏 𝑖 )))

Instantiation 14 (Expressing Implementation-only defects {14}). Given B the set of blocks:

¬𝑠𝑎𝑡 (𝑏 𝑖 ↔ PC 𝑆𝑖𝑛 (𝑏 𝑖 )) ⇔ ¬𝑠𝑎𝑡 (PC 𝐼𝑛𝑡 (𝑏 𝑖 )) ⇔ 𝑏 𝑖 ∈ 𝑑𝑒𝑎𝑑𝑠 (B) (𝑑𝑒 𝑓 . 4) ¬𝑠𝑎𝑡 (¬ (𝑏 𝑖 ↔ PC 𝑆𝑖𝑛 (𝑏 𝑖 ))) ⇔ ¬𝑠𝑎𝑡 (¬ (PC 𝐼𝑛𝑡 (𝑏 𝑖 ))) ⇔ 𝑏 𝑖 ∈ 𝑐𝑜𝑟𝑒 (B) (𝑑𝑒 𝑓 . 5)
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 configurationimplementation defects.

dead: ¬𝑠𝑎𝑡 ((𝑏 𝑖 ↔ PC(𝑏 𝑖 )) ∧ V)

undead: ¬𝑠𝑎𝑡 (¬ (𝑏 𝑖 ↔ PC(𝑏 𝑖 )) ∧ V)

with V the propositional formula representing the configuration space (i.e., the feature model of Kconfig).

Instantiation 15 (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).

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.

Instantiation 16 (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.

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.

Instantiation 17 (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.

Anomaly 18 (Code anomalies [START_REF] Nadi | Mining Kbuild to detect variability anomalies in Linux[END_REF]). Code anomalies are defined as "Conflicting code constraints" and are not expressed in the paper as they are already determined by the Undertaker tool designed in [START_REF] Tartler | Feature consistency in compile-time-configurable system software: Facing the Linux 10,000 feature problem[END_REF]. Thus, formulas to detect these anomalies are the ones from anom. {2} and anom. {14}.

Instantiation 18 (Expressing code anomalies {18}). Same as inst. 2.

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.

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

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.

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

Anomaly 21 (Code-Make [START_REF] Nadi | Mining Kbuild to detect variability anomalies in Linux[END_REF]). Code-Make anomalies are defined as "Code constraints are not consistent with constraints in Makefiles". Although their formulas are not given in the paper, we can deduce them from anom. {19}:

𝐷𝑒𝑎𝑑 𝐵 𝑁 = ¬𝑠𝑎𝑡 (𝐵𝑙𝑜𝑐𝑘 𝑁 ∧ 𝐶 ∧ 𝑀) 𝑈 𝑛𝑑𝑒𝑎𝑑 𝐵 𝑁 = ¬𝑠𝑎𝑡 (¬𝐵𝑙𝑜𝑐𝑘 𝑁 ∧ 𝑝𝑎𝑟𝑒𝑛𝑡 (𝐵𝑙𝑜𝑐𝑘 𝑁 ) ∧ 𝐶 ∧ 𝑀)
Instantiation 21 (Expressing code-Make defects {21}). Same as inst. 22 with C = C Kbuild .

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: anom. {22} thus expresses dead (def. 6) and full-mandatory defects (def. 8).

𝐷𝑒𝑎𝑑 𝐵 𝑁 =
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".

Instantiation 23 (Expressing code-Make-Kconfig missing defects {23}). We showed in inst. 22 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.

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.

𝐷𝑒𝑎𝑑 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

In section 3 . 1 ,

 31 we instantiate on CPP the definition of external presence condition given in def. 3, using for context C = C Kconfig ∪ C Kbuild . Thus, C Kconfig = 𝐾 and C Kbuild = 𝑀, and:𝑠𝑙𝑖𝑐𝑒 (C Kconfig , 𝑡𝑒𝑟𝑚𝑠 (PC 𝐼𝑛𝑡 (𝑎)) ∪ 𝑡𝑒𝑟𝑚𝑠 (𝜙 𝑑𝑒𝑝𝐸𝑥𝑡 𝑎 )) |= 𝐾 𝑠𝑙𝑖𝑐𝑒 (C Kbuild , 𝑡𝑒𝑟𝑚𝑠 (PC 𝐼𝑛𝑡 (𝑎)) ∪ 𝑡𝑒𝑟𝑚𝑠 (𝜙 𝑑𝑒𝑝𝐸𝑥𝑡 𝑎 )) |= 𝑀4 DEFINITIONSPresence Condition[START_REF] Sincero | Efficient extraction and analysis of preprocessor-based variability[END_REF]:PC(𝑏 𝑖 ) = 𝑒𝑥𝑝𝑟𝑒𝑠𝑠𝑖𝑜𝑛(𝑏 𝑖 ) ∧ 𝑛𝑜𝑃𝑟𝑒𝑑𝑒𝑐𝑒𝑠𝑠𝑜𝑟𝑠 (𝑏 𝑖 ) ∧ 𝑝𝑎𝑟𝑒𝑛𝑡 (𝑏 𝑖 )with 𝑒𝑥𝑝𝑟𝑒𝑠𝑠𝑖𝑜𝑛(𝑏 𝑖 ) Given a block 𝑏 𝑖 , the function 𝑒𝑥𝑝𝑟𝑒𝑠𝑠𝑖𝑜𝑛(𝑏 𝑖 ) returns the logical expression as specified in the block declaration. Example: For the block B1 in fig.1, the function 𝑒𝑥𝑝𝑟𝑒𝑠𝑠𝑖𝑜𝑛(𝑏 1 ) returns: 𝐴 ∨ 𝐵 ∨ 𝐶.𝑝𝑎𝑟𝑒𝑛𝑡 (𝑏 𝑖 ) Given 𝑏 𝑖 , 𝑝𝑎𝑟𝑒𝑛𝑡 (𝑏 𝑖 ) returns the logical variable that represents the selection of its parent. If the block is not nested in any other block, then the result is always true. Example: For the block B3 in fig.1, the function returns: 𝑏 1 .

  𝑖=1..𝑚 𝑏 𝑖 ↔ PC(𝑏 𝑖 ) ∧ 𝑏 𝑖 Instantiation 2 (Expressing Internal consistency {2}). 𝑖=1..𝑚 𝑏 𝑖 ↔ PC(𝑏 𝑖 ) corresponds to the set of constraints of the code space, and 𝑏 𝑖 the selection of the 𝑏 𝑖 block. Therefore, 𝑖=1..𝑚 𝑏 𝑖 ↔ PC(𝑏 𝑖 ) ∧ 𝑏 𝑖 can be simplified to 𝑏 𝑖 ↔ PC(𝑏 𝑖 ),

  𝐹 𝑁 = ¬𝑠𝑎𝑡 (𝐹𝑖𝑙𝑒 𝑁 ∧ 𝑀 ∧ 𝐾) 𝑈 𝑛𝑑𝑒𝑎𝑑 𝐹 𝑁 = ¬𝑠𝑎𝑡 (¬𝐹𝑖𝑙𝑒 𝑁 ∧ 𝑀 ∧ 𝐾)Instantiation 24 (Expressing Make-Kconfig anomalies {24}). Let us consider 𝑠 the asset that represents the file 𝐹 𝑁 , and C = C Kconfig .PC 𝐼𝑛𝑡 (𝑠) = 𝜙 𝑠𝑒𝑙𝑒𝑐𝑡 𝑠 ∧ 𝑒𝑥𝑝𝑎𝑛𝑑 𝜙 𝑝𝑟𝑒𝑑𝑠 𝑠 ∧ 𝑒𝑥𝑝𝑎𝑛𝑑 𝜙 𝑑𝑒𝑝𝐼𝑛𝑡 𝑠 = 𝜙 𝑠𝑒𝑙𝑒𝑐𝑡 𝑠 ∧ PC 𝐼𝑛𝑡 (𝑐𝑜𝑚𝑝) ∧ PC 𝐼𝑛𝑡 (𝑑𝑖𝑟 )

Table 1 .

 1 Terminologies for each space of the Linux build system

	Paper	Kconfig files	Kbuild Makefiles	CPP / Source files
	Tartler et al. [18]	Model level	Generation level	Source code level
	Tartler et al. [17]	Configuration space Implementation variant Implementation space
	Nadi and Holt [10, 11]	Kconfig space	Make space	Code space
	Hengelein [6], Tartler [15]	Feature Modeling Configuration	Build system	Generator Preprocessor
	Passos et al. [12]	Variability Model	Mapping	Implementation
	El-Sharkawy et al. [3]	Problem space	Solution space
	Abal et al. [1]	Problem space Model	/	Solution space Code
	Nadi and Holt [9]	Configuration space	Compilation space	Implementation space
	Nadi [8]	Configuration space	Build space	Code space
	Sincero et al. [14]	Problem space Model	/	Solution space Implementation
	Tartler et al. [16]	Configuration space	/	Implementation space
	Chosen terminology

Table 2 .

 2 Notation mapping for constraints in the three spaces

  is an #elsif or #else block, 𝑏 𝑖 represents the corresponding #if block and the potential #elsif blocks before 𝑏 ;• 𝜙 𝑑𝑒𝑝𝐼𝑛𝑡 = 𝑝 with 𝑝 the parent block of 𝑏 if 𝑏 is a nested block.

Table 3 .

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

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

  ¬𝑠𝑎𝑡 (𝐵𝑙𝑜𝑐𝑘 𝑁 ∧ 𝐶 ∧ 𝑀 ∧ 𝐾) 𝑈 𝑛𝑑𝑒𝑎𝑑 𝐵 𝑁 = ¬𝑠𝑎𝑡 (¬𝐵𝑙𝑜𝑐𝑘 𝑁 ∧ 𝑝𝑎𝑟𝑒𝑛𝑡 (𝐵𝑙𝑜𝑐𝑘 𝑁 ) ∧ 𝐶 ∧ 𝑀 ∧ 𝐾)Instantiation 22 (Expressing code-Make-Kconfig anomalies {22}).¬𝑠𝑎𝑡 (𝐵𝑁 ∧ 𝐶 ∧ 𝑀 ∧ 𝐾) ⇔ ¬𝑠𝑎𝑡 (PC 𝐼𝑛𝑡 (𝐵 𝑁 ) ∧ C) ⇔ ¬𝑠𝑎𝑡 (PC 𝐸𝑥𝑡 (𝐵 𝑁 )) (𝑑𝑒 𝑓 . 3) ¬𝑠𝑎𝑡 (¬𝐵 𝑁 ∧ 𝑝𝑎𝑟𝑒𝑛𝑡 (𝐵 𝑁 ) ∧ 𝐶 ∧ 𝑀 ∧ 𝐾) ⇔ ¬𝑠𝑎𝑡 (C ∧ ¬PC 𝐼𝑛𝑡 (𝐵 𝑁 ) ∧ 𝑒𝑥𝑝𝑎𝑛𝑑 (𝜙 𝑑𝑒𝑝𝐼𝑛𝑡 𝐵 𝑁))⇔ ¬𝑠𝑎𝑡 ¬PC 𝐸𝑥𝑡 (𝐵 𝑁 ) ∧ 𝑒𝑥𝑝𝑎𝑛𝑑 (𝜙 𝑑𝑒𝑝𝐼𝑛𝑡 𝐵 𝑁 )

Table 5 .

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

	Paper		Sincero et al. [14]	Tartler et al. [16]	Nadi and Holt [9]	Nadi and Holt [10]	Hengelein [6]
	Internal	Dead	anom. {2}	anom. {14}	anom. {12}	anom. {18}
	consistency	Core	anom. {2}	anom. {14}		anom. {18}
	External	Dead	anom. {1,3}	anom. {13,15}		anom. {19,21,22,24}
	Derivator
	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
					anom. {10}		anom. {7,8,9}
	(e.g., unreachable symbol, file not used)

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

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

https://www.kernel.org/doc/html/latest/kbuild/makefiles.html#descending-down-in-directories

Code space Kbuild derivator on source files [START_REF] Hengelein | Analyzing the Internal Consistency of the Linux KConfig Model[END_REF]: anom. {4,5,6,7,8,9} [START_REF] Tartler | Feature consistency in compile-time-configurable system software: Facing the Linux 10,000 feature problem[END_REF]: anom. {16} [START_REF] Nadi | Make it or break it: Mining anomalies from Linux Kbuild[END_REF]: anom. {10,11,12} [START_REF] Sincero | Efficient extraction and analysis of preprocessor-based variability[END_REF]: anom. {2}, [START_REF] Nadi | Mining Kbuild to detect variability anomalies in Linux[END_REF]: anom. {18}, [START_REF] Tartler | Feature consistency in compile-time-configurable system software: Facing the Linux 10,000 feature problem[END_REF]: anom. {14} [START_REF] Nadi | Mining Kbuild to detect variability anomalies in Linux[END_REF]: anom. {24,25} [START_REF] Nadi | Mining Kbuild to detect variability anomalies in Linux[END_REF]: anom. {21} We can then express anom. {24} in our model:

anom. {24} thus expresses dead (def. 6) and core defects (def. 7).

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.

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

RESULTING TABLES

We summarize our study of the existing work on anomalies in the Linux build system by providing a synthetic map illustrates the coverage of the different papers and the anomalies they express over the different spaces of the Linux build system fig. 2. Table 4 describes for every anomaly the expressed property in our formalism.