Message-ID: <CAFJgqgRxfTVxrWja=ZW=mTj1ShPE5s-atAqxzMOq5poajMh=4A@mail.gmail.com>
Date: Wed, 26 Feb 2025 05:36:06 -0700
From: Ventura Jack <venturajack85@...il.com>
To: Alice Ryhl <aliceryhl@...gle.com>
Cc: 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, 
	miguel.ojeda.sandonis@...il.com, rust-for-linux@...r.kernel.org
Subject: Re: C aggregate passing (Rust kernel policy)

On Tue, Feb 25, 2025 at 10:36 AM Alice Ryhl <aliceryhl@...gle.com> wrote:
>
> On Tue, Feb 25, 2025 at 6:21 PM Ventura Jack <venturajack85@...il.com> wrote:
> > Is there a specification for aliasing that defines your first bullet
> > point, that people can read and use, as a kind of partial
> > specification? Or maybe a subset of your first bullet point, as a
> > conservative partial specification? I am guessing that stacked
> > borrows or tree borrows might be useful for such a purpose.
> > But I do not know whether either of stacked borrows or tree
> > borrows have only false positives, only false negatives, or both.
>
> In general I would say read the standard library docs. But I don't
> know of a single resource with everything in one place.
>
> Stacked borrows and tree borrows are attempts at creating a full model
> that puts everything in the two first categories. They are not
> conservative partial specifications.

Tree borrows is, as far as I can tell, the successor to stacked borrows.

    https://perso.crans.org/vanille/treebor/
        "Tree Borrows is a proposed alternative to Stacked Borrows that
        fulfills the same role: to analyse the execution of Rust code at
        runtime and define the precise requirements of the aliasing
        constraints."

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

    https://perso.crans.org/vanille/treebor/aux/preprint.pdf
        "This overcomes the aforementioned limitations: our evaluation
        on the 30 000 most widely used Rust crates shows that Tree
        Borrows rejects 54% fewer test cases than Stacked Borrows does."

That paper also refers specifically to LLVM.

    https://perso.crans.org/vanille/treebor/aux/preprint.pdf
        "Tree Borrows (like Stacked Borrows) was designed with this in
        mind, so that a Rust program that complies with the rules of Tree
        Borrows should translate into an LLVM IR program that satisfies
        all the assumptions implied by noalias."

Are you sure that both stacked borrows and tree borrows are
meant to be full models with no false positives and false negatives,
and no uncertainty, if I understand you correctly? It should be
noted that they are both works in progress.

MIRI is also used a lot like a sanitizer, and that means that MIRI
cannot in general ensure that a program has no undefined
behavior/memory safety bugs, only at most that a given test run
did not violate the model. So if the test runs do not cover all
possible runs, UB may still hide. MIRI is still very good, though,
as it has caught a lot of undefined behavior/memory safety bugs,
and potential bugs, in the Rust standard library and other Rust
code.

    https://github.com/rust-lang/miri#bugs-found-by-miri

> > For Rust documentation, I have heard of the official
> > documentation websites at
> >
> >     https://doc.rust-lang.org/book/
> >     https://doc.rust-lang.org/nomicon/
> >
> > And various blogs, forums and research papers.
> >
> > If there is no such conservative partial specification for
> > aliasing yet, I wonder if such a conservative partial
> > specification could be made with relative ease, especially if
> > it is very conservative, at least in its first draft. Though there
> > is currently no specification of the Rust language and just
> > one major compiler.
> >
> > I know that Java defines an additional conservative reasoning
> > model for its memory model that is easier to reason about
> > than the full memory model, namely happens-before
> > relationship. That conservative reasoning model is taught in
> > official Java documentation and in books.
>
> On the topic of conservative partial specifications, I like the blog
> post "Tower of weakenings" from back when the strict provenance APIs
> were started, which I will share together with a quote from it:
>
> > Instead, we should have a tower of Memory Models, with the ones at the top being “what users should think about and try to write their code against”. As you descend the tower, the memory models become increasingly complex or vague but critically always more permissive than the ones above it. At the bottom of the tower is “whatever the compiler actually does” (and arguably “whatever the hardware actually does” in the basement, if you care about that).
> > https://faultlore.com/blah/tower-of-weakenings/
>
> You can also read the docs for the ptr module:
> https://doc.rust-lang.org/stable/std/ptr/index.html

That latter link refers through the undefined behavior page to.

    https://doc.rust-lang.org/stable/reference/behavior-considered-undefined.html
    http://llvm.org/docs/LangRef.html#pointer-aliasing-rules

The aliasing rules being tied to a specific compiler backend,
instead of a specification, might make it harder for other
Rust compilers, like gccrs, to implement the same behavior for
compiled programs, as what the sole major Rust compiler,
rustc, has of behavior for compiled programs.

> > On the topic of difficulty, even if there was a full specification,
> > it might still be difficult to work with aliasing in unsafe Rust.
> > For C "restrict", I assume that "restrict" is fully specified, and
> > C developers still typically avoid "restrict". And for unsafe
> > Rust, the Rust community helpfully encourages people to
> > avoid unsafe Rust when possible due to its difficulty.
>
> This I will not object to :)
>
> Alice

On the topic of difficulty and the aliasing rules not being
specified, some have claimed that the aliasing rules for
Rust not being fully specified makes unsafe Rust harder.

    https://chadaustin.me/2024/10/intrusive-linked-list-in-rust/
        "The aliasing rules in Rust are not fully defined. That’s
        part of what makes this hard. You have to write code
        assuming the most pessimal aliasing model."

        "Note: This may have been a MIRI bug or the rules have
        since been relaxed, because I can no longer reproduce
        as of nightly-2024-06-12. Here’s where the memory
        model and aliasing rules not being defined caused some
        pain: when MIRI fails, it’s unclear whether it’s my fault or
        not. For example, given the &mut was immediately
        turned into a pointer, does the &mut reference still exist?
        There are multiple valid interpretations of the rules."

I am also skeptical of the apparent reliance on MIRI in the
blog post and by some other Rust developers, since
MiRI according to its own documentation cannot catch
everything. It is better not to rely on a sanitizer for trying
to figure out the correctness of a program. Sanitizers are
useful for purposes like mitigation and debugging, not
necessarily for determining correctness.

Best, VJ.

Powered by blists - more mailing lists