The Coq mailing list

[Frédéric Blanqui <frederic.blanqui AT inria.fr>]

Hi Guillaume.

With /usr/bin/time make -j20, I get:

2017.92user 108.62system 8:14.59elapsed 429%CPU (0avgtext+0avgdata 
1850172maxresident)k
0inputs+607752outputs (0major+12904377minor)pagefaults 0swaps

Here are some information about my processors (they are all the same) 
and memory:

/proc/cpuinfo:

processor       : 0
vendor_id       : GenuineIntel
cpu family      : 6
model           : 62
model name      : Intel(R) Xeon(R) CPU E5-2620 v2 @ 2.10GHz
stepping        : 4
microcode       : 0x416
cpu MHz         : 1200.000
cache size      : 15360 KB
physical id     : 0
siblings        : 12
core id         : 0
cpu cores       : 6
apicid          : 0
initial apicid  : 0
fpu             : yes
fpu_exception   : yes
cpuid level     : 13
wp              : yes
flags           : fpu vme de pse tsc msr pae mce cx8 apic sep mtrr pge 
mca cmov pat pse36 clflush dts acpi mmx fxsr sse sse2 ss ht tm pbe 
syscall nx pdpe1gb rdtscp lm constant_tsc arch_perfmon pebs bts rep_good 
nopl xtopology nonstop_tsc aperfmperf eagerfpu pni pclmulqdq dtes64 
monitor ds_cpl vmx smx est tm2 ssse3 cx16 xtpr pdcm pcid dca sse4_1 
sse4_2 x2apic popcnt tsc_deadline_timer aes xsave avx f16c rdrand 
lahf_lm ida arat epb xsaveopt pln pts dtherm tpr_shadow vnmi 
flexpriority ept vpid fsgsbase smep erms
bogomips        : 4189.95
clflush size    : 64
cache_alignment : 64
address sizes   : 46 bits physical, 48 bits virtual
power management:

/proc/meminfo:

MemTotal:       32890420 kB
MemFree:        19477652 kB
Buffers:          947696 kB
Cached:          8147924 kB
SwapCached:            0 kB
Active:          8704684 kB
Inactive:        3104580 kB
Active(anon):    2714868 kB
Inactive(anon):    27356 kB
Active(file):    5989816 kB
Inactive(file):  3077224 kB
Unevictable:          32 kB
Mlocked:              32 kB
SwapTotal:       2097148 kB
SwapFree:        2097148 kB
Dirty:               356 kB
Writeback:             0 kB
AnonPages:       2713600 kB
Mapped:           277072 kB
Shmem:             28588 kB
Slab:            1269428 kB
SReclaimable:    1164600 kB
SUnreclaim:       104828 kB
KernelStack:        6864 kB
PageTables:        37732 kB
NFS_Unstable:          0 kB
Bounce:                0 kB
WritebackTmp:          0 kB
CommitLimit:    18542356 kB
Committed_AS:    6145288 kB
VmallocTotal:   34359738367 kB
VmallocUsed:      382708 kB
VmallocChunk:   34342167384 kB
HardwareCorrupted:     0 kB
AnonHugePages:   1640448 kB
HugePages_Total:       0
HugePages_Free:        0
HugePages_Rsvd:        0
HugePages_Surp:        0
Hugepagesize:       2048 kB
DirectMap4k:      123508 kB
DirectMap2M:     4014080 kB
DirectMap1G:    29360128 kB

I don't know how to interpret all this. Does this answer your questions?

Frédéric.


Le 25/01/2016 11:20, Guillaume Melquiond a écrit :
> On 25/01/2016 11:08, Frédéric Blanqui wrote:
> > Hello Guillaume.
> >
> > I know what you mention. That's why I precised "when using make -j20". I
> > have 24 processors on my computer. So, I don't think that it should be a
> > problem to use "-j20". In a previous version of CoLoR, I had the
> > following times:
> >
> > j  |
> > --------------------
> > 1  | 27'00"
> > 3  | 10'47"
> > 20|   6'45"
> >
> > So, you can see that it is really important for me to use -j20...
> Yet there must be a reason for the compilation to be 30% slower while
> Coq itself is only 5% slower. You didn't mention anything about the
> memory of your computer; I hope you have enough memory so that 20 Coq
> processes can run concurrently and do not have to be swapped out.
>
> One thing you could try first is to use the "time" command from your
> system rather than the one from your shell, so that we get the number of
> major and minor pagefaults. That would give us a hint about whether your
> compilation process is being I/O bound because of memory.
>
> Then you can also tell us how large the .vo files are between 8.4 and
> 8.5. It might be that Coq is producing .vo files so large that it
> actually brings your system down to its knees.
>
> Finally, you might have to use "perf"-like tools to discover what the
> operating system is busy doing. Indeed, while Coq is only 5% slower, the
> operating system is 25% slower in your tests, so it would be interesting
> to know what it is actually wasting time on.
>
> Best regards,
>
> Guillaume