Stream: Coq devs & plugin devs

Topic: Bench hardware


view this post on Zulip Janno (Oct 11 2023 at 12:55):

What kind of hardware are the benches running on? I just realized the reported timings are about 70% faster than what I can achieve locally.. and I thought my laptop was pretty fast

view this post on Zulip Gaëtan Gilbert (Oct 11 2023 at 13:00):

xeon E-2246G

view this post on Zulip Gaëtan Gilbert (Oct 11 2023 at 13:01):

it's a massive waste of cores as we run everything with -j 1 too

view this post on Zulip Janno (Oct 11 2023 at 13:05):

Thanks!

view this post on Zulip Janno (Oct 11 2023 at 13:08):

It seems I should be expecting a 20% difference on single thread workload. not 70%. Another mystery to investigate..

view this post on Zulip Gaëtan Gilbert (Oct 11 2023 at 13:09):

which timings are you looking at? eg the whole package or some particular commands?

view this post on Zulip Janno (Oct 11 2023 at 13:09):

https://coq.gitlabpages.inria.fr/-/coq/-/jobs/3485777/artifacts/_bench/html/coq-performance-tests-lite/src/pattern.v.html#L32

view this post on Zulip Janno (Oct 11 2023 at 13:10):

On master that line takes ~24s for me.

view this post on Zulip Janno (Oct 11 2023 at 13:13):

Actually, it might be closer to 22s. The results are quite noisy. Still, not close enough to ~13s on the bench runner.

view this post on Zulip Paolo Giarrusso (Oct 11 2023 at 13:14):

What's the source of the 20% figure, in what context is that, and does it account for caches and RAM speed?

view this post on Zulip Paolo Giarrusso (Oct 11 2023 at 13:16):

And does the bench server run at base clock (3.6GHz) or some boost clock (up to 4.8GHz)?

*https://www.intel.com/content/www/us/en/products/sku/191043/intel-xeon-e2246g-processor-12m-cache-3-60-ghz/specifications.html

view this post on Zulip Janno (Oct 11 2023 at 13:16):

It's from synthetic benchmarks. My laptop has a i7-9750H. I can't find anything super reliable but the usual suspects report a 20% overall difference, some saying that's single-threaded and some saying that's multi-threaded workloads.

view this post on Zulip Janno (Oct 11 2023 at 13:17):

The CPUs are from the same year, same node, both are coffee lake.. the only difference is the higher boost clock of 4.8 versus 4.5

view this post on Zulip Janno (Oct 11 2023 at 13:18):

And the power limit, obviously.. but I doubt they'd make it tight enough to kill single thread performance on the laptop part.

view this post on Zulip Janno (Oct 11 2023 at 13:19):

@Paolo Giarrusso I am curious, how long does that line take on your apple hardware? You can just copy the contents of the link above and put Time in front of the line 32.

view this post on Zulip Gaëtan Gilbert (Oct 11 2023 at 13:24):

about 16s on my laptop (i7-12700H) with master compiled with dune dev profile
but 13s with 8.17 compiled with release profile, and I don't think the change is because of the coq version

view this post on Zulip Janno (Oct 11 2023 at 13:25):

Oh, of course. I suppose the bench uses the release version?

view this post on Zulip Gaëtan Gilbert (Oct 11 2023 at 13:25):

yes

view this post on Zulip Janno (Oct 11 2023 at 13:35):

Okay, that explains everything. With the release profile I get roughly 14.5s which is well within the 20% estimate.

view this post on Zulip Janno (Oct 11 2023 at 13:37):

It might also explain why I often cannot replicate slowdowns from the bench results locally. If everything is already slow, a small slowdown could look even smaller in terms of percentages.

view this post on Zulip Janno (Oct 11 2023 at 13:40):

8.17 with the release profile is even faster at 13.7s.. unfortunately this also shows that I've been using an unoptimized build as my daily driver. My main coqtop binary takes 20s. :face_palm:

view this post on Zulip Janno (Oct 11 2023 at 13:50):

Maybe not.. it's just my custom OCAMLRUNPARAM settings I usually use. Okay, I guess that solves all the remaining questions.


Last updated: Oct 13 2024 at 01:02 UTC