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@xxxxxxxxxx> > Signed-off-by: Patrick Franz <deltaone@xxxxxxxxxx> > Co-developed-by: Ibrahim Fayaz <phayax@xxxxxxxxx> > Signed-off-by: Ibrahim Fayaz <phayax@xxxxxxxxx> > Reviewed-by: Luis Chamberlain <mcgrof@xxxxxxxxxx> > Tested-by: Evgeny Groshev <eugene.groshev@xxxxxxxxx> > Suggested-by: Sarah Nadi <nadi@xxxxxxxxxxx> > Suggested-by: Thorsten Berger <thorsten.berger@xxxxxx> > Signed-off-by: Thorsten Berger <thorsten.berger@xxxxxx> > Signed-off-by: Ole Schuerks <ole0811sch@xxxxxxxxx> 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
