linux-kernel - Re: [ANNOUNCE] GSoC project: Improving kconfig using a SAT solver

lists.openwall.net		lists / announce owl-users owl-dev john-users john-dev passwdqc-users yescrypt popa3d-users / oss-security kernel-hardening musl sabotage tlsify passwords / crypt-dev xvendor / Bugtraq Full-Disclosure linux-kernel linux-netdev linux-ext4 linux-hardening linux-cve-announce PHC
Open Source and information security mailing list archives

Hash Suite: Windows password security audit tool. GUI, reports in PDF.

[<prev] [next>] [<thread-prev] [thread-next>] [day] [month] [year] [list]

Message-ID: <AANLkTil9lmdG5LY2SFk3cMsPOK-gUm2diMFL_o5bT08u@mail.gmail.com>
Date:	Mon, 17 May 2010 16:21:32 +0200
From:	Vegard Nossum <vegard.nossum@...il.com>
To:	James Bottomley <James.Bottomley@...senpartnership.com>
Cc:	Andi Kleen <andi@...stfloor.org>, linux-kernel@...r.kernel.org,
	linux-kbuild@...r.kernel.org, Bart Massey <bart@...pdx.edu>,
	Michal Marek <mmarek@...e.cz>,
	Greg Kroah-Hartman <greg@...ah.com>,
	Ingo Molnar <mingo@...e.hu>
Subject: Re: [ANNOUNCE] GSoC project: Improving kconfig using a SAT solver

On 17 May 2010 15:21, James Bottomley
<James.Bottomley@...senpartnership.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.

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.


Vegard
--
To unsubscribe from this list: send the line "unsubscribe linux-kernel" in
the body of a message to majordomo@...r.kernel.org
More majordomo info at  http://vger.kernel.org/majordomo-info.html
Please read the FAQ at  http://www.tux.org/lkml/