From mboxrd@z Thu Jan 1 00:00:00 1970 Return-Path: X-Original-To: caml-list@sympa.inria.fr Delivered-To: caml-list@sympa.inria.fr Received: from mail2-relais-roc.national.inria.fr (mail2-relais-roc.national.inria.fr [192.134.164.83]) by sympa.inria.fr (Postfix) with ESMTPS id 6275B7FCD9 for ; Mon, 15 Feb 2016 10:59:33 +0100 (CET) X-IronPort-AV: E=Sophos;i="5.22,449,1449529200"; d="asc'?scan'208";a="203137740" Received: from ron.emn.fr (HELO [172.28.3.27]) ([193.54.76.162]) by mail2-relais-roc.national.inria.fr with ESMTP/TLS/DHE-RSA-AES128-SHA; 15 Feb 2016 10:59:33 +0100 To: caml-list@inria.fr From: =?UTF-8?Q?Pierre-Marie_P=c3=a9drot?= X-Enigmail-Draft-Status: N1110 Message-ID: <56C1A17D.9020902@inria.fr> Date: Mon, 15 Feb 2016 10:59:25 +0100 User-Agent: Mozilla/5.0 (X11; Linux x86_64; rv:38.0) Gecko/20100101 Icedove/38.5.0 MIME-Version: 1.0 Content-Type: multipart/signed; micalg=pgp-sha256; protocol="application/pgp-signature"; boundary="6P5A9FWlLr7GoN4Oc2v79S72Oei30sl6C" Subject: [Caml-list] Decrease in addressable memory on Windows 32-bits between 3.12 and 4.01? This is an OpenPGP/MIME signed message (RFC 4880 and 3156) --6P5A9FWlLr7GoN4Oc2v79S72Oei30sl6C Content-Type: text/plain; charset=utf-8 Content-Transfer-Encoding: quoted-printable 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=20 > 32-bit Coq 8.5 is less than max memory available in 32-bit Coq=20 > 8.4pl6? (The 2nd-to-last paragraph of my original bug report.) >=20 > That is, run Coq 8.4pl6 in a 32-bit Windows binary, on some script=20 > that takes many gigabytes to process, and see what is the maximum=20 > memory usage is before it dies. It should be about 2048 megabytes.=20 > Then run the same script in Coq 8.5 32-bit Windows binary, and=20 > measure the same. In the case of bug 4547, it was 1848 MB. Can the=20 > same disparity be measured under Linux? What is causing Coq to lose=20 > 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 --6P5A9FWlLr7GoN4Oc2v79S72Oei30sl6C Content-Type: application/pgp-signature; name="signature.asc" Content-Description: OpenPGP digital signature Content-Disposition: attachment; filename="signature.asc" -----BEGIN PGP SIGNATURE----- Version: GnuPG v2 iQIcBAEBCAAGBQJWwaF9AAoJEHkiwB/Zujx7zVEP/1sGz2nsRrhpJuKD7cNBVZWK gudHaxfFutvXW9ethtaowb4HHjf0eAhaJfiaxT7+/Iz8I6jJnSO+qyoqPHte5W1q OdTQKB4MvrlRMEVT9QHXxBWu56+35+3qxunmBvXtJREhzrAVD66j2llWWpBmSTcf W5YJBn6tqnfvbyHalEi3biQbyMefq/jmVkvHn6q8gNxv4mP4K1WnE/4a6+m6MGCS hJC5Q3vp/Jsfabgled24blnhLSAkSn7WtEXdeQlg8zLcA/skzZA7/wFxNwM8yDgR ipElCcK2PTo3VSE2DHXumYZF4j+dqwy2dlCLDqJNcLHS8fCXVuMClcURrCspD0SU grzryWVVt1s3ZhnaxNFEEalmEm8KVTN2qStzFERjnflBbSvdFGKm3Rh7uc3AGilF MXf/ig4TUAUfAjEGCFmkhiQTaUZjF9agZVgj5i4rz86RniT4GINL4UDb9T+63qjR sRjKCZSxirxN/WKk1XvibnwdaHrUVD7PJewXuGCXqQ19BW0VxfFXCPknuM66/0uQ 20AIguCu4YyJZGb2Dc9s8aKdcnd/DDDR1yHTqJyL+J4kNOy21ujwBGhGs9nmJERB UOu6DEmvSJ/WHdXKKZcDYugcfbjJQ0SnQ1ATSaUCgSfOql2egMy3Z4qmyxMf/rem 86rUN5Dey/djx/8sbeLV =IdO3 -----END PGP SIGNATURE----- --6P5A9FWlLr7GoN4Oc2v79S72Oei30sl6C--