Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] Intel Core i9


view this post on Zulip Email Gateway (Aug 22 2022 at 18:01):

From: Tobias Nipkow <nipkow@in.tum.de>
I have recently upgraded from a Mac Book Pro with 2.9 GHz Intel Core i7 to a new
Mac Book Pro with 2.9 GHz Intel Core i9. When building HOL-Analysis o both
laptops, the times look like this:

i9:
Finished HOL-Analysis (0:05:24 elapsed time, 0:23:12 cpu time, factor 4.29)
i7:
Finished HOL-Analysis (0:05:32 elapsed time, 0:18:09 cpu time, factor 3.28)

This is at least surprising because it seems to suggest that the individual i9
cores are significantly slower than the fewer i7 cores. I have not fixed the
number of threads in the build options (except ML_OPTIONS --gcthreads 4).

Any ideas?

Tobias
smime.p7s

view this post on Zulip Email Gateway (Aug 22 2022 at 18:01):

From: Julian <parsert.julian@gmail.com>
I recall reading a news article saying that this is a known issue with
the new Apple devices and the i9 processors.

Julian
pEpkey.asc

view this post on Zulip Email Gateway (Aug 22 2022 at 18:01):

From: Jeremy Dawson <Jeremy.Dawson@anu.edu.au>
Hi Tobias,

Weird things happen.

When I first got a 4-core machine, one benchmark took 5 secs with all
but one core disabled, 20+ secs using more than one.

Then when I doubled the amount of memory, it ran better on 2 cores (7
secs) but 26 secs using 4 cores.

No-one could explain this with any confidence.

This was on Linux, where it seems you can disable core N by

echo 0 > /sys/devices/system/cpu/cpuN/online

(other benchmarks behaved sensibly)

May be worth trying to detect peculiar effects!

Cheers,

Jeremy

view this post on Zulip Email Gateway (Aug 22 2022 at 18:01):

From: Makarius <makarius@sketis.net>
On 20.08.2018 14:20, Tobias Nipkow wrote:

I have recently upgraded from a Mac Book Pro with 2.9 GHz Intel Core i7
to a new Mac Book Pro with 2.9 GHz Intel Core i9. When building
HOL-Analysis o both laptops, the times look like this:

i9:
Finished HOL-Analysis (0:05:24 elapsed time, 0:23:12 cpu time, factor 4.29)
i7:
Finished HOL-Analysis (0:05:32 elapsed time, 0:18:09 cpu time, factor 3.28)

This is at least surprising because it seems to suggest that the
individual i9 cores are significantly slower than the fewer i7 cores.

I can't say anything about potential problems of current Apple product
lines. Decline can certainly happen here.

In general, Intel "i3", "i5", "i7", and now "i9" are merely labels for
product lines and price classes, and higher numbers here are not
necessarily better. I depends on many other parameters, including cache
sizes and memory speed.

Comparison of Intel CPUs requires a precise identification according to
the database, e.g.
https://ark.intel.com/products/134903/Intel-Core-i9-8950HK-Processor-12M-Cache-up-to-4_80-GHz

I have not fixed the number of threads in the build options (except
ML_OPTIONS --gcthreads 4).

There is rarely a need to touch --gcthreads these days. The normal
Isabelle system option in "isabelle build -o threads=N" adjusts both the
ML user threads and the GC threads, if ML_OPTIONS leaves this unspecified.

Makarius

view this post on Zulip Email Gateway (Aug 22 2022 at 18:01):

From: Richard Waldinger <waldinger@AI.SRI.COM>
did you try putting your laptop in freezer? i have heard rumors that new apple products slow down in case of overheating.

view this post on Zulip Email Gateway (Aug 22 2022 at 18:01):

From: Tobias Nipkow <nipkow@in.tum.de>
Strangely enough, I didn't. I would also hate to work in a freezer myself ;-)

Seriously, the two laptops ran side by side in a reasonably cool office.

Tobias
smime.p7s

view this post on Zulip Email Gateway (Aug 22 2022 at 18:01):

From: Tobias Nipkow <nipkow@in.tum.de>
Some other people sent me links to an update of the OS that should fix this
problem but as far as we can tell, I have that update already.

Thanks
Tobias
smime.p7s

view this post on Zulip Email Gateway (Aug 22 2022 at 18:02):

From: "Achim D. Brucker" <brucker@spamfence.net>
Hi,
(Disclaimer: I am not an Apple user, i.e., reading my crystal ball combined
with news sites ...)

Could this issue be related to the throttling issue of recent
MacBook Pros:

https://venturebeat.com/2018/07/24/apple-addresses-macbook-pro-core-i9-throttling-with-software-update/

If yes, the "macOS High Sierra 10.13.6 Supplemental Update”
should relieve (some of) the pain.

Best,
Achim

view this post on Zulip Email Gateway (Aug 22 2022 at 18:18):

From: Lawrence Paulson <lp15@cam.ac.uk>
In case it's useful, here's what I got for my Mac Pro (Late 2013), 3.5 GHz 6-Core Intel Xeon E5:

Finished HOL-Analysis (0:05:01 elapsed time, 0:22:22 cpu time, factor 4.46)

I am using

ML_OPTIONS="-H 4000"

Previously I included --maxheap 8G, but got the error message "Value of --maxheap option is too large".

Larry
signature.asc

view this post on Zulip Email Gateway (Aug 22 2022 at 18:20):

From: Tobias Nipkow <nipkow@in.tum.de>
Now that it has become cooler again, I actually built HOL-Analysis outside, and
it ran 20% faster!

Finished HOL-Analysis (0:04:29 elapsed time, 0:20:32 cpu time, factor 4.58)

So my laptop does have a temperature problem. Quite a severe one, actually. I
took it inside again and built HOL-Analysis once more and

...
HOL-Analysis: theory HOL-Analysis.Analysis
Warning - Unable to increase stack - interrupting thread
*** Interrupt
HOL-Analysis FAILED

Maybe a fluke? I take the laptop outside again, everything works. I build it
inside and again, FAILED.

It seems high time I changed manufacturer. Unless I really want work in a freezer.

Tobias
smime.p7s

view this post on Zulip Email Gateway (Aug 22 2022 at 18:25):

From: Lawrence Paulson <lp15@cam.ac.uk>
That is certainly weird! I have a 2012 vintage MacBook Pro (not with retina display) and I sometimes had temperature problems, especially if I used it on a hotel room bed, which impedes its internal ventilation. It could get too hot to touch and would shut down automatically. But I never got you are getting.

Larry
signature.asc

view this post on Zulip Email Gateway (Aug 22 2022 at 18:25):

From: Richard Waldinger <waldinger@AI.SRI.COM>
i heard it was a known feature that new Mac laptops slow down to avoid overheating.

view this post on Zulip Email Gateway (Aug 22 2022 at 18:26):

From: Ching-Tsun Chou <chingtsun.chou@gmail.com>
You may want to check out this:

https://software.intel.com/en-us/articles/intel-power-gadget-20

It gives you useful real-time information about your Intel CPU.


Last updated: Apr 24 2024 at 04:17 UTC