Based on discussions I had with @JoJoDeveloping, it seems like there will have to be some sort of interaction between the aliasing model and the concurrency model. We'll have to figure out the details before finalizing decisions here.

One of the ways in which they interact is the "end of a function call" event that deactivates protectors: if that event happens in one thread, while another thread accesses that location, there's the question of -- did the access happen before or after the end of the call? Miri just uses the actual execution order for this, but in a weak memory world, we will likely have to use something like happens-before here or else we may lose some of the optimizations we were hoping for.