David, looks like the source of the problem is in the following code (not
connected with DiscretePDF):
*WeightedRandomSearcher::WeightedRandomSearcher(WeightType _type)*
* : states(new DiscretePDF<ExecutionState*>()),*
* type(_type) {*
* switch(type) {*
* case Depth: *
* updateWeights = false;*
* break;*
* case InstCount:*
* case CPInstCount:*
* case QueryCost:*
* case MinDistToUncovered:*
* case CoveringNew:*
* updateWeights = true;*
* break;*
* default:*
* assert(0 && "invalid weight type");*
* }*
*}*
This "false" caused the internal tree of DiscretePDF to be incorrect
(node.sumWeights != sum of children weights).
After changing this to true got a reasonable distribution:
*0.025 305 (297 with the path)*
*0.05 186 (192 with the path)*
*0.075 0*
*0.1 0*
*0.125 0*
*0.15 0*
*0.175 0*
*0.2 0*
*0.225 0*
*0.25 509 (511 with the path)*
*
*
And the states are (for the initial version - without the path)
*0.25, 0.03125, 0.03125, 0.03125, 0.015625, 0.015625, 0.015625, 0.0078125,
0.0078125, 0.0078125, 0.0078125, 0.0078125, 0.0078125, 0.0078125,
0.00390625, 0.00390625, 0.00390625, 0.00390625, 0.00390625, 0.00390625,
0.00390625, 0.00390625, 0.00390625, 0.00390625, 0.00195312, 0.00195312,
0.00195312, 0.00195312, 0.00195312, 0.00195312, 0.00195312, 0.000976562,
0.000488281, 0.000244141, 0.00012207, 6.10352e-05, 3.05176e-05, 1.52588e-05,
7.62939e-06, 3.8147e-06, 1.90735e-06, 1.90735e-06*
SumOfNodeWeights (weight <= 0.025) = 0.156
SumOfNodeWeights (0.025 < weight <= 0.05) = 0.093
305/186 = 1.64 ~ 1.67 = .156/.093
(when apply the path, these sums remain the same).
If this was done (false value) for a specific purpose please comment..
--
Sincerely,
Ayrat
On Wed, Feb 2, 2011 at 2:21 AM, Ayrat Khalimov <airat.halimov at
gmail.com>wrote:
> David,
> Applied patch and got similar distribution (before, after):
> 0.05 403 335
> 0.1 0 52
> 0.15 0 0
> 0.2 0 0
> 0.25 193 184
> 0.3 0 0
> 0.35 0 0
> 0.4 0 0
> 0.45 0 0
> 0.5 391 413
>
> The states changed but the sum of weights below 0.05 remained the same ~
> 0.234.
> After applying the patch states at the moment of gathering data were:
> 0.5, 0.25, 0.0625, 0.03125, 0.03125, 0.015625, 0.015625, 0.0078125,
> 0.0078125, 0.0078125, 0.00390625, 0.00390625, 0.00390625, 0.00390625,
> 0.00390625, 0.00390625, 0.00390625, 0.00390625, 0.00390625, 0.00195312,
> 0.00195312, 0.00195312, 0.00195312, 0.00195312, 0.00195312, 0.00195312,
> 0.00195312, 0.000976562, 0.000976562, 0.000976562, 0.000488281, 0.000244141,
> 0.00012207, 6.10352e-05, 3.05176e-05, 1.52588e-05, 7.62939e-06, 3.8147e-06,
> 1.90735e-06, 1.91E-006
>
> For transparency here is the description of the experiment:
> run printf.bc (with --sym-args 0 2 4) under klee. Used *WeightedRandomSearcher
> *with *Depth WeightType.*
> In the call selectState the check on number of states in the DiscretePDF is
> added -- when DiscretePDF contains more than 30 states start gathering data
> (call choose with *theRNG*).
>
>
> --Sincerely, Ayrat
>
>
> On Tue, Feb 1, 2011 at 11:26 PM, David A. Ramos <daramos at
> stanford.edu>wrote:
>
>> Ayrat,
>>
>> Thanks for the clarification. In that case, some of the results do seem
>> valid. At first glance, the single 0.5 state was chosen twice as often as
>> the 0.25 state.
>>
>> The bucket size for weights <= 0.05 is a little deceptive since it
>> includes states with much smaller weights. In reality, what matters is the
>> sum of the weights of all the states in that bucket. With the data you gave,
>> that's a sum of 0.234 for the 29 "smaller" states. Now, if DiscretePDF is
>> working correctly, it should have chosen states from this bucket about as
>> often as it chose the single state with weight 0.25.
>>
>> However, it chose these smaller states *twice* as often, which is wrong
>> (assuming the RNG is working correctly). Disproportionately choosing states
>> with smaller weights could certainly be one source of low coverage.
>>
>> Can you try applying the patch I sent out and see how that affects these
>> results?
>>
>> Thanks for your help,
>> -David
>>
>> On Feb 1, 2011, at 12:03 PM, Ayrat Khalimov wrote:
>>
>> David, thanks,
>>
>>> DiscretePDF::choose() is supposed to return nodes uniformly distributed
>>> over the sum of the weights of all the nodes. That is, a node with weight 2N
>>> is twice as likely to be chosen as a node with weight N. It's supposed to be
>>> uniform, however, so the results you report are worrisome
>>
>>
>> Looked again at my experiment. There is definitely a weak point:
>> initial distribution of weights of states is not a uniform distribution -
>> there are lots of states with small weights and very little states with
>> large weights:
>> 0.5, 0.25, 0.03125, 0.03125, 0.03125, 0.015625, 0.015625, 0.015625,
>> 0.015625, 0.0078125, 0.0078125, 0.0078125, 0.00390625, 0.00390625,
>> 0.00390625, 0.00390625, 0.00390625, 0.00390625, 0.00390625, 0.00390625,
>> 0.00390625, 0.00390625, 0.00195312, 0.00195312, 0.00195312, 0.00195312,
>> 0.00195312, 0.00195312, 0.00195312, 0.000976562, 0.000976562
>>
>> Well, in this case I think it is OK to have described earlier
>> distribution:
>> 0.05 402
>> 0.1 0
>> 0.15 0
>> 0.2 0
>> 0.25 198
>> 0.3 0
>> 0.35 0
>> 0.4 0
>> 0.45 0
>> 0.5 400
>>
>> What do u think?
>>
>>
>> --
>> Best regards,
>> Ayrat
>>
>>
>>
>> On Tue, Feb 1, 2011 at 5:24 AM, David A. Ramos <daramos at
>> stanford.edu>wrote:
>>
>>> Ayrat,
>>>
>>> Can you tell me if this patch changes your results at all? If not, could
>>> you send us the complete code for the experiment you're using to evaluate
>>> DiscretePDF?
>>>
>>> Daniel/Cristi: It seems like after a rotation, we should be setting the
>>> sums of the child before the parent, which relies on the child.
>>>
>>> Thanks,
>>> -David
>>>
>>>
>>>
>>> On Jan 31, 2011, at 12:42 PM, Ayrat Khalimov wrote:
>>>
>>> Hi, All,
>>> During testing different path exploration strategies (*
>>> WeightedRandomSearcher* with *Depth* *WeightType)*
>>> **I have encountered an interesting class - *DiscretePDF.*
>>> What is its purpose?
>>> Ok, the first purpose is clear - it is an associative set (looks like
>>> red-black tree).
>>> But what about its *choose* method?
>>> Does it choose states according to some probability distribution of
>>> values? If yes - then what distribution does it use? The more weight the
>>> greater/less probability? How it take into account states' depth (or states'
>>> weight) ?
>>> (I found no known to me distribution of chosen values during
>>> experiments.. please correct if this is wrong)
>>>
>>> Also what is strange is that the location of the node in the *DiscretePDF
>>> *internal tree depends on memory address of inserted value.
>>> And child-parent connection depends on these memory addresses. And
>>> doesn't depend on weights.
>>> But the result of *choose* method depends on the total weight of the
>>> node (with kids weights) and hence on the structure of the internal tree.
>>> And hence the result of *choose* method depends on memory addresses of
>>> ExecutionState objects..
>>>
>>> I've made an experiment. When tree size reach 30 states, 10000 samples
>>> are chosen:
>>> *if(nodesCount > 30) {*
>>> * for(int i = 0; i < 10000; ++i) {*
>>> * ExecutionState* state = states->choose(theRNG.getDoubleL());*
>>> * std::cerr << state->weight << "\t" <<
>>> states->getFamilyWeight(state) << std::endl;*
>>> * }*
>>> *}*
>>>
>>> Results:
>>> here is two distributions of chosen values:
>>> 1. own node weight (range of own weight, the number of values chosen in
>>> this range)
>>> 0.05 4003
>>> 0.1 0
>>> 0.15 0
>>> 0.2 0
>>> 0.25 1993
>>> 0.3 0
>>> 0.35 0
>>> 0.4 0
>>> 0.5 3880
>>>
>>> 2. sum node weight (weight of node + weights of its children):
>>> 0.1 1784
>>> 0.2 554
>>> 0.3 1986
>>> 0.4 0
>>> 0.5 0
>>> 0.6 0
>>> 0.7 0
>>> 0.8 4157
>>> 1.3 1519
>>>
>>> As you can see - quite a strange distribution.
>>> (Also checked the random generator - it is ok - random distributed).
>>>
>>> Please comment on these questions.
>>>
>>> Thanks!
>>>
>>> --
>>> Sincerely,
>>> Ayrat Khalimov,
>>> Russia, Uljanovsk
>>>
>>>
>>> _______________________________________________
>>> klee-dev mailing list
>>> klee-dev at keeda.stanford.edu
>>> http://keeda.Stanford.EDU/mailman/listinfo/klee-dev
>>>
>>>
>>>
>>>
>>
>>
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL:
http://keeda.Stanford.EDU/pipermail/klee-dev/attachments/20110202/191e4d1e/attachment.html
