Table of Contents

A formally verified incremental cycle detection algorithm: from paper to practice

1 Context

Armaël Guéneau (that's me)

1.1 PhD student at Gallium

1.2 I work on formal proofs of OCaml programs, using Coq

1.3 Goal: write machine checked proofs that particular programs do not have bugs

1.4 What do we prove: correctness, but also asymptotic complexity!

2 Case study: an incremental cycle detection algorithm

"Incremental cycle detection": add edges to a graph, while checking that the graph remains acyclic after each edge insertion.

Let's look at the state of the art:


3 Case study: an incremental cycle detection algorithm (2)

paper_algo_1.png paper_algo_2.png

paper_thm_1.png [ Paper proof … ] paper_thm_2.png [ Paper proof … ]

4 …Six months later

We wrote some actual code: OCaml implementation interface And proved it correct: Coq specifications

5 Now what? Write a paper and move on?

We can do better! This cycle detection algorithm is actually used in practice, in serious projects:

coq-logo2.png Coq (one of the main proof assistants around)

But it uses a more complicated version of the algorithm: future work!

6 Now what? Write a paper and move on? (2)

dune_logo.png (latest trendy build system for OCaml)

In version 1.7.0, introduces its own implementation of the incremental cycle detection algorithm by Bender et al.

Keeps track of "build actions" in a big graph, and uses the algorithm to make sure it stays acyclic.

7 Shipping our verified implementation into Dune

7.1 Easy enough: Dune already had "vendoring" scripts for external dependencies

7.2 Our implementation can be provided as a "drop-in" replacement

7.3 Test and benchmark our implementation vs. the existing one

7.3.1 Found one correctness bug

7.3.2 Our implementation is also 7x faster! (… mainly because no complexity bugs)

7.4 Opened a pull-request, which got merged today!


Author: Thierry Martinez

Created: 2019-03-21 jeu. 16:17

Emacs 25.2.2 (Org mode 8.2.10)