[klee-dev] Percentage of KLEE's cache hits

[Cristian Cadar]

I see.  However, I think it's important to understand in a bit more 
detail how KLEE operates if you want to report precise measurements.  In 
particular, note that the fact that we have two caches and that a branch 
query (on which the first cache operates) is broken down into two 
satisfiability queries may mean that your current formula might need to 
be adjusted, depending on what exactly you would like to measure.

Best,
Cristian

On 17/10/14 17:17, Andrea Aquino wrote:
> Thank you very much Cristian,
>
> fortunately the programs I am dealing with at the moment are quite
> small and KLEE takes a reasonable amount of time to perform its task.
> When I will deal with bigger programs I will definitely have a look
> at the SolverStats.cpp file :)
>
> Best regards, Andrea Aquino
>
>
> On 17 Oct 2014, at 18:03, Cristian Cadar <c.cadar at imperial.ac.uk>
> wrote:
>
>> Hi Andrea,
>>
>> This seems reasonable, but could be quite expensive, as you have to
>> log all these queries.  A better way to do it would be to use the
>> statistics in lib/Solver/SolverStats.cpp (note that there are two
>> caches in KLEE, as explained briefly in our OSDI'08 paper and in a
>> bit more detail in CAV'13).
>>
>> Best, Cristian
>>
>> On 17/10/14 16:31, Andrea Aquino wrote:
>>> Dear all,
>>>
>>> I analyzed some programs using KLEE and I am trying to calculate
>>> how many cache hits the cache implemented in KLEE gets.
>>>
>>> I am currently doing it counting the formulas in the
>>> all-queries.smt2 file (AQ), counting the formulas in the
>>> solver-queries.smt2 file (SQ) and then calculating the percentage
>>> of hits as: [(AQ - SQ) / AQ] * 100
>>>
>>> Is this correct or am I doing some wrong assumption on the
>>> content of these two files? If it is the case, what is the
>>> easiest way to do it?
>>>
>>> Best regards, Andrea Aquino
>>> _______________________________________________ klee-dev mailing
>>> list klee-dev at imperial.ac.uk
>>> https://mailman.ic.ac.uk/mailman/listinfo/klee-dev
>>>
>>
>> _______________________________________________ klee-dev mailing
>> list klee-dev at imperial.ac.uk
>> https://mailman.ic.ac.uk/mailman/listinfo/klee-dev
>