Validation and inlining don't work together

[oli-obk]

I'm not sure what the exact issues are, but we should get them to work

[RalfJung]

There are some conceptual issues -- validation relies on all locks being released when the function returns, which does not happen after inlining. After inlining, the locks acquired by the "outer" and "inner" function are not distinguishable, so it is not clear currently how that should even look like.

[oli-obk]

We probably need to either mark the validation statements as inlined and do some logic here, or properly inline validation statements in the inline pass in rustc.

[RalfJung]

The thing is, the statements/model as it is ow can't handle inlining. This needs a conceptual change.

For example, rather than just identifying locks by stack frame number, there could be an additional index differentiating the "outer" and "inner" part of the inlined function. That should make inlining invertible; the resulting program is equivalent to the one before inlining. I am worried however that then validation statements will end up being in the way frequently; we'd have to figure out the rules for reordering them with other things.

Or maybe, the border between the two functions should somehow "disappear". The release and acquire statements around the call should be gone, and same for the acquire statements in the callee. However, I think this will not handle lifetimes inside the callee that outlive the callee properly.

Another option would be to erase validation before doing inlining; however that would probably prevent many useful optimizations that build on validation and are only discoverable after inlining.

[oli-obk]

The release and acquire statements around the call should be gone, and same for the acquire statements in the callee.

That sounds like an approach in the right direction to me

However, I think this will not handle lifetimes inside the callee that outlive the callee properly.

We can rewrite any statements during inlining if we modify the inlining pass.

[RalfJung]

The validation stuff is going to completely change anyway. Closing this.