[isabelle-dev] Max threads & Sledgehammer

[Gottfried Barrow]

On 1/4/2013 6:37 AM, Jasmin Blanchette wrote:
> Hi Makarius,
>
> Change cb5cdbb645cd ("clarified bootstrapping of Pure") altered the semantics of
>
>      Multithreading.max_threads_value ()
>
> with Poly/ML. Namely, all of a sudden the function returns 1 instead of 4 on a 4-CPU machine, which seems strage as a default for a function called "max_threads_value". As a result, Sledgehammer launches only one local thread -- see "avoid_too_many_threads" and its use in "src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML". SPASS is then no longer run at all.
>
> This has been like this for some time now. I failed to notice the issue because I had overwritten the number of threads via a Proof General setting.
>
> This really needs to be fixed before the release -- either in "multithreading_polyml.ML" or in "sledgehammer_isar.ML".
>
> Cheers,
>
> Jasmin

Jasmin,

So far I've managed to stay out of the development list, but this ties 
into what I saw in the past in my experiments with Sledgehammer, and how 
many ATPs it would launch at a time, which was a maximum of four even 
though an i7 has 8 virtual cores, and 8 graphs are displayed on an i7 by 
my CPU monitor and process monitor.

I actually don't have the i7 notebook anymore, but for the dual-core i3 
notebook I use, it shows 4 cores, since for an i3 there are two virtual 
cores for each physical core.

First, I don't care what happens here, but I bring it up because it's 
ingrained in us to always want more.

So, if possible, it would be nice if Sledgehammer would lanuch 8 ATPs on 
a quad core i7, since there are 8 virtual cores. I guess that would be 
nice. It seems like it would be possible. The CPU gets maxed out when 
running four ATPs, but if I run 15 ATPs on one theorem, some ATPs will 
finish fast, and some won't, so running more in parallel can sometimes 
help get information back faster.

Regards,
GB