So. My vision for our fancy MIR-future where we do all sorts of cool stuff with mir opts includes the idea of proving the soundness of the transformations we make while optimizing MIR.
This is of course a long term project more than a "right now" thing. Specially because it would need a precise understanding of MIR semantics, which haven't yet been fully defined if I understood correctly.
BUT. I want to help push this forward at some point. I don't know if I can do a good job of it, I don't know if there's a tool for this, and I only sort of understand one of the opts (the const-prop one). Still, I think it would be really good to have.
Have there been discussions on this topic? Also, is there a group in the community that has experience proving these kinds of things?
@RalfJ you've probably thought about this at some point, right? :3
Anywho, I ping you because I'd figure you'd want to chip in here ^^
The Stacked Borrows paper (https://plv.mpi-sws.org/rustbelt/stacked-borrows/) includes proofs for some optimizations justified by the aliasing rules -- though, as far as I can tell, only for some specific pairs of programs which illustrate the desired optimization (rather than giving an optimization algorithm, and then proving it correct for all programs). A noteworthy alternative/complement to traditional "pen and paper" (or Coq) formalization of algorithms is translation validation, which addresses the problem of gaps between the formalization of the optimization and its production implementation. The Alive project (https://blog.regehr.org/archives/1722) has been doing this very successfully with LLVM optimizations, a similar approach may be effective for MIR optimizations once we have precise semantics for it.
(Though I do wonder if/how translation from IR to SMT formulas, as done in Alive, can be reconciled with MIR being polymorphic. Last I heard, even generalizing over integer bit widths was an area of active research. Perhaps the simple approach of "try some concrete instances and hope that will catch most bugs" will be good enough for a start?)
@Félix Fischer the "formal-methods" stream might be a better fit for this topic, actually :)
I have many thoughts, indeed.^^ but realistically, rustc isn't going to get CompCert-style Coq proofs. Those are too much work, there are too few people who can do them, and there is now they they could keep up with Rust's development pace.
So I think our best bet is something like Alive2, as mentioned by @Hanna Kruppe
(the stacked borrows proofs show that some reorderings are in principle possible in an idealized Rust. this is a crucial first step, but there's a significant gap between that and verifying what our MIR optimizations are doing.)
(also, aliasing-based optimizations are amongst the hardest to verify. I think we should start with easier ones. :D )
coming back to Alive2, I would happily be involved with figuring out MIR semantics more precisely, but I have no idea how Alive2 does its actual checking
my background is in doing complex proofs by hand in coq, I know little about automated theorem proving
Ohh, I see!
Btw @Hanna Kruppe those are great links, thank you <3
So... I was thinking more of doing proofs by hand
After we exhaust one branch of optimization (like const prop for example, in which I'm planning to put some serious effort after I get some bureaucracy done with uni, hopefully during the following weeks)
We freeze the code, or the algorithm at least
And we try to prove that some invariants are being held through each step of the optimization pass
I think that just that could be big
It would at least make us question our code's soundness and try to prove that the edge cases hold it
I think that's most of what we need. With the algorithm being frozen, and the proof being out in the open, even if it's not actually machine-verified, it could be checked by the eyes of everyone that wants to help.
Félix Fischer the "formal-methods" stream might be a better fit for this topic, actually :)
Haha that's fair. Is it possible to move it there?
Félix Fischer said:
We freeze the code, or the algorithm at least
I strongly doubt such a freeze will ever happen...
Right, for const prop in particular this would mean freezing both the definition of MIR (well, the subset that const prop operates on) and miri (again, at least the parts relevant to const prop). This seems very invasive and undesirable.
I also have serious doubts about the value of (mechanized or pen-and-paper) proofs for this particular part. The "core" of constant evaluation is conceptually trivial once operational semantics for MIR are fixed (OTOH, picking reasonable semantics is quite challenging). This is not to say there aren't any bugs in it -- but many are either
In my personal view, the kind of approach you described is more valuable when there's subtle invariants internal to a reasonably small module (e.g., a very clever data structure), because then you can actually confidently state and validate a useful invariant, rather than either verifying trivial things ("miri indeed performs an addition when there's an
Add operation in the MIR") or having to content with many integration points.
Ohh, I see. Both of you two expose very fair points.
I guess I didn't see that we'd have to freeze MIR and maybe miri for that (although now that I've worked on const-prop, I'm not sure what is and what isn't miri anymore. I was sure I hadn't ever touched it until someone said that it was used for const prop, so I guess all of what I did touch was actually miri? Anywho). And yeah, that sure seems invasive. Specially freezing miri. Freezing MIR seems like it could be a thing tho? Like after semantics are well defined and all of that. In the long term, there might be a day when MIR is frozen right?
I think I more or less agree with you, Hanna. That makes sense :)
I see no reason to expect either the "surface" Rust language or rustc implementation details (e.g., internal architecture, data structures) to ever be frozen, and changes to either of those lead to MIR changes, even if they are backwards compatible changes.
Ahh, you mean the produced MIR code
I was thinking more on the definition and semantics of MIR itself :laughing:
Okay, now I think I really get what you mean
No, I mean the definition and semantics of MIR itself.
Really? Wait, how would that cha- ohh. Okay, yeah, the compiler IS sort of the definition and semantics of MIR
So if you change the compiler, you change MIR
For example, the specific way NLL is done right now influences the definition of MIR statements and places, and future changes (like Polonius) will probably fit better with different representations.
(Or the other way around: changes to MIR are being proposed and running into challenges related to borrow checking; if borrow checking changes then different designs become more attractive.)
That makes sense
Thank you for the explanation, Hanna ^^
I feel like it's much more valuable to prove the optimizations correct on a idealised version of Rust than to attempt to prove the actual implementation. At least then the gap narrows to 'does the implementation behave like the idealised version'?
That's a good point
yeah, that's why this is what we did with Stacked Borrows
it's about validation that the optimizations are eight in principle, not that they are implemented correctly
experience with LLVM shows that this is non-trivial in many cases
const-prop is just very simple, conceptually, which makes it less interesting to look at here
Haha, no wonder I like const-prop so much :big_smile: it felt really approachable