diff options
| author | Necip Fazil Yildiran <fazilyildiran@gmail.com> | 2022-04-05 06:33:51 +0200 |
|---|---|---|
| committer | Masahiro Yamada <masahiroy@kernel.org> | 2022-04-06 12:27:41 +0200 |
| commit | cab802b7b8c9eea6fe30161dab77a05d20d76195 (patch) | |
| tree | 26ca8ff2ca7fd65b6a2aed8a89a63bcb76a8474c /Documentation/kbuild | |
| parent | kbuild: Allow kernel installation packaging to override pkg-config (diff) | |
| download | linux-cab802b7b8c9eea6fe30161dab77a05d20d76195.tar.xz linux-cab802b7b8c9eea6fe30161dab77a05d20d76195.zip | |
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>
Diffstat (limited to 'Documentation/kbuild')
| -rw-r--r-- | Documentation/kbuild/kconfig-language.rst | 6 |
1 files changed, 6 insertions, 0 deletions
diff --git a/Documentation/kbuild/kconfig-language.rst b/Documentation/kbuild/kconfig-language.rst index 93a5b6e1fabd..a7173843a294 100644 --- a/Documentation/kbuild/kconfig-language.rst +++ b/Documentation/kbuild/kconfig-language.rst @@ -693,6 +693,8 @@ in documenting basic Kconfig syntax a more precise definition of Kconfig semantics is welcomed. One project deduced Kconfig semantics through the use of the xconfig configurator [1]_. Work should be done to confirm if 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 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 find dead code / features (always inactive), 114 dead features were found in 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 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 .. [8] https://undertaker.cs.fau.de .. [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 |