pres
Table of Contents
- 1. Context
- 2. Case study: an incremental cycle detection algorithm
- 3. Case study: an incremental cycle detection algorithm (2)
- 4. …Six months later
- 5. Now what? Write a paper and move on?
- 6. Now what? Write a paper and move on? (2)
- 7. Shipping our verified implementation into Dune
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 proof … ]
[ 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 (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)
(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!
