《Go 语言高级编程》5.1 Go 内存模型正式定义

$ ls /usr/local/go/doc/ | grep mem
go_mem.html
$ python3 -c '
import re, html
t = open("/usr/local/go/doc/go_mem.html").read()
t = re.sub(r"<script.*?</script>", "", t, flags=re.S)
print(html.unescape(re.sub(r"<[^>]+>", "", t))[:180])'

If you must read the rest of this document to understand the behavior of your program,
you are being too clever.

Don't be clever.

A memory operation is modeled by four details:

	its kind, indicating whether it is an ordinary data read, an ordinary data write,
    or a synchronizing operation such as an atomic data access,
	a mutex operation, or a channel operation,
	its location in the program,
	the memory location or variable being accessed, and
	the values read or written by the operation.

Some memory operations are read-like, including read, atomic read, mutex lock, and channel receive.
Other memory operations are write-like, including write, atomic write, mutex unlock, channel send, and channel close.
Some, such as atomic compare-and-swap, are both read-like and write-like.

Requirement 1:
The memory operations in each goroutine must correspond to a correct sequential execution of that goroutine,
given the values read from and written to memory.
That execution must be consistent with the sequenced before relation,
defined as the partial order requirements set out by the Go language specification
for Go's control flow constructs as well as the order of evaluation for expressions.

The synchronized before relation is a partial order on synchronizing memory operations,
derived from W.
If a synchronizing read-like memory operation r
observes a synchronizing write-like memory operation w
(that is, if W(r) = w),
then w is synchronized before r.

The happens before relation is defined as the transitive closure of the
union of the sequenced before and synchronized before relations.

Requirement 3:
For an ordinary (non-synchronizing) data read r on a memory location x,
W(r) must be a write w that is visible to r,
where visible means that both of the following hold:

	w happens before r.
	w does not happen before any other write w' (to x) that happens before r.

A read-write data race on memory location x
consists of a read-like memory operation r on x
and a write-like memory operation w on x,
at least one of which is non-synchronizing,
which are unordered by happens before
(that is, neither r happens before w
nor w happens before r).

A write-write data race on memory location x
consists of two write-like memory operations w and w' on x,
at least one of which is non-synchronizing,
which are unordered by happens before.

var a, b int

func f() { a = 1; b = 2 }
func g() { print(b); print(a) }

func main() {
	go f()
	g()
}

In the absence of data races, Go programs behave as if all the goroutines
were multiplexed onto a single processor.
This property is sometimes referred to as DRF-SC: data-race-free programs
execute in a sequentially consistent manner.

A read r of a memory location x
holding a value
that is not larger than a machine word must observe
some write w such that r does not happen before w
and there is no write w' such that w happens before w'
and w' happens before r.
That is, each read must observe a value written by a preceding or concurrent write.

Additionally, observation of acausal and “out of thin air” writes is disallowed.

This means that races on multiword data structures
can lead to inconsistent values not corresponding to a single write.
When the values depend on the consistency
of internal (pointer, length) or (pointer, type) pairs,
as can be the case for interface values, maps,
slices, and strings in most Go implementations,
such races can in turn lead to arbitrary memory corruption.