On Wed, Sep 1, 2010 at 10:15 AM, Cristian Cadar <c.cadar at imperial.ac.uk> wrote: > > Hi Denis, > > The non-deterministic behavior that you see in your runs is most likely > caused by the addresses returned by malloc(). ?I think there was a > previous thread on the list which discussed possible solutions to this, > let me know if you have trouble finding it in the archives.
This isn't actually likely to be a huge problem, depending on the platform. In most situations, the addresses returned from malloc() are deterministic as long as address space randomization and such is not in place. I recommend trying to disable as much of that stuff as you can if you care strongly about determinism. There are two major sources of non-determinism related to using OS timing information to make decisions. The first uses timing information about queries to prioritize the search. Since that information isn't deterministic, the search strategy can quickly diverge even if all other sources of non-determinism are eliminated. The other source is the options to terminate the STP queries after a certain amount of time. It is possible that some queries will be right on the border and will fail in some runs and pass in others, which would be a major divergence. This is very unfortunate as those options are very important for testing most large applications. The two sources above can both be avoided by not using particular options, so I guess the first goal is determining whether you can get KLEE to be behave deterministically without those problems. - Daniel > Best, > Cristian > > On 01/09/10 16:37, Bueno, Denis wrote: >> Hello, >> >> I'm trying to run some tests in Klee and I'd like to be able to get >> deterministic runs of Klee. ?I think I've found all relevant sources of >> non-determinism, and it appears to me that Klee should run >> deterministically, but it doesn't. ?Essentially, I've verified that srand, >> srandom, and other pseudo-random seeds are all constant. >> >> What are the other sources of non-determinism? ?Is it easy to remove them >> and stick with pseudo-randomness? >> >> Thanks. >> >> -Denis >> _______________________________________________ >> klee-dev mailing list >> klee-dev at keeda.stanford.edu >> http://keeda.Stanford.EDU/mailman/listinfo/klee-dev > _______________________________________________ > klee-dev mailing list > klee-dev at keeda.stanford.edu > http://keeda.Stanford.EDU/mailman/listinfo/klee-dev >
