Re: [isabelle] Isabelle2015-RC0 available for testing



On Mon, 20 Apr 2015, Jasmin Blanchette wrote:

On 20.04.2015, at 16:19, C. Diekmann <diekmann at in.tum.de> wrote:

Incidentally, this behavior of Sledgehammer is nothing new. Is the issue really new with Isabelle2015-RC0? What happens if you write

  ML {* Multithreading.max_threads_value () *}

in Isabelle2014 vs. Isabelle2015-RC0?

Both report "2". I have a dual core cpu with 2 physical cores and
thanks to hyperthreading two additional virtual cores. /proc/cpuinfo
lists 4 processors.

Then I presume Sledgehammer also invoked only two ATPs in Isabelle2014?

Irrespective of this, you probably want to check the Isabelle system manual to find out how to change the number of threads. 2 is perhaps needlessly low.

This nominal number of ML threads is critical for overall system performance. CPUs today usually have much more virtual hardware threads than actual CPU cores (due to Intel hyperthreading and similar AMD technology). Asking the system about the CPU number in old-fashioned ways leads to a number of threads that maximizes CPU cycle burning, without much gain of performance, often a loss of it. CPU cycle burning is particularly bad on mobile devices.

This also explains why PIDE was often perceived as unbearably slow in the past: the defaults were not right, and most users did not know how to tune the Harley Davidson themselves.

David Matthews has already provided more refined CPU query operations for the Poly/ML runtime system already for Isabelle2014. It should be mostly the same for Isabelle2015-RC1. This means the default Multithreading.max_threads_value is the preferred one for most purposes.


Generally, the threads number should be just a matter of performance, and not of change of semantics.

My impression is that the auto-adaptive mode of the slegehammer command is coming from a time when there was still a TTY loop and at most one command active, so one could rely on all threads being free, before starting the next command. Now many things can be active all the time, and the thread pool continuously busy with many different tasks.


	Makarius




This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.