[isabelle-dev] Quickcheck Examples

[Makarius]

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_PLATFORM=x86_64-darwin
   ML_HOME=/home/polyml/polyml-5.4.1/x86_64-darwin
   ML_SYSTEM=polyml-5.4.1
   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"?


 	Makarius