Distributed Symbolic Execution

[e***@public.gmane.org]

Hello,

I am involved in a project that aims to develop a scalable symbolic
execution (KLEE) based testing tool. I have already done background
research and tested KLEE and Cloud9, and I'm in the process of getting
more familiar with the internal functionality and the code bases, and
deciding in which direction to continue. I have a few preliminary questions:

1) On the KLEE website, under the "Open Projects" section, you list
"Distributed Constraint Solving" as one possible improvement. Since
constraint solving dominates the run time of KLEE, it makes sense that
this is the hottest target to parallelize. Based on your experience, do
you imagine a good scalable KLEE implementation to be one that targets
mainly/only parallel constraint solving? Also, do you think this is
feasible on KLEE-level, without modifying the underlying constraint
solver (and thereby restricting ourselves to one specific solver)?
2) In the context of question 1, what is your opinion about Cloud9's
(higher-level) way of parallelizing KLEE?
3) Cloud9 is based on KLEE, and besides distributed execution, it
provides further improvements like an extended POSIX model, incl.
multi-thread/process support. What is the reason that (part of) these
improvements have not been merged into KLEE?

The first two questions are a bit broad, so I'm not expecting concrete
answers, I would rather like to hear the opinions or gut feelings of
people experienced with KLEE's architecture and symbolic execution. This
would also help to go in a direction that could potentially be of
benefit to KLEE, too.

Thank you!
Best regards,
Emil

[Cristian Cadar]

Post by e***@public.gmane.org
1) On the KLEE website, under the "Open Projects" section, you list
"Distributed Constraint Solving" as one possible improvement. Since
constraint solving dominates the run time of KLEE, it makes sense that
this is the hottest target to parallelize. Based on your experience, do
you imagine a good scalable KLEE implementation to be one that targets
mainly/only parallel constraint solving? Also, do you think this is
feasible on KLEE-level, without modifying the underlying constraint
solver (and thereby restricting ourselves to one specific solver)?

One thing that we have already tried out is to use multiple constraint
solvers, take a look here
http://srg.doc.ic.ac.uk/projects/klee-multisolver/. So KLEE is not
restricted to a single solver anymore, although STP still seems to
generally perform the best, at least based on our (limited) experience.

Post by e***@public.gmane.org
3) Cloud9 is based on KLEE, and besides distributed execution, it
provides further improvements like an extended POSIX model, incl.
multi-thread/process support. What is the reason that (part of) these
improvements have not been merged into KLEE?

I think that's a better question to ask the Cloud9 developers :) In
general, there are many nice tools out there that are based on KLEE, and
it is indeed unfortunate that they are not part of a single tool. I
strongly encourage people to contribute their techniques to KLEE, and
we've also tried to integrate more of our research work into the main
codebase (the multi-solver example mentioned above is one example).

But at the same time I do understand that it is not always possible to
easily integrate things into KLEE's main codebase, often for logistical
reasons and time constraints. From my conversation a while ago with
Stefan from Cloud9, I understand time is really the main reason. And
now that the KLEE codebase has seen significant changes in the last few
years, this would be even more difficult.

Best,
Cristian

[Emil Rakadjiev]

Hello Cristian,

Post by Cristian Cadar
One thing that we have already tried out is to use multiple constraint
solvers, take a look here
http://srg.doc.ic.ac.uk/projects/klee-multisolver/. So KLEE is not
restricted to a single solver anymore, although STP still seems to
generally perform the best, at least based on our (limited) experience.

Thanks for the reply! The multisolver/portfolio approach is definitely
interesting, but with it the overall performance is still bounded by the
performance of the fastest solver. That is, it improves symbolic
execution performance, but it doesn't make it scalable. Our initial aim
is similar to that of Cloud9, i.e. to have an implementation that can
easily scale out, thus making it possible to test large applications and
achieve higher coverage in a shorter amount of time.

Post by Cristian Cadar
I think that's a better question to ask the Cloud9 developers :) In
general, there are many nice tools out there that are based on KLEE,
and it is indeed unfortunate that they are not part of a single tool.
I strongly encourage people to contribute their techniques to KLEE,
and we've also tried to integrate more of our research work into the
main codebase (the multi-solver example mentioned above is one example).
But at the same time I do understand that it is not always possible to
easily integrate things into KLEE's main codebase, often for
logistical reasons and time constraints. From my conversation a while
ago with Stefan from Cloud9, I understand time is really the main
reason. And now that the KLEE codebase has seen significant changes
in the last few years, this would be even more difficult.

Thank you for those details! I agree that it would be great to make KLEE
even more versatile and possibly "production-ready" with the help of
external contributions. But time indeed causes lots of inconvenience
(... I've heard...).
The distributed execution part of Cloud9 introduces many changes to the
code, so that would be harder to merge, but I was mainly surprised why
the extended POSIX model has not been contributed to KLEE. Of course,
multi-threading support also requires changes like extending states,
adding scheduling, etc., and e.g. replaying thread interleavings is not
trivial, but I think those additions from Cloud9 would be very useful
for KLEE, too. Actually, this is something I was planning to look into,
whether those extensions can be cleanly integrated into upstream KLEE.
Unfortunately, Cloud9 doesn't seem to be maintained anymore.

Best regards,
Emil