Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Adding an attribute for abstract types that are not float / lazy #7485

Closed
vicuna opened this issue Feb 16, 2017 · 7 comments
Closed

Adding an attribute for abstract types that are not float / lazy #7485

vicuna opened this issue Feb 16, 2017 · 7 comments

Comments

@vicuna
Copy link

vicuna commented Feb 16, 2017

Original bug ID: 7485
Reporter: @ppedrot
Status: acknowledged (set by @xavierleroy on 2017-02-16T14:52:41Z)
Resolution: open
Priority: normal
Severity: feature
Version: 4.04.0
Category: middle end (typedtree to clambda)
Related to: #5361 #7597

Bug 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.

@vicuna
Copy link
Author

vicuna commented Feb 16, 2017

Comment author: @ppedrot

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.

@vicuna
Copy link
Author

vicuna commented Feb 16, 2017

Comment author: @xavierleroy

An attribute looks like a good way to express this information (contrast with the discussion in #5361). Still, it has to be checked by the type-checker. A proof-of-concept implementation as a pull request would be welcome.

@vicuna
Copy link
Author

vicuna commented Feb 17, 2017

Comment author: @gasche

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

#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.

@vicuna
Copy link
Author

vicuna commented Jul 21, 2017

Comment author: @alainfrisch

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?

@vicuna
Copy link
Author

vicuna commented Jul 21, 2017

Comment author: @alainfrisch

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.

@vicuna
Copy link
Author

vicuna commented Jul 24, 2017

Comment author: @ppedrot

See #1261.

@stedolan
Copy link
Contributor

With flat-float-array (#1294), the possibility that a type might be float no longer slows down array accesses, so this feature no longer seems necessary.

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Projects
None yet
Development

No branches or pull requests

2 participants