Message-ID: <CAFJgqgREAtPkx+r_QNPnt-bOekjVjCNBv=tAuuEC6dT2HCA0jg@mail.gmail.com>
Date: Wed, 26 Feb 2025 11:36:55 -0700
From: Ventura Jack <venturajack85@...il.com>
To: Miguel Ojeda <miguel.ojeda.sandonis@...il.com>
Cc: Alice Ryhl <aliceryhl@...gle.com>, Linus Torvalds <torvalds@...ux-foundation.org>, 
	Kent Overstreet <kent.overstreet@...ux.dev>, Gary Guo <gary@...yguo.net>, airlied@...il.com, 
	boqun.feng@...il.com, david.laight.linux@...il.com, ej@...i.de, 
	gregkh@...uxfoundation.org, hch@...radead.org, hpa@...or.com, 
	ksummit@...ts.linux.dev, linux-kernel@...r.kernel.org, 
	rust-for-linux@...r.kernel.org, Ralf Jung <post@...fj.de>
Subject: Re: C aggregate passing (Rust kernel policy)

On Wed, Feb 26, 2025 at 10:49 AM Miguel Ojeda
<miguel.ojeda.sandonis@...il.com> wrote:
>
> On Wed, Feb 26, 2025 at 4:21 PM Ventura Jack <venturajack85@...il.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.

Ralf Jung explained matters well, I think I understood him. I found his
answer clearer than both your answers and Alice's on this topic.

> > 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.

"Currently tied" is accurate as far as I can tell. Ralf Jung
did explain it well. He suggested removing those links from the
Rust reference, as I understand him. But, importantly, having
more than 1 major Rust compiler would be very helpful in my opinion.
It is easy to accidentally or incidentally tie language definition
to compiler implementation, and having at least 2 major compilers
helps a lot with this. Ralf Jung described it as a risk of overfitting I think,
and that is a good description in my opinion.

Best, VJ.

Powered by blists - more mailing lists