Discussion:
OSDI2008 experiment
(too old to reply)
Zhiyi Zhang
2014-07-31 09:31:04 UTC
Permalink
Hi all,

In the section3.2 of your OSDI2008's paper, there is a experiment about
independence and cex.cache optimizations. You run klee for 5 minutes with
both optimization turned off and then run same number *instructions(not
query) *with independence and cex,cache separately.

However, I am confused about the meaning of query. I have two questions.

First, I used the command in
http://klee.github.io/klee/TestingCoreutils.html, and result contains the
number of *instruction.* But* how can I get the execution number of the
queries*? I didn't find the related options in klee‘s help. And *what is
the different between the instruction and the query*?

Second, In the experiment of OSDI2008's paper, you run klee for 5 minutes.
If one program was small and executed less than 5 minutes, such as echo,*
how to deal with the remaining time*? Do nothing, run this program again
until 5 minutes or run other program until 5 minutes?


Thank you very much.
Zhiyi Zhang
Cristian Cadar
2014-09-12 13:31:03 UTC
Permalink
Hi Zhiyi,
Post by Zhiyi Zhang
Hi all,
In the section3.2 of your OSDI2008's paper, there is a experiment about
independence and cex.cache optimizations. You run klee for 5 minutes
with both optimization turned off and then run same number
*instructions(not query) *with independence and cex,cache separately.
However, I am confused about the meaning of query. I have two questions.
First, I used the command
in http://klee.github.io/klee/TestingCoreutils.html, and result contains
the number of *instruction.* But*how can I get the execution number of
the queries*?
Look at http://klee.github.io/klee/klee-tools.html#klee-stats
Post by Zhiyi Zhang
I didn't find the related options in klee‘s help. And
*what is the different between the instruction and the query*?
The latter refers to constraint solver queries.
Post by Zhiyi Zhang
Second, In the experiment of OSDI2008's paper, you run klee for 5
minutes. If one program was small and executed less than 5 minutes, such
as echo,*how to deal with the remaining time*? Do nothing, run this
program again until 5 minutes or run other program until 5 minutes?
We ignored those utilities for which KLEE takes less than 5 minutes to
execute.

Best,
Cristian
Post by Zhiyi Zhang
Thank you very much.
Zhiyi Zhang
_______________________________________________
klee-dev mailing list
https://mailman.ic.ac.uk/mailman/listinfo/klee-dev
Loading...