[isabelle-dev] Max threads & Sledgehammer

Gottfried Barrow gottfried.barrow at gmx.com
Fri Jan 4 14:09:28 CET 2013

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


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.


More information about the isabelle-dev mailing list