When doing verification on the weak memory model, scheduling, RCU stuff, it becomes more urgent for us to have a spec model to articulate the "CPU local" semantics so that we can reason about, e.g., what kind of tasks are currently running on the current CPU.
This should be beneficial even if we don't need the weak memory model for now as the next stage involves TLB, mm push-forwards which need a more accurate CPU-local semantic too.
@rikosellic How do you think?
When doing verification on the weak memory model, scheduling, RCU stuff, it becomes more urgent for us to have a spec model to articulate the "CPU local" semantics so that we can reason about, e.g., what kind of tasks are currently running on the current CPU.
This should be beneficial even if we don't need the weak memory model for now as the next stage involves TLB, mm push-forwards which need a more accurate CPU-local semantic too.
@rikosellic How do you think?