Discussion:
Why there are so many weighted random search algorithms in KLEE?
Loi Luu
2013-04-28 02:31:23 UTC
Permalink
Dear all,

I noticed that there are several NURS algorithms in klee, and each will
randomly select a state based on its own distribution. So why do we need
many of them in KLEE while after all we do randomly select states?

Thanks,
--
Loi, Luu The (Mr.)
University of Engineering and Technology, Vietnam National University,
Hanoi.
g***@public.gmane.org
2013-04-30 11:57:32 UTC
Permalink
Hello,
Post by Loi Luu
I noticed that there are several NURS algorithms in klee, and each will
randomly select a state based on its own distribution. So why do we need
many of them in KLEE while after all we do randomly select states?
For me it feels like you've answered your own question:
Because they have different distributions :).

If you would have findings about best distribution for selecting next
node (maybe taking into account control/data flow structure) this
might be nice contribution.

Cheers,
Greg
Loi Luu
2013-04-30 12:12:31 UTC
Permalink
Hi Greg,

What I am curious is that when we select the state, we do it randomly.
Therefore, the effect of distribution type is reduced or maybe zero. So am
I right to think that?

Regards,
Post by g***@public.gmane.org
Hello,
Post by Loi Luu
I noticed that there are several NURS algorithms in klee, and each will
randomly select a state based on its own distribution. So why do we need
many of them in KLEE while after all we do randomly select states?
Because they have different distributions :).
If you would have findings about best distribution for selecting next
node (maybe taking into account control/data flow structure) this
might be nice contribution.
Cheers,
Greg
--
Loi, Luu The (Mr.)
University of Engineering and Technology, Vietnam National University,
Hanoi.
g***@public.gmane.org
2013-04-30 12:40:07 UTC
Permalink
Hi Loi,

As far as I remember from papers, it was NOT like taking any random
not processed leafs, but some kind of mixture between bfs/dfs to avoid
problems with loops. However I have not digged (yet) into that part of
code, so it's hard to me to point specifics.

Cheers,
Greg
Post by Loi Luu
Hi Greg,
What I am curious is that when we select the state, we do it randomly.
Therefore, the effect of distribution type is reduced or maybe zero. So am I
right to think that?
Regards,
Post by g***@public.gmane.org
Hello,
Post by Loi Luu
I noticed that there are several NURS algorithms in klee, and each will
randomly select a state based on its own distribution. So why do we need
many of them in KLEE while after all we do randomly select states?
Because they have different distributions :).
If you would have findings about best distribution for selecting next
node (maybe taking into account control/data flow structure) this
might be nice contribution.
Cheers,
Greg
--
Loi, Luu The (Mr.)
University of Engineering and Technology, Vietnam National University,
Hanoi.
Loi Luu
2013-04-30 15:41:37 UTC
Permalink
Hi Greg,

In file searcher.cpp, the selectState function is implemented as:

ExecutionState &WeightedRandomSearcher::selectState() {
return *states->choose(theRNG.getDoubleL());
}

They just randomize a double number as the weight of the wanted state and
find it from the execution tree.

Regards,
Post by g***@public.gmane.org
Hi Loi,
As far as I remember from papers, it was NOT like taking any random
not processed leafs, but some kind of mixture between bfs/dfs to avoid
problems with loops. However I have not digged (yet) into that part of
code, so it's hard to me to point specifics.
Cheers,
Greg
Post by Loi Luu
Hi Greg,
What I am curious is that when we select the state, we do it randomly.
Therefore, the effect of distribution type is reduced or maybe zero. So
am I
Post by Loi Luu
right to think that?
Regards,
Post by g***@public.gmane.org
Hello,
Post by Loi Luu
I noticed that there are several NURS algorithms in klee, and each
will
Post by Loi Luu
Post by g***@public.gmane.org
Post by Loi Luu
randomly select a state based on its own distribution. So why do we
need
Post by Loi Luu
Post by g***@public.gmane.org
Post by Loi Luu
many of them in KLEE while after all we do randomly select states?
Because they have different distributions :).
If you would have findings about best distribution for selecting next
node (maybe taking into account control/data flow structure) this
might be nice contribution.
Cheers,
Greg
--
Loi, Luu The (Mr.)
University of Engineering and Technology, Vietnam National University,
Hanoi.
--
Loi, Luu The (Mr.)
University of Engineering and Technology, Vietnam National University,
Hanoi.
Loading...