Skip to content

The Pattern-Matching Bug: introduce a temporality heuristic to de-pessimize certain programs#13154

Merged
gasche merged 1 commit intoocaml:trunkfrom
gasche:matching-bug-temporality-heuristic
Sep 12, 2024
Merged

The Pattern-Matching Bug: introduce a temporality heuristic to de-pessimize certain programs#13154
gasche merged 1 commit intoocaml:trunkfrom
gasche:matching-bug-temporality-heuristic

Conversation

@gasche
Copy link
Copy Markdown
Member

@gasche gasche commented May 7, 2024

(This PR sits on top of #13152 and #13153; for now it is best reviewed by looking only at the latest commit.)

#13152 pessimizes Total matches in transitively mutable position. It gives two examples of code that now generates worse code:

(* case (A) *)
let f : bool option ref -> ... = function
| { contents = None } -> ...
| { contents = Some true } -> ...
| _ when guard () -> ...
| { contents = Some false } (* here *) -> ...

type _ gadt = Int : int t | Bool : bool t

(* case (B) *)
let g : int gadt ref -> ... = function
| { contents = Int } (* here *) -> ...

In the case A, the generated code first checks something about the argument root.0, then it checks a guard, then it goes back to the argument root.0. (We say that there are two "splits", resulting in three submatrices, that are checked in sequence.) When it goes back to root.0, its value could have changed in the meantime, so assuming that root.0.0 could only be false is wrong, and we really needed to make the code worse.

In the case B, the generated code reads the mutable field root.0, then immediately checks all possible cases on this constructor. In this case there cannot have been any mutation "in the meantime", this is the first time ever that we are checking this value. So generating a Match_failure case here was not necessary, and we are generating worse code than we could.

In general it is hard to know for sure "this is the first time we do something on this value". Tracking this precisely might be done with more context information, but it would be a tricky change with quickly diminishing returns. There is however a case where it is very easy to see that we are in this situation: where we have not generated any "split", any logic of the form "check this about the first value, and if that fails check that".

The present PR introduces a new piece of static context information used by the pattern-matching compiler to track this criterion. In code:

type temporality =
  | First
  | Following
(** The [temporality] information tracks information about the
    placement of the current submatrix within the
    whole pattern-matching.

    - [First]: this is the first submatrix on this position seen by values
      that flow into the submatrix.
    - [Following]: there was a split, some other submatrix was tried first
      and failed, and the control jumped to the current submatrix.

    This information is used in {!compute_arg_partial}.
*)

When deciding whether a switch on a given position should be pessimized, we now use a refined criterion: we are in a transitively mutable position and the current temporality is Following, we have already accessed this position before.

In particular, the example g above now produces good code again, as well as any reasonable usage of GADTs in mutable positions that I can think of.

It is, of course, possible to build examples where the heuristic is too coarse-grained and which will generate worse code than they could. For example:

type _ gadt = Int : int t | Bool : bool t

let test : int gadt ref -> unit = function
  | _ when Random.bool () -> ()
  | { contents = Int } -> ()

Copy link
Copy Markdown
Contributor

@ncik-roberts ncik-roberts left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

The approach looks correct. In a survey of a large codebase, I found only one instance where this PR de-pessimizes a program -- I would consider arguing against this change if it significantly complicated the matching.ml code, but given that the change is clear and well-structured, I'm in favor of merging it.

@gasche
Copy link
Copy Markdown
Member Author

gasche commented Jul 31, 2024

One reason I like this heuristic is that it helps me reason about "structural matches" that do not contain splits -- all possible cases are explored in full. For example:

function
| None -> 0
| Some {contents = A} -> 1
| Some {contents = B _} -> 2
| Some {contents = C _} -> 3

(assuming the type-checker finds this example exhaustive: A, B of ..., C are the only valid constructors at the specific type involved -- it could be a GADT with other, incompatible constructors.)

For this fragment of pattern-matching programs, the type-checker exhaustiveness analysis is always correct, and the temporality heuristic guarantees that we generate good code.

@gasche gasche force-pushed the matching-bug-temporality-heuristic branch 2 times, most recently from d727011 to 47c16ae Compare July 31, 2024 20:05
@gasche
Copy link
Copy Markdown
Member Author

gasche commented Jul 31, 2024

Rebasing this on top of #13338 (transitively) made the implementation quite a bit less invasive, because I can add the temporality as an extra field to the partiality record instead of passing it along as before.

@gasche gasche force-pushed the matching-bug-temporality-heuristic branch 2 times, most recently from 73fef1d to 522abfb Compare July 31, 2024 20:26
(opaque *match*/298))
*match*/298)))
*match*/305 =o (field_mut 0 (field_imm 1 param/297)))
(if (isint *match*/305) (if *match*/305 12 (exit 3)) (exit 3)))))
Copy link
Copy Markdown
Member Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I did not understand why this test case changed -- there was a Match_failure case before and there is still one after, so what did the temporality change in the code? This is much easier to see in the -drawlambda output for this test:

(setglobal Test!
  (let
    (lazy_needs_partial/274 =
       (function param/276 : int
         (catch
           (let (*match*/279 =a (field_imm 0 param/276))
             (catch
               (let
                 (*match*/280 =a (field_imm 1 param/276)
                  *match*/281 =o (field_mut 0 *match*/280))
-                 (if (isint *match*/281) (if *match*/281 (exit 2) 0)
-                   (exit 1)))
+                 (switch* *match*/281 case int 0: 0
+                                      case int 1: (exit 2)))
               with (2)
               (let
                 (*match*/288 =
                    (let
                      (lzarg/282 = *match*/279
                       tag/283 =a (caml_obj_tag lzarg/282))
                      (if (== tag/283 250) (field_mut 0 lzarg/282)
                        (if (|| (== tag/283 246) (== tag/283 244))
                          (apply (field_imm 1 (global CamlinternalLazy!))
                            (opaque lzarg/282))
                          lzarg/282)))
                  *match*/289 =a (field_imm 1 param/276)
                  *match*/290 =o (field_mut 0 *match*/289))
                 (if (isint *match*/290) (if *match*/290 12 (exit 1))
                   (exit 1)))))
         with (1)
           (raise
             (makeblock 0 (global Match_failure/20!) [0: "test.ml" 6 49])))))
    (makeblock 0 lazy_needs_partial/274)))

This is about the way that the check (_, {contents = True}) is compiled in the first clause. The GADT type declaration is as follows:

type _ t =
  | Int : int -> int t
  | True : bool t
  | False : bool t

Before the compiled would do first an isint test to rule out Int, and then an if test to distinguish True from False. But with this commit, the compiler now trusts the totality information that tells it that the Int case is impossible, and generates a simpler check to differentiate True from False. (There is a similar check down below, after the lazy () pattern, and that ones is pessimized as it should.)

@gasche gasche force-pushed the matching-bug-temporality-heuristic branch 3 times, most recently from 64e24b5 to e5e2b95 Compare August 1, 2024 07:52
Copy link
Copy Markdown
Contributor

@lpw25 lpw25 left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Approving on the basis of @ncik-roberts review

@gasche
Copy link
Copy Markdown
Member Author

gasche commented Aug 22, 2024

Thanks! The present PR sits on top of #13341, so I should wait for that PR to be merged before merging the present one.

@gasche gasche force-pushed the matching-bug-temporality-heuristic branch from 9392e14 to 94a8158 Compare September 12, 2024 15:18
@gasche
Copy link
Copy Markdown
Member Author

gasche commented Sep 12, 2024

This PR can be merged now that #13341 has been approved and merged. I am planning to do this after/if the CI passes.

@gasche gasche merged commit 9e72506 into ocaml:trunk Sep 12, 2024
gasche added a commit that referenced this pull request Sep 12, 2024
The Pattern-Matching Bug: introduce a temporality heuristic to de-pessimize certain programs

(cherry picked from commit 9e72506)
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Projects

None yet

Development

Successfully merging this pull request may close these issues.

3 participants