OrgACRN
/
acrn-kernel
mirror of https://github.com/projectacrn/acrn-kernel.git
1
0
Fork 0
Code Issues Releases Wiki Activity

docs: kbuild: add references on Kconfig semantics 

Add references to 1) a research paper which provides a definition of
Kconfig semantics, 2) the kismet tool, which checks for unmet direct
dependency bugs in Kconfig specifications.

Signed-off-by: Paul Gazzillo <paul@pgazz.com>
Signed-off-by: Necip Fazil Yildiran <fazilyildiran@gmail.com>
Signed-off-by: Masahiro Yamada <masahiroy@kernel.org>
This commit is contained in:
Necip Fazil Yildiran 2022-04-05 00:33:51 -04:00 committed by Masahiro Yamada
parent d5ea4fece4
commit cab802b7b8
1 changed files with 6 additions and 0 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

6
Documentation/kbuild/kconfig-language.rst
View File

@ -693,6 +693,8 @@ in documenting basic Kconfig syntax a more precise definition of Kconfig
semantics is welcomed. One project deduced Kconfig semantics through semantics is welcomed. One project deduced Kconfig semantics through
the use of the xconfig configurator [1]_. Work should be done to confirm if the use of the xconfig configurator [1]_. Work should be done to confirm if
the deduced semantics matches our intended Kconfig design goals. the deduced semantics matches our intended Kconfig design goals.
Another project formalized a denotational semantics of a core subset of
the Kconfig language [10]_.
Having well defined semantics can be useful for tools for practical Having well defined semantics can be useful for tools for practical
evaluation of dependencies, for instance one such case was work to evaluation of dependencies, for instance one such case was work to
@ -700,6 +702,8 @@ express in boolean abstraction of the inferred semantics of Kconfig to
translate Kconfig logic into boolean formulas and run a SAT solver on this to translate Kconfig logic into boolean formulas and run a SAT solver on this to
find dead code / features (always inactive), 114 dead features were found in find dead code / features (always inactive), 114 dead features were found in
Linux using this methodology [1]_ (Section 8: Threats to validity). Linux using this methodology [1]_ (Section 8: Threats to validity).
The kismet tool, based on the semantics in [10]_, finds abuses of reverse
dependencies and has led to dozens of committed fixes to Linux Kconfig files [11]_.
Confirming this could prove useful as Kconfig stands as one of the leading Confirming this could prove useful as Kconfig stands as one of the leading
industrial variability modeling languages [1]_ [2]_. Its study would help industrial variability modeling languages [1]_ [2]_. Its study would help
@ -738,3 +742,5 @@ https://kernelnewbies.org/KernelProjects/kconfig-sat
.. [7] https://vamos.cs.fau.de .. [7] https://vamos.cs.fau.de
.. [8] https://undertaker.cs.fau.de .. [8] https://undertaker.cs.fau.de
.. [9] https://www4.cs.fau.de/Publications/2011/tartler_11_eurosys.pdf .. [9] https://www4.cs.fau.de/Publications/2011/tartler_11_eurosys.pdf
.. [10] https://paulgazzillo.com/papers/esecfse21.pdf
.. [11] https://github.com/paulgazz/kmax