[isabelle-dev] Quickcheck Examples

[Lukas Bulwahn]

On 04/20/2012 02:12 PM, Lukas Bulwahn wrote:
> 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 
>>> 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"?
>>
> I have not noticed that non-termination on my laptop when checking my 
> changesets.
> Also with the setting mentioned above, I could not reproduce the 
> non-terminating behaviour on macbroy2 with changesets baf90cb2a606.
>
I was mistaken--I was checking with f5eaa7fa8d72.


Lukas