On Mon, Oct 28, 2024 at 04:49:38AM +0100, Ole Schuerks wrote:
> Hi,
>
> Configuring a kernel requires a forward enabling approach where one enables
> each option one needs at a time. If one enables an option that selects
> other options, these options are no longer de-selectable by design.
> Likewise, if one has enabled an option which creates a conflict with a
> secondary option one wishes to enable, one cannot easily enable that
> secondary option, unless one is willing to spend time analyzing the
> dependencies that led to this conflict. Sometimes, these conflicts are not
> easy to understand [0,1].
This paragraph is a bit too researchy, move it to:
https://kernelnewbies.org/KernelProjects/kconfig-sat
> This patch series (for linux-next) provides support to enable users to
> express their desired target configuration and display possible resolutions
> to their conflicts. This support is provided within xconfig.
This should be your next cover letter's first paragraph.
> Conflict resolution is provided by translating kconfig's configuration
> option tree to a propositional formula, and then allowing our resolution
> algorithm, which uses a SAT solver (picosat, implemented in C) calculate
> the possible fixes for an expressed target kernel configuration.
Just say something like:
Conflict resolution is provided by translating kconfig's configuration
option tree to a propositional formula and allowing our resolution
algorithm and picosat to calculate the possible fixes for an expressed
target kernel configuration. Picosat is the smallest and most robust C
SAT solver we could find which is also GPL compatible. <insert
information about the efforts done to also provide debian packages
for picosat and briefly mention how picosat is used as library>.
> New UI extensions are made to xconfig with panes and buttons to allow users
> to express new desired target options, calculate fixes, and apply any of
> found solutions.
This can be the third paragraph.
> We created a separate test infrastructure that we used to validate the
> correctness of the suggestions made. It shows that our resolution algorithm
> resolves around 95% of the conflicts. We plan to incorporate this with a
> later patch series.
>
> We envision that our translation of the kconfig option tree into a
> propositional formula could potentially also later be repurposed to address
> other problems. An example is checking the consistency between the use of
> ifdefs and logic expressed in kconfig files. We suspect that this could,
> for example, help avoid invalid kconfig configurations and help with ifdef
> maintenance.
I think these two paragraphs are very forward lookjng and can be just
put into the wiki for now.
> You can see a YouTube video demonstrating this work [2]. This effort is
> part of the kernelnewbies Kconfig-SAT project [3], the approach and effort
> is also explained in detail in our paper [4]. The results from the
> evaluation have significantly improved since then: Around 80 % of the
> conflicts could be resolved, and 99.9 % of the generated fixes resolved the
> conflict. It is also our attempt at contributing back to the kernel
> community, whose configurator researchers studied a lot.
I think this is a nice final paragraph summary for the research to
include.
> Patches applicable to next-20241025.
>
> [0] https://gsd.uwaterloo.ca/sites/default/files/vamos12-survey.pdf
> [1] https://www.linux-magazine.com/Issues/2021/244/Kconfig-Deep-Dive
> [2] https://www.youtube.com/watch?v=vn2JgK_PTbc
> [3] https://kernelnewbies.org/KernelProjects/kconfig-sat
> [4] http://www.cse.chalmers.se/~bergert/paper/2021-icseseip-configfix.pdf
>
> Thanks from the team! (and thanks to Luis Chamberlain for guiding us here)
Sure.
> Co-developed-by: Patrick Franz <deltaone@debian.org>
> Signed-off-by: Patrick Franz <deltaone@debian.org>
> Co-developed-by: Ibrahim Fayaz <phayax@gmail.com>
> Signed-off-by: Ibrahim Fayaz <phayax@gmail.com>
> Reviewed-by: Luis Chamberlain <mcgrof@kernel.org>
> Tested-by: Evgeny Groshev <eugene.groshev@gmail.com>
> Suggested-by: Sarah Nadi <nadi@ualberta.ca>
> Suggested-by: Thorsten Berger <thorsten.berger@rub.de>
> Signed-off-by: Thorsten Berger <thorsten.berger@rub.de>
> Signed-off-by: Ole Schuerks <ole0811sch@gmail.com>
This all can be removed, patch tags have no meaning for cover letters.
> Changelog v6:
> * remove script for manually installing PicoSAT
> * adapt documentation and help text in the GUI accordingly
> * convert Qt signal/slot connects to new style
It is wonderful you are keeping tabs of the changes on the cover letter,
keep it up!
Luis