Kbuild: rename CC_STACKPROTECTOR[_STRONG] config variables
[linux-2.6-block.git] / Documentation / kbuild / kconfig-language.txt
CommitLineData
1da177e4
LT
1Introduction
2------------
3
e95be9a5 4The configuration database is a collection of configuration options
1da177e4
LT
5organized 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
20Every entry has its own dependencies. These dependencies are used
21to determine the visibility of an entry. Any child entry is only
22visible if its parent entry is also visible.
23
24Menu entries
25------------
26
0486bc90 27Most entries define a config option; all other entries help to organize
1da177e4
LT
28them. A single configuration option is defined like this:
29
30config 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
37Every line starts with a key word and can be followed by multiple
38arguments. "config" starts a new config entry. The following lines
39define attributes for this config option. Attributes can be the type of
40the config option, input prompt, dependencies, help text and default
41values. A config option can be defined multiple times with the same
42name, but every definition can have only a single input prompt and the
43type must not conflict.
44
45Menu attributes
46---------------
47
48A menu entry can have a number of attributes. Not all of them are
49applicable 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
b7d4ec39
DHV
80 The default value deliberately defaults to 'n' in order to avoid bloating the
81 build. With few exceptions, new config options should not change this. The
82 intent is for "make oldconfig" to add as little as possible to the config from
83 release to release.
84
85 Note:
86 Things that merit "default y/m" include:
87
88 a) A new Kconfig option for something that used to always be built
89 should be "default y".
90
91 b) A new gatekeeping Kconfig option that hides/shows other Kconfig
92 options (but does not generate any code of its own), should be
93 "default y" so people will see those other options.
94
95 c) Sub-driver behavior or similar options for a driver that is
96 "default n". This allows you to provide sane defaults.
97
98 d) Hardware or infrastructure that everybody expects, such as CONFIG_NET
99 or CONFIG_BLOCK. These are rare exceptions.
100
6e66b900
RD
101- type definition + default value:
102 "def_bool"/"def_tristate" <expr> ["if" <expr>]
103 This is a shorthand notation for a type definition plus a value.
104 Optionally dependencies for this default value can be added with "if".
105
106- dependencies: "depends on" <expr>
1da177e4 107 This defines a dependency for this menu entry. If multiple
83dcde4e 108 dependencies are defined, they are connected with '&&'. Dependencies
1da177e4
LT
109 are applied to all other options within this menu entry (which also
110 accept an "if" expression), so these two examples are equivalent:
111
112 bool "foo" if BAR
113 default y if BAR
114 and
115 depends on BAR
116 bool "foo"
117 default y
118
119- reverse dependencies: "select" <symbol> ["if" <expr>]
120 While normal dependencies reduce the upper limit of a symbol (see
121 below), reverse dependencies can be used to force a lower limit of
122 another symbol. The value of the current menu symbol is used as the
123 minimal value <symbol> can be set to. If <symbol> is selected multiple
124 times, the limit is set to the largest selection.
125 Reverse dependencies can only be used with boolean or tristate
126 symbols.
f8a74594 127 Note:
dfecbec8
MW
128 select should be used with care. select will force
129 a symbol to a value without visiting the dependencies.
130 By abusing select you are able to select a symbol FOO even
131 if FOO depends on BAR that is not set.
132 In general use select only for non-visible symbols
133 (no prompts anywhere) and for symbols with no dependencies.
134 That will limit the usefulness but on the other hand avoid
135 the illegal configurations all over.
1da177e4 136
237e3ad0
NP
137- weak reverse dependencies: "imply" <symbol> ["if" <expr>]
138 This is similar to "select" as it enforces a lower limit on another
139 symbol except that the "implied" symbol's value may still be set to n
140 from a direct dependency or with a visible prompt.
141
142 Given the following example:
143
144 config FOO
145 tristate
146 imply BAZ
147
148 config BAZ
149 tristate
150 depends on BAR
151
152 The following values are possible:
153
154 FOO BAR BAZ's default choice for BAZ
155 --- --- ------------- --------------
156 n y n N/m/y
157 m y m M/y/n
158 y y y Y/n
159 y n * N
160
161 This is useful e.g. with multiple drivers that want to indicate their
162 ability to hook into a secondary subsystem while allowing the user to
163 configure that subsystem out without also having to unset these drivers.
164
df835c2e
MM
165- limiting menu display: "visible if" <expr>
166 This attribute is only applicable to menu blocks, if the condition is
167 false, the menu block is not displayed to the user (the symbols
168 contained there can still be selected by other symbols, though). It is
40e47125 169 similar to a conditional "prompt" attribute for individual menu
df835c2e
MM
170 entries. Default value of "visible" is true.
171
1da177e4
LT
172- numerical ranges: "range" <symbol> <symbol> ["if" <expr>]
173 This allows to limit the range of possible input values for int
174 and hex symbols. The user can only input a value which is larger than
175 or equal to the first symbol and smaller than or equal to the second
176 symbol.
177
178- help text: "help" or "---help---"
179 This defines a help text. The end of the help text is determined by
180 the indentation level, this means it ends at the first line which has
181 a smaller indentation than the first line of the help text.
182 "---help---" and "help" do not differ in behaviour, "---help---" is
53cb4726 183 used to help visually separate configuration logic from help within
1da177e4
LT
184 the file as an aid to developers.
185
93449082
RZ
186- misc options: "option" <symbol>[=<value>]
187 Various less common options can be defined via this option syntax,
188 which can modify the behaviour of the menu entry and its config
189 symbol. These options are currently possible:
190
191 - "defconfig_list"
192 This declares a list of default entries which can be used when
193 looking for the default configuration (which is used when the main
194 .config doesn't exists yet.)
195
196 - "modules"
197 This declares the symbol to be used as the MODULES symbol, which
198 enables the third modular state for all config symbols.
e0627813 199 At most one symbol may have the "modules" option set.
93449082 200
5d2acfc7
JT
201 - "allnoconfig_y"
202 This declares the symbol as one that should have the value y when
203 using "allnoconfig". Used for symbols that hide other symbols.
204
1da177e4
LT
205Menu dependencies
206-----------------
207
208Dependencies define the visibility of a menu entry and can also reduce
209the input range of tristate symbols. The tristate logic used in the
210expressions uses one more state than normal boolean logic to express the
211module state. Dependency expressions have the following syntax:
212
213<expr> ::= <symbol> (1)
214 <symbol> '=' <symbol> (2)
215 <symbol> '!=' <symbol> (3)
9059a349
NP
216 <symbol1> '<' <symbol2> (4)
217 <symbol1> '>' <symbol2> (4)
218 <symbol1> '<=' <symbol2> (4)
219 <symbol1> '>=' <symbol2> (4)
220 '(' <expr> ')' (5)
221 '!' <expr> (6)
222 <expr> '&&' <expr> (7)
223 <expr> '||' <expr> (8)
1da177e4
LT
224
225Expressions are listed in decreasing order of precedence.
226
227(1) Convert the symbol into an expression. Boolean and tristate symbols
228 are simply converted into the respective expression values. All
229 other symbol types result in 'n'.
230(2) If the values of both symbols are equal, it returns 'y',
231 otherwise 'n'.
232(3) If the values of both symbols are equal, it returns 'n',
233 otherwise 'y'.
9059a349
NP
234(4) If value of <symbol1> is respectively lower, greater, lower-or-equal,
235 or greater-or-equal than value of <symbol2>, it returns 'y',
236 otherwise 'n'.
237(5) Returns the value of the expression. Used to override precedence.
238(6) Returns the result of (2-/expr/).
239(7) Returns the result of min(/expr/, /expr/).
240(8) Returns the result of max(/expr/, /expr/).
1da177e4
LT
241
242An expression can have a value of 'n', 'm' or 'y' (or 0, 1, 2
4280eae0 243respectively for calculations). A menu entry becomes visible when its
1da177e4
LT
244expression evaluates to 'm' or 'y'.
245
0486bc90
RD
246There are two types of symbols: constant and non-constant symbols.
247Non-constant symbols are the most common ones and are defined with the
248'config' statement. Non-constant symbols consist entirely of alphanumeric
1da177e4
LT
249characters or underscores.
250Constant symbols are only part of expressions. Constant symbols are
83dcde4e 251always surrounded by single or double quotes. Within the quote, any
1da177e4
LT
252other character is allowed and the quotes can be escaped using '\'.
253
254Menu structure
255--------------
256
257The position of a menu entry in the tree is determined in two ways. First
258it can be specified explicitly:
259
260menu "Network device support"
bef1f402 261 depends on NET
1da177e4
LT
262
263config NETDEVICES
264 ...
265
266endmenu
267
268All entries within the "menu" ... "endmenu" block become a submenu of
269"Network device support". All subentries inherit the dependencies from
270the menu entry, e.g. this means the dependency "NET" is added to the
271dependency list of the config option NETDEVICES.
272
273The other way to generate the menu structure is done by analyzing the
274dependencies. If a menu entry somehow depends on the previous entry, it
275can be made a submenu of it. First, the previous (parent) symbol must
276be part of the dependency list and then one of these two conditions
277must be true:
278- the child entry must become invisible, if the parent is set to 'n'
279- the child entry must only be visible, if the parent is visible
280
281config MODULES
282 bool "Enable loadable module support"
283
284config MODVERSIONS
285 bool "Set version information on all module symbols"
bef1f402 286 depends on MODULES
1da177e4
LT
287
288comment "module support disabled"
bef1f402 289 depends on !MODULES
1da177e4
LT
290
291MODVERSIONS directly depends on MODULES, this means it's only visible if
3e2ba95f
DG
292MODULES is different from 'n'. The comment on the other hand is only
293visible when MODULES is set to 'n'.
1da177e4
LT
294
295
296Kconfig syntax
297--------------
298
299The configuration file describes a series of menu entries, where every
300line starts with a keyword (except help texts). The following keywords
301end a menu entry:
302- config
303- menuconfig
304- choice/endchoice
305- comment
306- menu/endmenu
307- if/endif
308- source
309The first five also start the definition of a menu entry.
310
311config:
312
313 "config" <symbol>
314 <config options>
315
316This defines a config symbol <symbol> and accepts any of above
317attributes as options.
318
319menuconfig:
320 "menuconfig" <symbol>
321 <config options>
322
53cb4726 323This is similar to the simple config entry above, but it also gives a
1da177e4 324hint to front ends, that all suboptions should be displayed as a
cfd7c612
ER
325separate list of options. To make sure all the suboptions will really
326show up under the menuconfig entry and not outside of it, every item
327from the <config options> list must depend on the menuconfig symbol.
328In practice, this is achieved by using one of the next two constructs:
329
330(1):
331menuconfig M
332if M
333 config C1
334 config C2
335endif
336
337(2):
338menuconfig M
339config C1
340 depends on M
341config C2
342 depends on M
343
344In the following examples (3) and (4), C1 and C2 still have the M
345dependency, but will not appear under menuconfig M anymore, because
346of C0, which doesn't depend on M:
347
348(3):
349menuconfig M
350 config C0
351if M
352 config C1
353 config C2
354endif
355
356(4):
357menuconfig M
358config C0
359config C1
360 depends on M
361config C2
362 depends on M
1da177e4
LT
363
364choices:
365
0719e1d2 366 "choice" [symbol]
1da177e4
LT
367 <choice options>
368 <choice block>
369 "endchoice"
370
83dcde4e 371This defines a choice group and accepts any of the above attributes as
032a3187
DG
372options. A choice can only be of type bool or tristate. If no type is
373specified for a choice, it's type will be determined by the type of
374the first choice element in the group or remain unknown if none of the
375choice elements have a type specified, as well.
376
377While a boolean choice only allows a single config entry to be
378selected, a tristate choice also allows any number of config entries
379to be set to 'm'. This can be used if multiple drivers for a single
380hardware exists and only a single driver can be compiled/loaded into
381the kernel, but all drivers can be compiled as modules.
382
1da177e4
LT
383A choice accepts another option "optional", which allows to set the
384choice to 'n' and no entry needs to be selected.
0719e1d2
YM
385If no [symbol] is associated with a choice, then you can not have multiple
386definitions of that choice. If a [symbol] is associated to the choice,
387then you may define the same choice (ie. with the same entries) in another
388place.
1da177e4
LT
389
390comment:
391
392 "comment" <prompt>
393 <comment options>
394
395This defines a comment which is displayed to the user during the
396configuration process and is also echoed to the output files. The only
397possible options are dependencies.
398
399menu:
400
401 "menu" <prompt>
402 <menu options>
403 <menu block>
404 "endmenu"
405
406This defines a menu block, see "Menu structure" above for more
df835c2e
MM
407information. The only possible options are dependencies and "visible"
408attributes.
1da177e4
LT
409
410if:
411
412 "if" <expr>
413 <if block>
414 "endif"
415
416This defines an if block. The dependency expression <expr> is appended
417to all enclosed menu entries.
418
419source:
420
421 "source" <prompt>
422
423This reads the specified configuration file. This file is always parsed.
6e66b900
RD
424
425mainmenu:
426
427 "mainmenu" <prompt>
428
429This sets the config program's title bar if the config program chooses
8ea13e2c
AL
430to use it. It should be placed at the top of the configuration, before any
431other statement.
0486bc90
RD
432
433
434Kconfig hints
435-------------
436This is a collection of Kconfig tips, most of which aren't obvious at
437first glance and most of which have become idioms in several Kconfig
438files.
439
9b3e4dad
SR
440Adding common features and make the usage configurable
441~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
442It is a common idiom to implement a feature/functionality that are
443relevant for some architectures but not all.
444The recommended way to do so is to use a config variable named HAVE_*
445that is defined in a common Kconfig file and selected by the relevant
446architectures.
447An example is the generic IOMAP functionality.
448
449We would in lib/Kconfig see:
450
451# Generic IOMAP is used to ...
452config HAVE_GENERIC_IOMAP
453
454config GENERIC_IOMAP
455 depends on HAVE_GENERIC_IOMAP && FOO
456
457And in lib/Makefile we would see:
458obj-$(CONFIG_GENERIC_IOMAP) += iomap.o
459
460For each architecture using the generic IOMAP functionality we would see:
461
462config X86
463 select ...
464 select HAVE_GENERIC_IOMAP
465 select ...
466
467Note: we use the existing config option and avoid creating a new
468config variable to select HAVE_GENERIC_IOMAP.
469
470Note: the use of the internal config variable HAVE_GENERIC_IOMAP, it is
471introduced to overcome the limitation of select which will force a
472config option to 'y' no matter the dependencies.
473The dependencies are moved to the symbol GENERIC_IOMAP and we avoid the
474situation where select forces a symbol equals to 'y'.
475
8373b7d9
MY
476Adding features that need compiler support
477~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
478
479There are several features that need compiler support. The recommended way
480to describe the dependency on the compiler feature is to use "depends on"
481followed by a test macro.
482
050e9baa 483config STACKPROTECTOR
8373b7d9
MY
484 bool "Stack Protector buffer overflow detection"
485 depends on $(cc-option,-fstack-protector)
486 ...
487
488If you need to expose a compiler capability to makefiles and/or C source files,
489CC_HAS_ is the recommended prefix for the config option.
490
491config CC_HAS_STACKPROTECTOR_NONE
492 def_bool $(cc-option,-fno-stack-protector)
493
0486bc90
RD
494Build as module only
495~~~~~~~~~~~~~~~~~~~~
496To restrict a component build to module-only, qualify its config symbol
497with "depends on m". E.g.:
498
499config FOO
500 depends on BAR && m
501
502limits FOO to module (=m) or disabled (=n).
1c199f28
LR
503
504Kconfig recursive dependency limitations
505~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
506
507If you've hit the Kconfig error: "recursive dependency detected" you've run
508into a recursive dependency issue with Kconfig, a recursive dependency can be
509summarized as a circular dependency. The kconfig tools need to ensure that
510Kconfig files comply with specified configuration requirements. In order to do
511that kconfig must determine the values that are possible for all Kconfig
512symbols, this is currently not possible if there is a circular relation
513between two or more Kconfig symbols. For more details refer to the "Simple
514Kconfig recursive issue" subsection below. Kconfig does not do recursive
515dependency resolution; this has a few implications for Kconfig file writers.
516We'll first explain why this issues exists and then provide an example
517technical limitation which this brings upon Kconfig developers. Eager
518developers wishing to try to address this limitation should read the next
519subsections.
520
521Simple Kconfig recursive issue
522~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
523
524Read: Documentation/kbuild/Kconfig.recursion-issue-01
525
526Test with:
527
528make KBUILD_KCONFIG=Documentation/kbuild/Kconfig.recursion-issue-01 allnoconfig
529
530Cumulative Kconfig recursive issue
531~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
532
533Read: Documentation/kbuild/Kconfig.recursion-issue-02
534
535Test with:
536
537make KBUILD_KCONFIG=Documentation/kbuild/Kconfig.recursion-issue-02 allnoconfig
538
539Practical solutions to kconfig recursive issue
540~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
541
542Developers who run into the recursive Kconfig issue have three options
543at their disposal. We document them below and also provide a list of
544historical issues resolved through these different solutions.
545
546 a) Remove any superfluous "select FOO" or "depends on FOO"
547 b) Match dependency semantics:
548 b1) Swap all "select FOO" to "depends on FOO" or,
549 b2) Swap all "depends on FOO" to "select FOO"
237e3ad0 550 c) Consider the use of "imply" instead of "select"
1c199f28
LR
551
552The resolution to a) can be tested with the sample Kconfig file
553Documentation/kbuild/Kconfig.recursion-issue-01 through the removal
554of the "select CORE" from CORE_BELL_A_ADVANCED as that is implicit already
555since CORE_BELL_A depends on CORE. At times it may not be possible to remove
556some dependency criteria, for such cases you can work with solution b).
557
558The two different resolutions for b) can be tested in the sample Kconfig file
559Documentation/kbuild/Kconfig.recursion-issue-02.
560
561Below is a list of examples of prior fixes for these types of recursive issues;
562all errors appear to involve one or more select's and one or more "depends on".
563
564commit fix
565====== ===
56606b718c01208 select A -> depends on A
567c22eacfe82f9 depends on A -> depends on B
5686a91e854442c select A -> depends on A
569118c565a8f2e select A -> select B
570f004e5594705 select A -> depends on A
571c7861f37b4c6 depends on A -> (null)
57280c69915e5fb select A -> (null) (1)
573c2218e26c0d0 select A -> depends on A (1)
574d6ae99d04e1c select A -> depends on A
57595ca19cf8cbf select A -> depends on A
5768f057d7bca54 depends on A -> (null)
5778f057d7bca54 depends on A -> select A
578a0701f04846e select A -> depends on A
5790c8b92f7f259 depends on A -> (null)
580e4e9e0540928 select A -> depends on A (2)
5817453ea886e87 depends on A > (null) (1)
5827b1fff7e4fdf select A -> depends on A
58386c747d2a4f0 select A -> depends on A
584d9f9ab51e55e select A -> depends on A
5850c51a4d8abd6 depends on A -> select A (3)
586e98062ed6dc4 select A -> depends on A (3)
58791e5d284a7f1 select A -> (null)
588
589(1) Partial (or no) quote of error.
590(2) That seems to be the gist of that fix.
591(3) Same error.
592
593Future kconfig work
594~~~~~~~~~~~~~~~~~~~
595
596Work on kconfig is welcomed on both areas of clarifying semantics and on
597evaluating the use of a full SAT solver for it. A full SAT solver can be
598desirable to enable more complex dependency mappings and / or queries,
599for instance on possible use case for a SAT solver could be that of handling
600the current known recursive dependency issues. It is not known if this would
601address such issues but such evaluation is desirable. If support for a full SAT
602solver proves too complex or that it cannot address recursive dependency issues
603Kconfig should have at least clear and well defined semantics which also
604addresses and documents limitations or requirements such as the ones dealing
605with recursive dependencies.
606
607Further work on both of these areas is welcomed on Kconfig. We elaborate
608on both of these in the next two subsections.
609
610Semantics of Kconfig
611~~~~~~~~~~~~~~~~~~~~
612
613The use of Kconfig is broad, Linux is now only one of Kconfig's users:
614one study has completed a broad analysis of Kconfig use in 12 projects [0].
615Despite its widespread use, and although this document does a reasonable job
616in documenting basic Kconfig syntax a more precise definition of Kconfig
617semantics is welcomed. One project deduced Kconfig semantics through
618the use of the xconfig configurator [1]. Work should be done to confirm if
619the deduced semantics matches our intended Kconfig design goals.
620
621Having well defined semantics can be useful for tools for practical
622evaluation of depenencies, for instance one such use known case was work to
623express in boolean abstraction of the inferred semantics of Kconfig to
624translate Kconfig logic into boolean formulas and run a SAT solver on this to
625find dead code / features (always inactive), 114 dead features were found in
626Linux using this methodology [1] (Section 8: Threats to validity).
627
628Confirming this could prove useful as Kconfig stands as one of the the leading
629industrial variability modeling languages [1] [2]. Its study would help
630evaluate practical uses of such languages, their use was only theoretical
631and real world requirements were not well understood. As it stands though
632only reverse engineering techniques have been used to deduce semantics from
633variability modeling languages such as Kconfig [3].
634
635[0] http://www.eng.uwaterloo.ca/~shshe/kconfig_semantics.pdf
636[1] http://gsd.uwaterloo.ca/sites/default/files/vm-2013-berger.pdf
637[2] http://gsd.uwaterloo.ca/sites/default/files/ase241-berger_0.pdf
638[3] http://gsd.uwaterloo.ca/sites/default/files/icse2011.pdf
639
640Full SAT solver for Kconfig
641~~~~~~~~~~~~~~~~~~~~~~~~~~~
642
643Although SAT solvers [0] haven't yet been used by Kconfig directly, as noted in
644the previous subsection, work has been done however to express in boolean
645abstraction the inferred semantics of Kconfig to translate Kconfig logic into
646boolean formulas and run a SAT solver on it [1]. Another known related project
647is CADOS [2] (former VAMOS [3]) and the tools, mainly undertaker [4], which has
648been introduced first with [5]. The basic concept of undertaker is to exract
649variability models from Kconfig, and put them together with a propositional
650formula extracted from CPP #ifdefs and build-rules into a SAT solver in order
651to find dead code, dead files, and dead symbols. If using a SAT solver is
652desirable on Kconfig one approach would be to evaluate repurposing such efforts
653somehow on Kconfig. There is enough interest from mentors of existing projects
654to not only help advise how to integrate this work upstream but also help
655maintain it long term. Interested developers should visit:
656
657http://kernelnewbies.org/KernelProjects/kconfig-sat
658
659[0] http://www.cs.cornell.edu/~sabhar/chapters/SATSolvers-KR-Handbook.pdf
660[1] http://gsd.uwaterloo.ca/sites/default/files/vm-2013-berger.pdf
661[2] https://cados.cs.fau.de
662[3] https://vamos.cs.fau.de
663[4] https://undertaker.cs.fau.de
664[5] https://www4.cs.fau.de/Publications/2011/tartler_11_eurosys.pdf