Stream: t-compiler/wg-mir-opt

Topic: Proofs of soundness


Félix Fischer (Jun 23 2020 at 08:10, on Zulip):

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.

So:
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 ^^

Hanna Kruppe (Jun 23 2020 at 09:16, on Zulip):

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.

Hanna Kruppe (Jun 23 2020 at 13:13, on Zulip):

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

RalfJ (Jun 23 2020 at 16:48, on Zulip):

@Félix Fischer the "formal-methods" stream might be a better fit for this topic, actually :)

RalfJ (Jun 23 2020 at 16:49, on Zulip):

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.

RalfJ (Jun 23 2020 at 16:49, on Zulip):

So I think our best bet is something like Alive2, as mentioned by @Hanna Kruppe

RalfJ (Jun 23 2020 at 16:50, on Zulip):

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

RalfJ (Jun 23 2020 at 16:51, on Zulip):

(also, aliasing-based optimizations are amongst the hardest to verify. I think we should start with easier ones. :D )

RalfJ (Jun 23 2020 at 16:51, on Zulip):

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

RalfJ (Jun 23 2020 at 16:52, on Zulip):

my background is in doing complex proofs by hand in coq, I know little about automated theorem proving

Félix Fischer (Jun 25 2020 at 00:51, on Zulip):

Ohh, I see!

Félix Fischer (Jun 25 2020 at 00:52, on Zulip):

Btw @Hanna Kruppe those are great links, thank you <3

Félix Fischer (Jun 25 2020 at 00:52, on Zulip):

So... I was thinking more of doing proofs by hand

Félix Fischer (Jun 25 2020 at 00:52, on Zulip):

Like

Félix Fischer (Jun 25 2020 at 00:53, on Zulip):

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)

Félix Fischer (Jun 25 2020 at 00:53, on Zulip):

We freeze the code, or the algorithm at least

Félix Fischer (Jun 25 2020 at 00:54, on Zulip):

And we try to prove that some invariants are being held through each step of the optimization pass

Félix Fischer (Jun 25 2020 at 00:54, on Zulip):

I think that just that could be big

Félix Fischer (Jun 25 2020 at 00:54, on Zulip):

It would at least make us question our code's soundness and try to prove that the edge cases hold it

Félix Fischer (Jun 25 2020 at 00:57, on Zulip):

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 (Jun 25 2020 at 00:58, on Zulip):

RalfJ said:

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?

RalfJ (Jun 25 2020 at 09:25, on Zulip):

Félix Fischer said:

We freeze the code, or the algorithm at least

I strongly doubt such a freeze will ever happen...

Hanna Kruppe (Jun 25 2020 at 09:28, on Zulip):

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.

Hanna Kruppe (Jun 25 2020 at 09:49, on Zulip):

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

  1. integration issues (e.g., #67019 was due to not accounting for layout optimizations properly) where focusing solely on the pass itself won't help
  2. Plainly incorrect transformations (e.g., #73609) that can be found just as well by simpler means than attempting proofs

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.

Félix Fischer (Jun 25 2020 at 17:54, on Zulip):

Ohh, I see. Both of you two expose very fair points.

Re: freeze
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?

Félix Fischer (Jun 25 2020 at 17:55, on Zulip):

Re: proofs.
I think I more or less agree with you, Hanna. That makes sense :)

Hanna Kruppe (Jun 25 2020 at 17:56, on Zulip):

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.

Félix Fischer (Jun 25 2020 at 18:06, on Zulip):

Ahh, you mean the produced MIR code

Félix Fischer (Jun 25 2020 at 18:07, on Zulip):

I was thinking more on the definition and semantics of MIR itself :laughing:

Félix Fischer (Jun 25 2020 at 18:07, on Zulip):

Okay, now I think I really get what you mean

Hanna Kruppe (Jun 25 2020 at 18:07, on Zulip):

No, I mean the definition and semantics of MIR itself.

Félix Fischer (Jun 25 2020 at 18:08, on Zulip):

Really? Wait, how would that cha- ohh. Okay, yeah, the compiler IS sort of the definition and semantics of MIR

Félix Fischer (Jun 25 2020 at 18:08, on Zulip):

So if you change the compiler, you change MIR

Hanna Kruppe (Jun 25 2020 at 18:08, on Zulip):

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.

Hanna Kruppe (Jun 25 2020 at 18:09, on Zulip):

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

Félix Fischer (Jun 25 2020 at 18:09, on Zulip):

(Right! :D)

Félix Fischer (Jun 25 2020 at 18:10, on Zulip):

That makes sense

Félix Fischer (Jun 25 2020 at 18:10, on Zulip):

Thank you for the explanation, Hanna ^^

Xavier Denis (Jun 27 2020 at 10:20, on Zulip):

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

Félix Fischer (Jun 27 2020 at 21:06, on Zulip):

That's a good point

RalfJ (Jul 05 2020 at 07:11, on Zulip):

yeah, that's why this is what we did with Stacked Borrows

RalfJ (Jul 05 2020 at 07:11, on Zulip):

it's about validation that the optimizations are eight in principle, not that they are implemented correctly

RalfJ (Jul 05 2020 at 07:11, on Zulip):

experience with LLVM shows that this is non-trivial in many cases

RalfJ (Jul 05 2020 at 07:12, on Zulip):

const-prop is just very simple, conceptually, which makes it less interesting to look at here

Félix Fischer (Jul 06 2020 at 06:30, on Zulip):

Haha, no wonder I like const-prop so much :big_smile: it felt really approachable

Last update: Sep 28 2020 at 14:15UTC