Upstream Verus support for the weak memory model

[hiroki-chen]

PR from verus-lang/verus#2716 added the Iris-like weak memory model to Verus and is gated behind -vstd-weak-memory feature when building Verus. This accidentally aligns with one of our verification goals to support non-SC models especially when verifying the RCU module. The semantics they use follow exactly what we need and our codebases overlap signifiantly.

I'm thus considering to first try if the upstream weak memory model is expressive enough to cover our use cases and porting this specific version to our verification baselines and see if this works (I'd expect some proof failure and code fixes though).

@rikosellic @Marsman1996

[hiroki-chen]

I did some quick validation on my side using the weak memory and immediately had several issues with the sync module which didn't verify at first. The first thing is that the CAS semantics of vstd lack the support. We can introduce extra TCB wrappers for that though. Second, because of the memory model change, the invariants for these sync objects need update and may increase verification debts.

Migration is not impossible on the engineering side but I'm afraid that the performance would downgrade.