Linux kbuild/kconfig development
 help / color / mirror / Atom feed
* [PATCH v7 00/11] kconfig: Add support for conflict resolution
@ 2025-02-08 16:39 Ole Schuerks
  2025-02-08 16:39 ` [PATCH v7 01/11] kconfig: Add PicoSAT interface Ole Schuerks
                   ` (11 more replies)
  0 siblings, 12 replies; 22+ messages in thread
From: Ole Schuerks @ 2025-02-08 16:39 UTC (permalink / raw)
  To: linux-kbuild
  Cc: ole0811sch, jude.gyimah, thorsten.berger, deltaone, jan.sollmann,
	mcgrof, masahiroy, linux-kernel, nathan, nicolas

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"

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

Changelog v5:
* use lists from scripts/include/list.h
* use PicoSAT as a dynamically loaded library
* Fix GUI bug that made the displayed tables editable
* Allow cycling through the desired values of a symbol in the conflict view
  in the GUI by clicking on the cell
* Fix usage of "NO" instead of "N" etc. in some places in the GUI
* Improve function naming
* Add documentation
* Simlify xcalloc to xmalloc in some places
* Fix allocation bug in fexpr_add_to_satmap() and init_data()
* Remove functions pexpr_eliminate_dups() and print_expr()

Ole Schuerks (11):
  kconfig: Add PicoSAT interface
  kconfig: Add definitions
  kbuild: Add list_count_nodes and list_for_each_entry_from
  kconfig: Add files for building constraints
  kconfig: Add files for handling expressions
  kconfig: Add files for fix generation
  kconfig: Add files with utility functions
  kconfig: Add tools
  kconfig: Add xconfig-modifications
  kconfig: Add loader.gif
  kconfig: Add documentation for the conflict resolver

 Documentation/kbuild/kconfig.rst    |   56 +
 scripts/include/list.h              |   26 +
 scripts/kconfig/.gitignore          |    1 +
 scripts/kconfig/Makefile            |   11 +-
 scripts/kconfig/cf_constraints.c    | 1777 ++++++++++++++++++++++++
 scripts/kconfig/cf_constraints.h    |   24 +
 scripts/kconfig/cf_defs.h           |  391 ++++++
 scripts/kconfig/cf_expr.c           | 2003 +++++++++++++++++++++++++++
 scripts/kconfig/cf_expr.h           |  181 +++
 scripts/kconfig/cf_fixgen.c         | 1136 +++++++++++++++
 scripts/kconfig/cf_fixgen.h         |   21 +
 scripts/kconfig/cf_utils.c          |  980 +++++++++++++
 scripts/kconfig/cf_utils.h          |  136 ++
 scripts/kconfig/cfoutconfig.c       |  149 ++
 scripts/kconfig/configfix.c         |  352 +++++
 scripts/kconfig/configfix.h         |   31 +
 scripts/kconfig/expr.h              |   17 +
 scripts/kconfig/loader.gif          |  Bin 0 -> 4177 bytes
 scripts/kconfig/picosat_functions.c |   79 ++
 scripts/kconfig/picosat_functions.h |   35 +
 scripts/kconfig/qconf.cc            |  676 ++++++++-
 scripts/kconfig/qconf.h             |  111 ++
 22 files changed, 8189 insertions(+), 4 deletions(-)
 create mode 100644 scripts/kconfig/cf_constraints.c
 create mode 100644 scripts/kconfig/cf_constraints.h
 create mode 100644 scripts/kconfig/cf_defs.h
 create mode 100644 scripts/kconfig/cf_expr.c
 create mode 100644 scripts/kconfig/cf_expr.h
 create mode 100644 scripts/kconfig/cf_fixgen.c
 create mode 100644 scripts/kconfig/cf_fixgen.h
 create mode 100644 scripts/kconfig/cf_utils.c
 create mode 100644 scripts/kconfig/cf_utils.h
 create mode 100644 scripts/kconfig/cfoutconfig.c
 create mode 100644 scripts/kconfig/configfix.c
 create mode 100644 scripts/kconfig/configfix.h
 create mode 100644 scripts/kconfig/loader.gif
 create mode 100644 scripts/kconfig/picosat_functions.c
 create mode 100644 scripts/kconfig/picosat_functions.h

-- 
2.39.5


^ permalink raw reply	[flat|nested] 22+ messages in thread

end of thread, other threads:[~2025-04-09 18:09 UTC | newest]

Thread overview: 22+ messages (download: mbox.gz follow: Atom feed
-- links below jump to the message on this page --
2025-02-08 16:39 [PATCH v7 00/11] kconfig: Add support for conflict resolution Ole Schuerks
2025-02-08 16:39 ` [PATCH v7 01/11] kconfig: Add PicoSAT interface Ole Schuerks
2025-02-10 15:37   ` Luis Chamberlain
2025-02-08 16:39 ` [PATCH v7 02/11] kconfig: Add definitions Ole Schuerks
2025-02-08 16:39 ` [PATCH v7 03/11] kbuild: Add list_count_nodes and list_for_each_entry_from Ole Schuerks
2025-02-10 15:36   ` Luis Chamberlain
2025-02-08 16:39 ` [PATCH v7 04/11] kconfig: Add files for building constraints Ole Schuerks
2025-02-08 16:39 ` [PATCH v7 05/11] kconfig: Add files for handling expressions Ole Schuerks
2025-02-08 16:39 ` [PATCH v7 06/11] kconfig: Add files for fix generation Ole Schuerks
2025-02-08 16:39 ` [PATCH v7 07/11] kconfig: Add files with utility functions Ole Schuerks
2025-02-08 16:39 ` [PATCH v7 08/11] kconfig: Add tools Ole Schuerks
2025-02-08 16:39 ` [PATCH v7 09/11] kconfig: Add xconfig-modifications Ole Schuerks
2025-02-08 16:39 ` [PATCH v7 10/11] kconfig: Add loader.gif Ole Schuerks
2025-02-08 16:39 ` [PATCH v7 11/11] kconfig: Add documentation for the conflict resolver Ole Schuerks
2025-02-10  5:00 ` [PATCH v7 00/11] kconfig: Add support for conflict resolution Masahiro Yamada
2025-02-10 15:43   ` Luis Chamberlain
2025-02-11  0:46     ` Masahiro Yamada
2025-02-21  3:16       ` Jude Gyimah
     [not found]       ` <ac98e417-1587-4806-9576-7661acc6bf6e@ruhr-uni-bochum.de>
2025-03-02 16:56         ` Masahiro Yamada
2025-03-23  8:40           ` Luis Chamberlain
2025-03-23  8:55             ` Luis Chamberlain
2025-04-09 18:08       ` Ole Schuerks

This is a public inbox, see mirroring instructions
for how to clone and mirror all data and code used for this inbox