Stream: Mirror: Isabelle Users Mailing List

Topic: [isabelle] Isabelle Performance Benchmark

view this post on Zulip Email Gateway (Feb 10 2022 at 07:33):

From: Fabian Huch <huch@in.tum.de>
Thanks for all the participation so far. Results are accumulated and
visualized in the spreadsheet [1]. If you want to see more details,
there are separate sheets in that document for the calculation.

Notably, the 12th generation Intel cores seem to do quite well on
desktop (<2 min), and the Apple M1 Pro for laptops (2:45). Performance
is generally best for 8-16 cores.

One more thing: Disabling Hyper-Threading can improve performance by a
lot (thanks @Ian Hayes). If you can disable that on your system,
re-running the benchmark and posting your results again (suffixing the
CPU name with ' w/o HT') would be insightful.

Fabian

[1]:
https://docs.google.com/spreadsheets/d/12GhEwSNSopowDBq5gSem3u39fliiIcoTIZHMnX4RE3A

view this post on Zulip Email Gateway (Feb 10 2022 at 08:22):

From: Mathias Fleury <mathias.fleury12@gmail.com>
Hi Fabian,

Thanks for starting that, the results are interesting.

I add a question on the 12th-generation-Intel test: do you know if that
test was with DDR4 or DDR5 memory?

Thanks,

Mathias

view this post on Zulip Email Gateway (Feb 10 2022 at 08:53):

From: Fabian Huch <huch@in.tum.de>
DDR5 memory.

Fabian

view this post on Zulip Email Gateway (Feb 10 2022 at 10:39):

From: Makarius <makarius@sketis.net>
Apple M1 is ARM64, but for Isabelle2021-1 this iron is used indirectly via
Rosetta 2 Intel-to-ARM translation.

Here is an updated test version of Poly/ML with a fairly good native ARm64
code generator:
https://isabelle.in.tum.de/components/polyml-test-15c840d48c9a.tar.gz

That needs to replace the bundled contrib/polyml-5.9 in Isabelle2021-1.

Makarius

view this post on Zulip Email Gateway (Feb 24 2022 at 16:31):

From: Fabian Huch <huch@in.tum.de>

I would be particularly interested in results for the recent AMD Epyc
Milan series (e.g. 7302 @ 3.00 GHz, 16 Cores).

Unfortunately nobody seems to have one available, but based on the
results we have so far I predict between 4:10 and 5:20 for the Epyc 7543
on 8 threads (based on a regression on cpu benchmark scores).

Fabian

Last updated: Jan 04 2025 at 20:18 UTC