Apr
15
2014

Here is a short report of some of our activities in March 2014 !

Welcome Thomas

First, we would like to welcome Thomas Blanc on board ! Thomas is starting a PhD at OCamlPro, with Michel Mauny from ENSTA as his PhD advisor. So, he will stay with us for three years, working on static analysis of whole OCaml programs, with two main objectives:

  • To detect uncaught exceptions, using a different approach than ocamlexc, the tool that François Pessaux developed during his PhD thesis, a method that will make Thomas' tool easier to upgrade at each new OCaml version;

  • To optimize generated code, with the benefits of whole program knowledge;

OPAM Improvements

OPAM has seen its share of code quality improvements during this month, with a rewritten parser for OPAM description files, now reporting error locations, better handling of some corner cases, more expressive install requests from the command-line, and a more friendly way of handling pinned packages. We are now stabilizing these features and you should expect soon a Beta release of OPAM 1.2.0.

Binary Release of OCaml in OPAM

We also spent some time this month working on using OPAM to distribute binary releases of OCaml. OPAM is great to use, but it sometimes takes a lot of time to compile OCaml when a new switch is needed for some small experimentation. We decided it would be interesting to experiment with a binary package of OCaml (4.01.0 for now).

The results are quite interesting, in most of our tests, downloading the compiler binary archive and uncompressing it takes an order of magnitude less time than compiling from sources, even with a slow connection:

OCaml 4.01.0 installation time on OPAM
From Sources Binary DownloadBinary Install
Intel i7 2.10GHz, Linux 64 bits, 16 GB RAM, SSD 238s 220s (DSL) 8s
Intel i7 2.60GHz, Linux 64 bits, 8 GB, SSD 253s 22s (Cable) 9s
Intel i5 2.67GHz, Linux 64 bits, 2 GB, SATA 289s 65s (Wifi) 26s
Intel Core2 2.53 GHz, Linux 32 bits, 4 GB, SSD 402s 68s (Wifi) 40s
Intel Xeon 2.67GHz, Linux 64 bits, 8 GB, SATA 289s
Intel core2 3.00 Ghz, Linux 32 bits, 4 GB, SATA 258s 15s (Cable) 7s

You can try our compiler on your system (on Intel Linux only for now, but we plan to add binary versions for other architectures):

opam switch 4.01.0+bin-ocp

So now, the fastest way to get OCaml running on a computer is downloading OPAM and calling:

opam init --comp 4.01.0+bin-ocp

Another great thing with this compiler is that the binary archive is kept in a cache (in ~/.opam/ocp-compiler-cache/), so that creating more switches for this compiler is almost cost free. For example, you can try:

opam switch 4.01.0+test+my+soft --switch 4.01.0+bin-ocp

If you have an Intel Linux computer, and you get any problem with this distribution, you should send us the output of OPAM and we will try to fix the problem ! Unfortunately for CentOS users, we had to choose a recent libc, so that it will probably not run on this system.

Solvers in the Cloud for OPAM

In some cases, OPAM's internal heuristic is not enough -- upgrades are a np-complete problem after all. For this reason, OPAM has been thought from the beginning to be able to use an external solver, using the CUDF format to interoperate with solvers. Unfortunately, depending on your system, such a solver, like aspcud, may not be available or easy to install.

So last month, we worked with the Mancoosi team to set up on one of their servers a CUDF solver farm, to work around this issue. Following the instructions on the site:

http://cudf-solvers.irill.org/index.html

you can setup your OPAM configuration to use a remote CUDF solver, that will usually propose better solutions than the one provided internally by OPAM.

A bit "hackish" way of using it immediatly is to copy the following script in a file aspcud in your path:

#!/bin/bash
SERVER=cudf-solvers.irill.org
if bzip2 -c $1 | curl -f --data-binary @- http://$SERVER/cudf.bz2?criteria="$3" | bunzip2 -c > $2;
then exit 0
else echo FAIL > $2
fi

The Alt-Ergo SMT Solver

In the context of the Bware project, where we are working on improving automatic solvers for Atelier B, we submitted a short paper to the ABZ conference describing the improvements we made in Alt-Ergo to increase its success rate on formulas translated from B proof obligations. Our paper has been accepted for publication! We will present it at ABZ 2014, which will be held in Toulouse (France) in the beginning of June.

In the Scilab Corner

We are pursuing our quest for a JIT for Scilab. Scilab really is a dynamic scripting language, in terms of typing, scoping, constructs and of how its users consider it. For most of them, it is basically an advanced, scriptable calculator. A common usecase is to pause in the middle of a function, open a toplevel at this point to edit some local variable or open a graphical visualisation, and then resume the execution.

In this context, we decided to adopt a really pragmatic approach, which is to detect statement-level code patterns that we know to be JITable, instead of trying to JIT whole functions. This way, we'll be able to leave the intro and outro of functions (which may do whatever they want to control and scope) to the interpreter, and concentrate on the inner, performance critical loop.

So, this month, we worked on several tasks required to achieve this goal. First, we worked on the detection of code snipplets, and as a side effect of this work, we plan to provide Scilab users with a new syntax-aware grep-like tool. We also worked on how to customize Scilab's loading function to replace some parts of the code by foreign calls to the future JIT. We also worked on the introspection of Scilab's context to build the environment of the JIT's type system.