doc: update Go memory model

[rsc]

In June 2021 I posted a series of articles about memory models, ending with an article about changes I thought we should make to the Go memory model. See https://research.swtch.com/mm especially https://research.swtch.com/gomm.

Then I opened a GitHub Discussion to discuss these changes; see #47141.

Based on that discussion, I propose the following concrete changes to the memory model:

• Document Go's overall approach.
• Document that multiword races can cause crashes.
• Document happens-before for runtime.SetFinalizer.
• Document (or link to) happens-before for more sync types.
• Document happens-before for sync/atomic, matching C++ sequentially consistent atomics (and Java, JavaScript, Rust, Swift, C, ...)
• Document disallowed compiler optimizations.

The exact details can be viewed in pending CLs prepared for concreteness, in particular CL 381315 (memory model) and CL 381316 (library docs).

I have filed a separate proposal - #50860 - for another item that arose during that discussion, namely adding typed atomic values to sync/atomic.

[gopherbot]

Change https://golang.org/cl/381315 mentions this issue: doc: update Go memory model

[gopherbot]

Change https://golang.org/cl/381316 mentions this issue: runtime, sync, sync/atomic: document happens-before guarantees

[rsc]

This proposal has been added to the active column of the proposals project
and will now be reviewed at the weekly proposal review meetings.
— rsc for the proposal review group

[rsc]

Based on feedback from ARM, I revised the examples toward the end of the memory model to remove the implication that hoisting reads (provided they don't fault) out of conditionals is always problematic.

[rsc]

Does anyone object to accepting this proposal?

[hboehm]

Sorry about leaving a comment on the CL before seeing the comment not to. I continue to believe there are serious problems with the approach, which I will again offer to discuss.

[rsc]

Thanks @hboehm. I will take you up on that offer.

[rsc]

To update the issue here, I had a good discussion with @hboehm.

Hans's primary objection is that the new text claims that Go provides DRF-SC but that the rules given in the current draft are not strong enough to support that claim.

My goal for the current rules is to try to restrict what compilers are allowed to do, to avoid cleverness like reloading a value from memory rather than spilling it to a private location like the stack. In general my goal is to say to users "don't depend on the behavior of racy programs" while at the same time say to compiler writers (in contrast to C/C++) "don't assume programs are race-free / make races worse". That is, we might call this "DRF-SC but avoid catching fire".

Hans believes that for the user part, it should be possible to reduce the C++ DRF-SC model down to something that is reasonable for Go (and much simpler than C++, since we don't have relaxed atomics), and that the compiler writer part can be delivered as informal implementation advice. I am going to look into this approach.

[rsc]

Hans also pointed me at http://www.open-std.org/jtc1/sc22/wg21/docs/papers/2019/p1217r2.html, in particular the section titled "A new class of out-of-thin-air results", which is certainly worrying. We currently do not allow relaxed atomic loads/stores, but if we did start thinking about those operations, we would need to grapple with what those programs should be allowed to do.

[rsc]

I have updated the text based on a discussion with @hboehm from early April. The main change is to start with a "here are the semantics for race-free programs" section, which explicitly aligns with C, C++, Java, JavaScript, Rust, Swift, and so on. Then the old text limiting the damage possible in racy programs follows as an informal implementation restriction.

In my head, this new text says what I always wanted to say and is a no-op. But formally, it actually says the right things so that race-free programs can be proved to provide sequentially consistent semantics (DRF-SC).

The diff is https://go-review.googlesource.com/c/go/+/381315/5..6.

[rsc]

Based on the discussion above, this proposal seems like a likely accept.
— rsc for the proposal review group