On 20/08/14 02:00, [email protected] wrote:
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.
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
_______________________________________________
klee-dev mailing list
[email protected]
https://mailman.ic.ac.uk/mailman/listinfo/klee-dev
