Message-ID: <CAK7LNAQBBKfSwQ=z3yBchg--gcrAykWz6xvpAYWKse9R9g8KVQ@mail.gmail.com>
Date: Mon, 10 Feb 2025 14:00:52 +0900
From: Masahiro Yamada <masahiroy@...nel.org>
To: Ole Schuerks <ole0811sch@...il.com>
Cc: linux-kbuild@...r.kernel.org, jude.gyimah@....de, thorsten.berger@....de, 
	deltaone@...ian.org, jan.sollmann@....de, mcgrof@...nel.org, 
	linux-kernel@...r.kernel.org, nathan@...nel.org, nicolas@...sle.eu
Subject: Re: [PATCH v7 00/11] kconfig: Add support for conflict resolution

On Sun, Feb 9, 2025 at 1:40 AM Ole Schuerks <ole0811sch@...il.com> wrote:
>
> Hi,
>
> This patch series (for next-20250207) provides support to enable users
> to express their desired target configuration and display possible
> resolutions to their conflicts. This support is provided within xconfig.
>
> 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. PicoSAT is used as a
> dynamically loaded library. For Debian and Fedora, the apt and dnf packages
> named "picosat" provide the library. For other distros, we provide
> instructions on how PicoSAT needs to be compiled from the sources in the
> documentation.
>
> 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.
>
> 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.
>
> Patches applicable to next-20250207.
>
> [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)
>
> Changelog v7:
> * improve error handling when loading picosat symbols with dlsym(): use
>   dlerror() instead of checking for NULL
> * move list_at_index from scripts/include/list.h to
>   scripts/kconfig/cf_utils.h
> * change interface of list_for_each_entry_from and rename list_size to
>   list_count_nodes to more closely match scripts/include/list.h
> * change misleading name "rangefix" of fix generation algorithm to
>   "fixgen"



Thanks for this, but I have no plans to merge the SAT solver.

The reason is that my future plan is to move toolchain selection
to the Kconfig stage instead of specifying it statically from the command line.
This approach was suggested by Linus [1], and to achieve that,
the shell evaluation must be dynamically re-evaluated [2].

The SAT solver would likely conflict with this plan. At least due to the
significant amount of additional code, which would be an obstacle.


[1] https://lore.kernel.org/lkml/CAHk-=whdrvCkSWh=BRrwZwNo3=yLBXXM88NGx8VEpP1VTgmkyQ@mail.gmail.com/

[2] https://lore.kernel.org/lkml/CAK7LNATe7Ah-ow9wYGrtL9i4z-VD=MCo=sJjbC_S0ofEoH6CFQ@mail.gmail.com/


-- 
Best Regards
Masahiro Yamada

Powered by blists - more mailing lists