| Message ID | 20250208163959.3973163-1-ole0811sch@gmail.com (mailing list archive) |
|---|---|
| Headers | show |
| Series | kconfig: Add support for conflict resolution | expand |
On Sun, Feb 9, 2025 at 1:40 AM Ole Schuerks <ole0811sch@gmail.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/
On Mon, Feb 10, 2025 at 02:00:52PM +0900, Masahiro Yamada wrote: > 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. That makes sense. > This approach was suggested by Linus [1], and to achieve that, > the shell evaluation must be dynamically re-evaluated [2]. Sure. > The SAT solver would likely conflict with this plan. At least due to the > significant amount of additional code, which would be an obstacle. I can't see how the toolchain selection, if set on Kconfig can't be leveraged later to enable / disable the SAT solver, however I can see the amount of code shuffling incurred to be an extra hurdle to address and a preference to leave that for later. In other words, I susepct it is still possible to evaluate to add support for the SAT solver post toolchain kconfig integration. Thoughts? Luis
On Tue, Feb 11, 2025 at 12:43 AM Luis Chamberlain <mcgrof@kernel.org> wrote: > > On Mon, Feb 10, 2025 at 02:00:52PM +0900, Masahiro Yamada wrote: > > 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. > > That makes sense. > > > This approach was suggested by Linus [1], and to achieve that, > > the shell evaluation must be dynamically re-evaluated [2]. > > Sure. > > > The SAT solver would likely conflict with this plan. At least due to the > > significant amount of additional code, which would be an obstacle. > > I can't see how the toolchain selection, if set on Kconfig can't be > leveraged later to enable / disable the SAT solver, however I can > see the amount of code shuffling incurred to be an extra hurdle to > address and a preference to leave that for later. > > In other words, I susepct it is still possible to evaluate to > add support for the SAT solver post toolchain kconfig integration. > > Thoughts? It depends on how the dynamic shell evaluation is implemented. This is not limited to bool/tristate, but SAT solver only works for those two types.
Quick follow-up. On our end, our SAT-solver implementations can be easily adapted to accommodate your future toolchain selection refactorings. Also, could you share with us the timelines for your refactorings so we can plan and deliver the adjusted SAT-solver patches. Best Regards, Jude Gyimah On 2/11/25 01:46, Masahiro Yamada wrote: > On Tue, Feb 11, 2025 at 12:43 AM Luis Chamberlain <mcgrof@kernel.org> wrote: >> On Mon, Feb 10, 2025 at 02:00:52PM +0900, Masahiro Yamada wrote: >>> 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. >> That makes sense. >> >>> This approach was suggested by Linus [1], and to achieve that, >>> the shell evaluation must be dynamically re-evaluated [2]. >> Sure. >> >>> The SAT solver would likely conflict with this plan. At least due to the >>> significant amount of additional code, which would be an obstacle. >> I can't see how the toolchain selection, if set on Kconfig can't be >> leveraged later to enable / disable the SAT solver, however I can >> see the amount of code shuffling incurred to be an extra hurdle to >> address and a preference to leave that for later. >> >> In other words, I susepct it is still possible to evaluate to >> add support for the SAT solver post toolchain kconfig integration. >> >> Thoughts? > > It depends on how the dynamic shell evaluation is implemented. > This is not limited to bool/tristate, but SAT solver only works for > those two types. > > > >