LKML Archive mirror
 help / color / mirror / Atom feed
* [PATCH v4 00/12] kconfig: Add support for conflict resolution
@ 2024-07-10  6:52 Ole Schuerks
  2024-07-10  6:52 ` [PATCH v4 01/12] kconfig: Add picosat.h Ole Schuerks
                   ` (11 more replies)
  0 siblings, 12 replies; 25+ messages in thread
From: Ole Schuerks @ 2024-07-10  6:52 UTC (permalink / raw)
  To: linux-kbuild
  Cc: ole0811sch, jude.gyimah, thorsten.berger, deltaone, jan.sollmann,
	mcgrof, masahiroy, linux-kernel

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-20240703.

[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>

Ole Schuerks (12):
  kconfig: Add picosat.h
  kconfig: Add picosat.c (1/3)
  kconfig: Add picosat.c (2/3)
  kconfig: Add picosat.c (3/3)
  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

 scripts/kconfig/.gitignore       |    1 +
 scripts/kconfig/Makefile         |   13 +-
 scripts/kconfig/cf_constraints.c | 1720 ++++++
 scripts/kconfig/cf_constraints.h |   26 +
 scripts/kconfig/cf_defs.h        |  287 +
 scripts/kconfig/cf_expr.c        | 2594 +++++++++
 scripts/kconfig/cf_expr.h        |  296 ++
 scripts/kconfig/cf_rangefix.c    | 1066 ++++
 scripts/kconfig/cf_rangefix.h    |   21 +
 scripts/kconfig/cf_utils.c       | 1031 ++++
 scripts/kconfig/cf_utils.h       |  115 +
 scripts/kconfig/cfoutconfig.c    |  142 +
 scripts/kconfig/configfix.c      |  337 ++
 scripts/kconfig/configfix.h      |   40 +
 scripts/kconfig/expr.h           |   17 +
 scripts/kconfig/loader.gif       |  Bin 0 -> 4177 bytes
 scripts/kconfig/picosat.c        | 8502 ++++++++++++++++++++++++++++++
 scripts/kconfig/picosat.h        |  658 +++
 scripts/kconfig/qconf.cc         |  515 +-
 scripts/kconfig/qconf.h          |  103 +
 20 files changed, 17480 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 100644 scripts/kconfig/loader.gif
 create mode 100644 scripts/kconfig/picosat.c
 create mode 100644 scripts/kconfig/picosat.h

-- 
2.39.2


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

end of thread, other threads:[~2024-09-20  9:07 UTC | newest]

Thread overview: 25+ messages (download: mbox.gz follow: Atom feed
-- links below jump to the message on this page --
2024-07-10  6:52 [PATCH v4 00/12] kconfig: Add support for conflict resolution Ole Schuerks
2024-07-10  6:52 ` [PATCH v4 01/12] kconfig: Add picosat.h Ole Schuerks
2024-07-10  6:52 ` [PATCH v4 02/12] kconfig: Add picosat.c (1/3) Ole Schuerks
2024-08-12  8:41   ` Masahiro Yamada
2024-08-16 10:20     ` Ole Schuerks
2024-08-19 22:04       ` Luis Chamberlain
2024-08-29 21:23         ` Ole Schuerks
2024-09-05  8:55           ` Luis Chamberlain
2024-09-20  9:07             ` Ole Schuerks
2024-07-10  6:52 ` [PATCH v4 03/12] kconfig: Add picosat.c (2/3) Ole Schuerks
2024-07-10  6:52 ` [PATCH v4 04/12] kconfig: Add picosat.c (3/3) Ole Schuerks
2024-07-10  6:52 ` [PATCH v4 05/12] kconfig: Add definitions Ole Schuerks
2024-07-10  6:52 ` [PATCH v4 06/12] kconfig: Add files for building constraints Ole Schuerks
2024-08-12  8:49   ` Masahiro Yamada
2024-08-12 10:00     ` Masahiro Yamada
2024-07-10  6:52 ` [PATCH v4 07/12] kconfig: Add files for handling expressions Ole Schuerks
2024-08-12  8:46   ` Masahiro Yamada
2024-08-16 10:23     ` Ole Schuerks
2024-07-10  6:52 ` [PATCH v4 08/12] kconfig: Add files for RangeFix Ole Schuerks
2024-07-10  6:52 ` [PATCH v4 09/12] kconfig: Add files with utility functions Ole Schuerks
2024-08-12  8:48   ` Masahiro Yamada
2024-07-10  6:52 ` [PATCH v4 10/12] kconfig: Add tools Ole Schuerks
2024-07-10  6:52 ` [PATCH v4 11/12] kconfig: Add xconfig-modifications Ole Schuerks
2024-08-12  9:28   ` Masahiro Yamada
2024-07-10  6:52 ` [PATCH v4 12/12] kconfig: Add loader.gif Ole Schuerks

This is a public inbox, see mirroring instructions
for how to clone and mirror all data and code used for this inbox;
as well as URLs for read-only IMAP folder(s) and NNTP newsgroup(s).