Join GitHub today
GitHub is home to over 31 million developers working together to host and review code, manage projects, and build software together.Sign up
Closure computation is quadratic in the number of functions #7826
Original bug ID: 7826
The Closure.close_functions function computes the set of free variables of its arguments, which is O(n). Unluckily this function is recursive and it subcalls can do the same, which leads to a runtime quadratic in the number of nested abstraction nodes.
I doubt this is an issue in handwritten code, but the problem sure happens in generated code. I hit it in the native compilation scheme of Coq code from fiat-crypto, and the compiler takes ages for a term that is big but not crazy either (~ 500kloc of sparse code, every line being a constructor most of the time).
I do not have a small reproducible test-case at hand, this would require extracting it from the generated code and making it standalone, which is not easy.
Comment author: ppedrot
Easy enough to reproduce with a trivial example:
let file = "out.ml"
let clos_size = int_of_string Sys.argv.(1)
let rec gen chan n =
let () =
$ ocaml gen.ml 5000 && time ocamlopt -c out.ml
$ ocaml gen.ml 10000 && time ocamlopt -c out.ml
$ ocaml gen.ml 20000 && time ocamlopt -c out.ml
Comment author: @xavierleroy
Yes, this is one of the many quadratic behaviors in ocamlopt. (There are exponential behaviors too.) They are never encountered by hand-written code and sometimes encountered by auto-generated code. As a consequence, nobody feels a strong urge to rewrite from scratch with more efficient algorithms when they exist.