The proof in relaxed-memory concurrency doesn't account for dynamic participant registration
Closed this issue · 4 comments
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 before unlink()'s SC fence". Because pin()'s SC fence (3. in the timeline) is performed before try_advance()'s SC fence, the registration of the pinning participant should be visible to try_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.
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.