Verifying Supercompilation in Coq

Almost in the nick of time, I managed to submit a paper to META-2010. It describes some of my recent experiments in Coq, particularly those related to supercompilation. The draft is (maybe temporarily) here. Let's hope I'll find some time to write more about it ... some day.

ICFP 2008 Contest Results Published

The results of this year's ICFP Contest are finally here (conference announcement video, some early unofficial reports, announcement on the official site). Almost unbelievable - my submission ended at the 4th place! I am really happy with this lucky achievement, but what makes me especially proud is to have added one more Haskell entry to the Top 10 list.

ICFP08 Contest Write-Up

Final submission: icfp08.tgz

This year it was my 3^rd (or more like 2^nd and a half) take at participating in the annual ICFP contest (11-14.07.2008, http://icfpcontest.org). In 2006, I finally summoned some courage to actually take part in the contest, after following it silently from the very beginning (and finding it very interesting and challenging). I was quite determined to try to use Haskell, as it was (and still is) my favorite among languages with industrial-strength implementations. Unfortunately, back in 2006, I did not plan in advance to have the weekend completely free to myself, so I actually managed to spend just a few hours here and there on the task... and finally did not manage to submit anything. In 2007 my preparation was better, but I was still a lonely player – not knowing anybody personally who knows Haskell and would like to play along. Still, I managed to get along, to see at least some daylight in the picture (http://save-endo.cs.uu.nl/) ... and came up 146 in the final ranking. This year, the organization was almost the same – enough free time for all the 3 days, Haskell one more time as my language of choice; the positive development was that I had at least some supporters, who followed closely the course of the event, and helped me with some valuable advise, even though they did not want to take official part in the team. I had a fairly new Windows laptop, which I intended to use primarily, and a 4-5 years old Windows desktop.

Day 0, Parsing rover messages:

Friday, 22:00 EEST – the task is published. I had barely managed to burn a real CD with the Knoppix installation that was to be used as testing environment. Initially, the problem seemed not so much to my liking as the previous year, but I decided to give it a try anyway, and today I do not regret it the least – it was quite some fun! As it was getting late already, and I did not plan to deprive myself too much of sleep, I decided to start with something simple – getting the network connection open, and parsing incoming messages into typed internal records. That piece seemed ready at about 2:30-3:00, and it was time to go to bed.

Day 1, Making the rover move:

Saturday started and ended with bad and frustrating surprises. The first one was making the LiveCD work, and in a way permitting easy transfer of new versions to it for test. The environment worked more or less OK under Qemu, but not at all under MS Virtual PC. For some reasons or other, I did not try immediately with VMPlayer. The physical CD booted quite OK both on the desktop and the laptop, but I was not prepared to develop in this environment, and the desktop CD player turned too noisy to use it as a test machine. Besides, it was not clear if I could make easy network file transfers between the notepad running Windows, and the desktop running Knoppix. Transferring files all the time through an USB stick seemed just too preposterous. Luckily, a friend of mine following closely my progress finally came with a brilliantly simple idea: To make easy file transfers between Knoppix under Qemu and Windows running on the bare metal, make a directory in Windows network-shared, and connect to it from Konquerer using the SMB protocol. It worked almost perfectly, but it was already around 14:30 when I could finally consider my testing environment well set up. Then the second nasty surprise of the event followed: my code, compiling perfectly with ghc 6.8.3 under Windows, refused to compile in the LiveCD environment – missing network libraries?! At first I hoped it was some trivial configuration problem, but some investigation with ghc-pkg did not confirm it. Some hectic searching around the contest mailing-list and Trac, and voilà – someone reported having the same problem, luckily with some partial workaround – use stdin/out in Haskell and use netcat to make the actual network connection. So far, so good... I could finally make my first real tests. The good thing: my message parsing code seemed to work immediately, no nasty bugs to fix (16:00).

My next idea was to proceed by small steps, and first try to make the rover move and head straight for the home base, oblivious of any obstacles en route. At that point I also decided to simplify things temporarily and make separate decisions about changing the turn and the move state. The move control logic was simple – accelerate till very close to the maximum speed, then keep rolling. Unfortunately, this quite simplistic heuristics persisted till my final submission.

After some coding I started testing. The rover started moving, albeit with some delay... but it was not heading directly to base, instead turning around as if led by a drunken driver (~18:30). Some log analysis showed that the commands I sent were quite reasonable... but the rover was not changing state accordingly... at least not immediately. I suspected the reason was that netcat did not set the TCP_NODELAY flag on the socket (which flag was explicitly suggested by the organizers). After some searching and consultations with some friends, more Linux- and network-savvy than me, it appeared that netcat did not support this option directly, the best approximation being “-T Minimize-Delay”. That last option did not help much in my tests. I was getting completely desperate, feeling handicapped by both my choices of Windows and Haskell as working environment and programming language. After thinking of, and getting advise about a lot of crazy ideas, I finally pursued one of them – make a stripped-down version of netcat in Python. After reading most of the original netcat source code (quite amusing comments, btw), and also the sources of several clones in different languages that I found on the net, I finally ended, even to my surprise, with just a 5-10 lines of Python, which happened to duplicate the relevant netcat functionality, at least under Linux and Cygwin. Unfortunately, though replacing netcat by this python script showed some progress in avoiding command reaction lags, it was far from enough. Besides, the opportunity to submit a lightning entry was missed. Quite unhappy ending of this day.

Day 2, Avoiding single obstacles:

The new morning brought some new ideas – after having refused this advise the previous day, I decided to test under Knoppix running outside of Qemu anyway... and there, my code appeared to run perfectly. So, it was maybe the Qemu software emulation after all that contributed to a great extent to the server lags that I observed. As it still appeared difficult to me to use the spare desktop as test machine, I resorted to downloading VMPlayer, and borrowing a set-up LiveCD VM for it. The trick of copying files between the host and the VM using SMB in Konquerer still worked, and the server responsiveness was much better under VMPlayer, than under Qemu (13:30-14:00). There were still some lags in processing the commands I sent, but they appeared limited to the first 1-2 seconds of the 1^st run. Somewhat later I decided to add some code, which detected such server lags, and postponed (for some time) sending new commands to the server.

Anyway, I was finally able to see the rover heading straight and fast to home... until it bumped into an obstacle. It was time to add some refinements in the control logic. Still following the idea to advance by small steps, I decided to first add some code to avoid the nearest obstacle en route. My code was collecting, from the very beginning, all static objects in a big set (kept intact across runs), and all the Martians from the last telemetry reading – in a separate list. It remained to detect the crossing points between the current route and any of the obstacle, and draw a new route to avoid the closest obstacle found – time for some basic geometry calculations. I thought I might spare some time by googling, and indeed, the formulas for the crossing points between a line segment and a circle were readily available on at least one site. After finding the nearest obstacle en route, the idea was to avoid it by the tangent... and I was stuck badly calculating unwieldy quadratic equations in order to find the 2 tangent points... At one moment I was so desperate that I started looking for computer algebra systems to give me some help. After quickly scanning some reviews and comparisons, mostly on Wikipedia, I decided to give Mathomatic a try. It was a breeze to download and install (under Cygwin), but not very helpful with systems of quadratic equations... a friend with Sage and Maxima installed also tried to help with these equations, to no avail. Apparently I was getting a bit worn out, it took me quite some time to realize that it sufficed to split the task in 2 – finding the crossing points of 2 circles (which I found quickly on the net) and then the tangent was easy. After coding all this (23:30-24:00), the rover behavior became much more reasonable. Actually, it was able already to navigate safely and quite quickly to the home base at least on the supplied sample maps.

Day 3, Trying to avoid multiple obstacles at once:

I spent most of the morning on the last day preparing the distribution according to the rules. Luckily, “darcs dist” turned out to prepare distribution tar-balls instantly; it was necessary, however, to re-organize the directory structure, to fill the descriptive files, and to check the install and run scripts. All this took much longer than expected, so in the end I was glad I did not leave this job for the last 20 or 15 minutes before the deadline. After that the beginning of the afternoon was spent on some relatively trivial tasks (like adding an exception handler around the main message-processing loop, just in case), while thinking how to improve the control logic at least a little in the few hours that remained.

In accordance with the idea to progress by small steps, it seemed to me logical to address the situation where several obstacles occur in succession, and the path avoiding the nearest obstacle leads unavoidably to the next one. Meanwhile I concocted a very simple map with 2 overlapping obstacles one after the other (tst1.wrld in my submission tar-ball), and testing quickly proved my fears – after avoiding successfully, but closely, the first, smaller obstacle, the rover bumped directly into the next one, not having time to react. Finally, the idea that formed to me as a possible improvement was to gradually construct an ever-widening “forbidden” sector: at the first step, this sector would be formed by the 2 tangent lines to the nearest obstacle, then each of this lines would be considered as a potential new route, and recursively checked for obstacles. Having laziness by default in Haskell is actually quite handy oftentimes; in this case, for example, it was easy to build a potentially infinite list of ever-widening “forbidden” sectors, and worry after that how to peruse just a finite portion of this sequence. For lack of better ideas, I actually settled on 2 conditions – take no more than N sectors (N being one of the several parameters controlling my fragile heuristics), and stop if the sectors start to repeat. Speaking of heuristics, let's mention a couple of others: static obstacles were made slightly larger than they actually were, to have some safety margin, and more – craters (being the most dangerous obstacles) were made to appear slightly closer to the vehicle. As for Martians, I could not glean any hints about their behavior neither from the rules, nor from the sample server. Initially I treated them simply as static obstacles, but at some point imagined it would be cheap to do some tricks: make them appear centered not where they are reported to be, but where they would be in one time-slice, keeping current speed, and direction; and also extend their radius to cover an area they may reach in 2 more time-slices.

All was not nice with all these quickly-cooked heuristics. While the code for trying to avoid multiple obstacles at once was ready at about 17:00, it took me till about 20:00 to debug it. Finally it turned out I was bitten by naïve ==0 comparisons on doubles, my only excuse being that it was quite some time ago when I last dabbled in complicated floating-point calculations. Besides, I had to dig through quite unwieldy logs full of coordinates in order to discover the exact problem. At one point I felt so lost that I turned aside to look for some drawing tool that might help me visualize better what was going on. My first choice fell on Asymptote, and I did not regret – it was quick to install and make running, and I was able to see some pictures after just a couple of minutes of reading help files. With that visual help at hand, the problem became clear – my segment-to-circle intersection routine returned 2(!) crossing points (although only slightly different) for the same line segment that my other routine has just calculated as being tangent... Well, it is never too late to get badly bitten by stupid mistakes.

With less than 2 hours to go, I spent some time trying to tune the different heuristics parameters and verifying several times my submission in the LiveCD environment. Finally, I was able to send my final (and only) submission about 40 minutes before the deadline – quite some progress compared to last year.

To sum it up, though it was not love at first sight, I gradually turned liking this year's task a lot. I had a couple of despairing surprises along the run, but as a whole it was a lot of fun. Thanks a lot to the organizers, but also to all the other participants, who kept the contest forums alive, useful, and fun. I am also grateful to all the friends that sympathized with my progress and were always eager to help at least with some advise for lack of other options.