The Coq mailing list

["Soegtrop, Michael" <michael.soegtrop AT intel.com>]

Dear Andrew,

 

you might be interested in this documentation from Microsoft:

 

https://msdn.microsoft.com/en-us/library/aa366778.aspx

 

Essentially it is a linker option if 32 bit binaries on 64 bit Windows support 2GB or 4GB user virtual address space. I don’t know if OCaml makes any hacky use of the fact that the top bit of pointers tend to be 0 on 32 bit Windows – probably not because this wouldn’t be the case on Linux or 64 bit Windows. In order to try it, you can patch the IMAGE_FILE_LARGE_ADDRESS_AWARE flag of the coqc binary and see what happens. I don’t think the OCaml linker has an option to do this, but if it proves to be useful use, one could request it – shouldn’t be a big deal. Of cause it is also a good question what OCaml does with the extra memory: not use it at all / split it half half or give all extra to the heap.

 

One more note: the difference is likely larger on machines with more cores (or a worse cache size / core count ratio). The dual socket Xeon servers I am currently using  have 2x (22 cores=44 threads and 55 MB cache), so in total 88 threads and 110MB cache. I think latest Xeons even have a bit more.

 

And I have a question: do you also make substantial use of parallelism in one coqc call (parallel proofs and/or parallel branches in one proof) or did you find that it is more optimal to run each coqc instance single threaded on a single core because the in file parallelism can have substantial peaks and lead to bad load balancing? Do you use different settings for batch and interactive mode?

 

Best regards,

 

Michael

Intel Deutschland GmbH
Registered Address: Am Campeon 10-12, 85579 Neubiberg, Germany
Tel: +49 89 99 8853-0, www.intel.de
Managing Directors: Christin Eisenschmid, Christian Lamprechter
Chairperson of the Supervisory Board: Nicole Lau
Registered Office: Munich
Commercial Register: Amtsgericht Muenchen HRB 186928