[klee-dev] Non-determinism in KLEE
Cristian Cadar
c.cadar at imperial.ac.uk
Wed Nov 13 23:22:18 GMT 2013
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
> <paul.marinescu at imperial.ac.uk <mailto:paul.marinescu at imperial.ac.uk>>
> 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 <leftcopy.chx at gmail.com
> <mailto:leftcopy.chx at gmail.com>> 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
>> <leftcopy.chx at gmail.com <mailto:leftcopy.chx at gmail.com>> 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
>> <leftcopy.chx at gmail.com <mailto:leftcopy.chx at gmail.com>> 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
>> klee-dev at imperial.ac.uk <mailto: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
>
More information about the klee-dev
mailing list