[PATCH] D93376: [LangRef] Clarify the semantics of lifetime intrinsics

[Johannes Doerfert via Phabricator via llvm-commits]

jdoerfert added a comment.

In D93376#2463143 <https://reviews.llvm.org/D93376#2463143>, @RalfJung wrote:

>> This mixes semantic and implementation of an alloca. Let's not do that.
>
> I'm afraid that happened a long time ago when these intrinsics were added. It is, as far as I can see, not possible to describe the semantic of alloca in a correct way without adding this "magic rule".
>
> You stated what you think the semantics of lifetime.start should be, but what about alloca?

I would argue the alloca is the problem not the lifetime markers. The crucial problem in your example is that we assume alloca represents a unique address, unconditionally.
Let's assume it doesn't for a second, see below.

> Somehow you have to explain the following behavior:
>
>   x = alloca 4
>   y = alloca 4
>   // assume no lifetime.start in the rest of the function
>   // now I can prove that x != y
>
> but
>
>   x = alloca 4
>   y = alloca 4
>   // Now, x and y may be equal!
>   
>   lifetime.start x
>   ...
>   lifetime.end x
>   lifetime.start y
>   ...
>   lifetime.end y
>
> In other words, to describe the semantics of alloca (its behavior on the Abstract Machine), we need to "look ahead" and check the lifetime.start of the current function.
>
> We shouldn't mix semantics and what analyses can conclude about a program (which is a consequence of the semantics). "It marks the local dead before the call" is an effect on liveness analyses, it doesn't say anything about what happens in the Abstract Machine. You have to explain in which way "deadness" is reflected in the Abstract Machine.
>
> In particular, one key aspect of the semantics of alloca + lifetime.start is when the allocation (the non-deterministic choice of the address for this local) is made, and how the choice is constrained. Usually for allocation the semantics is that you can pick anything that doesn't overlap with other currently existing allocations, but for alloca in the presence of lifetime.start, this does not work, as the example above shows. That's why we keep talking about "looking ahead", "delaying the allocation", etc.

Proposal:

1. As you noted, there are "constrainted" and "unconstrained" allocas; if there might be a lifetime marker use, an alloca is constrained.
2. Once an alloca is unconstrained, it cannot go back, thus we need to manifest it with the alloca.
3. We do not know that constrained allocas have unique addresses, thus don't fold comparisons of (different) allocas if one is constrained.
4. [Optional] Provide a alloca coalescing pass in the middle-end that will utilize the lifetime markers and split/coalesce allocas.

Interestingly, I think 2) is also needed in this approach as we could otherwise introduce lifetime markers after folding some comparisons but not others.
So if we start with:

  x = alloca
  y = alloca
  r0 = x == y; // `false` as of now and with this proposal, afaict
  //
  use(/* noescape */ x);
  //
  use(/* noescape */ y);
  //
  autp cmp = [&](){ return x == y; };
  r1 = cmp();
  
  return r0 + r1;

Now we fold r0 to false first. Then we inline `cmp`. Then we realize `x` and `y` are only dereferenced in the `use` part and we introduce lifetime markers:

  x = alloca
  y = alloca
  
  lifetime.start(x);
  use(/* noescape */ x);
  lifetime.end(x);
  
  lifetime.start(y);
  use(/* noescape */ y);
  lifetime.end(y);
  
  r1 = x == y;
  
  return false + r1;

we coalesce x and y and `r1` might be true. WDYT?


Repository:
  rG LLVM Github Monorepo

CHANGES SINCE LAST ACTION
  https://reviews.llvm.org/D93376/new/

https://reviews.llvm.org/D93376