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 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.
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.
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.
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.
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-20240917.
[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)
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>
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
kbuild: Add list_is_{first,last}, list_size, list_at_index,
list_for_each_from
kconfig: Add definitions
kconfig: Add files for building constraints
kconfig: Add files for handling expressions
kconfig: Add files for RangeFix
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 | 53 +
scripts/include/list.h | 71 +
scripts/kconfig/.gitignore | 1 +
scripts/kconfig/Makefile | 11 +-
scripts/kconfig/cf_constraints.c | 1789 ++++++++++++++++++++++++
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_rangefix.c | 1136 +++++++++++++++
scripts/kconfig/cf_rangefix.h | 21 +
scripts/kconfig/cf_utils.c | 980 +++++++++++++
scripts/kconfig/cf_utils.h | 112 ++
scripts/kconfig/cfoutconfig.c | 149 ++
scripts/kconfig/configfix.c | 351 +++++
scripts/kconfig/configfix.h | 31 +
scripts/kconfig/expr.h | 17 +
scripts/kconfig/install-picosat.sh | 29 +
scripts/kconfig/loader.gif | Bin 0 -> 4177 bytes
scripts/kconfig/picosat_functions.c | 74 +
scripts/kconfig/picosat_functions.h | 35 +
scripts/kconfig/qconf.cc | 623 ++++++++-
scripts/kconfig/qconf.h | 111 ++
23 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_rangefix.c
create mode 100644 scripts/kconfig/cf_rangefix.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 100755 scripts/kconfig/install-picosat.sh
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.2