Skip to content

Notes on uniqueness for initial Flambda 2 implementation

Anton Felix Lorenzen edited this page Oct 30, 2024 · 6 revisions

Primitives that allocate in Lambda will be equipped with uniqueness information, c.f. this PR:

type uniqueness_mode = private
  | Alloc_unique (* Might be reused *)
  | Alloc_aliased (* No reuse *)

type alloc_mode = locality_mode * uniqueness_mode

This new mode information will be added to Alloc_mode in Flambda 2.

The uniqueness mode will be used to:

  • disable CSE
  • disable static allocation

Block projections will be marked as Reads_vary by the frontend. This will in particular prevent Flambda 2 from inferring block approximations from them, thus in turn disabling the optimization that elides re-allocation of immutable blocks, if the contents would be the same.

During Cmm translation, the reuse primitives will be treated as full barriers, in the same way as End_region is. In due course we will refine the effect system used by this pass to more properly handle locals and overwriting.

The type checker should mark the minimum number of things as being unique, otherwise degradation of optimization is likely to be widespread.

Conversion from unique to aliased (pchambart)

type t = { field : int }

let get_field (x [@aliased]) = x.field

let update (y [@unique]) n =
  { y with field = n } (* Unique magical update *)

let f (x [@unique]) =
  let z = update x 42 in
  (* conversion from unique to aliased happens here *)
  let field = get_field z in
  field

If internally the magical update is compiled to something similar to that

let update (y [@unique]) n =
  set_field y 0 n;
  y

After inlining, we get

let f (x [@unique]) =
  set_field x 0 42;
  let field = get_field x 0 in 
  field

the get_field must not be moved. But since the get_field comes from an aliased read its original annotation is not sufficient to know that it can't be moved.

mshinwell: the idea is that the set_field here would be one of the overwriting primitives, and this would be a full barrier.

Borrowing (ncourant)

type t = { field : int }

let make_copy (x [@local aliased]) = { field = x.field }

let update (y [@unique]) n =
  { y with field = n } (* Unique magical update *)

let f (x [@unique]) =
  let y = make_copy &x in
  let z = update x 42 in
  (y.field, z.field)

In make_copy, x is local aliased so the read is taken as immutable; { field = x.field } will then be optimized by returning x, but this breaks uniqueness!