Back to home page

OSCL-LXR

 
 

    


0001 ================
0002 Kconfig Language
0003 ================
0004 
0005 Introduction
0006 ------------
0007 
0008 The configuration database is a collection of configuration options
0009 organized in a tree structure::
0010 
0011         +- Code maturity level options
0012         |  +- Prompt for development and/or incomplete code/drivers
0013         +- General setup
0014         |  +- Networking support
0015         |  +- System V IPC
0016         |  +- BSD Process Accounting
0017         |  +- Sysctl support
0018         +- Loadable module support
0019         |  +- Enable loadable module support
0020         |     +- Set version information on all module symbols
0021         |     +- Kernel module loader
0022         +- ...
0023 
0024 Every entry has its own dependencies. These dependencies are used
0025 to determine the visibility of an entry. Any child entry is only
0026 visible if its parent entry is also visible.
0027 
0028 Menu entries
0029 ------------
0030 
0031 Most entries define a config option; all other entries help to organize
0032 them. A single configuration option is defined like this::
0033 
0034   config MODVERSIONS
0035         bool "Set version information on all module symbols"
0036         depends on MODULES
0037         help
0038           Usually, modules have to be recompiled whenever you switch to a new
0039           kernel.  ...
0040 
0041 Every line starts with a key word and can be followed by multiple
0042 arguments.  "config" starts a new config entry. The following lines
0043 define attributes for this config option. Attributes can be the type of
0044 the config option, input prompt, dependencies, help text and default
0045 values. A config option can be defined multiple times with the same
0046 name, but every definition can have only a single input prompt and the
0047 type must not conflict.
0048 
0049 Menu attributes
0050 ---------------
0051 
0052 A menu entry can have a number of attributes. Not all of them are
0053 applicable everywhere (see syntax).
0054 
0055 - type definition: "bool"/"tristate"/"string"/"hex"/"int"
0056 
0057   Every config option must have a type. There are only two basic types:
0058   tristate and string; the other types are based on these two. The type
0059   definition optionally accepts an input prompt, so these two examples
0060   are equivalent::
0061 
0062         bool "Networking support"
0063 
0064   and::
0065 
0066         bool
0067         prompt "Networking support"
0068 
0069 - input prompt: "prompt" <prompt> ["if" <expr>]
0070 
0071   Every menu entry can have at most one prompt, which is used to display
0072   to the user. Optionally dependencies only for this prompt can be added
0073   with "if".
0074 
0075 - default value: "default" <expr> ["if" <expr>]
0076 
0077   A config option can have any number of default values. If multiple
0078   default values are visible, only the first defined one is active.
0079   Default values are not limited to the menu entry where they are
0080   defined. This means the default can be defined somewhere else or be
0081   overridden by an earlier definition.
0082   The default value is only assigned to the config symbol if no other
0083   value was set by the user (via the input prompt above). If an input
0084   prompt is visible the default value is presented to the user and can
0085   be overridden by him.
0086   Optionally, dependencies only for this default value can be added with
0087   "if".
0088 
0089  The default value deliberately defaults to 'n' in order to avoid bloating the
0090  build. With few exceptions, new config options should not change this. The
0091  intent is for "make oldconfig" to add as little as possible to the config from
0092  release to release.
0093 
0094  Note:
0095         Things that merit "default y/m" include:
0096 
0097         a) A new Kconfig option for something that used to always be built
0098            should be "default y".
0099 
0100         b) A new gatekeeping Kconfig option that hides/shows other Kconfig
0101            options (but does not generate any code of its own), should be
0102            "default y" so people will see those other options.
0103 
0104         c) Sub-driver behavior or similar options for a driver that is
0105            "default n". This allows you to provide sane defaults.
0106 
0107         d) Hardware or infrastructure that everybody expects, such as CONFIG_NET
0108            or CONFIG_BLOCK. These are rare exceptions.
0109 
0110 - type definition + default value::
0111 
0112         "def_bool"/"def_tristate" <expr> ["if" <expr>]
0113 
0114   This is a shorthand notation for a type definition plus a value.
0115   Optionally dependencies for this default value can be added with "if".
0116 
0117 - dependencies: "depends on" <expr>
0118 
0119   This defines a dependency for this menu entry. If multiple
0120   dependencies are defined, they are connected with '&&'. Dependencies
0121   are applied to all other options within this menu entry (which also
0122   accept an "if" expression), so these two examples are equivalent::
0123 
0124         bool "foo" if BAR
0125         default y if BAR
0126 
0127   and::
0128 
0129         depends on BAR
0130         bool "foo"
0131         default y
0132 
0133 - reverse dependencies: "select" <symbol> ["if" <expr>]
0134 
0135   While normal dependencies reduce the upper limit of a symbol (see
0136   below), reverse dependencies can be used to force a lower limit of
0137   another symbol. The value of the current menu symbol is used as the
0138   minimal value <symbol> can be set to. If <symbol> is selected multiple
0139   times, the limit is set to the largest selection.
0140   Reverse dependencies can only be used with boolean or tristate
0141   symbols.
0142 
0143   Note:
0144         select should be used with care. select will force
0145         a symbol to a value without visiting the dependencies.
0146         By abusing select you are able to select a symbol FOO even
0147         if FOO depends on BAR that is not set.
0148         In general use select only for non-visible symbols
0149         (no prompts anywhere) and for symbols with no dependencies.
0150         That will limit the usefulness but on the other hand avoid
0151         the illegal configurations all over.
0152 
0153 - weak reverse dependencies: "imply" <symbol> ["if" <expr>]
0154 
0155   This is similar to "select" as it enforces a lower limit on another
0156   symbol except that the "implied" symbol's value may still be set to n
0157   from a direct dependency or with a visible prompt.
0158 
0159   Given the following example::
0160 
0161     config FOO
0162         tristate "foo"
0163         imply BAZ
0164 
0165     config BAZ
0166         tristate "baz"
0167         depends on BAR
0168 
0169   The following values are possible:
0170 
0171         ===             ===             =============   ==============
0172         FOO             BAR             BAZ's default   choice for BAZ
0173         ===             ===             =============   ==============
0174         n               y               n               N/m/y
0175         m               y               m               M/y/n
0176         y               y               y               Y/m/n
0177         n               m               n               N/m
0178         m               m               m               M/n
0179         y               m               m               M/n
0180         y               n               *               N
0181         ===             ===             =============   ==============
0182 
0183   This is useful e.g. with multiple drivers that want to indicate their
0184   ability to hook into a secondary subsystem while allowing the user to
0185   configure that subsystem out without also having to unset these drivers.
0186 
0187   Note: If the combination of FOO=y and BAR=m causes a link error,
0188   you can guard the function call with IS_REACHABLE()::
0189 
0190         foo_init()
0191         {
0192                 if (IS_REACHABLE(CONFIG_BAZ))
0193                         baz_register(&foo);
0194                 ...
0195         }
0196 
0197   Note: If the feature provided by BAZ is highly desirable for FOO,
0198   FOO should imply not only BAZ, but also its dependency BAR::
0199 
0200     config FOO
0201         tristate "foo"
0202         imply BAR
0203         imply BAZ
0204 
0205 - limiting menu display: "visible if" <expr>
0206 
0207   This attribute is only applicable to menu blocks, if the condition is
0208   false, the menu block is not displayed to the user (the symbols
0209   contained there can still be selected by other symbols, though). It is
0210   similar to a conditional "prompt" attribute for individual menu
0211   entries. Default value of "visible" is true.
0212 
0213 - numerical ranges: "range" <symbol> <symbol> ["if" <expr>]
0214 
0215   This allows to limit the range of possible input values for int
0216   and hex symbols. The user can only input a value which is larger than
0217   or equal to the first symbol and smaller than or equal to the second
0218   symbol.
0219 
0220 - help text: "help"
0221 
0222   This defines a help text. The end of the help text is determined by
0223   the indentation level, this means it ends at the first line which has
0224   a smaller indentation than the first line of the help text.
0225 
0226 - module attribute: "modules"
0227   This declares the symbol to be used as the MODULES symbol, which
0228   enables the third modular state for all config symbols.
0229   At most one symbol may have the "modules" option set.
0230 
0231 Menu dependencies
0232 -----------------
0233 
0234 Dependencies define the visibility of a menu entry and can also reduce
0235 the input range of tristate symbols. The tristate logic used in the
0236 expressions uses one more state than normal boolean logic to express the
0237 module state. Dependency expressions have the following syntax::
0238 
0239   <expr> ::= <symbol>                           (1)
0240            <symbol> '=' <symbol>                (2)
0241            <symbol> '!=' <symbol>               (3)
0242            <symbol1> '<' <symbol2>              (4)
0243            <symbol1> '>' <symbol2>              (4)
0244            <symbol1> '<=' <symbol2>             (4)
0245            <symbol1> '>=' <symbol2>             (4)
0246            '(' <expr> ')'                       (5)
0247            '!' <expr>                           (6)
0248            <expr> '&&' <expr>                   (7)
0249            <expr> '||' <expr>                   (8)
0250 
0251 Expressions are listed in decreasing order of precedence.
0252 
0253 (1) Convert the symbol into an expression. Boolean and tristate symbols
0254     are simply converted into the respective expression values. All
0255     other symbol types result in 'n'.
0256 (2) If the values of both symbols are equal, it returns 'y',
0257     otherwise 'n'.
0258 (3) If the values of both symbols are equal, it returns 'n',
0259     otherwise 'y'.
0260 (4) If value of <symbol1> is respectively lower, greater, lower-or-equal,
0261     or greater-or-equal than value of <symbol2>, it returns 'y',
0262     otherwise 'n'.
0263 (5) Returns the value of the expression. Used to override precedence.
0264 (6) Returns the result of (2-/expr/).
0265 (7) Returns the result of min(/expr/, /expr/).
0266 (8) Returns the result of max(/expr/, /expr/).
0267 
0268 An expression can have a value of 'n', 'm' or 'y' (or 0, 1, 2
0269 respectively for calculations). A menu entry becomes visible when its
0270 expression evaluates to 'm' or 'y'.
0271 
0272 There are two types of symbols: constant and non-constant symbols.
0273 Non-constant symbols are the most common ones and are defined with the
0274 'config' statement. Non-constant symbols consist entirely of alphanumeric
0275 characters or underscores.
0276 Constant symbols are only part of expressions. Constant symbols are
0277 always surrounded by single or double quotes. Within the quote, any
0278 other character is allowed and the quotes can be escaped using '\'.
0279 
0280 Menu structure
0281 --------------
0282 
0283 The position of a menu entry in the tree is determined in two ways. First
0284 it can be specified explicitly::
0285 
0286   menu "Network device support"
0287         depends on NET
0288 
0289   config NETDEVICES
0290         ...
0291 
0292   endmenu
0293 
0294 All entries within the "menu" ... "endmenu" block become a submenu of
0295 "Network device support". All subentries inherit the dependencies from
0296 the menu entry, e.g. this means the dependency "NET" is added to the
0297 dependency list of the config option NETDEVICES.
0298 
0299 The other way to generate the menu structure is done by analyzing the
0300 dependencies. If a menu entry somehow depends on the previous entry, it
0301 can be made a submenu of it. First, the previous (parent) symbol must
0302 be part of the dependency list and then one of these two conditions
0303 must be true:
0304 
0305 - the child entry must become invisible, if the parent is set to 'n'
0306 - the child entry must only be visible, if the parent is visible::
0307 
0308     config MODULES
0309         bool "Enable loadable module support"
0310 
0311     config MODVERSIONS
0312         bool "Set version information on all module symbols"
0313         depends on MODULES
0314 
0315     comment "module support disabled"
0316         depends on !MODULES
0317 
0318 MODVERSIONS directly depends on MODULES, this means it's only visible if
0319 MODULES is different from 'n'. The comment on the other hand is only
0320 visible when MODULES is set to 'n'.
0321 
0322 
0323 Kconfig syntax
0324 --------------
0325 
0326 The configuration file describes a series of menu entries, where every
0327 line starts with a keyword (except help texts). The following keywords
0328 end a menu entry:
0329 
0330 - config
0331 - menuconfig
0332 - choice/endchoice
0333 - comment
0334 - menu/endmenu
0335 - if/endif
0336 - source
0337 
0338 The first five also start the definition of a menu entry.
0339 
0340 config::
0341 
0342         "config" <symbol>
0343         <config options>
0344 
0345 This defines a config symbol <symbol> and accepts any of above
0346 attributes as options.
0347 
0348 menuconfig::
0349 
0350         "menuconfig" <symbol>
0351         <config options>
0352 
0353 This is similar to the simple config entry above, but it also gives a
0354 hint to front ends, that all suboptions should be displayed as a
0355 separate list of options. To make sure all the suboptions will really
0356 show up under the menuconfig entry and not outside of it, every item
0357 from the <config options> list must depend on the menuconfig symbol.
0358 In practice, this is achieved by using one of the next two constructs::
0359 
0360   (1):
0361   menuconfig M
0362   if M
0363       config C1
0364       config C2
0365   endif
0366 
0367   (2):
0368   menuconfig M
0369   config C1
0370       depends on M
0371   config C2
0372       depends on M
0373 
0374 In the following examples (3) and (4), C1 and C2 still have the M
0375 dependency, but will not appear under menuconfig M anymore, because
0376 of C0, which doesn't depend on M::
0377 
0378   (3):
0379   menuconfig M
0380       config C0
0381   if M
0382       config C1
0383       config C2
0384   endif
0385 
0386   (4):
0387   menuconfig M
0388   config C0
0389   config C1
0390       depends on M
0391   config C2
0392       depends on M
0393 
0394 choices::
0395 
0396         "choice" [symbol]
0397         <choice options>
0398         <choice block>
0399         "endchoice"
0400 
0401 This defines a choice group and accepts any of the above attributes as
0402 options. A choice can only be of type bool or tristate.  If no type is
0403 specified for a choice, its type will be determined by the type of
0404 the first choice element in the group or remain unknown if none of the
0405 choice elements have a type specified, as well.
0406 
0407 While a boolean choice only allows a single config entry to be
0408 selected, a tristate choice also allows any number of config entries
0409 to be set to 'm'. This can be used if multiple drivers for a single
0410 hardware exists and only a single driver can be compiled/loaded into
0411 the kernel, but all drivers can be compiled as modules.
0412 
0413 A choice accepts another option "optional", which allows to set the
0414 choice to 'n' and no entry needs to be selected.
0415 If no [symbol] is associated with a choice, then you can not have multiple
0416 definitions of that choice. If a [symbol] is associated to the choice,
0417 then you may define the same choice (i.e. with the same entries) in another
0418 place.
0419 
0420 comment::
0421 
0422         "comment" <prompt>
0423         <comment options>
0424 
0425 This defines a comment which is displayed to the user during the
0426 configuration process and is also echoed to the output files. The only
0427 possible options are dependencies.
0428 
0429 menu::
0430 
0431         "menu" <prompt>
0432         <menu options>
0433         <menu block>
0434         "endmenu"
0435 
0436 This defines a menu block, see "Menu structure" above for more
0437 information. The only possible options are dependencies and "visible"
0438 attributes.
0439 
0440 if::
0441 
0442         "if" <expr>
0443         <if block>
0444         "endif"
0445 
0446 This defines an if block. The dependency expression <expr> is appended
0447 to all enclosed menu entries.
0448 
0449 source::
0450 
0451         "source" <prompt>
0452 
0453 This reads the specified configuration file. This file is always parsed.
0454 
0455 mainmenu::
0456 
0457         "mainmenu" <prompt>
0458 
0459 This sets the config program's title bar if the config program chooses
0460 to use it. It should be placed at the top of the configuration, before any
0461 other statement.
0462 
0463 '#' Kconfig source file comment:
0464 
0465 An unquoted '#' character anywhere in a source file line indicates
0466 the beginning of a source file comment.  The remainder of that line
0467 is a comment.
0468 
0469 
0470 Kconfig hints
0471 -------------
0472 This is a collection of Kconfig tips, most of which aren't obvious at
0473 first glance and most of which have become idioms in several Kconfig
0474 files.
0475 
0476 Adding common features and make the usage configurable
0477 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
0478 It is a common idiom to implement a feature/functionality that are
0479 relevant for some architectures but not all.
0480 The recommended way to do so is to use a config variable named HAVE_*
0481 that is defined in a common Kconfig file and selected by the relevant
0482 architectures.
0483 An example is the generic IOMAP functionality.
0484 
0485 We would in lib/Kconfig see::
0486 
0487   # Generic IOMAP is used to ...
0488   config HAVE_GENERIC_IOMAP
0489 
0490   config GENERIC_IOMAP
0491         depends on HAVE_GENERIC_IOMAP && FOO
0492 
0493 And in lib/Makefile we would see::
0494 
0495         obj-$(CONFIG_GENERIC_IOMAP) += iomap.o
0496 
0497 For each architecture using the generic IOMAP functionality we would see::
0498 
0499   config X86
0500         select ...
0501         select HAVE_GENERIC_IOMAP
0502         select ...
0503 
0504 Note: we use the existing config option and avoid creating a new
0505 config variable to select HAVE_GENERIC_IOMAP.
0506 
0507 Note: the use of the internal config variable HAVE_GENERIC_IOMAP, it is
0508 introduced to overcome the limitation of select which will force a
0509 config option to 'y' no matter the dependencies.
0510 The dependencies are moved to the symbol GENERIC_IOMAP and we avoid the
0511 situation where select forces a symbol equals to 'y'.
0512 
0513 Adding features that need compiler support
0514 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
0515 
0516 There are several features that need compiler support. The recommended way
0517 to describe the dependency on the compiler feature is to use "depends on"
0518 followed by a test macro::
0519 
0520   config STACKPROTECTOR
0521         bool "Stack Protector buffer overflow detection"
0522         depends on $(cc-option,-fstack-protector)
0523         ...
0524 
0525 If you need to expose a compiler capability to makefiles and/or C source files,
0526 `CC_HAS_` is the recommended prefix for the config option::
0527 
0528   config CC_HAS_FOO
0529         def_bool $(success,$(srctree)/scripts/cc-check-foo.sh $(CC))
0530 
0531 Build as module only
0532 ~~~~~~~~~~~~~~~~~~~~
0533 To restrict a component build to module-only, qualify its config symbol
0534 with "depends on m".  E.g.::
0535 
0536   config FOO
0537         depends on BAR && m
0538 
0539 limits FOO to module (=m) or disabled (=n).
0540 
0541 Compile-testing
0542 ~~~~~~~~~~~~~~~
0543 If a config symbol has a dependency, but the code controlled by the config
0544 symbol can still be compiled if the dependency is not met, it is encouraged to
0545 increase build coverage by adding an "|| COMPILE_TEST" clause to the
0546 dependency. This is especially useful for drivers for more exotic hardware, as
0547 it allows continuous-integration systems to compile-test the code on a more
0548 common system, and detect bugs that way.
0549 Note that compile-tested code should avoid crashing when run on a system where
0550 the dependency is not met.
0551 
0552 Architecture and platform dependencies
0553 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
0554 Due to the presence of stubs, most drivers can now be compiled on most
0555 architectures. However, this does not mean it makes sense to have all drivers
0556 available everywhere, as the actual hardware may only exist on specific
0557 architectures and platforms. This is especially true for on-SoC IP cores,
0558 which may be limited to a specific vendor or SoC family.
0559 
0560 To prevent asking the user about drivers that cannot be used on the system(s)
0561 the user is compiling a kernel for, and if it makes sense, config symbols
0562 controlling the compilation of a driver should contain proper dependencies,
0563 limiting the visibility of the symbol to (a superset of) the platform(s) the
0564 driver can be used on. The dependency can be an architecture (e.g. ARM) or
0565 platform (e.g. ARCH_OMAP4) dependency. This makes life simpler not only for
0566 distro config owners, but also for every single developer or user who
0567 configures a kernel.
0568 
0569 Such a dependency can be relaxed by combining it with the compile-testing rule
0570 above, leading to:
0571 
0572   config FOO
0573         bool "Support for foo hardware"
0574         depends on ARCH_FOO_VENDOR || COMPILE_TEST
0575 
0576 Kconfig recursive dependency limitations
0577 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
0578 
0579 If you've hit the Kconfig error: "recursive dependency detected" you've run
0580 into a recursive dependency issue with Kconfig, a recursive dependency can be
0581 summarized as a circular dependency. The kconfig tools need to ensure that
0582 Kconfig files comply with specified configuration requirements. In order to do
0583 that kconfig must determine the values that are possible for all Kconfig
0584 symbols, this is currently not possible if there is a circular relation
0585 between two or more Kconfig symbols. For more details refer to the "Simple
0586 Kconfig recursive issue" subsection below. Kconfig does not do recursive
0587 dependency resolution; this has a few implications for Kconfig file writers.
0588 We'll first explain why this issues exists and then provide an example
0589 technical limitation which this brings upon Kconfig developers. Eager
0590 developers wishing to try to address this limitation should read the next
0591 subsections.
0592 
0593 Simple Kconfig recursive issue
0594 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
0595 
0596 Read: Documentation/kbuild/Kconfig.recursion-issue-01
0597 
0598 Test with::
0599 
0600   make KBUILD_KCONFIG=Documentation/kbuild/Kconfig.recursion-issue-01 allnoconfig
0601 
0602 Cumulative Kconfig recursive issue
0603 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
0604 
0605 Read: Documentation/kbuild/Kconfig.recursion-issue-02
0606 
0607 Test with::
0608 
0609   make KBUILD_KCONFIG=Documentation/kbuild/Kconfig.recursion-issue-02 allnoconfig
0610 
0611 Practical solutions to kconfig recursive issue
0612 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
0613 
0614 Developers who run into the recursive Kconfig issue have two options
0615 at their disposal. We document them below and also provide a list of
0616 historical issues resolved through these different solutions.
0617 
0618   a) Remove any superfluous "select FOO" or "depends on FOO"
0619   b) Match dependency semantics:
0620 
0621         b1) Swap all "select FOO" to "depends on FOO" or,
0622 
0623         b2) Swap all "depends on FOO" to "select FOO"
0624 
0625 The resolution to a) can be tested with the sample Kconfig file
0626 Documentation/kbuild/Kconfig.recursion-issue-01 through the removal
0627 of the "select CORE" from CORE_BELL_A_ADVANCED as that is implicit already
0628 since CORE_BELL_A depends on CORE. At times it may not be possible to remove
0629 some dependency criteria, for such cases you can work with solution b).
0630 
0631 The two different resolutions for b) can be tested in the sample Kconfig file
0632 Documentation/kbuild/Kconfig.recursion-issue-02.
0633 
0634 Below is a list of examples of prior fixes for these types of recursive issues;
0635 all errors appear to involve one or more "select" statements and one or more
0636 "depends on".
0637 
0638 ============    ===================================
0639 commit          fix
0640 ============    ===================================
0641 06b718c01208    select A -> depends on A
0642 c22eacfe82f9    depends on A -> depends on B
0643 6a91e854442c    select A -> depends on A
0644 118c565a8f2e    select A -> select B
0645 f004e5594705    select A -> depends on A
0646 c7861f37b4c6    depends on A -> (null)
0647 80c69915e5fb    select A -> (null)              (1)
0648 c2218e26c0d0    select A -> depends on A        (1)
0649 d6ae99d04e1c    select A -> depends on A
0650 95ca19cf8cbf    select A -> depends on A
0651 8f057d7bca54    depends on A -> (null)
0652 8f057d7bca54    depends on A -> select A
0653 a0701f04846e    select A -> depends on A
0654 0c8b92f7f259    depends on A -> (null)
0655 e4e9e0540928    select A -> depends on A        (2)
0656 7453ea886e87    depends on A > (null)           (1)
0657 7b1fff7e4fdf    select A -> depends on A
0658 86c747d2a4f0    select A -> depends on A
0659 d9f9ab51e55e    select A -> depends on A
0660 0c51a4d8abd6    depends on A -> select A        (3)
0661 e98062ed6dc4    select A -> depends on A        (3)
0662 91e5d284a7f1    select A -> (null)
0663 ============    ===================================
0664 
0665 (1) Partial (or no) quote of error.
0666 (2) That seems to be the gist of that fix.
0667 (3) Same error.
0668 
0669 Future kconfig work
0670 ~~~~~~~~~~~~~~~~~~~
0671 
0672 Work on kconfig is welcomed on both areas of clarifying semantics and on
0673 evaluating the use of a full SAT solver for it. A full SAT solver can be
0674 desirable to enable more complex dependency mappings and / or queries,
0675 for instance one possible use case for a SAT solver could be that of handling
0676 the current known recursive dependency issues. It is not known if this would
0677 address such issues but such evaluation is desirable. If support for a full SAT
0678 solver proves too complex or that it cannot address recursive dependency issues
0679 Kconfig should have at least clear and well defined semantics which also
0680 addresses and documents limitations or requirements such as the ones dealing
0681 with recursive dependencies.
0682 
0683 Further work on both of these areas is welcomed on Kconfig. We elaborate
0684 on both of these in the next two subsections.
0685 
0686 Semantics of Kconfig
0687 ~~~~~~~~~~~~~~~~~~~~
0688 
0689 The use of Kconfig is broad, Linux is now only one of Kconfig's users:
0690 one study has completed a broad analysis of Kconfig use in 12 projects [0]_.
0691 Despite its widespread use, and although this document does a reasonable job
0692 in documenting basic Kconfig syntax a more precise definition of Kconfig
0693 semantics is welcomed. One project deduced Kconfig semantics through
0694 the use of the xconfig configurator [1]_. Work should be done to confirm if
0695 the deduced semantics matches our intended Kconfig design goals.
0696 Another project formalized a denotational semantics of a core subset of
0697 the Kconfig language [10]_.
0698 
0699 Having well defined semantics can be useful for tools for practical
0700 evaluation of dependencies, for instance one such case was work to
0701 express in boolean abstraction of the inferred semantics of Kconfig to
0702 translate Kconfig logic into boolean formulas and run a SAT solver on this to
0703 find dead code / features (always inactive), 114 dead features were found in
0704 Linux using this methodology [1]_ (Section 8: Threats to validity).
0705 The kismet tool, based on the semantics in [10]_, finds abuses of reverse
0706 dependencies and has led to dozens of committed fixes to Linux Kconfig files [11]_.
0707 
0708 Confirming this could prove useful as Kconfig stands as one of the leading
0709 industrial variability modeling languages [1]_ [2]_. Its study would help
0710 evaluate practical uses of such languages, their use was only theoretical
0711 and real world requirements were not well understood. As it stands though
0712 only reverse engineering techniques have been used to deduce semantics from
0713 variability modeling languages such as Kconfig [3]_.
0714 
0715 .. [0] https://www.eng.uwaterloo.ca/~shshe/kconfig_semantics.pdf
0716 .. [1] https://gsd.uwaterloo.ca/sites/default/files/vm-2013-berger.pdf
0717 .. [2] https://gsd.uwaterloo.ca/sites/default/files/ase241-berger_0.pdf
0718 .. [3] https://gsd.uwaterloo.ca/sites/default/files/icse2011.pdf
0719 
0720 Full SAT solver for Kconfig
0721 ~~~~~~~~~~~~~~~~~~~~~~~~~~~
0722 
0723 Although SAT solvers [4]_ haven't yet been used by Kconfig directly, as noted
0724 in the previous subsection, work has been done however to express in boolean
0725 abstraction the inferred semantics of Kconfig to translate Kconfig logic into
0726 boolean formulas and run a SAT solver on it [5]_. Another known related project
0727 is CADOS [6]_ (former VAMOS [7]_) and the tools, mainly undertaker [8]_, which
0728 has been introduced first with [9]_.  The basic concept of undertaker is to
0729 extract variability models from Kconfig and put them together with a
0730 propositional formula extracted from CPP #ifdefs and build-rules into a SAT
0731 solver in order to find dead code, dead files, and dead symbols. If using a SAT
0732 solver is desirable on Kconfig one approach would be to evaluate repurposing
0733 such efforts somehow on Kconfig. There is enough interest from mentors of
0734 existing projects to not only help advise how to integrate this work upstream
0735 but also help maintain it long term. Interested developers should visit:
0736 
0737 https://kernelnewbies.org/KernelProjects/kconfig-sat
0738 
0739 .. [4] https://www.cs.cornell.edu/~sabhar/chapters/SATSolvers-KR-Handbook.pdf
0740 .. [5] https://gsd.uwaterloo.ca/sites/default/files/vm-2013-berger.pdf
0741 .. [6] https://cados.cs.fau.de
0742 .. [7] https://vamos.cs.fau.de
0743 .. [8] https://undertaker.cs.fau.de
0744 .. [9] https://www4.cs.fau.de/Publications/2011/tartler_11_eurosys.pdf
0745 .. [10] https://paulgazzillo.com/papers/esecfse21.pdf
0746 .. [11] https://github.com/paulgazz/kmax