On Mar 9, 2010, at 2:46 AM, Daniel Dunbar wrote: > On Sat, Mar 6, 2010 at 3:38 PM, Chung-chieh Shan > <ccshan at rutgers.edu> wrote: > >> A broader question is about how KLEE explores its search space of >> states. It seems that states only fork (on branches), never >> rejoin. Might it be profitable to identify states that are >> equivalent and merge them (so the search space is a DAG rather than >> tree)? Or is it pretty clear that the cost of merging states >> outweighs the benefits? > > Yes, KLEE as described in the OSDI paper only forks. And yes, it can > be very very profitable to merge states, and the repository contains > some basic functionality for experimenting with this. It is relatively > cheap to (precisely) merge two states whose heaps haven't diverged, > but there are a number of non-trivial problems: > (1) How to decide when to merge states? > (2) What to do with states whose heaps have diverged? This is hard to > solve given the current memory model in KLEE. Solving it is possible, > but then impacts performance in other areas. > (3) What is the impact of merging states on the constraint solver? In > general merging states is going to introduce disjunctions, which lead > to more expensive queries. It will often be a win since the > disjunctions can be simplified, but it may sometimes be a loss. > > All in all, there is lots of potential for merging and it is a good > direction for future work, but definitely a research project. An > interesting approach is to do something like "speculative merging", as > in: > http://www.doc.ic.ac.uk/~cristic/papers/exe-rwset-tacas-08.pdf
I recently came across this paper, which discusses some costs and benefits of merging states (although in a different tool, not in KLEE itself): http://ww2.cs.mu.oz.au/~thansen/stateJoining.pdf Elnatan -------------- next part -------------- An HTML attachment was scrubbed... URL: http://keeda.Stanford.EDU/pipermail/klee-dev/attachments/20100309/82321ada/attachment.html
