Frama-C news and ideas

To content | To menu | To search | Frama-C Home

Zarith

Perhaps you are looking for something to do pending the upcoming release of Frama-C (someone called it "Nitrozen" once by accident in a commit message. I would like the name to stick, but I anticipate it won't)…


Or you are already a serious user of the value analysis plug-in or of one of the plug-ins that rely on it…


Or you might be in the near future…


Then this blog post is for you, because this blog post is about Zarith, that you should install.


Zarith is a multiprecision library for OCaml created by Antoine Miné. Zarith relies on GMP for the actual computations on big integers. Small integers, and there lies Zarith's advantage over previous multiprecision libraries for OCaml, use the same unboxed representation as OCaml's 31/63-bit integers. For computing on small integers, if you are not using some exotic architecture, Zarith uses the processor's instruction set most efficiently, relying on the processor's flags to detect whether the result can itself be represented as an unboxed integer.

The bottom line is that a multiprecision operation (say, a multiplication) is most of the times executed as the processor's corresponding instruction, with a couple of conditional branches before and after for handling the uncommon cases, and a couple of memory accesses and jumps (including a computed one) for the OCaml ↔ C interface. This may seem like a lot, but it's much less than the other multiprecision libraries. And of course, the unboxed representation saves space, too, as small integers do not have to be allocated at all and just reside in the word that would otherwise have been a pointer to their representation.


Benchmarks comparing Carbon and Nitrogen will come later; these will include the gains from switching from Big_int to Zarith. For minimal fuss, Frama-C will continue to compile with Big_int (the multiprecision library provided as part of the OCaml distribution), and perhaps I will include "Nitrogen compiled with Big_int" in the benchmarks, just to make the point.

Meanwhile, if you plan to use the value analysis for more than ten minutes, trust me, install Zarith now. You can use either the SVN version (instructions) or the 1.0 version. If you already knew about Zarith and had installed it a long time ago, I suggest you upgrade, to benefit from bugfixes and so that Frama-C Nitrogen's -save and -load options work.

[EDIT: deleted compilation instruction for obsolete Frama-C version]

Comments

1. On Tuesday, October 11 2011, 13:14 by ftk

Making an informal before / after comparison on the Skein tutorial is quite educational: Zarith provides an approximate 150% performance boost on an modern x64 system.

A quick note for users installing Zarith with Findlib: this method creates a zarith directory in the installation path, which the Frama-C compilation commands need to include. An easy method to do so is to set the environment variable ZARITH_INC to "-I +zarith".