Segfault involving recursive lazy values and GC shortcutting

[lthls]

The following program segfaults:

let f x =
  let rec l =
    let v = lazy x in
    Gc.minor ();
    v
  in
  l
let lazy_one = f 1

What happens is that lazy x is compiled as (makeforward x), as f could be called with float or lazy arguments (otherwise we would get x directly).
This lures Value_rec_check and Value_rec_compiler into thinking that l will always be a block of size 1 with tag Forward_tag.
However, if a GC runs between the moment the value is allocated and the moment it is used to update the dummy value used for compiling recursive bindings, then if the value turns out to be neither a float nor a lazy the GC will shortcut it, and then we will try to update the dummy block using the integer 1.

I don't have a good idea of how to fix that. I think that we could update the environments used in Value_rec_check and Value_rec_compiler to either not consider forward blocks as having a static size (easier to do but may introduce regressions), or to clear the static sizes of forward blocks whenever a non-trivial expression is encountered.

As I said in #13919, I also think that we could completely remove the lazy optimisations from this part of the compiler, making Value_rec_check and Value_rec_compiler simpler, and instead implement them in the backends (or in Simplif, if we don't want to duplicate the implementation).

[gasche]

Ideally we would want that let rec x = lazy ... is always accepted -- adding lazy should be a way to make arbitrary expressions accepted in recursive definitions. So I ideally would try to fix the issue without conservatively marking more values as short-cuttable, which would lead to rejecting more value definitions.

I think that a fix for this issue would be to have a separate caml_update_dummy_lazy primitive -- in the code that generates the caml_update_dummy call we have the size information in which we already store typing information to distinguish floats from other values. If this specialized update function is passed an immediate value, it creates a Forward block.

As I said in #13919, I also think that we could completely remove the lazy optimisations from this part of the compiler, making Value_rec_check and Value_rec_compiler simpler, and instead implement them in the backends (or in Simplif, if we don't want to duplicate the implementation).

This sounds promising and I would be available to help by writing or reviewing changes. But note that the lazy optimisations rely on type information, so we would have to store the summarized type information somewhere during Translcore to be able to do that. The natural choice would be to add them to Pmakelazyblock, I suppose.

[gasche]

This being said, I'm not sure how moving the lazy optimizations later in the pipeline would avoid the present issue. It seems that the problem is that the code generated for recursive values makes assumptions on value representations that are broken by those optimizations. (eg. caml_update_dummy believes that it always get a block argument, but shortcutting Forward can turn blocks into immediates). Wouldn't we get the same issue if we did the optimization later?

[lthls]

This being said, I'm not sure how moving the lazy optimizations later in the pipeline would avoid the present issue. It seems that the problem is that the code generated for recursive values makes assumptions on value representations that are broken by those optimizations. (eg. caml_update_dummy believes that it always get a block argument, but shortcutting Forward can turn blocks into immediates). Wouldn't we get the same issue if we did the optimization later?

If we do all lazy optimisations after recursive value compilation, the criterion for being able to make a forward block instead of a regular lazy block becomes:

• The payload has to be "simple", for some definition of simple (this is more or less what we already have, and is made more obvious with lazy v: optimize structured constants #13919)
• The resulting value must never flow into caml_update_dummy directly. This is a bit annoying to do properly in bytecode, but the native compiler has various passes where computing this is straightforward. I suspect this is actually doable in Simplif if we wanted to, although I'd like to benefit from inlining when making this decision.

What we would lose is the ability to compile forward blocks into their raw contents at compile time based on type information. That could be recovered by computing Typeopt.classify and storing it in the Pmakelazyblock primitive, I think.

I like your suggestion of a dedicated caml_update_dummy_lazy primitive, though. I'll probably try to propose the delayed optimisation because I find it more principled, but if you (or somebody else) want to submit a fix based on the special primitive I'm willing to review or help with the implementation if needed.

[gasche]

If the criterion to optimize is local (it's about the payload of the lazy), I agree we win by moving to Lambda which is a simpler language. But for the non-local part "must not flow into...", this seems fairly fragile even in later stages, and I think we should try to get rid of this non-local criterion completely, for example with this type-directed insertion of lazy-specific dummy logic.

[lthls]

I hope I will be able to show you that the "must not flow" criterion is not that bad, but that will have to wait until I actually have the code.

[gasche]

Note: I cannot reproduce the behavior on this particular test program, I get

>> Fatal error: letrec: No size found for Static binding
Fatal error: exception Misc.Fatal_error

on 5.2 and 5.3 (ocamlc or ocamlopt (closure)).

[gasche]

I propose a fix in #13933 that introduces caml_update_dummy_lazy. I haven't included a testcase yet, I will look for one that I can reproduce.

[gasche]

The failure to reproduce comes from the fact that the bug exists only in trunk and pre-5.2 versions:

• before 5.2 we didn't have the safety of Value_rec_compiler
• in 5.2 and 5.3, the Forward-block constructor is compiled into Lambda with a Popaque primitive applied, and this results in Value_rec_compiler (reasonably) refusing to predict the size of the value
• in trunk, @lthls made the compilation of Forward_block more precise with Pmakelazyblock, and made Value_rec_compiler more precise as well, so the bug is available again

[stedolan]

I'm probably missing something here, but what's the problem with the simple solution of counting Forward blocks as Dynamic instead of Static in Value_rec_check? (They're not static as they change at runtime when the GC runs).

The patch is trivial (below) and it fixes the testcase here. Is the argument against it just that it might reject some previously-accepted programs? Is there a useful such program?

diff --git a/typing/value_rec_check.ml b/typing/value_rec_check.ml
index c5b1d86f11..c9fdf4220b 100644
--- a/typing/value_rec_check.ml
+++ b/typing/value_rec_check.ml
@@ -221,7 +221,7 @@ let classify_expression : Typedtree.expression -> sd =
       | `Float_that_cannot_be_shortcut
       | `Identifier `Forward_value ->
           (* Forward blocks *)
-          Static
+          Dynamic
       | `Identifier `Other ->
           classify_expression env e
       | `Other ->
diff --git a/lambda/value_rec_compiler.ml b/lambda/value_rec_compiler.ml
index 00cd66add6..4f154ce01f 100644
--- a/lambda/value_rec_compiler.ml
+++ b/lambda/value_rec_compiler.ml
@@ -219,8 +219,10 @@ let compute_static_size lam =
            Note that flat float arrays/records use Pmakearray, so we don't need
            to check the tag here. *)
         Block (Regular_block (List.length args))
-    | Pmakelazyblock _ ->
+    | Pmakelazyblock Lazy_tag ->
         Block (Regular_block 1)
+    | Pmakelazyblock Forward_tag ->
+        dynamic_size ()
     | Pmakearray (kind, _) ->
         let size = List.length args in
         begin match kind with

[gasche]

Yes, my issue with that approach is that it starts rejecting more program if we optimize more lazy e into forward blocks. In particular it is in tension with #13919 that tries to shortcut more expressions. let rec x = lazy e is a systematic approach to make many more terms usable in recursive definitions. I would like to preserve the property that this pattern is broadly accepted, instead of exposing the behavior of the optimizer (or restricting it) to delineate the cases that are or are not accepted.

More importantly, it is fundamentally invalid to assume that non-shortcut lazy e blocks are Static if we assume that forward blocks are Dynamic, because of examples of the form let rec x = let v = lazy e in ...; v. The rec-check analysis as formulated will use the same static-or-dynamic value for x and for v, which is correct when Static indicates data constructors that remain around forever, but invalid for lazy blocks that may be shortcut at runtime during the ... part. This is a compounding issue that was identified by @lthls in the discussion of my proposed fix #13933 -- he was worried about the case where v gets forced concurrently, which is maximum fun.

[stedolan]

Yes, my issue with that approach is that it starts rejecting more program if we optimize more lazy e into forward blocks. In particular it is in tension with #13919 that tries to shortcut more expressions. let rec x = lazy e is a systematic approach to make many more terms usable in recursive definitions. I would like to preserve the property that this pattern is broadly accepted, instead of exposing the behavior of the optimizer (or restricting it) to delineate the cases that are or are not accepted.

That doesn't sound right to me. #13919 is about let rec x = lazy e when e does not mention x. In such cases, the Value_rec check will pass regardless of whether the lazy value is Static or Dynamic, as there's no value recursion involved.

Do you have an example of a term that this change would reject?

More importantly, it is fundamentally invalid to assume that non-shortcut lazy e blocks are Static if we assume that forward blocks are Dynamic, because of examples of the form let rec x = let v = lazy e in ...; v. The rec-check analysis as formulated will use the same static-or-dynamic value for x and for v, which is correct when Static indicates data constructors that remain around forever, but invalid for lazy blocks that may be shortcut at runtime during the ... part. This is a compounding issue that was identified by @lthls in the discussion of my proposed fix #13933 -- he was worried about the case where v gets forced concurrently, which is maximum fun.

Thanks, I hadn't seen that class of examples.

In any such example, the term e will have to be nonrecursive. (If it mentioned x then forcing it in the ... section would fail the Value_rec_check). So could we classify it as Static or Dynamic based on whether there was a recursive use of the bound variable? (If there is, it must be Static, since a recursive lazy cannot be forced before it is defined. If there is not, making it Dynamic doesn't rule out any programs, as far as I can tell)

[gasche]

The meaning of the Static/Dynamic analysis is to know if we can pre-allocate dummy blocks for the values, independently of their (non-)dependencies on recursive names. I wouldn't want to start mixing the two concerns.

(Note: let forever v = let rec cy = lazy Cons(v, cy) in cy is an example of recursive value where the optimization of #13919 would apply, with Cons : 'a * 'a lazy_list -> 'a lazy_list_cell.)

[lthls]

The kind of examples that would start being rejected if we treated lazy constructors as Dynamic look like that:

let rec x =
  let _ = Some x in
  lazy 0.

I don't expect anybody has actually written something like that, of course, but that's the kind of annoying corner case caused by Value_rec_check's allow-everything-we-can design.

[stedolan]

The meaning of the Static/Dynamic analysis is to know if we can pre-allocate dummy blocks for the values, independently of their (non-)dependencies on recursive names. I wouldn't want to start mixing the two concerns.

But these don't seem to in fact be independent?

(Note: let forever v = let rec cy = lazy Cons(v, cy) in cy is an example of recursive value where the optimization of #13919 would apply, with Cons : 'a * 'a lazy_list -> 'a lazy_list_cell.)

let rec x = let _ = Some x in lazy 0

Both of these examples are accepted with Forward_tag values treated as Dynamic. (The former, because there are no Forward_tag values, and the latter, because there is no recursive use under the Forward_tag).

[lthls]

and the latter, because there is no recursive use under the Forward_tag

If I remember correctly, any occurrence of the recursive variable, even in positions where it is not actually used, is forbidden for Dynamic bindings.
I believe that rule is intended to prevent silly code like let rec univ : type a b. (a, b) Type.eq = let Equal = univ in Equal (but I might be wrong).