[isabelle-dev] Quickcheck Examples
makarius at sketis.net
Mon Feb 27 14:31:55 CET 2012
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 deallocations.
> 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"?
More information about the isabelle-dev