From mboxrd@z Thu Jan 1 00:00:00 1970 Return-Path: Received: from mail2-relais-roc.national.inria.fr (mail2-relais-roc.national.inria.fr [192.134.164.83]) by c5ff346549e7 (Postfix) with ESMTP id F11F35D5 for ; Tue, 28 May 2019 17:23:17 +0000 (UTC) X-IronPort-AV: E=Sophos;i="5.60,523,1549926000"; d="scan'208,217";a="385104485" Received: from sympa.inria.fr ([193.51.193.213]) by mail2-relais-roc.national.inria.fr with ESMTP; 28 May 2019 19:23:17 +0200 Received: by sympa.inria.fr (Postfix, from userid 20132) id 26C8A826E3; Tue, 28 May 2019 19:23:17 +0200 (CEST) Received: from mail3-relais-sop.national.inria.fr (mail3-relais-sop.national.inria.fr [192.134.164.104]) by sympa.inria.fr (Postfix) with ESMTPS id 1A39D7ED69 for ; Tue, 28 May 2019 19:23:03 +0200 (CEST) Authentication-Results: mail3-smtp-sop.national.inria.fr; spf=None smtp.pra=ivg@ieee.org; spf=Pass smtp.mailfrom=ivg@ieee.org; spf=None smtp.helo=postmaster@mail-lj1-f180.google.com IronPort-PHdr: =?us-ascii?q?9a23=3AIRmUHxEA+XcaO0lHFMUNLZ1GYnF86YWxBRYc798d?= =?us-ascii?q?s5kLTJ78oMmwAkXT6L1XgUPTWs2DsrQY0rOQ6vq9EjVYsd6oizMrSNR0TRgLiM?= =?us-ascii?q?EbzUQLIfWuLgnFFsPsdDEwB89YVVVorDmROElRH9viNRWJ+iXhpTEdFQ/iOgVr?= =?us-ascii?q?O+/7BpDdj9it1+C15pbffxhEiCCybL9vMRm6txjdutcWjIdtN6o91hjEqWZUdu?= =?us-ascii?q?pLwm9lOUidlAvm6Meq+55j/SVQu/Y/+MNFTK73Yac2Q6FGATo/K2w669HluhfF?= =?us-ascii?q?TQuU+3sTSX4WnQZSAwjE9x71QJH8uTbnu+Vn2SmaOcr2Ta0oWTmn8qxmRgPkhD?= =?us-ascii?q?sBOjUk62zclNB+g7xHrxKgvxx/wpDbYIeJNPplY6jRecoWSXddUspNUiBMBJ63?= =?us-ascii?q?YYkSAOobJetXoIf9qFkOoxWwBgeiGf3hxSNTi3DswaE3yf4sHR3a0AEiGd8FrX?= =?us-ascii?q?TarM/yNKcXSe27z7fIwi/Fb/hL2Dn975TIchc/of6QXbJwcNbRyVIyHA7Cj1WQ?= =?us-ascii?q?t4PlMiiU1usTrWeU8fBsVeW1i24osgx8pCWkyMkrionMnI0Vy1bE+D12wIY0Od?= =?us-ascii?q?24SFN7bsW+HJRMsCGaMo17Sd4hTWFwoCs21KEKtJqhcCUJyJkr3QDTZ+CEfoSS?= =?us-ascii?q?/x7uV/qdLDFlj3x/Yr2/nQy98U24x+38SMa01FFKozJAktbWt3AN0wXf6syFSv?= =?us-ascii?q?dg50uh1yuD2gPP5u1eLkA0kq3bK5ElwrEujJYcrUPDHirulEX3iq+ZaFkk9/C2?= =?us-ascii?q?5+j7ZrjqvJyROo9uhg3gLqgjmdazDfk7PwQSR2Sb/P6z1Lzn/U33WrVKifg2n7?= =?us-ascii?q?HYsJDEKsQWva+5DBFL3Yk98Rq/CC2m0NsAkXkdMF1FYA6Hj5TuO1zWPP/3F/K/?= =?us-ascii?q?g1C1nDdvxvDGJaHhD47WLnnDlbfhZaxy51RdyAo119Bf5ohbBqsPIPLpCQfNs4?= =?us-ascii?q?n6CRlxHRa5xe3nQIF/2N9DAEqEC6rfOaiUrFzetcw1JOzZRZEcvn7SLOQi+fXu?= =?us-ascii?q?jGMi0QscY6aB3JYaZTa/BPswcBbRWmblntpUSTRChQE5VuG/zQTaCWcONUb3ZL?= =?us-ascii?q?o143QAMKzjDYrHQdrz0rmI3SP+Gp8PI24fWgjKHnDveIGJHfwLbXDKe5Mzonk/?= =?us-ascii?q?TbGkDrQZ+1S2rgajk+hmI+fZvCoCusC7jYkn16jojRg3sAdMIYGY2mCJQXtzmz?= =?us-ascii?q?pQFT470a05plZymA6O?= X-IronPort-Anti-Spam-Filtered: true X-IronPort-Anti-Spam-Result: =?us-ascii?q?A0C8AQABbe1chrTQVdFlDg8BAQUBBwUBg?= =?us-ascii?q?WWCeoEEKIQTgR2RdIINfohRkQUJAQMBDB8QAQGEQAKCYxsHAQQ0EwEDAQEEAQE?= =?us-ascii?q?CAQEDARMBAQEICwsIKSMMgjopAYJnAQICASMdAQE3AQQLCQIEBwM0AgIiEgEFA?= =?us-ascii?q?RwGE4MiAYF2BQ8PjXqQDjyKL3GBL4J5AQEFhWmBPQMGEoEii1MXgUA/gRGCXQc?= =?us-ascii?q?uPoJhAoIOgl2CWKhXCYIPhjSMYRuCH4pmiUSTcI8PDyGBRYF4fQg7MQaCNYIPG?= =?us-ascii?q?oNWhRSFBFcmMI8QAQE?= X-IPAS-Result: =?us-ascii?q?A0C8AQABbe1chrTQVdFlDg8BAQUBBwUBgWWCeoEEKIQTgR2?= =?us-ascii?q?RdIINfohRkQUJAQMBDB8QAQGEQAKCYxsHAQQ0EwEDAQEEAQECAQEDARMBAQEIC?= =?us-ascii?q?wsIKSMMgjopAYJnAQICASMdAQE3AQQLCQIEBwM0AgIiEgEFARwGE4MiAYF2BQ8?= =?us-ascii?q?PjXqQDjyKL3GBL4J5AQEFhWmBPQMGEoEii1MXgUA/gRGCXQcuPoJhAoIOgl2CW?= =?us-ascii?q?KhXCYIPhjSMYRuCH4pmiUSTcI8PDyGBRYF4fQg7MQaCNYIPGoNWhRSFBFcmMI8?= =?us-ascii?q?QAQE?= X-IronPort-AV: E=Sophos;i="5.60,523,1549926000"; d="scan'208,217";a="307485458" X-MGA-submission: =?us-ascii?q?MDFIvoU52/J36O7J3Dp9KrCNxoIKARN4BB8ETZ?= =?us-ascii?q?5MualzUzWgdXO6BOGoOFl6kEpw2L3OSjTS2npHXieaE7bCin3CrdXTv4?= =?us-ascii?q?OvVyO/sA5/TsWL7K4QSMP5j9gGcdDWeY0cBE4N6VEJYlOQl3V5eHNBGl?= =?us-ascii?q?+Y0TGtS05XW1jrqHHwTvnM2w=3D=3D?= Received: from mail-lj1-f180.google.com ([209.85.208.180]) by mail3-smtp-sop.national.inria.fr with ESMTP/TLS/AES128-GCM-SHA256; 28 May 2019 19:23:02 +0200 Received: by mail-lj1-f180.google.com with SMTP id 188so18465695ljf.9 for ; Tue, 28 May 2019 10:23:01 -0700 (PDT) DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=ieee.org; s=google; h=mime-version:references:in-reply-to:from:date:message-id:subject:to :cc; bh=pdKEl0DpQ+UfztI5cZxArRI6dXAQX9R7APK02NuigQ4=; b=RBSZWnaeCcRjSTgCcayR+s/AiHknaRZ7qvbct+Yk9gPLqZXLA++ZLU7eTPMcHxrUp4 6fKFwWbxxxfOvKrPZl4522Wf5W7gd77THyCwnAWyOkDgP6a/tcGNnTFmd/P1sKe5S1o0 5iwuc5Z3AqDg1d6yT3ovwk+S6e+cF5yL3Dbwg= X-Google-DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=1e100.net; s=20161025; h=x-gm-message-state:mime-version:references:in-reply-to:from:date :message-id:subject:to:cc; bh=pdKEl0DpQ+UfztI5cZxArRI6dXAQX9R7APK02NuigQ4=; b=FvJ6hGPzC0NGDxxN4DweNHkHdv/y/Gddp1Cc0sSfuV8WGaZ0pNgpbXyn8WBig30jxD mdx3enyYwQFcHPIQXG95m92Xvo2Ej3SIiMA1M9yEggN44tvJVDf5UyaoPeHktAiWn4hk HN2q3zntUx//0/t//Kn/jJgESkYIJ11dDKKSSsTJDV9iOIaweGJCa0LVXwbqMYis9NQ4 RFdpzoTiXSoz+V0yEV24yJih2DyN3P+DGKbhrA2ULQXhLNllcHWnC6E5vGclHesfNYXX apoypZoawFQYrls0sS2lxV+URnbAWex6rCvbKJ3kGamAOmyF7zewn42h7fPeoZKBqvPv I3Zw== X-Gm-Message-State: APjAAAVl1nfE4g0DyBbDuYPt4n0aWCXILGY72jUycCzxLHCf/xj3G3eM 80vh49l3A/015yHPL7NSo7gg4CYxr+fRwtCcMWwKIQ== X-Google-Smtp-Source: APXvYqwFtY3oJBL9fKZOAayDJKvMsumuFA5UYXFXeHLKXvKeaTHzUrsaO7r/nmkXHgD9vsDWYdkBkPETIigEnurLo8k= X-Received: by 2002:a2e:9bd2:: with SMTP id w18mr16003091ljj.120.1559064181209; Tue, 28 May 2019 10:23:01 -0700 (PDT) MIME-Version: 1.0 References: <8d058e9d-5293-46f1-9941-7c33fd232e04@www.fastmail.com> In-Reply-To: <8d058e9d-5293-46f1-9941-7c33fd232e04@www.fastmail.com> From: Ivan Gotovchits Date: Tue, 28 May 2019 13:23:56 -0400 Message-ID: To: Jon French Cc: caml-list Content-Type: multipart/alternative; boundary="000000000000b427e60589f5ea06" Subject: Re: [Caml-list] Only bytecode version of executable allocating huge amounts Reply-To: Ivan Gotovchits X-Loop: caml-list@inria.fr X-Sequence: 17583 Errors-to: caml-list-owner@inria.fr Precedence: list Precedence: bulk Sender: caml-list-request@inria.fr X-no-archive: yes List-Id: List-Archive: List-Help: List-Owner: List-Post: List-Subscribe: List-Unsubscribe: --000000000000b427e60589f5ea06 Content-Type: text/plain; charset="UTF-8" My (common) suspect is Zarith. It uses a different backend when compiled to bytecode, so I would start my investigation from this point :) Hope it helps, Ivan On Tue, May 28, 2019 at 8:27 AM Jon French wrote: > Hi all, > > I'm wondering if anyone on this list might have encountered this issue > before, since it's got me pretty stumped. > > We have an OCaml project ( https://github.com/rems-project/sail ) which > tries to allocate huge amounts of memory, but only when compiled to > bytecode. The native version works perfectly fine. > > strace for an example run ends in: > > openat(AT_FDCWD, "/home/ojno/work/sail2/lib/vector_dec.sail", > O_RDONLY|O_CLOEXEC) = 3 > lseek(3, 0, SEEK_CUR) = 0 > read(3, "$ifndef _VECTOR_DEC\n$define _VEC"..., 65536) = 7031 > mmap(NULL, 1965819695104, PROT_READ|PROT_WRITE, MAP_PRIVATE|MAP_ANONYMOUS, > -1, 0) = -1 ENOMEM (Cannot allocate memory) > brk(0x5729f32c4000) = 0x55603f2f4000 > mmap(NULL, 1965819826176, PROT_READ|PROT_WRITE, MAP_PRIVATE|MAP_ANONYMOUS, > -1, 0) = -1 ENOMEM (Cannot allocate memory) > write(2, "Fatal error: out of memory.\n", 28Fatal error: out of memory. > ) = 28 > exit_group(2) = ? > +++ exited with 2 +++ > > > which naturally fails since I don't have 2 TB of memory available. > > The exact amount of the allocation varies from input to input and even run > to run, but is always that approximate size. There's no characteristic > pattern of heap or stack running out of control if I turn on memory > debugging info in $OCAMLRUNPARAM, just that one huge allocation. When run > in ocamldebug, it also doesn't appear to be failing at a location which is > sensible to be allocating such amounts of memory -- and the location also > varies with the input. And on tiny inputs it doesn't seem to try and make > the allocation at all. > > Are we actually seeing a compiler/runtime bug here? Is there something I'm > missing? > > Thanks, > > Jon French > Computer Laboratory > University of Cambridge > --000000000000b427e60589f5ea06 Content-Type: text/html; charset="UTF-8" Content-Transfer-Encoding: quoted-printable
My (common) suspect is Zarith. It uses a different backend= when compiled to bytecode, so I would start my investigation from this poi= nt :)=C2=A0

Hope it helps,
Ivan
On Tue, M= ay 28, 2019 at 8:27 AM Jon French <jf= 451@cam.ac.uk> wrote:
Hi all,

I'm = wondering if anyone on this list might have encountered this issue before, = since it's got me pretty stumped.

We have = an OCaml project ( https://github.com/rems-project/sail ) which tries to alloc= ate huge amounts of memory, but only when compiled to bytecode. The native = version works perfectly fine.

strace for an ex= ample run ends in:

o= penat(AT_FDCWD, "/home/ojno/work/sail2/lib/vector_dec.sail", O_RD= ONLY|O_CLOEXEC) =3D 3
lseek(3, 0, SEEK_CUR)=C2=A0=C2=A0=C2=A0= =C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2= =A0=C2=A0=C2=A0 =3D 0
read(3, "$ifndef _VECTOR_DEC\n$def= ine _VEC"..., 65536) =3D 7031
mmap(NULL, 1965819695104, = PROT_READ|PROT_WRITE, MAP_PRIVATE|MAP_ANONYMOUS, -1, 0) =3D -1 ENOMEM (Cann= ot allocate memory)
brk(0x5729f32c4000)=C2=A0=C2=A0=C2=A0=C2= =A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0= =C2=A0=C2=A0=C2=A0=C2=A0 =3D 0x55603f2f4000
mmap(NULL, 196581= 9826176, PROT_READ|PROT_WRITE, MAP_PRIVATE|MAP_ANONYMOUS, -1, 0) =3D -1 ENO= MEM (Cannot allocate memory)
write(2, "Fatal error: out = of memory.\n", 28Fatal error: out of memory.
) =3D 28
exit_group(2)=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0= =C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2= =A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0 =3D ?
+++ exited with 2 +++=

which naturally fails since I do= n't have 2 TB of memory available.

The ex= act amount of the allocation varies from input to input and even run to run= , but is always that approximate size. There's no characteristic patter= n of heap or stack running out of control if I turn on memory debugging inf= o in $OCAMLRUNPARAM, just that one huge allocation. When run in ocamldebug,= it also doesn't appear to be failing at a location which is sensible t= o be allocating such amounts of memory -- and the location also varies with= the input. And on tiny inputs it doesn't seem to try and make the allo= cation at all.

Are we actually seeing a compil= er/runtime bug here? Is there something I'm missing?

=
Thanks,

Jon French
Co= mputer Laboratory
University of Cambridge
--000000000000b427e60589f5ea06--