[klee-dev] Non-determinism in KLEE
Hongxu Chen
leftcopy.chx at gmail.com
Thu Nov 14 02:47:12 GMT 2013
On Thu, Nov 14, 2013 at 7:22 AM, Cristian Cadar <c.cadar at imperial.ac.uk>wrote:
> 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"
>
> Thanks for explaination, and sorry for my ignorance.
>
> 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.
>
> I'll read the code and think about it carefully. Thanks so much for
pointing out that!
> 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
>>
>>
-------------- next part --------------
HTML attachment scrubbed and removed
More information about the klee-dev
mailing list