OCaml Weekly News Previous week Up Next week

Hello

Here is the latest OCaml Weekly News, for the week of May 24 to 31, 2016.

  1. FoCaLiZe 0.9.1 released
  2. Measuring GC latencies for OCaml program
  3. Ocaml Github Pull Requests
  4. Other OCaml News

FoCaLiZe 0.9.1 released

Archive: https://sympa.inria.fr/sympa/arc/caml-list/2016-05/msg00218.html

François Pessaux announced:
It is my pleasure to announce the new release for FoCaLiZe (the
0.9.1 version).

A certain number of bugs found in the focalizec compiler have been fixed.
The generated code is slightly lighter. Termination proofs for recursive
functions, in addition to the previously available structural way, can be now
written using a measure or a well-founded relation.
A complete description of changes / new features can in found in the CHANGES
file of the distribution.

The 0.9.1 release is available from focalize.inria.fr at
http://focalize.inria.fr/download/focalize-0.9.1.tgz
Uncompress, extract, then read the INSTALL file in the newly created
directory focalize.0.9.1 and follow the simple instructions written there.


A public GIT repository is also available, allowing to fetch the latest
development state of FoCaLiZe. However, its content is not bullet-proof and
may be unstable at some times. It reflects the real-time state of FoCaLiZe
and may bring fixes and features not available in previous releases and that
will be part of the next release.
To clone the current FoCaLiZe GIT repository, invoke:
   git clone http://focalize.inria.fr/focalize.git
This will create a focalize repository in your current directory. Once cloned,
it is possible to fetch updates with the usual GIT commands (essentially git
pull origin master). Note that this access being public, it doesn't allow
pushing (i.e. submitting) modifications done in the sources tree.


To join people and discussions write to focalize-users@inria.fr.
Implementors also listen to suggestions (and compliments if some ^_^) at the
mail address: focalize-devel@inria.fr.

Enjoy.

For the entire FoCaLiZe implementation group,

François Pessaux.

May 2016

What is it FoCaLiZe ?
---------------------

FoCaLiZe is an integrated development environment to write high integrity
programs and systems. It provides a purely functional language to formally
express specifications, describe the design and code the algorithms.
Within the functional language, FoCaLiZe provides a logical framework to
express the properties of the code. A simple declarative language provides
the natural expression of proofs of properties them from within the program
source code.

The FoCaLiZe compiler extracts statements and proof scripts from the source
file, to pass them to the Zenon proof generator to produce Coq proof terms
that are then formally verified.

The FoCaLiZe compiler also generates the code corresponding to the
program as an Objective Caml source file. This way, programs developed in
FoCaLiZe can be efficiently compiled to native code on a large variety of
architectures.

Last but not least, FoCaLiZe automatically generates the documentation
corresponding to the development, a requirement for high evaluation
assurance.

The FoCaLiZe system provides means for the developers to formally express
their specifications and to go step by step (in an incremental approach) to
design and implementation, while proving that their implementation
meets its specification or design requirements. The FoCaLiZe language offers
high level mechanisms such as inheritance, late binding, redefinition,
parametrization, etc. Confidence in proofs submitted by developers or
automatically generated ultimately relies on Coq formal proof verification.

FoCaLiZe is a son of the previous Focal system. However, it is a completely
new implementation with vastly revised syntax and semantics, featuring a
rock-solid infrastructure and greatly improved capabilities.
      

Measuring GC latencies for OCaml program

Archive: https://sympa.inria.fr/sympa/arc/caml-list/2016-05/msg00219.html

Gabriel Scherer announced:
You may be interested in the following blog post, in which I give
instructions to measure the worst-case latencies incurred by the GC:

  Measuring GC latencies in Haskell, OCaml, Racket
  http://prl.ccs.neu.edu/blog/2016/05/24/measuring-gc-latencies-in-haskell-ocaml-racket/

In summary, the commands to measure latencies look something like:

    % build the program with the instrumented runtime
    ocamlbuild -tag "runtime_variant(i)" myprog.native

    % run with instrumentation enabled
    OCAML_INSTR_FILE="ocaml.log" ./main.native

    % visualize results from the raw log
    $(OCAML_SOURCES)/tools/ocaml-instr-graph ocaml.log
    $(OCAML_SOURCES)/tools/ocaml-instr-report ocaml.log

While the OCaml GC has had a good incremental mode with low latencies
for most workloads for a long time, the ability to instrument it to
actually measure latencies is still in its infancy: it is
a side-result of Damien Doligez's stint at Jane Street last year, and
4.03.0 is the first release in which this work is available.

A practical consequence of this youth is that the "user experience" of
actually performing these measurements is currently very bad. The GC
measurements are activated in an instrumented runtime variant (OCaml
supports having several variants of the runtime available, and
deciding which one to use for a specific program at link-time), which
is the right design choice, but right now this variant is not built by
default by the compiler distribution -- building it is
a configure-time option disabled by default. This means that, as
a user interested in doing the measurements, you have to compile an
alternative OCaml compiler.
Furthermore, processing the raw instrumented log requires tool that
are also in their infancy, and are currently included in the compiler
distribution sources but not installed -- so you have to have a source
checkout available to use them. In contrast, GHC's instrumentation is
enabled by just passing the option "+RTS -s" to the Haskell program of
interest; this is superbly convenient and something we should aim at.

I discussed with Damien whether we should enable building the
instrumented runtime by default (for example pass
the --with-instrumented-runtime option to the opam switches people are
using, and encourage distributions to use it in their packages as
well). Of course there is a cost/benefit trade-off: currently
virtually nobody is using this instrumentation, but enabling it by
default would increase the compilation time of the compiler
distribution for everyone. (On my machine it only adds 5 seconds to
total build time.)

I personally think that we should aim for a rock-solid experience for
profiling and instrumenting OCaml program enabled by default¹. It is
worth making it slightly longer for anyone to install the compiler if
we can make it vastly easier to measure GC pauses in our program when
the need arises (even if it's not very often). But that is
a discussion that should be had before making any choice.

Regarding the log analysis tools, before finding about Damien's
included-but-not installed tools (a shell and an awk script, in the
finest Unix tradition) I built a quick&dirty OCaml script to do some
measurements, which can be found in the benchmark repository below. It
would not be much more work to grow this in a reusable library to
extract the current log format into a structured data structure -- the
format is undocumented but the provided scripts in tools/ have enough
information to infer the structure. Such a script/library would, of
course, remain tightly coupled to the OCaml version, but I think it
could be useful to have it packaged for users to play with.

  https://gitlab.com/gasche/gc-latency-experiment/blob/master/parse_ocaml_log.ml

¹: We cannot expect users to effectively write performant code if they
don't have the tool support for it. The fact that lazyness in Haskell
makes it harder for users to reason about efficiency or memory usage
has made the avaibility of excellent performance tooling *necessary*,
where it is merely nice-to-have in OCaml. Rather ironically, Haskell
tooling is now much better than OCaml's in this area, to the point
that it can be easier to write efficient code in Haskell.

Three side-notes on profiling tools:

1. `perf record --call-graph=dwarf` works fine for ocamlopt binaries
  (no need for a frame-pointers switch), and this is documented:
    https://ocaml.org/learn/tutorials/performance_and_profiling.html#UsingperfonLinux

2. Thomas Leonard has done excellent work on domain-specific profiling
   tools for Mirage, and this is the kind of tool support that I think
   should be available to anyone out of the box.
     http://roscidus.com/blog/blog/2014/08/15/optimising-the-unikernel/
     http://roscidus.com/blog/blog/2014/10/27/visualising-an-asynchronous-monad/

3. There is currently more debate than anyone could wish for around
   a pull request of Mark Shinwell for runtime support for dynamic call
   graph construction and its use for memory profiling.
     https://github.com/ocaml/ocaml/pull/585

4. Providing a good user experience for performance or space profiling
   is a fundamentally harder problem than for GC pauses. It may
   require specially-compiled versions of the libraries used by your
   program, and thus a general policy/agreement across the
   ecosystem. Swapping a different runtime at link-time is very easy.
      

Ocaml Github Pull Requests

Gabriel Scherer compiled this list:
Here is a sneak peek at some potential future features of the Ocaml
compiler, discussed by their implementers in these Github Pull Requests.

Do not perform compaction if the real overhead is less than expected
https://github.com/ocaml/ocaml/pull/590

Manual: New chapter on polymorphic types and functions in the tutorial
https://github.com/ocaml/ocaml/pull/594
      

Other OCaml News

From the ocamlcore planet blog:
Here are links from many OCaml blogs aggregated at OCaml Planet,
http://ocaml.org/community/planet/.

Odepack 0.6.7 released
 http://forge.ocamlcore.org/forum/forum.php?forum_id=933

Full Time: Software Developer (Functional Programming) at Jane Street in New York, NY; London, UK; Hong Kong
 http://jobs.github.com/positions/0a9333c4-71da-11e0-9ac7-692793c00b45
      

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 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