Re: C aggregate passing (Rust kernel policy)

Ralf Jung
2025-02-26T14:14:57Z

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