Mantis Bug Tracker

View Issue Details Jump to Notes ] Issue History ] Print ]
IDProjectCategoryView StatusDate SubmittedLast Update
0007826OCamlmiddle end (typedtree to clambda)public2018-07-19 14:142018-07-19 18:01
Reporterppedrot 
Assigned To 
PrioritynormalSeverityminorReproducibilityalways
StatusacknowledgedResolutionopen 
PlatformOSOS Version
Product Version4.06.1 
Target VersionFixed in Version 
Summary0007826: Closure computation is quadratic in the number of functions
DescriptionThe 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.
TagsNo tags attached.
Attached Files

- Relationships

-  Notes
(0019257)
ppedrot (reporter)
2018-07-19 14:32

Easy enough to reproduce with a trivial example:

gen.ml:
%%%%%%%%%%%%%%%%%%

let file = "out.ml"

let clos_size = int_of_string Sys.argv.(1)

let rec gen chan n =
  if n = 0 then ()
  else
    let () = Printf.fprintf chan "fun x_%i ->\nlet () = print_newline () in\n" n in
    gen chan (n - 1)

let () =
  let chan = open_out file in
  let () = Printf.fprintf chan "let f =\n%!" in
  let () = Printf.fprintf chan "%a\n%!" gen clos_size in
  let () = Printf.fprintf chan "()\n%!" in
  close_out chan

%%%%%%%%%%%%%%%%%%

$ ocaml gen.ml 5000 && time ocamlopt -c out.ml
2.45user 0.11system 0:02.56elapsed 99%CPU (0avgtext+0avgdata 86292maxresident)k

$ ocaml gen.ml 10000 && time ocamlopt -c out.ml
10.11user 0.22system 0:10.33elapsed 99%CPU (0avgtext+0avgdata 163768maxresident)k

$ ocaml gen.ml 20000 && time ocamlopt -c out.ml
30.02user 0.45system 0:30.48elapsed 99%CPU (0avgtext+0avgdata 319000maxresident)k
(0019259)
xleroy (administrator)
2018-07-19 18:01

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.

- Issue History
Date Modified Username Field Change
2018-07-19 14:14 ppedrot New Issue
2018-07-19 14:32 ppedrot Note Added: 0019257
2018-07-19 18:01 xleroy Note Added: 0019259
2018-07-19 18:01 xleroy Status new => acknowledged


Copyright © 2000 - 2011 MantisBT Group
Powered by Mantis Bugtracker