[isabelle-dev] Max threads & Sledgehammer
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".
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