Re: [isabelle] sledgehammer in RC4
On Thu, 14 Nov 2013, Randy Pollack wrote:
I'm not sure if it is useful or harmful to count the hyperthreads
(double the number of real cores). The host OS (OSX or Windows or
Linux) can see the difference between cores and hyperthreads, and
hopefully schedules accordingly (i.e. distributes threads to different
cores before using a hyperthread on a core already running).
This confusion of real cores vs. hyperthreaded virtual cores will probably
entertain the computing industry for a few more years. My experience is
that (1) the OSes today are smart enough to schedule threads for real
cores first and (2) the additional virtaul cores actually help a bit with
On my old 8 core Xeon * hyperthreading system (2009), I can get a true
factor of 9.6 in the best possible situation. That extra burning of CPU
cycles consumes quite a lot of energy, though. Users of mobile systems
should make sure that they don't overload the CPU unneccessary.
Isabelle provides a global system option "threads" for that (both for
Isabelle/Scala/jEdit and in Proof General via its own elips-based
Moreover, the Poly/ML settings can be fine-tuned in
$ISABELLE_HOME_USER/etc/settings like this:
ML_OPTIONS="-H 500 --gcthreads 4"
Further tuning might be required to make the JVM run smoothly on a given
system -- this is relevant for Isabelle/Scala and the PIDE front-ends.
Modern hardware requires considerable manual tuning to get the best
performance vs. energy consumption ratio.
I've heard occasionally complaints about too much burning of cycles, by
people who did not look at any of their hardware specifications nor the
The issue is complicated by the fact that I'm running Ubuntu in a VBox
What is your host platform then? Since Isabelle claims to support all
major OSes routinely, I am always interested to see counterexamples.
(Android will not work, though.)
This archive was generated by a fusion of
Pipermail (Mailman edition) and