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.

[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.