Add snapshotting to ObligationForest, take 2

[soltanmm]

Take 2 (3?) of adding snapshotting to ObligationForest, this time with a simpler undo-list approach (separate PR because the last one's commit deltas were nearly removed from history with these). Additionally adds snapshotting methods to FulfillmentContext.

Note: I tried adding the snapshotting of the FulfillmentContext to snapshotting calls in InferCtxt and hit RefCell borrow panics. The action callback in the ObligationForest::process_obligations call attempts to borrow the FulfillmentContext already in the middle of a select_* (specifically for a probe), and because we've already borrowed it in the earlier stack frame for calling select_* it falls on its face. If I understand the rest of the compiler correctly, the usual solution is to make everything a RefCell. We could do that in ObligationForest and in FulfillmentContext, but then that means every call to process_obligations would need to make a copy of <self as ObligationForest>.nodes: Vec to release all borrows surrounding the call to action in ObligationForest::process_obligations. Moreover, because actions may do more mutating things with the ObligationForest, the alternative of not making a copy via something unsafe could leave us with a dangling mutable reference if some action increases the size of nodes... which then leads to the alternative of using a stable vec (and other more complicated possibilities maintaining the required invariants). The rabbit hole goes down a ways...

Playing with some notion of a StackCell ^(wc?) (something that explicitly allows one mutable borrow per snapshot level) could be fruitful, at least to bless the needed patterns of unsafe code for partially persistent structures as discouraged yet idiomatic, or perhaps much better finding a way of guaranteeing the invariants of snapshotting.

r? @nikomatsakis
cc @jroesch (because I think you're doing something eventually with a snapshotting trait?)

[rust-highfive]

Thanks for the pull request, and welcome! The Rust team is excited to review your changes, and you should hear from @nikomatsakis (or someone else) soon.

If any changes to this PR are deemed necessary, please add them as extra commits. This ensures that the reviewer can see what has changed since they last reviewed the code. Due to the way GitHub handles out-of-date commits, this should also make it reasonably obvious what issues have or haven't been addressed. Large or tricky changes may require several passes of review and changes.

Please see the contribution instructions for more information.

[nikomatsakis]

@soltanmm I've not read this code yet, but the ref-cell problem sounds annoying. Let me take a look. I know @jroesch spent quite some time wrestling with the best setup here and has been talking about rebasing a branch of his related to that. I think we can get things sorted out, we definitely want to think carefully a bit about where to draw the "refcell boundary".

[nikomatsakis]

The pattern I used elsewhere is to have one vector and to push OpenSnapshot events into it. This way you only need one vector (the vector is empty if no snapshots are active). Committing the base snapshot clears the vector (but leaves the state the same). Converting a non-base snapshot converts the OpenSnapshot to CommittedSnapshot. Reverting a snapshot pops things off of the undo vector. If you ever pop off an OpenSnapshot (as opposed to a CommittedSnapshot)...then something went wrong. You can see an example in src/librustc/middle/infer/region_inference.rs.

[nikomatsakis]

OK, so, this code looks pretty good. I didn't dig into the precise details of each push-pop yet (or the precise patterns run by the tests), mostly because I wanted to raise one other question: to fix #31157, I think I want to add some "per-tree" state associated with the root (a HashMap). I'd prefer for the type of this state to just be a generic type, which makes rollbacks pretty hard.

However, it occurs to me now that the state I actually want in practice is a HashMap. If we used a persistent hashmap, then we could clone the state very easily. Might be the thing to do. Alternatively, I could probably make the "per-tree" state not as generic, so that it can be built into the snapshotting relatively easily. That might be the better thing to do.

[soltanmm]

@nikomatsakis comments addressed. :-)

If we used a persistent hashmap, then we could clone the state very easily.

Just to clarify: when you say 'persistent', do you mean 'persistent enough to be able to backtrack to a parent' (as opposed to 'fully persistent')?

Alternatively, I could probably make the "per-tree" state not as generic, so that it can be built into the snapshotting relatively easily. That might be the better thing to do.

Something like a hook to push undoable actions (e.g. undoable via closures) into some other entity's log? Or something using the future Transactional trait, e.g. forest snapshots end up being lists of snapshots like InferCtxt's CombinedSnapshot but of per-tree-state snapshots?

[nikomatsakis]

@soltanmm

Just to clarify: when you say 'persistent', do you mean 'persistent enough to be able to backtrack to a parent' (as opposed to 'fully persistent')?

I meany fully persistent, but of course the weaker property (which I would call "snapshottable") would suffice. It just makes the interface between OF and its clients a bit more complex. Let me do some experiments on my end, I'm still trying to figure out the best fix in any case.

[soltanmm]

@nikomatsakis
Another alternative to tackling the borrow problem: we could change ObligationForest::process_obligations from checking all obligations in one go to an associated function accepting a reference to a refcell of the forest and returning an iterator that steps over each pending node in a specific snapshot (if control is ever passed to the iterator and the snapshot is different than what the iterator was constructed with it panics). The iterator runs the specified action on a particular obligation by: borrowing the forest from its refcell, scanning for the next pending node starting from a last-known-index, setting the node to an active state (to be explained later), cloning the obligation, releasing the borrow on the obligation forest, passing the cloned obligation to the action callback, reborrowing the forest, checking the still-in-the-same-snapshot-as-was-constructed-in invariant, using the result of the action call to update the tree, and releasing the borrow. The result of the iterator at each step is the same as the result of the current ObligationForest::process_obligations (only it contains the results from processing exactly one obligation at the active snapshot).

Within the action callback, the currently active obligation's node has a special active node-state. This state is ignored when searching for 'pending' nodes, and is effectively treated as a success node with nonzero active children (let's just say 1 to make it easy).

Added safety could involve adding a flag to StartSnapshot indicating in the log whether or not there's an iterator active (set on creation, unset on drop) and using that to panic on the creation of any additional (erroneous) iterators.

If it's required, ensuring that the number of obligations checked by the iterator is the same as the number that would've been checked in the current formulation of process_obligations can be done by
keeping track of the number of nodes that were present at iterator construction.

If it's required, ensuring that iterators created within an action call (and elsewhere) don't check pending obligations that would be checked by an active iterator in an earlier snapshot can be done by starting that iterator's 'last-known-index' after the pending nodes that'd be handled by an earlier snapshot's iterator.

As best I can tell, this solves the problem of borrows by introducing an extra refcell in one location at argument position (new process_obligations) and in one location as a field (in the FulfillmentContext). It effectively externalizes the process_obligations call, while keeping (I think) the convenience the current code has. It also, as best as I can tell, doesn't adversely affect whatever comes of #31349. I further believe it'd recover ObligationForest's usefulness in @jroesch's branch.

I'm probably going to attempt an implementation and see where it goes (might be this weekend; pants afire with other things), short of anyone saying that it's a no-go.

[nikomatsakis]

@soltanmm Yes, that seems plausible. I checked out @jroesch's branch yesterday but haven't had time to play with it myself. It seems like we basically have two choices:

• Externalize the obligation processing, as you suggest.
• Internalize the trait selection, projection etc.

In general, I'd prefer to internalize, but that may indeed be very difficult. This is clearly what @jroesch has been doing, which is why I want to study his branch a bit, and maybe attempt some local ports, in order to see what is the most targeted diff we can achieve.

I think in the end I might want to try it both ways, to see which works out the cleanest -- so I certainly have no objection to you giving that a try. It'd be an important data point. Sound good?

[soltanmm]

Sounds good, but I have to wonder if it'd then be more prudent to stick with the approach in @jroesch's branch? Despite being a tad gung-ho I'm not attached to much beyond pushing my filed issues into history and leaving them there. :-)

[bors]

☔ The latest upstream changes (presumably #31349) made this pull request unmergeable. Please resolve the merge conflicts.

[soltanmm]

Rebased (rewritten? sans FulfillmentContext modifications). The discussion w/ @nikomatsakis today indicated that this has the possibility of not being necessary, but I'll leave it here just in case.

[bors]

☔ The latest upstream changes (presumably #31680) made this pull request unmergeable. Please resolve the merge conflicts.

[nikomatsakis]

@soltanmm I think I'm going to close this PR for the time being-- but let's keep the branch around in case it turns out we do want to do this. :)