[Caml-list] Decrease in addressable memory on Windows 32-bits between 3.12 and 4.01?

[Caml-list] Decrease in addressable memory on Windows 32-bits between 3.12 and 4.01?

[Pierre-Marie Pédrot]

[-- Attachment #1: Type: text/plain, Size: 1399 bytes --]

Hello caml-list,

We Coq developers were given a fancy bug report by Andrew Appel
regarding Coq 8.5 memory usage that spawned quite a lot of distinct
discussions related to several performance issues. Although most of them
were solved, there is one which I believe is not due to Coq but rather
to OCaml. Here is the issue.

> Can I ask you all about my observation that max memory available in 
> 32-bit Coq 8.5 is less than max memory available in 32-bit Coq 
> 8.4pl6?  (The 2nd-to-last paragraph of my original bug report.)
> 
> That is, run Coq 8.4pl6 in a 32-bit Windows binary, on some script 
> that takes many gigabytes to process, and see what is the maximum 
> memory usage is before it dies. It should be about 2048 megabytes. 
> Then run the same script in Coq 8.5 32-bit Windows binary, and 
> measure the same.  In the case of bug 4547, it was 1848 MB.  Can the 
> same disparity be measured under Linux?  What is causing Coq to lose 
> the use of the last 200MB of a 31-bit address space?

Note that

> Coq 8.5 is compiled with 4.01 on windows.  Coq 8.4 was compiled with
> 3.12 IIRC.

so I am led to think that this has to do with OCaml runtime, as I can't
really see where this would come from the Coq codebase.

What do you OCaml experts think about this? Has there been some change
in the runtime that could explain this problem?

Thanks,
PMP



[-- Attachment #2: OpenPGP digital signature --]
[-- Type: application/pgp-signature, Size: 819 bytes --]

Re: [Caml-list] Decrease in addressable memory on Windows 32-bits between 3.12 and 4.01?

[Enrico Tassi]

On Mon, Feb 15, 2016 at 10:59:25AM +0100, Pierre-Marie Pédrot wrote:
> > Coq 8.5 is compiled with 4.01 on windows.  Coq 8.4 was compiled with
> > 3.12 IIRC.
> 
> so I am led to think that this has to do with OCaml runtime, as I can't
> really see where this would come from the Coq codebase.

One bit of info that may be relevant.
Coq 8.5 sets different Gc parameters, in particular a larger minor heap size.

My2C
-- 
Enrico Tassi

Re: [Caml-list] Decrease in addressable memory on Windows 32-bits between 3.12 and 4.01?

[Xavier Leroy]

On 15/02/2016 10:59, Pierre-Marie Pédrot wrote:

>> Can I ask you all about my observation that max memory available in 
>> 32-bit Coq 8.5 is less than max memory available in 32-bit Coq 
>> 8.4pl6?  (The 2nd-to-last paragraph of my original bug report.)
[...]
>> Coq 8.5 is compiled with 4.01 on windows.  Coq 8.4 was compiled with
>> 3.12 IIRC.
> 
> so I am led to think that this has to do with OCaml runtime, as I can't
> really see where this would come from the Coq codebase.

For the reasons that Enrico mentioned, it could come from the Coq code
base, so it would be best to use the same version of Coq to investigate
this issue.

This could be related to http://caml.inria.fr/mantis/view.php?id=6990
or not.  (I don't know whether the heap growing policy changed between
OCaml 3.12 and OCaml 4.01).

It's helpful to run with OCAMLRUNPARAM=v=4 to monitor how much memory
OCaml requests from the OS and at which points in program execution.

- Xavier Leroy