[cwn] Attn: Development Editor, Latest Caml Weekly News

Tue Mar 10 01:35:52 PDT 2009

Hello,

Here is the latest Caml Weekly News, for the week of March 03 to 10,  
2009.

1) HLVM is now garbage collected!
2) Using OCaml with SMT solvers

========================================================================
1) HLVM is now garbage collected!
Archive: <http://groups.google.com/group/fa.caml/browse_thread/thread/d04446e64ce6c3b6# 
 >
------------------------------------------------------------------------
** Jon Harrop announced:

Well, I have my first working GC running in HLVM now! Woohoo!

The implementation has some interesting properties:

.. The GC is written entirely in HLVM's own intermediate language.

.. When a new type is defined a new function to traverse that type is  
JIT
compiled. So code for the GC is generated on-the-fly.

.. The GC is very simple and uses a shadow stack to track roots and an
allocated list that stores all heap allocated locations and their mark  
bit.

.. When the GC gets involved, performance is currently awful. Two simple
optimizations will go a long way to curing this: touch the shadow  
stack only
when necessary, and do something cleverer than the current linear  
lookup (!)
of allocated pointers in the GC.

.. When the heap is deep the current GC stack overflows because it is  
not tail
recursive. This is easily fixed.

I have applied to the OCaml Forge to create a new project for HLVM  
where I
will upload my initial prototype. Just as soon as my French gets good  
enough
to understand this automated e-mail... ;-)

** Jon Harrop later added:

The OCaml Forge has kindly accepted to host the HLVM project:

  <http://hlvm.forge.ocamlcore.org>

If you are interested in following, discussing or contributing to this  
project
please join me on the hlvm-list:

  <http://lists.forge.ocamlcore.org/cgi-bin/mailman/listinfo/hlvm-list>

** Jan Kybic asked and Jon Harrop replied:

 > Hello. Just out of curiosity:
 >
 > I recall reading that one of your priorities for HLVM is  
performance of
 > numerical code.

HLVM aspires to provide the following benefits over OCaml:

.. High performance numerics (often 2-4x faster than OCaml on x86).

.. High performance polymorphism: polymorphic definitions are  
instantiated for
different types.

.. More numeric types (float32, complexes, low-dimensional vectors and
matrices).

.. More optimizations for the benefit of numerical computing: common
subexpression elimination, hoisting of loop invariants, inlining of  
function
arguments to higher-order functions.

.. Faster and easier FFI for external libraries like FFTW and LAPACK.

.. Dynamic capabilities such as generic printing, hashing, comparison,
serialization and run-time type information.

.. Community led development: you can contribute to the open source  
HLVM code
base.

.. Commerce friendly design so it will be viable for you to buy and sell
libraries written for HLVM.

.. A common language run-time so you can safely consume and produce  
libraries
written in any languages with implementations that target HLVM.

 > Does it mean that you expect numerical code to run faster than  
natively
 > compiled (with ocamlopt) Ocaml?

Absolutely. Most numerical code already runs a lot faster in HLVM than  
it does
in ocamlopt if you disable GC in any inner loops that act upon arrays.  
In the
future, I expect HLVM to be a lot faster still because it will  
generate SSE
instructions (using LLVM's vector intrinsics) and perform many  
optimizations
of its own (such as hoisting the GC code automatically).

 > Do you have any experiments so far to support this?

Yes. The "test.ml" file from the HLVM subversion repository contains  
over 500
lines of test code that includes a few simple benchmarks. Here is a
comparison of the performance of ordinary OCaml with the best  
performance I
have been able to obtain using HLVM:

Float Fibonacci (recursive floating point functions)
OCaml: 6.10s
HLVM:  1.74s  3.5x faster than ocamlopt

Mandelbrot (complex arithmetic)
OCaml: 4.39s
HLVM:  1.89s  2.3x faster than ocamlopt

Sieve of Eratosthenes (int arrays)
OCaml: 14.9s  (had to use big arrays)
HLVM:  7.05s  2.1x faster than ocamlopt

As you can see HLVM is already generating much faster code than  
ocamlopt. Note
that the OCaml code can be improved (e.g. by avoiding OCaml's complex  
number
type) but the point is that idiomatic code is much faster with HLVM.

 > I am doing large scale numerical calculations in Ocaml and  
performance
 > is always an issue for me.

A lot of people have adopted OCaml for number crunching and string  
munging
(bioinformatics). Although ocamlopt is an excellent compiler, HLVM has  
shown
that it is possible to do much better still. I hope HLVM will form the
backbone of an OCaml variant designed specifically for technical  
computing.

** Jon Harrop later added:

 > HLVM aspires to provide the following benefits over OCaml:

I forgot the second most important goal (!):

.. Easy and efficient parallelism to leverage multicores.

========================================================================
2) Using OCaml with SMT solvers
Archive: <http://groups.google.com/group/fa.caml/browse_thread/thread/2e8214f84ff90cbc# 
 >
------------------------------------------------------------------------
** Jean Yang asked:

   I don't know if this is the right place to ask this question, but  
what is
the best way of using an SMT solver with an OCaml interface on Linux?

   After a brief search it seems that Z3 is the most popular solver  
with an
OCaml interface, but unfortunately it only supports Windows.

** Virgile Prevosto replied:

alt-ergo (<http://alt-ergo.lri.fr>) is written in Ocaml. Alternatively,
you may be interested in the why infrastructure to call various
external provers (<http://why.lri.fr>)

** Peter Hawkins also replied:

STP is one option (for the quantifier-free theory of finite bit
vectors and arrays). It has an OCaml interface.
<http://people.csail.mit.edu/vganesh/STP_files/stp.html>

I also have a binding for MONA if that's of interest to anyone.

More generally, have you considered communicating with a solver of
your choice via file I/O (i.e. writing out the query to a file which
you give to the solver, and parsing the solver's output)? You wouldn't
need an ocaml binding for the solver, although you will pay a
performance cost.

** Chris Conway also replied:

I have written an OCaml binding for CVC3. It is available here:
    <https://code.launchpad.net/~cconway/+junk/cvc3-ocaml>

** Jim Grundy also replied:

You might also want to look at the Decision Procedure Toolkit (DPT):
<http://dpt.sourceforge.net/>

DPT is an open source (Apache 2 licensed, source forge hosted) SMT  
solver
implemented in OCaml with good performance. The current release  
supports only
SAT + EUF, but future releases will soon add integer and rational linear
arithmetic ? of course, you can always add the theory you want yourself.

** Michael Hicks also replied:

Another option is STP.  It's written in C++ I think, with OCaml binders.

<http://people.csail.mit.edu/vganesh/STP_files/stp.html>

========================================================================
Using folding to read the cwn in vim 6+
------------------------------------------------------------------------
Here is a quick trick to help you read this CWN if you are viewing it  
using
vim (version 6 or greater).

:set foldmethod=expr
:set foldexpr=getline(v:lnum)=~'^=\\{78}$'?'<1':1
zM
If you know of a better way, please let me know.

========================================================================
Old cwn
------------------------------------------------------------------------

If you happen to miss a CWN, you can send me a message
(alan.schmitt at polytechnique.org) and I'll mail it to you, or go take a  
look at
the archive (<http://alan.petitepomme.net/cwn/>) or the RSS feed of the
archives (<http://alan.petitepomme.net/cwn/cwn.rss>). If you also wish
to receive it every week by mail, you may subscribe online at
<http://lists.idyll.org/listinfo/caml-news-weekly/> .

========================================================================

-- 
Alan Schmitt <http://alan.petitepomme.net/>

The hacker: someone who figured things out and made something cool  
happen.
  .O.
  ..O
  OOO

-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://lists.idyll.org/pipermail/caml-news-weekly/attachments/20090310/fd0adefb/attachment.html 
-------------- next part --------------
A non-text attachment was scrubbed...
Name: PGP.sig
Type: application/pgp-signature
Size: 195 bytes
Desc: This is a digitally signed message part
Url : http://lists.idyll.org/pipermail/caml-news-weekly/attachments/20090310/fd0adefb/attachment.pgp 