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 performance.

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 mechanism).

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 Isabelle options.

The issue is complicated by the fact that I'm running Ubuntu in a VBox
virtual machine.

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 MHonArc.