On Thu, Nov 14, 2013 at 7:22 AM, Cristian Cadar <[email protected]>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 >> <[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
