Closed jeehoonkang closed 6 years ago
Hmm, indeed - that's a nice catch! Want to update the text?
I'll make a correction soon.
What will be the best practice for modifying an existing RFC? I prefer just sending a PR, instead of sending another RFC that supersedes an old one. What you think?
Yeah, just create a normal PR.
Proof: https://github.com/crossbeam-rs/rfcs/blob/master/text/2017-07-23-relaxed-memory.md
It assumes that the set of participants ("threads" in the RFC text) is constant. But actually a new participant can join the registry. The proof doesn't account for this possibility of dynamic participant registration.
Fortunately, the proof doesn't seem broken. But we need to update the third bullet of "When
pin()
's SC fence is performed beforeunlink()
's SC fence". Becausepin()
's SC fence (3. in the timeline) is performed beforetry_advance()
's SC fence, the registration of the pinning participant should be visible totry_advance(): 'L42
, where the registered participants are iterated over. Thus the loop should visit the pinning participant, and the rest of the proof is exactly the same.