GSoC project: Improving kconfig using a SAT solver
in [Kernel]
|
Prev: [2.6.34 PATCH] USB: option.c: OLIVETTI OLICARD100 support
Next: [PATCH] perf_events: fix errors path in perf_output_begin() (take 3)
From: Andi Kleen on 17 May 2010 08:20 Vegard Nossum <vegard.nossum(a)gmail.com> writes: > I just wanted to say that I've been accepted into this year's Google > Summer of Code program and will spend this summer working on improving > the kconfig system in a very particular direction: I want to integrate > a proper boolean constraint satisfiability solver into the > configuration editors (menuconfig, etc.) in order to allow > partial/incomplete configuration specifications. In short, this means > that the user can choose to not specify a particular value for some > config options, but let the system deduce their values. This will > hopefully improve usability and also solve the select problem once and > for all. Nice idea. I read your proposal and it looks good. I assume you got inspired by the libzypp use of a SAT solver for package dependencies? One problem that is visible there is that it can be hard to display conflicts in a nice and understandable way to the user, especially if there are lots of dependencies. It might be worth planning in some time to solve that nicely. -Andi -- ak(a)linux.intel.com -- Speaking for myself only. -- To unsubscribe from this list: send the line "unsubscribe linux-kernel" in the body of a message to majordomo(a)vger.kernel.org More majordomo info at http://vger.kernel.org/majordomo-info.html Please read the FAQ at http://www.tux.org/lkml/
From: Vegard Nossum on 17 May 2010 09:10 On 17 May 2010 14:13, Andi Kleen <andi(a)firstfloor.org> wrote: > Vegard Nossum <vegard.nossum(a)gmail.com> writes: > >> I just wanted to say that I've been accepted into this year's Google >> Summer of Code program and will spend this summer working on improving >> the kconfig system in a very particular direction: I want to integrate >> a proper boolean constraint satisfiability solver into the >> configuration editors (menuconfig, etc.) in order to allow >> partial/incomplete configuration specifications. In short, this means >> that the user can choose to not specify a particular value for some >> config options, but let the system deduce their values. This will >> hopefully improve usability and also solve the select problem once and >> for all. > > Nice idea. I read your proposal and it looks good. > > I assume you got inspired by the libzypp use of a SAT solver > for package dependencies? One problem that is visible there > is that it can be hard to display conflicts in a nice and understandable > way to the user, especially if there are lots of dependencies. > > It might be worth planning in some time to solve that nicely. Thanks! I didn't actually get inspired by libzypp -- but somebody else mentioned it too, so I guess I should take a look! You bring up a valid point, and I admittedly haven't given it VERY much thought yet, but I think that conflicts could be displayed in the following way: If an instance is unsolvable, then it means that all possible valuations/assignments make at least one clause (disjunction) false. Each clause is usually generated by exactly one dependency specification (the "depends on" directive), so we could print these dependencies to the screen as suggestions for how to resolve the conflict. Vegard -- To unsubscribe from this list: send the line "unsubscribe linux-kernel" in the body of a message to majordomo(a)vger.kernel.org More majordomo info at http://vger.kernel.org/majordomo-info.html Please read the FAQ at http://www.tux.org/lkml/
From: James Bottomley on 17 May 2010 09:30 On Mon, 2010-05-17 at 15:09 +0200, Vegard Nossum wrote: > On 17 May 2010 14:13, Andi Kleen <andi(a)firstfloor.org> wrote: > > Vegard Nossum <vegard.nossum(a)gmail.com> writes: > > > >> I just wanted to say that I've been accepted into this year's Google > >> Summer of Code program and will spend this summer working on improving > >> the kconfig system in a very particular direction: I want to integrate > >> a proper boolean constraint satisfiability solver into the > >> configuration editors (menuconfig, etc.) in order to allow > >> partial/incomplete configuration specifications. In short, this means > >> that the user can choose to not specify a particular value for some > >> config options, but let the system deduce their values. This will > >> hopefully improve usability and also solve the select problem once and > >> for all. > > > > Nice idea. I read your proposal and it looks good. > > > > I assume you got inspired by the libzypp use of a SAT solver > > for package dependencies? One problem that is visible there > > is that it can be hard to display conflicts in a nice and understandable > > way to the user, especially if there are lots of dependencies. > > > > It might be worth planning in some time to solve that nicely. > > Thanks! I didn't actually get inspired by libzypp -- but somebody else > mentioned it too, so I guess I should take a look! > > You bring up a valid point, and I admittedly haven't given it VERY > much thought yet, but I think that conflicts could be displayed in the > following way: If an instance is unsolvable, then it means that all > possible valuations/assignments make at least one clause (disjunction) > false. Each clause is usually generated by exactly one dependency > specification (the "depends on" directive), so we could print these > dependencies to the screen as suggestions for how to resolve the > conflict. Actually, the problem is a bit different from the zypper one: Since each package supplies its own dependencies and obsoletes, it is possible to get an unsolvable installation problem. What zypper tries to do in these situations is recommend possible courses of action (like remove these five packages from your current system, or downgrade this one etc.). For the Kconfig system, an unsolvable configuration is actually a bug in the Kconfig files. You can proceed on the premise that it's a single symbol that has the wrong depends or selects and isolate it from there. Done right, the Kconfig SAT solver shouldn't detect this problem only when a triggering configuration is input, but all the time, so it becomes impossible to introduce buggy Kconfig directives into the kernel tree. James -- To unsubscribe from this list: send the line "unsubscribe linux-kernel" in the body of a message to majordomo(a)vger.kernel.org More majordomo info at http://vger.kernel.org/majordomo-info.html Please read the FAQ at http://www.tux.org/lkml/
From: Andi Kleen on 17 May 2010 10:20 > You bring up a valid point, and I admittedly haven't given it VERY > much thought yet, but I think that conflicts could be displayed in the > following way: If an instance is unsolvable, then it means that all > possible valuations/assignments make at least one clause (disjunction) > false. Each clause is usually generated by exactly one dependency > specification (the "depends on" directive), so we could print these > dependencies to the screen as suggestions for how to resolve the > conflict. The problem is that might be a lot of entries, e.g. for "depends on PCI" You then end up displaying pages and pages of information, which is very hard to make sense of. You can see that by playing around with libzypp dependencies. -Andi -- ak(a)linux.intel.com -- Speaking for myself only. -- To unsubscribe from this list: send the line "unsubscribe linux-kernel" in the body of a message to majordomo(a)vger.kernel.org More majordomo info at http://vger.kernel.org/majordomo-info.html Please read the FAQ at http://www.tux.org/lkml/
From: James Bottomley on 17 May 2010 10:30
On Mon, 2010-05-17 at 16:21 +0200, Vegard Nossum wrote: > On 17 May 2010 15:21, James Bottomley > <James.Bottomley(a)hansenpartnership.com> wrote: > >> > I assume you got inspired by the libzypp use of a SAT solver > >> > for package dependencies? One problem that is visible there > >> > is that it can be hard to display conflicts in a nice and understandable > >> > way to the user, especially if there are lots of dependencies. > >> > > >> > It might be worth planning in some time to solve that nicely. > >> > >> Thanks! I didn't actually get inspired by libzypp -- but somebody else > >> mentioned it too, so I guess I should take a look! > >> > >> You bring up a valid point, and I admittedly haven't given it VERY > >> much thought yet, but I think that conflicts could be displayed in the > >> following way: If an instance is unsolvable, then it means that all > >> possible valuations/assignments make at least one clause (disjunction) > >> false. Each clause is usually generated by exactly one dependency > >> specification (the "depends on" directive), so we could print these > >> dependencies to the screen as suggestions for how to resolve the > >> conflict. > > > > Actually, the problem is a bit different from the zypper one: Since each > > package supplies its own dependencies and obsoletes, it is possible to > > get an unsolvable installation problem. What zypper tries to do in > > these situations is recommend possible courses of action (like remove > > these five packages from your current system, or downgrade this one > > etc.). For the Kconfig system, an unsolvable configuration is actually > > a bug in the Kconfig files. You can proceed on the premise that it's a > > single symbol that has the wrong depends or selects and isolate it from > > there. Done right, the Kconfig SAT solver shouldn't detect this problem > > only when a triggering configuration is input, but all the time, so it > > becomes impossible to introduce buggy Kconfig directives into the kernel > > tree. > > Even if the problem is different from zypper's, it is also here > possible to get an unsatisfiable instance. You are right that, yes, > the kconfig files on their own should always be satisfiable. But > that's before the user has made any choices at all. An example of an > unsatisfiable instance would be one where the user demands that 1. > some USB driver is enabled, while 2. USB support in general is > disabled. Actually, these are two separate problems. The first is basic consistency within the Kconfig subsytstem (something that select currently damages for us). The second is what to present to the user, which is where the inception of the select problem came from. A user doesn't really want to know that USB device X depends on usb storage, SCSI and a raft of other things ... they just want it to configure a kernel that supports their device. In particular, we don't want to present every possible option to users and then try to work out a solution, we really need guided configuration (which, in some measure, is what we have today: if you don't select general USB, you won't see any USB drivers. Or more importantly, if you select an Adaptec SCSI card, we just enable whichever transport library it needs). > But yes, once the basic infrastructure is in place, checking the > consistency of the kconfig files alone (not taking user's config into > account) should be trivial. Right, this will solve our current kernel developer issue ... I'm betting the guiding users one will be slightly harder. James -- To unsubscribe from this list: send the line "unsubscribe linux-kernel" in the body of a message to majordomo(a)vger.kernel.org More majordomo info at http://vger.kernel.org/majordomo-info.html Please read the FAQ at http://www.tux.org/lkml/ |