As part of my PhD at Gallium, I have been working on formally proving OCaml programs using Coq. More precisely, the focus has been on proving not only that a program is functionally correct (always compute the right result), but also does so in the expected amount of time. In other words, we are interested in formally verifying the asymptotic complexity of OCaml programs.
In this blog-post, I’m happy to report on our latest endeavour: the verification of the correctness and (amortized) complexity of a state-of-the art incremental cycle detection algorithm.
This is joint work with Jacques-Henri Jourdan and my advisors François Pottier and Arthur Charguéraud.
The initial motivation for this work comes from the implementation of Coq itself! More specifically, efficiently checking the consistency of universe constraints that result from the type-checking phase is a difficult problem, that can be seen as an incremental cycle detection problem. A few years ago, Jacques-Henri reimplemented the part of Coq responsible for this, following a state-of-the-art algorithm published by Bender, Fineman, Gilbert and Tarjan. They prove that using their algorithm, adding an edge in a graph with m edges and n nodes while ensuring that after each addition the graph remains acyclic has amortized asymptotic complexity O(min (m1/2, n2/3)). In the common case where the graph is sparse enough, this is equivalent to O(√m).
Jacques-Henri’s implementation resulted in a nice speedup in practice, but it is not so easy to convince oneself that it indeed has the right asymptotic complexity in all cases (in other words, that it does not have a “complexity bug”). The amortized analysis required to establish the O() bound on paper is quite subtle, and for instance relies on a parameter Δ computed at runtime that looks quite magical at first glance.
In the work I’m presenting here, we try to untangle this mystery. We give a formally verified OCaml implemention for a (slightly modified) incremental cycle detection algorithm from Bender et al. We prove that it is not only correct, but also satisfies the expected complexity bound.
Note that this is not yet the exact algorithm that is currently part of Coq’s implementation, but still an important milestone on the way there! (Coq implements the variant by Bender et al. that additionally maintains “strong components”. We believe it could be implemented and verified in a modular fashion, by combining the algorithm we present here and a union-find data structure.)
Here’s the draft (currently under submission), and a link to the OCaml code and Coq proofs:
We exploit Separation Logic with Time Credits to verify the correctness and worst-case amortized asymptotic complexity of a state-of-the-art incremental cycle detection algorithm.