Linux Kconfig-SAT integration wiki and mailing list

[Luis R. Rodriguez]

We've been discussing for a while now documentation nitpicks over SAT
solving integration prospects with Kconfig, the kernel documentation
is not the place for that since this work is at this point theoretical
and we need ideas to be expressed and exchanged loosely. A dedicated
wiki and mailing list seems more appropriate. This is the mailing
list, and I've set up the wiki up on kernenewbies [0] just because it
was an easy place to set it up.

At this point we've managed to recruit enough mentors to help
developers that might be able to complete this task. This includes:

* Valentin Rothberg - one of the authors behind Undertaker, willing
to help with using PicoSAT, interfacing PicoSAT with with Kconfig
* Andrzej Wąsowski - Experience in modeling configuration problems
in SAT both in Kconfig and other universes
* Armin Biere - author of PicoSAT - SAT expert
* Máté Soós - author of CryptoMiniSat - SAT expert
* Luis R. Rodriguez - Kernel developer - willing to help with general advice
* Thorsten Berger - Willing to mentor, if a student is found
interested in this as part of a thesis topic at University of
Gothenburg

We have at least one developer interested, not yet committed, but at
least interested in this work:

* Chi Pham

Chi will be starting her masters soon and is seeing if this might be
one of the thing she might be able to take up as part of her course
work. If Chi is not available I can try to tackle this but until next
year's SUSE hackweek, and I'd hope to share a bit of work with
Valentin.

Chi, can you describe you recent finding you sent me in private
regarding previous GSoC work ?

[0] http://kernelnewbies.org/KernelProjects/kconfig-sat

Luis

[Chi Pham]

I'd be able to do actual work on this in February at the earliest, but can until then participate in preliminary discussions.
 

Chi, can you describe you recent finding you sent me in private
regarding previous GSoC work ?

Yep, it's a GSoC project from 2010 about "... integrat[ing] a proper boolean constraint satisfiability solver into the configuration editors (menuconfig, etc.) in order to allow partial/incomplete configuration specifications" and the goal was to "hopefully improve usability and also solve the select problem once and for all".

An announcement mail (the source of the above quotes) has been archived here: https://lkml.org/lkml/2010/5/17/164.

The code is publicly available here: https://github.com/vegard/linux-2.6.

It is a bit unclear what the current state of that project is, but it does sound like it has some overlap with this current project. The above linked fork hasn't been touched since October 2011 though.

 

[0] http://kernelnewbies.org/KernelProjects/kconfig-sat

- Chi

[Jesper Andersen]

On Thursday, October 8, 2015 at 2:49:56 AM UTC+2, Chi Pham wrote:

I'd be able to do actual work on this in February at the earliest, but can until then participate in preliminary discussions.
 

I am able to commit time to help on this work now. 

From the wiki it seems like one of the first tasks to consider is to find a way to convert Kconfig data to a format usable by (e.g.) PicoSAT? Is the documentation at https://www.kernel.org/doc/Documentation/kbuild/kconfig-language.txt sufficient for describing the Kconfig data?

Jesper

[Thorsten Berger]

In our experience it is not. In addition to this text file, we needed to study actual models and the behavior of xconfig in depth in order to come up with our formal semantics: http://gsd.uwaterloo.ca/sites/default/files/kconfig_semantics.pdf

Best, Thorsten

Jesper

--
Project details:
 
http://kernelnewbies.org/KernelProjects/kconfig-sat
---
You received this message because you are subscribed to the Google Groups "kconfig-sat" group.
To unsubscribe from this group and stop receiving emails from it, send an email to kconfig-sat...@googlegroups.com.
Visit this group at http://groups.google.com/group/kconfig-sat.
To view this discussion on the web visit https://groups.google.com/d/msgid/kconfig-sat/2ece26f1-9fcf-42ad-a837-58b50b715875%40googlegroups.com.
For more options, visit https://groups.google.com/d/optout.

-- 
Dr. Thorsten Berger
Assistant Professor
Department of Computer Science and Engineering
University of Gothenburg & Chalmers University of Technology
Hörselgången 5
41756 Göteborg, Sweden
http://gsd.uwaterloo.ca/tberger
Tel.: +46 (0) 31 772 6075
Mob.: +49 177 6225422
Skype: tberger.work

[Jesper Andersen]

On Thursday, October 8, 2015 at 2:57:14 PM UTC+2, Thorsten Berger wrote:

On 08/10/2015 9:03 AM, Jesper Andersen wrote:

On Thursday, October 8, 2015 at 2:49:56 AM UTC+2, Chi Pham wrote:

I'd be able to do actual work on this in February at the earliest, but can until then participate in preliminary discussions.
 

I am able to commit time to help on this work now. 

From the wiki it seems like one of the first tasks to consider is to find a way to convert Kconfig data to a format usable by (e.g.) PicoSAT? Is the documentation at https://www.kernel.org/doc/Documentation/kbuild/kconfig-language.txt sufficient for describing the Kconfig data?

In our experience it is not. In addition to this text file, we needed to study actual models and the behavior of xconfig in depth in order to come up with our formal semantics: http://gsd.uwaterloo.ca/sites/default/files/kconfig_semantics.pdf

Thanks for providing the link to you document. I have not read it yet, but will do so. Is it correct that the document ends with the section titled: "1-Var Propositional Semantics"?

Jesper

[Thorsten Berger]

Yes. We had worked on two different encodings (both implemented in our tool LVAT), one using two Boolean variables to represent tristate configs, and another one using just one variable (which is, thus, an abstraction). The last section in the document describes the latter.

But I should also point you to a more recent work by a PhD student from Hildesheim, who also analyzed the Kconfig semantics: http://sse.uni-hildesheim.de/media/fb4/informatik/AG_SSE/PDFs/publications/Kconfig/Report.pdf
Both documents should be a good start to consolidate the formal semantics for Kconfig.

As was discussed before, there are more tools in addition to our implementation (e.g., Undertaker from Erlangen) that can transform Kconfig models into propositional formulas, each probably using slightly different encodings and abstractions. However, the two documents above are the only that formally define/document the Kconfig semantics. It would actually be interesting to know whether our semantics (or those from Hildesheim) match the original intentions behind Kconfig.

HTH!
Best, Thorsten

Jesper

[Luis R. Rodriguez]

I should also note that I recently sent a patch to enhance the kbuild
documentation with a few corner case issues, this is actually what
lead me to jump looking at SAT solving prospects. The patch is now
merged but won't appear on linux-next for a few days, but you can
find the patch here:

http://lkml.kernel.org/r/1444259793-32486-1-g...@do-not-panic.com

> But I should also point you to a more recent work by a PhD student from
> Hildesheim, who also analyzed the Kconfig semantics:
> http://sse.uni-hildesheim.de/media/fb4/informatik/AG_SSE/PDFs/publications/Kconfig/Report.pdf
> Both documents should be a good start to consolidate the formal
> semantics for Kconfig.

Nice !

It may be a good time to also mention that an evolution in semantics on Kconfig
*could* implicate code as well. I'm not saying it needs to but we should be
open to it. We can't force old code to change, or at least that can't be a
requirement but if for whatever reason some clarifications on semantics within
Kconfig might mean some new code requirements I'd at least be open to consider
them. Part of this is that the definition alone of "clear semantics on code" is
also fuzzy these days, and we *should* be thinking about this as well. One
possibilty here *might* be to draw up relationships between kconfig symbols,
and kobjects (sysfs). This might be have to be a post-evaluation effort *after*
a SAT solver is integrated, not sure, but something to keep in mind to help
clear things up both on kconfig *and* code. If we go down this road I realize
there may be some code which does not have Kconfig symbols, but perhaps an
implicit relationship could be made for a series of code.

> As was discussed before, there are more tools in addition to our
> implementation (e.g., Undertaker from Erlangen) that can transform
> Kconfig models into propositional formulas, each probably using slightly
> different encodings and abstractions. However, the two documents above
> are the only that formally define/document the Kconfig semantics. It
> would actually be interesting to know whether our semantics (or those
> from Hildesheim) match the original intentions behind Kconfig.

Other than semantics two other design considerations for this work:

1) SAT modulariation

It seems PicoSAT might be the way to go as its written in C and there
is already quite a bit of work that uses that, both Undertaker and
the earlier GSoC attempt at Kconfig-SAT integration used PicoSAT.
PicoSAT is a good candidate for these reasons and that it would enable
compilation within kconfig, with the prospect of future kernel run time
integration use, if some use if found. Even while PicoSAT stands as
the leading candidate a SAT solver should still be stand-alone and
we should strive to modularize SAT integration then if possible so
that if another C-capable SAT solver stumbles along in the next few
years we can easily plug and play it, or at least enable folks to
easily try integration.

2) Built-in and tooling re-purposing

Having a SAT solver built as part of Kconfig is nice as it enables
the future prospect of that code to eventually be considered for
built-in functionality at kernel run time, should a use case arise.
While we can only speculate of such use, even though I'm already
aware of concrete use cases for it (but with lower latency
requirements) we should not disregard out-of-tree tooling uses
for SAT solvers and independent kernel tooling. So for instance
some SAT solvers might not be GPL compatible, likewise some tools
might also not be GPL compatible, or might be R&D material and as
such not intended or designed for upstream integration. We want
then the ability to extract boolean formulations so that third
party SAT solvers / tools can keep working and are enabled. So for
instance it would be nice if with this work, even though we'd have
PicoSAT integrated (hopefully modularized) we'd still enable
Undertaker to then exist outside of Linux, it'd just re-use the
now in-kernel features to dump out some formulations.

[0] https://github.com/vegard/linux-2.6.git

Luis

[Jesper Andersen]

On Thursday, October 8, 2015 at 9:36:28 PM UTC+2, Thorsten Berger wrote:

On 08/10/2015 9:21 PM, Jesper Andersen wrote:

On Thursday, October 8, 2015 at 2:57:14 PM UTC+2, Thorsten Berger wrote:

On 08/10/2015 9:03 AM, Jesper Andersen wrote:

On Thursday, October 8, 2015 at 2:49:56 AM UTC+2, Chi Pham wrote:

I'd be able to do actual work on this in February at the earliest, but can until then participate in preliminary discussions.
 

I am able to commit time to help on this work now. 

From the wiki it seems like one of the first tasks to consider is to find a way to convert Kconfig data to a format usable by (e.g.) PicoSAT? Is the documentation at https://www.kernel.org/doc/Documentation/kbuild/kconfig-language.txt sufficient for describing the Kconfig data?

In our experience it is not. In addition to this text file, we needed to study actual models and the behavior of xconfig in depth in order to come up with our formal semantics: http://gsd.uwaterloo.ca/sites/default/files/kconfig_semantics.pdf

Thanks for providing the link to you document. I have not read it yet, but will do so. Is it correct that the document ends with the section titled: "1-Var Propositional Semantics"?

Yes. We had worked on two different encodings (both implemented in our tool LVAT), one using two Boolean variables to represent tristate configs, and another one using just one variable (which is, thus, an abstraction). The last section in the document describes the latter.

But I should also point you to a more recent work by a PhD student from Hildesheim, who also analyzed the Kconfig semantics: http://sse.uni-hildesheim.de/media/fb4/informatik/AG_SSE/PDFs/publications/Kconfig/Report.pdf
Both documents should be a good start to consolidate the formal semantics for Kconfig.

It looks like there is quite a bit of reading to do here (I'm on vacation the next week or so and I might actually get to read a little then)!

 

As was discussed before, there are more tools in addition to our implementation (e.g., Undertaker from Erlangen) that can transform Kconfig models into propositional formulas, each probably using slightly different encodings and abstractions. However, the two documents above are the only that formally define/document the Kconfig semantics. It would actually be interesting to know whether our semantics (or those from Hildesheim) match the original intentions behind Kconfig.

I should point out that for now I have little insight in kconfig (although back when I started using gentoo, I spent a *lot* of time trying to get my kernel configuration correct) but some experience in SAT solvers and constraint satisfaction problems. I would have expected there to be a tool (menuconfig?) that would read a kconfig spec and allow the user to set values which should be taken as the basis for defining the semantics of kconfig?

Jesper

[Luis R. Rodriguez]

It may be then useful to highlight a previosu kconfig-sat attemtp which under
GSoC but that its work never was attempted to get upstream here, that Chi pointed
out:

https://github.com/vegard/linux-2.6

That used PicoSAT, and has code changes for integration, I have just given this
a cursory overview. It'd be interesting to learn why the student, Vegard
(cc'd), did not try to prupose the changes upstream in the end.

Expected challenges I've been hinted might exist is that SAT solvers might
be too slow to use for all kconfig evaluations, I do wonder if that hindered
the original motivation for using PicoSAT in kconfig through Vegard's work,
but note that Vegard's work dates back to 2011 and over time SAT sovlers have
gotten much better. Another thing to consider is that if at evaluation time
it is determined a SAT solver used on kconfig for all things is too slow we
could at least consider its use for only a few key things such as select
resolution lookup (a kconfig symbol using select doesn't check if dependencies
match today), for example, another example may be to just use it to help
give more verbose details upon error of causes of an error through the use
of MUS.

> > As was discussed before, there are more tools in addition to our
> > implementation (e.g., Undertaker from Erlangen) that can transform Kconfig
> > models into propositional formulas, each probably using slightly different
> > encodings and abstractions. However, the two documents above are the only
> > that formally define/document the Kconfig semantics. It would actually be
> > interesting to know whether our semantics (or those from Hildesheim) match
> > the original intentions behind Kconfig.
> >
>
> I should point out that for now I have little insight in kconfig (although
> back when I started using gentoo, I spent a *lot* of time trying to get my
> kernel configuration correct) but some experience in SAT solvers and
> constraint satisfaction problems. I would have expected there to be a tool
> (menuconfig?) that would read a kconfig spec and allow the user to set
> values which should be taken as the basis for defining the semantics of
> kconfig?

That's right only that menuconfig is the ncurse interface, and there are others
such as 'make xconfig' or just 'make config', underneath this kconfig parses
Kconfig symbols and enables interactions through whatever user interface is
preferred.

Other than Documentation/kbuild/kconfig-language.txt there is no clear
semantics other than the publications listed above.

My own recommendation for this work would be to nose dive into Vegard's
work, see why that wasn't upstreamed, see if it had limitations, and then
see if clearing / fixing semantics migth help with some of the known issues.
Known issues of semantics seem to be well documented on Hildesheim,'s work
under "2.3 Non-Critical Observations" and "2.4 Critical Observations".
For instance "2.3.1 Hierarchies inside String/Numerical Config Options"
notes how strings are allowed in "depends", and this could throw off
a SAT solver. In such cases we may want to do a sweep evaluation of
such uses in the kernel, see if it was a mistake and/or if we can use
an alternative mechanism that would use clearer semantics and then just
not allow this sort of mechanism. Similar hunt might need to be done
for the other observations, both on the paper and on the patch I posted
about recursive issues due to select. Using a SAT solver may also solve
some of the issues so keeping that in mind should help as well.

Expecting to fi all semantic issues is not required for a SAT solver
to be integrated, as we could stage this. If we knew we had some kconfig
semantics homework we could for instance only enable a SAT solver for
a few uses cases we were comfortable would not make a SAT solver barf
with, leave the option to enable it for others but annotate all the
homework we need to complete. This would for instance enable the ability to
optionally use the SAT solver provided some new well defined semantics are used
and let us grow its use as things get cleared up / fixed.

Luis

[Josh Triplett]

On Mon, Oct 12, 2015 at 07:44:38PM +0200, Luis R. Rodriguez wrote:
> Expected challenges I've been hinted might exist is that SAT solvers might
> be too slow to use for all kconfig evaluations, I do wonder if that hindered
> the original motivation for using PicoSAT in kconfig through Vegard's work,
> but note that Vegard's work dates back to 2011 and over time SAT sovlers have
> gotten much better. Another thing to consider is that if at evaluation time
> it is determined a SAT solver used on kconfig for all things is too slow we
> could at least consider its use for only a few key things such as select
> resolution lookup (a kconfig symbol using select doesn't check if dependencies
> match today), for example, another example may be to just use it to help
> give more verbose details upon error of causes of an error through the use
> of MUS.

I would find it quite surprising if a SAT solver found the Kconfig
prolem space challenging to solve quickly; while it contains a huge
*number* of symbols, the interactions between them seem fairly
straightforward in the majority of cases, and only a small number of
symbols get involved in complex logic.

My concern about applying a SAT solver comes from solution (or
especially non-solution) comprehensibility and explainability: how well
can we translate the output of a SAT solver into a clear, meaningful
explanation? We can't just say "no such kernel configuration exists";
ideally, we want the simplest possible explanation of why your desired
set of config symbols can't work, or the solution closest to what the
user asked for if one exists, for some sensible values of "simplest" and
"closest".

- Josh Triplett

[Luis R. Rodriguez]

On Mon, Oct 12, 2015 at 10:56:01AM -0700, Josh Triplett wrote:
> On Mon, Oct 12, 2015 at 07:44:38PM +0200, Luis R. Rodriguez wrote:
> > Expected challenges I've been hinted might exist is that SAT solvers might
> > be too slow to use for all kconfig evaluations, I do wonder if that hindered
> > the original motivation for using PicoSAT in kconfig through Vegard's work,
> > but note that Vegard's work dates back to 2011 and over time SAT sovlers have
> > gotten much better. Another thing to consider is that if at evaluation time
> > it is determined a SAT solver used on kconfig for all things is too slow we
> > could at least consider its use for only a few key things such as select
> > resolution lookup (a kconfig symbol using select doesn't check if dependencies
> > match today), for example, another example may be to just use it to help
> > give more verbose details upon error of causes of an error through the use
> > of MUS.
>
> I would find it quite surprising if a SAT solver found the Kconfig
> prolem space challenging to solve quickly; while it contains a huge
> *number* of symbols, the interactions between them seem fairly
> straightforward in the majority of cases, and only a small number of
> symbols get involved in complex logic.

In that case then even less work should be expected on the corner cases.
That's good but we should remain attentitive towards such possible issues.

> My concern about applying a SAT solver comes from solution (or
> especially non-solution) comprehensibility and explainability: how well
> can we translate the output of a SAT solver into a clear, meaningful
> explanation? We can't just say "no such kernel configuration exists";
> ideally, we want the simplest possible explanation of why your desired
> set of config symbols can't work, or the solution closest to what the
> user asked for if one exists, for some sensible values of "simplest" and
> "closest".

Valentin has hinted Minimally Unsatisfiable Subformula (MUS) support could help
with this, it would show the minimum set of unsatisfiable configuration
options.

Luis

[Vegard Nossum]

On 12 October 2015 at 19:44, Luis R. Rodriguez <mcg...@suse.com> wrote:

That used PicoSAT, and has code changes for integration, I have just given this
a cursory overview. It'd be interesting to learn why the student, Vegard
(cc'd), did not try to prupose the changes upstream in the end.

Expected challenges I've been hinted might exist is that SAT solvers might
be too slow to use for all kconfig evaluations, I do wonder if that hindered
the original motivation for using PicoSAT in kconfig through Vegard's work,
but note that Vegard's work dates back to 2011 and over time SAT sovlers have
gotten much better. Another thing to consider is that if at evaluation time
it is determined a SAT solver used on kconfig for all things is too slow we
could at least consider its use for only a few key things such as select
resolution lookup (a kconfig symbol using select doesn't check if dependencies
match today), for example, another example may be to just use it to help
give more verbose details upon error of causes of an error through the use
of MUS.

Here's a reply I gave John Stultz back in 2011, quoted in full:

"""
On 28 June 2011 21:45, John Stultz <john....@linaro.org> wrote:
> Your SAT work is interesting, as it could help with the dependency
> resolution of terse kconfig fragments. While I've not looked closely at
> it yet, I'm just curious to hear what happened with it? Are you still
> workign on it? Were there any problematic roadblocks that got in your
> way?

Hey :-)

kconfig-sat is in a half-finished state. It sorta/kinda/nearly works.
For example, it doesn't really handle config options of string and int
types and will use the default values unless you specify your own
values. It also doesn't correspond 100% with the rules of the current
kconfig, so kconfig may modify the config slightly when it is written
out, and the best way to get around this is to run satconfig twice.

Please also check out the documentation, it should say more or less
what else is missing and/or how to fix it:

https://raw.github.com/vegard/linux-2.6-kconfig-sat/kconfig-sat/Documentation/kbuild/kconfig-sat.txt

I guess there was no single roadblock. I mostly ran out of time during
the GSoC and never really found the time to finish it afterwards. That
said, I did have a lot of problems with finding the right
encoding/formalisation of the kconfig language. It's simply not very
well documented (the code is the only standard) and there are a lot of
weird corner cases with hidden prompts, choice values, prompt
dependencies, symbol dependencies, default values, conditional default
values, you name it...

I still *do* have a hope of finishing it, maybe even this year, since
my university coursework is finally done.

One of the main ideas of satconfig was indeed to be able to do
consistent policy decisions and to get away from the defconfig hell
where every arch has its own, completely specified defconfig, and move
the "main default features" into a common file and put ONLY the
architecture-specifics into architecture-specific files. (satconfig
would of course be able to fill out the rest, so not every option
would have to be specified precisely.)

If you are interested in working on satconfig, I can help you. If/when
I start working on it myself, the changes will show up on github. Let
me know if you have any questions/problems/etc.!
"""

So, in short, while it does work and produce valid full-configs given a partial .satconfig file (it's actually pretty fun to play with), it doesn't always give configs which have everything set according to the solution that the SAT solver found. I guess this was the main reason I didn't try to upstream it, i.e. it wasn't production ready and I was not going to have the time to maintain it.

I can confirm that the time spent doing actual solving is minimal, the resulting SAT problem is not difficult for a SAT solver _at all_. there was even a potential to do solving on the fly inside menuconfig or similar (with a new run every time the user made a change). IIRC most of the time spent in 'make satconfig' comes from reading Kconfig files and generating the CNF.

I'm sort of short on time these days so I can't make any large commitments (though of course I'd love to see satconfig find a home in the upstream kernel). I'd be happy to answer anything like "what exactly are you doing on line 347 of satconf.c", though.

BTW, I seem to have done a bit of work on satconfig in 2013, check out this slightly more recent branch than the GSoC 2011 work:
https://github.com/vegard/linux-2.6/tree/v3.6+kconfig-sat

If I were to do this again I would probably write it in C++ instead because this kind of C code is frankly horrible:

t3 = bool_var(choice2->sat_variable);
t4 = bool_not_put(t3);

t5 = bool_or(t2, t4);
bool_put(t4);

add_clauses(t5, "%s and %s are mutual exclusive",
       choice->name ?: "<choice>",
       choice2->name ?: "<choice>");
bool_put(t5);

This conceptually does:

sat_assert(!var(choice) || !var(choice2), "%s and %s are mutually exclusive", ...);

(Though, now, looking at it, I'm glad I added those descriptions, they should be useful for understanding the semantics I used.)

I haven't really looked at this kconfig-sat google project much, is there a reference list of things I can read (in order) to get up to scratch on the new project?

I'd be happy to help GSoC and/or university students (I completed my master thesis, also related to SAT solving, in 2012), not sure if I can dedicate enough time to be a full mentor but feel free to send me any kind of questions/proposals!

Vegard

[Vegard Nossum]

On 12 October 2015 at 19:56, Josh Triplett <jo...@joshtriplett.org> wrote:

I would find it quite surprising if a SAT solver found the Kconfig
prolem space challenging to solve quickly; while it contains a huge
*number* of symbols, the interactions between them seem fairly
straightforward in the majority of cases, and only a small number of
symbols get involved in complex logic.

Right, as I just wrote in this same thread, actual time spent in the SAT solver is very small in my experience.

 

My concern about applying a SAT solver comes from solution (or
especially non-solution) comprehensibility and explainability: how well
can we translate the output of a SAT solver into a clear, meaningful
explanation?  We can't just say "no such kernel configuration exists";
ideally, we want the simplest possible explanation of why your desired
set of config symbols can't work, or the solution closest to what the
user asked for if one exists, for some sensible values of "simplest" and
"closest".

In my 2011 work I included a "reason" for every clause that was generated. This combined with the MUS feature of PicoSAT lets me output a reason why a given .satconfig file has no solutions, e.g. for this:

$ cat .satconfig
CONFIG_DEFAULT_SECURITY_SELINUX=y
CONFIG_DEFAULT_SECURITY_SMACK=y

it gives:

$ make satconfig
[...]
39665 variables (30017 symbols, 7387 prompts, 2261 defaults)
336416 clauses
error: unsatisfiable constraints
clause: DEFAULT_SECURITY_SMACK and DEFAULT_SECURITY_SELINUX are mutual exclusive
clause: DEFAULT_SECURITY_SMACK and DEFAULT_SECURITY_SELINUX are mutual exclusive
make[1]: *** [satconfig] Error 1
make: *** [satconfig] Error 2

Or this (admittedly slightly harder to read):

$ cat .satconfig
CONFIG_TIGON3=y
CONFIG_PCI=n

$ make satconfig
scripts/kconfig/satconf Kconfig
39665 variables (30017 symbols, 7387 prompts, 2261 defaults)
336416 clauses
error: unsatisfiable constraints
clause: "Broadcom Tigon3 support" prompt depends on NETDEVICES [=n] && ETHERNET [=n] && NET_VENDOR_BROADCOM [=n] && PCI [=n]
clause: "Broadcom Tigon3 support" prompt depends on NETDEVICES [=n] && ETHERNET [=n] && NET_VENDOR_BROADCOM [=n] && PCI [=n]
clause: "Broadcom Tigon3 support" prompt depends on NETDEVICES [=n] && ETHERNET [=n] && NET_VENDOR_BROADCOM [=n] && PCI [=n]
clause: TIGON3 has at least one prompt if entered by the user
clause: TIGON3 has at least one prompt if entered by the user
make[1]: *** [satconfig] Error 1
make: *** [satconfig] Error 2

The reason "TIGON3 has at least one prompt if entered by the user" is essentially saying that if the user was able to request CONFIG_TIGON3=y in the .satconfig file, then the (a) prompt for that symbol must exist. And that prompt depends on NETDEVICES && ETHERNET && NET_VENDOR_BROADCOM && PCI, which was false. (Ignore the "[=n]" which are just artifacts of how expressions are printed.)

There's some low-hanging fruit here to make this more readable/user friendly, for example by splitting up the conjunction "NETDEVICES && ..." so that you can definitely see that it was the CONFIG_PCI dependency that failed and also only output each reason once (here it is output once for each clause that is part of the MUS).

Vegard

[Josh Triplett]

On Mon, Oct 12, 2015 at 09:36:02PM +0200, Vegard Nossum wrote:
> On 12 October 2015 at 19:56, Josh Triplett <jo...@joshtriplett.org> wrote:
> > I would find it quite surprising if a SAT solver found the Kconfig
> > prolem space challenging to solve quickly; while it contains a huge
> > *number* of symbols, the interactions between them seem fairly
> > straightforward in the majority of cases, and only a small number of
> > symbols get involved in complex logic.
>
> Right, as I just wrote in this same thread, actual time spent in the SAT
> solver is very small in my experience.

Excellent.

That looks quite reasonable.

> There's some low-hanging fruit here to make this more readable/user
> friendly, for example by splitting up the conjunction "NETDEVICES && ..."
> so that you can definitely see that it was the CONFIG_PCI dependency that
> failed and also only output each reason once (here it is output once for
> each clause that is part of the MUS).

Agreed; reducing the conjunction to just the failing term would help, as
would clarifying "has at least one prompt" and similar.

- Josh Triplett

[Thorsten Berger]

Hi everyone,

I just received an email from a student interested in this topic for a Master's thesis. I'm currently trying to figure out a bit more about his background (e.g., whether he can do C programming, as this seems to be a core requirement, right?).

Now, I lost a bit of overview here. Is there already someone else actively implementing a solution, or could the student pretty much start implementing (possibly on top of existing work, such as kconfig-sat)? If there's already a developer, could there a be a specific reasoning task (e.g., improving choice propagation, controlling visibility of subtrees, etc.) the student could be working on?

In case the student would not be efficient in implementing, I could also imagine some more empirical study about the use of configuration symbols in the code, or the impact of any migration efforts (there was a discussion about that by Luis a while ago) in case the Kconfig semantics would be changed.

Best, Thorsten

-- 
Dr. Thorsten Berger
Assistant Professor
Department of Computer Science and Engineering
University of Gothenburg & Chalmers University of Technology
Hörselgången 5
41756 Göteborg, Sweden

http://www.thorsten-berger.net

[jespera]

Hi,

I was planning on working on this out of interest in sat-solvers and
improving the experience of configuring a kernel, but if you have a
student who would want to do this for his Master's thesis, I think
that would be more appropriate than me doing it because he'd most
likely have more time than me right now. I'd still love to help in any
way I can though.

So far I've only been reading the material linked in this thread but
not implemented so far.

Regards,
Jesper A

[Thorsten Berger]

Hi Jesper,

Thanks for the quick follow-up! Even if we have a student, it would be
great if you could be involved with coding, discussing the realization,
working in transformations, quality-assuring the work, etc.

Let me meet with the student next week to see whether he'd be the right
candidate, and then get back to you and others here on the mailing list.

Best, Thorsten

[Chi Pham]

On Fri, Oct 16, 2015 at 3:39 PM, Thorsten Berger <thorste...@chalmers.se> wrote:

Hi everyone,

I just received an email from a student interested in this topic for a Master's thesis. I'm currently trying to figure out a bit more about his background (e.g., whether he can do C programming, as this seems to be a core requirement, right?).

Now, I lost a bit of overview here. Is there already someone else actively implementing a solution, or could the student pretty much start implementing (possibly on top of existing work, such as kconfig-sat)? If there's already a developer, could there a be a specific reasoning task (e.g., improving choice propagation, controlling visibility of subtrees, etc.) the student could be working on?

In case the student would not be efficient in implementing, I could also imagine some more empirical study about the use of configuration symbols in the code, or the impact of any migration efforts (there was a discussion about that by Luis a while ago) in case the Kconfig semantics would be changed.

Hi,

I joined this project in the hopes of being able to contribute some code as well.
As I will not be able to work on this before February, and Jesper has offered to work on it immediately, I'll just be following the progress from the sideline.

Thanks,

- Chi

[Jesper Andersen]

Hi Thorsten,

Did you find time to talk to the student you mentioned?

Jesper

[Thorsten Berger]

Hi,

Sorry for the very late follow-up, and apologies for writing a long email. I've talked to the student and we're currently evaluating all the options. I'm also coordinating with a group of students from Waterloo (my previous university) that is aiming at re-implementing the range-fix algorithm from Yingfei [1] in C. I now have a couple of questions.

Luis, what is the usual way you define requirements in the community? Is there some Wiki we could use? I think we'd like to realize an interactive, GUI-supported solution that helps people during the actual configuration of the kernel. Vegard has realized a non-interactive solution, which completes a partial configuration (outputting contradicting clauses if that's not possible). I think both use cases are beneficial for the kernel community, but I was wondering whether we could flesh them out a bit more. In the current Wiki, there are some more use cases, which go a bit more in the direction of verifying dependency structures by the developers (i.e., avoid circular dependencies, whereas I'm not sure whether they're really a problem when using a proper reasoner). So if we could have such a platform where we could define use cases and requirements, let us know. Otherwise we could also use bitbucket or so.

Once we have that defined, it should be easier to distribute work, also with all on this list (esp. Jesper) interested in helping.

Vegard, we had looked at your github project, and found your documentation [2]. My early assessment is that this project could be a good basis for the implementation, I'll discuss this with the students. You mentioned that you're sort of thinking that re-implementing parts of it in C++ would be better. What is your current opinion? Would C++ also work if we wanted to realized an interactive solution within xconfig?

Furthermore, Vegard, you mentioned that there were too many corner cases in Kconfig (which I can confirm) that made it hard to have a final version of your tool. I was wondering whether we could somehow discuss and classify these cases, potentially using the Hildesheim TR [3]. This could trigger some discussion with the kconfig developers about the future evolution of the language.

Finally, let me get back to the range-fix algorithm from Yingfei [1]. So there's a group of fourth-year SE students who'll re-implement the algorithm in C. This algorithm supports an interactive resolution of configuration conflicts: If you cannot enable an option, it tells you different fixes (sets of options you have to change and how). It's called range-fix, because it supports arithmetic constraints, for which it uses an SMT solver instead of a SAT solver. It was mainly developed for eCos with its CDL language [4], which uses a lot of such constraints. The Linux model has none or very few of those (there're int ranges, but no constraints over these ranges afair), so it might be possible to just use a SAT solver instead of an SMT solver. However, the encoding of non-Boolean options, such as tristate, is way more straightforward in SMT, so it might be easier to use SMT. Now, the question is also whether an SMT solver would be an option at all for the Linux community. Yingfei used the SMTlib format, which abstracts over actual SMT solver implementations. So if there would be an SMT solver compatible with GPL, would this be an alternative or should I tell the students that they definitely need to use SAT?

On a final note, beyond the configurator support, I also see potential for work in the area of verifying constraints with the source code (e.g., removing unnecessary constraints if we find such), detecting dead code (for which Undertaker could be used) or optimizing the modularization of the whole kconfig model ("defconfig hell", which seems to arise from duplication of common options for the different architectures as far as I understand).

Hope this assessment helps, and sorry again for the long email.
Best, Thorsten


[1] http://sei.pku.edu.cn/~xiongyf04/papers/TSE14.pdf
[2] https://github.com/vegard/linux-2.6/blob/kconfig-sat/Documentation/kbuild/kconfig-sat.txt
[3] http://sse.uni-hildesheim.de/media/fb4/informatik/AG_SSE/PDFs/publications/Kconfig/Report.pdf
[4] http://gsd.uwaterloo.ca/sites/default/files/vm-2013-berger.pdf

[Armin Biere]

If the ranges of options used in the kernel are only made up of few
numbers, say the expected range of these integers is below 100
or way lower, and there are no complicated constraints (like using
additions or more complicated stuff), then SMT is overkill. Also
SW engineering wise SMT solvers are way bigger and have more
dependencies. In SAT there is a nice generic interface now,
the IPASIR interface used in this year's competition. It is modelled
after a subset of PicoSAT's API (well I was involved). Targeting
that API (semantic wise) will easily allow us to use different SAT
solvers.

Even if there are more complicated constraints, it might be easier
to add some glue logic to handle those constraints (like bit-blasting).
Only if solving time could be speed up by using more advanced
techniques available in SMT solvers (like special theories IDL/LA)
it would make sense to me to go through SMT.

Armin

> --
> Project details:
>
> http://kernelnewbies.org/KernelProjects/kconfig-sat
> ---
> You received this message because you are subscribed to the Google Groups
> "kconfig-sat" group.
> To unsubscribe from this group and stop receiving emails from it, send an
> email to kconfig-sat...@googlegroups.com.
> Visit this group at http://groups.google.com/group/kconfig-sat.
> To view this discussion on the web visit

> https://groups.google.com/d/msgid/kconfig-sat/563C8CFC.9030707%40chalmers.se.

[Josh Triplett]

On Fri, Nov 06, 2015 at 12:20:28PM +0100, Thorsten Berger wrote:
> Luis, what is the usual way you define requirements in the community? Is
> there some Wiki we could use?

Usually, such requirements get handled through discussion, either on
mailing lists or in-person. That said, a wiki seems helpful for
collaboration; the kernel.org admins could help you create a
"sat.wiki.kernel.org" if you like.

> I think we'd like to realize an
> interactive, GUI-supported solution that helps people during the actual
> configuration of the kernel.

I would suggest that if you want to ease adoption of this and acceptance
of patches, you'll likely have a much easier time if you can do so as an
extension of the existing kconfig UIs such as menuconfig, rather than
creating a new UI. For instance, you could extend Kconfig to help with
things like "If I wanted to turn this option, what would I need to
enable as dependencies?" or "If I wanted to turn this option off, what
would I need to change?". (In addition to improving kconfig's
dependency resolver to better handle selects and dependencies.)

Longer-term, you could then look to unify things like "select" and
"depends", since they mean approximately the same thing, just with
different resolution models: "select" exists for cases where turning an
option on should automatically enable another, while "depends" doesn't
allow turning on the option unless the other has been enabled. (Though
note that in some cases "depends" also exists to hide away a family of
options behind one, especially for the textual "make config".)

- Josh Triplett

[Thorsten Berger]

Hi,

>
>> I think we'd like to realize an
>> interactive, GUI-supported solution that helps people during the actual
>> configuration of the kernel.
> I would suggest that if you want to ease adoption of this and acceptance
> of patches, you'll likely have a much easier time if you can do so as an
> extension of the existing kconfig UIs such as menuconfig, rather than
> creating a new UI. For instance, you could extend Kconfig to help with
> things like "If I wanted to turn this option, what would I need to
> enable as dependencies?" or "If I wanted to turn this option off, what
> would I need to change?". (In addition to improving kconfig's
> dependency resolver to better handle selects and dependencies.)

Thanks, Josh. That's what the group of students in Waterloo is currently
trying to do. They have to hand-in their project in a week, and the goal
is to have such an extension for xconfig. This will be an early
prototype to show how an integration could look like. They probably
won't have time to re-implement the fix generation in C/C++, and will
likely call the existing scala code for now. But this can be the basis
for re-implementation either in SAT or SMT (thanks, Armin for commenting
on this) by those interested, such as my Master student here.

> Longer-term, you could then look to unify things like "select" and
> "depends", since they mean approximately the same thing, just with
> different resolution models: "select" exists for cases where turning an
> option on should automatically enable another, while "depends" doesn't
> allow turning on the option unless the other has been enabled. (Though
> note that in some cases "depends" also exists to hide away a family of
> options behind one, especially for the textual "make config".)

That is actually an interesting question. Based on our studies of
configurators, it seems that one wants to distinguish between visibility
constraints (depends on) and other configuration constraints (select).
The former cannot temporarily be violated (i.e., are immediately
enforced -- when sub-trees are greyed out or are not visible at all in
make config), while the latter can be (then you have a list of conflicts
shown in the configurator, which you can ask the reasoner to resolve).
The latter case allows you to make a lot of changes, without caring
about the constraints, and have them sorted out later. This seems to
boil down to usability and efficiency when working with the
configurator. Only allowing valid changes might slow you down, but I'm
curious about opinions here. Finally, this distinction between these two
different kinds of constraints also appears in other configurators, such
as in the one from eCos (open source) or in pure::variants (commercial).

Best, Thorsten


>
> - Josh Triplett

[Mate Soos]

Hi All,

Let me chirp in here a bit.

On 06/11/15 13:38, Armin Biere wrote:
> If the ranges of options used in the kernel are only made up of few
> numbers, say the expected range of these integers is below 100
> or way lower, and there are no complicated constraints (like using
> additions or more complicated stuff), then SMT is overkill. Also
> SW engineering wise SMT solvers are way bigger and have more
> dependencies. In SAT there is a nice generic interface now,
> the IPASIR interface used in this year's competition. It is modelled
> after a subset of PicoSAT's API (well I was involved). Targeting
> that API (semantic wise) will easily allow us to use different SAT
> solvers.

I agree on all these points. IPASIR would be great, it would allow for
any SAT solver to be plugged in. SMT solvers are heavy beasts. If
complicated theories are needed they are painful necessities but
otherwise just a burden.

Cheers,

Mate

[Andrzej Wasowski]

I completely agree. If an SMT solver can be avoided the result will be way more maintainable, and it will be more robust to changes of the solver (less licenses issues, etc). I think this is worse even if it requires introducing a bit of abstraction, and the tool not providing a "complete" advice in some cases (as long as these cases are rare).

Andrzej

--
associate prof. Andrzej Wąsowski, http://www.itu.dk/~wasowski
IT University, Rued Langgaards Vej 7, 2300 Copenhagen, Denmark
room 4D10 phone +45 7218 5086 fax *5001 skype wasowski_andrzej

________________________________________
From: kconf...@googlegroups.com <kconf...@googlegroups.com> on behalf of Mate Soos <soos...@gmail.com>
Sent: Wednesday, November 11, 2015 23:30
To: kconf...@googlegroups.com
Subject: Re: [kconfig-sat] Linux Kconfig-SAT integration wiki and mailing list

--
Project details:

http://kernelnewbies.org/KernelProjects/kconfig-sat
---
You received this message because you are subscribed to the Google Groups "kconfig-sat" group.
To unsubscribe from this group and stop receiving emails from it, send an email to kconfig-sat...@googlegroups.com.
Visit this group at http://groups.google.com/group/kconfig-sat.

To view this discussion on the web visit https://groups.google.com/d/msgid/kconfig-sat/5643C17B.3060102%40gmail.com.

[xiong....@gmail.com]

Hi all,

Thorsten asked me to comment on this discussion thread. Regarding the discussion, there are mainly two points I would like to address:

First, we can always encoding everything in SAT. In fact, this is one basic way to implement SMT solvers, called "the early approach". So the question is not whether we can use SAT solvers, is whether the benefits offset the cost.

Second, it is not clear to me what benefits we get if we use SAT. Andrzej mentioned license issue, but there are a large number of SMT solvers available today, and we can choose one meet the license requirement. On the other hand, the cost is obvious: we need more time to develop the SAT encoding, and the maintenance is more difficult.

Regards,

Yingfei

[Thorsten Berger]

Hi,

Let me add that Yingfei is the one who has implemented and evaluated the interactive RangeFix algorithm, which generates fixes for configuration conflicts. I asked him to join the discussion, because he can give some concrete figures from the evaluation. This is not meant as a SAT vs. SMT thread, but let's try to understand the practical implications better.

Yingfei, it would be good if you could briefly outline the encoding of tristate configs and of the logical operators on them, and also give us some experiences from the performance (time to generate fixes) and the scalability evaluation of your algorithm.

Best, Thorsten

To view this discussion on the web visit https://groups.google.com/d/msgid/kconfig-sat/3d216b07-1b0a-46be-80a0-bbf2942d25ab%40googlegroups.com.

For more options, visit https://groups.google.com/d/optout.

[Yingfei Xiong]

Hi Thorsten and all,

Thank Thorsten for introducing me. Previously I saw a few familiar names and thought that this was a discussion within a few research groups.

The experiments were done several years ago and I could not remember all the details. Regarding encoding tristate, we tried several ways to encode tristate options, for example, as integers or enumerations. I do not remember the exact methods we tried and the exact result, but somehow in the final experiments we decided to use the enumeration encoding. There was nothing difficult in encoding operators, as they can be directly translated into SMT.

There is also a trivial issue about how to encode Booleans when they are mixed used with tristate. Details about this can be found in Sect 6.2 our TSE paper: http://sei.pku.edu.cn/~xiongyf04/papers/TSE14.pdf

Regards,

Yingfei

Xiong, Yingfei / 熊英飞 / 熊英飛

Assistant Professor ("Young Talents" Plan)
Software Engineering Institute
School of Electronics Engineering and Computer Science
Peking University
China

Web: http://sei.pku.edu.cn/~xiongyf04

-- 
Dr. Thorsten Berger
Assistant Professor
Department of Computer Science and Engineering
University of Gothenburg & Chalmers University of Technology
Göteborg, Swedenhttp://www.thorsten-berger.netTel.: +46 (0) 31 772 6075

Mob.: +49 177 6225422
Skype: tberger.work

 

--

Project details:
 
http://kernelnewbies.org/KernelProjects/kconfig-sat
---

You received this message because you are subscribed to a topic in the Google Groups "kconfig-sat" group.
To unsubscribe from this topic, visit https://groups.google.com/d/topic/kconfig-sat/G6HA_3ecAQI/unsubscribe.
To unsubscribe from this group and all its topics, send an email to kconfig-sat...@googlegroups.com.

Visit this group at http://groups.google.com/group/kconfig-sat.

To view this discussion on the web visit https://groups.google.com/d/msgid/kconfig-sat/564EE090.7070809%40chalmers.se.

[Armin Biere]

Once again for the list ...

---------- Forwarded message ----------
From: Armin Biere <armin...@gmail.com>
Date: Fri, Nov 20, 2015 at 11:58 AM
Subject: Re: Re: [kconfig-sat] Linux Kconfig-SAT integration wiki and
mailing list

To: Yingfei Xiong <xio...@pku.edu.cn>


Well, I think the SAT encoding for the tristate option is as least as simple.

Use three variables (instead of one):

opt_is_n, opt_is_m, opt_is_y

and add an exactly one constraint over them. Having glue logic for
adding these trivial cardinality constraints is easy to write (and probably
much more efficient than what the SMT solver would). In this particular
case you write not two are true at the same time

(-opt_is_n, -opt_is_m)
(-opt_is_n, -opt_is_y)
(-opt_is_m, -opt_y)

and at least one is true

(opt_is_n, opt_is_m, opt_is_y)

For larger cardinality or pseudo boolean constraints there is lots of literature
and also implementations available, which one could use to add some
say Linux specific glue/encoding logic. That is trivial (compared to depending
on 100 KLOC for SMT versus 10KLOC for SAT) and probably way faster
in particular in this case. The same is true to some extend if
we even need arithmetic constraints over small sets of domains.

Then there is no standardized API for SMT solvers. So one either
has to go through the piped SMT-LIB, or depend on one fixed SMT solver.
For SAT there is now a standard, which can easily mapped to many
solvers.

Armin

P.S. I am working on SMT and SAT solvers, so I do not have any
stake in preferring SMT over SAT from my background, it is just a engineering
argument.

> https://groups.google.com/d/msgid/kconfig-sat/29e5292f.1a7.15124411dcb.Coremail.xiongyf%40pku.edu.cn.

[Yingfei Xiong]

Hi Armin,

The problem is not only about tristate. We may have constraint like this: A -> (B > 100 /\ B < C). Where A is a Boolean or tristate option and B and C are integer options. Encoding them into SAT, while still possible, is more complex.

Regards,

Yingfei

Xiong, Yingfei / 熊英飞 / 熊英飛

Assistant Professor ("Young Talents" Plan)
Software Engineering Institute
School of Electronics Engineering and Computer Science
Peking University
China

Web: http://sei.pku.edu.cn/~xiongyf04

> send an email to kconfig-sat+unsub...@googlegroups.com.

>      Visit this group at http://groups.google.com/group/kconfig-sat.
>      To view this discussion on the web visit
> https://groups.google.com/d/msgid/kconfig-sat/3d216b07-1b0a-46be-80a0-bbf2942d25ab%40googlegroups.com.
>      For more options, visit https://groups.google.com/d/optout.
>
>
>
>
>
>
> --
> Dr. Thorsten Berger
> Assistant Professor
> Department of Computer Science and Engineering
> University of Gothenburg & Chalmers University of Technology
> Göteborg, Swedenhttp://www.thorsten-berger.netTel.: +46 (0) 31 772 6075
> Mob.: +49 177 6225422
> Skype: tberger.work
>
>
>
> --
> Project details:
>
> http://kernelnewbies.org/KernelProjects/kconfig-sat
> ---
> You received this message because you are subscribed to a topic in the
> Google Groups "kconfig-sat" group.
> To unsubscribe from this topic, visit
> https://groups.google.com/d/topic/kconfig-sat/G6HA_3ecAQI/unsubscribe.
> To unsubscribe from this group and all its topics, send an email to

> kconfig-sat+unsub...@googlegroups.com.

> Visit this group at http://groups.google.com/group/kconfig-sat.
> To view this discussion on the web visit
> https://groups.google.com/d/msgid/kconfig-sat/564EE090.7070809%40chalmers.se.
> For more options, visit https://groups.google.com/d/optout.
>
> --
> Project details:
>
> http://kernelnewbies.org/KernelProjects/kconfig-sat
> ---
> You received this message because you are subscribed to the Google Groups
> "kconfig-sat" group.
> To unsubscribe from this group and stop receiving emails from it, send an

> email to kconfig-sat+unsub...@googlegroups.com.

> Visit this group at http://groups.google.com/group/kconfig-sat.
> To view this discussion on the web visit
> https://groups.google.com/d/msgid/kconfig-sat/29e5292f.1a7.15124411dcb.Coremail.xiongyf%40pku.edu.cn.
>
> For more options, visit https://groups.google.com/d/optout.

--
Project details:

http://kernelnewbies.org/KernelProjects/kconfig-sat
---
You received this message because you are subscribed to a topic in the Google Groups "kconfig-sat" group.
To unsubscribe from this topic, visit https://groups.google.com/d/topic/kconfig-sat/G6HA_3ecAQI/unsubscribe.

To unsubscribe from this group and all its topics, send an email to kconfig-sat+unsub...@googlegroups.com.

Visit this group at http://groups.google.com/group/kconfig-sat.

To view this discussion on the web visit https://groups.google.com/d/msgid/kconfig-sat/CANp8Ba0x0p0Axx7t0-Z_rn7ZjVPwd6sjKkQnS-tnbg6GTiqGHg%40mail.gmail.com.

[Armin Biere]

So is there a list of these options with non boolean
domain (and their value ranges?). There is also CP
and ILP one would need to consider if we open the discussion
on using SMT instead of SAT ...

Armin

>> https://groups.google.com/d/msgid/kconfig-sat/3d216b07-1b0a-46be-80a0-bbf2942d25ab%40googlegroups.com.
>> For more options, visit https://groups.google.com/d/optout.
>>
>>
>>
>>
>>
>>
>> --
>> Dr. Thorsten Berger
>> Assistant Professor
>> Department of Computer Science and Engineering
>> University of Gothenburg & Chalmers University of Technology
>> Göteborg, Swedenhttp://www.thorsten-berger.netTel.: +46 (0) 31 772 6075
>> Mob.: +49 177 6225422
>> Skype: tberger.work
>>
>>
>>
>> --
>> Project details:
>>
>> http://kernelnewbies.org/KernelProjects/kconfig-sat
>> ---
>> You received this message because you are subscribed to a topic in the
>> Google Groups "kconfig-sat" group.
>> To unsubscribe from this topic, visit
>> https://groups.google.com/d/topic/kconfig-sat/G6HA_3ecAQI/unsubscribe.
>> To unsubscribe from this group and all its topics, send an email to

>> kconfig-sat...@googlegroups.com.
>> Visit this group at http://groups.google.com/group/kconfig-sat.
>> To view this discussion on the web visit
>>

>> https://groups.google.com/d/msgid/kconfig-sat/564EE090.7070809%40chalmers.se.
>> For more options, visit https://groups.google.com/d/optout.
>>
>> --
>> Project details:
>>
>> http://kernelnewbies.org/KernelProjects/kconfig-sat
>> ---
>> You received this message because you are subscribed to the Google Groups
>> "kconfig-sat" group.
>> To unsubscribe from this group and stop receiving emails from it, send an

>> email to kconfig-sat...@googlegroups.com.
>> Visit this group at http://groups.google.com/group/kconfig-sat.
>> To view this discussion on the web visit
>>

>> https://groups.google.com/d/msgid/kconfig-sat/29e5292f.1a7.15124411dcb.Coremail.xiongyf%40pku.edu.cn.
>>
>> For more options, visit https://groups.google.com/d/optout.
>
> --
> Project details:
>
> http://kernelnewbies.org/KernelProjects/kconfig-sat
> ---
> You received this message because you are subscribed to a topic in the
> Google Groups "kconfig-sat" group.
> To unsubscribe from this topic, visit
> https://groups.google.com/d/topic/kconfig-sat/G6HA_3ecAQI/unsubscribe.
> To unsubscribe from this group and all its topics, send an email to

> kconfig-sat...@googlegroups.com.
> Visit this group at http://groups.google.com/group/kconfig-sat.
> To view this discussion on the web visit

> https://groups.google.com/d/msgid/kconfig-sat/CANp8Ba0x0p0Axx7t0-Z_rn7ZjVPwd6sjKkQnS-tnbg6GTiqGHg%40mail.gmail.com.
> For more options, visit https://groups.google.com/d/optout.
>

> --
> Project details:
>
> http://kernelnewbies.org/KernelProjects/kconfig-sat
> ---
> You received this message because you are subscribed to the Google Groups
> "kconfig-sat" group.
> To unsubscribe from this group and stop receiving emails from it, send an
> email to kconfig-sat...@googlegroups.com.
> Visit this group at http://groups.google.com/group/kconfig-sat.
> To view this discussion on the web visit

> https://groups.google.com/d/msgid/kconfig-sat/47b631cb.1b2.151245b01f3.Coremail.xiongyf%40pku.edu.cn.

[Andrzej Wasowski]

I strongly believe that in the interest of maximizing maintainability and chance of adoption it would be good to consider ignoring non-boolean/non-tristate configs.

This can be done in several ways (ignoring constraints, or the substituting terms like B > 100 with ture, or best, substituting them with fresh Boolean variables).  This will of course introduce imprecision, but I doubt the imprecision will be significant.  It is important that we offer a good solution with respect to what the kernel has now, not with respect to what is in the cutting egde papers, IMHO.  Of course, without trying the approximations, we do not really know whether they are problematic or not.  If constraints involving numerals are not interdependent, an SMT solver will give little additional value.

Andrzej

--
associate prof. Andrzej Wąsowski,  http://www.itu.dk/~wasowski
IT University, Rued Langgaards Vej 7, 2300 Copenhagen, Denmark
room 4D10 phone +45 7218 5086 fax *5001 skype wasowski_andrzej

---

From: kconf...@googlegroups.com <kconf...@googlegroups.com> on behalf of Yingfei Xiong <xio...@pku.edu.cn>
Sent: Friday, November 20, 2015 11:05
To: biere
Cc: kconfig-sat
Subject: Re:Fwd: Re: [kconfig-sat] Linux Kconfig-SAT integration wiki and mailing list

 

To view this discussion on the web visit https://groups.google.com/d/msgid/kconfig-sat/47b631cb.1b2.151245b01f3.Coremail.xiongyf%40pku.edu.cn.

[Yingfei Xiong]

There are interdependent constraints with numeric values. And as Andrzej expected, they consists of only a small portion in the system.

Xiong, Yingfei / 熊英飞 / 熊英飛

Assistant Professor ("Young Talents" Plan)
Software Engineering Institute
School of Electronics Engineering and Computer Science
Peking University
China

Web: http://sei.pku.edu.cn/~xiongyf04

To unsubscribe from this group and all its topics, send an email to kconfig-sat...@googlegroups.com.

Visit this group at http://groups.google.com/group/kconfig-sat.

To view this discussion on the web visit https://groups.google.com/d/msgid/kconfig-sat/DB4PR02MB0333648BA9C6267177351871BF1A0%40DB4PR02MB0333.eurprd02.prod.outlook.com.

[Valentin Rothberg]

On Nov 20 '15 18:22, Yingfei Xiong wrote:
> There are interdependent constraints with numeric values. And as Andrzej expected, they consists of only a small portion in the system.

I agree. I don't have fresh numbers, but using value-like options in
Kconfig constraints and expressions is rather rare. Personally, I don't
expect 100 percent accuracy of any approach as the precision mainly
depends on the extracted models. I cannot evaluate SAT over SMT and the
vice versa, but what I read so far gave me the impression that a SAT
solver seems to fit more in what the community needs, something that:
- is easy to use
- is easy to maintain
- doesn't consume much time
- (and most importantly) doesn't disturb the dinosaurs' working
environment

Personally, I prefer a practical approach over bleeding-edge research in
this case.

Best regards,
Valentin

[Mate Soos]

Hi All,

I'm strongly in favour of Armin's points. As for integer stuff, I would
also advise to try to avoid it at first. Trying to create a "solution of
all solutions" is always a bad idea. Instead of overarchitecting it,
let's make something simple that does some of the job, and once we have
some experience, we can extend it if still needed.

In fact, I would be in favour of doing a small PoC (proof of concept) in
Python that calls a SAT solve, see how that works, showcase it, play
with it, and once we have some experience, decide on how to write it in
a language that fits the kernel and how it can be integrated. My
experience is that trying to plan large projects inevitably goes
haywire. Planing small iterations tends to fare better.

Just my 2 cents,

Mate

[Luis R. Rodriguez]

On Tue, Nov 10, 2015 at 02:04:39PM +0100, Thorsten Berger wrote:
> > Longer-term, you could then look to unify things like "select" and
> > "depends", since they mean approximately the same thing, just with
> > different resolution models: "select" exists for cases where turning an
> > option on should automatically enable another, while "depends" doesn't
> > allow turning on the option unless the other has been enabled. (Though
> > note that in some cases "depends" also exists to hide away a family of
> > options behind one, especially for the textual "make config".)
> That is actually an interesting question. Based on our studies of
> configurators, it seems that one wants to distinguish between visibility
> constraints (depends on) and other configuration constraints (select).
> The former cannot temporarily be violated (i.e., are immediately
> enforced -- when sub-trees are greyed out or are not visible at all in
> make config), while the latter can be (then you have a list of conflicts
> shown in the configurator, which you can ask the reasoner to resolve).
> The latter case allows you to make a lot of changes, without caring
> about the constraints, and have them sorted out later. This seems to
> boil down to usability and efficiency when working with the
> configurator. Only allowing valid changes might slow you down, but I'm
> curious about opinions here. Finally, this distinction between these two
> different kinds of constraints also appears in other configurators, such
> as in the one from eCos (open source) or in pure::variants (commercial).

During the 2016 Linux Plumbers we had a "Fixing kconfig semantics" kernel
summit track [0] on this and it was decided that it was perhaps best to just
stick to one. ie get rid of one, and emulate one with the other. I sprinkled
my notes about that session over a follow up on the similar kconfig topic a
little while ago to which Linus also replied and I'd suggest folks here read
[1].

Also, Ulf Magnusson has been doing great work upstream recently on kconfig,
some may be of interest in his unit test work, some of which should be upstream
now [2].

[0] http://www.linuxplumbersconf.org/2016/ocw/proposals/4605.html
[1] https://lists.linuxfoundation.org/pipermail/ksummit-discuss/2017-June/004499.html
[2] https://lkml.kernel.org/r/CAFkk2KSdg0+AdnncRuwUNeHH...@mail.gmail.com

Luis

[Thorsten Berger]

Hi Luis,

Thanks for the update, and for following up on this thread! I actually
have a new Master's student (Patrick Franz, in CC) who is interested in
working on this topic as part of his thesis. Remember that Daniel
Jonsson [1], who was jointly supervised by Sarah Nadi (CC) and me, had
worked on this in his thesis, but was struggling with the translation of
kconfig into propositional logic, for which he used an existing
translation, but which was inaccurate (like most translations, incl.
ours [2]). So, Patrick's focus will likely be on the translation, since
the resolution algorithm (based on rangefix) appears to work so far.

Now, given that there was some progress and various plans have been
made, it would be good to get a first-hand summary on that. The summit
you mention is already more than a year ago, and I briefly looked into
the discussion threads you provided, but it's difficult to keep an
overview on the development+plans. I also remember that there was an
email on this mailing list about some new API that allows accessing the
kconfig tree more easily. Do you think that you or someone else, who was
involved in these discussions, can give us an update via Skype in the
near future?

Best, Thorsten

[1]
http://studentarbeten.chalmers.se/publication/238168-a-case-study-of-interactive-conflict-resolution-support-in-software-configuration
[2] http://www.eng.uwaterloo.ca/~shshe/kconfig_semantics.pdf

--
Thorsten Berger
Associate Professor

Department of Computer Science and Engineering

Chalmers | University of Gothenburg, Sweden
http://www.cse.chalmers.se/~bergert

Tel.: +46 (0) 31 772 6075

Mob.: +46 (0) 729 746 246
Skype: tberger.work

[Luis R. Rodriguez]

On Sun, Feb 25, 2018 at 07:37:22PM +0100, Thorsten Berger wrote:
> Hi Luis,
>
> Thanks for the update, and for following up on this thread! I actually have
> a new Master's student (Patrick Franz, in CC) who is interested in working
> on this topic as part of his thesis. Remember that Daniel Jonsson [1], who
> was jointly supervised by Sarah Nadi (CC) and me, had worked on this in his
> thesis, but was struggling with the translation of kconfig into
> propositional logic, for which he used an existing translation, but which
> was inaccurate (like most translations, incl. ours [2]). So, Patrick's focus
> will likely be on the translation, since the resolution algorithm (based on
> rangefix) appears to work so far.

Ulf Magnusson's (CC'd now) tool (announced on this list a while ago) may help
-- not sure.

> Now, given that there was some progress and various plans have been made, it
> would be good to get a first-hand summary on that. The summit you mention is
> already more than a year ago, and I briefly looked into the discussion
> threads you provided, but it's difficult to keep an overview on the
> development+plans.

Very sure the status of that is a few folks were volunteered to work on the
things each complained about, but no one has done any of the work.

> I also remember that there was an email on this mailing
> list about some new API that allows accessing the kconfig tree more easily.

That should have been Ulf Magnusson tool -- I think he's subscribed.

> Do you think that you or someone else, who was involved in these
> discussions, can give us an update via Skype in the near future?

I don't think this is really required. I just gave you a brain dump of
what I am aware of. If there are other questions I also think the mailing
list can be used.

Luis

> --
> Project details:
>
> http://kernelnewbies.org/KernelProjects/kconfig-sat
> --- You received this message because you are subscribed to the Google
> Groups "kconfig-sat" group.
> To unsubscribe from this group and stop receiving emails from it, send an email to kconfig-sat...@googlegroups.com.

> Visit this group at https://groups.google.com/group/kconfig-sat.
> To view this discussion on the web visit https://groups.google.com/d/msgid/kconfig-sat/31eb1704-705b-8760-2f7a-cae94e9bca05%40chalmers.se.

> For more options, visit https://groups.google.com/d/optout.
>

--

Luis Rodriguez, SUSE LINUX GmbH
Maxfeldstrasse 5; D-90409 Nuernberg