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 | |
3e2ba95f DG |
244 | MODULES is different from 'n'. The comment on the other hand is only |
245 | visible when MODULES is set to 'n'. | |
1da177e4 LT |
246 | |
247 | ||
248 | Kconfig syntax | |
249 | -------------- | |
250 | ||
251 | The configuration file describes a series of menu entries, where every | |
252 | line starts with a keyword (except help texts). The following keywords | |
253 | end a menu entry: | |
254 | - config | |
255 | - menuconfig | |
256 | - choice/endchoice | |
257 | - comment | |
258 | - menu/endmenu | |
259 | - if/endif | |
260 | - source | |
261 | The first five also start the definition of a menu entry. | |
262 | ||
263 | config: | |
264 | ||
265 | "config" <symbol> | |
266 | <config options> | |
267 | ||
268 | This defines a config symbol <symbol> and accepts any of above | |
269 | attributes as options. | |
270 | ||
271 | menuconfig: | |
272 | "menuconfig" <symbol> | |
273 | <config options> | |
274 | ||
53cb4726 | 275 | This is similar to the simple config entry above, but it also gives a |
1da177e4 LT |
276 | hint to front ends, that all suboptions should be displayed as a |
277 | separate list of options. | |
278 | ||
279 | choices: | |
280 | ||
0719e1d2 | 281 | "choice" [symbol] |
1da177e4 LT |
282 | <choice options> |
283 | <choice block> | |
284 | "endchoice" | |
285 | ||
83dcde4e | 286 | This defines a choice group and accepts any of the above attributes as |
032a3187 DG |
287 | options. A choice can only be of type bool or tristate. If no type is |
288 | specified for a choice, it's type will be determined by the type of | |
289 | the first choice element in the group or remain unknown if none of the | |
290 | choice elements have a type specified, as well. | |
291 | ||
292 | While a boolean choice only allows a single config entry to be | |
293 | selected, a tristate choice also allows any number of config entries | |
294 | to be set to 'm'. This can be used if multiple drivers for a single | |
295 | hardware exists and only a single driver can be compiled/loaded into | |
296 | the kernel, but all drivers can be compiled as modules. | |
297 | ||
1da177e4 LT |
298 | A choice accepts another option "optional", which allows to set the |
299 | choice to 'n' and no entry needs to be selected. | |
0719e1d2 YM |
300 | If no [symbol] is associated with a choice, then you can not have multiple |
301 | definitions of that choice. If a [symbol] is associated to the choice, | |
302 | then you may define the same choice (ie. with the same entries) in another | |
303 | place. | |
1da177e4 LT |
304 | |
305 | comment: | |
306 | ||
307 | "comment" <prompt> | |
308 | <comment options> | |
309 | ||
310 | This defines a comment which is displayed to the user during the | |
311 | configuration process and is also echoed to the output files. The only | |
312 | possible options are dependencies. | |
313 | ||
314 | menu: | |
315 | ||
316 | "menu" <prompt> | |
317 | <menu options> | |
318 | <menu block> | |
319 | "endmenu" | |
320 | ||
321 | This defines a menu block, see "Menu structure" above for more | |
df835c2e MM |
322 | information. The only possible options are dependencies and "visible" |
323 | attributes. | |
1da177e4 LT |
324 | |
325 | if: | |
326 | ||
327 | "if" <expr> | |
328 | <if block> | |
329 | "endif" | |
330 | ||
331 | This defines an if block. The dependency expression <expr> is appended | |
332 | to all enclosed menu entries. | |
333 | ||
334 | source: | |
335 | ||
336 | "source" <prompt> | |
337 | ||
338 | This reads the specified configuration file. This file is always parsed. | |
6e66b900 RD |
339 | |
340 | mainmenu: | |
341 | ||
342 | "mainmenu" <prompt> | |
343 | ||
344 | This sets the config program's title bar if the config program chooses | |
8ea13e2c AL |
345 | to use it. It should be placed at the top of the configuration, before any |
346 | other statement. | |
0486bc90 RD |
347 | |
348 | ||
349 | Kconfig hints | |
350 | ------------- | |
351 | This is a collection of Kconfig tips, most of which aren't obvious at | |
352 | first glance and most of which have become idioms in several Kconfig | |
353 | files. | |
354 | ||
9b3e4dad SR |
355 | Adding common features and make the usage configurable |
356 | ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ | |
357 | It is a common idiom to implement a feature/functionality that are | |
358 | relevant for some architectures but not all. | |
359 | The recommended way to do so is to use a config variable named HAVE_* | |
360 | that is defined in a common Kconfig file and selected by the relevant | |
361 | architectures. | |
362 | An example is the generic IOMAP functionality. | |
363 | ||
364 | We would in lib/Kconfig see: | |
365 | ||
366 | # Generic IOMAP is used to ... | |
367 | config HAVE_GENERIC_IOMAP | |
368 | ||
369 | config GENERIC_IOMAP | |
370 | depends on HAVE_GENERIC_IOMAP && FOO | |
371 | ||
372 | And in lib/Makefile we would see: | |
373 | obj-$(CONFIG_GENERIC_IOMAP) += iomap.o | |
374 | ||
375 | For each architecture using the generic IOMAP functionality we would see: | |
376 | ||
377 | config X86 | |
378 | select ... | |
379 | select HAVE_GENERIC_IOMAP | |
380 | select ... | |
381 | ||
382 | Note: we use the existing config option and avoid creating a new | |
383 | config variable to select HAVE_GENERIC_IOMAP. | |
384 | ||
385 | Note: the use of the internal config variable HAVE_GENERIC_IOMAP, it is | |
386 | introduced to overcome the limitation of select which will force a | |
387 | config option to 'y' no matter the dependencies. | |
388 | The dependencies are moved to the symbol GENERIC_IOMAP and we avoid the | |
389 | situation where select forces a symbol equals to 'y'. | |
390 | ||
0486bc90 RD |
391 | Build as module only |
392 | ~~~~~~~~~~~~~~~~~~~~ | |
393 | To restrict a component build to module-only, qualify its config symbol | |
394 | with "depends on m". E.g.: | |
395 | ||
396 | config FOO | |
397 | depends on BAR && m | |
398 | ||
399 | limits FOO to module (=m) or disabled (=n). | |
1c199f28 LR |
400 | |
401 | Kconfig recursive dependency limitations | |
402 | ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ | |
403 | ||
404 | If you've hit the Kconfig error: "recursive dependency detected" you've run | |
405 | into a recursive dependency issue with Kconfig, a recursive dependency can be | |
406 | summarized as a circular dependency. The kconfig tools need to ensure that | |
407 | Kconfig files comply with specified configuration requirements. In order to do | |
408 | that kconfig must determine the values that are possible for all Kconfig | |
409 | symbols, this is currently not possible if there is a circular relation | |
410 | between two or more Kconfig symbols. For more details refer to the "Simple | |
411 | Kconfig recursive issue" subsection below. Kconfig does not do recursive | |
412 | dependency resolution; this has a few implications for Kconfig file writers. | |
413 | We'll first explain why this issues exists and then provide an example | |
414 | technical limitation which this brings upon Kconfig developers. Eager | |
415 | developers wishing to try to address this limitation should read the next | |
416 | subsections. | |
417 | ||
418 | Simple Kconfig recursive issue | |
419 | ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ | |
420 | ||
421 | Read: Documentation/kbuild/Kconfig.recursion-issue-01 | |
422 | ||
423 | Test with: | |
424 | ||
425 | make KBUILD_KCONFIG=Documentation/kbuild/Kconfig.recursion-issue-01 allnoconfig | |
426 | ||
427 | Cumulative Kconfig recursive issue | |
428 | ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ | |
429 | ||
430 | Read: Documentation/kbuild/Kconfig.recursion-issue-02 | |
431 | ||
432 | Test with: | |
433 | ||
434 | make KBUILD_KCONFIG=Documentation/kbuild/Kconfig.recursion-issue-02 allnoconfig | |
435 | ||
436 | Practical solutions to kconfig recursive issue | |
437 | ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ | |
438 | ||
439 | Developers who run into the recursive Kconfig issue have three options | |
440 | at their disposal. We document them below and also provide a list of | |
441 | historical issues resolved through these different solutions. | |
442 | ||
443 | a) Remove any superfluous "select FOO" or "depends on FOO" | |
444 | b) Match dependency semantics: | |
445 | b1) Swap all "select FOO" to "depends on FOO" or, | |
446 | b2) Swap all "depends on FOO" to "select FOO" | |
447 | ||
448 | The resolution to a) can be tested with the sample Kconfig file | |
449 | Documentation/kbuild/Kconfig.recursion-issue-01 through the removal | |
450 | of the "select CORE" from CORE_BELL_A_ADVANCED as that is implicit already | |
451 | since CORE_BELL_A depends on CORE. At times it may not be possible to remove | |
452 | some dependency criteria, for such cases you can work with solution b). | |
453 | ||
454 | The two different resolutions for b) can be tested in the sample Kconfig file | |
455 | Documentation/kbuild/Kconfig.recursion-issue-02. | |
456 | ||
457 | Below is a list of examples of prior fixes for these types of recursive issues; | |
458 | all errors appear to involve one or more select's and one or more "depends on". | |
459 | ||
460 | commit fix | |
461 | ====== === | |
462 | 06b718c01208 select A -> depends on A | |
463 | c22eacfe82f9 depends on A -> depends on B | |
464 | 6a91e854442c select A -> depends on A | |
465 | 118c565a8f2e select A -> select B | |
466 | f004e5594705 select A -> depends on A | |
467 | c7861f37b4c6 depends on A -> (null) | |
468 | 80c69915e5fb select A -> (null) (1) | |
469 | c2218e26c0d0 select A -> depends on A (1) | |
470 | d6ae99d04e1c select A -> depends on A | |
471 | 95ca19cf8cbf select A -> depends on A | |
472 | 8f057d7bca54 depends on A -> (null) | |
473 | 8f057d7bca54 depends on A -> select A | |
474 | a0701f04846e select A -> depends on A | |
475 | 0c8b92f7f259 depends on A -> (null) | |
476 | e4e9e0540928 select A -> depends on A (2) | |
477 | 7453ea886e87 depends on A > (null) (1) | |
478 | 7b1fff7e4fdf select A -> depends on A | |
479 | 86c747d2a4f0 select A -> depends on A | |
480 | d9f9ab51e55e select A -> depends on A | |
481 | 0c51a4d8abd6 depends on A -> select A (3) | |
482 | e98062ed6dc4 select A -> depends on A (3) | |
483 | 91e5d284a7f1 select A -> (null) | |
484 | ||
485 | (1) Partial (or no) quote of error. | |
486 | (2) That seems to be the gist of that fix. | |
487 | (3) Same error. | |
488 | ||
489 | Future kconfig work | |
490 | ~~~~~~~~~~~~~~~~~~~ | |
491 | ||
492 | Work on kconfig is welcomed on both areas of clarifying semantics and on | |
493 | evaluating the use of a full SAT solver for it. A full SAT solver can be | |
494 | desirable to enable more complex dependency mappings and / or queries, | |
495 | for instance on possible use case for a SAT solver could be that of handling | |
496 | the current known recursive dependency issues. It is not known if this would | |
497 | address such issues but such evaluation is desirable. If support for a full SAT | |
498 | solver proves too complex or that it cannot address recursive dependency issues | |
499 | Kconfig should have at least clear and well defined semantics which also | |
500 | addresses and documents limitations or requirements such as the ones dealing | |
501 | with recursive dependencies. | |
502 | ||
503 | Further work on both of these areas is welcomed on Kconfig. We elaborate | |
504 | on both of these in the next two subsections. | |
505 | ||
506 | Semantics of Kconfig | |
507 | ~~~~~~~~~~~~~~~~~~~~ | |
508 | ||
509 | The use of Kconfig is broad, Linux is now only one of Kconfig's users: | |
510 | one study has completed a broad analysis of Kconfig use in 12 projects [0]. | |
511 | Despite its widespread use, and although this document does a reasonable job | |
512 | in documenting basic Kconfig syntax a more precise definition of Kconfig | |
513 | semantics is welcomed. One project deduced Kconfig semantics through | |
514 | the use of the xconfig configurator [1]. Work should be done to confirm if | |
515 | the deduced semantics matches our intended Kconfig design goals. | |
516 | ||
517 | Having well defined semantics can be useful for tools for practical | |
518 | evaluation of depenencies, for instance one such use known case was work to | |
519 | express in boolean abstraction of the inferred semantics of Kconfig to | |
520 | translate Kconfig logic into boolean formulas and run a SAT solver on this to | |
521 | find dead code / features (always inactive), 114 dead features were found in | |
522 | Linux using this methodology [1] (Section 8: Threats to validity). | |
523 | ||
524 | Confirming this could prove useful as Kconfig stands as one of the the leading | |
525 | industrial variability modeling languages [1] [2]. Its study would help | |
526 | evaluate practical uses of such languages, their use was only theoretical | |
527 | and real world requirements were not well understood. As it stands though | |
528 | only reverse engineering techniques have been used to deduce semantics from | |
529 | variability modeling languages such as Kconfig [3]. | |
530 | ||
531 | [0] http://www.eng.uwaterloo.ca/~shshe/kconfig_semantics.pdf | |
532 | [1] http://gsd.uwaterloo.ca/sites/default/files/vm-2013-berger.pdf | |
533 | [2] http://gsd.uwaterloo.ca/sites/default/files/ase241-berger_0.pdf | |
534 | [3] http://gsd.uwaterloo.ca/sites/default/files/icse2011.pdf | |
535 | ||
536 | Full SAT solver for Kconfig | |
537 | ~~~~~~~~~~~~~~~~~~~~~~~~~~~ | |
538 | ||
539 | Although SAT solvers [0] haven't yet been used by Kconfig directly, as noted in | |
540 | the previous subsection, work has been done however to express in boolean | |
541 | abstraction the inferred semantics of Kconfig to translate Kconfig logic into | |
542 | boolean formulas and run a SAT solver on it [1]. Another known related project | |
543 | is CADOS [2] (former VAMOS [3]) and the tools, mainly undertaker [4], which has | |
544 | been introduced first with [5]. The basic concept of undertaker is to exract | |
545 | variability models from Kconfig, and put them together with a propositional | |
546 | formula extracted from CPP #ifdefs and build-rules into a SAT solver in order | |
547 | to find dead code, dead files, and dead symbols. If using a SAT solver is | |
548 | desirable on Kconfig one approach would be to evaluate repurposing such efforts | |
549 | somehow on Kconfig. There is enough interest from mentors of existing projects | |
550 | to not only help advise how to integrate this work upstream but also help | |
551 | maintain it long term. Interested developers should visit: | |
552 | ||
553 | http://kernelnewbies.org/KernelProjects/kconfig-sat | |
554 | ||
555 | [0] http://www.cs.cornell.edu/~sabhar/chapters/SATSolvers-KR-Handbook.pdf | |
556 | [1] http://gsd.uwaterloo.ca/sites/default/files/vm-2013-berger.pdf | |
557 | [2] https://cados.cs.fau.de | |
558 | [3] https://vamos.cs.fau.de | |
559 | [4] https://undertaker.cs.fau.de | |
560 | [5] https://www4.cs.fau.de/Publications/2011/tartler_11_eurosys.pdf |