Gagallium

In a previous post I described two extensions to CompCert’s memory model that I implemented during my visit at Gallium. Another thing I have been working on is non-determinism and sequence points in C. As some of you will know, the evaluation order of expressions is not specified by the C standard. This allows a compiler to pick its preferred evaluation strategy. To allow a compiler also to delay side-effects, and to interleave evaluation, the allowed non-determinism is slightly restricted.

Let me start this post by briefly introducing myself: I am a PhD student at the Radboud University Nijmegen, the Netherlands, working on developing a formal semantics for the C11 standard in Coq. Between January and March, I have been a guest at Gallium (many thanks to Xavier Leroy for inviting me!). During this stay I have been able to do some CompCert hacking, and to get more experience with CompCert and its semantics.

For my 25th birthday, my (awesome) friends offered me a new gadget, a Nexus 7 tablet. Of course, my first impulse was to install Debian on it. That seemed a little bit excessive; I tried to be reasonable, and decided to first try to run OCaml programs on the tablet.

I successfully managed to set up Unison on the tablet, and used it to synchronize documents between the tablet and my home computer. At the end of this blog post, hopefully you’ll be able to do the same!