Re: C aggregate passing (Rust kernel policy)

[Ralf Jung]

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