Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] Isabelle/jEdit and hyperthreading

Email Gateway (Aug 22 2022 at 10:26):

From: Matthew Fernandez <matthew.fernandez@nicta.com.au>
Hi,

Isabelle/jEdit has an option to configure the number of threads in use for parallel proofs:
Plugins > Plugin options > Isabelle > General > Parallel processing > Threads

By default, this is set to 0 which indicates the "hardware max." I find on machines with hyperthreading, this means the
number of physical cores, not the number of logical hardware threads. E.g. on a machine I have here with 2 hyperthreaded
cores, Isabelle/jEdit appears to use 2 threads when I would prefer 4. I realise I can set this manually, but I was
wondering if the default behaviour is deliberate? Perhaps the assumption is that the shared resources on the cores are
kept busy enough by Isabelle that the extra threads won't help. I'm just asking out of curiosity, more than anything
else. The host environment is 64-bit Linux by the way.

Thanks,
Matt

The information in this e-mail may be confidential and subject to legal professional privilege and/or copyright. National ICT Australia Limited accepts no liability for any damage caused by this email or its attachments.

Email Gateway (Aug 22 2022 at 10:26):

From: Harry Butterworth <heb1001@gmail.com>
I think the behaviour has changed between 2014 and 2015 as 2014 used to use
100% of CPU with hyperthreading turned on and 2015 now peaks only just
above 50%.

I've been running with hyperthreading disabled in the BIOS anyway as I did
some benchmarking (using run_tests from seL4) with 2014 and the fastest
configuration I found (for my x5680) was with hyperthreading disabled.
Some of the tests were a bit faster at the same clock speed with
hyperthreading disabled but the main benefit was that by disabling
hyperthreading I could run with a higher clock speed for the same CPU
temperature at max load.

I also benchmarked the difference between speedstep on and off (on an i7
5820k this time) and see a 10% improvement by turning speedstep off which
will be useful in the winter when I need a heater.

Email Gateway (Aug 22 2022 at 10:27):

From: Matthew Fernandez <matthew.fernandez@nicta.com.au>
On 29/06/15 14:22, Harry Butterworth wrote:

I think the behaviour has changed between 2014 and 2015 as 2014 used to use 100% of CPU with
hyperthreading turned on and 2015 now peaks only just above 50%.

I've been running with hyperthreading disabled in the BIOS anyway as I did some benchmarking (using
run_tests from seL4) with 2014 and the fastest configuration I found (for my x5680) was with
hyperthreading disabled. Some of the tests were a bit faster at the same clock speed with
hyperthreading disabled but the main benefit was that by disabling hyperthreading I could run with a
higher clock speed for the same CPU temperature at max load.

I also benchmarked the difference between speedstep on and off (on an i7 5820k this time) and see a
10% improvement by turning speedstep off which will be useful in the winter when I need a heater.

Thanks, Harry, informative to hear your results. I don't have the same processor, but I suspect mine
behaves the same in limiting the clock frequency with hyperthreading enabled. I don't want to
disable it or speedstep, so I'll just live with my current setup.

On 29 Jun 2015 09:08, "Matthew Fernandez" <matthew.fernandez@nicta.com.au
<mailto:matthew.fernandez@nicta.com.au>> wrote:

Hi,

Isabelle/jEdit has an option to configure the number of threads in use for parallel proofs:
Plugins > Plugin options > Isabelle > General > Parallel processing > Threads

By default, this is set to 0 which indicates the "hardware max." I find on machines with
hyperthreading, this means the
number of physical cores, not the number of logical hardware threads. E.g. on a machine I have
here with 2 hyperthreaded
cores, Isabelle/jEdit appears to use 2 threads when I would prefer 4. I realise I can set this
manually, but I was
wondering if the default behaviour is deliberate? Perhaps the assumption is that the shared
resources on the cores are
kept busy enough by Isabelle that the extra threads won't help. I'm just asking out of
curiosity, more than anything
else. The host environment is 64-bit Linux by the way.

Thanks,
Matt

________________________________

The information in this e-mail may be confidential and subject to legal professional privilege
and/or copyright. National ICT Australia Limited accepts no liability for any damage caused by
this email or its attachments.

The information in this e-mail may be confidential and subject to legal professional privilege and/or copyright. National ICT Australia Limited accepts no liability for any damage caused by this email or its attachments.

Last updated: Apr 26 2024 at 16:20 UTC