Formal verification of spacecraft control programs

Last February I spent two weeks in Vienna, visiting Jakob Lechner and RUAG Space Austria, a company developing components for space missions. Jakob and his colleagues designed a specialised processing core called REDFIN (REDuced instruction set for Fixed-point & INteger arithmetic) for executing simple spacecraft control tasks, such as satellite antenna pointing. During the visit I implemented a prototype of a formal verification framework to support the development of REDFIN programs. Afterwards I was quite busy with my other projects, but my PhD student Georgy Lukyanov helped to further improve the prototype.

Jakob, Georgy and I have just submitted a conference paper describing the REDFIN core and the verification framework. Please have a look and let us know what you think. This will be a timely read after yesterday’s exciting SpaceX launch.

Continue reading Formal verification of spacecraft control programs

Hadrian is on the way

Hadrian, a new build system for GHC that we have been working on for the past three years, has finally been merged into the GHC tree (update: we have temporally switched to a submodule). However it’s not yet time to celebrate — there are still many issues that need to be addressed before the Make-based build system may retire.

Want to try? Checkout the GHC repository and run hadrian/build.sh -j or hadrian/build.bat -j on Windows and it should build you a GHC binary. In case of problems, have a look at the README and/or raise an issue.

Here is a quick update on the on-going development:

  • Hadrian can build GHC and can already be used as part of the CI infrastructure. However, the resulting binary does not pass the validation. Zhen Zhang is looking into this, but more help is needed.
  • A major refactoring by Moritz Angermann is on the way. Moritz is primarily interested in cross compilation, but to make it work he had to get rid of the ghc-cabal utility, reorganise the build tree, and make numerous other improvements to Hadrian.
  • There is currently no support for binary distribution. Ben Gamari is looking into this issue.
  • Dynamic linking on Windows is not implemented. Tamar Christina has kindly offered help with this.
  • Hadrian source code is still not fully documented and tested, and generally requires some polishing. I am currently taking care of this when not distracted by urgent bug fixes and will appreciate your help in making Hadrian easier to understand and use.

I can’t believe that we seem to approach the finish line! It’s been a long, tedious but also interesting project. Thank you all for helping us get this far, and I hope we’ll celebrate the switch from Make to Hadrian soon.

Old graphs from new types

After I got back from the holiday that I planned in the previous blog post, I spent the whole January playing with the algebra of graphs and trying to find interesting and useful ways of constructing graphs, focusing on writing polymorphic code that can manipulate graph expressions without turning them into concrete data structures. I’ve put together a small toolbox containing a few quirky types, which I’d like to share with you in this blog post. If you are not familiar with the algebra of graphs, please read the introductory blog post first.

Update: This series of blog posts was published as a functional pearl at the Haskell Symposium 2017.

Continue reading Old graphs from new types

Graphs in disguise: from todo lists to build systems

In this blog post we will look at an example of using the algebra of graphs for manipulating sequences of items, which at first sight might not look like graphs, but are actually dependency graphs in disguise. We will develop a tiny DSL for composing todo lists on top of the alga library and will show how it can be used for planning a holiday and, on a more serious note, for writing software build systems. This blog post will partially answer the question about possible applications of the algebra of graphs that was asked in this reddit discussion.

Update: This series of blog posts was published as a functional pearl at the Haskell Symposium 2017.

Continue reading Graphs in disguise: from todo lists to build systems

Graphs à la carte

I received an overwhelming response to the introductory blog post about the algebra of graphs; thank you all for your remarks, questions and suggestions! In the second part of the series I will show that the algebra is not restricted only to directed graphs, but can be extended to axiomatically represent undirected graphs, reachability and dependency graphs (i.e. preorders and partial orders), their various combinations, and even hypergraphs.

Update: This series of blog posts was published as a functional pearl at the Haskell Symposium 2017.

Continue reading Graphs à la carte

An algebra of graphs

Graph theory is my favourite topic in mathematics and computing science and in this blog post I’ll introduce an algebra of graphs that I’ve been working on for a while. The algebra has become my go-to tool for manipulating graphs and I hope you will find it useful too.

The roots of this work can be traced back to my CONCUR’09 conference submission that was rightly rejected. I subsequently published a few application-specific papers gradually improving my understanding of the algebra. The most comprehensive description can be found in ACM TECS (a preprint is available here). Here I’ll give a general introduction to the simplest version of the algebra of graphs and show how it can be implemented in Haskell.

Update: This series of blog posts was published as a functional pearl at the Haskell Symposium 2017.

Continue reading An algebra of graphs

Towards Cloud Build Systems with Dynamic Dependency Graphs

I’ve recently submitted an application to the Royal Society Industry Fellowship scheme, aiming to continue my journey into the world of build systems. Below is the technical section, which I think is worth sharing regardless of the outcome of my application. I’d like to thank Neil Mitchell, Simon Peyton Jones, Simon Marlow and Nick Benton for many enlightening discussions on build systems that helped me understand both the problem and possible approaches to solving it.

Continue reading Towards Cloud Build Systems with Dynamic Dependency Graphs

Build GHC on Windows using Hadrian and Stack

To build GHC on Windows you usually need to jump through a lot of hoops, which may be confusing even for experienced GHC developers.

Hadrian to the rescue!

Hadrian, a new build system for GHC that I’ve been developing, is written in Haskell and can therefore be built and run via Stack that can install appropriate bootstrapping GHC and MSYS2 environment in an automated and robust way. This was first pointed out by Neil Mitchell, and I’ve recently simplified build instructions even further. The latest version of the instructions is maintained here.

Continue reading Build GHC on Windows using Hadrian and Stack

Walking on trees

Yesterday I learned a cool algorithm, which can be intuitively described as follows:

Pick a starting node, walk as far as you can, turn around, and walk as far as you can again.

Doesn’t sound too complicated, right? But it actually solves a non-trivial problem: it finds the diameter of a tree in linear computation time. The diameter of a tree is the length of the longest possible walk on it. For example, the tree below has diameter 8, because the longest walk on it goes through 8 links. There are actually three walks of length 8, we show the one between nodes p and q:

Tree diameter

Continue reading Walking on trees