Stacked borrows analysis is super-linear (in time and space)

[Robbepop]

While trying to prepare the codebase I am working on for frequent miri usage I found a few related test cases that seem to be messing with the runtime of cargo miri test.

After a quick chat with @oli-obk it was found that when disabling stacked borrows analysis via -Zmiri-disabled-stacked-borrows the required time to analyse the tests via miri dropped significantly back to what would be expected from a miri run that is normally approximately slower compared to native execution by a magnitude of 5.

The approximated "benchmarks" are the following:

With stacked borrows analysis enabled:

Iterations	required time
1	0.0s
10	0.5s
100	5s
1000	7m50s
10_000	N/A

Note that for exhausting the data structure under test a minimum of 8193 iterations are needed to explain the 10k iterations in this test.

With stacked borrows analysis disabled:

Iterations	required time
1	0.0s
10	0.3s
100	2.5s
1000	37s
10_000	4m55s

The tested algorithm is approximately linear to the iterations with the test but with a very low factor. The actual type of operation mainly performed in this test is bit-fiddling since we are mainly working on a bitvector data structure and on a bit level of detail.

It seems to me that the stacked borrows analysis somehow explodes given this type of code.

The original code of the test in question can be found here:
https://github.com/paritytech/ink/blob/redo-init-and-flush/core/src/storage2/alloc/tests.rs#L63

Test the code via:

cargo miri test -- -- many_alloc_and_free_works

Or test the code with disabled stacked borrows using:

cargo miri test -- -Zmiri-disable-stacked-borrows -- many_alloc_and_free_works

The used miri version yielded by cargo miri --version is the following:

miri 0.1.0 (5c823a1 2020-04-15)

I will try to minimize the test case and make another post if I succeed.

[RalfJung]

Yeah, Stacked Borrows keeps track of a lot of metadata, and more metadata can accumulate during execution, which would explain at least quadratic behavior. I would be surprised if it was truly exponential.

This is a special case of #654, but it is worth having a separate issue for Stacked Borrows.

[Robbepop]

Are there already plans or ideas to sort out the problem with the associated costs of the analysis? Is it actually even possible to fix this runtime explosion while keeping all the checks? @oli-obk had the idea to have some more caches for the borrow stacks. (I hope I correctly remembered what he said since I am obviously missing details about the implementation.).

[oli-obk]

No, my idea with caching was before we knew it was stacked borrows. With stacked borrows I believe all we can do is figure out whether we can throw away more metadata earlier.

[Robbepop]

Sorry, didn't mean to close this issue ...
Thanks for the clarification @oli-obk .

[RalfJung]

We could reduce memory consumption of Stacked Borrows through a more clever encoding of the data we need, and some deduplication. And I am sure there are some low-hanging fruits in terms of performance, I did not do a ton of optimizations. There might even be a more clever data structure we could use to track the stack for each location.

[oli-obk]

I was wondering whether some stacks grow indefinitely even though the interpreted code is just a loop. So basically whether we keep some borrows on the stack that don't exist anymore. If each loop iteration creates a borrow and that's pushed to the stack, and never popped, but the next loop iteration creates a borrow again, that may happen.

[RalfJung]

Yeah, I am pretty sure I saw that happen. We'd need some kind of "tag garbage collection" to avoid that. I don't know how to do that in a way that does not cost more performance than it gains...

[oli-obk]

I can cook something up and benchmark it. If it takes just a second or so, we can run it every 10 seconds, which should solve the problem at least for the use case at hand.

[Robbepop]

Is there some news or update concerning this issue?
If not, how can I help you in this process?
We are about to integrate miri into our general CI pipeline very soon. Currently I flag certain tests that would take too long via conditional compilation for miri to skip. Ideally, we wouldn't need to skip too many functions (or no functions) in the long run :)

[oli-obk]

Unfortunately I am out of implementation capacity right now. I apologize for my last post, since it definitely lets hope for more.

[Robbepop]

No need to feel sorry. Thank you for the update and thank you for your work!
We are going to integrate miri into our CI pipeline anyways since it is already an amazing tool and found many errors. Today I was actually even able to debug some weird error much better using miri than using a proper debugger.

[RalfJung]

Today I was actually even able to debug some weird error much better using miri than using a proper debugger.

❤️

Back on topic, it is fairly common to lower iteration counts when testing in Miri so that tests take less long:

let count = if cfg!(miri) { 10 } else { 10_000 };

Maybe that can help here, too. Also if you want to guesstimate how much optimizing Stacked Borrows can help, try -Zmiri-disable-stacked-borrows, as in:

cargo miri test -- -Zmiri-disable-stacked-borrows -- <test suite args>

I suspect even without Stacked Borrows, Miri will be too slow for your long tests.

[Robbepop]

Thank you for your suggestions!

Back on topic, it is fairly common to lower iteration counts when testing in Miri so that tests take less long:

Yep, that's exactly what we currently do in our test suite. :) Didn't use the cfg! macro though, much better than what I use atm.

I suspect even without Stacked Borrows, Miri will be too slow for your long tests.

Aaaaand you are right. Even with stacked borrows checks turned off the original test values takes several minutes for miri. 🤔

---

Thank you both for working so hard on miri. It really has become my secret weapon against UB and bugs in my Rust codebases. ❤️

[RalfJung]

If your code is public and you have any bugs that actually made it into the repo and then got found by Miri and subsequently fixed, we are always looking for submissions to the trophy case in our README. :)

Aaaaand you are right. Even with stacked borrows checks turned off the original test values takes several minutes for miri. thinking

Another "miri-go-faster" switch is -Zmiri-disable-validation. But that also means a bunch of bugs are not found.

[saethlin]

Just commenting here that I'm going to take a crack at this. It looks to me like nearly all of the runtime of Miri with stacked borrows turned on is scanning the borrow stack. Seems like an opportunity to introduce a better data structure.

[RalfJung]

Sounds good! It's probably best if you sketch a rough plan before spending a lot of time to implement it, to make sure it all works out. (Though if you prefer to just hack away, then by all means do -- but please be ready to describe the high-level ideas during code review. :D )

Also, we currently don't even have a good set of benchmarks here, so that might be the first thing that is needed.