Uniqueness mode by anfelor · Pull Request #33 · ocaml-flambda/ocaml-jst

anfelor · 2022-07-05T13:04:45Z

This PR tracks the ongoing development of uniqueness mode.

…not build)

lpw25

The test cases look good

testsuite/tests/typing-local/unique.ml

anfelor · 2022-07-14T12:38:02Z

typing/printtyped.ml

-  | None -> line i ppf "value_mode <modevar>\n");
+  ( let consts = Btype.Value_mode.check_const x.exp_mode in
+    line i ppf "value_mode ";
+    line 0 ppf (match fst consts with


This is somewhat ugly as I couldn't find a way to combine two format strings (the way '^' acts on normal strings). Is there a nice operator for that?

There is but generally I try to avoid it. I would write this by lifting out these two matches into functions called fmt_locality and fmt_uniqueness and then call them using %a. I'd also avoid using fst and snd by replacing let consts with let locality, uniqueness.

lpw25

Looks good so far

lpw25 · 2022-07-14T13:34:27Z

typing/printtyped.ml

-  | None -> line i ppf "value_mode <modevar>\n");
+  ( let consts = Btype.Value_mode.check_const x.exp_mode in
+    line i ppf "value_mode ";
+    line 0 ppf (match fst consts with


There is but generally I try to avoid it. I would write this by lifting out these two matches into functions called fmt_locality and fmt_uniqueness and then call them using %a. I'd also avoid using fst and snd by replacing let consts with let locality, uniqueness.

parsing/parser.mly

lpw25 · 2022-07-18T09:17:33Z

parsing/parser.mly

 ;
-fun_binding:
-    strict_binding
+fun_binding_gen(wrap):


I think we should spend a bit more time trying to find a simpler solution to this part. The simplest approach that might work would be to separate out the list of parameters from the final EQUAL seq_expr or type_constraint EQUAL seq_expr in a strict_binding. That would allow the type_constraint to get treated differently depending on context. Probably that will require adding a type like:

type parameter = | Ordinary of arg_label * expression option * pattern | Type of Longident.t list

to represent the parameters before they are folded onto the body expression.

Flagging this as not implemented as of 0d0c78b

typing/typecore.ml

lpw25

I've looked over all of parsing and typing again

lpw25 · 2022-08-11T12:57:23Z

parsing/parser.mly

  Exp.mk ~loc:Location.none (Pexp_extension(local_ext_loc, PStr []))

-let mkexp_stack ~loc exp =
+let mkexp_stack  ~loc exp =


Looks like an accidental whitespace change

lpw25 · 2022-08-11T13:12:57Z

typing/mode.mli

+(*   the GNU Lesser General Public License version 2.1, with the          *)
+(*   special exception on linking described in the file LICENSE.          *)
+(*                                                                        *)
+(**************************************************************************)


Leaving it like this is fine.

lpw25 · 2022-08-11T13:16:45Z

typing/mode.ml

+  let newvar () = Amodevar (fresh ())
+
+  let newvar_below = function
+    | Amode c when L.eq_const c L.min_const -> Amode L.min_const, false


Amode L.min_const is already available as min_mode.

lpw25 · 2022-08-11T13:26:23Z

typing/mode.ml

+  let newvar_below { locality; uniqueness } =
+    let l = Locality.newvar_below locality in
+    let u = Uniqueness.newvar_below uniqueness in
+    { locality = fst l; uniqueness = fst u }, snd l || snd u


Better to use patterns to destruct tuples than to use projections

lpw25 · 2022-08-11T13:34:57Z

typing/printtyp.ml

+    | Some Global -> Olm_global
+    | Some Local -> Olm_local
+    | None -> Olm_unknown
+  and uniqueness = match uniqueness with


Gratuitous and

lpw25 · 2022-08-26T09:09:38Z

typing/typecore.ml

+               and the update is not unique *)
+            let is_unique_with = has_unique_attr_exp sexp in
+            let expected_mode = if is_unique_with
+              then mode_unique (mode_subcomponent expected_mode).mode


This doesn't need the mode_subcomponent. That is needed when we do an allocation, but here we are really doing a mutation.

lpw25 · 2022-08-26T09:12:47Z

typing/typecore.ml

      in
      let closed = (opt_sexp = None) in
-      let rmode = Value_mode.regional_to_global expected_mode.mode in
+      let rmode = Mode.Value.regional_to_global expected_mode.mode in


This mode needs to be different if this is a { unique_ ... with ... } expression. The values used for these fields might be escaping an unknown number of regions, just like for a mutation. That means that they will need to be at a global mode.

lpw25 · 2022-08-26T09:59:57Z

typing/typecore.ml

-        | Global -> Value_mode.global
-        | Nonlocal -> Value_mode.local_to_regional rmode
+        | Global -> Mode.Value.global (* lbl_global==Global also implies Shared *)
+        | Nonlocal -> Mode.Value.local_to_regional rmode


lbl_global==Nonlocal should also imply Shared

lpw25 · 2022-08-26T10:01:39Z

typing/typecore.ml

+        | Nonlocal -> Mode.Value.local_to_regional rmode
        | Unrestricted -> rmode
      in
+      let mode, _ = Mode.Value.newvar_above mode in


We shouldn't bother making this new mode variable if the label is global. Maybe we should also only do it if the srecord is an ident or a projection from an ident (or a projection from a projection from ...).

We should also only make a variable for the uniqueness part, rather than for the whole mode.

Maybe we should also only do it if the srecord is an ident or a projection from an ident (or a projection from a projection from ...).

I have not implemented this.

lpw25 · 2022-08-26T11:08:47Z

typing/typecore.ml

+  if has_local || has_unique then begin
+    let mode = match has_local, has_unique with
+      | true, true -> Mode.Alloc.local_unique
+      | true, false -> Mode.Alloc.local


I think that this case (and the one below) is too restrictive. It should probably have a variable for its uniqueness. That will allow code like the following (maybe put this in the testsuite):

let foo : local_ unique_ string -> unit = fun (local_ s) -> () let bar : local_ unique_ string -> unit = fun (unique_ s) -> ()

The additional variable (and the assert false below) could also be avoided by pulling the equality constraint up into these branches and using more specific equality functions (e.g. using equality on just locality rather than the whole mode).

…rrect handling of named args)

lpw25

I made a review pass over the middle-end and back-end parts.

lpw25 · 2022-09-01T20:39:46Z

lambda/translcore.ml

         They could be Alloc_local, but that would require changes
         to pattern typing, as patterns can close over them. *)
-      Lprim (Pmakeblock (Obj.object_tag, Immutable_unique, None, alloc_heap),
+      Lprim (Pmakeblock (Obj.object_tag, Immutable, None, alloc_heap_unique),


I think this part should be reverted. For annoying reasons that may go away one day Immutable_unique is not quite the same as Immutable and alloc_heap_unique.

lpw25 · 2022-09-01T20:54:57Z

lambda/lambda.mli

+  | Alloc_shared
+
+(* CR-soon: This can be private once it is possible to pattern-match on private aliases *)
+type alloc_mode = locality_mode * uniqueness_mode


I think that the alloc_modes in Lsend, lfunction and lambda_apply can all be replaced by just locality_modes. This is because they are all related to the allocation mode of closures, and closures can't actually be mutated even if they are unique. I think the uniqueness part of those modes is currently just being ignored.

The one in Assignment can also probably just be a locality_mode. I don't think uniqueness affects the write barrier.

lpw25 · 2022-09-01T20:59:32Z

lambda/translcore.ml

@@ -553,7 +555,7 @@ and transl_exp0 ~in_new_scope ~scopes e =
              Lprim (Pmakearray (kind, Immutable, mode), ll,


I think that the mode here should probably always be global_shared. This value can't be local and it will never be used uniquely: it is only used as a template for making new values of mode mode.

lpw25 · 2022-09-01T21:06:51Z

lambda/translcore.ml

+  let maybe_unique_update_on =
+    match opt_init_expr with
+    | None -> None
+    | Some exp -> match Builtin_attributes.has_unique exp.exp_attributes with


It would be good to have opt_init_expr already have some explicit data saying whether the update is a unique one. It's best if we only actually check for attributes once in the type-checker, and after that use normal types and data.

lpw25 · 2022-09-01T21:15:43Z

lambda/translcore.ml

+                                     (fun (_, r) -> match r with
+                                        | Reuse_keep -> false
+                                        | Reuse_set _ -> true)
+                                     (List.combine ll reuses)) in


You can use List.filter_map to make this simpler.

lpw25 · 2022-09-01T21:26:58Z

lambda/translcore.ml

+      | Ok false | Error _ -> None
+      | Ok true -> Some (transl_exp ~scopes exp) in
+  let is_unique_update_on =
+    match maybe_unique_update_on with | None -> false | Some _ -> true in


I think it would be better to just have is_unique_update_on and get rid of maybe_unique_update_on.

lpw25 · 2022-09-01T21:29:16Z

lambda/translcore.ml

+                Lprim(Pmakeblock(0, mut, Some (Pgenval :: shape), mode),
+                      slot :: ll, loc)
+            end
+        | Some id ->


I think it would be better to use Lvar init_id in place of id and then bind that to the init expression, just like in the non-unique case.

lpw25 · 2022-09-01T21:30:01Z

lambda/translcore.ml

-    begin match opt_init_expr with
-      None -> assert false
+    begin match opt_init_expr, maybe_unique_update_on with
+    | None, _ | _, Some _ -> lam


So this case would become just | None -> and not match on maybe_unique_update_on

lpw25 · 2022-09-01T21:47:28Z

asmcomp/printcmm.ml

-  | Calloc Alloc_heap -> "alloc" ^ location d
-  | Calloc Alloc_local -> "alloc_local" ^ location d
+  | Calloc (Alloc_heap, _) -> "alloc" ^ location d
+  | Calloc (Alloc_local, _) -> "alloc_local" ^ location d


I think that we probably can just use locality_mode rather than alloc_mode for everything in cmm. That's because there is no lifting of allocations after this point, so we only need to know whether to put them on the stack or the heap.

lpw25 · 2022-09-01T21:48:23Z

asmcomp/printmach.ml

+  | Ialloc { bytes = n; mode = Alloc_heap, _ } ->
    fprintf ppf "alloc %i" n;
-  | Ialloc { bytes = n; mode = Alloc_local } ->
+  | Ialloc { bytes = n; mode = Alloc_local, _ } ->


As with cmm, we probably only need locality_mode in the mach IR.

…ns/etc

anfelor · 2022-09-09T15:09:10Z

To release this the following items should be completed:

There is currently a bug in matching.ml where matches on record fields are bound to a Llet(Alias, _, _, _, _). These let-aliases can be inlined to the place where the bound variable is used if the bound variable is used only once. However, this usage site might come after an overwrite of the record by the { unique_ x with ... } construct. As such, this is unsound and can lead to bugs. Equally, later stages of the compiler might do similar transformations and it should be checked that that is disabled for unique values. To fix the first bug, however, it suffices to make the handling of unique fields in matching.ml more similar to that of mutable fields (grep for lbl_mut).
With uniqueness analysis the order of evaluation matters. In the spirit of point one, consider ({ unique_ x with foo = ... }, x.foo). Thanks to Ocaml's right-to-left evaluation order this is actually sound -- the field foo of x is accessed before it is overwritten for the first tuple entry. However, we should not codify this evaluation order in the uniqueness analysis. As such, all occurrences of fold_right in the current uniqueness analysis should be changed to pass the uenv to a map and later merge.
We currently do not mark borrowed contexts as shared that also contain a unique use of the borrowed variables (e.g. in a separate branch). While this is sound, it can be surprising to users why their code should fail when they delete a branch. See the test borrow_overwritten_by_once in unique.ml as an example. This can be fixed by constraining the current context as global as soon as we see a borrowed use.

Extends Lambda.function_kind to track modes of curried functions. The supported modes have a heap-returning prefix, followed by a local-returning suffix, both of which may be empty. Functions which do not fit this pattern cannot be expressed as a single Lfunction, and must be explicitly curried in Lambda and Clambda. (See the new Lambda.check_lfunction for the exact invariants) Most of the changes are straightforward plumbing of the new info. Some delicate changes are needed to preserve the new invariants, in: - simplif.ml: optimisations which combine Lfunctions - translcore.ml: transl_curried_function and friends - closure.ml: optimisations for partial and over-application - cmm_helpers.ml: mode-aware variants of caml_curry Caveat: build_apply in translcore is wrong

lpw25 · 2023-08-18T10:24:51Z

Closed in favour of #138, which has now been merged in the other repo. We still need to add borrowing and support for in-place record update.

Anton Lorenzen added 6 commits July 5, 2022 13:50

Initial work on uniqueness mode: Working syntax and some tests

25eaf54

Fix typos in unique.ml

7ebe8c9

Idea for integrating uniqueness

f5afbc3

Integrate changes for uniqueness mode into compiler (but stdlib does …

c5804bb

…not build)

Add missing cases in printtyp.ml

93e6e69

Use Shared everywhere to get old behaviour

31dc0af

lpw25 reviewed Jul 8, 2022

View reviewed changes

testsuite/tests/typing-local/unique.ml Outdated Show resolved Hide resolved

testsuite/tests/typing-local/unique.ml Show resolved Hide resolved

testsuite/tests/typing-local/unique.ml Outdated Show resolved Hide resolved

testsuite/tests/typing-local/unique.ml Outdated Show resolved Hide resolved

Anton Lorenzen added 17 commits July 8, 2022 12:12

Bootstrap

84496de

Add vars for uniques

9848fd3

Fix unique.ml testsuite

a5d8de9

Updated dependencies

cd28d57

Bootstrap

05eec48

Enable newvars

35292df

Cleanup and print uniqueness info

11aefc7

Enable joins

97aa6e2

Add formatting changes to testsuite

c0f95dc

Propagate uniqueness information somewhat further into the type checker

a6bd623

Convert structural eq on (lattice) modes to manual eq_const.

af3b5c4

Uniqueness in mode inference

c231f55

New test and look behind uniqueness extensions appropriately

b193df3

Bootstrap

b0dd422

Add real behavior in unique.ml test

0a724e8

Force unique returns in the type

fcfc53c

Cleanup; ready for first review

43254bf

anfelor commented Jul 14, 2022

View reviewed changes

First draft with pattern matching and datatypes defined

44b0ae0

lpw25 reviewed Jul 19, 2022

View reviewed changes

Anton Lorenzen added 3 commits July 22, 2022 16:28

More progress

6e0d665

More progress

671dedc

Fix bugs and todos

c46470b

Anton Lorenzen added 5 commits August 16, 2022 20:24

Some more review feedback implemented + rbtree example

0beadbb

Bugfixes

4878543

Bootstrap

f93466d

Add other expression to error messages

bcd3642

Cleanup: remove mode from Tpat_var and Tpat_alias

9bc99c2

lpw25 reviewed Aug 26, 2022

View reviewed changes

Anton Lorenzen added 9 commits August 30, 2022 15:52

New uniqueness analysis

12a60c6

Bootstrap

00a57dd

Fix various bugs

40171f7

Allow foo/bar as suggested in code review

81bd847

Bootstrap

3a3dfe7

First draft of currying (but with no checks for applications and inco…

1cab7be

…rrect handling of named args)

Bootstrap

53047c7

Fix wrong arg_mode used for constraining arr_mode

4f91c21

Currying for uniqueness done

2b2ebf7

lpw25 reviewed Sep 1, 2022

View reviewed changes

Anton Lorenzen added 9 commits September 2, 2022 11:26

Implement review suggestions and fix gc_soundness_bug

0144c98

Implement middle-end and back-end review suggestions

4cb1010

Add reason to uniqueness lock for better errors in loops/comprehensio…

b0b0d04

…ns/etc

Bootstrap

4ab4c85

Fix some bugs in uniqueness analysis

f3f5694

Borrowing and some bugfixes

8566793

Bootstrap

cd44e63

Add more comments

9c43b80

Give test better name

5ca45dd

riaqn mentioned this pull request Feb 3, 2023

add unique extension #116

Closed

lpw25 closed this Aug 18, 2023

		@@ -553,7 +555,7 @@ and transl_exp0 ~in_new_scope ~scopes e =
		Lprim (Pmakearray (kind, Immutable, mode), ll,

Conversation

anfelor commented Jul 5, 2022 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

lpw25 left a comment

Choose a reason for hiding this comment

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

lpw25 left a comment

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

lpw25 left a comment

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

lpw25 left a comment

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

anfelor commented Jul 5, 2022 •

edited

Loading