Mantis Bug Tracker

View Issue Details Jump to Notes ] Issue History ] Print ]
IDProjectCategoryView StatusDate SubmittedLast Update
0007345OCamlback end (clambda to assembly)public2016-09-08 13:072017-10-10 10:53
Reportershinwell 
Assigned To 
PrioritynormalSeverityminorReproducibilityalways
StatusacknowledgedResolutionopen 
PlatformOSOS Version
Product Version4.04.0 +dev / +beta1 / +beta2 
Target VersionlaterFixed in Version 
Summary0007345: Some GADT matches cause closure allocation with ocamlc -g
DescriptionIt looks like let bindings introduced to alias function parameters holding constructed values of inline record type cause debugging events to be inserted that subsequently cause closure allocation. The allocations happen because the code for combining closures in Simplif (see simplif.ml:464) won't apply owing to the intervening events.

This doesn't happen from 4.04 onwards with native code after the changes to remove debugging events in that context. It still happens with bytecode, however.

For the example below:

     f/1207 =
       (function param/1281
         (funct-body inline_allocation.ml(10)<ghost>:130-153
           (let (a/1209 =a param/1281) (* this let causes the problem *)
             (before inline_allocation.ml(10)<ghost>:136-153
               (function z/1210
                 (funct-body inline_allocation.ml(10)<ghost>:136-153
                   (before inline_allocation.ml(11):142-153
                     (after inline_allocation.ml(11):142-153
                       (apply equal/1204 (field 0 a/1209) z/1210)))))))))
Steps To ReproduceCompile and run the following using ocamlc (not ocamlopt).
The answer should be zero, but it prints four.

type _ t =
  | A : { x : int } -> [`A] t
  | B : [`B] t

let _unused_constr = B

let equal (x : int) (y : int) =
  x = y

let f (A a) z =
  equal a.x z

let t = A { x = 5 }

let () =
  let start = Gc.minor_words () in
  let (_res : bool) = f t 3 in
  let stop = Gc.minor_words () in
  Printf.printf "%f\n" (stop -. start -. 2.)
TagsNo tags attached.
Attached Files

- Relationships
related to 0007384resolvedfrisch the optimization of optional arguments never applies with -g 

-  Notes
(0016699)
xleroy (administrator)
2016-12-07 12:36

Just from reading the description of this PR, not going back to the code:

- It is strange that debugging events are inserted for these compiler-generated "let"s. Are those "let"s of the correct kind? (In the sense of type Lambda.let_kind.) Do we need an extra "let" kind?

- Playing devil's advocate: so we have a slight performance degradation in bytecode when compiled with -g. Who really cares?
(0017334)
xleroy (administrator)
2017-02-18 17:22

Playing some more with the repro case:

- Inline records are innocent: take

type t = A of {x: int}

in your example and the intermediate closure goes away.

- GADTs have something to do with it. If t is not a GADT

type t = A of {x: int} | B

you get lambda code of the form

     f/1211 =
       (function param/1214
         (if param/1214
           (function z/1213 (apply equal/1208 (field 0 param/1214) z/1213))
           (raise (makeblock 0 (global Match_failure/17g) [0: "gee.ml" 8 6])))))

even if -g is not given. That makes sense because f must take one argument, check that it is indeed an A, then return a function taking the second parameter. Taking the two parameters at once then doing the matching on the first would be semantically incorrect.

With a GADT, the "B -> raise Match_failure" branch is eliminated, I don't know where, but the debug event was already inserted.

For the time being I'm pushing this to 4.06. But I suggest to close this PR as not worth fixing.
(0018527)
xleroy (administrator)
2017-10-10 10:53

This issue won't be looked at in time for 4.06. I move it to "later" as I doubt anyone really cares about it.

- Issue History
Date Modified Username Field Change
2016-09-08 13:07 shinwell New Issue
2016-09-08 13:07 shinwell Status new => acknowledged
2016-09-08 13:07 shinwell Target Version => 4.05.0 +dev/beta1/beta2/beta3/rc1
2016-10-13 08:51 shinwell Relationship added related to 0007384
2016-12-07 12:36 xleroy Note Added: 0016699
2017-02-18 17:22 xleroy Note Added: 0017334
2017-02-18 17:22 xleroy Target Version 4.05.0 +dev/beta1/beta2/beta3/rc1 => 4.06.0 +dev/beta1/beta2/rc1
2017-02-18 17:22 xleroy Summary Inline record matches cause closure allocation => Some GADT matches cause closure allocation with ocamlc -g
2017-02-23 16:35 doligez Category OCaml backend (code generation) => Back end (clambda to assembly)
2017-02-23 16:44 doligez Category Back end (clambda to assembly) => back end (clambda to assembly)
2017-10-10 10:53 xleroy Note Added: 0018527
2017-10-10 10:53 xleroy Target Version 4.06.0 +dev/beta1/beta2/rc1 => later


Copyright © 2000 - 2011 MantisBT Group
Powered by Mantis Bugtracker