All of lore.kernel.org
 help / color / mirror / Atom feed
* [RFC 0/12] kconfig: add support for conflict resolution
@ 2021-10-20  9:32 Thorsten Berger
  2021-10-20  9:35 ` [RFC 01/12] Add picosat.h Thorsten Berger
                   ` (11 more replies)
  0 siblings, 12 replies; 15+ messages in thread
From: Thorsten Berger @ 2021-10-20  9:32 UTC (permalink / raw)
  To: linux-kbuild
  Cc: Luis R. Rodriguez, deltaone, phayax, Eugene Groshev, Sarah Nadi,
	Mel Gorman, Luis R. Rodriguez

Hi,

(resending everything with smaller patches)

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 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]. It is also our attempt at contributing
back to the kernel community, whose configurator researchers studied a lot.

Patches applicable to linux-next.

[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://youtu.be/vyX7zCRiLKU
[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@suse.com>
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>


Patrick Franz (12):
  Add picosat.h
  Add picosat.c (1/3)
  Add picosat.c (2/3)
  Add picosat.c (3/3)
  Add definitions
  Add files for building constraints
  Add files for handling expressions
  Add files for RangeFix
  Add files with utility functions
  Add tools
  Add xconfig-modifications
  Simplify dependencies for MODULE_SIG_KEY_TYPE_RSA &
    MODULE_SIG_KEY_TYPE_ECDSA

 certs/Kconfig                    |    3 +-
 scripts/kconfig/Makefile         |   19 +-
 scripts/kconfig/cf_constraints.c | 1219 +++++
 scripts/kconfig/cf_constraints.h |   23 +
 scripts/kconfig/cf_defs.h        |  233 +
 scripts/kconfig/cf_expr.c        | 2146 ++++++++
 scripts/kconfig/cf_expr.h        |  237 +
 scripts/kconfig/cf_rangefix.c    | 1017 ++++
 scripts/kconfig/cf_rangefix.h    |   18 +
 scripts/kconfig/cf_satutils.c    |  536 ++
 scripts/kconfig/cf_satutils.h    |   30 +
 scripts/kconfig/cf_utils.c       |  510 ++
 scripts/kconfig/cf_utils.h       |   90 +
 scripts/kconfig/cfconfig.c       |  176 +
 scripts/kconfig/cfoutconfig.c    |  128 +
 scripts/kconfig/configfix.c      |  420 ++
 scripts/kconfig/configfix.h      |   41 +
 scripts/kconfig/expr.h           |   13 +
 scripts/kconfig/picosat.c        | 8502 ++++++++++++++++++++++++++++++
 scripts/kconfig/picosat.h        |  658 +++
 scripts/kconfig/qconf.cc         | 1003 +++-
 scripts/kconfig/qconf.h          |  179 +-
 22 files changed, 16943 insertions(+), 258 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_satutils.c
 create mode 100644 scripts/kconfig/cf_satutils.h
 create mode 100644 scripts/kconfig/cf_utils.c
 create mode 100644 scripts/kconfig/cf_utils.h
 create mode 100644 scripts/kconfig/cfconfig.c
 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/picosat.c
 create mode 100644 scripts/kconfig/picosat.h

-- 
2.33.0

-- 
Prof. Dr. Thorsten Berger
Chair of Software Engineering
Faculty of Computer Science
Ruhr University Bochum, Germany

http://www.thorsten-berger.net
Tel.: +49 (0) 234 32 25975
Mob.: +49 (0) 160 926 878 10
Skype: tberger.work


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

end of thread, other threads:[~2021-10-28  2:49 UTC | newest]

Thread overview: 15+ messages (download: mbox.gz / follow: Atom feed)
-- links below jump to the message on this page --
2021-10-20  9:32 [RFC 0/12] kconfig: add support for conflict resolution Thorsten Berger
2021-10-20  9:35 ` [RFC 01/12] Add picosat.h Thorsten Berger
2021-10-20 15:54   ` Luis Chamberlain
2021-10-20  9:36 ` [RFC 02/12] Add picosat.c (1/3) Thorsten Berger
2021-10-20  9:37 ` [RFC 03/12] Add picosat.c (2/3) Thorsten Berger
2021-10-20  9:38 ` [RFC 04/12] Add picosat.c (3/3) Thorsten Berger
2021-10-20  9:40 ` [RFC 05/12] Add definitions Thorsten Berger
2021-10-20  9:41 ` [RFC 06/12] Add files for building constraints Thorsten Berger
2021-10-20  9:43 ` [RFC 07/12] Add files for handling expressions Thorsten Berger
2021-10-20  9:44 ` [RFC 08/12] Add files for RangeFix Thorsten Berger
2021-10-20  9:45 ` [RFC 09/12] Add files with utility functions Thorsten Berger
2021-10-20  9:46 ` [RFC 10/12] Add tools Thorsten Berger
2021-10-20  9:48 ` [RFC 11/12] Add xconfig-modifications Thorsten Berger
2021-10-20  9:49 ` [RFC 12/12] Simplify dependencies for MODULE_SIG_KEY_TYPE_RSA & MODULE_SIG_KEY_TYPE_ECDSA Thorsten Berger
2021-10-28  2:48   ` Masahiro Yamada

This is an external index of several public inboxes,
see mirroring instructions on how to clone and mirror
all data and code used by this external index.