|Anonymous | Login | Signup for a new account||2018-07-22 22:16 CEST|
|Main | My View | View Issues | Change Log | Roadmap|
|View Issue Details|
|ID||Project||Category||View Status||Date Submitted||Last Update|
|0007485||OCaml||middle end (typedtree to clambda)||public||2017-02-16 15:42||2017-07-24 16:06|
|Target Version||Fixed in Version|
|Summary||0007485: Adding an attribute for abstract types that are not float / lazy|
|Description||Currently, 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.
|Tags||No tags attached.|
|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.|
|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.|
edited on: 2017-02-17 04:24
ppedrot: a patch to disable the float-array optimization was proposed
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.
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?
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.
|See https://github.com/ocaml/ocaml/pull/1261. [^]|
|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|