Update on master's thesis work

[Daniel Jonsson]

Hi,

I am a Master's student at Chalmers University of Technology in Gothenburg,
Sweden. I'm working together with my supervisors Thorsten Berger
(Chalmers/Gothenburg University) and Sarah Nadi (TU Darmstadt, Germany) on
integrating a SAT solver into Kconfig. Thorsten had sent around an email
earlier about my planned thesis. I just wanted to update everybody with the
progress I have made so far.

After looking at many of the tools suggested in this thread, we decided that
Yingfei Xiong's RangeFix algorithm [1] seems to be the best fit to the
problem.
It is able to propose one or more fixes for resolving dependencies. I
have made
a prototype of xconfig [2] that helps the user with modifying options by
calling Yingfei's Scala implementation of RangeFix [3]. I have also
recorded a
video of how the workflow with the prototype looks like [4].

For RangeFix to work, you must first install Java and the SMT solver Z3.
xconfig is then able to compute configuration resolutions by running
RangeFix.jar in the background.

There are currently some issues with the prototype that we are aware of:

1. RangeFix is implemented in Scala.
2. RangeFix currently only works with version 2.6 of the Linux kernel.
3. It depends on the SMT solver Z3.
4. The presentation of the fixes in xconfig needs improvement. For
instance, we
plan to remove the option we want to modify from the proposed fixes and
order the fixes in a more sensible way.
5. For some inputs, RangeFix is not able to compute fixes. I haven't looked
into why yet.
6. It is quite slow.
7. RangeFix can currently only take tristates as arguments.

The plan is to reimplement RangeFix in C. By doing that, it will
integrate more
nicely with xconfig and the presentation of the fixes will be easier to
tweak
(I am currently reading the fixes as strings from stdout). At the same
time, I
imagine that it should be possible to make it work with a newer kernel
version
and perhaps also change the SMT solver to a SAT solver (Yingfei believes it
should be possible). The speed will hopefully also improve then. At
least, from
an earlier discussion on this mailing list, we understood that there's a
strong
preference for SAT solvers.

I am currently examining the RangeFix code and looking at Vegard's code
to see
what I can reuse for my implementation. If you have any feedback about the
prototype and about the next steps, please let us know.

Best regards,
Daniel Jonsson

[1]:
https://scholar.google.com/citations?view_op=view_citation&hl=en&user=kiG3fBsAAAAJ&citation_for_view=kiG3fBsAAAAJ:GYcXSSpN504C
[2]:
https://github.com/matachi/linux-2.6.32.y/blob/master/README-RANGEFIX.md
[3]: https://github.com/matachi/rangeFix
[4]: https://www.youtube.com/watch?v=F8RZ8YpBeew

[Luis R. Rodriguez]

On Mon, Feb 29, 2016 at 12:17:34AM +0100, Daniel Jonsson wrote:
> Hi,
>
> I am a Master's student at Chalmers University of Technology in Gothenburg,
> Sweden. I'm working together with my supervisors Thorsten Berger
> (Chalmers/Gothenburg University) and Sarah Nadi (TU Darmstadt, Germany) on
> integrating a SAT solver into Kconfig. Thorsten had sent around an email
> earlier about my planned thesis. I just wanted to update everybody with the
> progress I have made so far.

Great! I'll provide feedback but I'll be straight to the point in terms
of concerns for adoption upstream.

> After looking at many of the tools suggested in this thread, we decided that
> Yingfei Xiong's RangeFix algorithm [1] seems to be the best fit to the
> problem. It is able to propose one or more fixes for resolving dependencies.
> I have made a prototype of xconfig [2] that helps the user with modifying
> options by calling Yingfei's Scala implementation of RangeFix [3]. I have
> also recorded a video of how the workflow with the prototype looks like [4].
>
> For RangeFix to work, you must first install Java and the SMT solver Z3.
> xconfig is then able to compute configuration resolutions by running
> RangeFix.jar in the background.
>
> There are currently some issues

Thanks for pointing these are known issues..

> with the prototype that we are aware of:
>
> 1. RangeFix is implemented in Scala.

I see you note below it will be ported to C. Is it under a license that is
GPLv2 compatible? If not can the port to C be GPLv2 compatible?

> 2. RangeFix currently only works with version 2.6 of the Linux kernel.

As with prior work on SAT solver I've seen one of the issues is the
lack of keeping up to date. To solve this I recommend folks to
simply work off of Linus' tree and then daily just do:

git rebase origin/master

If you do this daily the issues of keeping up to date are minimized.

> 3. It depends on the SMT solver Z3.

What language is that based on and is it GPLv2 compatible?

> 4. The presentation of the fixes in xconfig needs improvement. For
> instance, we
> plan to remove the option we want to modify from the proposed fixes and
> order the fixes in a more sensible way.

Is there a way to just ask it to also jut go ahead and make the required
changes for for the subset of required kconfig entries we need automatically?

> 5. For some inputs, RangeFix is not able to compute fixes. I haven't looked
> into why yet.
> 6. It is quite slow.

How slow?

> 7. RangeFix can currently only take tristates as arguments.
>
> The plan is to reimplement RangeFix in C.

That's great!

> By doing that, it will integrate more nicely with xconfig and the
> presentation of the fixes will be easier to tweak (I am currently reading the
> fixes as strings from stdout). At the same time, I imagine that it should be
> possible to make it work with a newer kernel version and perhaps also change
> the SMT solver to a SAT solver (Yingfei believes it should be possible).

Can you describe what gains there are if this is done ?

> The speed will hopefully also improve then.

Great!

> At least, from an earlier discussion on this mailing list, we understood that
> there's a strong preference for SAT solvers.

I help advise on the kernel front, so I am not a SAT solver expert, I've
only loosely looked into a few papers to see how we could possibly use
one. That said I'm not too familiar with SMT solver other than from what
I've read. A SAT solver was a consideration for us on kconfig given long
ago it was considered one of the outlets for us to help avoid some issues
we could not resolve. If an SMT solver can help further please help us
in understanding how.

So: its not we prefer a SAT solver -- we need a solution to the complex
problems Kconfig has and we can't resolve today, you folks working on
all these fancy things can help us by advising us upon looking at the
problems and telling us what the main differences are. You should be
telling us what is best and why.

At a cursory review I get the sense that SMT solver just provide a more
ground for more complex problems. Is that true? If so then the next question
should be, I think, does a SAT solver suffice for our needs in Kconfig?
If not would an SMT solver help? It seems an SMT solver is slower generally,
is that true? If so why? Can't parity be maintained to SAT solver if
the predicates are not used ? Could we optionally stick to a SAT solvers
for simple boolean logic and optionally use an SMT solver for only the
cases we really need it for ? What are they?

> I am currently examining the RangeFix code and looking at Vegard's code to
> see what I can reuse for my implementation. If you have any feedback about
> the prototype and about the next steps, please let us know.

I'd like to take the time to say that I see using a SAT solver on kconfig as a
stepping stone for us in terms of the prospects of how we can use a SAT solver
on Linux, there are other uses cases -- so the impact may be more significant
long term if we get this done right. I've hinted at this before and documented
the first other use case outside of kconfig, on the Linux scheduler on
select_idle_sibling() where the schedular checks if the overall compute and
NUMA accesses of the system would be improved if the source tasks were migrated
to another target CPU. I also noted though that such use would require a
resolution in the thousands of CPU cycles time frame, and the that size of the
problems will vary depending on the number of CPUs, topology, and workloads.
Because of this I envision such uses cases futuristic as of now, but since
the rate of evolution of SAT solver seems promising one should keep this in
mind as one ideal goal we can strive towards. Also the added flexibility of
an SMT solvers with predicates might be worthy to consider if the problems
for the scheduler can be expressed with a SAT solver. There are other uses
cases of a SAT solver which I learned about at the last kernel summit.
I've taken time to document them here:

http://kernelnewbies.org/KernelProjects/linux-sat

Also one which I did not add to the list, the thee Linux media controller seems
to have its own feature graph, I was only recently made aware of this, Mauro
can provide more details.

> [1]: https://scholar.google.com/citations?view_op=view_citation&hl=en&user=kiG3fBsAAAAJ&citation_for_view=kiG3fBsAAAAJ:GYcXSSpN504C
> [2]: https://github.com/matachi/linux-2.6.32.y/blob/master/README-RANGEFIX.md
> [3]: https://github.com/matachi/rangeFix
> [4]: https://www.youtube.com/watch?v=F8RZ8YpBeew

Any chance you can extend the kconfig-sat wiki referring to your work with all
these details?

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

Luis

[Thorsten Berger]

Hi,

Let me briefly post an update of Daniel's work by replying to this old
email from Luis. In fact, we wanted to reply earlier, but had to clarify
the license issue (which actually won't be a problem, see below).

The results of Daniel's thesis will be: (1) a report providing an
overview of relevant techniques/tools for realizing an interactive
conflict-resolution technique for Kconfig, a description of the exact
challenges when trying to realize one using C and SAT, incl. the
problems of implementing the encoding transformation, (2) a prototype,
which you saw in the video (but still relying on a Scala and SMT), and
(3) empirical data stemming from an evaluation of the prototype's
performance and the survey.

For the latter, we definitely need your help distributing it. If you
have any suggestion where to post it, please let us know.

Now, what we've learned so far is that in order to have a correct
conflict-resolution support for Kconfig, we need to properly solve the
encoding problem first. None of the existing transformations is
completely correct, and it seems to be infeasible to solve this problem
in the context of a thesis project. So maybe there could be a dedicated
project (e.g., in the context of GSoC) to realize a correct
transformation. A second problem here is the constant evolution of the
Kconfig language. Kconfig's semantics are intricate anyway, but doing
little changes on its constructs seems really problematic. So, in order
to have any correct conflict-resolution, configuration-completion,
choice-propagation, or constraint-checking technique, we need to put
substantial efforts into an infrastructure project that provides a
correct encoding transformation and somehow clarifies/controls the
evolution of the Kconfig language, or even improves the language.

See more comments inline below.

We can put it under any license, which we also clarified with Yingfei
Xiong, the author of the Scala RangeFix implementation.

>> 2. RangeFix currently only works with version 2.6 of the Linux kernel.
> As with prior work on SAT solver I've seen one of the issues is the
> lack of keeping up to date. To solve this I recommend folks to
> simply work off of Linus' tree and then daily just do:
>
> git rebase origin/master
>
> If you do this daily the issues of keeping up to date are minimized.
>
>> 3. It depends on the SMT solver Z3.
> What language is that based on and is it GPLv2 compatible?

Z3 is under the MIT license, but it doesn't matter, given the preference
for SAT solvers, see below.

>> 4. The presentation of the fixes in xconfig needs improvement. For
>> instance, we
>> plan to remove the option we want to modify from the proposed fixes and
>> order the fixes in a more sensible way.
> Is there a way to just ask it to also jut go ahead and make the required
> changes for for the subset of required kconfig entries we need automatically?

Yes, this just needs to be implemented. The idea is that the user
selects the desired fix (which changes multiple configs) and let it
apply automatically. In the future,

>> 5. For some inputs, RangeFix is not able to compute fixes. I haven't looked
>> into why yet.
>> 6. It is quite slow.
> How slow?

Details will be in the thesis, Daniel is working on that.

>
>> 7. RangeFix can currently only take tristates as arguments.
>>
>> The plan is to reimplement RangeFix in C.
> That's great!

Daniel has started implementing parts in C, which can be used by
follow-up works. But he was stuck with the encoding (he could use some
code and ideas from Vegard), but it's clear that we need to put more
effort into this and to make it correct; he discovered many subtle errors.

>
>> By doing that, it will integrate more nicely with xconfig and the
>> presentation of the fixes will be easier to tweak (I am currently reading the
>> fixes as strings from stdout). At the same time, I imagine that it should be
>> possible to make it work with a newer kernel version and perhaps also change
>> the SMT solver to a SAT solver (Yingfei believes it should be possible).
> Can you describe what gains there are if this is done ?

Yeah, so from previous discussions in this mailing list, we noticed a
strong preference for SAT solvers. Although we don't have full empirical
evidence that they're in fact faster for generating conflict
resolutions, it's very likely that they are. SMT allows dealing with
arithmetic constraints, and Yingfei's range-fix algorithm was developed
with keeping such constraints in mind, as they're very common in the
eCos configurator. In the Kconfig model, currently, there are no
constraints over arithmetic restrictions (e.g., ranges), so there's no
benefit of using an SMT solver, unless there are any plans of doing so.
In fact, the eCos configurator uses arithmetic and string constraints
that a lot (e.g., calculating CPU frequency based on other configuration
options, or calculating strings controlling header includes based on
other options, afair).

>
>> The speed will hopefully also improve then.
> Great!
>
>> At least, from an earlier discussion on this mailing list, we understood that
>> there's a strong preference for SAT solvers.
> I help advise on the kernel front, so I am not a SAT solver expert, I've
> only loosely looked into a few papers to see how we could possibly use
> one. That said I'm not too familiar with SMT solver other than from what
> I've read. A SAT solver was a consideration for us on kconfig given long
> ago it was considered one of the outlets for us to help avoid some issues
> we could not resolve. If an SMT solver can help further please help us
> in understanding how.

See above. It would be interesting to know the future plans for the
configurator. How you think it will be growing, whether there will be
arithmetic or string constraints in the future, etc.

>
> So: its not we prefer a SAT solver -- we need a solution to the complex
> problems Kconfig has and we can't resolve today, you folks working on
> all these fancy things can help us by advising us upon looking at the
> problems and telling us what the main differences are. You should be
> telling us what is best and why.
>
> At a cursory review I get the sense that SMT solver just provide a more
> ground for more complex problems. Is that true? If so then the next question
> should be, I think, does a SAT solver suffice for our needs in Kconfig?
> If not would an SMT solver help? It seems an SMT solver is slower generally,
> is that true? If so why? Can't parity be maintained to SAT solver if
> the predicates are not used ? Could we optionally stick to a SAT solvers
> for simple boolean logic and optionally use an SMT solver for only the
> cases we really need it for ? What are they?

That's a good question, where the SAT experts in this mailing list could
help. In principle, SMT solvers should be as fast as SAT solvers when
sticking to Boolean logic; but I could also imagine that the SAT
community has put more effort into optimizing their solvers so that
dedicated SAT solvers would be faster anyway. Whether it has a practical
impact for Kconfig is another question. At least the SMT-based prototype
is slow, as shown by Daniel in the video.

>
>> I am currently examining the RangeFix code and looking at Vegard's code to
>> see what I can reuse for my implementation. If you have any feedback about
>> the prototype and about the next steps, please let us know.
> I'd like to take the time to say that I see using a SAT solver on kconfig as a
> stepping stone for us in terms of the prospects of how we can use a SAT solver
> on Linux, there are other uses cases -- so the impact may be more significant
> long term if we get this done right. I've hinted at this before and documented
> the first other use case outside of kconfig, on the Linux scheduler on
> select_idle_sibling() where the schedular checks if the overall compute and
> NUMA accesses of the system would be improved if the source tasks were migrated
> to another target CPU. I also noted though that such use would require a
> resolution in the thousands of CPU cycles time frame, and the that size of the
> problems will vary depending on the number of CPUs, topology, and workloads.
> Because of this I envision such uses cases futuristic as of now, but since
> the rate of evolution of SAT solver seems promising one should keep this in
> mind as one ideal goal we can strive towards. Also the added flexibility of
> an SMT solvers with predicates might be worthy to consider if the problems
> for the scheduler can be expressed with a SAT solver. There are other uses
> cases of a SAT solver which I learned about at the last kernel summit.
> I've taken time to document them here:
>
> http://kernelnewbies.org/KernelProjects/linux-sat
>

Yeah, so that's another point to consider. When SAT solvers are faster
than SMT solvers in general, even when sticking to Boolean problems,
then just integrating and maintaining one solver in the kernel codebase
is probably the best option. That's also what we got from the previous
discussion. But again, it also depends on the future plans with Kconfig.

HTH!
Best, Thorsten

> Also one which I did not add to the list, the thee Linux media controller seems
> to have its own feature graph, I was only recently made aware of this, Mauro
> can provide more details.
>
>> [1]:https://scholar.google.com/citations?view_op=view_citation&hl=en&user=kiG3fBsAAAAJ&citation_for_view=kiG3fBsAAAAJ:GYcXSSpN504C
>> [2]:https://github.com/matachi/linux-2.6.32.y/blob/master/README-RANGEFIX.md
>> [3]:https://github.com/matachi/rangeFix
>> [4]:https://www.youtube.com/watch?v=F8RZ8YpBeew
> Any chance you can extend the kconfig-sat wiki referring to your work with all
> these details?
>
> http://kernelnewbies.org/KernelProjects/kconfig-sat
>
> Luis
>

--
Dr. Thorsten Berger
Assistant Professor
Department of Computer Science and Engineering
Chalmers | University of Gothenburg
Göteborg, Sweden
http://www.thorsten-berger.net
Tel.: +46 (0) 31 772 6075
Skype: tberger.work