11institutetext: Dept. of Informatics, University of Oslo

# Ready, set, Go!

Data-race detection and the Go language††thanks: Supported by the bilateral
project UTF-2018-CAPES-Diku/10001 “Modern Refactoring”.

Daniel Schnetzer Fava Martin Steffen
<EMAIL_ADDRESS><EMAIL_ADDRESS>
###### Abstract

Data races are often discussed in the context of lock acquisition and release,
with race-detection algorithms routinely relying on _vector clocks_ as a means
of capturing the relative ordering of events from different threads. In this
paper, we present a data-race detector for a language with channel
communication as its sole synchronization primitive, and provide a semantics
directly tied to the _happens-before_ relation, thus forging the notion of
vector clocks.

##  1 Introduction

One way of dealing with complexity is by partitioning a system into
cooperating subcomponents. When these subcomponents compete for resources,
coordination becomes a prominent goal. One common programming paradigm is to
have threads cooperating around a pool of shared memory. In this case,
coordination involves, for example, avoiding conflicting accesses to memory.
Two concurrent accesses constitute a _data race_ if they reference the same
memory location and at least one of the accesses is a write. Because data
races can lead to counter intuitive behavior, it is important to detect them.

The problem of data-race detection in shared memory systems is well studied in
the context of lock acquisition and release. When it comes to message passing,
the problem of concurrent accesses to _channels_ , in the absence of shared
memory, is also well studied—the goal, in these cases, is to achieve
determinism rather than race-freedom [6, 7, 38]. What is less prominent in the
race-detection literature is the study of channel communication as the
synchronization primitive for shared memory systems. In this paper, we present
exactly that; a dynamic data-race detector for a language in the style of Go,
featuring channel communication as means of coordinating accesses to shared
memory.

We fix the syntax of our calculus in Section 3 and present a corresponding
operational semantics. The configurations of the semantics keep track of
memory events (i.e. of read and write accesses to shared variables) such that
the semantics can be used to detect races. A proper book-keeping of events
also involves tracking _happens-before_ information. In the absence of a
global clock, the happens-before relation is a vehicle for reasoning about the
relative order of execution of different threads [18]. We describe the race
detection task and present a framework, called Grace [9], that is based on
what we call _happens-before sets_. Different from other race detectors, which
often employ vector clocks (VCs) as a mechanism for capturing the happen-
before relation, we tie our formalization more closely to the concept of
happens-before. The proposed approach, based on what we call happens-before
sets, allows for garbage collection of “stale” memory access information that
would otherwise be tracked. Although, in the worst case, the proposed detector
requires a larger foot-print when compared to VC-based implementations, we
conjecture the existence of a hybrid approach that can offer benefits from
both worlds.

Our race detector is built upon a previous result [10], where we formalize a
weak memory model inspired by the Go specification [12]. The core of the paper
was a proof of the DRF-SC guarantee, meaning, we proved that the proposed
relaxed memory model behaves Sequentially Consistently (SC) when running Data-
Race Free (DRF) programs. The proof hinges on the fact that, in the absence of
races, all threads agree on the contents of memory. The scaffolding used in
the proof contains the ingredients for the race detector presented in this
paper. We should point out, however, that the operational semantics presented
here and used for race detection is _not_ a weak semantics.111Note that while
the mentioned semantics of [10] differs from the one presented here, both
share some commonalities. Both representations are based on appropriately
recording information of previous read and write events in their run-time
configuration. In both versions, a crucial ingredient of the book-keeping is
connecting events in happens-before relation. The purpose of the book-keeping
of events, however, is different: in [10], the happens-before relation serves
to operationally formalize the weak memory model (corresponding roughly to
PSO) in the presence of channel communication. In the current paper, the same
relation serves to obtain a race detector. Both versions of the semantics are
connected by the DRF-SC result, as mentioned. Apart from the additional
information for race detection, the semantics is “strong” in that it
formalizes a memory guaranteeing _sequential consistency._ To focus on a form
of strong memory is not a limitation. Since we have established that a
corresponding weak semantics enjoys the crucial DRF-SC property [10], the
strong and weak semantics agree up to the first encountered race condition.
Given that even racy program behaves sequentially consistently up to the point
in which the first data-race is encountered, a complete race detector can
safely operate under the assumption of sequential consistency.

The remainder of the paper is organized as follows. Section 2 presents
background information on data races and synchronization via message passing
that are directly related to the formalization of our approach to race
detection. Section 3 formalizes race detection in the context of channel
communication as sole synchronization mechanism. We turn our attention to the
issue of efficiency in Section 4. Section 5 gives a detailed comparison of our
algorithm and VC-based algorithms for the acquire-release semantics. Section 6
puts our work in the perspective of trace theory. Section 7 examines related
work. Section 8 provides a conclusion and touches on future work.

##  2 Background

##### Read and write conflicts.

Memory accesses conflict if they target the same location and at least one of
the accesses is a _write_ —there are no read-read conflicts. A data race
constitutes of conflicting accesses that are unsynchronized.

Listing 1: Program with race condition. [12]

⬇

var a string

func main() {

go func() { a = ”hello” }()

print(a)

}

Take the Go code of Listing 1 as an example. There, the main function invokes
an anonymous function; this anonymous function sets the global variable “a” to
“hello”. Note, however, that the call is prepended with the keyword go. When
this keyword is present in a function invocation, Go spawns a new thread (or
goroutine), and the caller continues execution without waiting for the callee
to return. The main and the anonymous functions access the same shared
variable in a conflicting manner (i.e. one of the accesses is a write). Since
both the main and the anonymous functions run in parallel and no
synchronization is used (as evidenced by the lack of channel communication),
the two accesses are also concurrent. This allows us to conclude that this
program has a race.

A data race _manifests_ itself when an execution step is immediately followed
by another and the two steps are conflicting. This definition is the closest
one can get to a notion of simultaneity in an operational semantics, where
memory interactions are modeled as instantaneous atomic steps. While manifest
races are obvious and easy to account for, races in general can involve
accesses that are arbitrarily far apart in a linear execution. A “memory-less”
detector can fail to report races, for example non-manifest races, that could
otherwise be flagged by more sophisticated race detectors. The ability to flag
non-manifest data-races is correlated with the amount of information kept and
the length in which this information is kept for. In general, recording more
information and storing it for longer leads to higher degrees of
“completeness” at the expense of higher run-time overheads.222It should go
without saying that observing one execution as being race free is not enough
to assert race-freedom of the program, even if one has observed a complete
trace of a terminating run of a program. Completeness can at best be expected
with respect to alternative schedules or linearizations of a given execution.

We break down the notions of read-write and write-write conflicts into a more
fine-grained distinction. Inspired by the notion of data hazards in the
computer architecture literature, we break down read-write conflicts into
read-after-write (RaW) and write-after-read (WaR) conflicts. To keep
consistent with this nomenclature, we refer to write-write conflicts as write-
after-write (WaW).333The mentioned “temporal” ordering and the use of the word
“after” refers to the occurrence of events in the trace or execution of the
running program. It is incorrect to conflate the concept of happens-before
with the ordering of occurrences in a trace. For instance, in a RaW situation,
the read step occurs after a write in an execution, i.e., the read is
mentioned after the write in the linearization. This order of occurrence does
_not_ mean, however, that the read happens-after the write or, conversely, the
write happens-before the read. Actually, for a RaW race (same as for the other
kinds of races), the read occurs after the write but the accesses are
_concurrent_ , which means that they are _unordered_ as far as the happens-
before relation is concerned. Going back to the example in Listing 1, there
are two possible executions: one in which the spawned goroutine writes “hello”
to the shared variable after the main function prints it, and another
execution in which the print occurs after the writing of the variable. The
first execution illustrates a write-after-read race, while the first
illustrates a read-after-write. Note that this example does not contain a
write-after-write race.

We make the distinction between the detection of after-write races and the
detection of write-after-read ones. As we will see in Section 3.3, the
detection of after-write races can be done with little overhead. The detection
of after-read, however, cannot.

When reading or writing a variable, it must be checked that conflicting
accesses _happened-before_ the current access. The check must happen from the
perspective of the thread attempting the access. In other words, the question
of whether an event occurred in the “definite past” (i.e., whether an event is
in happened-before relation with “now”) is _thread-local_ ; threads can have
different views on whether an event belongs to the past. This thread-local
nature is less surprising than it may sound: if one threads executes two steps
in sequence, the second step can safely assume that the first has taken
effect; after all, that is what the programmer must have intended by
sequentially composing instructions in the given program order. Such
guarantees hold locally, which is to say that the semantics _respects program
order within a thread_. It is possible, however, for steps to not take effect
in program order. A compiler or hardware may rearrange instructions, and it
often does so in practice. What must remain true is that these reorderings
cannot be observable from the perspective of a single thread. When it comes to
more than one thread, however, agreement on what constitutes the past cannot
be achieved without synchronization. Synchronization and consensus are
integrally related.444In the context of channel communication and weak memory,
the connection between synchronization and consensus is discussed in a precise
manner in our previous work; see the _consensus lemmas_ of [10]. Specifically,
given a thread $t$, events from a different thread $t^{\prime}$ are not in the
past of $t$ unless synchronization forces them to be.

##### Synchronization via bounded channels.

In the calculus presented here, channel communication is the only way in which
threads synchronize. Channels can be created dynamically and closed; they are
also first-class data, which means channel identifiers can be passed as
arguments, stored in variables, and sent over channels. Send and receive
operations are central to synchronization. Clearly, a receive statement is
synchronizing in that it is potentially blocking: a thread blocks when
attempting to receive from an empty channel until, if ever, a value is made
available by a sender. Since channels here are bounded, there is also
potential for blocking when sending, namely, when attempting to send on a
channel that is full.

We can use a channel c to eliminate the data race in Listing 1 as follows: the
anonymous function sends a message to communicate that the shared variable has
been set. Meanwhile, the main thread receives from the channel before printing
the shared variable.

Listing 2: Repaired program.

⬇

var a string

var c = make(chan bool, 1);

func main() {

go func() { a = ”hello”; c <- true }()

<- c

print(a)

}

The happens-before memory model stipulates, not surprisingly, a causal
relationship between the communicating partners [12]:

A send on $c$ happens-before the corresponding receive from $c$ completes. (1)

Given that channels have finite capacity, a thread remains blocked when
sending on a full channel until, if ever, another process frees a slot in the
channel’s buffer. In other words, the sender is blocked until another thread
receives from the channel. Correspondingly, there is a happens-before
relationship between a receive and a subsequent send on a channel with
capacity $k$ [12]:

The $i^{\mathit{th}}$ receive from $c$ happens-before the
$(i+k)^{\mathit{th}}$ send on $c$ completes. (2)

Interestingly, because of this rule, a causal connection is forged between the
sender and _some previous_ receiver who is otherwise unrelated to the current
send operation. When multiple senders and receivers share a channel, rule (2)
implies that it is possible for two threads to become related (via happens-
before) without ever directly exchanging a message.555Communication means
sending a message to or receiving a message from a channel; messages are not
addressed to or received from specific threads. Thus, sharing the channel by
performing sends and receives does not necessarily make two threads
“communication partners.” Two threads are partners when one receives a message
deposited by the other.

The indirect relation between a sender and a prior receiver, postulated by
rule (2), allows channels to be used as locks. In fact, free and taken binary
locks are analogous to empty and full channels of capacity one. A process
takes and releases locks for the purpose of synchronization (such as assuring
mutually exclusive access to shared data) without being aware of
“synchronization partners.” In the (mis-)use of channels as locks, there is
also no inter-process communication. Instead, a process “communicates” with
itself: In a proper lock protocol, the process holding a lock (i.e. having
performed a send onto a channel) is the only one supposed to release the lock
(i.e. performing the corresponding receive). Thus, a process using a channel
as lock receives its own previously sent message—there is no direct inter-
process exchange. Note, however, synchronization still occurs: subsequent
accesses to a critical region are denied by sending onto a channel and making
it full. See Section 3.5.2 for a more technical elaboration.

To establish a happens-before relation between sends and receives, note the
distinction, between a channel operation and its _completion_ in the
formulation of rules (1) and (2). The order of events in a concurrent system
is partial; not only that, it is strictly partial since we don’t think of an
event as happening-before itself. A strict partial order is an irreflexive,
transitive, and asymmetric relation. In the case of synchronous channels, if
we were to ignore the distinction between an event and its completion,
according to rule (1), a send would then happen-before its corresponding
receive, and, according to rule (2), the receive would happen-before the send.
This cycle breaks asymmetry. Asymmetry can be repaired by interpreting a
send/receive pair on a synchronous channel as a single operation; indeed, it
can be interpreted as a _rendezvous_.

The distinction between a channel operation and its completion is arguably
more impactful when it comes to buffered channels. For one, it prevents sends
from being in happens-before with other sends, and receives from being in
happens-before with other receives. To illustrate, let
$\mathrel{\mathtt{sd}}^{i}$ and $\mathrel{\mathtt{rv}}^{i}$ represent the
$i^{\mathit{th}}$ send and receive on a channel. If we remove from rules (1)
and (2) the distinction between an operation and its completion, the
$i^{\mathit{th}}$ receive would then happens-before the $(i+k)^{\mathit{th}}$
send—based on rule (2)—and the $(i+k)^{\mathit{th}}$ send would happens-before
the $(i+k)^{\mathit{th}}$ receive—based on rule (1):

$\mathrel{\mathtt{rv}}^{i}~{}\rightarrow_{\mathsf{hb}}~{}\mathrel{\mathtt{sd}}^{i+k}~{}\rightarrow_{\mathsf{hb}}~{}\mathrel{\mathtt{rv}}^{i+k}$

By transitivity of the happens-before relation, we would then conclude that
the $i^{\mathit{th}}$ receive happens-before the $(i+k)^{\mathit{th}}$
receive, which would happen-before the $(i+2k)^{\mathit{th}}$ receive and so
on. As a consequence, a receive operation would have a lingering effect
through-out the execution of the program—similarly for send operations. This
accumulation of effects can be counter intuitive for the application
programmer, who would be forced to reason about arbitrarily long histories.

##  3 Data-race detection

We start in Section 3.1 by presenting the abstract syntax of our calculus and,
in Section 3.2, an overview of the operational semantics used for data-race
detection. The race detector itself is introduced incrementally. We start in
Section 3.3 with a simple detector that has a small footprint but that is
limited to detecting after-write races. We build onto this first iteration of
the detector in Section 3.4, making it capable of detecting after-write as
well as after-read races. The detector’s operation is illustrated by examples
in Section 3.5. Later, in Section 4, we turn to the issue of efficiency and
introduce “garbage collection” as a mean to reduce the detector’s footprint.
These race detectors can be seen as augmented versions of an underlying
semantics without additional book-keeping related to race checking. This
“undecorated” semantics, including the definition of internal steps and a
notion of structural congruence, can be found in Appendix
LABEL:sec:gomm.race.semantics.strong.

###  3.1 A calculus with shared variables and channel communication

We formalize our ideas in terms of an idealized language shown in Figure 1 and
inspired by the Go programming language.

$\begin{array}[t]{rcl@{\quad}l}v&::=&r\ \mathrel{|}\
\underline{n}&\text{values}\\\ e&::=&t\ \mathrel{|}\ v\ \mathrel{|}\
\mathrel{\mathtt{load}}z\ \mathrel{|}\ z:=v\ \mathrel{|}\
\mathrel{\mathtt{go}}t&\text{expressions}\\\ &\
\mathrel{|}&\mathrel{\mathtt{if}}v\mathrel{\mathtt{then}}t\mathrel{\mathtt{else}}t\\\
&\ \mathrel{|}&\mathrel{\mathtt{make}}(\mathrel{\mathtt{chan}}T,v)\
\mathrel{|}\ \mathop{\leftarrow v}\ \mathrel{|}\ v\leftarrow v\ \mathrel{|}\
\mathrel{\mathtt{close}}v&\\\ g&::=&v\leftarrow v\ \mathrel{|}\
\mathop{\leftarrow v}\ \mathrel{|}\
\mathrel{\mathtt{default}}&\text{guards}\\\
t&::=&\mathrel{\mathtt{let}}r=e\mathrel{\mathtt{in}}t\ \mathrel{|}\
\sum_{i}\mathrel{\mathtt{let}}r_{i}=g_{i}\mathrel{\mathtt{in}}t_{i}&\text{threads}\end{array}$
Figure 1: Abstract syntax

The syntax is basically unchanged from [10]. _Values_ $v$ can be of two forms:
$r$ denotes local variables or registers; $n$ is used to denote references or
names in general and, in specific, $p$ for processes or goroutines, $m$ for
memory events, and $c$ for channel names. We do not explicitly list values
such as the unit value, booleans, integers, etc. We also omit compound local
expressions like $e_{1}+e_{2}$. Shared variables are denoted by $x$, $z$,
etc., $\mathrel{\mathtt{load}}z$ represents reading the shared variable $z$
into the thread, and $z:=v$ denotes writing to $z$. References are dynamically
created. A new channel is created by
$\mathrel{\mathtt{make}}(\mathrel{\mathtt{chan}}T,v)$, where $T$ represents
the type of values carried by the channel and $v$ a non-negative integer
specifying the channel’s capacity. Sending a value $v$ over a channel $c$ and
receiving a value as input from a channel are denoted respectively as
$c\leftarrow v$ and $\mathop{\leftarrow c}$. After the operation
$\mathrel{\mathtt{close}}$, no further values can be sent on the specified
channel. Attempting to send values on a closed channel leads to a panic.

Starting a new asynchronous activity, called goroutine in Go, is done using
the $\mathrel{\mathtt{go}}$-keyword. In Go, the
$\mathrel{\mathtt{go}}$-statement is applied to function calls only. We omit
function calls, asynchronous or otherwise, as they are orthogonal to the
memory model’s formalization. The select-statement, here written using the
$\sum$-symbol, consists of a finite set of branches (or communication clauses
in Go-terminology). These branches act as guarded threads. General expressions
in Go can serve as guards. Our syntax requires that only communication
statements (i.e., channel sending and receiving) and the
$\mathrel{\mathtt{default}}$-keyword can serve as guards. This does not reduce
expressivity and corresponds to an A-normal form representation [32]. At most
one branch is guarded by $\mathrel{\mathtt{default}}$ in each select-
statement. The same channel can be mentioned in more than one guard. “Mixed
choices” [27, 28] are also allowed, meaning that sending- and receiving-guards
can both be used in the same select-statement. We use
$\mathrel{\mathtt{stop}}$ as syntactic sugar for the empty select statement;
it represents a permanently blocked thread. The
$\mathrel{\mathtt{stop}}$-thread is also the only way to syntactically
“terminate” a thread, meaning that it is the only element of $t$ without
syntactic sub-terms.

The $\mathrel{\mathtt{let}}$-construct
$\mathrel{\mathtt{let}}r=e\mathrel{\mathtt{in}}t$ combines sequential
composition and scoping for local variables $r$. After evaluating $e$, the
rest $t$ is evaluated where the resulting value of $e$ is handed over using
$r$. The let-construct acts as a binder for variable $r$ in $t$. When $r$ does
not occur free in $t$, $\mathrel{\mathtt{let}}$ boils down to _sequential
composition_ and, therefore, is more conveniently written with a semicolon.
See also Figure LABEL:fig:race.syn.sugar in the appendix for syntactic sugar.

###  3.2 Overview of the operational semantics

To capture the notion of ordering of events between threads, an otherwise
unadorned operational semantics (equation (LABEL:eq:gomm.race.naked.configs))
is equipped with additional information: each thread and memory location
tracks the events it is aware of as having happened-before—see the happens-
before set $E_{\mathit{hb}}$ in the run-time configurations of equation (3)
and (4), this set is present in terms corresponding to threads, $p\langle
E_{\mathit{hb}},t\rangle$, as well as memory locations,
$(\\!\\!|E_{\mathit{hb}},\,z{:=}v|\\!\\!)$ or
$m(\\!\\!|E_{\mathit{hb}}^{r},\,z{:=}v|\\!\\!)$. Depending on the capabilities
of the race detector, slightly different information is tracked as having
happened-before (i.e. stored in a happens-before set).

####  3.2.1 After-write races

When detecting after-write races (i.e. RaW and WaW), in order to know whether
a subsequent access to the same variable occurs without proper
synchronization, one has to remember additional information concerning past
write-events. Specifically, it must be checked that all write events to the
same variable _happened-before_ the current access. The happens-before set is
then used to store information pertaining to write events; read events are not
tracked. Also, terms representing a memory location have a different shape
when compared to the undecorated semantics. In the undecorated semantics, the
content $v$ of a variable $z$ is written as a pair $(\\!\\!|z{:=}v|\\!\\!)$.
When after-write races come into play, it is not enough to store the last
value written to each variable; we also need to identify write events
associated with the variable. Thus, an entry in memory takes the form
$(\\!\\!|E_{\mathit{hb}},\,z{:=}v|\\!\\!)$ where $E_{\mathit{hb}}$ holds
identifiers $m$, $m^{\prime}$, etc. that uniquely identify write events to
$z$—contrast the run-time configurations in equation
(LABEL:eq:gomm.race.naked.configs) and (3). The number of prior write events
that need to be tracked can be reduced for the sake of efficiency, in which
case the term representing a memory location takes the form
$m(\\!\\!|E_{\mathit{hb}}^{r},\,z{:=}v|\\!\\!)$ where $m$ is the identifier of
the most recent write to $z$. See equation (4).

####  3.2.2 Write-after-read races

Besides the detailed coverage of RaW and WaW races in Section 3.3, we describe
the detection of _write-after-read_ races in Section 3.4. When it comes to
WaR, the race checker needs to remember information about past reads in
addition to past write events. Abstractly, a read event represents the fact
that a load-statement has executed. Thus, the set $E_{\mathit{hb}}$ of an
entry $(\\!\\!|E_{\mathit{hb}},\,z{:=}v|\\!\\!)$ in memory holds identifiers
of both read and write events.

In the strong semantics, a read always observes one definite value which is
the result of one particular write event. Therefore, the configuration
contains entries of the form $m(\\!\\!|E_{\mathit{hb}}^{r},\,z{:=}v|\\!\\!)$
where $m$ is the identifier of the “last” write event and
$E_{\mathit{hb}}^{r}$ is a set of identifiers of read events, namely those
that accumulated after $m$. Note that “records” of the form
$m(\\!\\!|E_{\mathit{hb}}^{r},\,z{:=}v|\\!\\!)$ can be seen as $n+1$ recorded
events, one write event together with $n\geq 0$ read-events. This definition
of records with one write per variable stands in contrast to a weak semantics,
where many different write events may be observable by a given read [10].

####  3.2.3 Synchronization

Channel communication propagates happens-before information between threads,
and thus, affects synchronization. In the operational rules, each channel $c$
is actually realized with _two_ channels, which we refer to as _forward_ ,
$c_{f}$, and _backward_ , $c_{b}$—see Figure 4. The forward part serves to
communicate a value transmitted from a sender to a receiver; it also
stipulates a causal relationship between the communicating partners [12]—see
rule (1) of page 1. To capture this relationship in the context of race
checking, the sender also communicates its current information about the
happens-before relation to the receiver. The communication of happens-before
information is accomplished by the transmission of $E_{\mathit{hb}}$ over
channels; see rule R-Rec in Figure 4.

The memory model also stipulates a happens-before relationship between a
receive and a subsequent send on a channel with capacity $k$—see rule (2) of
page 2. While we refer to the _forward channel_ as carrying a message from a
sender to a receiver, the backward part of the channel is used to model the
indirect connection between some prior receiver and a current sender; see
R-Send in Figure 4.

The interplay between forward and backward channels can also be understood as
a form of flow control. Entries in the backward channel’s queue are not values
deposited by threads. Instead, they can be seen as tickets that grant senders
a free slot in the communication channel, i.e., the forward channel.666In the
case of lossy channels, backward channels are sometimes used for the purpose
of error control and regulating message retransmissions, where the receiver of
messages informs the sender about the successful or also non-successful
reception of a message. Here, channels are assumed non-lossy and there is no
need for error control. In that sense, the term “backward” should not be
interpreted as communication _back_ to the receiver in the form of an
acknowledgment. Thus, the number of “messages” in the backward channel capture
the notion of fullness: a channel is full if the backward channel is empty.
See rule R-Send in Figure 4 or Figure 0.A.3 for the underlying semantics
without race checking. When a channel of capacity $k$ is created, the forward
queue is empty and the backward queue is initialized so that it contains dummy
elements ${E_{\mathit{hb}}}_{\bot}$ (cf. rule R-Make). The dummy elements
represent the number of empty or free slots in the channel. Upon creation, the
number of dummy elements equals the capacity of the channel.

As discussed in Section 2, there is a distinction between a synchronization
operation and its completion. A send/receive pair on a synchronous channel can
be seen as a rendezvous operation; captured in our semantics by the R-Rend
reduction rule of Figure 4. When it comes to asynchronous communication, the
distinction between a channel operation and its completion is handled by the
fact that send and receive operations update a thread’s local state but do not
immediately transmit the updated state onto the channel—see rules R-Send and
R-Rec in Figure 4.

###  3.3 Detecting read-after-write (RaW) and write-after-write (WaW) races

To detect “after-write” races, run-time configurations are given following
syntax:

$R::=p\langle E_{\mathit{hb}},t\rangle\ \mathrel{|}\
(\\!\\!|E_{\mathit{hb}}^{z},\,z{:=}v|\\!\\!)\ \mathrel{|}\ \bullet\
\mathrel{|}\ R\parallel R\ \ \mathrel{|}\ c[q]\ \mathrel{|}\ \nu n\ R\ .$ (3)

Configurations are considered up-to structural congruence, with the empty
configuration $\bullet$ as neutral element and $\parallel$ as associative and
commutative. The definition is standard and included in Appendix
LABEL:sec:gomm.race.cong. Likewise relegated to the appendix are _local_
reduction rules, i.e., those not referring to shared variables or channels
(see Appendix LABEL:sec:gomm.race.steps.local).

In the configurations, a triple $(\\!\\!|E_{\mathit{hb}}^{z},\,z{:=}v|\\!\\!)$
not only stores the current value of $z$ but also records the unique
identifiers $m$, $m^{\prime}$, etc of every write _event_ to $z$ in
$E_{\mathit{hb}}^{z}$.777We will later use the term “event” also when talking
about histories or traces. There, events carry slightly different information.
For instance, being interested in the question whether a history contains
evidence of a race, it won’t be necessary to mention the actual value being
written in the write event in the history. Both notions of events, of course,
hang closely together. It should be clear from the context whether we are
referring to events as part of a linear history or recorded as part of the
configuration. When being precise, we refer to a configuration event as
_recorded_ event. Since recorded events in the semantics are uniquely labeled,
we also allow ourselves to use words like “event $m$” even if $m$ is just the
identifier for the recorded event $m(\\!\\!|z{:=}v|\\!\\!)$. A write to memory
updates a variable’s value and also generates a fresh identifier $m$. In order
to record the write event, the tuple
${\color[rgb]{0.7,0.2,0.2}\definecolor[named]{pgfstrokecolor}{rgb}{0.7,0.2,0.2}{(m,!z)}}$
is placed in the happens-before set of the term representing the memory
location that has been written to. The initial configuration starts with one
write-event per variable and the semantics maintains this uniqueness as an
invariant. In effect, the collection of recorded write events behave as a
mapping from variable to values.888The fact that memory behaves like a mapping
is consistent with the strong memory assumption.

A thread $t$ is represented as $p\langle E_{\mathit{hb}},t\rangle$ at run-
time, with $p$ serving as identifier. To be able to determine whether a next
action should be flagged as race or not, a goroutine keeps track of happens-
before information corresponding to past write events. An event mentioned in
$E_{\mathit{hb}}$ is an event of the past, as opposed to being an event that
simply occurred in a prior step. An event is “concurrent” if it occurred in a
prior step but is not in happens-before relation with the current thread
state. Concurrent memory events are potentially in conflict with a thread’s
next step. More precisely, if the memory record
$(\\!\\!|E_{\mathit{hb}}^{z},\,z{:=}v|\\!\\!)$ is part of the configuration,
then it is safe for thread $p\langle E_{\mathit{hb}},t\rangle$ to write to $z$
if $E_{\mathit{hb}}^{z}\subseteq E_{\mathit{hb}}$. Otherwise, there exist a
write to $z$ that is not accounted for by thread $p$ and a WaW conflict is
raised. Similar when reading from a variable.

Data-races are marked as a transition to an exception $\mathsf{E}$—see the
derivation rules of Figure 3, and, when write-after-read races are considered,
Figure 7. The exception takes as argument a set containing the prior memory
operations that conflict and are concurrent with the attempted memory access.

$\begin{array}[b]{l}{\small{tensy\vbox{\hbox spread0.0pt{\hskip 0.0pt plus
0.0001fil\hbox{$\displaystyle\penalty
1{{\begin{array}[]{c}E_{\mathit{hb}}^{z}\subseteq
E_{\mathit{hb}}\quad\quad\mathit{fresh}(m^{\prime})\quad\quad
E_{\mathit{hb}}^{\prime}=\\{{\color[rgb]{0.7,0.2,0.2}\definecolor[named]{pgfstrokecolor}{rgb}{0.7,0.2,0.2}{(m^{\prime},!z)}}\\}\cup
E_{\mathit{hb}}\quad\quad E_{\mathit{hb}}^{\prime
z}=\\{{\color[rgb]{0.7,0.2,0.2}\definecolor[named]{pgfstrokecolor}{rgb}{0.7,0.2,0.2}{(m^{\prime},!z)}}\\}\cup
E_{\mathit{hb}}^{z}\end{array}}}$}\hskip 0.0pt plus
0.0001fil}\hbox{\hbox{\kern 0.0pt\vrule
height=0.25002pt,depth=0.25002pt,width=282.58698pt\hbox{\kern
2.70003pt$\mbox{{R-Write}}$}}}\hbox{\kern 35.20657pt\hbox{$\displaystyle
p\langle
E_{\mathit{hb}},z:=v^{\prime};t\rangle\parallel(\\!\\!|E_{\mathit{hb}}^{z},\,z{:=}v|\\!\\!)\xrightarrow{}p\langle
E_{\mathit{hb}}^{\prime},t\rangle\parallel(\\!\\!|E_{\mathit{hb}}^{\prime
z},\,z{:=}v^{\prime}|\\!\\!)$}}}\par}}\\\ \\\\[-11.00008pt] \end{array}$

Figure 2: Operational semantics augmented for RaW and WaW race detection

$\begin{array}[b]{l}{\small{tensy\vbox{\hbox spread0.0pt{\hskip 0.0pt plus
0.0001fil\hbox{\kern 58.79764pt\hbox{$\displaystyle\penalty
1{{\begin{array}[]{c}E_{\mathit{hb}}^{z}\not\subseteq
E_{\mathit{hb}}\end{array}}}$}}\hskip 0.0pt plus 0.0001fil}\hbox{\hbox{\kern
0.0pt\vrule height=0.25002pt,depth=0.25002pt,width=166.59026pt\hbox{\kern
2.70003pt$\mbox{{R-Write-$\mathsf{E}_{WaW}$}}$}}}\hbox{\kern
0.0pt\hbox{$\displaystyle p\langle
E_{\mathit{hb}},z:=v^{\prime};t\rangle\parallel(\\!\\!|E_{\mathit{hb}}^{z},\,z{:=}v|\\!\\!)\xrightarrow{}\mathsf{E}\left({E_{\mathit{hb}}^{z}-E_{\mathit{hb}}}\right)$}}}\vspace{2pt}\par}}\\\
\\\\[-11.00008pt] \end{array}$

Figure 3: Exception conditions for RaW and WaW data-race detection

Goroutines synchronize via message passing, which means that channel
communication must transfer happens-before information between goroutines.
Suppose a goroutine $p$ has just updated variable $z$ thus generating the
unique label $m$. The tuple
${\color[rgb]{0.7,0.2,0.2}\definecolor[named]{pgfstrokecolor}{rgb}{0.7,0.2,0.2}{(m,!z)}}$
is placed in the happens-before set of both the thread $p$ and the memory
record associated with $z$. At this point, $p$ is the only goroutine whose
happens-before set contains the label $m$ associated with this write-record.
No other goroutine can read or write to $z$ without causing a data-race. When
$p$ sends a message onto a channel, the information about $m$ is also sent.
Suppose now that a thread $p^{\prime}$ reads from the channel and receives the
corresponding message before $p$ makes any further modifications to $z$. The
tuple
${\color[rgb]{0.7,0.2,0.2}\definecolor[named]{pgfstrokecolor}{rgb}{0.7,0.2,0.2}{(m,!z)}}$
is added to $p^{\prime}$’s happens-before set, so both $p$ and $p^{\prime}$
are aware of $z$’s most recent write to $z$. The existence of $m$ in both
goroutine’s happens-before sets implies that either $p$ or $p^{\prime}$ are
allowed to update $z$’s value. The rules for channel communication are given
in Figure 4. They will remain unchanged when we extend the treatment to RaW
conflicts. The exchange of happens-before information via channel
communication is also analogous to the treatment of the weak semantics in
[10].

$\begin{array}[b]{l}{\small{tensy\vbox{\hbox spread0.0pt{\hskip 0.0pt plus
0.0001fil\hbox{\kern 57.76375pt\hbox{$\displaystyle\penalty
1{{\begin{array}[]{c}q=[{E_{\mathit{hb}}}_{\bot},\ldots,{E_{\mathit{hb}}}_{\bot}]\quad\quad|\,q\,|=v\quad\quad\mathit{fresh}(c)\end{array}}}$}}\hskip
0.0pt plus 0.0001fil}\hbox{\hbox{\kern 0.0pt\vrule
height=0.25002pt,depth=0.25002pt,width=276.44908pt\hbox{\kern
2.70003pt$\mbox{{R-Make}}$}}}\hbox{\kern 0.0pt\hbox{$\displaystyle p\langle
E_{\mathit{hb}},\mathrel{\mathtt{let}}r=\
\mathrel{\mathtt{make}}(\mathrel{\mathtt{chan}}T,v)\mathrel{\mathtt{in}}t\rangle~{}~{}\xrightarrow{}~{}~{}\mathbf{\nu}c\
(p\langle
E_{\mathit{hb}},\mathrel{\mathtt{let}}r=c\mathrel{\mathtt{in}}t\rangle\parallel
c_{f}[]\parallel c_{b}[q])$}}}\par}}\\\ \\\\[-11.00008pt]
{\small{tensy\vbox{\hbox spread0.0pt{\hskip 0.0pt plus 0.0001fil\hbox{\kern
65.76999pt\hbox{$\displaystyle\penalty
1{{\begin{array}[]{c}\lnot\mathit{closed}(c_{f}[q_{2}])\quad\quad
E_{\mathit{hb}}^{\prime}=E_{\mathit{hb}}+E_{\mathit{hb}}^{\prime\prime}\end{array}}}$}}\hskip
0.0pt plus 0.0001fil}\hbox{\hbox{\kern 0.0pt\vrule
height=0.25002pt,depth=0.25002pt,width=266.72298pt\hbox{\kern
2.70003pt$\mbox{{R-Send}}$}}}\hbox{\kern 0.0pt\hbox{$\displaystyle
c_{b}[q_{1}::E_{\mathit{hb}}^{\prime\prime}]\parallel p\langle
E_{\mathit{hb}},c\leftarrow v;t\rangle\parallel
c_{f}[q_{2}]~{}~{}\xrightarrow{}~{}~{}c_{b}[q_{1}]\parallel p\langle
E_{\mathit{hb}}^{\prime},t\rangle\parallel
c_{f}[{\color[rgb]{0.56,0.74,0.56}\definecolor[named]{pgfstrokecolor}{rgb}{0.56,0.74,0.56}(v,E_{\mathit{hb}})}::q_{2}]$}}}\par}}\\\
\\\\[-11.00008pt] {\small{tensy\vbox{\hbox spread0.0pt{\hskip 0.0pt plus
0.0001fil\hbox{\kern 55.59444pt\hbox{$\displaystyle\penalty
1{{\begin{array}[]{c}v\not=\bot\quad\quad
E_{\mathit{hb}}^{\prime}=E_{\mathit{hb}}+E_{\mathit{hb}}^{\prime\prime}\end{array}}}$}}\hskip
0.0pt plus 0.0001fil}\hbox{\hbox{\kern 0.0pt\vrule
height=0.25002pt,depth=0.25002pt,width=216.49182pt\hbox{\kern
2.70003pt$\mbox{{R-Rec}}$}}}\hbox{\kern
0.0pt\hbox{$\displaystyle\begin{array}[]{rcl}c_{b}[q_{1}]\parallel&p\langle
E_{\mathit{hb}},\mathrel{\mathtt{let}}r=\mathop{\leftarrow
c}\mathrel{\mathtt{in}}t\rangle&\parallel
c_{f}[q_{2}::{\color[rgb]{0.56,0.74,0.56}\definecolor[named]{pgfstrokecolor}{rgb}{0.56,0.74,0.56}(v,E_{\mathit{hb}}^{\prime\prime})}]~{}~{}\xrightarrow{}{}{}\\\
c_{b}[E_{\mathit{hb}}::q_{1}]\parallel&p\langle
E_{\mathit{hb}}^{\prime},\mathrel{\mathtt{let}}r=v\mathrel{\mathtt{in}}t\rangle&\parallel
c_{f}[q_{2}]\end{array}$}}}\par}}\\\ \\\\[-11.00008pt]
{\small{tensy\vbox{\hbox spread0.0pt{\hskip 0.0pt plus 0.0001fil\hbox{\kern
99.52374pt\hbox{$\displaystyle\penalty
1{{\begin{array}[]{c}E_{\mathit{hb}}^{\prime}=E_{\mathit{hb}}+E_{\mathit{hb}}^{\prime\prime}\end{array}}}$}}\hskip
0.0pt plus 0.0001fil}\hbox{\hbox{\kern 0.0pt\vrule
height=0.25002pt,depth=0.25002pt,width=260.91496pt\hbox{\kern
2.70003pt$\mbox{{R-Rec${}_{\bot}$}}$}}}\hbox{\kern 0.0pt\hbox{$\displaystyle
p\langle E_{\mathit{hb}},\mathrel{\mathtt{let}}r=\mathop{\leftarrow
c}\mathrel{\mathtt{in}}t\rangle\parallel
c_{f}[{\color[rgb]{0.56,0.74,0.56}\definecolor[named]{pgfstrokecolor}{rgb}{0.56,0.74,0.56}(\bot,E_{\mathit{hb}}^{\prime\prime})}]~{}~{}\xrightarrow{}~{}~{}p\langle
E_{\mathit{hb}}^{\prime},\mathrel{\mathtt{let}}r=\bot\mathrel{\mathtt{in}}t\rangle\parallel
c_{f}[{\color[rgb]{0.56,0.74,0.56}\definecolor[named]{pgfstrokecolor}{rgb}{0.56,0.74,0.56}(\bot,E_{\mathit{hb}}^{\prime\prime})}]$}}}\par}}\\\
\\\\[-11.00008pt] {\small{tensy\vbox{\hbox spread0.0pt{\hskip 0.0pt plus
0.0001fil\hbox{\kern 80.1457pt\hbox{$\displaystyle\penalty
1{{\begin{array}[]{c}E_{\mathit{hb}}^{\prime}={E_{\mathit{hb}}}_{1}+{E_{\mathit{hb}}}_{2}\end{array}}}$}}\hskip
0.0pt plus 0.0001fil}\hbox{\hbox{\kern 0.0pt\vrule
height=0.25002pt,depth=0.25002pt,width=227.1989pt\hbox{\kern
2.70003pt$\mbox{{R-Rend}}$}}}\hbox{\kern
0.0pt\hbox{$\displaystyle\begin{array}[]{rcll}c_{b}[]\parallel&p_{1}\langle{E_{\mathit{hb}}}_{1},c\leftarrow
v;t\rangle&\parallel
p_{2}\langle{E_{\mathit{hb}}}_{2},\mathrel{\mathtt{let}}r=\mathop{\leftarrow
c}\mathrel{\mathtt{in}}t_{2}\rangle&\parallel
c_{f}[]~{}~{}\xrightarrow{}{}{}\\\ c_{b}[]\parallel&p_{1}\langle
E_{\mathit{hb}}^{\prime},t\rangle&\parallel p_{2}\langle
E_{\mathit{hb}}^{\prime},\mathrel{\mathtt{let}}r=v\mathrel{\mathtt{in}}t_{2}\rangle&\parallel
c_{f}[]\end{array}$}}}\par}}\\\ \\\\[-11.00008pt] \end{array}$

Figure 4: Operational semantics augmented for race detection: channel
communication

As in Fava et al.,  [10], “the R-Close rule closes both sync and async
channels. Executing a receive on a _closed_ channel results in receiving the
end-of-transmission marker $\bot$ (cf. rule R-Rec⊥) and updating the local
state $E_{\mathit{hb}}$ in the same way as when receiving a properly sent
value. The “value” $\bot$ is not removed from the queue, so that all clients
attempting to receive from the closed channel obtain the communicated happens-
before synchronization information.”

Finally, goroutine creation is a synchronizing operation where the child, who
is given a unique identifier $p^{\prime}$, inherits the happens-before set
from the parent—see the R-Go rule in Figure 5.

$\begin{array}[b]{l}\end{array}$

Figure 5: Operational semantics augmented for race detection: thread creation

###  3.4 Detecting write-after-read (WaR) races

In the previous section, the detection of read-after-write and write-after-
write races required happens-before sets to contain write labels only. The
detection of write-after-read races requires recording read labels, as well. A
successful read of variable $z$ causes a fresh read label, say $m^{\prime}$,
to be generated. The pair
${\color[rgb]{0.2,0.2,0.7}\definecolor[named]{pgfstrokecolor}{rgb}{0.2,0.2,0.7}(m^{\prime},?z)}$
is added to the reader’s happens-before set as well as to the record
associated with $z$ in memory—see rule R-Read of Figure 6.

$\begin{array}[b]{l}{\small{tensy\vbox{\hbox spread0.0pt{\hskip 0.0pt plus
0.0001fil\hbox{$\displaystyle\penalty
1{{\begin{array}[]{c}E_{\mathit{hb}}^{z}\subseteq
E_{\mathit{hb}}\quad\quad\mathit{fresh}(m^{\prime})\quad\quad
E_{\mathit{hb}}^{\prime}=\\{{\color[rgb]{0.7,0.2,0.2}\definecolor[named]{pgfstrokecolor}{rgb}{0.7,0.2,0.2}{(m^{\prime},!z)}}\\}\cup
E_{\mathit{hb}}\quad\quad E_{\mathit{hb}}^{\prime
z}=\\{{\color[rgb]{0.7,0.2,0.2}\definecolor[named]{pgfstrokecolor}{rgb}{0.7,0.2,0.2}{(m^{\prime},!z)}}\\}\cup
E_{\mathit{hb}}^{z}\end{array}}}$}\hskip 0.0pt plus
0.0001fil}\hbox{\hbox{\kern 0.0pt\vrule
height=0.25002pt,depth=0.25002pt,width=282.58698pt\hbox{\kern
2.70003pt$\mbox{{R-Write}}$}}}\hbox{\kern 35.20657pt\hbox{$\displaystyle
p\langle
E_{\mathit{hb}},z:=v^{\prime};t\rangle\parallel(\\!\\!|E_{\mathit{hb}}^{z},\,z{:=}v|\\!\\!)\xrightarrow{}p\langle
E_{\mathit{hb}}^{\prime},t\rangle\parallel(\\!\\!|E_{\mathit{hb}}^{\prime
z},\,z{:=}v^{\prime}|\\!\\!)$}}}\vspace{6pt}\par}}\\\ \\\\[-11.00008pt]
\end{array}{\\\ }{\\\\[-11.00008pt] }$

Figure 6: Operational semantics augmented for data-race detection

$\begin{array}[b]{l}{\small{tensy\vbox{\hbox spread0.0pt{\hskip 0.0pt plus
0.0001fil\hbox{\kern 30.23512pt\hbox{$\displaystyle\penalty
1{{\begin{array}[]{c}E_{\mathit{hb}}^{z}\not\subseteq
E_{\mathit{hb}}\quad\quad E_{\mathit{hb}}^{z}\downarrow_{?}\subseteq
E_{\mathit{hb}}\end{array}}}$}}\hskip 0.0pt plus 0.0001fil}\hbox{\hbox{\kern
0.0pt\vrule height=0.25002pt,depth=0.25002pt,width=166.59026pt\hbox{\kern
2.70003pt$\mbox{{R-Write-$\mathsf{E}_{WaW}$}}$}}}\hbox{\kern
0.0pt\hbox{$\displaystyle p\langle
E_{\mathit{hb}},z:=v^{\prime};t\rangle\parallel(\\!\\!|E_{\mathit{hb}}^{z},\,z{:=}v|\\!\\!)\xrightarrow{}\mathsf{E}\left({E_{\mathit{hb}}^{z}-E_{\mathit{hb}}}\right)$}}}\vspace{2pt}\par}}\\\
\\\\[-11.00008pt] {\small{tensy\vbox{\hbox spread0.0pt{\hskip 0.0pt plus
0.0001fil\hbox{\kern 58.73262pt\hbox{$\displaystyle\penalty
1{{\begin{array}[]{c}E_{\mathit{hb}}^{z}\downarrow_{?}\nsubseteq
E_{\mathit{hb}}\end{array}}}$}}\hskip 0.0pt plus 0.0001fil}\hbox{\hbox{\kern
0.0pt\vrule height=0.25002pt,depth=0.25002pt,width=166.59024pt\hbox{\kern
2.70003pt$\mbox{{R-Write-$\mathsf{E}_{WaR}$}}$}}}\hbox{\kern
0.0pt\hbox{$\displaystyle p\langle
E_{\mathit{hb}},z:=v^{\prime};t\rangle\parallel(\\!\\!|E_{\mathit{hb}}^{z},\,z{:=}v|\\!\\!)\xrightarrow{}\mathsf{E}\left({E_{\mathit{hb}}^{r}-E_{\mathit{hb}}}\right)$}}}\vspace{2pt}}}\\\
\\\\[-11.00008pt] \end{array}{\\\ }{\\\\[-11.00008pt] }$

Figure 7: Exception conditions for WaR data-race detection

In order for a write to memory to be successful, the writing thread must not
only be aware of previous write events to a given shared variable, but must
also account for all accumulated reads to the variable. A write-after-read
data-race is raised when a write is attempted by a thread and the thread is
unaware of some previous reads to $z$. In other words, there exist some read-
label in the happens-before set associated with the variable’s record, say
$r\in E_{\mathit{hb}}^{z}\downarrow_{?}$, that is not in the thread’s happen-
before set, $r\notin E_{\mathit{hb}}$. The projection $\downarrow_{?}$
essentially filters out write events from the happens-before set. Under these
circumstances, the precondition $E_{\mathit{hb}}^{z}\downarrow_{?}\nsubseteq
E_{\mathit{hb}}$ of the R-Write-$\mathsf{E}_{WaR}$ rule is met and a race is
reported.

Compared to the detector of Section 3.3, the reporting of WaW races in rule
R-Write-$\mathsf{E}_{WaW}$ is augmented with the precondition
$E_{\mathit{hb}}^{z}\downarrow_{?}\subseteq E_{\mathit{hb}}$. Without this
precondition, there would be non-determinism when reporting WaW and WaR
conflicts.999Consider the scenario in which $p$ writes to and then reads from
the shared variable $z$. Say the write to $z$ generates a label $w$ and the
read generates $r$. If a thread $p^{\prime}$ attempts to write to $z$ without
first communicating with $p$, $p^{\prime}$ will not be aware of the prior read
and write events. In other words, the happens-before set of $p^{\prime}$ will
contain neither
${\color[rgb]{0.7,0.2,0.2}\definecolor[named]{pgfstrokecolor}{rgb}{0.7,0.2,0.2}{(w,!z)}}$
nor
${\color[rgb]{0.2,0.2,0.7}\definecolor[named]{pgfstrokecolor}{rgb}{0.2,0.2,0.7}(r,?z)}$.
Both rules R-Write-$\mathsf{E}_{WaW}$ and R-Write-$\mathsf{E}_{WaR}$ are
enabled in this case. However, the read happens-after the write that generated
${\color[rgb]{0.7,0.2,0.2}\definecolor[named]{pgfstrokecolor}{rgb}{0.7,0.2,0.2}{(w,!z)}}$.
Note, however, that when both WaW and WaR apply, the read in the WaR race
happens-after the write involved in the WaW race. We favor to resolve this
non-determinism and to report the most recent conflict.

The detector presented here can flag all conflicts: read-after-write, write-
after-write, and write-after-read. In Section 4 we also make the detector
efficient by “garbage collecting” stale information. But before then, let us
look at a couple of examples that illustrate the detector’s operation.

###  3.5 Examples

We will look at two examples of properly synchronized programs. The first is a
typical usage of channel communication; one in which an action is placed in
the past of another. The second example relies on mutual exclusion instead. In
this case, we know that actions are not concurrent, but we cannot infer an
order between them. By contrasting the two examples in Section 3.5.3, we
derive observations related to determinism and constructivism.

####  3.5.1 Message passing

Message passing, depicted in Figure 8, involves a producer writing to a shared
variable and notifying another thread by sending a message onto a channel. A
consumer receives from the channel and reads from the shared variable.

$\displaystyle p_{1}\langle{E_{\mathit{hb}}}_{1},z:=42;\ c\leftarrow 0\rangle$
$\displaystyle p_{2}\langle{E_{\mathit{hb}}}_{2},\mathop{\leftarrow c};\
\mathrel{\mathtt{load}}z\rangle$ Figure 8: Message passing example.

The access to the shared variable is properly synchronized. Given the
operational semantics presented in this chapter, we can arrive at this
conclusion as follows. A fresh label, say $m$, is generated when $p_{1}$
writes to $z$. The memory record involving $z$ is updated with this fresh
label, and the pair
${\color[rgb]{0.7,0.2,0.2}\definecolor[named]{pgfstrokecolor}{rgb}{0.7,0.2,0.2}{(m,!z)}}$
is placed into $p_{1}$’s happens-before set, thus yielding
${E_{\mathit{hb}}}_{1}^{\prime}$. A send onto $c$ sends not only the message
value, $0$ in this case, but also the happens-before set of the sender,
${E_{\mathit{hb}}}_{1}^{\prime}$, see rule R-Send. The act of receiving from
$c$ blocks until a message is available. When a message becomes available, the
receiving thread receives not only a value but also the happens-before set of
the sender at the time that the send took place, see rule R-Rec. Thus, upon
receiving from $c$, $p_{2}$’s happens-before set is updated to contain
${\color[rgb]{0.7,0.2,0.2}\definecolor[named]{pgfstrokecolor}{rgb}{0.7,0.2,0.2}{(m,!z)}}$.
Receiving from the channel places the writing to $z$ by $p_{1}$ into $p_{2}$’s
definite past. The race-checker makes sure of this fact by inspecting
$p_{2}$’s happens-before set when $p_{2}$ attempts to load from $z$. In other
words, the race-checker checks that the current labels associated with $z$ in
the configuration are also present in the happens-before set of the thread
performing the load.

The message passing example illustrates synchronization as imposing of an
order between events belonging to different threads. The message places the
producer’s write in the past of the consumer’s read. Next, we will look into
an example in which synchronization is achieve via mutual exclusion. Two
threads, $p_{1}$ and $p_{2}$, are competing to write to the same variable. We
will not be able to determine which write happens-before the other. Even
though we cannot infer the order, we can determine that a happens-before order
exists and, therefore, that the program is properly synchronized.

####  3.5.2 Mutual exclusion

Figure 9 shows a typical mutual exclusion scenario. It involves two threads
writing to a shared variable $z$. Before writing, a thread sends a message
onto a channel $c$ which capacity $|\,{c}\,|=1$. After writing, it receives
from $c$.101010Note that the channel is being used as a semaphore [8]. Sending
on the channel is analogous to a semaphore wait or P operation. Receive is
analogous to signal or V. The wait decrements the value of the semaphore and,
if the new value is negative, the process executing the wait is blocked. A
signal increments the value of the semaphore variable, thus allowing another
process (potentially coming from the pool of previously blocked processes) to
resume. Similarly, a send operation decrements the number of available slots
in the channel’s queue, while a receive increments it. Sending on a channel
with capacity 1 can only take place if the channel is empty; meaning, all
previous sends are matched with a corresponding receive.

$\displaystyle p_{1}\langle c\leftarrow 0;\ z:=17;\ \mathop{\leftarrow
c}\rangle$ $\displaystyle p_{2}\langle c\leftarrow 0;\ z:=42;\
\mathop{\leftarrow c}\rangle$ Figure 9: Mutual exclusion example.

A send and its corresponding receive do not directly contribute to
synchronization in this example. The send is matched by a receive from the
same thread; nothing new is learned from this exchange. To illustrate this
point, which may come as a surprise, let us look at an execution. Say $p_{1}$
is the first to send $0$ onto $c$. Then $p_{1}$’s happens-before set
${E_{\mathit{hb}}}_{1}$ is placed onto the channel along with the value of
$0$. The thread then proceeds to write to $z$, which generates a fresh label,
say $m^{\prime}$; the pair
${\color[rgb]{0.7,0.2,0.2}\definecolor[named]{pgfstrokecolor}{rgb}{0.7,0.2,0.2}{(m^{\prime},!z)}}$
is placed on $p_{1}$’s happens-before set. When receiving from $c$, $p_{1}$
does not learn anything new! It receives the message $0$ and a “stale”
happens-before set ${E_{\mathit{hb}}}_{1}$. The receiver’s happens-before set,
${E_{\mathit{hb}}}_{1}^{\prime}$, is updated to incorporate the stale happens-
before set, but this “update” causes no effective change:

$\displaystyle{E_{\mathit{hb}}}_{1}^{\prime}\cup{E_{\mathit{hb}}}_{1}$
$\displaystyle=({E_{\mathit{hb}}}_{1}\cup\\{{\color[rgb]{0.7,0.2,0.2}\definecolor[named]{pgfstrokecolor}{rgb}{0.7,0.2,0.2}{(m^{\prime},!z)}}\\})\cup{E_{\mathit{hb}}}_{1}$
$\displaystyle={E_{\mathit{hb}}}_{1}\cup\\{{\color[rgb]{0.7,0.2,0.2}\definecolor[named]{pgfstrokecolor}{rgb}{0.7,0.2,0.2}{(m^{\prime},!z)}}\\}$
$\displaystyle={E_{\mathit{hb}}}_{1}^{\prime}$

The explanation for why the program is synchronized, in this case, is more
subtle. It involves reasoning about the channel’s capacity. Recall that,
according to rule (2) on page 2, the $i^{\mathit{th}}$ receive from a channel
with capacity $k$ happens before the $(i+k)^{\mathit{th}}$ send onto the
channel completes. Since channel capacity is $1$ in our example, rule (2)
implies that the first receive from the channel happens-before the second send
completes. If $p_{1}$ is the first to write to $z$, then $p_{1}$ is also the
first to receive from $c$. Receiving from $c$ places $p_{1}$’s happens-before
set onto the backward channel (see rule R-Rec). This happens-before set
contains the entry
${\color[rgb]{0.7,0.2,0.2}\definecolor[named]{pgfstrokecolor}{rgb}{0.7,0.2,0.2}{(m^{\prime},!z)}}$
registering $p_{1}$’s write to $z$. Upon _sending_ onto $c$, $p_{2}$ receives
from the backward channel and learns of $p_{1}$’s previous write. Thus, by the
time $p_{2}$ writes to $z$, the write by $p_{1}$ has been-placed onto
$p_{2}$’s definite past. Since no concurrent accesses exist, the race checker
does not flag this execution as racy.

Similarly, $p_{2}$ could first send onto $c$ and write to $z$. The argument
for the proper synchronization of this alternate run would proceed in the same
way. Therefore, even though it is not possible to infer who, among $p_{1}$ and
$p_{2}$, writes to $z$ first, we know that one of the writes is in a happens-
before relation with the other. This knowledge is enough for us to conclude
that the program is properly synchronized.

This example shows that channels are excessively powerful when it comes to
implementing mutual exclusion, as evidenced by the fact that the forward queue
associated with the channel is not utilized. When it comes to mutual
exclusion, a more parsimonious synchronization mechanism suffices. Indeed, the
_acquire_ and _release_ semantics associated with locks is a perfect fit. When
acquiring a lock, a thread learns about the memory operations that precede the
lock’s release. In other words, memory operations preceding a lock’s release
are put in happens-before with respect to a thread that acquires the lock.
Assuming a lock $l$ starts with empty happens-before information, say
$l[\emptyset]$, the rules Acquire and Release capture a lock’s behavior.

$\begin{array}[b]{l}{\small{tensy\vbox{\hbox spread0.0pt{\hskip 0.0pt plus
0.0001fil\hbox{\kern 43.46857pt\hbox{$\displaystyle\penalty
1{{\begin{array}[]{c}E_{\mathit{hb}}^{\prime}=E_{\mathit{hb}}\cup
E_{\mathit{hb}}^{\prime\prime}\end{array}}}$}}\hskip 0.0pt plus
0.0001fil}\hbox{\hbox{\kern 0.0pt\vrule
height=0.25002pt,depth=0.25002pt,width=147.80461pt\hbox{\kern
2.70003pt$\mbox{{Acquire}}$}}}\hbox{\kern 0.0pt\hbox{$\displaystyle p\langle
E_{\mathit{hb}},\mathrel{\mathtt{acq}}(l);t\rangle\parallel
l[E_{\mathit{hb}}^{\prime\prime}]~{}~{}\xrightarrow{}~{}~{}p\langle
E_{\mathit{hb}}^{\prime},t\rangle\parallel l[]$}}}\par}}\\\ \\\\[-11.00008pt]
{\small{tensy\vbox{\hbox spread0.0pt{\hskip 0.0pt plus 0.0001fil\hbox{\kern
41.85606pt\hbox{$\displaystyle\penalty
1{{\begin{array}[]{c}E_{\mathit{hb}}^{\prime}=E_{\mathit{hb}}\cup
E_{\mathit{hb}}^{\prime\prime}\end{array}}}$}}\hskip 0.0pt plus
0.0001fil}\hbox{\hbox{\kern 0.0pt\vrule
height=0.25002pt,depth=0.25002pt,width=144.5796pt\hbox{\kern
2.70003pt$\mbox{{Release}}$}}}\hbox{\kern 0.0pt\hbox{$\displaystyle p\langle
E_{\mathit{hb}},\mathrel{\mathtt{rel}}(l);t\rangle\parallel
l[]~{}~{}\xrightarrow{}~{}~{}p\langle E_{\mathit{hb}},t\rangle\parallel
l[E_{\mathit{hb}}^{\prime}]$}}}}}\end{array}$

Note that an acquired lock, represented by $l[]$, cannot be re-acquired
without a prior release, and that a released lock, meaning
$l[E_{\mathit{hb}}]$, cannot re-released without a prior acquire.111111When
releases are matched by an prior acquire from the same thread, then happens-
before information accumulates monotonically, meaning, a thread learns about
all previous releases, not just the most recently occurring one. While a
thread’s happens-before is updated on both sends and receives, with locks,
only the acquisition updates a thread’s happens-before information.
Surrounding code with a call to acquire at the beginning and release at the
end is sufficient for ensuring mutual exclusion. The full generality of
channels is not required.

####  3.5.3 Determinism, confluence, and synchronization

In the message passing example of Section 3.5.1, we are able to give a
constructive proof-sketch of the synchronization between $p_{1}$ and $p_{2}$;
the “proof” puts an event from $p_{1}$ in the past of $p_{2}$. In the mutual
exclusion example of Section 3.5.2, no such guarantee is possible. Instead, we
give a non-constructive “proof” that $p_{1}$ and $p_{2}$ are synchronized by
arguing that either $p_{1}$’s actions are in the past of $p_{2}$’s or vice
versa. The _law of excluded middle_ is used in this non-constructive argument.

The absence of constructivism is tied to the absence of determinism. While in
the message passing example the program is deterministic, in the mutual
exclusion example it is not. There is no _data_ race in the mutual exclusion
example, but there is still a “race” insofar as the two threads compete for
access to a shared resource. The resource, in this case, is the channel, which
is being used as a lock. The two threads race towards acquiring the lock (i.e.
sending onto the channel) first. The initial configuration has two
transitions, one in which $p_{1}$ acquires the lock first and one in which
$p_{2}$ does. These transitions are non-confluent.

When it comes to reasoning about programs that model hardware, the lack of
constructivism and the non-confluence in the use of channels as locks is a
hindrance. Deterministic languages and constructive logics are needed in order
to rule out scenarios in which two logic gates attempt to drive the same _via_
with different logic values (i.e. a short circuit) [2]. In the case of channel
communication and in the absence of shared memory, determinism can be achieved
by enforcing ownership on channels; for example, by making sure a single
thread can read and a single thread can write on a given channel at any given
point in the execution [37]. It is possible for the ownership on channels to
be passed around the threads in a way that preserves determinism [38].

The examples show that the absence of absence of data races is not enough to
ensure determinism. In general, however, determinism is not a requirement.
Many applications require “only” data-race freedom.

##  4 Efficient data-race detection

We have been gradually introducing a data-race checker. In Section 3.3, we
presented a simple checker that flags after-write races (WaW and RaW) but is
not equipped for write-after-read (WaR) detection. In Section 3.4, we
augmented the detector to handle WaR. Here, we discuss how these detectors can
be implemented efficiently; where efficiency is gained by employing “garbage
collection” to reduce the detector’s memory footprint. Note that keeping one
record per variable is already a form of efficiency gain. In a relaxed memory
model, since there may be more than one value associated with a variable at
any point in the execution, one might keep one record per memory event [10].
The first step towards a smaller footprint is to realize that, if the
underlying memory model supports the DRF-SC guarantee, a data-race detector
can be built assuming sequential consistency. The reason being that, when a
data race is flagged, execution stops at the point in which the weak and
strong memory models’ executions would diverge.

Knowing that memory events can overtake each other, in this section we discuss
how stale or redundant information can be garbage collected. More precisely,
we show how to garbage collect the data structures that hold happens-before
information, that is, the thread-local happens-before set and the per-memory-
location one.

###  4.1 Most recent write

Terms representing a memory location have taken different shapes when compared
to the undecorated semantics. In the undecorated semantics, the content $v$ of
a variable $z$ is written as a pair $(\\!\\!|z{:=}v|\\!\\!)$. For after-write
race detection, an entry in memory took the form of
$(\\!\\!|E_{\mathit{hb}},\,z{:=}v|\\!\\!)$ with $E_{\mathit{hb}}$ holding
information about prior write events. Our first optimization comes from
realizing that we do not need to keep a set of prior write events. We can
record only the most recent write and still be able to flag all after-write
racy _executions._ With this optimization, we may fail to report all
_accesses_ involved in the race, but we will still be able to report the
execution as racy and to flag the most recent conflicting write event. This
optimization is significant; it reduces the arbitrarily large set of prior
write events to a single point.

An intuitive argument for the correctness of the optimization comes from
noticing that a successful write to a variable can be interpreted as the
writing thread taking _ownership_ of the variable. Suppose a goroutine $p$ has
just updated variable $z$. At this point, $p$ is only goroutine whose happens-
before set contains the label, say $m$, associated with this write-record. The
placement of the new label into $p$’s happens-before set can be seen as
recording $p$’s _ownership_ of the variable: a data-race is flagged if any
other thread attempts to read or write to $z$ without first synchronizing with
$p$—see the check
${\color[rgb]{0.7,0.2,0.2}\definecolor[named]{pgfstrokecolor}{rgb}{0.7,0.2,0.2}{(m,!z)}}\in
E_{\mathit{hb}}$ in the premise of the R-Write and R-Read rules of Figure 10.

When $p$ sends a message onto a channel, the information about $m$ is also
sent. Suppose now that a thread $p^{\prime}$ reads from the channel and
receives the corresponding message before $p$ makes any further modifications
to $z$. The tuple
${\color[rgb]{0.7,0.2,0.2}\definecolor[named]{pgfstrokecolor}{rgb}{0.7,0.2,0.2}{(m,!z)}}$
containing the write-record’s label is added to $p^{\prime}$’s happens-before
set. Now both $p$ and $p^{\prime}$ are aware of $z$’s most recent write to
$z$. The existence of $m$ in both goroutine’s happens-before sets imply that
either $p$ or $p^{\prime}$ are allowed to update $z$’s value. We can think of
the two goroutines as _sharing_ $z$. Among $p$ and $p^{\prime}$, whoever
updates $z$ first (re)gains the _exclusive_ rights to $z$.

It may be worth making a parallel with hardware and cache coherence protocols.
Given the derivation rules, we can write a race detector as a state machine.
Compared to the Modified-Exclusive-Shared-Invalid protocol (MESI), our
semantics does not have the _modified_ state: all changes to a variable are
immediately reflected in the configuration, there is no memory hierarchy in
the memory model. As hinted above, the other states can be interpreted as
follows: If the label of the most recent write to a variable is only recorded
in one goroutine’s happens-before set, then we can think of the goroutine as
having _exclusive_ rights to the variable. When a number of goroutines contain
the pair
${\color[rgb]{0.7,0.2,0.2}\definecolor[named]{pgfstrokecolor}{rgb}{0.7,0.2,0.2}{(m,!z)}}$
in their happen-before set with $m$ being the label of the most recent write,
then these goroutines can be thought to be _sharing_ the variable. Other
goroutines that are unaware of the most recent write can be said to hold
_invalid_ data.

###  4.2 Runtime configuration and memory related reduction rules

Given the “most recent write” optimization above, and, if we were satisfied
with after-write conflicts, an entry in memory would take the form of
$m(\\!\\!|z{:=}v|\\!\\!)$, with the label $m$ uniquely identifying the event
associated with $v$ having been stored into $z$. Being able to flag after-
write but not write-after-read races may be an adequate trade-off between
completeness and efficiency. By not having to record read events, a simplified
detector tailored for after-write race detection has a much smaller footprint
than when read-after-write conflicts are also taken into account. Besides, a
write-after-read race that is not flagged in an execution may realize itself
as a read-after-write race in another run, and then be flagged by the
simplified detector.121212Intuitively, say
$S_{0}\xrightarrow{e_{0}}S_{1}\xrightarrow{e_{1}}\cdots\xrightarrow{e_{n-1}}S_{n}$
is a run starting from an initial configuration $S_{0}$. Let $\bowtie$ be an
independence relation on events, meaning, given
$S_{i}\xrightarrow{e_{i}}S_{i+1}\xrightarrow{e_{i+1}}S_{i+2}$, we say that
$e_{i}\bowtie e_{i+1}$ if there exist $S^{\prime}$ such that
$S_{i}\xrightarrow{e_{i+1}}S^{\prime}\xrightarrow{e_{i}}S_{i+2}$. The
independence relation induces an equivalence relation on traces, namely,
traces are equivalent if they can be derived from one another via the
permutation of independent events. It can be shown that if
$S_{0}\xrightarrow{h}S_{n}$ is a run containing a write-after-read race, the
exist an equivalent run in which the race materializes as a read-after-write
race.

In contrast, the detection of write-after-read races requires more book-
keeping: we need read- in addition to write-labels. This addition is required
because a WaR conflict can ensue between an attempted write and _any_ previous
unsynchronized read to the same variable. Therefore, the race-checker is made
to remember all such potentially troublesome reads.131313Since depending on
scheduling, a WaR data-race can manifest itself as RaW race, one option would
be not add instrumentation for WaR race detection and, instead, hope to flag
the RaW manifestation instead. Such practical consideration illustrates the
trade-off between completeness versus run-time overhead. The runtime
configuration is thus modified, this time as to contain entries of the form
$m(\\!\\!|E_{\mathit{hb}}^{r},\,z{:=}v|\\!\\!)$. The label $m$ identifies of
the most recent write event to $z$ and the set $E_{\mathit{hb}}^{r}$ holds-
read event identifiers, namely, the identifiers of reads that accumulated
after $m$.

$R::=p\langle E_{\mathit{hb}},t\rangle\ \mathrel{|}\
m(\\!\\!|E_{\mathit{hb}}^{r},\,z{:=}v|\\!\\!)\ \mathrel{|}\ \bullet\
\mathrel{|}\ R\parallel R\ \ \mathrel{|}\ c[q]\ \mathrel{|}\ \nu n\ R\ .$ (4)

Note that _records_ of the form
$m(\\!\\!|E_{\mathit{hb}}^{r},\,z{:=}v|\\!\\!)$ can be seen as $n+1$ recorded
events: one write together with $n\geq 0$ read events.

The formal semantics maintains the following invariants. First, the happens-
before information $E_{\mathit{hb}}^{r}$ in
$m(\\!\\!|E_{\mathit{hb}}^{r},\,z{:=}v|\\!\\!)$ contains information of the
form
${\color[rgb]{0.2,0.2,0.7}\definecolor[named]{pgfstrokecolor}{rgb}{0.2,0.2,0.7}(m^{\prime},?z)}$
only, i.e., there are no write events and all read-events concern variable
$z$. Also, the event labels are unique for both reads and writes. In an abuse
of notation, we may refer to $m$ being in $E_{\mathit{hb}}^{r}$ and write
$m\in E_{\mathit{hb}}^{r}$ meaning, more precisely,
${\color[rgb]{0.2,0.2,0.7}\definecolor[named]{pgfstrokecolor}{rgb}{0.2,0.2,0.7}(m,?z)}\in
E_{\mathit{hb}}^{r}$.

$\begin{array}[b]{l}{\small{tensy\vbox{\hbox spread0.0pt{\hskip 0.0pt plus
0.0001fil\hbox{$\displaystyle\penalty
1{{\begin{array}[]{c}{\color[rgb]{0.7,0.2,0.2}\definecolor[named]{pgfstrokecolor}{rgb}{0.7,0.2,0.2}{(m,!z)}}\in
E_{\mathit{hb}}\quad\quad E_{\mathit{hb}}^{r}\subseteq
E_{\mathit{hb}}\quad\quad\mathit{fresh}(m^{\prime})\quad\quad
E_{\mathit{hb}}^{\prime}=\\{{\color[rgb]{0.7,0.2,0.2}\definecolor[named]{pgfstrokecolor}{rgb}{0.7,0.2,0.2}{(m^{\prime},!z)}}\\}\cup\left(E_{\mathit{hb}}-E_{\mathit{hb}}\downarrow_{z}\right)\end{array}}}$}\hskip
0.0pt plus 0.0001fil}\hbox{\hbox{\kern 0.0pt\vrule
height=0.25002pt,depth=0.25002pt,width=283.26646pt\hbox{\kern
2.70003pt$\mbox{{R-Write}}$}}}\hbox{\kern 31.01244pt\hbox{$\displaystyle
p\langle E_{\mathit{hb}},z:=v^{\prime};t\rangle\parallel
m(\\!\\!|E_{\mathit{hb}}^{r},\,z{:=}v|\\!\\!)\xrightarrow{}p\langle
E_{\mathit{hb}}^{\prime},t\rangle\parallel
m^{\prime}(\\!\\!|\emptyset,\,z{:=}v^{\prime}|\\!\\!)$}}}\vspace{10pt}\par}}\\\
\\\\[-11.00008pt] \end{array}{\\\ }{\\\\[-11.00008pt] }$

Figure 10: Operational semantics augmented for efficient data-race detection

###  4.3 Garbage collection of happens-before sets

Knowledge of past events contained in a happens-before set $E_{\mathit{hb}}$
is naturally monotonically increasing. For example, each time a goroutine
learns about happens-before information, it adds to its pool of knowledge. In
particular, events that are known to have “happened-before” cannot, by
learning new information, become “concurrent.” An efficient semantics,
however, does not accumulate happens-before information indiscriminately;
instead, it purges redundant information. We say “redundant” for the purpose
of flagging racy executions, but leaving out conflicting accesses that have
been overtaken by more recent memory events.

####  4.3.1 Garbage collection on _writes_

For a thread $t$ to successfully write to $z$, all previously occurring
accesses to $z$ must be in happens-before with the thread’s current state. One
optimization comes from realizing that we can purge all information about
prior accesses the variable $z$ from the happens-before set of the writing
thread $t$. We call these prior accesses _redundant_ from the point of view of
flagging racy executions. The reason for the correctness of this optimization
is as follows: All future access of $t$ to $z$ are synchronized with the
redundant accesses, after all, the accesses are recorded in $t$’s happens-
before set. Therefore, from the perspective of $t$, these accesses do not
affect data-race detection. For the same reason, if a thread $t^{\prime}$
synchronizes with $t$, there is no race to report if and when $t^{\prime}$
accesses memory—the absence of these redundant accesses from $t^{\prime}$’s
happens-before is, therefore, inconsequential. Finally, if $t^{\prime}$ does
not synchronize with $t$, then an access to $z$ is racy because it is
unsynchronized with $t$’s most recent write, regardless of the redundant prior
accesses. Note that this optimization allows us to flag all racy _executions_
even if we fail to report some of the accesses involved in the race.

Rule R-Write of Figure 10 embodies this discussion. Before writing, the rule
checks that the attempted write happens-after all previously occurring
accesses to $z$. This check is done by two premises: premise
${\color[rgb]{0.7,0.2,0.2}\definecolor[named]{pgfstrokecolor}{rgb}{0.7,0.2,0.2}{(m,!z)}}\in
E_{\mathit{hb}}$ makes sure that the most recent write to $z$, namely, the one
that produced event
${\color[rgb]{0.7,0.2,0.2}\definecolor[named]{pgfstrokecolor}{rgb}{0.7,0.2,0.2}{(m,!z)}}$,
is in happens-before with the current thread state $E_{\mathit{hb}}$. As per
discussion in Section 4.1, being synchronized with the most recent write means
the thread is synchronized with all writes up to that point in the execution.
The other premise, $E_{\mathit{hb}}^{r}\subseteq E_{\mathit{hb}}$, makes sure
that the attempted write is in happens-after read accesses to $z$. If these
two premises are satisfied, the write can proceed and prior accesses to $z$
are garbage collected from the point of view of $t$. The filtering of
redundant accesses is done by subtracting $E_{\mathit{hb}}\downarrow_{z}$ in

$E_{\mathit{hb}}^{\prime}=\\{{\color[rgb]{0.7,0.2,0.2}\definecolor[named]{pgfstrokecolor}{rgb}{0.7,0.2,0.2}{(m^{\prime},!z)}}\\}\cup\left(E_{\mathit{hb}}-E_{\mathit{hb}}\downarrow_{z}\right)$

where $\downarrow_{z}$ projects the happens-before set down to operations on
variable $z$. Finally, the write rule also garbage collects the in-memory
record $E_{\mathit{hb}}^{r}$ by setting it to $\emptyset$,141414As per
discussion in Section 4.1, a term representing a memory location
$m(\\!\\!|E_{\mathit{hb}}^{r},\,z{:=}v|\\!\\!)$ records in
$E_{\mathit{hb}}^{r}$ all the reads to $z$ that have accumulated after the
write that generated the write label $m$. When a new write $m^{\prime}$ of
value $z:=v^{\prime}$ ensues, we update the memory term to record this new
write and we reset its corresponding $E_{\mathit{hb}}^{r}$ to $\emptyset$.
meaning that no read event have accumulated after the write yet.

####  4.3.2 Garbage collection on _reads_

We also garbage collect on load operations. Say $t$ reads from $z$, thus
generating event
${\color[rgb]{0.2,0.2,0.7}\definecolor[named]{pgfstrokecolor}{rgb}{0.2,0.2,0.7}(m^{\prime},?z)}$.
Let us call _redundant_ the memory accesses to $z$ in $t$’s happens-before set
at the time event
${\color[rgb]{0.2,0.2,0.7}\definecolor[named]{pgfstrokecolor}{rgb}{0.2,0.2,0.7}(m^{\prime},?z)}$
takes place, with the exception of
${\color[rgb]{0.7,0.2,0.2}\definecolor[named]{pgfstrokecolor}{rgb}{0.7,0.2,0.2}{(m,!z)}}$.
A read operation can only conflict with a future write; there are not read-
read conflicts. For a future write to take place, the writing thread will need
to synchronize with a thread that “knows” about the read
$m^{\prime}$.151515“Knowing about the read $m^{\prime}$” is a necessary
condition for a thread to successfully write to $z$, but it is not a
sufficient one. There may exist other reads, say $m^{\prime\prime}$,
$m^{\prime\prime\prime}$, etc that are concurrent with $m^{\prime}$. A thread
needs to synchronize with all such concurrent reads before it can successfully
write to $z$. Any thread that knows of $m^{\prime}$ would also know about the
redundant access to $z$ and know of
${\color[rgb]{0.7,0.2,0.2}\definecolor[named]{pgfstrokecolor}{rgb}{0.7,0.2,0.2}{(m,!z)}}$.
In other words, $m^{\prime}$ and $m$ subsume all happened-before accesses of
$z$ from the perspective of $t$. Therefore, we can garbage collect all such
accesses by filtering them out of the thread’s happen-before set, as in

$E_{\mathit{hb}}^{\prime}=\\{{\color[rgb]{0.2,0.2,0.7}\definecolor[named]{pgfstrokecolor}{rgb}{0.2,0.2,0.7}(m^{\prime},?z)}\\}\cup\left(E_{\mathit{hb}}-E_{\mathit{hb}}\downarrow_{z}\right)\cup\\{{\color[rgb]{0.7,0.2,0.2}\definecolor[named]{pgfstrokecolor}{rgb}{0.7,0.2,0.2}{(m,!z)}}\\}\text{.}$

These redundant accesses are also filtered out of the in-memory happens-before
set:

$E_{\mathit{hb}}^{\prime
r}=\\{{\color[rgb]{0.2,0.2,0.7}\definecolor[named]{pgfstrokecolor}{rgb}{0.2,0.2,0.7}(m^{\prime},?z)}\\}\cup\left(E_{\mathit{hb}}^{r}-E_{\mathit{hb}}\downarrow_{z}\right)\text{.}$

####  4.3.3 Off-line garbage collection and channel communication

The garbage collector rules of Figure 11 can be run non-deterministically
during the execution of a program. Rule R-GC eliminates stale entries from the
happens-before set of a thread. It can be sensible to perform garbage
collection also _after_ a thread interacts with a channel, as happens-before
information communicated via channels are likely to become stale. For example,
suppose a thread, whose happens-before set does not contain stale entries,
sends onto a channel and continues executing. By the time a receive takes
place, the happens-before set transmitted via the channel may have become
stale. Similarly for happens-before transmitted between receives and prior
sends via the backward channel. Alternatively, we may choose an implementation
in which the happens-before of inflight messages are also gargabe collected,
in which case we would process the happens-before sets in a channel’s forward
and backquard queues.

$\begin{array}[b]{l}\end{array}{\\\ }{\\\\[-11.00008pt] }$

Figure 11: Off-line garbage collection

##  5 Comparison with vector-clock based race detection

Vector clocks (VCs) are a mechanism for capturing the happen-before relation
over events emanating from a program’s execution [22]. A _vector clock_
$\mathds{V}$ is a function
$\mathrel{\mathtt{Tid}}\rightarrow\mathrel{\mathtt{Nat}}$ which records a
clock, represented by a natural number, for each thread in the system. “VCs
are partially-ordered ($\sqsubseteq$) in a pointwise manner, with an
associated join operation ($\sqcup$) and minimal element ($\bot_{V}$). In
addition, the helper function $inc_{t}$ increments the $t$-component of a VC”
[11].

$\displaystyle\mathds{V}_{1}\sqsubseteq\mathds{V}_{2}~{}~{}$
$\displaystyle\text{iff}~{}~{}\forall
t.~{}\mathds{V}_{1}(t)\leq\mathds{V}_{2}(t)$
$\displaystyle\mathds{V}_{1}\sqcup\mathds{V}_{2}~{}~{}$
$\displaystyle=~{}~{}\lambda t.~{}max(\mathds{V}_{1}(t),\mathds{V}_{2}(t))$
$\displaystyle\bot_{V}~{}~{}$ $\displaystyle=~{}~{}\lambda t.~{}0$
$\displaystyle inc_{t}(\mathds{V})~{}~{}$ $\displaystyle=~{}~{}\lambda
u.~{}\mathrel{\mathtt{if}}u=t\mathrel{\mathtt{then}}\mathds{V}(u)+1\mathrel{\mathtt{else}}\mathds{V}(u)$

Using vector clocks, Pozniansky and Schuster,  [29] proposed a data-race
detection algorithm referred to as Djit$\overset{+}{\text{.}\hskip 3.00003pt}$
Their algorithm works as follows. Each thread $t$ is associated with a vector
clock $\mathds{C}_{t}$. Entry $\mathds{C}_{t}(t)$ stores the current time at
$t$, while $\mathds{C}_{t}(u)$ for $u\neq t$ keeps track of the time of the
last operation “known” to $t$ as having been performed by thread $u$.

The algorithm also keeps track of memory operations. Each memory location $x$
has two vector clocks, one associated with reads, $\mathds{R}_{x}$, and
another with writes, $\mathds{W}_{x}$. The clock of he last read from variable
$x$ by thread $t$ is recorded in $\mathds{R}_{x}(t)$; similar for
$\mathds{W}_{x}(t)$ and writes to $x$ by $t$. When it comes to reading from
memory, a race is flagged when a thread $t$ attempts to read from $x$ while
being “unaware” of some write to $x$. Precisely, a race is flagged when $t$
attempts to read from $x$ and there exists a write to $x$ by thread $u$,
$\mathds{W}_{x}(u)$, that is not accounted for by $t$, meaning
$\mathds{W}_{x}(u)\geq\mathds{C}_{t}(u)$, or, equivalently,
$\mathds{W}_{x}\not\sqsubseteq\mathds{C}_{t}$. If $t$ succeeds in reading from
$x$, then $\mathds{R}_{x}(t)$ is updated to the value of $\mathds{C}_{t}(t)$.
When it comes to writing to memory, a race is flagged when $t$ attempts to
write to $x$ while being unaware of some read or write to $x$, meaning either
$\mathds{R}_{x}\not\sqsubseteq\mathds{C}_{t}$ or
$\mathds{W}_{x}\not\sqsubseteq\mathds{C}_{t}$. If $t$ succeeds in writing to
$x$, then $\mathds{W}_{x}(t)$ is updated to $\mathds{C}_{t}(t)$.

A thread’s clock is advanced when the thread executes synchronization
operations, which have bearing on the happens-before relation. The algorithm
was proposed in the setting of locks; each lock $m$ is associated with a
vector clock $\mathds{L}_{m}$. When a thread $t$ acquires $m$, then
$\mathds{C}_{t}$ is updated to $\mathds{C}_{t}\sqcup\mathds{L}_{m}$. Acquiring
a lock is analogous to receiving from a channel with buffer size one: the
receiving thread updates its vector clock by incorporating the VC previously
“stored” in the lock. When a thread $t$ releases a lock $m$, the vector clock
$\mathds{L}_{m}$ is updated to $\mathds{C}_{t}$ and thread’s clock is
advanced, meaning $\mathds{C}_{t}:=inc_{t}(\mathds{C}_{t})$. We can think of
lock release as placing a message, namely the vector clock associated with the
releasing thread, into a buffer of size one. Thus, in comparison with the
approach presented in our paper, lock operations are a special case of
buffered channel communication. Our paper deals with channels of arbitrary
size and their capacity limitations.

A significant difference between our approach and Djit+ is that we dispense
with the notion of vector clocks. Vector clocks are a conceptual vehicle to
capturing partial order of events. Instead of relying on VCs, our
formalization is tied directly to the concept of happens-before. Vector clocks
are expensive. VCs require $O(\tau)$ storage space and common operations on
VCs consume $O(\tau)$ time where $\tau$ is the number of entries in the
vector. In the case of race detection, $\tau$ is the number of threads spawn
during the execution of a program. It turns out that not all uses of VCs in
Djit+ are strictly necessary. In fact, Flanagan and Freund,  [11] introduce
the concept of _epoch_ , which consists of a pair ${c}@{t}$ where $c$ is a
clock and $t$ a thread identifier. They then replace $\mathds{W}_{x}$, the
vector clock tracking writes to $x$, with a single epoch. This epoch captures
the clock and thread identity associated with the most recent write to $x$.
Similarly, in our approach, a memory location is associated with the
identifier of only the most-recent write to that location. Any thread who is
“aware” of this identifier is allowed to read from the corresponding variable.

FastTrack also reduces the dependency on vector clocks by replacing
$\mathds{R}_{x}$ with the epoch of the most recent read to $x$. However, since
reads are not totally ordered, FastTrack dynamically switches back to a vector
clock representation when needed. Similar to FastTrack, we record the most
recent (unordered) reads which, in the best case, involves an $O(1)$-memory
footprint and $O(\tau)$ at the worst.

When it comes to per-thread memory consumption, however, our approaches look
very different. While Djit+’s and FastTrack’s worst-case memory consumption
per thread is $O(\tau)$, our is $O(\nu\tau)$ where $\nu$ is the number of
shared variables in a program.161616We believe the worst case is a degenerate
case unlikely to happen: it involves every thread reading from every shared
variable and then exchanging messages as to inform everyone else about their
read events. Vector clocks’ memory efficiency, when compared to happens-before
sets, come from VC’s ability to succinctly capture the per-thread accesses
that take place in between advances of a clock. A thread’s clock is advanced
when the thread releases a lock.171717If channels were used instead of locks,
the advance would take place when a thread sends onto or receives from a
channel. All accesses made by a thread $t$ in a given clock $c$ are captured
by the clock: if another thread $u$ “knows” the value $c$ of $t$’s clock, then
$u$ is in happens-after with _all_ accesses made by $t$—that is, all accesses
up to when $t$’s clock was advanced to $c+1$. In contrast, the happens-before
set representation is much more coarse. We keep track of individual accesses,
as opposed to lumping them together into a clock number. This coarseness
explains the extra factor of $\nu$ in the worst-case analysis of the happens-
before set solution. Although being a disadvantage in the worst case scenario,
it does provide benefits, as we discuss next.

Note that the vector-clocks associated with threads and locks grow
monotonically. By _growing monotonically_ we do not mean that time marches
forward to increasing clock values. Instead, we mean that the number of clocks
in a vector grows without provisions for the removal of entries. This growth
can lead to the accumulation of “stale” information, where by stale we mean
information that is not useful from the point of view of race detection. This
growth stands in contrast to our approach to garbage collection. Stale
information is purged from happens-before sets, which means they can shrink
back to size zero after having grown in size.

Let us look at an example that illustrates this difference in treatment of
stale information. Consider the producer/consumer paradigm, where a thread
produces information to be consumed by other threads. Say $p_{0}$ produces
information by writing to the shared variable $z$. The thread then notifies
consumers, $p_{1}$ and $p_{2}$, by sending a message on channel $c$. The
consumers read from $z$ and signal the fact that they are done consuming by
sending onto channel $d$. The producer $p_{0}$ writes to $z$ again once it has
received the consumers’ messages.

$\begin{array}[]{lccll}\text{Producer}&&&\lx@intercol\hfil\text{Consumers}\hfil\lx@intercol\\\
~{}~{}~{}~{}~{}p_{0}&&&~{}~{}~{}p_{1}&~{}~{}~{}p_{2}\\\ \hline\cr\\\\[-4.0pt]
z:=42;&&&\mathop{\leftarrow c};&\mathop{\leftarrow c};\\\ c\leftarrow 0;\
c\leftarrow 0;&&&\mathrel{\mathtt{load}}z;&\mathrel{\mathtt{load}}z;\\\
\mathop{\leftarrow d};\ \mathop{\leftarrow d};&&&d\leftarrow 0&d\leftarrow
0\\\ z:=43&&&&\end{array}$

Let us run this example against a prototype implementation [9] of our proposed
race detector, called Grace, and against FastTrack. Consider the point in the
execution after $p_{0}$ has written to $z$, the consumers have read from $z$
and notified $p_{0}$, and $p_{0}$ is about to write to $z$ again. Below is the
state of the detectors at this point. The information contained in the
happens-before sets and the vector-clocks is very similar. There are three
entries for $p_{0}$, and two entries for $p_{1}$ and $p_{2}$ each.

Happens-before sets |  | Vector-clocks
---|---|---
$E_{\mathit{hb}}^{p_{0}}=\\{{\color[rgb]{0.7,0.2,0.2}\definecolor[named]{pgfstrokecolor}{rgb}{0.7,0.2,0.2}{(m_{0},!z)}},{\color[rgb]{0.2,0.2,0.7}\definecolor[named]{pgfstrokecolor}{rgb}{0.2,0.2,0.7}(m_{1},?z)},{\color[rgb]{0.2,0.2,0.7}\definecolor[named]{pgfstrokecolor}{rgb}{0.2,0.2,0.7}(m_{2},?z)}\\}$ |  | $\mathds{C}_{p_{0}}=\bot[p_{0}\mapsto 6,p_{1}\mapsto 1,p_{2}\mapsto 1]$
$E_{\mathit{hb}}^{p_{1}}=\\{{\color[rgb]{0.7,0.2,0.2}\definecolor[named]{pgfstrokecolor}{rgb}{0.7,0.2,0.2}{(m_{0},!z)}},{\color[rgb]{0.2,0.2,0.7}\definecolor[named]{pgfstrokecolor}{rgb}{0.2,0.2,0.7}(m_{1},?z)}\\}$ |  | $\mathds{C}_{p_{1}}=\bot[p_{0}\mapsto 2,p_{1}\mapsto 2]$
$E_{\mathit{hb}}^{p_{2}}=\\{{\color[rgb]{0.7,0.2,0.2}\definecolor[named]{pgfstrokecolor}{rgb}{0.7,0.2,0.2}{(m_{0},!z)}},{\color[rgb]{0.2,0.2,0.7}\definecolor[named]{pgfstrokecolor}{rgb}{0.2,0.2,0.7}(m_{2},?z)}\\}$ |  | $\mathds{C}_{p_{2}}=\bot[p_{0}\mapsto 3,p_{2}\mapsto 2]$

The happens-before set $E_{\mathit{hb}}^{p_{0}}$ show the reads by $p_{1}$ and
$p_{2}$ as being in happens-before with respect to $p_{0}$, along with
$p_{0}$’s own write to $z$. It also shows $p_{1}$ and $p_{2}$ as being “aware”
of $p_{0}$’s write to $z$, as well as being “aware” of their own reads to $z$.
The same information is captured by the vector clocks. Recall that the bottom
clock, $\bot$, maps every process-id to the clock value of $0$. Thus, the VC
associated with $p_{0}$ contains $p_{0}$’s clock (which happens to be 6) as
well as the clock associated with the reads to $z$ by $p_{1}$ and $p_{2}$. In
this execution, $p_{0}$’s clock was $2$ when the thread wrote to $z$. Thus,
the entry $p_{0}\mapsto 2$ in $\mathds{C}_{p_{1}}$ and the entry $p_{0}\mapsto
3$ in $\mathds{C}_{p_{2}}$ place the write to $z$ by $p_{0}$ in $p_{1}$’s and
$p_{2}$’s past.

The difference between our approach the VC based approach is evidenced in the
next step of execution, when $p_{0}$ writes to $z$ for the second time. This
write subsumes all previous memory interactions on $z$. In other words, this
write is in happens-after with respect to all reads and writes to $z$ up to
this point in the execution of the program. Therefore, it is sufficient for a
thread to synchronize with $p_{0}$ before issuing a new read or write to $z$;
also, it is no longer necessary to remember the original write to $z$ and the
reads from $z$ by $p_{1}$ and $p_{2}$. Here are the happens-before sets and
vector-clocks in the next step of execution, meaning, after $p_{0}$ writes to
$z$ the second time:

Happens-before sets |  | Vector-clocks
---|---|---
$E_{\mathit{hb}}^{p_{0}}=\\{{\color[rgb]{0.7,0.2,0.2}\definecolor[named]{pgfstrokecolor}{rgb}{0.7,0.2,0.2}{(m_{3},!z)}}\\}\phantom{,{\color[rgb]{0.2,0.2,0.7}\definecolor[named]{pgfstrokecolor}{rgb}{0.2,0.2,0.7}(m_{1},?z)},{\color[rgb]{0.2,0.2,0.7}\definecolor[named]{pgfstrokecolor}{rgb}{0.2,0.2,0.7}(m_{2},?z)}}$ |  | $\mathds{C}_{p_{0}}=\bot[p_{0}\mapsto 6,p_{1}\mapsto 1,p_{2}\mapsto 1]$
$E_{\mathit{hb}}^{p_{1}}=\\{\\}$ |  | $\mathds{C}_{p_{1}}=\bot[p_{0}\mapsto 2,p_{1}\mapsto 2]$
$E_{\mathit{hb}}^{p_{0}}=\\{\\}$ |  | $\mathds{C}_{p_{2}}=\bot[p_{0}\mapsto 3,p_{2}\mapsto 2]$

The happens-before sets are mostly empty; the only entry corresponds to the
most recent write to $z$, which is known to $p_{0}$. Meanwhile, the vector
clocks are unchanged. Note, however, that every entry with the exception of
$p_{0}\mapsto 6$ in $\mathds{C}_{p_{0}}$ is stale. In other words, with the
exception of $p_{0}\mapsto 6$, the presence or absence of all other entries
does not alter a thread’s behavior. To illustrate this point, take entry
$p_{0}\mapsto 2$ in $\mathds{C}_{p_{1}}$ as an example: if $p_{1}$ were to
attempt to access $z$, a data race will ensue regardless of whether or not the
entry $p_{0}\mapsto 2$ is in $p_{1}$’s vector clock. Therefore, ideally, we
would want these stale entries purged from the vector-clocks of $p_{0}$,
$p_{1}$, and $p_{2}$. Concretely, we would want
$\mathds{C}_{p_{0}}=\bot[p_{0}\mapsto 6]$ and
$\mathds{C}_{p_{1}}=\mathds{C}_{p_{2}}=\bot$.

Similar unbounded growth occurs in the VCs associated with locks,181818The
_acquire_ grows the VC associated with the acquiring thread; the _release_
sets the VC of the corresponding lock to the VC of the acquiring thread. thus
also leading to the accumulation of stale information. We conjecture that an
approach that purges stale information from VCs, similar to our notion of
garbage collection, would be highly be beneficial. VC-based implementations
are very efficient in managing the memory overhead associated with variables.
For example TSan, a popular race-detection library based on vector clocks and
that comes with the Go tool chain, stores one write and a small number of
reads per memory location (the number of reads stored is 4 in the current
implementation) [15]. Capping the number of tracked read events leads to false
negatives; the cap a fair compromise between _recall_ and memory consumption.
In order to further reduce the memory foot-print of modern race detection
implementations, we are thus left with devising approaches to managing
threads’ and locks’ memory overhead.

Unfortunately, reducing memory pressure on vector-clocks associated with
threads and locks is arguably more difficult than reducing memory pressure on
VCs associated with shared variables. In one hand, if a variable does not
“remember” a read or write to itself as having happened-before, then the
variable becomes more permissive from the point of view of race detection;
meaning, more threads would be able to interact with this variable without
raising a data-race, even when races should have been reported. On the other
hand, if a _thread_ “forgets” about some prior read or write access that have
taken place on a variable, a spurious data race may be raised. Thus, while
dropping clock entries in the VCs associated with variables can introduce
false negatives, dropping clock entries from VCs associated with threads and
locks introduce false positives. From a practical perspective, false negatives
are acceptable and can even be mitigated,191919Provided we run a program
enough times, we can randomly evict entries from a VC or happens-before set
associated with a variable such that we eventually flag all existing races of
the program. however, being warned of non-existing races is overwhelming to
the application programmer, which means false positives are generally not
tolerated.

##  6 Connections with trace theory

Our operational semantics mimics the Go memory model in defining
synchronization in terms of channel communication. Specifically, we abide by
rules (1) and (2), which establish a happens-before relation between a send
and the completion of its corresponding receive, and, due to the boundedness
of channels, between a receive and the completion of a future send. However,
these are not the only imposition by the semantics on the order of events.
Channels act as FIFO queues in both Go [4] as well as in our operational
semantics. However, neither Go nor our operational semantics establish a
happens-before relation between consecutive sends or consecutive receives. For
example, the $i^{\mathit{th}}$ send on a channel $c$ does not happens-before
the $(i+1)^{\mathit{th}}$ send on $c$. Therefore, there exist events that are
necessarily ordered, but that are not in happens-before relation.

It is tempting to think of happens-before in terms of observations, where $a$
and $b$ are in happens-before if and only if we observe $a$ followed by $b$,
and never the other way around. This intuition is captured by the following
tentative definition:

Let $\mathrel{\mathtt{idx}}({a},{h})$ be the index of event $a$ in a run $h$.
Given the set of runs $H$ starting from an initial configuration, we say that
event $a$ _happens-before_ $b$ if-and-only-if, for all runs $h\in H$ such that
$a,b\in h$, $\mathrel{\mathtt{idx}}({a},{h})<\mathrel{\mathtt{idx}}({b},{h})$.

When it comes to weak memory systems, there exist events that are ordered
according to the above tentative definition but that are not in happens-before
relation. Take the improperly synchronized message-passing example of Figure
12 as an example. In this example, a thread $p_{0}$ writes to a shared
variable `z` and sets a flag; another thread, $p_{1}$, checks the flag reads
from `z` if the flag has been set.

$p_{0}$ | $p_{1}$
---|---
z := 42; | $(A)$ | r = load done; | $(C)$
done := true; | $(B)$ | if r then |
|  |  load z | $(D)$
Figure 12: Message passing example.

If $A$ and $B$ are the first and second instructions in thread $p_{0}$, and
$C$ and $D$ are the loads of the flag and of the shared variable $z$ in
$p_{1}$, then program order gives rise to $A\rightarrow_{\mathsf{hb}}B$ and
$C\rightarrow_{\mathsf{hb}}D$. We also have that the load of $z$ in $D$ only
occurs if the value of the flag observed by thread $p_{1}$ is `true`, which
means it was previously set by thread $p_{0}$ in $B$. Therefore, in all runs
in which $D$ is observed, $B$ necessarily occurs earlier in the execution.
This necessity does not, however, place $B$ and $D$ in happens-before
relation. Under many flavors of weak memory, the memory accesses between the
two threads are not synchronized. As the example shows, our tentative
definition of happens-before as always-occurring-before or necessarily-
occurring-before does not work for weak memory systems. How about for
sequential consistent ones?

In the program of Figure 13, thread $p_{0}$ sends values $0$ and $1$ into
channel $c$ consecutively. Concurrently, thread $p_{1}$ writes $42$ to a
shared variable $z$ and receives from the channel, while thread $p_{2}$ first
receives from the channel and conditionally reads from $z$. From this program,
we construct an example in which events are necessarily ordered but are not in
happens-before—even if we assume sequential consistency.

$\displaystyle p_{0}\langle c\leftarrow 0;c\leftarrow 1\rangle$ $\displaystyle
p_{1}\langle z:=42;\ \mathop{\leftarrow c}\rangle$ $\displaystyle
p_{2}\langle\mathrel{\mathtt{let}}r:=\mathop{\leftarrow c}\
\mathrel{\mathtt{in}}\ \mathrel{\mathtt{if}}r=1\ \mathrel{\mathtt{then}}\
\mathrel{\mathtt{load}}z\rangle$ Figure 13: Conditional race example.

To illustrate this point, let us consider an execution of the program. Let
$({o})_{p}$ be a trace event capturing the execution of operation $o$ by
threads $p$. Let also ${z}!{}$ and ${z}?{}$ represent a write and read
operation on the shared variable $z$, and $\mathrel{\mathtt{sd}}\ {c}\ {}$ and
$\mathrel{\mathtt{rv}}\ {c}\ {}$ represent send and receive operations on
channel $c$. Assuming channel capacity $|\,{c}\,|\geq 2$, the sequence below
is a possible trace obtained from the execution of the program. Note that the
if-statement’s reduction is interpreted as an internal or silent transition:
Given that $p_{1}$ receives from $c$ before $p_{2}$ does, the value received
by $p_{2}$ must be $1$ as opposed to $0$. Therefore, $p_{2}$ takes the branch
and reads from the shared variable $z$. Figure 14 shows the partial order on
events for this execution.

$p_{0}$$p_{1}$$p_{2}$$\mathrel{\mathtt{sd}}\ {c}\
{0}$$~{}~{}\mathrel{\mathtt{sd}}\ {c}\ {1}$${z}!{}$$\mathrel{\mathtt{rv}}\
{c}\ {}$$\mathrel{\mathtt{rv}}\ {c}\ {}$${z}?{}$ Figure 14: Partial order on
conditional-race example.

Program order is captured by the vertical arrows in the diagram; channel
communication is captured by the solid diagonal arrows. As per discussion in
Section 3.2.3, we make the distinction between a channel operation and its
completion. A channel operations is depicted as two half-circles; the
operation’s completion is captured by the bottom half-circle. That way, a send
(top of the half-circle) happens-before its corresponding receive completes
(bottom half).

Now, given that the send operations are in happens-before, meaning
$({\mathrel{\mathtt{sd}}\ {c}\
{0}})_{p_{0}}\rightarrow_{\mathsf{hb}}({\mathrel{\mathtt{sd}}\ {c}\
{1}})_{p_{0}}$, and that channels are First-In-First-Out (FIFO), the reception
of value $0$ from $c$ must occur before the reception of $1$. This requirement
is captured by the dotted arrow in the diagram. However, according to the
semantics of channel communication (i.e. rules (1) and (2) of page 1), this
order does not impose a happens-before relation between the receiving events.
In other words, there exist events that are necessarily ordered, but not in
happens-before relation to one another.

The failure of our tentative definition of happens-before as necessarily-
occurring-before, given early in this section, has subtle implications as
discussed next.

###  6.1 Happens-before, traces, and commutativity of operations

Traces come from observing the execution of a program and are expressed as
strings of events. In a concurrent system, however, events may not be causally
related, which means that the order of some events is not pre-imposed. In
reality, instead of sequences, events in a concurrent system form a partially
ordered set (see Figure 14 for an example). As advocated by Mazurkiewicz,
[23], it is useful to combine sequential observations with a dependency
relation for studying “the nonsequential behaviour of systems via their
sequential observations.” By defining an _independence relation_ on events, it
is possible to derive a notion of equivalence on traces: two traces are
equivalent if it is possible to transform one into the other “by repeatedly
commuting adjacent pairs of independent operations” [17].

One way to define independence is as follows: Given a run
$R_{i}\xrightarrow{a}\cdot\xrightarrow{b}R$, we say that $a$ and $b$ are
independent if $R_{i}\xrightarrow{b}\cdot\xrightarrow{a}R$, meaning,

  * •

$b$ is enabled at $R_{i}$,

  * •

$a$ is enabled at $R_{i}\xrightarrow{b}\cdot$, and

  * •

there exists an $R^{\prime}$ such that
$R_{i}\xrightarrow{b}R^{\prime}\xrightarrow{a}R$.

Clearly, if $a$ happens-before $b$, then $a$ and $b$ cannot be swapped in a
trace. So, independence between two events means (at least) the absence of
happens-before relation between them. But happens-before is not all that needs
to be considered in the definition of independence.

When translating a partial order of events to a trace, not every linearization
that respects the happens-before relation is a valid trace. Some
linearizations of the partial order may not be “realizable” by the operational
semantics. In other words, there can be traces that abide by the happens-
before relation but that cannot be generated from the execution of a program.
For example, we can obtain the following linearization given the partial order
of Figure 14: This linearization respects the partial order based on the
happens-before relation: program order is respected, so is the relation
between sends and their corresponding receives. However, this linearization
breaks the first-in-first-out assumption on channels. FIFO is broken because,
in order for $p_{2}$ to read from $z$, it must be that it received the value
of $1$ from the channel. But $p_{2}$ is the first thread to receive from the
channel and, since $0$ was the first value into the channel, it must also have
been the first value read from the channel. Therefore, the linearization in
Trace LABEL:trace:conditional.race.not.realizable is not “realizable” by the
operational semantics. While happens-before restricts the commutation of trace
operations, there exist other operations that are ordered (though not ordered
by happens-before) and that, consequently, must not commute.

The difficulty in conciliating the commutativity of trace events with the
happens-before relation remains counterintuitive today, even though its
origins are related to an observation made years ago in a seminal paper by
Lamport,  [18]. In the paper, Lamport,  points out that “anomalies” can arise
when there exist orderings that are external to the definition of happens-
before—see the “Anomalous Behavior” section of [18]. In order to avoid these
anomalies, one suggestion from the paper is to expand the notion of happens-
before so that, if $a$ and $b$ are necessarily ordered, then $a$ and $b$ are
also in happens-before.

Let us analyze the consequences of rolling FIFO notions into the definition of
happens-before. Given the example of Figure 13, since the sends are ordered in
a happens-before relation, and the channel is FIFO, one can argue that the
receive events should also be ordered by happens-before. According to this
argument, we ought to promote the dotted line in Figure 14 to a solid
$\rightarrow_{\mathsf{hb}}$ arrow. This modification would make the example
well-synchronized. In one hand, given that the write to $z$ by $p_{1}$ and the
read from $z$ by $p_{2}$ are _always_ separated by events (by the two receive
events in specific), interpreting the two memory accesses as being
synchronized seems rather fitting: the two memory accesses cannot happen
simultaneously, nor can they exist side-by-side in a trace.

There are downsides to this approach. For one, the resulting semantics
deviates from Go’s, but, more importantly, such a change does impact
synchronization in counter intuitive ways. Specifically, making the dotted
arrow a happens-before arrow would imply that a receiver (in this case
$p_{2}$) can learn about prior events that are not known by the corresponding
sender. If the dotted arrow is promoted to a synchronization arrow, the write
${\color[rgb]{0.7,0.2,0.2}\definecolor[named]{pgfstrokecolor}{rgb}{0.7,0.2,0.2}{({{z}!{}})_{p_{1}}}}$
is communicated to $p_{2}$ via $p_{0}$ without $p_{0}$ itself being “aware” of
the write. In other words, the write identifier is transmitted via $p_{0}$ but
is not present in $p_{0}$’s happens-before set.

We follow Go and allow for some events to always occur in order without
affecting synchronization. Consequently, such ordered events are not
considered to be in _happens-before_ order. A less clear consequence, however,
is that races can longer be defined as simultaneous (or side-by-side) accesses
to a shared variable. This point is explored next.

###  6.2 Manifest data races

Section 2 mentioned the concept of manifest data race; below we give a
concrete definition.

######  Definition 1 (Manifest data race)

A well-formed configuration $R$ contains a _manifest data race_ if either
hold:

$\displaystyle
R\xrightarrow{{\color[rgb]{0.7,0.2,0.2}\definecolor[named]{pgfstrokecolor}{rgb}{0.7,0.2,0.2}{({{z}!{}})_{p_{1}}}}}\text{~{}and~{}}R\xrightarrow{{\color[rgb]{0.7,0.2,0.2}\definecolor[named]{pgfstrokecolor}{rgb}{0.7,0.2,0.2}{({{z}!{}})_{p_{2}}}}}$
(manifest write-write race on $z$) $\displaystyle
R\xrightarrow{{\color[rgb]{0.2,0.2,0.7}\definecolor[named]{pgfstrokecolor}{rgb}{0.2,0.2,0.7}({{z}?{}})_{p_{1}}}}\text{~{}and~{}}R\xrightarrow{{\color[rgb]{0.7,0.2,0.2}\definecolor[named]{pgfstrokecolor}{rgb}{0.7,0.2,0.2}{({{z}!{}})_{p_{2}}}}}$
(manifest read-write race on $z$)

for some $p_{1}\not=p_{2}$.

Manifest data races can also be defined on traces.

######  Definition 2 (Manifest data race)

A well-formed trace $h$ contains a _manifest data race_ if either

$\displaystyle{\color[rgb]{0.7,0.2,0.2}\definecolor[named]{pgfstrokecolor}{rgb}{0.7,0.2,0.2}{({{z}!{}})_{p_{1}}}}~{}$
$\displaystyle{\color[rgb]{0.7,0.2,0.2}\definecolor[named]{pgfstrokecolor}{rgb}{0.7,0.2,0.2}{({{z}!{}})_{p_{2}}}}\,$
(manifest write-after-write)
$\displaystyle{\color[rgb]{0.7,0.2,0.2}\definecolor[named]{pgfstrokecolor}{rgb}{0.7,0.2,0.2}{({{z}!{}})_{p_{1}}}}~{}$
$\displaystyle{\color[rgb]{0.2,0.2,0.7}\definecolor[named]{pgfstrokecolor}{rgb}{0.2,0.2,0.7}({{z}?{}})_{p_{2}}}\,$
(manifest read-after-write)
$\displaystyle{\color[rgb]{0.2,0.2,0.7}\definecolor[named]{pgfstrokecolor}{rgb}{0.2,0.2,0.7}({{z}?{}})_{p_{1}}}~{}$
$\displaystyle{\color[rgb]{0.7,0.2,0.2}\definecolor[named]{pgfstrokecolor}{rgb}{0.7,0.2,0.2}{({{z}!{}})_{p_{2}}}}$
(manifest write-after-read)

are a sub-sequence of $h$ and where $p_{1}\not=p_{2}$).

While manifest races are obvious, races in general may involve accesses that
are arbitrarily “far apart” in a linear execution. By bring conflicting
accesses side-by-side, we could show irrefutable evidence of a race that,
otherwise, may be obscured in a trace. Let $h\sqsubseteq h^{\prime}$ represent
the fact that $h^{\prime}$ is derivable from $h$ by the repeated commutation
of adjacent pairs of independent operations. If $h\sqsubseteq h^{\prime}$ and
$h^{\prime}$ contains a manifest data race, then we say $h$ contains a data-
race. This definition of races seems unequivocal. From here, soundness and
completeness of a race detector may be defined as such:

###### Theorem 6.1

(Soundness) If $S_{0}\xrightarrow{h}$ is a run flagged by a data-race
detector, then $h\sqsubseteq h_{dr}$ with $h_{dr}$ containing a manifest data-
race.

###### Theorem 6.2

(Completeness) Let $S_{0}\xrightarrow{h}$ be a run such that $h\sqsubseteq
h_{dr}$ and $h_{dr}$ contains a manifest race. Then $S_{0}\xrightarrow{h}$ is
flagged by the data-race detector.

Theorems 6.1 and 6.2 are also clear and unequivocal. More importantly, they
link two world views: the view of races as unsynchronized accesses with
respect to the happens-before relation and a view of races in terms of
commutativity of trace events à la Mazurkiewicz. The problem with the concept
of manifest data race and Theorems 6.1 and 6.2, however, is that when the
definition of independence is made to respect FIFO order as well as the
happens-before relation, the notion of manifest data race is no longer
attainable. In other words, given a definition of independence which respects
FIFO and happens-before, there exist racy traces from which a manifest data
race is not derivable.

The program of Figure 13 gives rise to such an example. The access to $z$ by
$p_{2}$ only occurs if $p_{2}$ receives the second message sent on the
channel. In other words, the existence of event
${\color[rgb]{0.2,0.2,0.7}\definecolor[named]{pgfstrokecolor}{rgb}{0.2,0.2,0.7}({{z}?{}})_{p_{2}}}$
in a trace is predicated on the order of execution of channel operations:
$p_{2}$ only reads from $z$ if the other thread, $p_{1}$, receives from $c$
before $p_{2}$ does.202020In this example, we use the value of the message
received on a channel to branch upon. But since a receive from a channel
changes a thread’s “visibility” of what is in memory, it is possible to craft
a similar example in which all message values are unit but in which a thread’s
behavior changes due to a change in the ordering of the receives. This
requirement places the receive operations between the memory operations.
Therefore, a trace in which
${\color[rgb]{0.7,0.2,0.2}\definecolor[named]{pgfstrokecolor}{rgb}{0.7,0.2,0.2}{({{z}!{}})_{p_{1}}}}$
and
${\color[rgb]{0.2,0.2,0.7}\definecolor[named]{pgfstrokecolor}{rgb}{0.2,0.2,0.7}({{z}?{}})_{p_{2}}}$
are side-by-side is not attainable. Yet, as discussed previously, the accesses
to $z$ are not ordered by happens-before, and, therefore, are concurrent.
Since the accesses are also conflicting, they constitute a data race.

It seems that Mazurkiewicz traces are “more compatible” with confluence
checking than data-race checking. In data-race checking, there are non-
confluent runs that do not exhibit data races; these runs are non-confluent
because they have “races on channels.” In our example, the two receives from
$p_{1}$ and $p_{2}$ are in competition for access to the channel. These
receive operations are concurrent and non-confluent. Finally, the example also
hints at the perhaps more fundamental observation: that races have little to
do with _simultaneous_ accesses to a shared variable but instead with
_unsynchronized_ accesses. While simultaneous accesses are clearly
unsynchronized, not all unsynchronized accesses may be made
simultaneous.212121There may not exist a configuration from which two
transitions are possible; transitions that involve conflicting memory
accesses. Yet, it is possible for two access separated “in time” to be
unsynchronized.

##  7 Related work

Race detection via the analysis of source code is an undecidable problem.
Regardless, race detectors via the static analysis of source code [24, 39, 3]
exist and have found application in industry. More recently, Blackshear et
al.,  [3] implement a static analysis tool called RacerD to help the
parallelization of previously sequential Java source code. The tool over
approximates the behavior of programs and can, thereby, reject programs that
turn out to be data-race free. This over approximation was not a hindrance, as
even conservative parallelization efforts can lead to gains over purely
sequential code.

By and large, however, instead of flagging races in a program as a whole, race
detectors have resorted the analysis of particular _runs_ of a program. To
that end, detectors instrument the program so that races are either flagged
during execution, in what is called _on-line_ or _on-the-fly_ race detection,
or on logs captured during execution and analyzed postmortem. Even still,
dynamic race detection is NP-hard [25] and many techniques have been proposed
for detection at scale. Broadly, these techniques involve static analysis used
to reduce the number of runtime checks [11][31], and heuristics that trade
false-positive [33, 30, 5] or false-negative rates [21] for better space/time
utilization. For example, by allowing races to sometimes go undetected,
_sampling_ race detectors let go of completeness in favor of lower overheads.
One common heuristic, called the _cold region hypothesis_ , is to sample more
frequently from less executed regions of the program. This rule-of-thumb
hinges on the assumption that faults are more likely to already have been
identified and fixed if they occur in the hot regions of a program [21].
Alternatively, by going after a proxy instead of an actual race, imprecise
race detectors let go of soundness. The prominent examples here are Eraser’s
LockSet [33] and Locksmith [30], which enforce a lock-based synchronization
discipline. A violation of the discipline is a _code smell_ but not
necessarily a race. The amalgamation of different approaches have also been
investigated, leading to _hybrid race detectors_. For example, O’Callahan and
Choi,  [26] combined LockSet-based detection with happens-before information
reconstructed from vector clocks; Choi et al.,  [5] extended LockSet to
incorporate static analyses.

Another avenue of inquiry has lead to _predictive race detection_ [36, 16],
which attempts to achieve higher detection capabilities by extrapolating
beyond individual runs. Huang et al.,  [16] incorporate abstracted control
flow information and formulate race detection as a constraint solving problem.
With the goal of observing more races per run, Smaragdakis et al.,  [36]
introduce a new relation, called _causally-precedes_ , which is a
generalization of the happens-before relation.

A number of papers address race detection in the context of channel
communication [6, 7, 38]. Some of the papers, however, do not speak of shared
memory but, instead, define races as conflicting channel accesses. In that
setting, the lack of conflicting accesses to channels imply determinacy. A
different angle is taken by Terauchi and Aiken,  [38], who, among different
kinds of channels, define a buffered channel whose buffer is overwritten by
every write (i.e. send) but never modified by a read (i.e. receive). This kind
of channel, referred to as a _cell_ , behaves, in essence, as shared memory.
The goal of Terauchi and Aiken,  [38] is, still, determinacy. Having conflated
the concept of shared memory as a channel, determinacy is then achieved by
ensuring the absence of conflicting accesses to channels. Our goal, however,
is different: we aim to detect data-races but do not want to go as far as
ensuring determinacy. Therefore, our approach allows “races” on channel
accesses. From a different perspective, however, the work of Terauchi and
Aiken,  [38] can be seen as complementary to ours: We conjecture that their
type system can serve as the basis for a static data-race detector.

Among the dynamic data-race detection tools from industry, Banerjee et al.,
[1] discuss different race detection algorithms including one used by the
Intel Thread Checker. The authors describe _adjacent conflicts_ , which is
similar to our notion of side-by-side or manifest data race. The paper also
classifies races similar to our WaR, RaW, and WaW classification.

Go has a race detector integrated to its tool chain [13]. The `-race` command-
line flag instructs the Go compiler to instrument memory accesses and
synchronization events. The race detector is built on top of Google’s
sanitizer project [14] and TSan in particular [34, 15]. TSan is part of the
LLVM’s runtime libraries [35, 20]; it works by instrumenting memory accesses
and monitoring locks acquisition and release as well as thread forks and
joins. Note, however, that channel communication is the vehicle for achieving
synchronization in Go. Even though locks exist, they are part of a package,
while channels are built into language. Yet, the race detector for Go sits at
a layer underneath. In this paper we study race detection with channel
communication taking a central role. Also, different from TSan, we employ
propose a technique based on what we call _happens-before sets_ as opposed to
vector clocks. The consequences of this decision is discussed in detail on
Section 5.

It is also relevant to point out that, in the absence of the DRF-SC guarantee,
one may resort to finding data races involving weak memory behavior. Since the
full C/C++11 memory model can harbor such races, and with the goal of finding
data races in production level code, Lidbury and Donaldson,  [19] extend the
ThreadSanitizer (TSan) [34, 15] to support a class of non-sequentially
consistent executions.

##  8 Conclusion

We presented a dynamic data-race detector for a language in the style of Go:
featuring channel communication as sole synchronization primitive. The
proposed detector records and analyzes information locally and is well-suited
for online detection.

Our race detector is built upon a previous result [10], where we formalize a
weak memory model inspired by the Go specification [12]. In that setting, we
recorded memory read- and write-events that were in happens-before relation
with respect to a thread’s present operation. This information was stored in a
set called $E_{\mathit{hb}}$ or the happens-before set of a thread, and it was
used to regulate a thread’s visibility of memory events. The core of the paper
was a proof of the DRF-SC guarantee, meaning, we proved that the proposed
relaxed memory model behaves sequentially consistently in the absence of data
races. The proof hinges on the fact that, in the absence of races, all threads
agree on the contents of memory; see the _consensus lemma_ in [10]. The
scaffolding used in the proof of the consensus lemma contains the ingredients
used of the race detectors presented in this paper. Based on our experience,
we conjecture that one may automatically derive a race detector given a weak
memory model and its corresponding proof of the DRF-SC guarantee.

In the DRF-SC the proof of [10], we show that if a program is racy, it behaves
sequentially consistent up to the point in which the first data-race is
encountered. In other words, this first point of divergence sets in motion all
behavior that is not sequentially consistent and which arise from the weakness
in the memory model. With this observation, we argue that a race detector can
operate under the assumption of sequential consistency. This is a useful
simplification, as sequential consistent memory is conceptually much simpler
than relaxed memories. If the data-race detector flags the first evidence of a
data-race, then program behavior is sequentially consistent up to that point.

Avenues for future work abound. In contrast to data-race detectors based on
vector clocks, our approach using happens-before sets does not provide as
terse of a representation for the collection of memory events performed by a
thread in between synchronization points. In effect, out approach has a larger
foot-print, which ought to be mitigated. On the other hand, our thorough
expunging of stale information can serve as inspiration to vector clock based
approaches, which allow for the accumulation of stale information—see Section
6. Another extension would be to statically analyze a target program with the
goal of removing dynamic checks or ameliorating the detector’s memory
consumption. Here, we may be able to borrow from the research on static
analysis for dynamic race-detection in the context of lock-based
synchronization disciplines.

## References

  * Banerjee et al., [2006] Banerjee, U., Bliss, B., Ma, Z., and Petersen, P. (2006).  A theory of data race detection.  In Proceedings of the 4th Workshop on Parallel and Distributed Systems: Testing, Analysis, and Debugging, held in conjunction with the ACM SIGSOFT International Symposium on Software Testing and Analysis (ISSTA 2006), PADTAD 2006, Portland, Maine, USA, July 17, 2006, pages 69–78.
  * Benveniste et al., [2003] Benveniste, A., Caspi, P., Edwards, S. A., Halbwachs, N., Guernic, P. L., and de Simone, R. (2003).  The synchronous languages 12 years later.  Proceedings of the IEEE, 91(1):64–83.
  * Blackshear et al., [2018] Blackshear, S., Gorogiannis, N., O’Hearn, P. W., and Sergey, I. (2018).  Racerd: compositional static race detection.  PACMPL, 2(OOPSLA):144:1–144:28.
  * Channel types, Go language specification, [2016] Channel types, Go language specification (2016).  Channel types, the Go programming language specification.  https://golang.org/ref/spec#Channel_types.
  * Choi et al., [2002] Choi, J., Lee, K., Loginov, A., O’Callahan, R., Sarkar, V., and Sridharan, M. (2002).  Efficient and precise datarace detection for multithreaded object-oriented programs.  In ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI) Berlin, Germany, pages 258–269. ACM.
  * Cypher and Leu, [1995] Cypher, R. and Leu, E. (1995).  Efficient race detection for message-passing programs with nonblocking sends and receives.  In Proceedings. Seventh IEEE Symposium on Parallel and Distributed Processing, pages 534–541. IEEE.
  * Damodaran-Kamal and Francioni, [1993] Damodaran-Kamal, S. K. and Francioni, J. M. (1993).  Nondeterminancy: testing and debugging in message passing parallel programs.  ACM SIGPLAN Notices, 28(12):118–128.
  * [8] Dijkstra, E. W. (n.d.).  Over de sequentialiteit van procesbeschrijvingen.  Circulated privately.
  * Fava, [2020] Fava, D. (2020).  Grace: a race detector based on happens-before sets.  https://github.com/dfava/grace.
  * Fava et al., [2018] Fava, D., Steffen, M., and Stolz, V. (2018).  Operational semantics of a weak memory model with channel synchronization.  Journal of Logic and Algebraic Methods in Programming.  An extended version of the FM’18 publication with the same title.
  * Flanagan and Freund, [2009] Flanagan, C. and Freund, S. N. (2009).  FastTrack: Efficient and precise dynamic race detection.  In Hind, M. and Diwan, A., editors, ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI), pages 121–133. ACM.
  * Go memory model, [2014] Go memory model (2014).  The Go memory model.  https://golang.org/ref/mem.  Version of May 31, 2014, covering Go version 1.9.1.
  * golang.race.detector, [2013] golang.race.detector (2013).  https://blog.golang.org/race-detector.
  * google.sanitizer, [2014] google.sanitizer (2014).  https://github.com/google/sanitizers.
  * google.thread.sanitizer, [2015] google.thread.sanitizer (2015).  https://github.com/google/sanitizers/wiki/ThreadSanitizerAlgorithm.
  * Huang et al., [2014] Huang, J., Meredith, P. O., and Rosu, G. (2014).  Maximal sound predictive race detection with control flow abstraction.  In ACM SIGPLAN Conference on Programming Language Design and Implementation, PLDI ’14, Edinburgh, United Kingdom - June 09 - 11, 2014, pages 337–348. ACM.
  * Katz and Peled, [1992] Katz, S. and Peled, D. (1992).  Defining conditional independence using collapses.  Theoretical Computer Science, 101.
  * Lamport, [1978] Lamport, L. (1978).  Time, clocks, and the ordering of events in a distributed system.  Communications of the ACM, 21(7):558–565.
  * Lidbury and Donaldson, [2017] Lidbury, C. and Donaldson, A. F. (2017).  Dynamic race detection for C++11.  In Castagna, G. and Gordon, A. D., editors, Proceedings of the 44th ACM SIGPLAN Symposium on Principles of Programming Languages, POPL 2017, Paris, France, January 18-20, 2017, pages 443–457. ACM.
  * llvm.thread.sanitizer, [2011] llvm.thread.sanitizer (2011).  https://clang.llvm.org/docs/ThreadSanitizer.html.
  * Marino et al., [2009] Marino, D., Musuvathi, M., and Narayanasamy, S. (2009).  Literace: effective sampling for lightweight data-race detection.  In ACM Sigplan notices, pages 134–143.
  * Mattern, [1988] Mattern, F. (1988).  Virtual time and global states in distributed systems.  In Proceedings of the International Conference on Parallel and Distributed Algorithms, pages 215–226.
  * Mazurkiewicz, [1987] Mazurkiewicz, A. (1987).  Trace theory.  In Brauer, W., Reisig, W., and Rozenberg, G., editors, Petri Nets: Applications and Relationships to Other Models of Concurrency, (Advances in Petri Nets 1986) Part II, volume 255 of Lecture Notes in Computer Science, pages 279–324. Springer Verlag.
  * Naik et al., [2006] Naik, M., Aiken, A., and Whaley, J. (2006).  Effective static race detection for Java.  In Proceedings of the 27th ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI), pages 308–319. ACM.
  * Netzer and Miller, [1990] Netzer, R. H. B. and Miller, B. P. (1990).  On the complexity of event ordering for shared-memory parallel program executions.  In Proceedings of the 1990 International Conference on Parallel Processing, Urbana-Champaign, IL, USA, August 1990. Volume 2: Software., pages 93–97.
  * O’Callahan and Choi, [2003] O’Callahan, R. and Choi, J.-D. (2003).  Hybrid dynamic data race detection.  In Proceedings of the ACM SIGPLAN Symposium on Principles and Practice of Parallel Programming, PPOPP 2003, June 11-13, 2003, San Diego, CA, USA, pages 167–178.
  * Palamidessi, [1997] Palamidessi, C. (1997).  Comparing the expressive power of the synchronous and the asynchronous $\pi$-calculus.  In Proceedings of POPL ’97, pages 256–265. ACM.
  * Peters and Nestmann, [2012] Peters, K. and Nestmann, U. (2012).  Is it a “good” encoding of mixed choice?  In Proceedings of the International Conference on Foundations of Software Science and Computation Structures (FoSSaCS ’12), volume 7213 of Lecture Notes in Computer Science, pages 210–224. Springer Verlag.
  * Pozniansky and Schuster, [2003] Pozniansky, E. and Schuster, A. (2003).  Efficient on-the-fly data race detection in multi-threaded C++ programs.  In Proceedings of the 9th ACM Symposium on Principles and Practice of Parallel Programming (PPoPP’03).
  * Pratikakis et al., [2006] Pratikakis, P., Foster, J. S., and Hicks, M. W. (2006).  LOCKSMITH: Context-sensitive correlation analysis for race detection.  In Proceedings of the 27th ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI), pages 320–331. ACM.
  * Rhodes et al., [2017] Rhodes, D., Flanagan, C., and Freund, S. N. (2017).  Bigfoot: Static check placement for dynamic race detection.  In Proceedings of the 38th ACM SIGPLAN Conference on Programming Language Design and Implementation, PLDI 2017, Barcelona, Spain, June 18-23, 2017, pages 141–156.
  * Sabry and Felleisen, [1992] Sabry, A. and Felleisen, M. (1992).  Reasoning about programs in continuation-passing style.  In Clinger, W., editor, Conference on Lisp and Functional Programming (San Francisco, California), pages 288–298. ACM.
  * Savage et al., [1997] Savage, S., Burrows, M., Nelson, G., Sobalvarro, P., and Anderson, T. (1997).  Eraser: A dynamic data race detector for multithreaded programs.  ACM Transactions on Computer Systems, 15(4):391–411.
  * Serebryany and Iskhodzhanov, [2009] Serebryany, K. and Iskhodzhanov, T. (2009).  Threadsanitizer: data race detection in practice.  In Proceedings of the Workshop on Binary Instrumentation and Applications, pages 62–71. ACM.
  * Serebryany et al., [2011] Serebryany, K., Potapenko, A., Iskhodzhanov, T., and Vyukov, D. (2011).  Dynamic race detection with llvm compiler.  In International Conference on Runtime Verification, pages 110–114. Springer.
  * Smaragdakis et al., [2012] Smaragdakis, Y., Evans, J., Sadowski, C., Yi, J., and Flanagan, C. (2012).  Sound predictive race detection in polynomial time.  In Proceedings of POPL ’12, pages 387–400. ACM.
  * Steffen and Nestmann, [1995] Steffen, M. and Nestmann, U. (1995).  Typing confluence.  Interner Bericht IMMD7-xx/95, Informatik VII, Universität Erlangen-Nürnberg.
  * Terauchi and Aiken, [2008] Terauchi, T. and Aiken, A. (2008).  A capability calculus for concurrency and determinism.  ACM Transactions on Programming Languages and Systems (TOPLAS), 30(5):27.
  * Voung et al., [2007] Voung, J. W., Jhala, R., and Lerner, S. (2007).  RELAY: Static race detection on millios of lines of code.  In Proceedings oof the 6th Joint Meeting of the European Software Engineering Conference and ACM SIGSOFT International Symposium on Foundations of Software Engineering, pages 205–214.

Figure 16: Local steps

###  0.A.3 Memory interactions and channel communication

Reading and writing, the two basic memory interactions, are covered in Figure
0.A.3 and channel communication in Figure 0.A.3. Compared to the semantics for
race detection (cf. Figures 6 and 4), the semantics here is done without extra
information and book-keeping of happens-before information. Related to that,