Stream: Coq devs & plugin devs

Topic: new bench machines


view this post on Zulip Gaëtan Gilbert (Feb 10 2021 at 16:19):

say hello to ci-coq-01.sophia.inria.fr ci-coq-02.sophia.inria.fr ci-coq-03.sophia.inria.fr and ci-coq-04.sophia.inria.fr, our new bench machines
setup according to https://github.com/coq/coq/wiki/Benchmarking#setting-up-new-machines

view this post on Zulip Gaëtan Gilbert (Feb 10 2021 at 16:21):

they are pretty beefy https://ark.intel.com/content/www/us/en/ark/products/191043/intel-xeon-e-2246g-processor-12m-cache-3-60-ghz.html
with 62GB RAM

view this post on Zulip Gaëtan Gilbert (Feb 10 2021 at 16:23):

with all those threads it's kinda sad to run with -j 1, how much perturbation should we expect if we used parallel builds?

view this post on Zulip Enrico Tassi (Feb 10 2021 at 16:24):

Gaëtan Gilbert said:

with all those threads it's kinda sad to run with -j 1, how much perturbation should we expect if we used parallel builds?

I guess you can give it a try ;-)

view this post on Zulip Enrico Tassi (Feb 10 2021 at 16:25):

I think there is a way to compile each opam package with -j1 but compile more packages at the same time

view this post on Zulip Enrico Tassi (Feb 10 2021 at 16:26):

Max Memory Size (dependent on memory type) 128 GB

Are you sure you picked the right model?

view this post on Zulip Théo Zimmermann (Feb 10 2021 at 16:35):

It's a bit sad to think that lots of money were spent on adding 4 beefy machines for performance testing when what was actually requested (according to the pad I've seen about this) were average machines. For the same price, we could have bought more of them...

view this post on Zulip Enrico Tassi (Feb 10 2021 at 16:39):

I don't know how the specs were decided, be we can also use them for CI... (also 300$ CPU is not really much IMO)

view this post on Zulip Gaëtan Gilbert (Feb 10 2021 at 16:40):

Enrico Tassi said:

Max Memory Size (dependent on memory type) 128 GB

Are you sure you picked the right model?

?

view this post on Zulip Enrico Tassi (Feb 10 2021 at 16:42):

oops, I read 624GB... I'm really tired

view this post on Zulip Enrico Tassi (Feb 10 2021 at 16:42):

but I guess you mean 64 ;-)

view this post on Zulip Gaëtan Gilbert (Feb 10 2021 at 16:50):

htop says 62.6G, not sure what kind of G it is really

view this post on Zulip Gaëtan Gilbert (Feb 10 2021 at 16:51):

could be GiB

view this post on Zulip Guillaume Melquiond (Feb 10 2021 at 16:51):

If those are GPU-less computer, part of the memory is recycled as video RAM.

view this post on Zulip Enrico Tassi (Feb 10 2021 at 16:51):

it could be it, the GPU is integrated

view this post on Zulip Enrico Tassi (Feb 10 2021 at 16:52):

for a unit with no screen, 2G VGA buffer is even too much

view this post on Zulip Enrico Tassi (Feb 10 2021 at 16:52):

but maybe it's the minimum ;-)

view this post on Zulip Guillaume Melquiond (Feb 10 2021 at 16:52):

Yes, I should have said "external GPU".

view this post on Zulip Guillaume Melquiond (Feb 10 2021 at 16:54):

It is not just used for VGA. The compute units of the integrated GPU are actually using this RAM. So, the default allocation is usually quite high, otherwise all those compute units are wasted.

view this post on Zulip Gaëtan Gilbert (Feb 10 2021 at 16:57):

         _,met$$$$$gg.           ggilbert@ci-coq-01
      ,g$$$$$$$$$$$$$$$P.        OS: Debian 10 buster
    ,g$$P""       """Y$$.".      Kernel: x86_64 Linux 4.19.0-13-amd64
   ,$$P'              `$$$.      Uptime: 21d 4h 50m
  ',$$P       ,ggs.     `$$b:    Packages: 600
  `d$$'     ,$P"'   .    $$$     Shell: bash 5.0.3
   $$P      d$'     ,    $$P     CPU: Intel Xeon E-2246G @ 12x 4.546GHz [33.0°C]
   $$:      $$.   -    ,d$$'     GPU: mgadrmfb
   $$\;      Y$b._   _,d$P'      RAM: 373MiB / 64140MiB
   Y$$.    `.`"Y$$$$P"'
   `$$b      "-.__
    `Y$$
     `Y$$.
       `$$b.
         `Y$$b.
            `"Y$b._
                `""""

view this post on Zulip Guillaume Melquiond (Feb 10 2021 at 17:06):

I am speechless. I thought Matrox had long disappeared.

view this post on Zulip Guillaume Melquiond (Feb 10 2021 at 17:08):

But that means this is actually an external GPU.

view this post on Zulip Enrico Tassi (Feb 10 2021 at 17:09):

can you lspci ?

view this post on Zulip Guillaume Melquiond (Feb 10 2021 at 17:11):

and you might as well do lshw -c display

view this post on Zulip Gaëtan Gilbert (Feb 10 2021 at 17:17):

ggilbert@ci-coq-01:~$ lspci
00:00.0 Host bridge: Intel Corporation 8th Gen Core Processor Host Bridge/DRAM Registers (rev 07)
00:01.0 PCI bridge: Intel Corporation Skylake PCIe Controller (x16) (rev 07)
00:01.1 PCI bridge: Intel Corporation Skylake PCIe Controller (x8) (rev 07)
00:08.0 System peripheral: Intel Corporation Skylake Gaussian Mixture Model
00:12.0 Signal processing controller: Intel Corporation Cannon Lake PCH Thermal Controller (rev 10)
00:14.0 USB controller: Intel Corporation Cannon Lake PCH USB 3.1 xHCI Host Controller (rev 10)
00:14.2 RAM memory: Intel Corporation Cannon Lake PCH Shared SRAM (rev 10)
00:16.0 Communication controller: Intel Corporation Cannon Lake PCH HECI Controller (rev 10)
00:16.4 Communication controller: Intel Corporation Device a364 (rev 10)
00:17.0 SATA controller: Intel Corporation Cannon Lake PCH SATA AHCI Controller (rev 10)
00:1c.0 PCI bridge: Intel Corporation Cannon Lake PCH PCI Express Root Port (rev f0)
00:1c.1 PCI bridge: Intel Corporation Cannon Lake PCH PCI Express Root Port (rev f0)
00:1e.0 Communication controller: Intel Corporation Device a328 (rev 10)
00:1f.0 ISA bridge: Intel Corporation Device a309 (rev 10)
00:1f.4 SMBus: Intel Corporation Cannon Lake PCH SMBus Controller (rev 10)
00:1f.5 Serial bus controller [0c80]: Intel Corporation Cannon Lake PCH SPI Controller (rev 10)
02:00.0 RAID bus controller: LSI Logic / Symbios Logic MegaRAID SAS-3 3008 [Fury] (rev 02)
03:00.0 PCI bridge: PLDA Device be00 (rev 02)
04:00.0 VGA compatible controller: Matrox Electronics Systems Ltd. Integrated Matrox G200eW3 Graphics Controller (rev 04)
05:00.0 Ethernet controller: Broadcom Limited NetXtreme BCM5720 Gigabit Ethernet PCIe
05:00.1 Ethernet controller: Broadcom Limited NetXtreme BCM5720 Gigabit Ethernet PCIe
ggilbert@ci-coq-01:~$ sudo lshw -c display
  *-display
       description: VGA compatible controller
       product: Matrox Electronics Systems Ltd.
       vendor: Matrox Electronics Systems Ltd.
       physical id: 0
       bus info: pci@0000:04:00.0
       version: 04
       width: 32 bits
       clock: 66MHz
       capabilities: pm vga_controller bus_master cap_list rom
       configuration: driver=mgag200 latency=64 maxlatency=32 mingnt=16
       resources: irq:16 memory:90000000-90ffffff memory:91808000-9180bfff memory:91000000-917fffff memory:c0000-dffff

view this post on Zulip Enrico Tassi (Feb 10 2021 at 17:18):

04:00.0 VGA compatible controller: Matrox Electronics Systems Ltd. Integrated Matrox G200eW3 Graphics Controller (rev 04)

vintage?

view this post on Zulip Guillaume Melquiond (Feb 10 2021 at 17:18):

apparently, Matrox is selling its venerable GPU so that motherboard makers can directly embed it

view this post on Zulip Guillaume Melquiond (Feb 10 2021 at 17:22):

I guess that makes the most sold GPU ever, if it ends up on any server motherboard

view this post on Zulip Guillaume Melquiond (Feb 10 2021 at 17:22):

and I just checked; it is indeed what we have on our benchmark machine for Why3

view this post on Zulip Enrico Tassi (Feb 10 2021 at 17:25):

I guess there are CUPs out there with no GPU integrated (maybe not from intel) hence the 5cents GPU soldered in

view this post on Zulip Jason Gross (Feb 10 2021 at 18:49):

In case this is useful: If you're using the machines for benchmarking with multiple threads, you probably want to turn off hyperthreading (we have a convenience script to do this in fiat-crypto at https://github.com/mit-plv/fiat-crypto/blob/master/etc/hyperthreading.sh , in case it's of interest)

view this post on Zulip Emilio Jesús Gallego Arias (Feb 11 2021 at 00:07):

Last time I tried to do benches with -j2 noise was quite high, that was a while ago, but I used quite a bit of care. But indeed, timing / memory pressure etc... tend to have a big impact. But it is cool we have those large servers, we can repurpose one to full incremental CI for example which does require a lot of RAM

view this post on Zulip Emilio Jesús Gallego Arias (Feb 11 2021 at 00:08):

Regarding Matrox I'm surprised they still ship it indeed! It's been a while since I get my hand dirty with rackmountable servers, but last time, this is what Dell was using on their blades


Last updated: Oct 15 2021 at 20:02 UTC