Percentage of KLEE's cache hits

[Andrea Aquino]

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

[Cristian Cadar]

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

Post by Andrea Aquino
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
https://mailman.ic.ac.uk/mailman/listinfo/klee-dev

[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

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

Post by Cristian Cadar
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

Post by Andrea Aquino
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
https://mailman.ic.ac.uk/mailman/listinfo/klee-dev

_______________________________________________ klee-dev mailing
https://mailman.ic.ac.uk/mailman/listinfo/klee-dev