<html><body style="word-wrap: break-word; -webkit-nbsp-mode: space; -webkit-line-break: after-white-space; "><div>Hello,</div><div><br></div><div>Here is the latest Caml Weekly News, for the week of March 03 to 10, 2009.</div><div><br></div><div>1) HLVM is now garbage collected!</div><div>2) Using OCaml with SMT solvers</div><div><br></div><div>========================================================================</div><div>1) HLVM is now garbage collected!</div><div>Archive: <<a href="http://groups.google.com/group/fa.caml/browse_thread/thread/d04446e64ce6c3b6#">http://groups.google.com/group/fa.caml/browse_thread/thread/d04446e64ce6c3b6#</a>></div><div>------------------------------------------------------------------------</div><div>** Jon Harrop announced:</div><div><br></div><div>Well, I have my first working GC running in HLVM now! Woohoo!</div><div><br></div><div>The implementation has some interesting properties:</div><div><br></div><div>.. The GC is written entirely in HLVM's own intermediate language.</div><div><br></div><div>.. When a new type is defined a new function to traverse that type is JIT </div><div>compiled. So code for the GC is generated on-the-fly.</div><div><br></div><div>.. The GC is very simple and uses a shadow stack to track roots and an </div><div>allocated list that stores all heap allocated locations and their mark bit.</div><div><br></div><div>.. When the GC gets involved, performance is currently awful. Two simple </div><div>optimizations will go a long way to curing this: touch the shadow stack only </div><div>when necessary, and do something cleverer than the current linear lookup (!) </div><div>of allocated pointers in the GC.</div><div><br></div><div>.. When the heap is deep the current GC stack overflows because it is not tail </div><div>recursive. This is easily fixed.</div><div><br></div><div>I have applied to the OCaml Forge to create a new project for HLVM where I </div><div>will upload my initial prototype. Just as soon as my French gets good enough </div><div>to understand this automated e-mail... ;-)</div><div><span class="Apple-tab-span" style="white-space:pre"> </span></div><div>** Jon Harrop later added:</div><div><br></div><div>The OCaml Forge has kindly accepted to host the HLVM project:</div><div><br></div><div> <<a href="http://hlvm.forge.ocamlcore.org">http://hlvm.forge.ocamlcore.org</a>></div><div><br></div><div>If you are interested in following, discussing or contributing to this project </div><div>please join me on the hlvm-list:</div><div><br></div><div> <<a href="http://lists.forge.ocamlcore.org/cgi-bin/mailman/listinfo/hlvm-list">http://lists.forge.ocamlcore.org/cgi-bin/mailman/listinfo/hlvm-list</a>></div><div><span class="Apple-tab-span" style="white-space:pre"> </span></div><div>** Jan Kybic asked and Jon Harrop replied:</div><div><br></div><div>> Hello. Just out of curiosity:</div><div>> </div><div>> I recall reading that one of your priorities for HLVM is performance of</div><div>> numerical code. </div><div><br></div><div>HLVM aspires to provide the following benefits over OCaml:</div><div><br></div><div>.. High performance numerics (often 2-4x faster than OCaml on x86).</div><div><br></div><div>.. High performance polymorphism: polymorphic definitions are instantiated for </div><div>different types.</div><div><br></div><div>.. More numeric types (float32, complexes, low-dimensional vectors and </div><div>matrices).</div><div><br></div><div>.. More optimizations for the benefit of numerical computing: common </div><div>subexpression elimination, hoisting of loop invariants, inlining of function </div><div>arguments to higher-order functions.</div><div><br></div><div>.. Faster and easier FFI for external libraries like FFTW and LAPACK.</div><div><br></div><div>.. Dynamic capabilities such as generic printing, hashing, comparison, </div><div>serialization and run-time type information.</div><div><br></div><div>.. Community led development: you can contribute to the open source HLVM code </div><div>base.</div><div><br></div><div>.. Commerce friendly design so it will be viable for you to buy and sell </div><div>libraries written for HLVM.</div><div><br></div><div>.. A common language run-time so you can safely consume and produce libraries </div><div>written in any languages with implementations that target HLVM.</div><div><br></div><div>> Does it mean that you expect numerical code to run faster than natively</div><div>> compiled (with ocamlopt) Ocaml? </div><div><br></div><div>Absolutely. Most numerical code already runs a lot faster in HLVM than it does </div><div>in ocamlopt if you disable GC in any inner loops that act upon arrays. In the </div><div>future, I expect HLVM to be a lot faster still because it will generate SSE </div><div>instructions (using LLVM's vector intrinsics) and perform many optimizations </div><div>of its own (such as hoisting the GC code automatically).</div><div><br></div><div>> Do you have any experiments so far to support this?</div><div><br></div><div>Yes. The "test.ml" file from the HLVM subversion repository contains over 500 </div><div>lines of test code that includes a few simple benchmarks. Here is a </div><div>comparison of the performance of ordinary OCaml with the best performance I </div><div>have been able to obtain using HLVM:</div><div><br></div><div>Float Fibonacci (recursive floating point functions)</div><div>OCaml: 6.10s</div><div>HLVM: 1.74s 3.5x faster than ocamlopt</div><div><br></div><div>Mandelbrot (complex arithmetic)</div><div>OCaml: 4.39s</div><div>HLVM: 1.89s 2.3x faster than ocamlopt</div><div><br></div><div>Sieve of Eratosthenes (int arrays)</div><div>OCaml: 14.9s (had to use big arrays)</div><div>HLVM: 7.05s 2.1x faster than ocamlopt</div><div><br></div><div>As you can see HLVM is already generating much faster code than ocamlopt. Note </div><div>that the OCaml code can be improved (e.g. by avoiding OCaml's complex number </div><div>type) but the point is that idiomatic code is much faster with HLVM.</div><div><br></div><div>> I am doing large scale numerical calculations in Ocaml and performance</div><div>> is always an issue for me.</div><div><br></div><div>A lot of people have adopted OCaml for number crunching and string munging </div><div>(bioinformatics). Although ocamlopt is an excellent compiler, HLVM has shown </div><div>that it is possible to do much better still. I hope HLVM will form the </div><div>backbone of an OCaml variant designed specifically for technical computing.</div><div><span class="Apple-tab-span" style="white-space:pre"> </span></div><div>** Jon Harrop later added:</div><div><br></div><div>> HLVM aspires to provide the following benefits over OCaml:</div><div><br></div><div>I forgot the second most important goal (!):</div><div><br></div><div>.. Easy and efficient parallelism to leverage multicores.</div><div><span class="Apple-tab-span" style="white-space:pre"> </span></div><div>========================================================================</div><div>2) Using OCaml with SMT solvers</div><div>Archive: <<a href="http://groups.google.com/group/fa.caml/browse_thread/thread/2e8214f84ff90cbc#">http://groups.google.com/group/fa.caml/browse_thread/thread/2e8214f84ff90cbc#</a>></div><div>------------------------------------------------------------------------</div><div>** Jean Yang asked:</div><div><br></div><div> I don't know if this is the right place to ask this question, but what is </div><div>the best way of using an SMT solver with an OCaml interface on Linux? </div><div><br></div><div> After a brief search it seems that Z3 is the most popular solver with an </div><div>OCaml interface, but unfortunately it only supports Windows.</div><div><span class="Apple-tab-span" style="white-space:pre"> </span></div><div>** Virgile Prevosto replied:</div><div><br></div><div>alt-ergo (<<a href="http://alt-ergo.lri.fr">http://alt-ergo.lri.fr</a>>) is written in Ocaml. Alternatively,</div><div>you may be interested in the why infrastructure to call various</div><div>external provers (<<a href="http://why.lri.fr">http://why.lri.fr</a>>)</div><div><span class="Apple-tab-span" style="white-space:pre"> </span></div><div>** Peter Hawkins also replied:</div><div><br></div><div>STP is one option (for the quantifier-free theory of finite bit</div><div>vectors and arrays). It has an OCaml interface.</div><div><<a href="http://people.csail.mit.edu/vganesh/STP_files/stp.html">http://people.csail.mit.edu/vganesh/STP_files/stp.html</a>></div><div><br></div><div>I also have a binding for MONA if that's of interest to anyone.</div><div><br></div><div>More generally, have you considered communicating with a solver of</div><div>your choice via file I/O (i.e. writing out the query to a file which</div><div>you give to the solver, and parsing the solver's output)? You wouldn't</div><div>need an ocaml binding for the solver, although you will pay a</div><div>performance cost.</div><div><span class="Apple-tab-span" style="white-space:pre"> </span></div><div>** Chris Conway also replied:</div><div><br></div><div>I have written an OCaml binding for CVC3. It is available here:</div><div> <<a href="https://code.launchpad.net/~cconway/+junk/cvc3-ocaml">https://code.launchpad.net/~cconway/+junk/cvc3-ocaml</a>></div><div><span class="Apple-tab-span" style="white-space:pre"> </span></div><div>** Jim Grundy also replied:</div><div><br></div><div>You might also want to look at the Decision Procedure Toolkit (DPT):</div><div><<a href="http://dpt.sourceforge.net/">http://dpt.sourceforge.net/</a>></div><div><br></div><div>DPT is an open source (Apache 2 licensed, source forge hosted) SMT solver</div><div>implemented in OCaml with good performance. The current release supports only</div><div>SAT + EUF, but future releases will soon add integer and rational linear</div><div>arithmetic ? of course, you can always add the theory you want yourself.</div><div><span class="Apple-tab-span" style="white-space:pre"> </span></div><div>** Michael Hicks also replied:</div><div><br></div><div>Another option is STP. It's written in C++ I think, with OCaml binders.</div><div><br></div><div><<a href="http://people.csail.mit.edu/vganesh/STP_files/stp.html">http://people.csail.mit.edu/vganesh/STP_files/stp.html</a>></div><div><span class="Apple-tab-span" style="white-space:pre"> </span></div><div>========================================================================</div><div>Using folding to read the cwn in vim 6+</div><div>------------------------------------------------------------------------</div><div>Here is a quick trick to help you read this CWN if you are viewing it using</div><div>vim (version 6 or greater).</div><div><br></div><div>:set foldmethod=expr</div><div>:set foldexpr=getline(v:lnum)=~'^=\\{78}$'?'<1':1</div><div>zM</div><div>If you know of a better way, please let me know.</div><div><br></div><div>========================================================================</div><div>Old cwn</div><div>------------------------------------------------------------------------</div><div><br></div><div>If you happen to miss a CWN, you can send me a message</div><div>(<a href="mailto:alan.schmitt@polytechnique.org">alan.schmitt@polytechnique.org</a>) and I'll mail it to you, or go take a look at</div><div>the archive (<<a href="http://alan.petitepomme.net/cwn/">http://alan.petitepomme.net/cwn/</a>>) or the RSS feed of the</div><div>archives (<<a href="http://alan.petitepomme.net/cwn/cwn.rss">http://alan.petitepomme.net/cwn/cwn.rss</a>>). If you also wish</div><div>to receive it every week by mail, you may subscribe online at</div><div><<a href="http://lists.idyll.org/listinfo/caml-news-weekly/">http://lists.idyll.org/listinfo/caml-news-weekly/</a>> .</div><div><br></div><div>========================================================================</div><div><br></div><div class="AppleMailSignature" id="E12A09DE-ADCF-40D6-B7D4-306ED5CADD30"><div>-- </div><div>Alan Schmitt <<a href="http://alan.petitepomme.net/">http://alan.petitepomme.net/</a>></div><div><br class="khtml-block-placeholder"></div><div>The hacker: someone who figured things out and made something cool happen.</div><div> .O.</div><div> ..O</div><div> OOO</div><br class="Apple-interchange-newline"> </div><br></body></html>