Message-ID: <91dbba64-ade3-4e46-854e-87cd9ecaa689@ralfj.de>
Date: Wed, 26 Feb 2025 15:14:54 +0100
From: Ralf Jung <post@...fj.de>
To: Ventura Jack <venturajack85@...il.com>, 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)

Hi all,

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

Speaking as an author of both models: yes. These models are candidates for the 
*definition* of which programs are correct and which are not. In that sense, 
once adopted, the model *becomes* the baseline, and by definition has no false 
negative or false positives.


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

That is true: if coverage is incomplete or there is non-determinism, Miri can 
miss bugs. Miri does testing, not verification. (However, verification tools are 
in the works as well, and thanks to Miri we have a very good idea of what 
exactly it is that these tools have to check for.)
However, unlike sanitizers, Miri can at least catch every UB that arises *in a 
given execution*, since it does model the *entire* Abstract Machine of Rust.
And since we are part of the Rust project, we are doing everything we can to 
ensure that this is the *same* Abstract machine as what the compiler implements.

This is the big difference to C, where the standard is too ambiguous to uniquely 
give rise to a single Abstract Machine, and where we are very far from having a 
tool that fully implements the Abstract Machine of C in a way that is consistent 
with a widely-used compiler, and that can be practically used to test real-world 
code.


Kind regards,
Ralf

Powered by blists - more mailing lists