On 13/11/2013 09:40, Hongxu Chen wrote:
Thanks, Paul. I think I really missed it.
In klee-multisolver-cav-13 paper, it mentions that some strategies to
avoid non-determinisms:
1. use DFS search strategy
2. turned o ff address-space layout randomisation
3. implement a deterministic memory allocator
For the 2nd item, is there some command line option for it or I have to
change the source code?
This has nothing to do with KLEE, just google for something like "turn
off address-space layout randomization"
Also, I'm lost on why "concrete memory addresses" matters; is it because
of the memory error check?
(Sorry I didn't read the source code of KLEE carefully)
One reason is the way KLEE does object resolution (you need to take a
look at the code for details), but there are other implementation-level
issues.
KLEE could certainly be made more deterministic (although there are
fundamental limitations, due to way it times out constraint queries),
and this would be a great contribution to make, if anyone is interested.
Cristian
Many thanks!
Best Regards,
Hongxu Chen
On Wed, Nov 13, 2013 at 1:45 PM, Paul Marinescu
<[email protected] <mailto:[email protected]>>
wrote:
You may have missed a message sent to the list just a few days ago,
related to your non-determinism question
"You might want to take a look at our CAV'13 paper
(http://srg.doc.ic.ac.uk/publications/klee-multisolver-cav-13.html),
which discusses in more detail the constraint solving optimizations
in KLEE (and cex caching in particular) and also what we had to do
to get deterministic runs."
Paul
On 13 Nov 2013, at 04:48, Hongxu Chen <[email protected]
<mailto:[email protected]>> wrote:
BTW, since there are some non-determinisms in KLEE, can I totally
avoid them and let 2 executions of KLEE
comparable in general with certain options? Would you please share
some good practice?
Thanks in advance.
Best Regards,
Hongxu
On Wed, Nov 13, 2013 at 9:07 AM, Hongxu Chen
<[email protected] <mailto:[email protected]>> wrote:
Sorry that I forgot mentioning that we slightly modified KLEE
and just let it "exit on assert",
so the running time results are all generated under this
circumstance.
On Wed, Nov 13, 2013 at 12:10 AM, Hongxu Chen
<[email protected] <mailto:[email protected]>> wrote:
Dear all,
We are doing some experiments with some determinism.
I find that there was at least 2 threads about it before:
1. Non-determinism in
Klee(http://keeda.stanford.edu/pipermail/klee-dev/2010-September/000470.html)
2. computing the
coverage(http://keeda.stanford.edu/pipermail/klee-dev/2010-March/000251.html)
Unfortunately I failed to fully understand them.
So here is what we've done:
(1) We basically follow the options at "coreutils
experiments" page.
klee \
--simplify-sym-indices --write-cvcs --write-cov
--output-module \
--max-memory=1000 --disable-inlining --optimize
--use-forked-solver \
--use-cex-cache --libc=uclibc --posix-runtime \
--allow-external-sym-calls
--only-output-states-covering-new \
--environ=test.env --run-in=/tmp/sandbox \
--max-sym-array-size=4096 --max-instruction-time=30.
--max-time=3600. \
--watchdog --max-memory-inhibit=false
--max-static-fork-pct=1 \
--max-static-solve-pct=1 --max-static-cpfork-pct=1
--switch-type=internal \
*--randomize-fork* *--search=random-path
--search=nurs:covnew \ *
*--use-batching-search --batch-instructions=10000 \ *
./rm.bc --sym-args 0 1 10 --sym-args 0 2 2 --sym-files 1 8
--sym-stdout
Firstly, we change the search strategy to DFS, i.e.
*--search=dfs*
But when tested with a slightly /modified /_rm _case, we
found that there are
some HUGE differences for the running time: KLEE finds the
error within about
2400s for once, but about one day later it finds the exact
error within only 30s-50s!
*So is it a regular result*?
The only potential difference I can think out is: the
machine I ran KLEE on may be used
by other CPU-bound operations(but since I don't have
priviledge to know the
details of the machine I cannot make sure) when KLEE took
2400s to file the bug.
(2) Later in order to keep the results a bit more
determinist, we also
1. discard "*--randomize-fork*"
2. discard "*--use-batching-search
--batch-instructions=10000*"
So the final option we are using is
klee \
--simplify-sym-indices --write-cvcs --write-cov
--output-module \
--max-memory=1000 --disable-inlining --optimize
--use-forked-solver \
--use-cex-cache --libc=uclibc --posix-runtime \
--allow-external-sym-calls
--only-output-states-covering-new \
--environ=test.env --run-in=/tmp/sandbox \
--max-sym-array-size=4096 --max-instruction-time=30.
--max-time=3600. \
--watchdog --max-memory-inhibit=false
--max-static-fork-pct=1 \
--max-static-solve-pct=1 --max-static-cpfork-pct=1
--switch-type=internal \
*--search=dfs* \
./rm.bc --sym-args 0 1 10 --sym-args 0 2 2 --sym-files 1 8
--sym-stdout
However it seems that when running, there are still some
time difference
even on a SINGLE machine(still mainly about the time; but
it seems that
the time is still unstable. From what we observed,the
longest time may
be bigger than 10% than the shortest one).
And for 2 machines that almost have the same power and
system configurations,
the running time difference is even bigger.
The counter example path condition also has several
differences for
a simple test case(I only compared the diff of the xxx.pc
files and notice
there are several changes but didn't get a better
knowledge about the semantics).
*Is it reasonable?*
(3) Also I tested with a script by running with a simple case:
This case is taken from one of the previous issues on GITHUB:
https://github.com/ccadar/klee/issues/50
Only the "main" function's signature has been changed to
2-args' version.
#include <assert.h>
#include <klee/klee.h>
const char *const errmsg[2] = {0, };
const char *get_error_message(int err) {
char const *x = errmsg[err];
return x;
}
int main(int argc, char** argv) {
int err;
klee_make_symbolic(&err, sizeof(err), "err");
get_error_message(err);
}
I ran it with a script like below:
while [ 1 ]
do
klee --search=dfs test.bc
sleep 10
done
From the 306 results KLEE executed, the longest time is
76.88s(50.15%) and the
shortest is 41.89s(TSolver: 48.22%). *
So is it common?*
Also I notice that when using a zero-args version of
"main", the time will be
much less; is it because the function function call
"stack" or the
environment(but there is no posix-runtime here)?
Best regards,
Hongxu Chen
_______________________________________________
klee-dev mailing list
[email protected] <mailto:[email protected]>
https://mailman.ic.ac.uk/mailman/listinfo/klee-dev
_______________________________________________
klee-dev mailing list
[email protected]
https://mailman.ic.ac.uk/mailman/listinfo/klee-dev
_______________________________________________
klee-dev mailing list
[email protected]
https://mailman.ic.ac.uk/mailman/listinfo/klee-dev
