Computing connected components in an undirected graph is one of the most basic graph problems. Given a graph with n vertices and m edges, you can find its components in linear time O(n + m) using depth-first or breadth-first search. But what if you need to go faster? In this blog post, I will describe a cool new concurrent algorithm for this problem, which I learned this week at the Heidelberg Laureate Forum from Robert Tarjan himself. The algorithm distributes the work among n + m tiny processors that work concurrently most of the time and requires O(log n) global synchronisation rounds. The algorithm is remarkably simple but it’s far from obvious that it works correctly and efficiently. Happily, Tarjan and his co-author S. Cliff Liu have done all the hard proofs in their recent paper, so we can simply take the algorithm and use it.
Category Archives: research
Build Systems à la Carte
In a recent blog post, I shared a preliminary version of the paper on build systems that Neil Mitchell, Simon Peyton Jones and I submitted to the ICFP 2018 conference. The paper was accepted and yesterday, after months of revisions and polishing, we’ve finally completed this work. The paper and associated executable models are openly available; here is a direct link to the PDF.
Build systems, such as classic Make, are big, complicated, and used by every software developer on the planet. But they are a sadly unloved part of the software ecosystem, very much a means to an end, and seldom the focus of attention. Rarely do people ask questions like “What does it mean for my build system to be correct?” or “What are the trade-offs between different approaches?”. For years Make dominated, but more recently the challenges of scale have driven large software firms like Microsoft, Facebook and Google to develop their own build systems, exploring new points in the design space. In this paper we offer a general framework in which to understand and compare build systems, in a way that is both abstract (omitting incidental detail) and yet precise (implemented as Haskell code).
The Task abstraction
Neil Mitchell, Simon Peyton Jones and I have just finished a paper describing a systematic and executable framework for developing and comparing build systems. The paper and associated code are available here: https://github.com/snowleopard/build. The code is not yet well documented and polished, but I’ll bring it in a good shape in April. You can learn more about the motivation behind the project here.
(Update: the paper got accepted to ICFP! Read the PDF, watch the talk.)
In this blog post I would like to share one interesting abstraction that we came up with to describe build tasks:
type Task c k v = forall f. c f => (k -> f v) -> k -> Maybe (f v)
A Task is completely isolated from the world of compilers, file systems, dependency graphs, caches, and all other complexities of real build systems. It just computes the value of a key k, in a side-effect-free way, using a callback of type k → f v to find the values of its dependencies. One simple example of a callback is Haskell’s readFile function: as one can see from its type FilePath → IO String, given a key (a file path k = FilePath) it can find its value (the file contents of type v = String) by performing arbitrary IO effects (hence, f = IO). We require task descriptions to be polymorhic in f, so that we can reuse them in different computational contexts f without rewriting from scratch.
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
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