Re: "Verifying and Optimizing Compact NUMA-Aware Locks on Weak Memory Models"

[Andrea Parri <parri.andrea@gmail.com>]

> FWIW, C++ defines this as (in https://eel.is/c++draft/atomics#order-11):
> 
> 	Implementations should make atomic stores visible to atomic
> 	loads within a reasonable amount of time.
> 
> in other words:
> 
> if one thread does an atomic store, then all other threads must see that
> store eventually.
> 
> (from: https://rust-lang.zulipchat.com/#narrow/stream/136281-t-lang.2Fwg-unsafe-code-guidelines/topic/Rust.20forward.20progress.20guarantees/near/294702950)
> 
> Should we add something somewhere in our model, maybe in the
> explanation.txt?

FYI, that's briefly mentioned in Section 11, "CACHE COHERENCE AND THE
COHERENCE ORDER RELATION: co, coi, and coe":

  "sequential consistency per variable and cache coherence mean the
   same thing except that cache coherence includes an extra requirement
   that every store eventually becomes visible to every CPU"

  Andrea


> Plus, I think we cannot express this in Herd because Herd uses
> graph-based model (axiomatic model) instead of an operational model to
> describe the model: axiomatic model cannot describe "something will
> eventually happen". There was also some discussion in the zulip steam
> of Rust unsafe-code-guidelines.