Commit | Line | Data |
---|---|---|
1da177e4 LT |
1 | Introduction |
2 | ------------ | |
3 | ||
e95be9a5 | 4 | The configuration database is a collection of configuration options |
1da177e4 LT |
5 | organized in a tree structure: |
6 | ||
7 | +- Code maturity level options | |
8 | | +- Prompt for development and/or incomplete code/drivers | |
9 | +- General setup | |
10 | | +- Networking support | |
11 | | +- System V IPC | |
12 | | +- BSD Process Accounting | |
13 | | +- Sysctl support | |
14 | +- Loadable module support | |
15 | | +- Enable loadable module support | |
16 | | +- Set version information on all module symbols | |
17 | | +- Kernel module loader | |
18 | +- ... | |
19 | ||
20 | Every entry has its own dependencies. These dependencies are used | |
21 | to determine the visibility of an entry. Any child entry is only | |
22 | visible if its parent entry is also visible. | |
23 | ||
24 | Menu entries | |
25 | ------------ | |
26 | ||
0486bc90 | 27 | Most entries define a config option; all other entries help to organize |
1da177e4 LT |
28 | them. A single configuration option is defined like this: |
29 | ||
30 | config MODVERSIONS | |
31 | bool "Set version information on all module symbols" | |
bef1f402 | 32 | depends on MODULES |
1da177e4 LT |
33 | help |
34 | Usually, modules have to be recompiled whenever you switch to a new | |
35 | kernel. ... | |
36 | ||
37 | Every line starts with a key word and can be followed by multiple | |
38 | arguments. "config" starts a new config entry. The following lines | |
39 | define attributes for this config option. Attributes can be the type of | |
40 | the config option, input prompt, dependencies, help text and default | |
41 | values. A config option can be defined multiple times with the same | |
42 | name, but every definition can have only a single input prompt and the | |
43 | type must not conflict. | |
44 | ||
45 | Menu attributes | |
46 | --------------- | |
47 | ||
48 | A menu entry can have a number of attributes. Not all of them are | |
49 | applicable everywhere (see syntax). | |
50 | ||
51 | - type definition: "bool"/"tristate"/"string"/"hex"/"int" | |
52 | Every config option must have a type. There are only two basic types: | |
0486bc90 | 53 | tristate and string; the other types are based on these two. The type |
1da177e4 LT |
54 | definition optionally accepts an input prompt, so these two examples |
55 | are equivalent: | |
56 | ||
57 | bool "Networking support" | |
58 | and | |
59 | bool | |
60 | prompt "Networking support" | |
61 | ||
62 | - input prompt: "prompt" <prompt> ["if" <expr>] | |
63 | Every menu entry can have at most one prompt, which is used to display | |
64 | to the user. Optionally dependencies only for this prompt can be added | |
65 | with "if". | |
66 | ||
67 | - default value: "default" <expr> ["if" <expr>] | |
68 | A config option can have any number of default values. If multiple | |
69 | default values are visible, only the first defined one is active. | |
83dcde4e JE |
70 | Default values are not limited to the menu entry where they are |
71 | defined. This means the default can be defined somewhere else or be | |
1da177e4 LT |
72 | overridden by an earlier definition. |
73 | The default value is only assigned to the config symbol if no other | |
74 | value was set by the user (via the input prompt above). If an input | |
75 | prompt is visible the default value is presented to the user and can | |
76 | be overridden by him. | |
83dcde4e | 77 | Optionally, dependencies only for this default value can be added with |
1da177e4 LT |
78 | "if". |
79 | ||
6e66b900 RD |
80 | - type definition + default value: |
81 | "def_bool"/"def_tristate" <expr> ["if" <expr>] | |
82 | This is a shorthand notation for a type definition plus a value. | |
83 | Optionally dependencies for this default value can be added with "if". | |
84 | ||
85 | - dependencies: "depends on" <expr> | |
1da177e4 | 86 | This defines a dependency for this menu entry. If multiple |
83dcde4e | 87 | dependencies are defined, they are connected with '&&'. Dependencies |
1da177e4 LT |
88 | are applied to all other options within this menu entry (which also |
89 | accept an "if" expression), so these two examples are equivalent: | |
90 | ||
91 | bool "foo" if BAR | |
92 | default y if BAR | |
93 | and | |
94 | depends on BAR | |
95 | bool "foo" | |
96 | default y | |
97 | ||
98 | - reverse dependencies: "select" <symbol> ["if" <expr>] | |
99 | While normal dependencies reduce the upper limit of a symbol (see | |
100 | below), reverse dependencies can be used to force a lower limit of | |
101 | another symbol. The value of the current menu symbol is used as the | |
102 | minimal value <symbol> can be set to. If <symbol> is selected multiple | |
103 | times, the limit is set to the largest selection. | |
104 | Reverse dependencies can only be used with boolean or tristate | |
105 | symbols. | |
f8a74594 | 106 | Note: |
dfecbec8 MW |
107 | select should be used with care. select will force |
108 | a symbol to a value without visiting the dependencies. | |
109 | By abusing select you are able to select a symbol FOO even | |
110 | if FOO depends on BAR that is not set. | |
111 | In general use select only for non-visible symbols | |
112 | (no prompts anywhere) and for symbols with no dependencies. | |
113 | That will limit the usefulness but on the other hand avoid | |
114 | the illegal configurations all over. | |
1da177e4 | 115 | |
df835c2e MM |
116 | - limiting menu display: "visible if" <expr> |
117 | This attribute is only applicable to menu blocks, if the condition is | |
118 | false, the menu block is not displayed to the user (the symbols | |
119 | contained there can still be selected by other symbols, though). It is | |
40e47125 | 120 | similar to a conditional "prompt" attribute for individual menu |
df835c2e MM |
121 | entries. Default value of "visible" is true. |
122 | ||
1da177e4 LT |
123 | - numerical ranges: "range" <symbol> <symbol> ["if" <expr>] |
124 | This allows to limit the range of possible input values for int | |
125 | and hex symbols. The user can only input a value which is larger than | |
126 | or equal to the first symbol and smaller than or equal to the second | |
127 | symbol. | |
128 | ||
129 | - help text: "help" or "---help---" | |
130 | This defines a help text. The end of the help text is determined by | |
131 | the indentation level, this means it ends at the first line which has | |
132 | a smaller indentation than the first line of the help text. | |
133 | "---help---" and "help" do not differ in behaviour, "---help---" is | |
53cb4726 | 134 | used to help visually separate configuration logic from help within |
1da177e4 LT |
135 | the file as an aid to developers. |
136 | ||
93449082 RZ |
137 | - misc options: "option" <symbol>[=<value>] |
138 | Various less common options can be defined via this option syntax, | |
139 | which can modify the behaviour of the menu entry and its config | |
140 | symbol. These options are currently possible: | |
141 | ||
142 | - "defconfig_list" | |
143 | This declares a list of default entries which can be used when | |
144 | looking for the default configuration (which is used when the main | |
145 | .config doesn't exists yet.) | |
146 | ||
147 | - "modules" | |
148 | This declares the symbol to be used as the MODULES symbol, which | |
149 | enables the third modular state for all config symbols. | |
e0627813 | 150 | At most one symbol may have the "modules" option set. |
93449082 RZ |
151 | |
152 | - "env"=<value> | |
153 | This imports the environment variable into Kconfig. It behaves like | |
154 | a default, except that the value comes from the environment, this | |
155 | also means that the behaviour when mixing it with normal defaults is | |
156 | undefined at this point. The symbol is currently not exported back | |
157 | to the build environment (if this is desired, it can be done via | |
158 | another symbol). | |
1da177e4 | 159 | |
5d2acfc7 JT |
160 | - "allnoconfig_y" |
161 | This declares the symbol as one that should have the value y when | |
162 | using "allnoconfig". Used for symbols that hide other symbols. | |
163 | ||
1da177e4 LT |
164 | Menu dependencies |
165 | ----------------- | |
166 | ||
167 | Dependencies define the visibility of a menu entry and can also reduce | |
168 | the input range of tristate symbols. The tristate logic used in the | |
169 | expressions uses one more state than normal boolean logic to express the | |
170 | module state. Dependency expressions have the following syntax: | |
171 | ||
172 | <expr> ::= <symbol> (1) | |
173 | <symbol> '=' <symbol> (2) | |
174 | <symbol> '!=' <symbol> (3) | |
175 | '(' <expr> ')' (4) | |
176 | '!' <expr> (5) | |
177 | <expr> '&&' <expr> (6) | |
178 | <expr> '||' <expr> (7) | |
179 | ||
180 | Expressions are listed in decreasing order of precedence. | |
181 | ||
182 | (1) Convert the symbol into an expression. Boolean and tristate symbols | |
183 | are simply converted into the respective expression values. All | |
184 | other symbol types result in 'n'. | |
185 | (2) If the values of both symbols are equal, it returns 'y', | |
186 | otherwise 'n'. | |
187 | (3) If the values of both symbols are equal, it returns 'n', | |
188 | otherwise 'y'. | |
189 | (4) Returns the value of the expression. Used to override precedence. | |
190 | (5) Returns the result of (2-/expr/). | |
191 | (6) Returns the result of min(/expr/, /expr/). | |
192 | (7) Returns the result of max(/expr/, /expr/). | |
193 | ||
194 | An expression can have a value of 'n', 'm' or 'y' (or 0, 1, 2 | |
4280eae0 | 195 | respectively for calculations). A menu entry becomes visible when its |
1da177e4 LT |
196 | expression evaluates to 'm' or 'y'. |
197 | ||
0486bc90 RD |
198 | There are two types of symbols: constant and non-constant symbols. |
199 | Non-constant symbols are the most common ones and are defined with the | |
200 | 'config' statement. Non-constant symbols consist entirely of alphanumeric | |
1da177e4 LT |
201 | characters or underscores. |
202 | Constant symbols are only part of expressions. Constant symbols are | |
83dcde4e | 203 | always surrounded by single or double quotes. Within the quote, any |
1da177e4 LT |
204 | other character is allowed and the quotes can be escaped using '\'. |
205 | ||
206 | Menu structure | |
207 | -------------- | |
208 | ||
209 | The position of a menu entry in the tree is determined in two ways. First | |
210 | it can be specified explicitly: | |
211 | ||
212 | menu "Network device support" | |
bef1f402 | 213 | depends on NET |
1da177e4 LT |
214 | |
215 | config NETDEVICES | |
216 | ... | |
217 | ||
218 | endmenu | |
219 | ||
220 | All entries within the "menu" ... "endmenu" block become a submenu of | |
221 | "Network device support". All subentries inherit the dependencies from | |
222 | the menu entry, e.g. this means the dependency "NET" is added to the | |
223 | dependency list of the config option NETDEVICES. | |
224 | ||
225 | The other way to generate the menu structure is done by analyzing the | |
226 | dependencies. If a menu entry somehow depends on the previous entry, it | |
227 | can be made a submenu of it. First, the previous (parent) symbol must | |
228 | be part of the dependency list and then one of these two conditions | |
229 | must be true: | |
230 | - the child entry must become invisible, if the parent is set to 'n' | |
231 | - the child entry must only be visible, if the parent is visible | |
232 | ||
233 | config MODULES | |
234 | bool "Enable loadable module support" | |
235 | ||
236 | config MODVERSIONS | |
237 | bool "Set version information on all module symbols" | |
bef1f402 | 238 | depends on MODULES |
1da177e4 LT |
239 | |
240 | comment "module support disabled" | |
bef1f402 | 241 | depends on !MODULES |
1da177e4 LT |
242 | |
243 | MODVERSIONS directly depends on MODULES, this means it's only visible if | |
244 | MODULES is different from 'n'. The comment on the other hand is always | |
245 | visible when MODULES is visible (the (empty) dependency of MODULES is | |
246 | also part of the comment dependencies). | |
247 | ||
248 | ||
249 | Kconfig syntax | |
250 | -------------- | |
251 | ||
252 | The configuration file describes a series of menu entries, where every | |
253 | line starts with a keyword (except help texts). The following keywords | |
254 | end a menu entry: | |
255 | - config | |
256 | - menuconfig | |
257 | - choice/endchoice | |
258 | - comment | |
259 | - menu/endmenu | |
260 | - if/endif | |
261 | - source | |
262 | The first five also start the definition of a menu entry. | |
263 | ||
264 | config: | |
265 | ||
266 | "config" <symbol> | |
267 | <config options> | |
268 | ||
269 | This defines a config symbol <symbol> and accepts any of above | |
270 | attributes as options. | |
271 | ||
272 | menuconfig: | |
273 | "menuconfig" <symbol> | |
274 | <config options> | |
275 | ||
53cb4726 | 276 | This is similar to the simple config entry above, but it also gives a |
1da177e4 LT |
277 | hint to front ends, that all suboptions should be displayed as a |
278 | separate list of options. | |
279 | ||
280 | choices: | |
281 | ||
0719e1d2 | 282 | "choice" [symbol] |
1da177e4 LT |
283 | <choice options> |
284 | <choice block> | |
285 | "endchoice" | |
286 | ||
83dcde4e | 287 | This defines a choice group and accepts any of the above attributes as |
1da177e4 LT |
288 | options. A choice can only be of type bool or tristate, while a boolean |
289 | choice only allows a single config entry to be selected, a tristate | |
290 | choice also allows any number of config entries to be set to 'm'. This | |
291 | can be used if multiple drivers for a single hardware exists and only a | |
292 | single driver can be compiled/loaded into the kernel, but all drivers | |
293 | can be compiled as modules. | |
294 | A choice accepts another option "optional", which allows to set the | |
295 | choice to 'n' and no entry needs to be selected. | |
0719e1d2 YM |
296 | If no [symbol] is associated with a choice, then you can not have multiple |
297 | definitions of that choice. If a [symbol] is associated to the choice, | |
298 | then you may define the same choice (ie. with the same entries) in another | |
299 | place. | |
1da177e4 LT |
300 | |
301 | comment: | |
302 | ||
303 | "comment" <prompt> | |
304 | <comment options> | |
305 | ||
306 | This defines a comment which is displayed to the user during the | |
307 | configuration process and is also echoed to the output files. The only | |
308 | possible options are dependencies. | |
309 | ||
310 | menu: | |
311 | ||
312 | "menu" <prompt> | |
313 | <menu options> | |
314 | <menu block> | |
315 | "endmenu" | |
316 | ||
317 | This defines a menu block, see "Menu structure" above for more | |
df835c2e MM |
318 | information. The only possible options are dependencies and "visible" |
319 | attributes. | |
1da177e4 LT |
320 | |
321 | if: | |
322 | ||
323 | "if" <expr> | |
324 | <if block> | |
325 | "endif" | |
326 | ||
327 | This defines an if block. The dependency expression <expr> is appended | |
328 | to all enclosed menu entries. | |
329 | ||
330 | source: | |
331 | ||
332 | "source" <prompt> | |
333 | ||
334 | This reads the specified configuration file. This file is always parsed. | |
6e66b900 RD |
335 | |
336 | mainmenu: | |
337 | ||
338 | "mainmenu" <prompt> | |
339 | ||
340 | This sets the config program's title bar if the config program chooses | |
8ea13e2c AL |
341 | to use it. It should be placed at the top of the configuration, before any |
342 | other statement. | |
0486bc90 RD |
343 | |
344 | ||
345 | Kconfig hints | |
346 | ------------- | |
347 | This is a collection of Kconfig tips, most of which aren't obvious at | |
348 | first glance and most of which have become idioms in several Kconfig | |
349 | files. | |
350 | ||
9b3e4dad SR |
351 | Adding common features and make the usage configurable |
352 | ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ | |
353 | It is a common idiom to implement a feature/functionality that are | |
354 | relevant for some architectures but not all. | |
355 | The recommended way to do so is to use a config variable named HAVE_* | |
356 | that is defined in a common Kconfig file and selected by the relevant | |
357 | architectures. | |
358 | An example is the generic IOMAP functionality. | |
359 | ||
360 | We would in lib/Kconfig see: | |
361 | ||
362 | # Generic IOMAP is used to ... | |
363 | config HAVE_GENERIC_IOMAP | |
364 | ||
365 | config GENERIC_IOMAP | |
366 | depends on HAVE_GENERIC_IOMAP && FOO | |
367 | ||
368 | And in lib/Makefile we would see: | |
369 | obj-$(CONFIG_GENERIC_IOMAP) += iomap.o | |
370 | ||
371 | For each architecture using the generic IOMAP functionality we would see: | |
372 | ||
373 | config X86 | |
374 | select ... | |
375 | select HAVE_GENERIC_IOMAP | |
376 | select ... | |
377 | ||
378 | Note: we use the existing config option and avoid creating a new | |
379 | config variable to select HAVE_GENERIC_IOMAP. | |
380 | ||
381 | Note: the use of the internal config variable HAVE_GENERIC_IOMAP, it is | |
382 | introduced to overcome the limitation of select which will force a | |
383 | config option to 'y' no matter the dependencies. | |
384 | The dependencies are moved to the symbol GENERIC_IOMAP and we avoid the | |
385 | situation where select forces a symbol equals to 'y'. | |
386 | ||
0486bc90 RD |
387 | Build as module only |
388 | ~~~~~~~~~~~~~~~~~~~~ | |
389 | To restrict a component build to module-only, qualify its config symbol | |
390 | with "depends on m". E.g.: | |
391 | ||
392 | config FOO | |
393 | depends on BAR && m | |
394 | ||
395 | limits FOO to module (=m) or disabled (=n). | |
1c199f28 LR |
396 | |
397 | Kconfig recursive dependency limitations | |
398 | ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ | |
399 | ||
400 | If you've hit the Kconfig error: "recursive dependency detected" you've run | |
401 | into a recursive dependency issue with Kconfig, a recursive dependency can be | |
402 | summarized as a circular dependency. The kconfig tools need to ensure that | |
403 | Kconfig files comply with specified configuration requirements. In order to do | |
404 | that kconfig must determine the values that are possible for all Kconfig | |
405 | symbols, this is currently not possible if there is a circular relation | |
406 | between two or more Kconfig symbols. For more details refer to the "Simple | |
407 | Kconfig recursive issue" subsection below. Kconfig does not do recursive | |
408 | dependency resolution; this has a few implications for Kconfig file writers. | |
409 | We'll first explain why this issues exists and then provide an example | |
410 | technical limitation which this brings upon Kconfig developers. Eager | |
411 | developers wishing to try to address this limitation should read the next | |
412 | subsections. | |
413 | ||
414 | Simple Kconfig recursive issue | |
415 | ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ | |
416 | ||
417 | Read: Documentation/kbuild/Kconfig.recursion-issue-01 | |
418 | ||
419 | Test with: | |
420 | ||
421 | make KBUILD_KCONFIG=Documentation/kbuild/Kconfig.recursion-issue-01 allnoconfig | |
422 | ||
423 | Cumulative Kconfig recursive issue | |
424 | ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ | |
425 | ||
426 | Read: Documentation/kbuild/Kconfig.recursion-issue-02 | |
427 | ||
428 | Test with: | |
429 | ||
430 | make KBUILD_KCONFIG=Documentation/kbuild/Kconfig.recursion-issue-02 allnoconfig | |
431 | ||
432 | Practical solutions to kconfig recursive issue | |
433 | ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ | |
434 | ||
435 | Developers who run into the recursive Kconfig issue have three options | |
436 | at their disposal. We document them below and also provide a list of | |
437 | historical issues resolved through these different solutions. | |
438 | ||
439 | a) Remove any superfluous "select FOO" or "depends on FOO" | |
440 | b) Match dependency semantics: | |
441 | b1) Swap all "select FOO" to "depends on FOO" or, | |
442 | b2) Swap all "depends on FOO" to "select FOO" | |
443 | ||
444 | The resolution to a) can be tested with the sample Kconfig file | |
445 | Documentation/kbuild/Kconfig.recursion-issue-01 through the removal | |
446 | of the "select CORE" from CORE_BELL_A_ADVANCED as that is implicit already | |
447 | since CORE_BELL_A depends on CORE. At times it may not be possible to remove | |
448 | some dependency criteria, for such cases you can work with solution b). | |
449 | ||
450 | The two different resolutions for b) can be tested in the sample Kconfig file | |
451 | Documentation/kbuild/Kconfig.recursion-issue-02. | |
452 | ||
453 | Below is a list of examples of prior fixes for these types of recursive issues; | |
454 | all errors appear to involve one or more select's and one or more "depends on". | |
455 | ||
456 | commit fix | |
457 | ====== === | |
458 | 06b718c01208 select A -> depends on A | |
459 | c22eacfe82f9 depends on A -> depends on B | |
460 | 6a91e854442c select A -> depends on A | |
461 | 118c565a8f2e select A -> select B | |
462 | f004e5594705 select A -> depends on A | |
463 | c7861f37b4c6 depends on A -> (null) | |
464 | 80c69915e5fb select A -> (null) (1) | |
465 | c2218e26c0d0 select A -> depends on A (1) | |
466 | d6ae99d04e1c select A -> depends on A | |
467 | 95ca19cf8cbf select A -> depends on A | |
468 | 8f057d7bca54 depends on A -> (null) | |
469 | 8f057d7bca54 depends on A -> select A | |
470 | a0701f04846e select A -> depends on A | |
471 | 0c8b92f7f259 depends on A -> (null) | |
472 | e4e9e0540928 select A -> depends on A (2) | |
473 | 7453ea886e87 depends on A > (null) (1) | |
474 | 7b1fff7e4fdf select A -> depends on A | |
475 | 86c747d2a4f0 select A -> depends on A | |
476 | d9f9ab51e55e select A -> depends on A | |
477 | 0c51a4d8abd6 depends on A -> select A (3) | |
478 | e98062ed6dc4 select A -> depends on A (3) | |
479 | 91e5d284a7f1 select A -> (null) | |
480 | ||
481 | (1) Partial (or no) quote of error. | |
482 | (2) That seems to be the gist of that fix. | |
483 | (3) Same error. | |
484 | ||
485 | Future kconfig work | |
486 | ~~~~~~~~~~~~~~~~~~~ | |
487 | ||
488 | Work on kconfig is welcomed on both areas of clarifying semantics and on | |
489 | evaluating the use of a full SAT solver for it. A full SAT solver can be | |
490 | desirable to enable more complex dependency mappings and / or queries, | |
491 | for instance on possible use case for a SAT solver could be that of handling | |
492 | the current known recursive dependency issues. It is not known if this would | |
493 | address such issues but such evaluation is desirable. If support for a full SAT | |
494 | solver proves too complex or that it cannot address recursive dependency issues | |
495 | Kconfig should have at least clear and well defined semantics which also | |
496 | addresses and documents limitations or requirements such as the ones dealing | |
497 | with recursive dependencies. | |
498 | ||
499 | Further work on both of these areas is welcomed on Kconfig. We elaborate | |
500 | on both of these in the next two subsections. | |
501 | ||
502 | Semantics of Kconfig | |
503 | ~~~~~~~~~~~~~~~~~~~~ | |
504 | ||
505 | The use of Kconfig is broad, Linux is now only one of Kconfig's users: | |
506 | one study has completed a broad analysis of Kconfig use in 12 projects [0]. | |
507 | Despite its widespread use, and although this document does a reasonable job | |
508 | in documenting basic Kconfig syntax a more precise definition of Kconfig | |
509 | semantics is welcomed. One project deduced Kconfig semantics through | |
510 | the use of the xconfig configurator [1]. Work should be done to confirm if | |
511 | the deduced semantics matches our intended Kconfig design goals. | |
512 | ||
513 | Having well defined semantics can be useful for tools for practical | |
514 | evaluation of depenencies, for instance one such use known case was work to | |
515 | express in boolean abstraction of the inferred semantics of Kconfig to | |
516 | translate Kconfig logic into boolean formulas and run a SAT solver on this to | |
517 | find dead code / features (always inactive), 114 dead features were found in | |
518 | Linux using this methodology [1] (Section 8: Threats to validity). | |
519 | ||
520 | Confirming this could prove useful as Kconfig stands as one of the the leading | |
521 | industrial variability modeling languages [1] [2]. Its study would help | |
522 | evaluate practical uses of such languages, their use was only theoretical | |
523 | and real world requirements were not well understood. As it stands though | |
524 | only reverse engineering techniques have been used to deduce semantics from | |
525 | variability modeling languages such as Kconfig [3]. | |
526 | ||
527 | [0] http://www.eng.uwaterloo.ca/~shshe/kconfig_semantics.pdf | |
528 | [1] http://gsd.uwaterloo.ca/sites/default/files/vm-2013-berger.pdf | |
529 | [2] http://gsd.uwaterloo.ca/sites/default/files/ase241-berger_0.pdf | |
530 | [3] http://gsd.uwaterloo.ca/sites/default/files/icse2011.pdf | |
531 | ||
532 | Full SAT solver for Kconfig | |
533 | ~~~~~~~~~~~~~~~~~~~~~~~~~~~ | |
534 | ||
535 | Although SAT solvers [0] haven't yet been used by Kconfig directly, as noted in | |
536 | the previous subsection, work has been done however to express in boolean | |
537 | abstraction the inferred semantics of Kconfig to translate Kconfig logic into | |
538 | boolean formulas and run a SAT solver on it [1]. Another known related project | |
539 | is CADOS [2] (former VAMOS [3]) and the tools, mainly undertaker [4], which has | |
540 | been introduced first with [5]. The basic concept of undertaker is to exract | |
541 | variability models from Kconfig, and put them together with a propositional | |
542 | formula extracted from CPP #ifdefs and build-rules into a SAT solver in order | |
543 | to find dead code, dead files, and dead symbols. If using a SAT solver is | |
544 | desirable on Kconfig one approach would be to evaluate repurposing such efforts | |
545 | somehow on Kconfig. There is enough interest from mentors of existing projects | |
546 | to not only help advise how to integrate this work upstream but also help | |
547 | maintain it long term. Interested developers should visit: | |
548 | ||
549 | http://kernelnewbies.org/KernelProjects/kconfig-sat | |
550 | ||
551 | [0] http://www.cs.cornell.edu/~sabhar/chapters/SATSolvers-KR-Handbook.pdf | |
552 | [1] http://gsd.uwaterloo.ca/sites/default/files/vm-2013-berger.pdf | |
553 | [2] https://cados.cs.fau.de | |
554 | [3] https://vamos.cs.fau.de | |
555 | [4] https://undertaker.cs.fau.de | |
556 | [5] https://www4.cs.fau.de/Publications/2011/tartler_11_eurosys.pdf |