WIP: Weak memory support

[hiroki-chen]

Ok so the weak memory has been started, and this serves as the triage PR for this feature. The core idea behind this implementation to encode message histories (parameterized by the timerstamp token) for each memory location as ghost states in the concurrent separation logic which allows the caller to open the invariant and obtain the handle to the underlying data.

Basically, the roadmap includes:

• Modelling the "weak" part (i.e., memory ordering) of the atomic operations. This includes adding new atomic wrapper types from the Rust std library and stopping using the vstd's atomic types at all (since they assume SC).
• Introduce idomatic macros, types, and interfaces for proving around our customized atomic types.
• Use the atomic types to prove the RCU reclamation as well as the traversal security properties.
• Add several examples.

[hiroki-chen]

Reference https://dl.acm.org/doi/pdf/10.1145/3729246 and https://dl.acm.org/doi/pdf/10.1145/3591297

There is no need to model the full C11 semantics (they are even flawed) so we just do an in-order spec.

[hiroki-chen]

Just done the low-level primitives so that we can model the atomic operations for the weak memory model.

[rikosellic]

This will be a huge win if it is correct. I've not read the paper in detail yet, so I'm afraid I will not have enough knowledge to review this PR until next week.

[hiroki-chen]

This will be a huge win if it is correct. I've not read the paper in detail yet, so I'm afraid I will not have enough knowledge to review this PR until next week.

No worries; the core idea is rather simple. I'll keep you updated.

[hiroki-chen]

/ci-upstream-verus