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 9CB835D5 for ; Tue, 7 Jan 2020 13:43:25 +0000 (UTC) X-IronPort-AV: E=Sophos;i="5.69,406,1571695200"; d="scan'208,217";a="430233104" Received: from sympa.inria.fr ([193.51.193.213]) by mail2-relais-roc.national.inria.fr with ESMTP; 07 Jan 2020 14:43:23 +0100 Received: by sympa.inria.fr (Postfix, from userid 20132) id C04A37F3A8; Tue, 7 Jan 2020 14:43:23 +0100 (CET) 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 073267EC74 for ; Tue, 7 Jan 2020 14:43:12 +0100 (CET) X-IronPort-AV: E=Sophos;i="5.69,406,1571695200"; d="scan'208,217";a="430232997" Received: from set.irisa.fr (HELO set) ([131.254.10.170]) by mail2-relais-roc.national.inria.fr with ESMTP/TLS/AES256-GCM-SHA384; 07 Jan 2020 14:43:11 +0100 From: Alan Schmitt To: "lwn" , "cwn" , caml-list@inria.fr Date: Tue, 07 Jan 2020 14:43:10 +0100 Message-ID: <87sgkrbcwh.fsf@polytechnique.org> MIME-Version: 1.0 Content-Type: multipart/alternative; boundary="=-=-=" Subject: [Caml-list] Attn: Development Editor, Latest OCaml Weekly News Reply-To: Alan Schmitt X-Loop: caml-list@inria.fr X-Sequence: 17930 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: --=-=-= Content-Type: text/plain; charset=utf-8 Content-Transfer-Encoding: quoted-printable Hello Here is the latest OCaml Weekly News, for the week of December 31, 2019 to January 07, 2020. Table of Contents =E2=94=80=E2=94=80=E2=94=80=E2=94=80=E2=94=80=E2=94=80=E2=94=80=E2=94=80=E2= =94=80=E2=94=80=E2=94=80=E2=94=80=E2=94=80=E2=94=80=E2=94=80=E2=94=80=E2=94= =80 ocaml-lsp preview Mkocaml Release - Project generator Garbage Collection, Side-effects and Purity A Lightweight OCaml Webapp Tutorial (Using Opium, Caqti, and Tyxml) Release of owl-symbolic 0.1.0 Static lifetime Old CWN ocaml-lsp preview =E2=95=90=E2=95=90=E2=95=90=E2=95=90=E2=95=90=E2=95=90=E2=95=90=E2=95=90=E2= =95=90=E2=95=90=E2=95=90=E2=95=90=E2=95=90=E2=95=90=E2=95=90=E2=95=90=E2=95= =90 Archive: Continuing this thread, Edwin T=C3=B6r=C3=B6k said =E2=94=80=E2=94=80=E2=94=80=E2=94=80=E2=94=80=E2=94=80=E2=94=80=E2=94=80=E2= =94=80=E2=94=80=E2=94=80=E2=94=80=E2=94=80=E2=94=80=E2=94=80=E2=94=80=E2=94= =80=E2=94=80=E2=94=80=E2=94=80=E2=94=80=E2=94=80=E2=94=80=E2=94=80=E2=94=80= =E2=94=80=E2=94=80=E2=94=80=E2=94=80=E2=94=80=E2=94=80=E2=94=80=E2=94=80=E2= =94=80=E2=94=80=E2=94=80=E2=94=80=E2=94=80=E2=94=80=E2=94=80 Here is an example with ALE and Neovim (tested with v0.3.8): =E2=80=A2 Install the [Ale] plugin. If your Vim has support for packages = (Vim 8+ or Neovim) you can simply clone it in the correct subdir, no need for a plugin manager: `git clone https://github.com/w0rp/ale.git .vim/pack/my-plugins/start/ale' =E2=80=A2 Add this to your .vimrc: =E2=94=8C=E2=94=80=E2=94=80=E2=94=80=E2=94=80 =E2=94=82 " only invoke merlin to check for errors when =E2=94=82 " exiting insert mode, not on each keystroke. =E2=94=82 let g:ale_lint_on_text_changed=3D"never" =E2=94=82 let g:ale_lint_on_insert_leave=3D1 =E2=94=82=20 =E2=94=82 " enable ALE's internal completion if deoplete is not used =E2=94=82 let g:ale_completion_enabled=3D1 =E2=94=82=20 =E2=94=82 " only pop up completion when stopped typing for ~0.5s, =E2=94=82 " to avoid distracting when completion is not needed =E2=94=82 let g:ale_completion_delay=3D500 =E2=94=82=20 =E2=94=82 " see ale-completion-completeopt-bug =E2=94=82 set completeopt=3Dmenu,menuone,preview,noselect,noinsert =E2=94=82=20 =E2=94=82 if has('packages') =E2=94=82 packloadall =E2=94=82=20 =E2=94=82 " This should be part of ALE itself, like ols.vim =E2=94=82 call ale#linter#Define('ocaml',{ =E2=94=82 \ 'name':'ocaml-lsp', =E2=94=82 \ 'lsp': 'stdio', =E2=94=82 \ 'executable': 'ocamllsp', =E2=94=82 \ 'command': '%e', =E2=94=82 \ 'project_root': function('ale#handlers#ols#Ge= tProjectRoot') =E2=94=82 \}) =E2=94=82=20 =E2=94=82 " remap 'gd' like Merlin would =E2=94=82 nmap gd (ale_go_to_definition_in_sp= lit) =E2=94=82=20 =E2=94=82 " go back =E2=94=82 nnoremap gb =E2=94=82=20 =E2=94=82 " show list of file:line:col of references for symbol under= cursor =E2=94=82 nmap go :ALEFindReferences -r= elative =E2=94=82=20 =E2=94=82 " Show documentation if available, and type =E2=94=82 nmap hh (ale_hover) =E2=94=82=20 =E2=94=82 " So I can type ,hh. More convenient than \hh. =E2=94=82 nmap , =E2=94=82 vmap , =E2=94=82 endif =E2=94=94=E2=94=80=E2=94=80=E2=94=80=E2=94=80 [Ale] Mkocaml Release - Project generator =E2=95=90=E2=95=90=E2=95=90=E2=95=90=E2=95=90=E2=95=90=E2=95=90=E2=95=90=E2= =95=90=E2=95=90=E2=95=90=E2=95=90=E2=95=90=E2=95=90=E2=95=90=E2=95=90=E2=95= =90=E2=95=90=E2=95=90=E2=95=90=E2=95=90=E2=95=90=E2=95=90=E2=95=90=E2=95=90= =E2=95=90=E2=95=90=E2=95=90=E2=95=90=E2=95=90=E2=95=90=E2=95=90=E2=95=90=E2= =95=90=E2=95=90 Archive: Chris Nevers announced =E2=94=80=E2=94=80=E2=94=80=E2=94=80=E2=94=80=E2=94=80=E2=94=80=E2=94=80=E2= =94=80=E2=94=80=E2=94=80=E2=94=80=E2=94=80=E2=94=80=E2=94=80=E2=94=80=E2=94= =80=E2=94=80=E2=94=80=E2=94=80=E2=94=80=E2=94=80 I recently created a tool to generate OCaml projects. I constantly have difficulties with dune commands and setting up opam files, etc. Mkocaml generates a dune project with inline tests, opam file, git repository, git ignore, and a Makefile with easy commands. This tool can be of great help to newcomers, allowing them to get up and running faster! Garbage Collection, Side-effects and Purity =E2=95=90=E2=95=90=E2=95=90=E2=95=90=E2=95=90=E2=95=90=E2=95=90=E2=95=90=E2= =95=90=E2=95=90=E2=95=90=E2=95=90=E2=95=90=E2=95=90=E2=95=90=E2=95=90=E2=95= =90=E2=95=90=E2=95=90=E2=95=90=E2=95=90=E2=95=90=E2=95=90=E2=95=90=E2=95=90= =E2=95=90=E2=95=90=E2=95=90=E2=95=90=E2=95=90=E2=95=90=E2=95=90=E2=95=90=E2= =95=90=E2=95=90=E2=95=90=E2=95=90=E2=95=90=E2=95=90=E2=95=90=E2=95=90=E2=95= =90=E2=95=90 Archive: Gerard asked =E2=94=80=E2=94=80=E2=94=80=E2=94=80=E2=94=80=E2=94=80=E2=94=80=E2=94=80=E2= =94=80=E2=94=80=E2=94=80=E2=94=80 GC =3D Garbage Collection GC, in a pure program, is a point that's always confused me. I always understood that freeing memory from a program was impure and would create side-effects but it seems it doesn't matter if the program is remove from all consequences of those impure acts and side-effects. Basically, if any memory block has no remaining references in the program, then freeing that block will have no consequences on the running program so its allowed to happen behind the scenes.. Is this correct reasoning? Guillaume Munch-Maccagnoni replied =E2=94=80=E2=94=80=E2=94=80=E2=94=80=E2=94=80=E2=94=80=E2=94=80=E2=94=80=E2= =94=80=E2=94=80=E2=94=80=E2=94=80=E2=94=80=E2=94=80=E2=94=80=E2=94=80=E2=94= =80=E2=94=80=E2=94=80=E2=94=80=E2=94=80=E2=94=80=E2=94=80=E2=94=80=E2=94=80= =E2=94=80=E2=94=80=E2=94=80=E2=94=80=E2=94=80=E2=94=80=E2=94=80=E2=94=80=E2= =94=80 To answer your question =E2=80=9Cdoes de-allocation creates a side-effect= ?=E2=80=9D: To state the obvious: if you care about the memory consumption of your program, then you care about the side-effect of de-allocation, and this indeed voids purity. A language like OCaml lets you reason about de-allocation. Memory is collected when values are no longer reachable. Like in other languages, 1) a value that does not escape and goes out of scope will get collected, and 2) you can reason about when a value escapes and goes out of scope thanks to OCaml respecting the strict evaluation order of value types. OCaml (like other compiled languages) is in fact more precise: it ties the dynamic notion of reachability to the lexical notion of variable occurrence. For instance, in the following: =E2=94=8C=E2=94=80=E2=94=80=E2=94=80=E2=94=80 =E2=94=82 let x =3D get_huge_data () in =E2=94=82 let z =3D long_running_function x in =E2=94=82 f z =E2=94=94=E2=94=80=E2=94=80=E2=94=80=E2=94=80 OCaml will be able to collect the value in `x' before `x' goes out of scope, and thus if possible before `long_running_function' returns. Indeed, OCaml performs liveness analysis during compilation, and records the information about variable occurrences in frame descriptors, for consumption by the GC when it scans for roots. In fact, you can rely on call-by-value operational semantics to (loosely) reason that a value no longer appears in a program, and therefore that the corresponding memory will be collected by the GC=C2=B9 ([Morrisett, Felleisen and Harper, "Abstract Models of Memory Management"]). Of course, using lazy or higher-order interfaces (when closures escape; with many idioms they do not) will make it harder to reason about the lifetime of values. (=C2=B9: For OCaml, this is a conjecture I make, for subsets which could = be given such operational semantics, and only for native compilation. Morrisett, Felleisen and Harper's semantics obviously assumes that the results of liveness analysis are made available to the GC, but this is not written, nor is there any mention of the link between liveness analysis and accuracy of garbage collection in Appel's "Modern Compiler Implementation in C". I assume that it was part of folklore at the time, though recently I mentioned it to some functional PL researcher and they seemed surprised. I only found it explicitly mentioned in later papers from the OOP community. I checked that everything seems in place for OCaml to allow such reasoning, but only the authors of the original code, @xavierleroy and @damiendoligez, can tell us if this is intended to be part of the language semantics.) Furthermore, memory is not collected immediately when a value becomes unreachable. Instead: =E2=80=A2 Short-lived values are allocated contiguously and deallocated i= n a batch, so that allocating and deallocating short-lived values is very cheap, with additional benefits in terms of cache locality. This replaces stack allocation from languages with explicit memory management. =E2=80=A2 Longer-lived values are moved to a heap that is scanned incrementally, to ensure a bounded latency. In contrast, naive reference-counting and unique pointers from C++/Rust make you pay the cost of deallocation up-front. While this is essential for understanding the performance of OCaml programs, from the point of view of deallocation-as-an-effect, the delaying of the collection of unreachable memory can be seen as a runtime optimisation, that does not change the effectful status of deallocation (the memory still gets freed). [The intuition is that an effect can support some degree of reordering without requiring purity, as illustrated by strong monads which can be commutative without being idempotent, one possible definition of purity for semanticists.] But is de-allocation an effect _in practice_? Faced with the scepticism and misunderstandings from this thread, I emit two hypotheses: 1) Memory consumption is not an issue in functional programming, for application areas that interest functional programmers. 2) Memory management in OCaml is efficient in such a way that programmers do not need to think about it in their day-to-day programming activities in those terms. Hypothesis 2) could be explained for instance if OCaml programmers are already dealing with effects and thinking about the order in which their code executes (my experience), and are only used to deal with deallocation as an afterthought, e.g. when chasing leaks with a profiler. Let us turn towards two programming language experiments from the 1990's that allow me to reject hypothesis 1). Both show what happens when one denies the status of deallocation as an effect controlled by the programmer. =E2=80=A2 Region-based memory management consisted in allocating in a sta= ck of memory _regions_ deallocated at once, and determined by a whole-program static analysis. Now regarded as a failed idea but successful experiment (i.e. good science!), it taught us a lot about the structure of functional programs in relationship to memory management ([see this retrospective]). There were some good performance results, but also pathological cases _=E2=80=9Cwhere lifeti= mes were not nested or where higher-order functions were used extensively=E2=80=9D_, sometimes requiring them to be altered to be _= =E2=80=9Cregion friendly=E2=80=9D_, which was _=E2=80=9Ctime-consuming=E2=80=9D_ and re= quired knowledge of the inference algorithm. In addition, the regions changed unpredictably when the programs evolved, and memory leaks appeared when the compiler inferred too wide regions. =E2=80=A2 Haskell was (at the time) an experiment with lazy functional programming. Pervasive laziness prevents reasoning about the lifetime of values, and purity is a central assumption used by the compiler for program transformations, which is antithetical with reasoning about deallocation as an effect. It is well-known that naive Haskell code has issues with memory leaks, and that realistic Haskell programs have to follow "best practices" to avoid leaks, by making extensive use of strictness annotations (e.g. bang patterns). Unfortunately, I found it hard to find reliable academic sources about lessons drawn from the experiment like the RBMM retrospective. The best I could find on the topic of memory leaks is the following blog post: , from a Haskell programmer who wrote in another post (linked from that one) _=E2=80=9CMy suspicion is that many (most?) large Haskell programs have space leaks, but they often go unnoticed=E2=80=9D_. This is consistent with comments I received from people with Haskell experience (first-hand, one academic and one industrial) and about an industrial Haskell consultant (second-hand) who reportedly commented that their main job was to fix memory leaks (but maybe in jest). Of course, take this with a grain of salt. At least, I believe that the Haskell academic community has accumulated empirical evidence of the extent and manner in which deallocation voids purity assumptions. Having an authoritative source about it would be pretty important to me, given the initial promises of functional programs being more tractable mathematically specifically via =E2=80=9Creferential transparency=E2=80= =9D and independence of execution order, whose theoretical justification already looks shaky to me from a semantic point of view. Some parts of the literature continues to promise far-reaching consequences of equational reasoning, without clear statements of limitation of the application domain. I have the impression that the Haskell which is practiced in the real world is very different from what you can read in some academic papers. The hypothesis that deallocation matters as an effect, and that ML makes it easy to program and reason about effects, seems to me a strong argument explaining OCaml's predictable and competitive performance. So, thank you for your healthy scepticism. [Morrisett, Felleisen and Harper, "Abstract Models of Memory Management"] [see this retrospective] Xavier Leroy replied =E2=94=80=E2=94=80=E2=94=80=E2=94=80=E2=94=80=E2=94=80=E2=94=80=E2=94=80=E2= =94=80=E2=94=80=E2=94=80=E2=94=80=E2=94=80=E2=94=80=E2=94=80=E2=94=80=E2=94= =80=E2=94=80=E2=94=80=E2=94=80 Concerning the "don't scan local variables that are dead" trick: =E2=80=A2 Technically it is not "intended to be part of the language semantics" because the bytecode compiler (ocamlc) doesn't implement it, only the native-code compiler (ocamlopt). =E2=80=A2 As far as I remember, I reinvented this trick circa 1993, but it seems it was used earlier in the Lazy ML compiler by Augustsson and Johnsson. See Appel and Shao's paper "An Empirical and Analytic Study of Stack vs. Heap Cost for Languages with Closures", JFP, 1996, end of section 5. Guillaume Munch-Maccagnoni the asked =E2=94=80=E2=94=80=E2=94=80=E2=94=80=E2=94=80=E2=94=80=E2=94=80=E2=94=80=E2= =94=80=E2=94=80=E2=94=80=E2=94=80=E2=94=80=E2=94=80=E2=94=80=E2=94=80=E2=94= =80=E2=94=80=E2=94=80=E2=94=80=E2=94=80=E2=94=80=E2=94=80=E2=94=80=E2=94=80= =E2=94=80=E2=94=80=E2=94=80=E2=94=80=E2=94=80=E2=94=80=E2=94=80=E2=94=80=E2= =94=80=E2=94=80=E2=94=80 TL;DR: the paper mentioned by @xavierleroy provides additional references regarding the importance of liveness analysis for GC, including a demonstration by Appel that this actually matters for space complexity (thanks!). I find that a link is still missing with an abstract semantics =C3=A0 la Morrisett, Felleisen & Harper. This seems important to me because more theoretical works about time & space complexity in the lambda-calculus seem to take for granted that garbage collection implements something like the latter (i.e., how does one specify and certify that a compiler is sound for space complexity?). Xavier Leroy replied =E2=94=80=E2=94=80=E2=94=80=E2=94=80=E2=94=80=E2=94=80=E2=94=80=E2=94=80=E2= =94=80=E2=94=80=E2=94=80=E2=94=80=E2=94=80=E2=94=80=E2=94=80=E2=94=80=E2=94= =80=E2=94=80=E2=94=80=E2=94=80 See for example [Closure Conversion is Safe for Space], by Zoe Paraskevopoulou and Andrew W. Appel, ICFP 2019. [Closure Conversion is Safe for Space] A Lightweight OCaml Webapp Tutorial (Using Opium, Caqti, and Tyxml) =E2=95=90=E2=95=90=E2=95=90=E2=95=90=E2=95=90=E2=95=90=E2=95=90=E2=95=90=E2= =95=90=E2=95=90=E2=95=90=E2=95=90=E2=95=90=E2=95=90=E2=95=90=E2=95=90=E2=95= =90=E2=95=90=E2=95=90=E2=95=90=E2=95=90=E2=95=90=E2=95=90=E2=95=90=E2=95=90= =E2=95=90=E2=95=90=E2=95=90=E2=95=90=E2=95=90=E2=95=90=E2=95=90=E2=95=90=E2= =95=90=E2=95=90=E2=95=90=E2=95=90=E2=95=90=E2=95=90=E2=95=90=E2=95=90=E2=95= =90=E2=95=90=E2=95=90=E2=95=90=E2=95=90=E2=95=90=E2=95=90=E2=95=90=E2=95=90= =E2=95=90=E2=95=90=E2=95=90=E2=95=90=E2=95=90=E2=95=90=E2=95=90=E2=95=90=E2= =95=90=E2=95=90=E2=95=90=E2=95=90=E2=95=90=E2=95=90=E2=95=90=E2=95=90=E2=95= =90 Archive: Shon announced =E2=94=80=E2=94=80=E2=94=80=E2=94=80=E2=94=80=E2=94=80=E2=94=80=E2=94=80=E2= =94=80=E2=94=80=E2=94=80=E2=94=80=E2=94=80=E2=94=80 The tutorial is [hosted on gitlab pages], out of [this repository]. I put this together in response to some requests for introductory material on the topic (here and on [/r/ocaml]. I don't have much expertise to offer in this area, but I had hacked together some simple servers based on Opium in the past few months, so it seemed like I should be able to memorialize some of what I learned for the benefit of others. I received some critical guidance by the Opium maintainers, rgrinberg and anuragsoni, and from other resources online (mentioned at the end of the tutorial). Any feedback or improvements are welcome: this is my first time writing such lengthy instructional material, and I'm sure there's lots of room to make it better. [hosted on gitlab pages] [this repository] [/r/ocaml] Release of owl-symbolic 0.1.0 =E2=95=90=E2=95=90=E2=95=90=E2=95=90=E2=95=90=E2=95=90=E2=95=90=E2=95=90=E2= =95=90=E2=95=90=E2=95=90=E2=95=90=E2=95=90=E2=95=90=E2=95=90=E2=95=90=E2=95= =90=E2=95=90=E2=95=90=E2=95=90=E2=95=90=E2=95=90=E2=95=90=E2=95=90=E2=95=90= =E2=95=90=E2=95=90=E2=95=90=E2=95=90 Archive: jrzhao42 announced =E2=94=80=E2=94=80=E2=94=80=E2=94=80=E2=94=80=E2=94=80=E2=94=80=E2=94=80=E2= =94=80=E2=94=80=E2=94=80=E2=94=80=E2=94=80=E2=94=80=E2=94=80=E2=94=80=E2=94= =80=E2=94=80 The Owl tutorial book URL address is now changed to: . Static lifetime =E2=95=90=E2=95=90=E2=95=90=E2=95=90=E2=95=90=E2=95=90=E2=95=90=E2=95=90=E2= =95=90=E2=95=90=E2=95=90=E2=95=90=E2=95=90=E2=95=90=E2=95=90 Archive: Andr=C3=A9 asked and Guillaume Munch-Maccagnoni replied =E2=94=80=E2=94=80=E2=94=80=E2=94=80=E2=94=80=E2=94=80=E2=94=80=E2=94=80=E2= =94=80=E2=94=80=E2=94=80=E2=94=80=E2=94=80=E2=94=80=E2=94=80=E2=94=80=E2=94= =80=E2=94=80=E2=94=80=E2=94=80=E2=94=80=E2=94=80=E2=94=80=E2=94=80=E2=94=80= =E2=94=80=E2=94=80=E2=94=80=E2=94=80=E2=94=80=E2=94=80=E2=94=80=E2=94=80=E2= =94=80=E2=94=80=E2=94=80=E2=94=80=E2=94=80=E2=94=80=E2=94=80=E2=94=80=E2=94= =80=E2=94=80=E2=94=80=E2=94=80=E2=94=80=E2=94=80=E2=94=80=E2=94=80=E2=94=80 > Is it possible to =E2=80=9Cstatically=E2=80=9D allocate a value? By thi= s I mean mark a value such that it gets ignored by the GC and lives until the program exits? This is indeed the purpose of Ancient, which comes with limitations and does not allow you to reclaim the memory until you exit the program. (I am curious to know how well it works with recent OCaml versions.) > it would be really interesting to learn whether Ocaml forbids blocks outside the heap. The OCaml runtime has two modes (chosen at compilation) for dealing with so-called "out-of-heap" pointers. In the legacy one that Chet remembers, the GC uses a page table when scanning to be able to tell which pointers it possesses. In the "no-naked-pointers" mode devised more recently for efficiency reasons, the page table is replaced by looking at the colour in the header of the dereferenced value. Out-of-heap values must be preceded by a header with colour black. The no-naked-pointer mode is more restricted, because once a static value is referenced, it can no longer be deallocated, as you never know whether it is still reachable by the GC. This should be enough to support Ancient. > One should verify such intuitions experimentally, before trying to fix them, but I=E2=80=99m not familiar with what OCaml profilers can do= =E2=80=A6 Excluding large long-lived data from the GC is an old idea. Among recent developments, Nguyen et al. [1] distinguish a "control path" (where the generational hypothesis is assumed to hold) from a "data path" (where values are assumed to follow an "epochal" behaviour (long-lived, similar lifetimes, benefit from locality), and are excluded from GC). They give as motivation so-called "big data" and as figures of pathological GC usage up to 50% of total runtime. I remember reading similar figures from blog posts about large data sets in OCaml. In reality this indeed depends on knobs you can turn on your GC that can result in increased peak memory usage among others. (Assuming infinite available memory, it is even possible to let the GC share drop to 0%.) @ppedrot reported to me that in a recent experiment with Coq, using an Ancient-like trick to exclude some large, long-lived and rarely-accessed values from being scanned (namely serialising them into bigarrays), they saw an 8% performance improvement across the board in benchmarks. Multicore, if I understood correctly, aims to support only the no-naked-pointer mode, and I am not sure what the page table will become. Coq currently does some out-of-heap allocation in the VM, and has been adapted to be compatible with the no-naked-pointer mode by wrapping out-of-heap pointers into custom blocks. For scanning its custom stack (which mixes in-heap and out-of-heap values), Coq sets up a custom root-scanning function (`caml_scan_roots_hook`), which still relies on the page table. Note that having to wrap out-of-heap pointers in custom blocks is (much!) less expressive: for instance with Ancient you can call `List.filter` on a statically-allocated list (and correctly get a GC-allocated list of statically-allocated values). With custom blocks you cannot mix in-heap and out-of-heap values in this way. For a type system to deal with "statically" allocated values, have a look at Rust, which: 1) prevents cycles of reference-counting schemes thanks to uniqueness, 2) can treat GC roots as resources to deal with backpointers at the leaves of the value (cf. the interoperability with SpiderMonkey's GC in Servo). A point of view that I like is that tracing GCs and static allocation differ fundamentally by how they traverse values for collection: traversing live values for the first one, and traversing values at the moment of their death for the other. This gives them distinct advantages and drawbacks so one can see them as complementary. (See notably [2,3].) Static allocation is interesting for performance in some aspects (no tracing, no read-write barrier, reusability of memory cells, avoids calling the GC at inappropriate times), but I find it even more interesting for interoperability (e.g. exchanging values freely with C or Rust, or [applications from that other thread]). It is natural to want to mix them in a language. As far as I understand, developing the runtime capabilities for OCaml to deal with out-of-heap pointers without resorting to an expensive page table is an engineering problem, not a fundamental one. If anyone is interested in this, please contact me. [1] Nguyen et al., [Yak : A High-Performance Big-Data-Friendly Garbage Collector], 2016 [2] Bacon, Cheng and Rajan, [A Unified Theory of Garbage Collection], 2004 [3] Shahriyar, Blackburn and Frampton, [Down for the Count? Getting Reference Counting Back in the Ring], 2012 [applications from that other thread] [Yak : A High-Performance Big-Data-Friendly Garbage Collector] [A Unified Theory of Garbage Collection] [Down for the Count? Getting Reference Counting Back in the Ring] UnixJunkie also replied =E2=94=80=E2=94=80=E2=94=80=E2=94=80=E2=94=80=E2=94=80=E2=94=80=E2=94=80=E2= =94=80=E2=94=80=E2=94=80=E2=94=80=E2=94=80=E2=94=80=E2=94=80=E2=94=80=E2=94= =80=E2=94=80=E2=94=80=E2=94=80=E2=94=80=E2=94=80=E2=94=80 If you can store your long-leaved data into a bigarray, I think you would reach the effect that you were looking for (no more GC scanning of this data). This was once advised to me by Oleg, for some performance-critical section of some code. Old CWN =E2=95=90=E2=95=90=E2=95=90=E2=95=90=E2=95=90=E2=95=90=E2=95=90 If you happen to miss a CWN, you can [send me a message] and I'll mail it to you, or go take a look at [the archive] or the [RSS feed of the archives]. If you also wish to receive it every week by mail, you may subscribe [online]. [Alan Schmitt] [send me a message] [the archive] [RSS feed of the archives] [online] [Alan Schmitt] --=-=-= Content-Type: text/html; charset=utf-8 Content-Disposition: inline Content-Transfer-Encoding: quoted-printable OCaml Weekly News

OCaml Weekly News

Previous Week Up Next Week

Hello

Here is the latest OCaml Weekly News, for the week of December 31, 2019 to = January 07, 2020.

ocaml-lsp preview

Continuing this thread, Edwin T=C3=B6r=C3=B6k said

Here is an example with ALE and Neovim (tested with v0.3.8):

  • Install the Ale p= lugin. If your Vim has support for packages (Vim 8+ or Neovim) you can simp= ly clone it in the correct subdir, no need for a plugin manager: git = clone https://github.com/w0rp/ale.git .vim/pack/my-plugins/start/ale=
  • Add this to your .vimrc:
" only invoke merlin to check for errors when
" exiting insert mode, not on each keystroke.
let g:ale_lint_on_text_changed=3D"never"
let g:ale_lint_on_insert_leave=3D1

" enable ALE's internal completion if deoplete is not used
let g:ale_completion_enabled=3D1

" only pop up completion when stopped typing for ~0.5s,
" to avoid distracting when completion is not needed
let g:ale_completion_delay=3D500

" see ale-completion-completeopt-bug
set completeopt=3Dmenu,menuone,preview,noselect,noinsert

if has('packages')
    packloadall

    " This should be part of ALE itself, like ols.vim
    call ale#linter#Define('ocaml',{
                \ 'name':'ocaml-lsp',
                \ 'lsp': 'stdio',
                \ 'executable': 'ocamllsp',
                \ 'command': '%e',
                \ 'project_root': function('ale#handlers#ols#GetProjectRoot=
')
                \})

    " remap 'gd' like Merlin would
    nmap <silent><buffer> gd  <Plug>(ale_go_to_definition=
_in_split)<CR>

    " go back
    nnoremap <silent> <LocalLeader>gb <C-O>

    " show list of file:line:col of references for symbol under cursor
    nmap <silent><buffer> <LocalLeader>go :ALEFindReferen=
ces -relative<CR>

    " Show documentation if available, and type
    nmap <silent><buffer> <LocalLeader>hh <Plug>(al=
e_hover)<CR>

    " So I can type ,hh. More convenient than \hh.
    nmap , <LocalLeader>
    vmap , <LocalLeader>
endif

Mkocaml Release - Project generator

Chris Nevers announced

I recently created a tool to generate OCaml projects. I constantly have dif= ficulties with dune commands and setting up opam files, etc. Mkocaml genera= tes a dune project with inline tests, opam file, git repository, git ignore= , and a Makefile with easy commands. This tool can be of great help to newcomers, a= llowing them to get up and running faster!

https://github.com/chris= nevers/mkocaml

Garbage Collection, Side-effects and Purity

Gerard asked

GC =3D Garbage Collection

GC, in a pure program, is a point that's always confused me. I always under= stood that freeing memory from a program was impure and would create side-e= ffects but it seems it doesn't matter if the program is remove from all con= sequences of those impure acts and side-effects.

Basically, if any memory block has no remaining references in the program, = then freeing that block will have no consequences on the running program so= its allowed to happen behind the scenes..

Is this correct reasoning?

Guillaume Munch-Maccagnoni replied

To answer your question =E2=80=9Cdoes de-allocation creates a side-effect?= =E2=80=9D:

To state the obvious: if you care about the memory consumption of your prog= ram, then you care about the side-effect of de-allocation, and this indeed = voids purity.

A language like OCaml lets you reason about de-allocation. Memory is collec= ted when values are no longer reachable. Like in other languages, 1) a valu= e that does not escape and goes out of scope will get collected, and 2) you= can reason about when a value escapes and goes out of scope thanks to OCam= l respecting the strict evaluation order of value types. OCaml (like other = compiled languages) is in fact more precise: it ties the dynamic notion of = reachability to the lexical notion of variable occurrence. For instance, in= the following:

let x =3D get_huge_data =
() in
let z =3D long_running_function x in
f z

OCaml will be able to collect the value in x before x goes out of scope, and thus if possible before long_running_func= tion returns. Indeed, OCaml performs liveness analysis during compil= ation, and records the information about variable occurrences in frame desc= riptors, for consumption by the GC when it scans for roots. In fact, you ca= n rely on call-by-value operational semantics to (loosely) reason that a va= lue no longer appears in a program, and therefore that the corresponding me= mory will be collected by the GC=C2=B9 (Morrisett, Felleisen and Harper, "Abstract Models of Mem= ory Management"). Of course, using lazy or higher-order interfaces (whe= n closures escape; with many idioms they do not) will make it harder to rea= son about the lifetime of values.

(=C2=B9: For OCaml, this is a conjecture I make, for subsets which could be= given such operational semantics, and only for native compilation. Morrise= tt, Felleisen and Harper's semantics obviously assumes that the results of = liveness analysis are made available to the GC, but this is not written, no= r is there any mention of the link between liveness analysis and accuracy o= f garbage collection in Appel's "Modern Compiler Implementation in C". I as= sume that it was part of folklore at the time, though recently I mentioned = it to some functional PL researcher and they seemed surprised. I only found= it explicitly mentioned in later papers from the OOP community. I checked = that everything seems in place for OCaml to allow such reasoning, but only = the authors of the original code, @xavierleroy and @damiendoligez, can tell= us if this is intended to be part of the language semantics.)

Furthermore, memory is not collected immediately when a value becomes unrea= chable. Instead:

  • Short-lived values are allocated contiguously and deallocated in a batc= h, so that allocating and deallocating short-lived values is very cheap, wi= th additional benefits in terms of cache locality. This replaces stack allo= cation from languages with explicit memory management.
  • Longer-lived values are moved to a heap that is scanned incrementally, = to ensure a bounded latency. In contrast, naive reference-counting and uniq= ue pointers from C++/Rust make you pay the cost of deallocation up-front.

While this is essential for understanding the performance of OCaml programs= , from the point of view of deallocation-as-an-effect, the delaying of the = collection of unreachable memory can be seen as a runtime optimisation, tha= t does not change the effectful status of deallocation (the memory still ge= ts freed). [The intuition is that an effect can support some degree of reor= dering without requiring purity, as illustrated by strong monads which can = be commutative without being idempotent, one possible definition of purity = for semanticists.]

But is de-allocation an effect in practice= ? Faced with the scepticism and misunderstandings from this thread, I emit = two hypotheses:

  1. Memory consumption is not an issue in functional programming, for appli= cation areas that interest functional programmers.
  2. Memory management in OCaml is efficient in such a way that programmers = do not need to think about it in their day-to-day programming activities in= those terms.

Hypothesis 2) could be explained for instance if OCaml programmers are alre= ady dealing with effects and thinking about the order in which their code e= xecutes (my experience), and are only used to deal with deallocation as an = afterthought, e.g. when chasing leaks with a profiler.

Let us turn towards two programming language experiments from the 1990's th= at allow me to reject hypothesis 1). Both show what happens when one denies= the status of deallocation as an effect controlled by the programmer.

  • Region-based memory management consisted in allocating in a stack of me= mory regions deallocated at once, and dete= rmined by a whole-program static analysis. Now regarded as a failed idea bu= t successful experiment (i.e. good science!), it taught us a lot about the = structure of functional programs in relationship to memory management (see this retrospective). There were some good performance results, bu= t also pathological cases =E2=80=9Cwhere lifetime= s were not nested or where higher-order functions were used extensively=E2= =80=9D, sometimes requiring them to be altered to be =E2=80=9Cregion friendly=E2=80=9D, which was =E2=80=9Ctime-consuming=E2=80=9D and required knowled= ge of the inference algorithm. In addition, the regions changed unpredictab= ly when the programs evolved, and memory leaks appeared when the compiler i= nferred too wide regions.
  • Haskell was (at the time) an experiment with lazy functional programmin= g. Pervasive laziness prevents reasoning about the lifetime of values, and = purity is a central assumption used by the compiler for program transformat= ions, which is antithetical with reasoning about deallocation as an effect.= It is well-known that naive Haskell code has issues with memory leaks, and= that realistic Haskell programs have to follow "best practices" to avoid l= eaks, by making extensive use of strictness annotations (e.g. bang patterns= ). Unfortunately, I found it hard to find reliable academic sources about l= essons drawn from the experiment like the RBMM retrospective. The best I co= uld find on the topic of memory leaks is the following blog post: https://queue.acm.org/de= tail.cfm?id=3D2538488, from a Haskell programmer who wrote in another p= ost (linked from that one) =E2=80=9CMy suspicion = is that many (most?) large Haskell programs have space leaks, but they ofte= n go unnoticed=E2=80=9D. This is consistent with comments I received= from people with Haskell experience (first-hand, one academic and one indu= strial) and about an industrial Haskell consultant (second-hand) who report= edly commented that their main job was to fix memory leaks (but maybe in je= st). Of course, take this with a grain of salt. At least, I believe that th= e Haskell academic community has accumulated empirical evidence of the exte= nt and manner in which deallocation voids purity assumptions. Having an aut= horitative source about it would be pretty important to me, given the initi= al promises of functional programs being more tractable mathematically spec= ifically via =E2=80=9Creferential transparency=E2=80=9D and independence of= execution order, whose theoretical justification already looks shaky to me= from a semantic point of view. Some parts of the literature continues to p= romise far-reaching consequences of equational reasoning, without clear sta= tements of limitation of the application domain. I have the impression that= the Haskell which is practiced in the real world is very different from wh= at you can read in some academic papers.

The hypothesis that deallocation matters as an effect, and that ML makes it= easy to program and reason about effects, seems to me a strong argument ex= plaining OCaml's predictable and competitive performance.

So, thank you for your healthy scepticism.

Xavier Leroy replied

Concerning the "don't scan local variables that are dead" trick:

  • Technically it is not "intended to be part of the language semantics" b= ecause the bytecode compiler (ocamlc) doesn't implement it, only the native= -code compiler (ocamlopt).
  • As far as I remember, I reinvented this trick circa 1993, but it seems = it was used earlier in the Lazy ML compiler by Augustsson and Johnsson. See= Appel and Shao's paper "An Empirical and Analytic Study of Stack vs. Heap = Cost for Languages with Closures", JFP, 1996, end of section 5.

Guillaume Munch-Maccagnoni the asked

TL;DR: the paper mentioned by @xavierleroy provides additional references r= egarding the importance of liveness analysis for GC, including a demonstrat= ion by Appel that this actually matters for space complexity (thanks!). I f= ind that a link is still missing with an abstract semantics =C3=A0 la Morri= sett, Felleisen & Harper. This seems important to me because more theor= etical works about time & space complexity in the lambda-calculus seem = to take for granted that garbage collection implements something like the l= atter (i.e., how does one specify and certify that a compiler is sound for = space complexity?).

Xavier Leroy replied

See for example Closure Conversion is Safe for Space, by Zoe Paraskevopoul= ou and Andrew W. Appel, ICFP 2019.

A Lightweight OCaml Webapp Tutorial (Using Opium, Caqti, and T= yxml)

Shon announced

The tutorial is hoste= d on gitlab pages, out of this repository.

I put this together in response to some requests for introductory material = on the topic (here and on /r/oc= aml. I don't have much expertise to offer in this area, but I had hacke= d together some simple servers based on Opium in the past few months, so it= seemed like I should be able to memorialize some of what I learned for the= benefit of others. I received some critical guidance by the Opium maintain= ers, rgrinberg and anuragsoni, and from other resources online (mentioned a= t the end of the tutorial).

Any feedback or improvements are welcome: this is my first time writing suc= h lengthy instructional material, and I'm sure there's lots of room to make= it better.

Release of owl-symbolic 0.1.0

jrzhao42 announced

The Owl tutorial book URL address is now changed to: https://ocaml.xyz/book/symbolic.html.

Static lifetime

Andr=C3=A9 asked and Guillaume Munch-Maccagnoni repli= ed

> Is it possible to =E2=80=9Cstatically=E2=80=9D allocate a value? By th= is I mean mark a value such that it gets ignored by the GC and lives until = the program exits?

This is indeed the purpose of Ancient, which comes with limitations and doe= s not allow you to reclaim the memory until you exit the program. (I am cur= ious to know how well it works with recent OCaml versions.)

> it would be really interesting to learn whether Ocaml forbids blocks o= utside the heap.

The OCaml runtime has two modes (chosen at compilation) for dealing with so= -called "out-of-heap" pointers. In the legacy one that Chet remembers, the = GC uses a page table when scanning to be able to tell which pointers it pos= sesses. In the "no-naked-pointers" mode devised more recently for efficienc= y reasons, the page table is replaced by looking at the colour in the heade= r of the dereferenced value. Out-of-heap values must be preceded by a heade= r with colour black. The no-naked-pointer mode is more restricted, because = once a static value is referenced, it can no longer be deallocated, as you = never know whether it is still reachable by the GC. This should be enough t= o support Ancient.

> One should verify such intuitions experimentally, before trying to fix= them, but I=E2=80=99m not familiar with what OCaml profilers can do=E2=80= =A6

Excluding large long-lived data from the GC is an old idea. Among recent de= velopments, Nguyen et al. [1] distinguish a "control path" (where the gener= ational hypothesis is assumed to hold) from a "data path" (where values are= assumed to follow an "epochal" behaviour (long-lived, similar lifetimes, b= enefit from locality), and are excluded from GC). They give as motivation s= o-called "big data" and as figures of pathological GC usage up to 50% of to= tal runtime. I remember reading similar figures from blog posts about large= data sets in OCaml. In reality this indeed depends on knobs you can turn o= n your GC that can result in increased peak memory usage among others. (Ass= uming infinite available memory, it is even possible to let the GC share dr= op to 0%.)

@ppedrot reported to me that in a recent experiment with Coq, using an Anci= ent-like trick to exclude some large, long-lived and rarely-accessed values= from being scanned (namely serialising them into bigarrays), they saw an 8= % performance improvement across the board in benchmarks.

Multicore, if I understood correctly, aims to support only the no-naked-poi= nter mode, and I am not sure what the page table will become. Coq currently= does some out-of-heap allocation in the VM, and has been adapted to be com= patible with the no-naked-pointer mode by wrapping out-of-heap pointers int= o custom blocks. For scanning its custom stack (which mixes in-heap and out= -of-heap values), Coq sets up a custom root-scanning function (`caml_scan_r= oots_hook`), which still relies on the page table.

Note that having to wrap out-of-heap pointers in custom blocks is (much!) l= ess expressive: for instance with Ancient you can call `List.filter` on a s= tatically-allocated list (and correctly get a GC-allocated list of statical= ly-allocated values). With custom blocks you cannot mix in-heap and out-of-= heap values in this way.

For a type system to deal with "statically" allocated values, have a look a= t Rust, which: 1) prevents cycles of reference-counting schemes thanks to u= niqueness, 2) can treat GC roots as resources to deal with backpointers at = the leaves of the value (cf. the interoperability with SpiderMonkey's GC in= Servo). A point of view that I like is that tracing GCs and static allocat= ion differ fundamentally by how they traverse values for collection: traver= sing live values for the first one, and traversing values at the moment of = their death for the other. This gives them distinct advantages and drawback= s so one can see them as complementary. (See notably [2,3].) Static allocat= ion is interesting for performance in some aspects (no tracing, no read-wri= te barrier, reusability of memory cells, avoids calling the GC at inappropr= iate times), but I find it even more interesting for interoperability (e.g.= exchanging values freely with C or Rust, or applications from that other thread). It is natural to want to mix = them in a language.

As far as I understand, developing the runtime capabilities for OCaml to de= al with out-of-heap pointers without resorting to an expensive page table i= s an engineering problem, not a fundamental one. If anyone is interested in= this, please contact me.

[1] Nguyen et al., Yak : A High-Performance Big-Data-Friendly Garb= age Collector, 2016

[2] Bacon, Cheng and Rajan, A Unified Th= eory of Garbage Collection, 2004

[3] Shahriyar, Blackburn and Frampton, Down for the Count? Getting Reference Counti= ng Back in the Ring, 2012

UnixJunkie also replied

If you can store your long-leaved data into a bigarray, I think you would r= each the effect that you were looking for (no more GC scanning of this data= ).

This was once advised to me by Oleg, for some performance-critical section = of some code.

Old CWN

If you happen to miss a CWN, you can send me a message and I'll mail it to you, or go take a loo= k at the archive or the RSS feed of the archives<= /a>.

If you also wish to receive it every week by mail, you may subscribe online.

--=-=-=--