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 ESMTPS id 2005B5D5 for ; Tue, 28 May 2019 17:58:54 +0000 (UTC) X-IronPort-AV: E=Sophos;i="5.60,523,1549926000"; d="scan'208,217";a="385107086" Received: from sympa.inria.fr ([193.51.193.213]) by mail2-relais-roc.national.inria.fr with ESMTP; 28 May 2019 19:58:52 +0200 Received: by sympa.inria.fr (Postfix, from userid 20132) id 0501D824A7; Tue, 28 May 2019 19:58:53 +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 837A47ED69 for ; Tue, 28 May 2019 19:58:17 +0200 (CEST) Authentication-Results: mail3-smtp-sop.national.inria.fr; spf=None smtp.pra=fabrice.le_fessant@ocamlpro.com; spf=Pass smtp.mailfrom=fabrissimo@gmail.com; spf=None smtp.helo=postmaster@mail-qk1-f180.google.com IronPort-PHdr: =?us-ascii?q?9a23=3ATEr76xz7m3u0Uz3XCy+O+j09IxM/srCxBDY+r6Qd?= =?us-ascii?q?2+8fIJqq85mqBkHD//Il1AaPAdyCrase1qGP6v2ocFdDyK7JiGoFfp1IWk1Nou?= =?us-ascii?q?QttCtkPvS4D1bmJuXhdS0wEZcKflZk+3amLRodQ56mNBXdrXKo8DEdBAj0OxZr?= =?us-ascii?q?KeTpAI7SiNm82/yv95HJbAhEmSexbalvIBmorQjdudQajZZiJ60s1hbHv3xEdv?= =?us-ascii?q?hMy2h1P1yThRH85smx/J5n7Stdvu8q+tBDX6vnYak2VKRUAzs6PW874s3rrgTD?= =?us-ascii?q?QhCU5nQASGUWkwFHDBbD4RrnQ5r+qCr6tu562CmHIc37SK0/VDq+46t3ThLjlT?= =?us-ascii?q?wKPCAl/m7JlsNwjbpboBO/qBx5347Ue5yeOP5ncq/AYd8WWW9NU8BMXCJDH4y8?= =?us-ascii?q?dZMCAOUPPelar4fzqVgAowagCwawH+7g0CNEi2Xs0KEmz+gsEwfL1xEgEdIUt3?= =?us-ascii?q?TUqc34OqcIXu+u1qnIzCnMYO1L0jn79ofDbxAvru+XXbJra8XRz1UvHB7Cg1We?= =?us-ascii?q?s4PqJCmV1uURvGeF9eZgUfyghHYpqw5vuTiv3d0jio/Vho8OzVDL6T92wIMxJd?= =?us-ascii?q?2gUk57ZsSoH4dXtyGfLoZ7RN4pTW9vuCY/0LIGuJi7cTAFyJQm2x7fa+GHfJOS?= =?us-ascii?q?7h3/U+aRJDF1j29mdrKnnxu+71Ssx+nmWsS30FtGtDRJnsfSunwXyhDe6dSLR/?= =?us-ascii?q?1g9Um7wzmPzRrc6uRcLEA0i6XbL5khz6Y1lpUJsETDGjb6mFz1jKOLb0kk9PWk?= =?us-ascii?q?5uf7brn8qZ+cMIh0ig76MqswgMCwHeM4Mg0WU2ia/+SzyqHj8FXnTLlWivA6iK?= =?us-ascii?q?rUvZDAKcgFuKK1HRVZ3psg5hqjFzum1c4XnXgDLFJLYhKHiI3pNknAIP/iFvi/?= =?us-ascii?q?mVWskCxwx/DHO73hBY7ALnfGkLj7fLZ971RQxxY0zdBa/55UEK0OIOrvWk/ts9?= =?us-ascii?q?zVFgM2PBaxw+bjEdl90oIeWXmTAqKCK6PTsVqI5vo1LOWWZY8Vviz9K/k/6PL0?= =?us-ascii?q?g385gwxVQa78/IUebjiXGehhPU6ZYGb3yoMAD2givwczQartklLUAhBJYHPnca?= =?us-ascii?q?s2/DAwBcqCAM/tS5u2ibqdlHO1F5dMZ2tLTFSBJnnlbJ6NXeskbymbJ8t5iDtC?= =?us-ascii?q?Xr+kHdxynSqyvRP3nuI0ZtHf/TcV4Ne6jIAstr/j0Coq/DkxNPyzlmSETmV6hG?= =?us-ascii?q?QNHmZk06V2oEg7wVCGg/Eh3q5oUOdL7vYMaT8UcJ7Ry+sgVYL3UwPFO86KEROo?= =?us-ascii?q?G4X+Rz42Sd01zpkFZEMvQ4z+3CCG5DKjBvour5LOHIY9q/6O2HP4IsJl0XGA36?= =?us-ascii?q?4k3QEr?= X-IronPort-Anti-Spam-Filtered: true X-IronPort-Anti-Spam-Result: =?us-ascii?q?A0AQAQB/de1chrTeVdFlHAEBAQQBAQcEA?= =?us-ascii?q?QGBZYJ6gQQohBOBHZF1gg1+mV8BAwEMHxABAYclGwcBBDQTAQMBAQQBAQIBAQM?= =?us-ascii?q?BEwEBAQgLCwgpIwyCOikBgmYBAQICASNWBQsJAgsDCioCAiISAQUBHAYTgyIBg?= =?us-ascii?q?XsPD419kA48iyCBL4hsgUAGEoEighaJPYIWgRGCXQcuPoJhAoRrglgEp2ppBwK?= =?us-ascii?q?CD4Y0jGEbgh+KZolEk3CPDw8hgUWBeE0jUDEGgjWFf4pVQDCPEAEB?= X-IPAS-Result: =?us-ascii?q?A0AQAQB/de1chrTeVdFlHAEBAQQBAQcEAQGBZYJ6gQQohBO?= =?us-ascii?q?BHZF1gg1+mV8BAwEMHxABAYclGwcBBDQTAQMBAQQBAQIBAQMBEwEBAQgLCwgpI?= =?us-ascii?q?wyCOikBgmYBAQICASNWBQsJAgsDCioCAiISAQUBHAYTgyIBgXsPD419kA48iyC?= =?us-ascii?q?BL4hsgUAGEoEighaJPYIWgRGCXQcuPoJhAoRrglgEp2ppBwKCD4Y0jGEbgh+KZ?= =?us-ascii?q?olEk3CPDw8hgUWBeE0jUDEGgjWFf4pVQDCPEAEB?= X-IronPort-AV: E=Sophos;i="5.60,523,1549926000"; d="scan'208,217";a="307487664" X-MGA-submission: =?us-ascii?q?MDGNhwHYGeXmC7QfivRLOJil3t4O/IacF3+FpB?= =?us-ascii?q?0e5N3ND7wlOz228hcXWUBF+cK0BFwVEjqQ4EzCD8GQQpkS/e+HnUxkrS?= =?us-ascii?q?Z8WnmD6P6ml6Ac47msEdCm+6LhWHXei225NK1GrIRNWKfrO4nH/6UV2l?= =?us-ascii?q?rpV1OIxx9MHsvjwNtnU4Z+Kw=3D=3D?= Received: from mail-qk1-f180.google.com ([209.85.222.180]) by mail3-smtp-sop.national.inria.fr with ESMTP/TLS/AES128-GCM-SHA256; 28 May 2019 19:58:16 +0200 Received: by mail-qk1-f180.google.com with SMTP id m18so23979303qki.8 for ; Tue, 28 May 2019 10:58:16 -0700 (PDT) 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=oBqTaaaaagSj3b/s+prOXcXmOHYAmQjHb5xeQBpL7RU=; b=LneYV2wjNQdrzFs0FNVdq17bUxHAim4EIulimdZ9j0kXhoF8xArYOv4BP1kU1Hi7RF cdHKI4SdsSniN7CdP8ZQ4D80ZiJf/EmXZJe6jz5Uuwt8ohwE46iHbkJT/kRUS60XuEQH +iMoc/4i18HrXPjMHDyr3aC2TEbGboTtxNPO3bJfGC0LT8VPcJh5f01hiI8aBZXkvttN 4J3NrdoCF0gx0dEVKU38ugblt8KmXGeHXmQ5ehCLXSVMaVtZsf9GTIw+HlrzFEf83mA2 OYsP86CSqge4SkLQFXHDCZs7zghdFrEHXO6SpKJzfCwkCWiHZdb51y2U3vMA9+v2fQY+ KBfQ== X-Gm-Message-State: APjAAAUMst4HnMR6JDU9s1s8RV7K0QXrqnvhDYwbZmo+dRaO24ULfDRE 3CyNExysoZNEg4EBsGb5WjJKsCd4LOH+aSwYmLYyiw== X-Google-Smtp-Source: APXvYqzKQqSYbgj4D1WjIZX5mrthKQ0pOX4pSrxN44AeJCFD/abjM0Ws5R9Gl09nyqyNJ8E8e6F0cGMzxK8H34Au7Lk= X-Received: by 2002:a37:5cc6:: with SMTP id q189mr21419633qkb.166.1559066295051; Tue, 28 May 2019 10:58:15 -0700 (PDT) MIME-Version: 1.0 References: <8d058e9d-5293-46f1-9941-7c33fd232e04@www.fastmail.com> In-Reply-To: From: Fabrice Le Fessant Date: Tue, 28 May 2019 19:58:03 +0200 Message-ID: To: Ivan Gotovchits Cc: Jon French , caml-list Content-Type: multipart/alternative; boundary="000000000000b2abb50589f668af" X-Validation-by: fabrice.le_fessant@ocamlpro.com Subject: Re: [Caml-list] Only bytecode version of executable allocating huge amounts Reply-To: Fabrice Le Fessant X-Loop: caml-list@inria.fr X-Sequence: 17584 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: --000000000000b2abb50589f668af Content-Type: text/plain; charset="UTF-8" Content-Transfer-Encoding: quoted-printable A common difference between bytecode and native programs is that the native compiler computes the liveness of variables in the stack, so that they are not scanned anymore afterwards (or coalesced with other variables). For example, if you have a data structure that is allocated before a computation, but not used in the computation, the structure might be kept alive in the bytecode, but garbage collected in native code. Le mar. 28 mai 2019 =C3=A0 19:23, Ivan Gotovchits a =C3=A9cr= it : > 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) =3D 3 >> lseek(3, 0, SEEK_CUR) =3D 0 >> read(3, "$ifndef _VECTOR_DEC\n$define _VEC"..., 65536) =3D 7031 >> mmap(NULL, 1965819695104, PROT_READ|PROT_WRITE, >> MAP_PRIVATE|MAP_ANONYMOUS, -1, 0) =3D -1 ENOMEM (Cannot allocate memory) >> brk(0x5729f32c4000) =3D 0x55603f2f4000 >> mmap(NULL, 1965819826176, PROT_READ|PROT_WRITE, >> MAP_PRIVATE|MAP_ANONYMOUS, -1, 0) =3D -1 ENOMEM (Cannot allocate memory) >> write(2, "Fatal error: out of memory.\n", 28Fatal error: out of memory. >> ) =3D 28 >> exit_group(2) =3D ? >> +++ 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 characterist= ic >> pattern of heap or stack running out of control if I turn on memory >> debugging info in $OCAMLRUNPARAM, just that one huge allocation. When ru= n >> 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 als= o >> varies with the input. And on tiny inputs it doesn't seem to try and mak= e >> 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 >> > -- Fabrice LE FESSANT CEO, OCamlPro SAS --000000000000b2abb50589f668af Content-Type: text/html; charset="UTF-8" Content-Transfer-Encoding: quoted-printable
A common difference between bytecode and native prog= rams is that the native compiler computes the liveness of variables in the = stack, so that they are not scanned anymore afterwards (or coalesced with o= ther variables). For example, if you have a data structure that is allocate= d before a computation, but not used in the computation, the structure migh= t be kept alive in the bytecode, but garbage collected in native code.

Le=C2=A0mar. 28 mai 2019 =C3=A0 19:23, Ivan Gotovchits <ivg@ieee.org> a =C3=A9crit=C2=A0:
My (common) suspect is Zarith.= It uses a different backend when compiled to bytecode, so I would start my= investigation from this point :)=C2=A0

Hope it helps,
Ivan

On Tue, May 28, 2019 at 8:27 AM Jon French <jf451@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 prett= y 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 fin= e.

strace for an example run ends in:

openat(AT_FDCWD, "/home= /ojno/work/sail2/lib/vector_dec.sail", O_RDONLY|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$define _VEC"..., 65536) = =3D 7031
mmap(NULL, 1965819695104, PROT_READ|PROT_WRITE, MAP_= PRIVATE|MAP_ANONYMOUS, -1, 0) =3D -1 ENOMEM (Cannot 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, 1965819826176, PROT_READ|PROT_W= RITE, MAP_PRIVATE|MAP_ANONYMOUS, -1, 0) =3D -1 ENOMEM (Cannot allocate memo= ry)
write(2, "Fatal error: out of memory.\n", 28Fat= al 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 don't have 2 TB of memory= available.

The exact amount of the allocatio= n varies from input to input and even run to run, but is always that approx= imate size. There's no characteristic pattern of heap or stack running = out of control if I turn on memory debugging info in $OCAMLRUNPARAM, just t= hat 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 amount= s of memory -- and the location also varies with the input. And on tiny inp= uts it doesn't seem to try and make the allocation at all.

Are we actually seeing a compiler/runtime bug here? Is the= re something I'm missing?

Thanks,

Jon French
Computer Laboratory
=
University of Cambridge
--
Fabrice LE FESSANT
CEO, OCamlPro SAS<= /div> --000000000000b2abb50589f668af--