* [PATCH] docs: kbuild: add references on Kconfig semantics
@ 2022-04-05 4:33 Necip Fazil Yildiran
2022-04-06 14:53 ` Masahiro Yamada
0 siblings, 1 reply; 2+ messages in thread
From: Necip Fazil Yildiran @ 2022-04-05 4:33 UTC (permalink / raw)
To: masahiroy; +Cc: linux-kernel, linux-doc, linux-kbuild, paul, fazilyildiran
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>
---
Documentation/kbuild/kconfig-language.rst | 6 ++++++
1 file changed, 6 insertions(+)
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
--
2.25.1
^ permalink raw reply related [flat|nested] 2+ messages in thread
* Re: [PATCH] docs: kbuild: add references on Kconfig semantics
2022-04-05 4:33 [PATCH] docs: kbuild: add references on Kconfig semantics Necip Fazil Yildiran
@ 2022-04-06 14:53 ` Masahiro Yamada
0 siblings, 0 replies; 2+ messages in thread
From: Masahiro Yamada @ 2022-04-06 14:53 UTC (permalink / raw)
To: Necip Fazil Yildiran
Cc: Linux Kernel Mailing List, open list:DOCUMENTATION,
Linux Kbuild mailing list, paul
On Tue, Apr 5, 2022 at 1:34 PM Necip Fazil Yildiran
<fazilyildiran@gmail.com> wrote:
>
> 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>
> ---
Applied to linux-kbuild. Thanks.
> Documentation/kbuild/kconfig-language.rst | 6 ++++++
> 1 file changed, 6 insertions(+)
>
> 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
> --
> 2.25.1
>
--
Best Regards
Masahiro Yamada
^ permalink raw reply [flat|nested] 2+ messages in thread
end of thread, other threads:[~2022-04-06 16:55 UTC | newest]
Thread overview: 2+ messages (download: mbox.gz / follow: Atom feed)
-- links below jump to the message on this page --
2022-04-05 4:33 [PATCH] docs: kbuild: add references on Kconfig semantics Necip Fazil Yildiran
2022-04-06 14:53 ` Masahiro Yamada
This is an external index of several public inboxes,
see mirroring instructions on how to clone and mirror
all data and code used by this external index.