Open Pointerbender opened 2 years ago
Pointerbender
commented
2 years ago Note to self: since its not (yet?) possible to pin-point any specific clause of the predicate that is causing the memory problems, the root cause may be related to the number of clauses (e.g. if the whole encoder state is cloned for each clause, there may be some kind of super-linear space complexity going on). I will check for this possibility, too, unless this already rings a bell with anyone :)
fpoli
commented
2 years ago Could you attach the .dot dump of the MIR of cursor_invariant? The definition is quite big and I wonder what its CFG looks like.
fpoli
commented
2 years ago You could also give a try at some memory profiling tool, like heaptrack, just to confirm whether there are gigabytes of vir::Expr instances. That tool should (hopefully) work out of the box with the Prusti binary.
Aurel300
commented
2 years ago Also, just in case you are not familiar with this: git bisect might make your search through the commits much faster.
Pointerbender
commented
2 years ago Could you attach the
.dotdump of the MIR ofcursor_invariant? The definition is quite big and I wonder what its CFG looks like.
Sure thing! There are multiple .dot files, but I believe this is the one of interest (target/verify/log/mir/prusti_cursor.database-cursor-prusti_pred_item_cursor_invariant_1cbcabab67d24e6abd150ea50721b9fb.-------.renumber.0.dot):
Thanks for the pointers to heaptrack and git bisect!
fpoli
commented
2 years ago The relevant comment is here :) https://github.com/viperproject/prusti-dev/blob/f8e70f9037b964498e83f58a3bb9387f60c7a454/prusti-viper/src/encoder/mir/pure/interpreter/mod.rs#L54-L56
The encoding of pure expressions currently generates an expression whose size is proportional to the number of paths in the CFG, which means exponential in the number of branches/clauses. (Rust's && does the short-circuit evaluation). It's this way because we initially didn't want to generate let ... in ... expressions, which we now have, and because we needed to automatically generate unfolding expressions, which is no longer necessary.
One possible fix is to detect in the following snippet if the then_expr and else_expr share a big sub-expression, and move that sub-expression to a let expression around the encoding of the switch terminator, such that shared sub-expressions do not end up being duplicated at each branch.
Another possible fix is to start wrapping every Expr type in Rc, such that cloning expressions becomes much cheaper. I remember that MIRAI did it and they were happy with the result.
A further alternative, as noted in that old comment, is to convert the encoding to a forward pass, using plenty of let expressions instead of the substitution calls. This seems to me the cleanest solution now that we have let expressions and no longer need to generate unfoldings.
Pointerbender
commented
2 years ago Wow, that's a swift find! That saves a lot of debugging, thanks! :smile:
A further alternative, as noted in that old comment, is to convert the encoding to a forward pass, using plenty of let expressions instead of the substitution calls. This seems to me the cleanest solution now that we have let expressions and no longer need to generate unfoldings.
This sounds promising!
fpoli
commented
2 years ago For the moment, splitting big predicates into multiple smaller predicates should help. Like:
predicate! {
pub(super) fn huge(cursor: &Cursor) -> bool {
small1(cursor) && small2(cursor) && small3(cursor)
}
}Disabling inline_constant_functions should also help reducing the peak memory usage of Prusti.
Pointerbender
commented
2 years ago The predicate-splitting work-around seems to do the trick, thanks @fpoli!
Somewhere between commits bb3cb3fe25 and f8e70f9 a regression was introduced that significantly increased memory usage, leading to a crash during the Prusti encoding step in both debug and release mode. On my computer with 16GB of physical memory and 32GB swap file (Ubuntu), the
prusti-driverprocess ends up consuming ~100% CPU and 10-11GB of physical memory and another ~25GB of virtual memory, utilizing all available memory (and bringing the whole system to a near-freeze because of excessive swapping in the rest of the OS) before exiting the process during the encoding of a predicate.I did not have a chance yet to deep dive into this during working weekdays, but I'm posting my preliminary findings here already in the hopes that someone might be able to spot where the problem could lie. I'll have some more time on the weekend to look deeper :)
The problem appears in a relatively large (WIP and unpublished) project, which makes debugging harder than usual. My plan of approach to narrow it down is:
Currently I'm on commit f8e70f9037 and the
cargo-prusticommand I use to verify the project is:Its
Prusti.tomlcontents are:In the moment right before crashing, the debug logs show the following:
The 16 warnings are all from rustc (unused import, unused function, useless comparison, and such), no warnings are generated by Prusti itself. The contents of the log messages don't stand out as immediately suspicious to me, but an interesting detail is the timestamps on the logs: there are long pauses lasting seconds in between log lines, usually the debug logs come in at a fairly fast pace (this is probably a side effect of the system struggling to allocate more memory, but just in case that is a helpful detail for the investigation).
The predicate that Prusti is encoding is shown below. For some context:
Cursoris a struct that visits an in-memory B+ tree andcursor_invariantis the predicate used to record the type invariant ofCursor.It might be entirely possible that the memory issue was also already latently present before the mentioned commits, but that the problem became more exaggerated with all the recent additions to the code base (before this regression, encoding also took a while in release mode - but still well under a minute for ~180 items). However, I'm not sure about this, because I don't have any data yet on memory consumption from before I noticed the regression. This will also be one of the things I will look deeper into this weekend.
If anything stands out from the bug report, or if anyone has a hunch which part of the Prusti code base could contain clues to resolving this, any pointers would be greatly appreciated :)
Thanks!