Re: C aggregate passing (Rust kernel policy)

[Miguel Ojeda <miguel.ojeda.sandonis@gmail.com>]

On Wed, Feb 26, 2025 at 4:21 PM Ventura Jack <venturajack85@gmail.com> wrote:
>
> I am not certain that I understand either you or Alice correctly.
> But Ralf Jung or others will probably help clarify matters.

When you said:

    "In a preprint paper, both stacked borrows and tree burrows
     are as far as I can tell described as having false positives."

I think that you mean to say that the new model allows/rejects
something that unsafe code out there wants/doesn't want to do. That is
fine and expected, although of course it would be great to have a
model that is simple, fits perfectly all the code out there and
optimizes well.

However, that is very different from what you say afterwards:

    "Are you sure that both stacked borrows and tree borrows are
     meant to be full models with no false positives and false negatives,"

Which I read as you thinking that the new model doesn't say whether a
given program has UB or not.

Thus I think you are using the phrase "false positives" to refer to
two different things.

> You are right that I should have written "currently tied", not "tied", and
> I do hope and assume that the work with aliasing will result
> in some sorts of specifications.
>
> The language reference directly referring to LLVM's aliasing rules,
> and that the preprint paper also refers to LLVM, does indicate a tie-in,
> even if that tie-in is incidental and not desired. With more than one
> major compiler, such tie-ins are easier to avoid.

Ralf, who is pretty much the top authority on this as far as I
understand, already clarified this:

    "we absolutely do *not* want Rust to be tied to LLVM's aliasing rules"

The paper mentioning LLVM to explain something does not mean the model
is tied to LLVM.

And the Rust reference, which you quote, is not the Rust specification
-- not yet at least. From its introduction:

    "should not be taken as a specification for the Rust language"

When the Rust specification is finally published, if they still refer
to LLVM (in a normative way), then we could say it is tied, yes.

Cheers,
Miguel