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:

• [x] 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). The Verus team is also designing this part.
• [x] 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.
• Design the OS scheduler/task struct (for sound thread/preemption reasoning).
• 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]

Note: somehow blocked by the CPU local/core design. This should be left as is until that part has been merged upstream.

[rikosellic]

I notice there is also some work about the weak memory model on a Verus branch. verus-lang/verus#2716

[hiroki-chen]

I notice there is also some work about the weak memory model on a Verus branch. verus-lang/verus#2716

Seems that we all follow the same logic.

[hiroki-chen]

This PR is large so in the future I'll split it into small pieces.

[hiroki-chen]

Ready now!

[hiroki-chen]

This one is done @rikosellic @Marsman1996