[isabelle-dev] Quickcheck Examples
bulwahn at in.tum.de
Fri Apr 20 14:12:05 CEST 2012
On 02/27/2012 02:31 PM, Makarius wrote:
> On Mon, 27 Feb 2012, Lukas Bulwahn wrote:
>> A large part of Quickcheck's run time is spent in the code generator
>> calls, and the evaluation, which does mostly memory allocations and
>> I am surprised that this issue suddenly occurs now that it is its own
>> session. Maybe the many parallel invocations of Quickcheck now
>> pressure the ML compiler much more than as it was just a part of HOL-ex.
> In principle the codegen infrastructure and all should work in
> parallel, but there might be additional oddities in the quickcheck
> scenario. You can reproduce the presumed non-termination on macbroy2
> with regular settings like this:
> ISABELLE_USEDIR_OPTIONS=-i false -d false -M 4 -q 2
> ML_OPTIONS=-H 1000 --gcthreads 4
> The process is running with approx. 100-200% most of the time, which
> is neither sequential nor fully parallel. Probably you merely benefit
> from theory parallelism, not from more fine-grained Par_List things
> that could be used in your own code.
> One potential source of problems is the pseudo-random generator, with
> its global state. There have been funny effects in the past that
> might have come back in one form or the other, even though random
> generators have been changed several times.
> Anyway, how long does the session run on "your laptop"?
I have not noticed that non-termination on my laptop when checking my
Also with the setting mentioned above, I could not reproduce the
non-terminating behaviour on macbroy2 with changesets baf90cb2a606.
I will continue testing Quickcheck-Examples to see if it only occurs
Can you other system configurations by running the isatest with the
More information about the isabelle-dev