The definition of data-race-free programs and the guarantee of sequential consistency
for race-free programs are equivalent to the ones in that work.
</p>
<p>
The memory model describes the requirements on program executions,
which are made up of goroutine executions,
which in turn are made up of memory operations.
</p>
<p>
A <i>memory operation</i> is modeled by four details:
</p>
<ul>
<li>its kind, indicating whether it is an ordinary data read, an ordinary data write,
or a <i>synchronizing operation</i> such as an atomic data access,
a mutex operation, or a channel operation,</li>
<li>its location in the program,</li>
<li>the memory location or variable being accessed, and</li>
<li>the values read or written by the operation.</li>
</ul>
<p>
Some memory operations are <i>read-like</i>, including read, atomic read, mutex lock, and channel receive.
Other memory operations are <i>write-like</i>, 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.
</p>
<p>
A <i>goroutine execution</i> is modeled as a set of memory operations executed by a single goroutine.
</p>
<p>
<b>Requirement 1</b>:
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 <i>sequenced before</i> relation,
defined as the partial order requirements set out by the <ahref="/ref/spec">Go language specification</a>
for Go's control flow constructs as well as the <ahref="/ref/spec#Order_of_evaluation">order of evaluation for expressions</a>.
</p>
<p>
A Go <i>program execution</i> is modeled as a set of goroutine executions,
together with a mapping <i>W</i> that specifies the write-like operation that each read-like operation reads from.
(Multiple executions of the same program can have different program executions.)
</p>
<p>
<b>Requirement 2</b>:
For a given program execution, the mapping <i>W</i>, when limited to synchronizing operations,
must be explainable by some implicit total order of the synchronizing operations
that is consistent with sequencing and the values read and written by those operations.
</p>
<p>
The <i>synchronized before</i> relation is a partial order on synchronizing memory operations,
derived from <i>W</i>.
If a synchronizing read-like memory operation <i>r</i>
observes a synchronizing write-like memory operation <i>w</i>
(that is, if <i>W</i>(<i>r</i>) = <i>w</i>),
then <i>w</i> is synchronized before <i>r</i>.
Informally, the synchronized before relation is a subset of the implied total order
mentioned in the previous paragraph,
limited to the information that <i>W</i> directly observes.
</p>
<p>
The <i>happens before</i> relation is defined as the transitive closure of the
union of the sequenced before and synchronized before relations.
</p>
<p>
<b>Requirement 3</b>:
For an ordinary (non-synchronizing) data read <i>r</i> on a memory location <i>x</i>,
<i>W</i>(<i>r</i>) must be a write <i>w</i> that is <i>visible</i> to <i>r</i>,
where visible means that both of the following hold:
</p>
<ol>
<li><i>w</i> happens before <i>r</i>.</li>
<li><i>w</i> does not happen before any other write <i>w'</i> (to <i>x</i>) that happens before <i>r</i>.</li>
</ol>
<p>
A <i>read-write data race</i> on memory location <i>x</i>
consists of a read-like memory operation <i>r</i> on <i>x</i>
and a write-like memory operation <i>w</i> on <i>x</i>,
at least one of which is non-synchronizing,
which are unordered by happens before
(that is, neither <i>r</i> happens before <i>w</i>
nor <i>w</i> happens before <i>r</i>).
</p>
<p>
A <i>write-write data race</i> on memory location <i>x</i>
consists of two write-like memory operations <i>w</i> and <i>w'</i> on <i>x</i>,
at least one of which is non-synchronizing,
which are unordered by happens before.
</p>
<p>
Note that if there are no read-write or write-write data races on memory location <i>x</i>,
then any read <i>r</i> on <i>x</i> has only one possible <i>W</i>(<i>r</i>):
the single <i>w</i> that immediately precedes it in the happens before order.
</p>
<p>
More generally, it can be shown that any Go program that is data-race-free,
meaning it has no program executions with read-write or write-write data races,
can only have outcomes explained by some sequentially consistent interleaving
of the goroutine executions.
(The proof is the same as Section 7 of Boehm and Adve's paper cited above.)
This property is called DRF-SC.
</p>
<p>
The intent of the formal definition is to match
the DRF-SC guarantee provided to race-free programs
by other languages, including C, C++, Java, JavaScript, Rust, and Swift.
</p>
<p>
Certain Go language operations such as goroutine creation and memory allocation
act as synchronization operations.
The effect of these operations on the synchronized-before partial order
is documented in the “Synchronization” section below.
Individual packages are responsible for providing similar documentation
for their own operations.
</p>
<h2id="restrictions">Implementation Restrictions for Programs Containing Data Races</h2>
<p>
The preceding section gave a formal definition of data-race-free program execution.
This section informally describes the semantics that implementations must provide
for programs that do contain races.
</p>
<p>
Any implementation can, upon detecting a data race,
report the race and halt execution of the program.
Implementations using ThreadSanitizer
(accessed with “<code>go</code><code>build</code><code>-race</code>”)
do exactly this.
</p>
<p>
A read of an array, struct, or complex number
may by implemented as a read of each individual sub-value
(array element, struct field, or real/imaginary component),
in any order.
Similarly, a write of an array, struct, or complex number
may be implemented as a write of each individual sub-value,
in any order.
</p>
<p>
A read <i>r</i> of a memory location <i>x</i>
holding a value
that is not larger than a machine word must observe
some write <i>w</i> such that <i>r</i> does not happen before <i>w</i>
and there is no write <i>w'</i> such that <i>w</i> happens before <i>w'</i>
and <i>w'</i> happens before <i>r</i>.
That is, each read must observe a value written by a preceding or concurrent write.
</p>
<p>
Additionally, observation of acausal and “out of thin air” writes is disallowed.
</p>
<p>
Reads of memory locations larger than a single machine word
are encouraged but not required to meet the same semantics
as word-sized memory locations,
observing a single allowed write <i>w</i>.
For performance reasons,
implementations may instead treat larger operations
as a set of individual machine-word-sized operations
in an unspecified order.
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.
</p>
<p>
Examples of incorrect synchronization are given in the
“Incorrect synchronization” section below.
</p>
<p>
Examples of the limitations on implementations are given in the
“Incorrect compilation” section below.
</p>
<h2id="synchronization">Synchronization</h2>
<h3id="init">Initialization</h3>
<p>
Program initialization runs in a single goroutine,
but that goroutine may create other goroutines,
which run concurrently.
</p>
<pclass="rule">
If a package <code>p</code> imports package <code>q</code>, the completion of
<code>q</code>'s <code>init</code> functions happens before the start of any of <code>p</code>'s.
</p>
<pclass="rule">
The completion of all <code>init</code> functions is synchronized before
the start of the function <code>main.main</code>.
</p>
<h3id="go">Goroutine creation</h3>
<pclass="rule">
The <code>go</code> statement that starts a new goroutine
is synchronized before the start of the goroutine's execution.
</p>
<p>
For example, in this program:
</p>
<pre>
var a string
func f() {
print(a)
}
func hello() {
a = "hello, world"
go f()
}
</pre>
<p>
calling <code>hello</code> will print <code>"hello, world"</code>
at some point in the future (perhaps after <code>hello</code> has returned).
</p>
<h3id="goexit">Goroutine destruction</h3>
<p>
The exit of a goroutine is not guaranteed to be synchronized before
any event in the program.
For example, in this program:
</p>
<pre>
var a string
func hello() {
go func() { a = "hello" }()
print(a)
}
</pre>
<p>
the assignment to <code>a</code> is not followed by
any synchronization event, so it is not guaranteed to be
observed by any other goroutine.
In fact, an aggressive compiler might delete the entire <code>go</code> statement.
</p>
<p>
If the effects of a goroutine must be observed by another goroutine,
use a synchronization mechanism such as a lock or channel
communication to establish a relative ordering.
</p>
<h3id="chan">Channel communication</h3>
<p>
Channel communication is the main method of synchronization
between goroutines. Each send on a particular channel
is matched to a corresponding receive from that channel,
usually in a different goroutine.
</p>
<pclass="rule">
A send on a channel is synchronized before the completion of the
corresponding receive from that channel.
</p>
<p>
This program:
</p>
<pre>
var c = make(chan int, 10)
var a string
func f() {
a = "hello, world"
c <- 0
}
func main() {
go f()
<-c
print(a)
}
</pre>
<p>
is guaranteed to print <code>"hello, world"</code>. The write to <code>a</code>
is sequenced before the send on <code>c</code>, which is synchronized before
the corresponding receive on <code>c</code> completes, which is sequenced before
the <code>print</code>.
</p>
<pclass="rule">
The closing of a channel is synchronized before a receive that returns a zero value
because the channel is closed.
</p>
<p>
In the previous example, replacing
<code>c <- 0</code> with <code>close(c)</code>
yields a program with the same guaranteed behavior.
</p>
<pclass="rule">
A receive from an unbuffered channel is synchronized before the completion of
the corresponding send on that channel.
</p>
<p>
This program (as above, but with the send and receive statements swapped and
using an unbuffered channel):
</p>
<pre>
var c = make(chan int)
var a string
func f() {
a = "hello, world"
<-c
}
func main() {
go f()
c <- 0
print(a)
}
</pre>
<p>
is also guaranteed to print <code>"hello, world"</code>. The write to <code>a</code>
is sequenced before the receive on <code>c</code>, which is synchronized before
the corresponding send on <code>c</code> completes, which is sequenced
before the <code>print</code>.
</p>
<p>
If the channel were buffered (e.g., <code>c = make(chan int, 1)</code>)
then the program would not be guaranteed to print
<code>"hello, world"</code>. (It might print the empty string,
crash, or do something else.)
</p>
<pclass="rule">
The <i>k</i>th receive on a channel with capacity <i>C</i> is synchronized before the completion of the <i>k</i>+<i>C</i>th send from that channel completes.
</p>
<p>
This rule generalizes the previous rule to buffered channels.
It allows a counting semaphore to be modeled by a buffered channel:
the number of items in the channel corresponds to the number of active uses,
the capacity of the channel corresponds to the maximum number of simultaneous uses,
sending an item acquires the semaphore, and receiving an item releases
the semaphore.
This is a common idiom for limiting concurrency.
</p>
<p>
This program starts a goroutine for every entry in the work list, but the
goroutines coordinate using the <code>limit</code> channel to ensure
that at most three are running work functions at a time.
</p>
<pre>
var limit = make(chan int, 3)
func main() {
for _, w := range work {
go func(w func()) {
limit <- 1
w()
<-limit
}(w)
}
select{}
}
</pre>
<h3id="locks">Locks</h3>
<p>
The <code>sync</code> package implements two lock data types,
<code>sync.Mutex</code> and <code>sync.RWMutex</code>.
</p>
<pclass="rule">
For any <code>sync.Mutex</code> or <code>sync.RWMutex</code> variable <code>l</code> and <i>n</i><<i>m</i>,
call <i>n</i> of <code>l.Unlock()</code> is synchronized before call <i>m</i> of <code>l.Lock()</code> returns.
</p>
<p>
This program:
</p>
<pre>
var l sync.Mutex
var a string
func f() {
a = "hello, world"
l.Unlock()
}
func main() {
l.Lock()
go f()
l.Lock()
print(a)
}
</pre>
<p>
is guaranteed to print <code>"hello, world"</code>.
The first call to <code>l.Unlock()</code> (in <code>f</code>) is synchronized
before the second call to <code>l.Lock()</code> (in <code>main</code>) returns,
which is sequenced before the <code>print</code>.
</p>
<pclass="rule">
For any call to <code>l.RLock</code> on a <code>sync.RWMutex</code> variable <code>l</code>,
there is an <i>n</i> such that the <i>n</i>th call to <code>l.Unlock</code>
is synchronized before the return from <code>l.RLock</code>,
and the matching call to <code>l.RUnlock</code> is synchronized before the return from call <i>n</i>+1 to <code>l.Lock</code>.
</p>
<pclass="rule">
A successful call to <code>l.TryLock</code> (or <code>l.TryRLock</code>)
is equivalent to a call to <code>l.Lock</code> (or <code>l.RLock</code>).
An unsuccessful call has no synchronizing effect at all.
