Stream: Coq devs & plugin devs

Topic: new bench machines

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

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

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?

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 ;-)

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

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?

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...

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)

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?

?

Enrico Tassi (Feb 10 2021 at 16:42):

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

Enrico Tassi (Feb 10 2021 at 16:42):

but I guess you mean 64 ;-)

Gaëtan Gilbert (Feb 10 2021 at 16:50):

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

Gaëtan Gilbert (Feb 10 2021 at 16:51):

could be GiB

Guillaume Melquiond (Feb 10 2021 at 16:51):

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

Enrico Tassi (Feb 10 2021 at 16:51):

it could be it, the GPU is integrated

Enrico Tassi (Feb 10 2021 at 16:52):

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

Enrico Tassi (Feb 10 2021 at 16:52):

but maybe it's the minimum ;-)

Guillaume Melquiond (Feb 10 2021 at 16:52):

Yes, I should have said "external GPU".

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.

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._
                `""""

Guillaume Melquiond (Feb 10 2021 at 17:06):

I am speechless. I thought Matrox had long disappeared.

Guillaume Melquiond (Feb 10 2021 at 17:08):

But that means this is actually an external GPU.

Enrico Tassi (Feb 10 2021 at 17:09):

can you lspci ?

Guillaume Melquiond (Feb 10 2021 at 17:11):

and you might as well do lshw -c display

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

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?

Guillaume Melquiond (Feb 10 2021 at 17:18):

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

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

Guillaume Melquiond (Feb 10 2021 at 17:22):

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

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

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)

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

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: May 28 2023 at 13:30 UTC