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? 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) Many thanks! Best Regards, Hongxu Chen On Wed, Nov 13, 2013 at 1:45 PM, Paul Marinescu < [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]> 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]>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]>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] > https://mailman.ic.ac.uk/mailman/listinfo/klee-dev > > >
_______________________________________________ klee-dev mailing list [email protected] https://mailman.ic.ac.uk/mailman/listinfo/klee-dev
