Mantis Bug Tracker

View Issue Details Jump to Notes ] Issue History ] Print ]
IDProjectCategoryView StatusDate SubmittedLast Update
0007485OCamlmiddle end (typedtree to clambda)public2017-02-16 15:422017-07-24 16:06
Reporterppedrot 
Assigned To 
PrioritynormalSeverityfeatureReproducibilityalways
StatusacknowledgedResolutionopen 
PlatformOSOS Version
Product Version4.04.0 
Target VersionFixed in Version 
Summary0007485: Adding an attribute for abstract types that are not float / lazy
DescriptionCurrently, there is the "ocaml.immediate" attribute to mark an opaque type as not containing any heap-allocated inhabitants. It would be useful to have a similar attribute that marks an opaque type as not being neither float nor lazy (an 'Addr' in Typeopt parlance).

This is important for critical code relying on array manipulation. As of today, opaque types in arrays lead the compiler into generating a lot of boilerplate code that dynamically dispatch considering whether the array contains floating point numbers. This introduces a lot of useless checks, and is responsible for assembly bloat even though one never uses floats.
TagsNo tags attached.
Attached Files

- Relationships
related to 0005361confirmed Syntax to specify that a custom type is never a float 
related to 0007597resolvedfrisch [@@unboxed] for single-constructor, single-field GADT introducing existential type 

-  Notes
(0017295)
ppedrot (reporter)
2017-02-16 15:52

Note that this would also simplify the code of Typeopt, removing a lot of hardwired non-float primitive types that could just be declared as so through attributes in the ML source instead.
(0017296)
xleroy (administrator)
2017-02-16 15:52

An attribute looks like a good way to express this information (contrast with the discussion in 0005361). Still, it has to be checked by the type-checker. A proof-of-concept implementation as a pull request would be welcome.
(0017300)
gasche (developer)
2017-02-17 04:24
edited on: 2017-02-17 04:24

ppedrot: a patch to disable the float-array optimization was proposed

  https://github.com/ocaml/ocaml/pull/163 [^]

Have you tried measuring the performance of Coq using this patch? This seems to be the easiest way to evaluate the potential performance benefits for Coq of what you propose.

(0018110)
frisch (developer)
2017-07-21 15:21

In addition to optimizing array accesses, this would also allow more ocaml.unboxed types.

But I don't think we need to exclude lazy. Claiming that a type cannot be float should be enough, no?
(0018113)
frisch (developer)
2017-07-21 17:04

I think this would be a nice opportunity to clean up the handling of value representation for types. In Types.type_declaration, one would replace the type_immediate field by a field with type:

  type type_representation =
  | Int
  | Float
  | Lazy
  | Non_float  (* values of the type are never represented as floats *)
  | Addr       (* neither float nor lazy *)
  | Generic


The "subtyping" is obvious. An abstract type without manifest is by default Generic but can be annotated through some attribute. The representation would be inferred with something like Typedecl.compute_immediacy.

The logic currently in Typeopt to infer the representation (following unboxed types), the one in Ctype.maybe_poiter and the one in Typedecl.get_unboxed_type_representation (/and Typedecl.is_float) should probably be merged.
(0018132)
ppedrot (reporter)
2017-07-24 16:06

See https://github.com/ocaml/ocaml/pull/1261. [^]

- Issue History
Date Modified Username Field Change
2017-02-16 15:42 ppedrot New Issue
2017-02-16 15:50 xleroy Relationship added related to 0005361
2017-02-16 15:52 ppedrot Note Added: 0017295
2017-02-16 15:52 xleroy Note Added: 0017296
2017-02-16 15:52 xleroy Status new => acknowledged
2017-02-17 04:24 gasche Note Added: 0017300
2017-02-17 04:24 gasche Note Edited: 0017300 View Revisions
2017-02-23 16:42 doligez Category Ocaml optimization => -Ocaml optimization
2017-02-27 15:23 doligez Severity feature => minor
2017-02-27 15:23 doligez Category -Ocaml optimization => middle end (typedtree to clambda)
2017-03-07 13:34 shinwell Severity minor => feature
2017-07-21 15:21 frisch Note Added: 0018110
2017-07-21 17:04 frisch Note Added: 0018113
2017-07-24 08:22 yallop Relationship added related to 0007597
2017-07-24 16:06 ppedrot Note Added: 0018132


Copyright © 2000 - 2011 MantisBT Group
Powered by Mantis Bugtracker