There is an established working group and RustBelt project. But for quite a while there was no significant news. Can someone close to the project give an update on the current developments in this area, please?
1 Like
In RustBelt we are currently working on Stacked Borrows. This will include a Coq formalization of Stacked Borrows and some correctness proofs of compiler transformations.
Since the original paper, RustBelt has been extended to also support reasoning about weak memory; that work is still under submission (it got rejected the first time 
).
And we have some ongoing work to verify âbrandingâ-style programming in Rust, also known as âlifetime generativityâ.
(I am not involved in all of these projects, âweâ here just means âthe RustBelt teamâ.)
20 Likes
Will there also be a correctness proof of Stacked Borrows itself?
I don t think that s possible . Correct me if i misunderstood something about stacked borrows, but as i understood it they are a semantics and not a Propery. Hence it defines what correct behaviour is.
The only things we could proof about a semanticsâ correctness is its equivalence to some other semantics, or that it has some intuitive properties.
AFAICT you appear to be the main contributor from the team back to Rust upstream. Are there any plans for contributing any of the other work in which you are not involved in ?
3 Likes
Yeah, I am our main "connection point" to the community.
Most of the other work is entirely theoretical (much like original RustBelt): verifying in Coq that some properties hold for (some model of) the Rust type system / a Rust library. There isn't very much to contribute back there except fur bug reports when we find issues (and the other team members do that). Jacques-Henri was also involved in some extension to the Cell API by verifying it in Coq.
Stacked Borrows, with its implementation in Miri, is just much more directly something one can "contribute back".
Ah, such a loaded question. 
As @joeschman noted, this first requires a definition of what it means to be "correct". So we identified four basic reorderings of instructions that are basically impossible to do in C, and that should be easy to justify in Rust based on Stacked Borrows. And my collaborators are working on formally proving correctness of those transformations (in Coq).
This doesn't show that Stacked Borrows is the final answer and solves all our problems, but it is a very good sanity check. Whenever one defines something like Stacked Borrows, one has to make sure that one allows "not too many" programs because that would permit "bad" programs, but one also has to make sure that one allows "not too few" programs because then the entire thing is just useless. We have the formal proofs to show that we allow "few enough" programs to make the model useful for justifying optimizations, and the implementation in Miri to show that we allow "enough" programs to actually be able to apply Stacked Borrows to real code. The latter part wouldn't be possible without support from the various involved Rust teams to actually let us experiment with Stacked Borrows in Miri, patch rustc to make that implementation feasible, patch the libstd test suite to make it runnable in Miri, and so on! <3
Of course this comes with the usual caveat that we are verifying a model of Stacked Borrows and MIR, and not actually proving anything about rustc.
9 Likes
This is fair. The purpose of borrow checking is supposedly to prevent data races. Has anyone defined the scope of this prevention, and, if so, is there a plan to prove that Stacked Borrows meets that requirement?
You are confusing two things.
The purpose of borrow checking is to prevent data races, which are a form of UB (undefined behavior). We have proved, with the first RustBelt paper, that our model of a type system with borrows successfully prevents data races. This is, however, conceptually quite far from how the Rust compiler implements borrow checking, so there is still a gap here.
The purpose of Stacked Borrows is to make more programs UB so that we can have more optimizations. It has nothing to do with data races. It recognizes that the borrow checker does more than just preventing data races, use-after-free, double-free, dangling pointers (as if that wasnât enough) â it also prevents certain forms of aliasing from happening. All the other things the borrow checker prevents are already UB. By making âdoes the wrong aliasingâ also UB, we are formalizing what exactly the borrow checker is preventing, and enabling more optimizations.
4 Likes
Okay, but presumably you are showing somehow that Stacked Borrows is consistent with your model of a type system with borrows?
Good question.
We have not done that yet, but it's on the list. This kind of stuff is a lot of work.
4 Likes
This topic was automatically closed 90 days after the last reply. New replies are no longer allowed.