1–LABEL:LastPageNov. 23, 2016Jan. 16, 2018 [Theory of computation]: AAA—BBB;
[Mathematics of computing]: CCC—DDD

* A preliminary version of this paper has appeared at FORTE 2016, held as Part of the 11th International Federated Conference on Distributed Computing Techniques, DisCoTec 2016

# Fencing Programs with Self-Invalidations and Self-Downgrades

Parosh Aziz Abdullaa  aUppsala University, Sweden<EMAIL_ADDRESS><EMAIL_ADDRESS><EMAIL_ADDRESS><EMAIL_ADDRESS><EMAIL_ADDRESS>,  Mohamed Faouzi Atiga  ,
Stefanos Kaxirasa  ,  Carl Leonardssona  ,  Alberto Rosb  bUniversidad de
Murcia, Spain<EMAIL_ADDRESS>and  Yunyun Zhua

# Mending Fences with Self-Invalidation and Self-Downgrade*

Parosh Aziz Abdullaa  aUppsala University, Sweden<EMAIL_ADDRESS><EMAIL_ADDRESS><EMAIL_ADDRESS><EMAIL_ADDRESS><EMAIL_ADDRESS>,  Mohamed Faouzi Atiga  ,
Stefanos Kaxirasa  ,  Carl Leonardssona  ,  Alberto Rosb  bUniversidad de
Murcia, Spain<EMAIL_ADDRESS>and  Yunyun Zhua

###### Abstract.

Cache coherence protocols based on self-invalidation and self-downgrade have
recently seen increased popularity due to their simplicity, potential
performance efficiency, and low energy consumption. However, such protocols
result in memory instruction reordering, thus causing extra program behaviors
that are often not intended by the programmers. We propose a novel formal
model that captures the semantics of programs running under such protocols,
and features a set of fences that interact with the coherence layer. Using the
model, we design an algorithm to analyze the reachability and check whether a
program satisfies a given safety property with the current set of fences. We
describe a method for insertion of optimal sets of fences that ensure
correctness of the program under such protocols. The method relies on a
counter-example guided fence insertion procedure. One feature of our method is
that it can handle a variety of fences (with different costs). This diversity
makes optimization more difficult since one has to optimize the total cost of
the inserted fences, rather than just their number. To demonstrate the
strength of our approach, we have implemented a prototype and run it on a wide
range of examples and benchmarks. We have also, using simulation, evaluated
the performance of the resulting fenced programs.

###### Key words and phrases:

automatic fence insertion, cache coherence protocol, self-invalidation, self-
downgrade

##  1\. Introduction

### Background.

Traditional cache coherence protocols, either directory-based or snooping-
based, are transparent to the programmer in the sense that they respect the
memory consistency model of the system, and hence there is no effect on memory
ordering due to the coherence protocol. On the other hand, there is an ever
larger demand on hardware designers to increase efficiency both in performance
and power consumption. The quest to increase performance while maintaining
transparency has led to complex coherence protocols with many states and
relying on directories, invalidations, broadcasts, etc, often at the price of
high verification cost, area (hardware cost) and increased energy consumption.
Therefore, many researchers have recently proposed ways to simplify coherence
without compromising performance but at the price of relaxing the memory
consistency model [LW95, CKS+11, KK11, RK12, SKA13, KR13, HHB+14, RDK15, SA15,
RK15a, DRHK15, KRHK16, RK16]. Principal techniques among these proposals are
Self-Invalidation (Si) and Self-Downgrade (Sd).

A protocol with Self-Invalidation (Si) allows old copies of the data to be
kept, without invalidation on each store operation by another core. This
eliminates the need for tracking readers [LW95]. In an Si protocol,
invalidation of data from a cache is caused by synchronization instructions
executed by the core local to the cache.

Correspondingly, in a protocol with Self-Downgrade (Sd), downgrades are not
caused by read operations in other cores, but again by synchronization
instructions. Sd eliminates the need to track the last writer of a cache line
[RK12].

A protocol with both self-invalidation and self-downgrade (SiSd) does not need
a directory, thus removing a main source of complexity and scalability
constraints in traditional cache coherence protocols [RK12]. But this comes at
a price: SiSd protocols induce weak memory semantics that allow reordering or
memory instructions. The behavior of a program may now deviate from its
behavior under the standard Sequentially Consistent (SC) semantics [Lam79],
sometimes leading to subtle errors that are hard to detect and correct.

In the context of weak memory, hardware designers provide memory fence
instructions to help the programmer to eliminate the undesired behaviors. A
fence instruction, executed by a thread, limits the allowed reorderings
between instructions issued before and after the fence instruction. To enforce
consistency under SiSd, fences should also be made visible to caches, such
that necessary invalidations or downgrades may be performed. In this paper, we
consider different types of fences. Each type eliminates a different kind of
non-SC behavior, and may have different impact on the program performance. In
fact, unnecessary fences may significantly jeopardize program performance.
This is particularly true for the fences considered in this work, since they
both incur latency, and affect the performance of the cache coherence
subsystem as a whole. These fences cause the invalidation of the contents of
the cache. Hence the more fences the less caching and the higher traffic we
have. Thus, it is desirable to find the _optimal_ set of fences, which
guarantee correctness at minimal performance cost. There are multiple ways of
defining optimality. The one we adopt is to calculate the number of
occurrences of fences in the source program, with the costs of different
fences taken into account.

### Challenge.

One possibility to make SiSd transparent to the program is to require the
programmer to ensure that the program does not contain any data races. In
fact, data race freedom is often required by designers of SiSd protocols in
order to guarantee correct program behavior [CKS+11, KK11]. However, this
approach would unnecessarily disqualify large sets of programs, since many
data races are in reality not harmful. Examples of correct programs with races
include lock-free data structures (e.g., the Chase-Lev Work-stealing queue
algorithm [CL05]), transactional memories (e.g., the TL2 algorithm [DSS06]),
and synchronization library primitives (e.g. pthread_spin_lock in glibc). In
this paper, we consider a different approach where fences are inserted to
restore correctness. This means that we may insert sufficiently many fences to
achieve program correctness without needing to eliminate all its races or non-
SC behaviors. The challenge then is to find sets of fences that guarantee
program correctness without compromising efficiency. Manual fence placement is
time-consuming and error-prone due to the complex behaviors of multithreaded
programs [HS08]. Thus, we would like to provide the programmer with a tool for
automatic fence placement. There are several requirements to be met in the
design of fence insertion algorithms. First, a set of fences should be sound,
i.e., it should have enough fences to enforce a sufficiently ordered behavior
for the program to be correct. Second, the set should be optimal, in the sense
that it has a lowest total cost among all sound sets of fences. We define the
cost to be the number of occurrences of fences in the source program, with the
costs of different fences taken into account. In general, there may exist
several different optimal sets of fences for the same program. Our experiments
(Section 7) show that different choices of sound fence sets may impact
performance and network traffic.

To carry out fence insertion we need to be able to perform program
verification, i.e., to check correctness of the program with a given set of
fences. This is necessary in order to be able to decide whether the set of
fences is sound, or whether additional fences are needed to ensure
correctness. A critical task in the design of formal verification algorithms
is to define the program semantics under the given memory model.

### Our Approach.

We present a method for automatic fence insertion in programs running in the
presence of SiSd. The method is applicable to a large class of self-
invalidation and self-downgrade protocols such as the ones in [LW95, CKS+11,
KK11, RK12, SKA13, KR13, HHB+14, RDK15, SA15, RK15a, DRHK15, KRHK16]. Our goal
is to eliminate incorrect behaviors that occur due to the memory model induced
by SiSd. We will not concern ourselves with other sources of consistency
relaxation, such as compiler optimizations. We formulate the correctness of
programs as safety properties. A safety property is an assertion that some
specified “erroneous”, or “bad”, program states can never occur during
execution. Such bad states may include e.g., states where a programmer-
specified assert statement fails, or where uninitialized data is read. To
check a safety property, we check the reachability of the set of “bad” states.

We provide an algorithm for checking the reachability of a set of bad states
for a given program running under SiSd. In the case that such states are
reachable, our algorithm provides a counter-example (i.e., an execution of the
program that leads to one of the bad states). This counter-example is used by
our fence insertion procedure to add fences in order to remove the counter-
examples introduced by SiSd semantics. Thus, we get a counter-example guided
procedure for inferring the optimal sets of fences. The termination of the
obtained procedure is guaranteed under the assumption that each call to the
reachability algorithm terminates. As a special case, our tool detects when a
program behaves incorrectly already under SC. Notice that in such a case, the
program cannot be corrected by inserting any set of fences.

### Contributions.

We make the following main contributions:

  * •

We define a novel formal model that captures the semantics of programs running
under SiSd, and employs a set of fences that interact with the coherence
layer. The semantics support the essential features of typical assembly code.

  * •

We develop a tool, Memorax, available at https://github.com/memorax/memorax,
that we have run successfully on a wide range of examples under SiSd and under
Si. Notably, our tool detects for the first time four bugs in programs in the
Splash-2 benchmark suite [WOT+95], which have been fixed in a recent Splash-3
release [SLKR16]. Two of these are present even under SC, while the other two
arise under SiSd. We employ the tool to infer fences of different kinds and
evaluate the relative performance of the fence-augmented programs by
simulation in GEMS.

We augment the semantics with a reachability analysis algorithm that can check
whether a program satisfies a given safety property with the current set of
fences. Inspired by an algorithm in [LNP+12] (which uses dynamic analysis
instead of verification as backend), we describe a counter-example guided
fence insertion procedure that automatically infers the optimal sets of fences
necessary for the correctness of the program. The procedure relies on the
counter-examples provided by the reachability algorithm in order to refine the
set of fences. One feature of our method is that it can handle different types
of fences with different costs. This diversity makes optimization more
difficult since one has to optimize the total cost of the inserted fences,
rather than just their number. Upon termination, the procedure will return all
optimal sets of fences.

### Related Work.

Adve and Hill proposed SC-for-DRF as a contract between software and hardware:
If the software is data race free, the hardware behaves as sequentially
consistent [AH90]. Dynamic self-invalidation (for DRF programs) was first
proposed by Lebeck and Wood [LW95]. Several recent works employ self-
invalidation to simplify coherence, including SARC coherence [KK11], DeNovo
[CKS+11, SKA13, SA15], and VIPS-M [RK12, KR13, RDK15, RK15a, KRHK16].

A number of techniques for automatic fence insertion have been proposed, for
different memory models and with different approaches. However, to our
knowledge, we propose the first counter-example guided fence insertion
procedure in the presence of a variety of fences (with different costs). In
our previous work [AAC+12], we propose counter-example guided fence insertion
for programs under TSO with respect to safety properties (also implemented in
Memorax). Considering the SiSd model makes the problem significantly more
difficult. TSO offers only one fence, whereas the SiSd model offers a variety
of fences with different costs. This diversity makes the optimization more
difficult since one has to minimize the total cost of the fences rather than
just their number.

The work presented in [KVY10] proposes an insertion procedure for different
memory models w.r.t. safety properties. This procedure computes the set of
needed fences in order to not reach each state in the transition graph.
Furthermore, this procedure assigns a unique cost for all fences. The
procedure is not counter-example based, and requires some modification to the
reachability procedure.

In [BDM13], the tool Trencher is introduced, which inserts fences under TSO to
enforce robustness (formalised by Shasha and Snir in [SS88]), also using an
exact, model-checking based technique. Musketeer [AKNP14] uses static analysis
to efficiently overapproximate the fences necessary to enforce robustness
under several different memory models. In contrast to our work, the fence
insertion procedures in [BDM13] and [AKNP14] first enumerate all solutions and
then use linear programming to find the optimal set of fences.

In [GHS11] and [GHS09], the authors discuss fence insertion and verification
of satisfiability modulo theory (SMT) of relaxed memory models under
transactional memories. Our work, in comparison, addresses the reachability
problem.

The program semantics under SiSd is different from those under other weak
memory models (e.g. TSO and POWER). Hence existing techniques cannot be
directly applied. To our knowledge, ours is the first work that defines the
SiSd model, proposes a reachability analysis and describes a fence insertion
procedure under SiSd.

There exist works on the verification of cache coherence protocols. This paper
is orthogonal to these works since we are concerned with verification of
programs running on such architectures and not the protocols themselves.

##  2\. Self-Invalidation, Self-Downgrade, and their Fences

In this section, we recall the notions of self-invalidation and self-
downgrade, and describe the main features of the system architecture and the
protocol we consider. We also introduce two fences that are defined under the
protocol.

###  2.1. Self-Invalidation and Self-Downgrade

Self-invalidation eliminates the need to track sharers of a cache line in a
directory structure [LW95]. We consider that invalidation of shared data in
caches is caused by fences inserted in the programs and not as a result of
writes from other cores.

Correspondingly, self-downgrade eliminates the need to track the last writer
(i.e., the owner, in a Moesi-like protocol) of a cache line [RK12]. This is
because downgrades are also not performed as a consequence of read operations,
but by means of fence instructions inserted in the programs.

A protocol that implements self-invalidation together with self-downgrade does
not need a directory, thus removing one of the main sources of complexity and
scalability constraints in traditional cache coherence protocols [RK12].

We first set the stage for the architecture and the coherence protocol we
study in this work, by discussing some of their details: i.e., how memory
accesses are resolved, and how the self-invalidation and the self-downgrade
are performed when a fence is encountered.

##### System architecture

We assume a standard multicore architecture with a number of cores, each with
a private L1 cache. The proposals and algorithms described in this paper are
more widely applicable to systems with several levels of private caches. The
last level cache (LLC) of the system is logically shared among all the cores.

###  2.2. Cache coherence protocol

We also assume a very simple version of a self-invalidation/self-downgrade
protocol with only three stable states in the L1 cache (invalid –I–, clean
–C–, and dirty –D–) and only two stable states in the LLC (invalid –I– and
valid –V–). There are no invalidations or downgrades, which means that there
are no transient states to account for the arrival of such coherence actions.
There are no requests other than from the L1s to the LLC (and from LLC to
memory). There is no distinction of data into private or shared as in [RK12],
as this would distract from our discussion. Such optimizations are
straightforward extensions in our approach.

##### Basic actions:

To connect with the formal specification of the system behavior that follows
in Section 4 we present here some necessary —if somewhat mundane— details of
the basic actions in our assumed system.

  * •

A read request that misses in the L1 cache issues a request to the LLC. If it
hits in the LLC, a reply containing the data is sent. In case of a miss, main
memory is accessed to get the data block. When the data arrives to the L1
cache, the miss is resolved and the data can be accessed. The block is stored
in an L1 cache line in clean state.

  * •

A write request is always resolved immediately, even if the block is not
present in the L1 (in this case, the miss status handling register –MSHR– can
temporarily hold the new data). This is because writes are assumed to be data-
race-free, i.e, they are always ordered with respect to conflicting reads
[AH90]. In this case, writes do not require “write permission”.

  * •

After writing in an L1 cache line (e.g., one word), if the data block is
missing it is fetched from the LLC. The block is merged with the written word.
Before merging the data, the cache line is in a transient state and once
merged transitions to dirty.

  * •

An atomic read-modify-write (RMW) request (e.g., test-and-set –TAS–) needs to
reach the LLC, get the data block and send it back to the L1 cache. During
this operation, the corresponding cache line in the LLC is blocked, so no
other RMW request can proceed. When the data arrives at the L1 cache it is
read and possibly modified. If modified, the data is written-back in the LLC,
unblocking the LLC line at the same time. Otherwise the LLC line will be
simply unblocked. This blocking operation —common in other protocols for
directory operations that generate new messages (indirection, invalidations,
etc.)— is only necessary in this protocol for RMW requests. Once the
transaction finishes, the data block remains in the L1 in clean state.

  * •

Evictions of clean cache lines only require a change of state to invalid.
However, evictions of dirty cache lines need to write back to the LLC the data
that have been modified locally. This is necessary to avoid overwriting
unrelated data in the LLC cache line (a different part of the LLC line may
have been modified independently without a conflict). When modified data are
written-back an acknowledgement message is sent to the L1 to signal the
completion of the corresponding writes.

  * •

To keep track of the locally modified data in an L1 cache line, it is
necessary to keep information in the form of a dirty bit per word (byte),
either with the L1 cache lines [CKS+11], or in the write-buffer or MSHRs
[RK12].

###  2.3. Self-Invalidation and Self-Downgrade fences

Since the described protocol has neither invalidation on writes nor downgrades
on reads, we need to ensure that a read operation sees the latest value
written, when this is intended by the program. Typically, the program contains
synchronization to enforce an order between conflicting writes and reads.

In this context, to ensure that a read gets the latest value of a
corresponding write, two things need to happen: first, the data in the
writer’s cache must be self-downgraded and put back in the LLC sometime after
the write but before the read; second, if there is a (stale) copy in the
reader’s cache, it must be self-invalidated sometime before the read. The
self-downgrade and self-invalidation also need to be ordered the same as the
write and read are ordered by synchronization.

Prior proposals [LW95, KK11, CKS+11, SKA13, ADC11, RK12, KR13] invariably
offer SC for data-race-free (DRF) programs [AH90]. In general, such proposals
can be thought of as employing a single fence causing the self-invalidation
and self-downgrade of cached data, _on every synchronization in the DRF
program_ (e.g., [RK12].)

Our approach is fundamentally different. We make no assumption as to what
constitutes synchronization (perhaps ordinary accesses relying on SC
semantics, or algorithms involving atomic RMW operations). We insert _fences_
in a program to cause self invalidation and self downgrade in such a way as to
produce the desired behavior.

With only a single fence, ensuring that a read sees the latest value of a
write causes the self-invalidation _and_ self-downgrade of _both_ the reader’s
and the writer’s cache. In many cases, this is unnecessary.

One of the contributions of our work is to propose two separate fences, which
we call “load-load fence” (llfence) and “store-store fence” (ssfence) to
address the above problem. An llfence self-invalidates only _clean_ data in
the cache (at word level), while an ssfence writes back only _dirty_ data to
the LLC (again at word level), so all the data in the L1 cache of the process
are clean.

The separation of self-invalidation and self-downgrade into two fences affects
performance in two ways: first, we reduce the fence latency when we do not
have to self-downgrade; second, we eliminate extraneous misses (that cost in
performance) when we only need to self-downgrade.

###  2.4. Improving self-invalidation of partially dirty cache lines: the DoI
state

The llfence defined above operates efficiently for cache lines that are
entirely clean, or entirely dirty. In particular, for clean data they take a
single cycle, while for dirty data they do not perform any action. However,
cache lines that contain both clean and dirty words are not self-invalidated
efficiently. Consider, for example, a cache line with one clean word and one
dirty word (its dirty bit is set). The llfence must invalidate the clean word
(if it were to be accessed afterwards), without affecting the dirty word. If
we invalidate the whole cache line we also have to write the dirty data to the
LLC. This would have the same impact (for this cache line) as a single full
fence, and would offer no advantage from using the llfence instead.

In order to improve the efficiency of llfence operations we propose that they
operate at word granularity, being able to self-invalidate the clean words in
a single cycle and leaving untouched the dirty words. Thus, we introduce a new
state for L1 cache lines, called DoI (dirty or invalid), for exactly this
purpose. A cache line in this state contains words that are either dirty (with
the dirty bit set) or invalid (with the dirt bit unset). An llfence
transitions any partially dirty cache line to the DoI state. No write back is
performed for its dirty words. This allows an efficient, one-cycle
implementation of llfence, since now the only necessary action for a llfence
is to change the cache-line state from dirty to DoI.

##  3\. Overview

In this section, we give an informal overview of the main concepts in our
framework. We describe the semantics (configurations and runs) of programs
running under SiSd, the notion of safety properties, the weak memory model
induced by SiSd, the roles of fences, and optimal sets of fences. This will be
formalized in later sections.

data x=0 y=0 z=0process P0registers $r0beginL1: y$x := 1;L2: y$y := 1;L3:
y$$r0 := z;endprocess P1registers $r1$r2 $r3beginL4: z := 1;L5: $r1 := x;L6:
$r2 := y;L7: $r3 := x;end Figure 1. A simple program ${\mathcal{P}}$.

##### Example.

We will use the toy program ${\mathcal{P}}$ in Figure 1 as a running example.
The program is written in a simple assembly-like programming language. The
syntax and semantics of the language are formally defined in Section 4.
${\mathcal{P}}$ consists of two processes P0 and P1 that share three variables
x, y, and z. Process P0 has one register $r0, and process P1 has three
registers $r1, $r2, and $r3. Process P0 has three instructions labeled with
L1, L2, L3, and process P1 has four instructions labeled with L4, L5, L6, L7.

To simplify the presentation, we assume that each cache line holds only one
variable. We also assume that the underlying protocol contains both Si and Sd.
It is straightforward to extend our framework to the case where a cache line
may hold several variables, and to the case where the protocol only contains
one of Si and Sd. In ${\mathcal{P}}$, all the instructions have unique labels.
Therefore, to simplify the presentation, we identify each label with the
corresponding instruction, e.g., L1 and x := 1 in P0.

##### Configurations.

ptx=0y=0z=0ptL1$r0=0ptL4 $r1=0$r2=0 $r3=0$c_{0}$LLCP0P1ptx=0y=0z=0ptL3$r0=0x=1
y=1ptL5 $r1=0$r2=0 $r3=0z=1$c_{1}$ptx=1y=1z=0ptL3$r0=0ptL6 $r1=0$r2=0 $r3=0x=0
z=1$c_{2}$ptx=1y=1z=0ptL3$r0=0ptend $r1=0$r2=1 $r3=0x=0 y=1 z=1 $c_{3}$

ptx=0y=1z=0ptL3$r0=0x=1ptend $r1=0$r2=1 $r3=0x=0 z=1
$c_{4}$LLCP0P1ptx=1y=0z=0ptend $r0=0 y=1 z=0ptend $r1=0$r2=0 $r3=0x=0 z=1
$c_{5}$

Figure 2. Configurations

A configuration is a snapshot of the global state of the system, and consists
of two parts, namely the local and shared parts. The local part defines the
local states of the processes, i.e., it defines for each process: (i) its next
instruction to be executed, (ii) the values stored in its registers, and (iii)
the variables (memory locations) that are currently cached in its L1, together
with their status: invalid, clean, or dirty; and the current value of the
variable in case it is valid. The shared part defines, for each variable, its
value in the LLC. Figure 2 shows different configurations of ${\mathcal{P}}$.
Each configuration is depicted as three fields, representing the LLC, P0, and
P1 respectively. ${\mathcal{P}}$ starts its execution from the initial
configuration $c_{0}$, where the values of all variables are $0$ in the LLC.
P0 and P1 are about to execute the instructions labeled L1 and L4,
respectively. The values of all registers are $0$. None of the variables is
valid in the L1 of the processes. In contrast, in $c_{4}$, the value of y is
$1$ in the LLC. P0 is about to execute the instruction L3, while P1 has ended
its execution. The value of the register $r2 is $1$. The variables x, and z
are valid in the L1 of P1, with values $0$ and $1$ respectively. The variable
z is dirty in the L1 of P1 (marked by underlining z=1), while x is clean (not
underlined). Finally, there is a dirty copy of x with value $1$ in P0.

##### Safety Properties.

Suppose that, together with the program ${\mathcal{P}}$, we are given a safety
property $\phi$ which states that a certain set ${\it Bad}$ of configurations
will not occur during any execution of ${\mathcal{P}}$. For the example, we
assume that ${\it Bad}$ is the set of configurations where (i) P1 has ended
its execution, and (ii) the registers $r2 and $r3 have values $1$ and $0$
respectively. For instance, $c_{3}$ and $c_{4}$ are members of ${\it Bad}$. We
are interested in checking whether ${\mathcal{P}}$ satisfies $\phi$ under the
SiSd semantics. Note that the set ${\it Bad}$ is not reachable in
${\mathcal{P}}$ under SC semantics, which also means that ${\mathcal{P}}$
satisfies $\phi$ under SC.

##### Runs.

The semantics of a program boils down to defining a transition relation on the
set of configurations. The execution of the program can be viewed as a run,
consisting of a sequence of transitions, i.e., events that take the program
from one configuration to another by changing the local states of the
processes and the shared parts. Such a transition will either be performed by
a given process when it executes an instruction, or it occurs due to a system
event. We consider three kinds of system events: ${\tt fetch}$, ${\tt evict}$,
and ${\tt wrllc}$. They model respectively fetching a value from LLC to L1,
invalidating an L1 entry, and writing a dirty L1 entry through to the LLC. The
system events are decoupled from program instructions and execute
independently.

$c_{0}$$\rho_{1}$$c_{1}$L4*L1*L2*$\rho_{2}$$c_{2}$L5*evict*(P0,x) evict*(P0,y)
$\rho_{3}$$c_{3}$L6*L7 Figure 3. The run $\pi_{1}$.

In Figure 3 we show one example run $\pi_{1}$ of ${\mathcal{P}}$. It consists
of three sequences $\rho_{1}$, $\rho_{2}$, $\rho_{3}$ of transitions, and
takes us from $c_{0}$ through $c_{1}$ and $c_{2}$ to $c_{3}$. $\rho_{1}$:
Starting from $c_{0}$, P1 executes L4. Since z is invalid in the L1 of P1, it
is fetched from the LLC. In Figure 3, the star in L4* is to simplify the
notation, and it indicates that the instruction L4 is preceded by fetch
event111In the examples of this section, fetch events always precede read or
write events. In general, fetch events may occur anywhere along the run. of
the process (here P1) on the relevant variable (here z). Consequently, a dirty
copy of z with value $1$ is stored in the L1 of P1. Next, P0 executes L1 and
L2, putting dirty copies (with values $1$) of x and y in its L1, reaching the
configuration $c_{1}$. $\rho_{2}$: P1 executes L5, fetching x from the LLC,
and storing a clean copy with value $0$. P0 evicts the variable x. An evict
event may only be performed on clean variables. To simplify the notation, we
augment the evict event in Figure 3 by a star. This indicates that it is
preceded by an wrllc event on x. The latter updates the value of x to $1$ in
the LLC, and makes x clean in the L1 of P0. Next, P0 evicts y in a similar
manner, thus reaching $c_{2}$. $\rho_{3}$: P1 executes L6. Since y is invalid
in the L1 of P1, it is fetched from the LLC, and stored with value $1$ as
clean. The register $r2 will be assigned the value $1$. Finally, P1 executes
L7. Since x is valid, it need not be fetched from the memory (L7 is therefore
not starred in Figure 3), and hence $r3 is assigned the value $0$. Thus we
reach $c_{3}$, which is in the set ${\it Bad}$. And so ${\mathcal{P}}$
violates the safety property $\phi$ under the SiSd semantics.

##### Weak Memory Model.

Although the configuration $c_{3}$ is not reachable from $c_{0}$ under SC
semantics, we demonstrated above that it is reachable under SiSd semantics.
The reason is that SiSd introduces a weak memory semantics in the form of
reorderings of events. In the case of $\pi_{1}$, we have a read-read
reordering. More precisely, the read event L7 overtakes the read event L6, in
the sense that L6 is issued before L7, but the value assigned to $r2 in L6
(coming from the write on y in L2) is more recent than the value assigned to
$r3 in L7 (which is the initial value of x). To prevent event reorderings, we
use fences. In this paper, we use four types of fences, namely ${\tt
llfence}$, ${\tt ssfence}$, ${\tt fence}$, and ${\tt syncwr}$. In this
section, we only describe the first three types.

data x=0 y=0 z=0process P0registers $r0beginL1: y$x := 1;L2: y$y := 1;L3:
y$$r0 := z;endprocess P1registers $r1$r2 $r3beginL4: z := 1;L5: $r1 := x;L6:
$r2 := y;L8: llfence;L7: $r3 := x;end Figure 4. The program
${\mathcal{P}}_{1}$.
$c_{0}$L1*L2*evict*(P0,y)L4*L5*L6*evict(P1,x)evict(P1,y)L8$c_{4}$L7 Figure 5.
The run $\pi_{2}$.

##### LL Fences.

To forbid the run $\pi_{1}$, we insert an ${\tt llfence}$ between L6 and L7,
obtaining a new program ${\mathcal{P}}_{1}$ (Figure 4). Intuitively, an ${\tt
llfence}$ (load-load-fence) blocks when there are clean entries in the L1 of
the process, and hence forbids the reordering of two read (load) operations.
For instance, in the above example, L8 cannot be executed before x has become
invalid in the L1 of P1, and hence the new value $1$ of x will be assigned to
$r3 in L7. Therefore, ${\mathcal{P}}_{1}$ does not contain the run $\pi_{1}$
any more.

##### SS Fences.

Despite the fact that the insertion of L8 eliminates the run $\pi_{1}$, the
program ${\mathcal{P}}_{1}$ still does not satisfy the safety property $\phi$:
the set ${\it Bad}$ is still reachable from $c_{0}$ in ${\mathcal{P}}_{1}$,
this time through a run $\pi_{2}$ (Figure 5) that leads to the configuration
$c_{4}$ (which is also a member of ${\it Bad}$). In $\pi_{2}$, P0 performs L1
and L2 and then evicts only y, which means that the values of x and y in the
LLC will be $0$ resp. $1$. Now, P1 will perform the instructions L4, L5, L6.
Next P1 evicts x and then y which means that now P1 does not contain any clean
variables, and hence L8 is enabled. Notice that these evict events are not
followed by stars (since they concern clean copies of the variables). Finally,
P1 executes L7. Since x is invalid in the L1 of P0, it is fetched from the LLC
(where its value is $0$ since it was never evicted by P0), and hence $r3 will
be assigned the value $0$. Thus, we are now in $c_{4}$.

data x=0 y=0 z=0process P0registers $r0beginL1: y$x := 1;L9: ssfence;L2: y$y
:= 1;L3: y$$r0 := z;endprocess P1registers $r1$r2 $r3beginL4: z := 1;L5: $r1
:= x;L6: $r2 := y;L7: $r3 := x;end Figure 6. The program ${\mathcal{P}}_{2}$.

Notice again that $\pi_{2}$ is not possible under SC (in the SC semantics,
fences have no effect, so they are equivalent to empty statements). The reason
why $\pi_{2}$ is possible under SiSd is due to a write-write reordering. More
precisely, the write event L1 is issued before the write event L2, but L2
takes effect (updates the LLC) before L1. To forbid the run $\pi_{2}$, we
insert an ${\tt ssfence}$ between L1 and L2, obtaining the program
${\mathcal{P}}_{2}$ (Figure 6). An ${\tt ssfence}$ (store-store-fence) is only
enabled when there are no dirty entries in the L1 of the process. Hence it
forbids the reordering of two write operations. For instance, in the above
example, L9 cannot be executed before x has been evicted by P0, and hence the
value of x in the LLC will be updated to $1$.

$c_{0}$L4*L5*L6*evict(P1,x)evict(P1,y)L8L7*L1*evict*(P0,x)L9L2*$c_{5}$L3*
Figure 7. The run $\pi_{3}$.

In fact, no configuration in ${\it Bad}$ is reachable from $c_{0}$ in
${\mathcal{P}}_{2}$, which means that ${\mathcal{P}}_{2}$ indeed satisfies the
property $\phi$. Thus, we have found a sound set of fences for ${\mathcal{P}}$
w.r.t. $\phi$. It is interesting to observe that, although ${\mathcal{P}}_{2}$
is correct w.r.t. $\phi$, the program still contains runs that are impossible
under SC, e.g., the run $\pi_{3}$ given in Figure 7.

##### Full Fences.

Consider a safety property $\phi^{\prime}$ defined by (unreachability of) a
new set of configurations ${\it Bad}^{\prime}$. The set ${\it Bad}^{\prime}$
contains all configurations in ${\it Bad}$, and also all configurations where
(i) the processes P0 and P1 have both terminated, and (ii) both $r0 and $r3
have values $0$. We show that ${\mathcal{P}}_{2}$ violates $\phi^{\prime}$,
i.e., the set ${\it Bad}^{\prime}$ is reachable from $c_{0}$ in
${\mathcal{P}}_{2}$. To that end, we construct the run $\pi_{3}$, depicted in
Figure 7. (The run can be explained similarly to $\pi_{1}$ and $\pi_{2}$.) At
the end of $\pi_{3}$, we reach the configuration $c_{5}$ which is in ${\it
Bad}^{\prime}$.

Notice that the run $\pi_{3}$ is not possible under SC, while it is feasible
under the SiSd semantics even in the presence of the two fences at L8 and L9.
The reason $\pi_{3}$ is possible under SiSd is write-read reordering. More
precisely, read events may overtake write events (although not the other way
round). In $\pi_{3}$, the write event L4 is issued before the read events L5,
L6, and L7, but L4 does not take effect (does not update the LLC) before the
read events. There are several ways to prevent the reachability of the set
${\it Bad}^{\prime}$. One is to replace the ${\tt llfence}$ at L8 and the
${\tt ssfence}$ at L9 by the full fence ${\tt fence}$, thus obtaining the
program ${\mathcal{P}}_{3}$ (Figure 8). A full fence ${\tt fence}$ is only
enabled when the L1 of the process is empty, and hence it forbids all
reorderings of events of the process. In ${\mathcal{P}}_{3}$, no configuration
in ${\it Bad}^{\prime}$ is reachable from $c_{0}$. Thus we have inserted a
sound set of fences in ${\mathcal{P}}$ w.r.t. the set ${\it Bad}^{\prime}$.

data x=0 y=0 z=0process P0registers $r0beginL1: y$x := 1;L9: fence;L2: y$y :=
1;L3: y$$r0 := z;endprocess P1registers $r1$r2 $r3beginL4: z := 1;L5: $r1 :=
x;L6: $r2 := y;L8: fence;L7: $r3 := x;end Figure 8. The program
${\mathcal{P}}_{3}$.

##### Optimal Sets of Fences.

We will describe some optimal sets of fences for the program ${\mathcal{P}}$.
As we will notice, this task is not trivial even for ${\mathcal{P}}$. Our
framework allows to make use of different kinds of fences. We saw above three
examples of fences (and we introduce another one in Section 4). The motivation
is that different kinds of fences may have different costs. Using a more
“light-weight” fence may both increase program performance and reduce network
traffic (see Section 7). In that respect, the cost of a full fence is higher
than that of an ${\tt llfence}$ or an ${\tt ssfence}$. The cost assignment is
provided by the user of our tool. Let us assume that an ${\tt llfence}$ or an
${\tt ssfence}$ costs 1 unit, and that a full fence costs 2 units. Let $F_{1}$
be the set of fences where there is an ${\tt ssfence}$ after L1, and an ${\tt
llfence}$ after L6. Then, $F_{1}$ is optimal for the program ${\mathcal{P}}$
w.r.t. the property $\phi$. First, $F_{1}$ is sound since ${\mathcal{P}}_{2}$
(which is the result of inserting the two fences in ${\mathcal{P}}$) satisfies
$\phi$, i.e., it does not reach ${\it Bad}$ from $c_{0}$. Second, $F_{1}$ has
the minimal cost that guarantees unreachability of ${\it Bad}$. The set
$F_{2}$ which we get by replacing both the ${\tt llfence}$ and ${\tt ssfence}$
by full fences is also sound. It is also minimal w.r.t. the number of fences
(which is $2$). However, it is not optimal w.r.t. $\phi$ since it has a larger
cost than $F_{1}$. On the other hand, $F_{2}$ is optimal w.r.t. the set
$\phi^{\prime}$. In fact, there are several optimal sets of fences w.r.t.
$\phi^{\prime}$ (12 sets to be exact, as reported by our tool). One such a set
is $F_{3}$ which we get by inserting an ${\tt ssfence}$ after L1, an ${\tt
llfence}$ after L2, and an ${\tt ssfence}$ followed by an ${\tt llfence}$
after L6. The set $F_{3}$ is not minimal w.r.t. the number of fences, but
optimal w.r.t. the property $\phi^{\prime}$. Notice that there are at least
$2^{15}$ ways to insert three types of fences in the simple program of Figure
1. (Each type may or may not be inserted in any particular position.)

##  4\. Programs – Syntax and Semantics

In this section, we formalize SiSd and Si protocols, by introducing a simple
assembly-like programming language, and defining its syntax and semantics.

###  4.1. Syntax

The syntax of programs is given by the grammar in Figure 9. A program has a
finite set of processes which share a number of variables (memory locations)
$\mathcal{M}$. A variable $x\in\mathcal{M}$ should be interpreted as one
machine word at a particular memory address. For simplicity, we assume that
all the variables and process registers take their values from a common finite
domain ${\mathcal{V}}$ of values. Each process contains a sequence of
instructions, each consisting of a program label and a statement. To simplify
the presentation, we assume that all instructions (in all processes) have
unique labels. For a label $\lambda$, we apply three functions: ${\sf
Proc}\left(\lambda\right)$ returns the process $p$ in which the label occurs.
${\sf Stmt}\left(\lambda\right)$ returns the statement whose label id is
$\lambda$. ${\sf Next}\left(\lambda\right)$ returns the label of the next
statement in the process code, or ${\tt end}$ if there is no next statement.

$\begin{array}[]{@{}r@{\;}c@{\;}l@{}}\langle{\it{pgm}}\rangle&::=&\tt{data}\;{\langle{\it{vdecl}}\rangle}^{+}{\langle{\it{proc}}\rangle}^{+}\\\
\\\
\langle{\it{vdecl}}\rangle&::=&\langle{\it{var}}\rangle\;\textrm{\textquotesingle}{=}\textrm{\textquotesingle}\;\left(\textrm{\textquotesingle}{*}\textrm{\textquotesingle}\;|\;\langle{\it{val}}\rangle\right)\\\
\\\
\langle{\it{proc}}\rangle&::=&\tt{process}\;\langle{\it{pid}}\rangle\;\par\tt{registers}\;{\langle{\it{reg}}\rangle}^{*}\;\langle{\it{stmts}}\rangle\\\
\\\
\langle{\it{stmts}}\rangle&::=&\tt{begin}\;{(\langle{\it{label}}\rangle\;\textrm{\textquotesingle}{:}\textrm{\textquotesingle}\;\langle{\it{stmt}}\rangle\;\textrm{\textquotesingle}{;}\textrm{\textquotesingle})}^{+}\;\tt{end}\\\
\\\
\langle{\it{stmt}}\rangle&::=&\langle{\it{var}}\rangle\;\textrm{\textquotesingle}{:=}\textrm{\textquotesingle}\;\langle{\it{expr}}\rangle\;\;\;|\;\;\;\langle{\it{reg}}\rangle\;\textrm{\textquotesingle}{:=}\textrm{\textquotesingle}\;\langle{\it{var}}\rangle\;\;\;|\\\
&&\langle{\it{reg}}\rangle\;\textrm{\textquotesingle}{:=}\textrm{\textquotesingle}\;\langle{\it{expr}}\rangle\;\;\;\;|\;\;\;\tt{llfence}\;\;\;|\;\;\;\tt{fence}\;\;\;|\\\
&&\tt{cas}\;\textrm{\textquotesingle}{(}\textrm{\textquotesingle}\;\langle{\it{var}}\rangle\;\textrm{\textquotesingle}{,}\textrm{\textquotesingle}\;\langle{\it{expr}}\rangle\;\textrm{\textquotesingle}{,}\textrm{\textquotesingle}\;\langle{\it{expr}}\rangle\;\textrm{\textquotesingle}{)}\textrm{\textquotesingle}\;\;\;|\\\
&&\tt{syncwr}\;\textrm{\textquotesingle}{:}\textrm{\textquotesingle}\;\langle{\it{var}}\rangle\;\textrm{\textquotesingle}{:=}\textrm{\textquotesingle}\;\langle{\it{expr}}\rangle\;\;\;|\;\;\;\tt{ssfence}\;\;\;|\\\
&&\tt{cbranch}\;\textrm{\textquotesingle}{(}\textrm{\textquotesingle}\;\langle{\it{bexpr}}\rangle\;\textrm{\textquotesingle}{)}\textrm{\textquotesingle}\;\langle{\it{label}}\rangle\\\
\end{array}$
Figure 9. The grammar of concurrent programs.
$\begin{array}[]{@{}r@{\;}c@{\;}l@{}}$c$&:&\mbox{(${\sf LConf},{\sf LLC})$}\\\
\\\ ${\sf LConf}$&:&\mbox{for each process $p$, returns the local
configuration of $p$}\\\ \\\ \mbox{$(\lambda,{\sf RVal},{\sf
L1})$}&:&\mbox{Local configuration of $p$}\\\ \\\ \mbox{$\lambda$}&:&\mbox{the
label of the next statement to execute in $p$}\\\ \\\ \mbox{${\sf
RVal}$}&:&\mbox{the values of the local registers in $p$}\\\ \\\ \mbox{${\sf
L1}$}&:&\mbox{$({\sf Valid},{\sf LStatus},{\sf LVal})$, the state of the L1
cache of $p$}\\\ \\\ \mbox{${\sf Valid}\subseteq\mathcal{M}$}&:&\mbox{the set
of shared variables currently in the valid state}\\\ \\\ \mbox{${\sf
LStatus}:{\sf Valid}\to\\{{\tt dirty},{\tt clean}\\}$}&:&\mbox{for each
$x\in{\sf Valid}$, whether $x$ is dirty or clean}\\\ \\\ \mbox{${\sf
LVal}:{\sf Valid}\to{\mathcal{V}}$}&:&\mbox{for each $x\in{\sf Valid}$, its
current value in the L1 cache of $p$}\\\ \\\
\mbox{LLC$:\mathcal{M}\to{\mathcal{V}}$}&:&\mbox{shared part of $c$, defines
for each $x\in\mathcal{M}$ its value in the LLC}\par\\\ \end{array}$ Figure
10. The definition of a configuration $c$

###  4.2. Configurations

As illustrated in Figure 10, a local configuration of a process $p$ is a
triple $(\lambda,{\sf RVal},{\sf L1})$, where $\lambda$ is the label of the
next statement to execute in $p$, ${\sf RVal}$ defines the values of the local
registers, and ${\sf L1}$ defines the state of the L1 cache of $p$. In turn,
${\sf L1}$ is a triple $({\sf Valid},{\sf LStatus},{\sf LVal})$. Here ${\sf
Valid}\subseteq\mathcal{M}$ defines the set of shared variables that are
currently in the valid state, and ${\sf LStatus}$ is a function from ${\sf
Valid}$ to the set $\\{{\tt dirty},{\tt clean}\\}$ that defines, for each
$x\in{\sf Valid}$, whether $x$ is dirty or clean, and ${\sf LVal}$ is a
function from ${\sf Valid}$ to ${\mathcal{V}}$ that defines for each $x\in{\sf
Valid}$ its current value in the L1 cache of $p$. The shared part of a
configuration is given by a function ${\sf LLC}$ that defines for each
variable $x\in\mathcal{M}$ its value ${\sf LLC}(x)$ in the LLC. A
configuration $c$ then is a pair $({\sf LConf},{\sf LLC})$ where ${\sf LConf}$
is a function that returns, for each process $p$, the local configuration of
$p$. In the formal definition below, our semantics allows system events to
occur non-deterministically. This means that we model not only instructions
from the program code itself, but also events that are caused by unpredictable
things as hardware prefetching, software prefetching, program preemption,
false sharing, multiple threads of the same program being scheduled on the
same core, etc.

A transition $t$ is either performed by a given process when it executes an
instruction, or is a system event. In the former case, $t$ will be of the form
$\lambda$, i.e., $t$ models the effect of a process $p$ performing the
statement labeled with $\lambda$. In the latter case, $t$ will be equal to
$\omega$ for some system event $\omega$. For a function $f$, we use
$f\left[{a}\leftarrow{b}\right]$, to denote the function $f^{\prime}$ such
that $f^{\prime}(a)=b$ and $f^{\prime}(a^{\prime})=f(a^{\prime})$ if
$a^{\prime}\neq a$. We write $f(a)=\bot$ to denote that $f$ is undefined for
$a$.

Below, we give an intuitive explanation of each transition. The formal
definition can be found in Figure 11 where we assume $c=\left({\sf LConf},{\sf
LLC}\right)$, and ${\sf LConf}(p)=(\lambda,{\sf RVal},{\sf L1})$, and ${\sf
L1}=({\sf Valid},{\sf LStatus},{\sf LVal})$, ${\sf
Proc}\left(\lambda\right)=p$, and ${\sf Stmt}\left(\lambda\right)=\sigma$. We
leave out the definitions for local instructions, since they have standard
semantics.

###  4.3. Semantics

####  4.3.1. Instruction Semantics.

Let $p$ be one of the processes in the program, and let $\lambda$ be the label
of an instruction in $p$ whose statement is $\sigma$. We will define a
transition relation $\stackrel{{\scriptstyle\lambda}}{{\longrightarrow}}$,
induced by $\lambda$, on the set of configurations. The relation is defined in
terms of the type of operation performed by the given statement $\sigma$. In
all the cases only the local state of $p$ and LLC will be changed. The local
states of the rest of the processes will not be affected. This mirrors the
principle in SiSd that L1 cache controllers will communicate with the LLC, but
never directly with other L1 caches.

Read $(\$r:=x)$: Process $p$ reads the value of $x$ from L1 into the register
$\$r$. The L1 and the LLC will not change. The transition is only enabled if
$x$ is valid in the L1 cache of $p$. This means that if $x$ is not in L1, then
a system event ${\tt fetch}$ must occur before $p$ is able to execute the read
operation.

Write $(x:=e)$: An expression $e$ contains only registers and constants. The
value of $x$ in L1 is updated with the evaluation of $e$ where registers have
values as indicated by ${\sf RVal}$, and $x$ becomes dirty. The write is only
enabled if $x$ is valid for $p$.

Fence $({\tt fence})$: A full fence transition is only enabled when the L1 of
$p$ is empty. This means that before the fence can be executed, all entries in
its L1 must be evicted (and written to the LLC if dirty). So $p$ must stall
until the necessary system events (${\tt wrllc}$ and ${\tt evict}$) have
occurred. Executing the fence has no further effect on the caches.

$\begin{array}[]{@{}c@{}}\textbf{Instruction Semantics}\\\ \\\
\textrm{\footnotesize$c=\left({\sf LConf},{\sf LLC}\right)$, ${\sf
LConf}(p)=(\lambda,{\sf RVal},{\sf L1})$,}\\\ \textrm{\footnotesize${\sf
L1}=({\sf Valid},{\sf LStatus},{\sf LVal})$, ${\sf
Proc}\left(\lambda\right)=p$, ${\sf Stmt}\left(\lambda\right)=\sigma$}\\\ \\\
{\displaystyle\frac{\sigma=(\$r:=x)\;,\;x\in{\sf
Valid}}{c\stackrel{{\scriptstyle\lambda}}{{\longrightarrow}}\left({\sf
LConf}\left[{p}\leftarrow{\left({\sf Next}\left(\lambda\right),{\sf
RVal}\left[{\$r}\leftarrow{{\sf LVal}(x)}\right],{\sf L1}\right)}\right],{\sf
LLC}\right)}}\\\ \\\ \frac{\sigma=(x:=e)\;,\;x\in{\sf
Valid}\;}{c\stackrel{{\scriptstyle\lambda}}{{\longrightarrow}}\left({\sf
LConf}\left[{p}\leftarrow{\left({\sf Next}\left(\lambda\right),{\sf
RVal},\left({\sf Valid},{\sf LStatus}\left[{x}\leftarrow{{\tt
dirty}}\right],{\sf LVal}\left[{x}\leftarrow{{\sf
RVal}(e)}\right]\right)\right)}\right],{\sf LLC}\right)}\\\ \\\
{\displaystyle\frac{\sigma={\tt fence}\;,\;{\sf
Valid}=\varnothing}{c\stackrel{{\scriptstyle\lambda}}{{\longrightarrow}}\left({\sf
LConf}\left[{p}\leftarrow{\left({\sf Next}\left(\lambda\right),{\sf RVal},{\sf
L1}\right)}\right],{\sf LLC}\right)}}\\\ \\\ {\displaystyle\frac{\sigma={\tt
ssfence}\;,\;\forall x\in\mathcal{M}.\;\left(x\in{\sf Valid}\Rightarrow{\sf
LStatus}(x)={\tt
clean}\right)}{c\stackrel{{\scriptstyle\lambda}}{{\longrightarrow}}\left({\sf
LConf}\left[{p}\leftarrow{\left({\sf Next}\left(\lambda\right),{\sf RVal},{\sf
L1}\right)}\right],{\sf LLC}\right)}}\\\ \\\ {\displaystyle\frac{\sigma={\tt
llfence}\;,\;\forall x\in\mathcal{M}.\;\left(x\in{\sf Valid}\Rightarrow{\sf
LStatus}(x)={\tt
dirty}\right)}{c\stackrel{{\scriptstyle\lambda}}{{\longrightarrow}}\left({\sf
LConf}\left[{p}\leftarrow{\left({\sf Next}\left(\lambda\right),{\sf RVal},{\sf
L1}\right)}\right],{\sf LLC}\right)}}\\\ \\\ {\displaystyle\frac{\sigma=({\tt
syncwr}:x\hskip 2.0pt{\tt:=}\hskip 2.0pte)\;,\;x\not\in{\sf
Valid}}{c\stackrel{{\scriptstyle\lambda}}{{\longrightarrow}}\left({\sf
LConf}\left[{p}\leftarrow{\left({\sf Next}\left(\lambda\right),{\sf RVal},{\sf
L1}\right)}\right],{\sf LLC}\left[{x}\leftarrow{{\sf
RVal}(e)}\right]\right)}}\\\ \\\ {\displaystyle\frac{\sigma={\tt
cas}(x,e_{0},e_{1})\;,\;x\not\in{\sf Valid}\;,\;{\sf LLC}(x)={\sf
RVal}(e_{0})}{c\stackrel{{\scriptstyle\lambda}}{{\longrightarrow}}\left({\sf
LConf}\left[{p}\leftarrow{\left({\sf Next}\left(\lambda\right),{\sf RVal},{\sf
L1}\right)}\right],{\sf LLC}\left[{x}\leftarrow{{\sf
RVal}(e_{1})}\right]\right)}}\\\ \\\ {\displaystyle\frac{\sigma=({\tt
cbranch}(e)\;\lambda^{\prime}),\;{\sf RVal}(e)={\tt
true}}{c\stackrel{{\scriptstyle\lambda}}{{\longrightarrow}}\left({\sf
LConf}\left[{p}\leftarrow{\left(\lambda^{\prime},{\sf RVal},{\sf
L1}\right)}\right],{\sf LLC}\right)}}\\\ \\\ {\displaystyle\frac{\sigma=({\tt
cbranch}(e)\;\lambda^{\prime}),\;{\sf RVal}(e)={\tt
false}}{c\stackrel{{\scriptstyle\lambda}}{{\longrightarrow}}\left({\sf
LConf}\left[{p}\leftarrow{\left({\sf Next}\left(\lambda\right),{\sf RVal},{\sf
L1}\right)}\right],{\sf LLC}\right)}}\\\ \\\ \textbf{System Event
Semantics}\\\ \\\ {\displaystyle\frac{\omega=({\tt
fetch}({p,x}))\;,\;x\not\in{\sf
Valid}\;}{c\stackrel{{\scriptstyle\omega}}{{\longrightarrow}}\left({\sf
LConf}\left[{p}\leftarrow{\left(\lambda,{\sf RVal},\left({\sf
Valid}\cup\\{x\\},{\sf LStatus}\left[{x}\leftarrow{{\tt clean}}\right],{\sf
LVal}\left[{x}\leftarrow{{\sf LLC}(x)}\right]\right)\right)}\right],{\sf
LLC}\right)}}\\\ \\\ {\displaystyle\frac{\omega=({\tt
wrllc}({p,x}))\;,\;x\in{\sf Valid}\;,\;{\sf LStatus}(x)={\tt
dirty}\;}{c\stackrel{{\scriptstyle\omega}}{{\longrightarrow}}\left({\sf
LConf}\left[{p}\leftarrow{\left(\lambda,{\sf RVal},\left({\sf Valid},{\sf
LStatus}\left[{x}\leftarrow{{\tt clean}}\right],{\sf
LVal}\right)\right)}\right],{\sf LLC}\left[{x}\leftarrow{{\sf
LVal}(x)}\right]\right)}}\\\ \\\ {\displaystyle\frac{\omega=({\tt
evict}({p,x}))\;,\;x\in{\sf Valid}\;,\;{\sf LStatus}(x)={\tt
clean}}{c\stackrel{{\scriptstyle\omega}}{{\longrightarrow}}\left({\sf
LConf}\left[{p}\leftarrow{\left(\lambda,{\sf RVal},\left({\sf
Valid}\setminus\\{x\\},{\sf LStatus}\left[{x}\leftarrow{\bot}\right],{\sf
LVal}\left[{x}\leftarrow{\bot}\right]\right)\right)}\right],{\sf
LLC}\right)}\par}\end{array}$

Figure 11. Semantics of programs running under SiSd.

SS-Fence $({\tt ssfence})$: Similarly, an ${\tt ssfence}$ transition is only
enabled when there are no dirty entries in the L1 cache of $p$. So $p$ must
stall until all dirty entries have been written to the LLC by ${\tt wrllc}$
system events. In contrast to a full fence, an ${\tt ssfence}$ permits clean
entries to remain in the L1.

LL-Fence $({\tt llfence})$: This is the dual of an SS-Fence. An ${\tt
llfence}$ transition is only enabled when there are no clean entries in the L1
cache of $p$. In other words, the read instructions before and after an ${\tt
llfence}$ cannot be reordered.

Synchronized write $({\tt syncwr}:x\hskip 2.0pt{\tt:=}\hskip 2.0pte)$: A
synchronized write is like an ordinary write, but acts directly on the LLC
instead of the L1 cache. For a ${\tt syncwr}$ transition to be enabled, $x$
may not be in the L1. (I.e., the cache must invalidate $x$ before executing
the ${\tt syncwr}$.) When it is executed, the value of $x$ in the LLC is
updated with the evaluation of the expression $e$ under the register valuation
${\sf RVal}$ of $p$. The L1 cache is not changed.

CAS $({\tt cas}(x,e_{0},e_{1}))$: A compare and swap transition acts directly
on the LLC. The ${\tt cas}$ is only enabled when $x$ is not in the L1 cache of
$p$, and the value of $x$ in the LLC equals $e_{0}$ (under ${\sf RVal}$). When
the instruction is executed, it atomically writes the value of $e_{1}$
directly to the LLC in the same way as a synchronized write would.

####  4.3.2. System Event Semantics.

The system may non-deterministically (i.e., at any time) perform a system
event. A system event is not a program instruction, and so will not change the
program counter (label) of a process. We will define a transition relation
$\stackrel{{\scriptstyle\omega}}{{\longrightarrow}}$, induced by the system
event $\omega$. There are three types of system events as follows.

Eviction $({\tt evict}({p,x}))$: An ${\tt evict}({p,x})$ system event may
occur when $x$ is valid and clean in the L1 of process $p$. When the event
occurs, $x$ is removed from the L1 of $p$.

Write-LLC $({\tt wrllc}({p,x}))$: If the entry of $x$ is dirty in the L1 of
$p$, then a ${\tt wrllc}({p,x})$ event may occur. The value of $x$ in the LLC
is then updated with the value of $x$ in the L1 of $p$. The entry of $x$ in
the L1 of $p$ becomes clean.

Fetch $({\tt fetch}({p,x}))$: If $x$ does not have an entry in the L1 of $p$,
then $p$ may fetch the value of $x$ from the LLC, and create a new, clean
entry with that value for $x$ in its L1.

###  4.4. Program Semantics under an SI Protocol

In a self-invalidation protocol without self-downgrade, a writing process will
be downgraded and forced to communicate its dirty data when another process
accesses that location in the LLC. This behavior can be modelled by a
semantics where writes take effect atomically with respect to the LLC. Hence,
to modify the semantics given in Section 4.3 such that it models a program
under an Si protocol, it suffices to interpret all write instructions as the
corresponding ${\tt syncwr}$ instructions.

###  4.5. Transition Graph and the Reachability Algorithm

Our semantics allows to construct, for a given program ${\mathcal{P}}$, a
finite transition graph, where each node in the graph is a configuration in
${\mathcal{P}}$, and each edge is a transition. Figure 12 shows four nodes in
the transition graph of the program in Figure 1. The configurations $c_{2}$
and $c_{3}$ are those depicted in Figure 2, while $c_{6}$ is the configuration
we get from $c_{2}$ by adding a clean copy of y with value $1$ to the L1 of
P1; and $c_{7}$ is the configuration we get from $c_{6}$ by updating the label
of P1 to L7, and the value of $r2 to $1$. A run is a sequence
$c_{0}\stackrel{{\scriptstyle
t_{1}}}{{\longrightarrow}}c_{1}\stackrel{{\scriptstyle
t_{2}}}{{\longrightarrow}}c_{2}\cdots\stackrel{{\scriptstyle
t_{n}}}{{\longrightarrow}}c_{n}$, which is a path in the transition graph,
where $t_{i}(0\leq{}i\leq{}n)$ is either a label $\lambda$ or a system event
$\omega$. Figure 12 shows the path of the run $\rho_{3}$.

$c_{2}$$c_{6}$$c_{7}$$c_{3}$fetch(P1,y)L6L7 Figure 12. Part of the transition
graph of the program in Figure 1.

Together with the program, the user provides a safety property $\phi$ that
describes a set ${\it Bad}$ of configurations that are considered to be
errors. Checking $\phi$ for a program ${\mathcal{P}}$ amounts to checking
whether there is a run leading from the initial configuration to a
configuration in ${\it Bad}$. To do that, the input program under SiSd is
translated to the code recognized by the reachability analysis tool chosen by
the user. The translated code simulates all the behaviors which are allowed in
the SiSd semantics. Also, there is instrumentation added to simulate the
caches. Verifying the input program amounts to verifying the translated code
which is analyzed under SC. If a bad configuration is encountered, a witness
run is returned by the tool. Otherwise, the program is declared to be correct.

##  5\. Litmus Tests and Comparison with Other Memory Models

In this section, we will first compare the behavior of SiSd with other weak
memory models. We do this by presenting a sequence of litmus tests that
differentiate the SiSd semantics from the other models. Each program consists
of a number of threads that share a number of variables. Later, we will
describe a number of additional litmus tests to clarify the bahavior of the
SiSd model.

###  5.1. Comparing with Other Memory Models

##### Sequential Consistency (SC)

The SiSd model is weaker than SC. Consider the classic SB (Dekker’s) algorithm
shown in Figure 13. Under the SC semantics, the program does not have any runs
satisfying the assertion, since the operations performed by the process $P0$
are not reordered. If $\$r_{1}=0$, then $x:=1$ must have been executed and the
value 1 of $x$ is updated to the memory. At this time, $P0$ sees the value of
y as 0 in the memory, which means that $y:=1$ is not executed by $P1$ yet.
When $P1$ executes $y:=1$ and $\$r_{2}:=x$, the value of $x$ in the memory is
already $1$ and thus $1$ is assigned to $\$r_{2}$.

Any run of a program ${\mathcal{P}}$ under SC can be simulated by a run of
${\mathcal{P}}$ under SiSd as the following: 1) right after each write
operation, the assigned value of the variable is updated to LLC and the
variable is invalidated from the local cache immediately; 2) right before each
read operation, the value of the variable is fetched from LLC and after
reading the value, the variable is immediately invalidated from the local
cache.

Initially: x=0, y=0process P0registers $r1beginL1: y$x := 1;L2: y$$r1 :=
y;endprocess P1registers $r2beginL3: y := 1;L4: $r2 := x;endAssertion: $r1=0,
$r2=0 Figure 13. SB (Dekker’s) algorithm.

##### Total Store Order (TSO)

The SiSd model and TSO are not comparable. As illustrated in Figure 14, the
TSO model inserts a store buffer between each process and the shared memory.
When a process executes a write instruction, the instruction is appended to
the end of the buffer of the process. At any point of the execution, the
instruction at the head of the buffer may nondeterministically be removed and
applied to update the memory. When a process reads the value of a variable, it
fetches the value from the most recent write operation on the variable in its
buffer. If such a write operation is missing, then the value is fetched from
the memory.

Figure 14. TSO Initially: x=0, y=0process P0registersbeginL1: y$x := 1;L2: y$y
:= 1;endprocess P1registers $r1 $r2beginL3: $r1 := x;L4: $r2 :=
y;endAssertion: $r1=0, $r2=1 Figure 15. Program MP.

First, we show that TSO is not weaker than SiSd. Consider the program MP in
Figure 15. Under the TSO semantics, the program MP does not have any runs that
satisfy the assertion. The reason is that the two write operations performed
by $P0$ will reach the memory in the same order as they are performed, i.e,
$x:=1$ and then $y:=1$. Furthermore, the two read operations performed by $P1$
are not re-ordered according to the TSO semantics. Therefore, if $\$r_{2}=1$
then $P1$ has already seen that the value of $x$ is equal to $1$ when it
performs the assignment $\$r_{1}:=x$. In contrast, the program MP has the
following run under SiSd that satisfies the assertion. First, the process $P0$
assigns $1$ to $x$ and $y$ respectively, but only updates the value of $y$ to
the LLC. Next, $P1$ fetches the values of $x$ and $y$ ($0$ and $1$
respectively) from the LLC, and assigns them to the registers using the
instructions $\$r_{1}:=x$ and $\$r_{2}:=y$, which means the assertion will be
satisfied.

Initially: x=0, y=0process P0registers $r1$r2 $r3 $r4beginL1: y$x := 1;L2: y$x
:= 2;L3: y$x := 3;L4: y$x := 4;L5: y$$r1 := y;L6: y$$r2 := y;L7: y$$r3 :=
y;L8: y$$r4 := y;endprocess P1registers $r5$r6 $r7 $r8beginL9: y := 1;L10: y
:= 2;L11: y := 3;L12: y := 4;L13: $r5 := x;L14: $r6 := x;L15: $r7 := x;L16:
$r8 := x;endAssertion:$r1=1, $r2=2, $r3=3, $r4=4,$r5=1, $r6=2, $r7=3, $r8=4
Figure 16. Program ReadSeq.

The program ReadSeq in Figure 16 shows that SiSd is not weaker than TSO. Under
TSO, the program exhibits a run that satisfies the assertion as follows.
First, $P0$ executes the instructions $x:=1$, $x:=2$, $x:=3$, and $x:=4$, one
by one, and the corresponding operations are put in its buffer. Then, $P1$
executes the instructions $y:=1$, $y:=2$, $y:=3$, and $y:=4$, one by one,
again putting the corresponding operations in its buffer. Now, the memory is
updated with $x:=1$ after which $P1$ executes $\$r_{5}:=x$, thus assigning $1$
to $\$r_{5}$. Following this, the memory is updated with $x:=2$ after which
$P1$ executes $\$r_{6}:=x$, thus assigning $2$ to $\$r_{6}$. Finally $3$ and
$4$ are assigned to $\$r_{7}$ and $\$r_{8}$ respectively in similar manners. A
similar sequence of operations is performed assigning $1$, $2$, $3$ and $4$ to
$\$r_{1}$, $\$r_{2}$, $\$r_{3}$, and $\$r_{4}$ respectively.

However, under the SiSd semantics, the ReadSeq program does not have any runs
that can satisfy the assertion. More specifically, since the processes do not
have any store buffers, at most three different values of a variable can be
kept in this example. I.e., one in the local cache of the process which
executes the write operation of the variable, one in the local cache of the
process which executes the read operation of the variable, and one in the LLC.
When there are four or more values assigned to a variable in a similar manner
as in ReadSeq, the assertion that each process reads all the values of the
variable in the same order as it is written by the other process cannot be
satisfied.

Figure 17. PSO

##### Partial Store Order (PSO)

The SiSd model and PSO are not comparable. In PSO, a store buffer is inserted
for each variable, between each process and the shared memory as illustrated
in Figure 17 .

Initially: x=0, y=0process P0registersbeginL1: y$x := 1;endprocess P1registers
$r1beginL2: $r1 := x;L3: y := 1;endprocess P2registers $r2 $r3beginL4: $r2 :=
y;L5: $r3 := x;endAssertion: $r1=1, $r2=1, $r3=0 Figure 18. Program WRC.

To illustrate the difference between SiSd and PSO, we consider the program WRC
in Figure 18. Under the PSO semantics, the program WRC does not have any runs
that satisfy the assertion. More precisely, if $\$r_{1}=1$ then the write
operation $x:=1$ by $P0$ must have reached the memory before the write
operation $y:=1$ has been performed by $P2$. Furthermore, if $\$r_{2}=1$ holds
then the write operation $y:=1$ must have reached the memory before the
instruction $\$r_{3}:=x$ has been performed by $P2$. Since read instructions
are not re-ordered in PSO and since $x:=1$ reaches the memory before $y:=1$ it
follows that the value of $x$ is equal to $1$ in the memory when $\$r_{3}:=x$
is performed by $P2$, and hence $\$r_{3}=1$.

The program WRC has the following run under SiSd that satisfies the assertion.
The process $P2$ fetches the initial value $0$ of the variable $x$. The
process $P0$ assigns $1$ to $x$ and updates the value to the LLC. The process
$P1$ fetches the value $1$ of $x$ from the LLC and then executes the
instruction $\$r_{1}:=x$ which means that the value of $\$r_{1}$ is equal to
$1$. Then, $P1$ assigns the value $1$ to the variable $y$ and updates the
value to the LLC. The process $P2$ fetches the value of $y$ from the LLC and
then executes the instruction $\$r_{2}:=y$ which means that $\$r_{2}=1$.
Finally, $P2$ executes the instruction $\$r_{3}:=x$ and we get $\$r_{3}=0$.

As PSO is weaker than TSO, we can use the same example in Figure 16 to show
that the ReadSeq program also has a run under PSO satisfying the assertion,
which means that SiSd is not weaker than PSO.

##### POWER/ARM

The SiSd model and POWER are not comparable. We show that the POWER memory
model is not weaker than SiSd with the program PwrEg in Figure 19. The program
does not have any runs that satisfy the assertion under POWER, since cycles of
the form write-(sync)$\rightarrow$write-(read from)$\rightarrow$ read-(address
dependency)$\rightarrow$read-(from read)$\rightarrow$ are not allowed by
POWER. The sync instruction maintains the order between the two write
instructions and the address dependency maintains the order between the two
read instructions, which make the cycle impossible.

Initially: x=0, y=0process P0registers beginL1: y$x := 1;L2: sync;L3: y$y :=
1;endprocess Pregisters $r1 $r2beginL4: $r1 := y;L5: $r2 := (&x +
0*$r1);endAssertion: $r1=1, $r2=0 Figure 19. PwrEg Initially: x=0, y=0process
P0registers beginL1: y$x := 1;L2: fence;L3: y$y := 1;endprocess P1registers
$r1 $r2beginL4: $r1 := y;L5: $r2 := x;endAssertion: $r1=1, $r2=0 Figure 20.
SisdEg

However, under SiSd the program SisdEg in Figure 20 has the run that satisfies
the assertion. The process $P1$ fetches the initial value 0 of the variable
$x$. The process $P0$ assigns 1 to $x$, updates the value to the LLC, assigns
1 to $y$, and updates the value to the LLC again. The process $P1$ fetches the
value 1 of $y$ from the LLC and then executes the instruction $\$r_{1}:=y$.
Therefore, the value of $\$r_{1}$ is equal to 1. Finally, $P1$ executes the
instruction $\$r_{2}:=x$ and we get $\$r_{2}=0$.

We can show that SiSd is not weaker than POWER with the program ReadSeq in
Figure 16.

We can also show that the SiSd model and ARM are not comparable with the
programs in Figure 16, Figure 19 and Figure 20.

##### Relaxed Memory Order (RMO)

We can show that SiSd is not weaker than RMO again with the program ReadSeq in
Figure 16, since RMO allows the reorder between both 1) write and write
operations and 2) read and read/write operations.

We keep the other direction open since we have not found any examples as the
proof.

###  5.2. Further Litmus Tests

We describe the behavior of the SiSd model for three more litmus tests.

##### Load-Buffering (LB)

The LB program in Figure 21 does not have any runs that can satisfy the
assertion under SiSd. If $\$r_{1}=1$, then process $P1$ must have executed the
write instruction $x:=1$ and updated the value 1 of $x$ to the LLC before $P0$
has executed the instruction $\$r_{1}:=x$. This means when $P1$ executes the
read instruction $\$r_{2}:=y$, the value of $y$ has not been updated by $P0$,
and thus $\$r_{2}=0$.

Initially: x=0, y=0process P0registers $r1beginL1: y$$r1 := x;L2: y$y :=
1;endprocess P1registers $r2beginL3: $r2 := y;L4: x := 1;endAssertion: $r1=1,
$r2=1 Figure 21. Program LB.

##### ISA2

The program ISA2 in Figure 22 has the following run under SiSd that satisfies
the assertion. The process $P2$ fetches the initial value $0$ of the variable
$x$. The process $P0$ assigns $1$ to $x$ and $y$, and updates the value to the
LLC. The process $P1$ fetches the value $1$ of $y$ from the LLC and then
executes the instruction $\$r_{1}:=y$, which means that the value of $\$r_{1}$
is equal to $1$. Then, $P1$ assigns the value $1$ to the variable $z$ and
updates the value to the LLC. The process $P2$ fetches the value of $z$ from
the LLC and then executes the instruction $\$r_{2}:=z$, which means that
$\$r_{2}=1$. Finally, $P2$ executes the instruction $\$r_{3}:=x$ and we get
$\$r_{3}=0$.

Initially: x=0, y=0, z=0process P0registersbeginL1: y$x := 1;L2: y$y :=
1;endprocess P1registers $r1beginL3: $r1 := y;L4: z := 1;endprocess
P2registers $r2 $r3beginL5: $r2 := z;L6: $r3 := x;endAssertion: $r1=1, $r2=1,
$r3=0 Figure 22. Program ISA2.

##### IRIW

The program IRIW in Figure 23 has the following run under SiSd that satisfies
the assertion. The processes $P1$ and $P3$ fetch the initial values $0$ of the
variables $y$ and $x$ respectively. The process $P0$ assigns $1$ to $x$ and
updates the values to the LLC. The process $P1$ fetches the value $1$ of $x$
from the LLC and executes the instruction $\$r_{1}:=x$, which means that the
value of $\$r_{1}$ is equal to $1$. Then $P1$ executes the instruction
$\$r_{2}:=y$, which means that $\$r_{2}=0$. After that, the process $P2$
assigns the value $1$ to the variable $y$ and updates the value to the LLC.
The process $P3$ fetches the value of $y$ from the LLC and then executes the
instruction $\$r_{3}:=y$, which means that $\$r_{3}=1$. Finally, $P3$ executes
the instruction $\$r_{4}:=x$ and we get $\$r_{4}=0$.

Initially: x=0, y=0process P0registersbeginL1: y$x := 1;endprocess P1registers
$r1 $r2beginL2: $r1 := x;L3: $r2 := y;endprocess P2registersbeginL4: y :=
1;endprocess P3registers $r3 $r4beginL5: $r3 := y;L6: $r4 := x;endAssertion:
$r1=1, $r2=0, $r3=1, $r4=0 Figure 23. Program IRIW.

##  6\. Fence Insertion

In this section we describe our fence insertion procedure, which is closely
related to the algorithm described in [LNP+12]. Given a program
${\mathcal{P}}$, a cost function $\kappa$ and a safety property $\phi$, the
procedure finds all the sets of fences that are optimal for ${\mathcal{P}}$
w.r.t. $\phi$ and $\kappa$.

In this section we take _fence constraint_ (or _fence_ for short) to mean a
pair $(\lambda,f)$ where $\lambda$ is a statement label and $f$ is a fence
instruction. A fence constraint $(\lambda,f)$ should be interpreted as the
notion of inserting the fence instruction $f$ into a program, between the
statement labeled $\lambda$ and the next statement (labeled by ${\sf
Next}\left(\lambda\right)$)222This definition can be generalized. Our
prototype tool does indeed support a more general definition of fence
positions, which is left out of the article for simplicity.. For a program
${\mathcal{P}}$ and a set $F$ of fence constraints, we define
${{\mathcal{P}}}\oplus{F}$ to mean the program ${\mathcal{P}}$ where all fence
constraints in $F$ have been inserted. To avoid ambiguities in the case when
$F$ contains multiple fence constraints with the same statement label (e.g
$(\lambda,{\tt llfence})$ and $(\lambda,{\tt ssfence})$), we assume that
fences are always inserted in some fixed order.

[Soundness of Fence Sets] For a program ${\mathcal{P}}$, safety property
$\phi$, and set $F$ of fence constraints, the set $F$ is sound for
${\mathcal{P}}$ w.r.t. $\phi$ if ${{\mathcal{P}}}\oplus{F}$ satisfies $\phi$
under SiSd.

A _cost function_ $\kappa$ is a function from fence constraints to positive
integer costs. We extend the notion of a cost function to sets of fence
constraints in the natural way: For a cost function $\kappa$ and a set $F$ of
fence constraints, we define $\kappa(F)=\sum_{c\in{}F}\kappa(c)$.

[Optimality of Fence Sets] For a program ${\mathcal{P}}$, safety property
$\phi$, cost function $\kappa$, and set $F$ of fence constraints, $F$ is
optimal for ${\mathcal{P}}$ w.r.t. $\phi$ and $\kappa$ if $F$ is sound for
${\mathcal{P}}$ w.r.t. $\phi$, and there is no sound fence set $G$ for
${\mathcal{P}}$ w.r.t. $\phi$ where $\kappa(G)<\kappa(F)$.

Observe that the optimality is evaluated with the number of occurrences of
fences in the source program and the costs of different fences.

In order to introduce our algorithm, we define the notion of a _hitting set_.

[Hitting Set] For a set $S=\\{S_{0},\cdots,S_{n}\\}$ of sets
$S_{0},\cdots,S_{n}$, and a set $T$, we say that $T$ is a hitting set of $S$
if $T\cap{}S_{i}\neq\varnothing$ for all $0\leq{}i\leq{}n$.

For example $\\{a,d\\}$ is a hitting set of
$\\{\\{a,b,c\\},\\{d\\},\\{a,e\\}\\}$. For a set $S$ of sets, hitting sets of
$S$ can be computed using various search techniques, such as constraint
programming. We will assume that we are given a function
$\textrm{{hits}}(S,\kappa)$ which computes all hitting sets for $S$ which are
cheapest w.r.t. $\kappa$. I.e., for a set $S$ of finite sets, and a cost
function $\kappa$, the call $\textrm{{hits}}(S,\kappa)$ returns the set of all
sets $T$ with $T\subseteq\bigcup_{S_{i}\in{}S}S_{i}$ such that

  * •

$T$ is a hitting set of $S$, and

  * •

there is no hitting set $T^{\prime}$ of $S$ such that
$\kappa(T^{\prime})<\kappa(T)$.

Fencins(${\mathcal{P}}$,$\phi$,$\kappa$)
---
MM1: opt := $\varnothing$; // Optimal fence sets
MM2: req := $\varnothing$; // Known requirements
MM3:
while($\exists\textrm{{F}}\in\textrm{{hits}}(\textrm{{req}},\kappa)\setminus\textrm{{opt}}$){
MM4:  $\pi$ :=
$\textrm{{reachable}}(\textrm{${{\mathcal{P}}}\oplus{\textrm{{F}}}$},\phi)$;
MM5:  if($\pi=\perp$){
MM6:  opt := $\textrm{{opt}}\cup\\{\textrm{{F}}\\}$;
MM7:  }else{ // $\pi$ is a witness run.
MM8:  C :=
$\textrm{{analyze\\_witness}}(\textrm{${{\mathcal{P}}}\oplus{\textrm{{F}}}$},\pi)$;
MM9:  if($\textrm{{C}}=\varnothing$){ // error under SC!
MM10:  return $\varnothing$;
MM11:  }
MM12:  req := $\textrm{{req}}\cup\\{\textrm{{C}}\\}$;
MM13:  }
MM14: }
MM15: return opt;
Figure 24. The fence insertion algorithm.

We present our fence insertion algorithm in Figure 24. The algorithm keeps two
variables opt and req. Both are sets of fence constraint sets, but are
intuitively interpreted in different ways. The set opt contains all the
optimal fence constraint sets for ${\mathcal{P}}$ w.r.t. $\phi$ and $\kappa$
that have been found thus far. The set req is used to keep track of the
requirements that have been discovered for which fences are necessary for
soundness of ${\mathcal{P}}$. We maintain the following invariant for req: Any
fence constraint set $F$ which is sound for ${\mathcal{P}}$ w.r.t. $\phi$ is a
hitting set of req. As the algorithm learns more about ${\mathcal{P}}$, the
requirements in req will grow, and hence give more information about what a
sound fence set may look like. Notice that the invariant holds trivially in
the beginning, when $\textrm{{req}}=\varnothing$.

In the loop from lines 24-24 we repeatedly compute a candidate fence set F
(line 24), insert it into ${\mathcal{P}}$, and call the reachability analysis
to check if F is sound (line 24). We assume that the call
$\textrm{{reachable}}(\textrm{${{\mathcal{P}}}\oplus{\textrm{{F}}}$},\phi)$
returns $\perp$ if $\phi$ is unreachable in
${{\mathcal{P}}}\oplus{\textrm{{F}}}$, and a witness run otherwise. If
${{\mathcal{P}}}\oplus{\textrm{{F}}}$ satisfies the safety property $\phi$,
then F is sound. Furthermore, since F is chosen as one of the cheapest (w.r.t.
$\kappa$) hitting sets of req, and all sound fence sets are hitting sets of
req, it must also be the case that F is optimal. Therefore, we add F to opt on
line 24.

If ${{\mathcal{P}}}\oplus{\textrm{{F}}}$ does not satisfy the safety property
$\phi$, then we proceed to analyze the witness run $\pi$. The witness analysis
procedure is outlined in Section 6.1. The analysis will return a set C of
fence constraints such that any fence set which is restrictive enough to
prevent the erroneous run $\pi$ must contain at least one fence constraint
from C. Since every sound fence set must prevent $\pi$, this means that every
sound fence set must have a non-empty intersection with C. Therefore we add C
to req on line 24, so that req will better guide our choice of fence set
candidates in the future.

Note that in the beginning, $\textrm{{hits}}(\textrm{{req}},\kappa)$ will
return a singleton set of the empty set, namely $\\{\varnothing\\}$. Then F is
chosen as the empty set $\varnothing$ and the algorithm continues. A special
case occurs when the run $\pi$ contains no memory access reorderings. This
means that ${\mathcal{P}}$ can reach the bad states even under the SC memory
model. Hence it is impossible to correct ${\mathcal{P}}$ by only inserting
fences. The call
$\textrm{{analyze\\_witness}}(\textrm{${{\mathcal{P}}}\oplus{\textrm{{F}}}$},\pi)$
will in this case return the empty set. The main algorithm then terminates,
also returning the empty set, indicating that there are no optimal fence sets
for the given problem.

###  6.1. Witness Analysis

The analyze_witness function takes as input a program ${\mathcal{P}}$ (which
may already contain some fences inserted by the fence insertion algorithm),
and a counter-example run $\pi$ generated by the reachability analysis. The
goal is to find a set $G$ of fences such that

  * •

all sound fence sets have at least one fence in common with $G$ and

  * •

$G$ contains no fence which is already in ${\mathcal{P}}$.

It is desirable to keep $G$ as small as possible, in order to quickly converge
on sound fence sets.

There are several ways to implement analyze_witness to satisfy the above
requirements. One simple way builds on the following insight: Any sound fence
set must prevent the current witness run. The only way to do that, is to have
fences preventing some access reordering that occurs in the witness. So a set
$G$ which contains all fences preventing some reordering in the current
witness satisfies both requirements listed above.

As an example, consider Figure 25. On the left, we show part of a program
${\mathcal{P}}$ where the thread P0 performs three memory accesses L0, L1 and
L2. On the right, we show the corresponding part of a counter-example run
$\pi$. We see that the store L0 becomes globally visible at line 7, while the
loads L1 and L2 access the LLC at respectively lines 3 and 5. Hence the order
between the instructions L0 and L1 and the order between L0 and L2 in the
program code, is opposite to the order in which they take effect w.r.t. the
LLC in $\pi$. We say that L0 is _reordered_ with L1 and L2. The loads are not
reordered with each other. Let us assume that $\pi$ does not contain any other
memory access reordering.

Program fragment  | Witness run
---|---
| process P0
---
...
L0: x := 1;
L1: $\$r_{0}$ := y;
L2: $\$r_{1}$ := z;
...
|  | ...
---|---
1. | fetch(P0,x)
2. | L0: x := 1
3. | fetch(P0,y)
4. |  L1: $\$r_{0}$ := y
5. | fetch(P0,z)
6. |  L2: $\$r_{1}$ := z
| ...
7. | wrllc(P0,x)
| ...
Figure 25.  Left: Part of a program ${\mathcal{P}}$, containing three
instructions of the thread P0. Right: A part of a counter-example run $\pi$ of
${\mathcal{P}}$.

The reordering is caused by the late ${\tt wrllc}$ on line 7\. Hence, this
particular error run can be prevented by the following four fence constraints:
$c_{0}=(\texttt{L0},{\tt ssfence})$, $c_{1}=(\texttt{L1},{\tt ssfence})$,
$c_{2}=(\texttt{L0},{\tt fence})$, and $c_{3}=(\texttt{L1},{\tt fence})$. The
fence set returned by $\textrm{{analyze\\_witness}}({\mathcal{P}},\pi)$ is
$G=\\{c_{0},c_{1},c_{2},c_{3}\\}$. Notice that $G$ satisfies both of the
requirements for analyze_witness.

##  7\. Experimental Results

We have implemented our fence insertion algorithm together with a reachability
analysis for SiSd in the tool Memorax. It is publicly available at
https://github.com/memorax/memorax. We apply the tool to a number of
benchmarks (Section 7.1). Using simulation, we show the positive impact of
using different types of fences, compared to using only the full fence, on
performance and network traffic (Section 7.2).

###  7.1. Fence Insertion Results

We evaluate the automatic fence insertion procedure by running our tool on a
number of different benchmarks containing racy code. For each example, the
tool gives us all optimal sets of fences. We run our tool on the same
benchmarks both for SiSd and for the Si protocol.333Our methods could also run
under a plain Sd protocol. However, to our knowledge, no cache coherence
protocol employs only Sd without Si. The results for SiSd are given in Table
1. We give the benchmark sizes in lines of code. All benchmarks have 2 or 3
processes. The fence insertion procedure was run single-threadedly on a 3.07
GHz Intel i7 CPU with 6 GB RAM.

| Only full fence | Mixed fences
---|---|---
Benchmark | Size (LOC) | Time | #solutions | #fences | Time | #solutions | Fences / proc
bakery | 45 | 17.3 s | 4 | 5 | 108.1 s | 16 |  2 sw, 4 ll, 1 ss
cas | 32 |  $<$0.1 s | 1 | 2 |  $<$0.1 s | 1 |  1 ll, 1 ss
clh | 37 | 4.4 s | 4 | 4 | 3.7 s | 1 |  3 sw, 2 ll, 1 ss
dekker | 48 | 2.0 s | 16 | 3 | 2.9 s | 16 |  1 sw,2 ll, 1 ss
mcslock | 67 | 15.6 s | 4 | 2 | 33.0 s | 4 |  1 ll, 1 ss
testtas | 38 |  $<$0.1 s | 1 | 2 |  $<$0.1 s | 1 |  1 ll, 1 ss
srbarrier | 60 | 0.3 s | 9 | 3 | 0.4 s | 4 |  2 ll, 1 ss
treebarrier | 56 | 33.2 s | 12 | 1 / 2 | 769.9 s | 132 |  1 ll, 1 ss
dclocking | 44 | 0.8 s | 16 | 4 | 0.9 s | 16 |  1 sw, 2 ll, 1 ss
postgresql | 32 |  $<$0.1 s | 4 | 2 | 0.1 s | 4 |  1 ll, 1 ss
barnes 1 | 30 | 0.2 s | 1 | 1 | 0.5 s | 1 |  1 ll / 1 ss
barnes 2 | 96 | 16.3 s | 16 | 1 | 16.1 s | 16 |  1 ss
cholesky | 98 | 1.6 s | 1 | 0 | 1.6 s | 1 | 0
radiosity | 196 | 25.1 s | 1 | 0 | 24.6 s | 1 | 0
raytrace | 101 | 69.3 s | 1 | 0 | 70.1 s | 1 | 0
volrend | 87 | 376.2 s | 1 | 0 | 376.9 s | 1 | 0
Table 1. Automatic fence insertion for SiSd.

The first set of benchmarks are classical examples from the context of lock-
free synchronization. They contain mutual exclusion algorithms: a simple CAS
lock –cas–, a test & TAS lock – _tatas_ – [Sco13], Lamport’s bakery algorithm
–bakery– [Lam74], the MCS queue lock –mcsqueue– [MCS91], the CLH queue lock
–clh– [MLH94], and Dekker’s algorithm –dekker– [Dij02]. They also contain a
work scheduling algorithm –postgresql–444http://archives.postgresql.org/pgsql-
hackers/2011-08/msg00330.php, and an idiom for double-checked locking
–dclocking– [SH96], as well as two process barriers –srbarrier– [Sco13] and
–treebarrier– [MCS91]. The second set of benchmarks are based on the Splash-2
benchmark suite [WOT+95]. We use the race detection tool Fast&Furious [RK15b]
to detect racy parts in the Splash-2 code. We then manually extract models
capturing the core of those parts.

In four cases the tool detects bugs in the original Splash-2 code. The
_barnes_ benchmark is an n-body simulation, where the bodies are kept in a
shared tree structure. We detect two bugs under SiSd: When bodies are inserted
(_barnes 2_), some bodies may be lost. When the center of mass is computed for
each node (_barnes 1_), some nodes may neglect entirely the weight of some of
their children. Our tool inserts fences that prevent these bugs. The
_radiosity_ model describes a work-stealing queue that appears in the Splash-2
_radiosity_ benchmark. Our tool detects data race from it. After careful code
inspection we find that it is possible for all workers but one to terminate
prematurely, leaving one worker to do all remaining work, which is caused by
data race. [SLKR16] The _volrend_ model is also a work-stealing queue. Our
tool detects that it is possible for some tasks to be performed twice. The
bugs in _radiosity_ and _volrend_ can occur even under SC. Hence the code
cannot be fixed only by adding fences. Instead we manually correct it.

For each benchmark, we apply the fence insertion procedure in two different
modes. In the first one (“Only full fence”), we use only full fences. In the
table, we give the total time for computing all optimal sets, the number of
such sets, and the number of fences to insert into each process. For
_treebarrier_ , one process (the root process) requires only one fence, while
the others require two. Notice also that if a benchmark has one solution with
zero fence, that means that the benchmark is correct without the need to
insert any fences.

In the second set of experiments (“Mixed fences”), we allow all four types of
fences, using a cost function assigning a cost of ten units for a full fence,
five units for an ${\tt ssfence}$ or an ${\tt llfence}$, and one unit for a
synchronized write. These cost assignments are reasonable in light of our
empirical evaluation of synchronization cost in Section 7.2. We list the
number of inserted fences of each kind. In _barnes 1_ , the processes in the
model run different codes. One process requires an ${\tt llfence}$, the other
an ${\tt ssfence}$.

In addition to running our tool for SiSd, we have also run the same benchmarks
for Si. As expected, ${\tt ssfence}$ and ${\tt syncwr}$ are no longer
necessary, and ${\tt fence}$ may be downgraded to ${\tt llfence}$. Otherwise,
the inferred fence sets are the same as for SiSd. Since Si allows fewer
behaviors than SiSd, the inference for Si is mostly faster. Each benchmark is
fenced under Si within 71 seconds.

###  7.2. Simulation Results

Here we show the impact of different choices of fences when executing
programs. In particular we show that an optimal fence set using the “Mixed
fences” cost function yields a better performance and network traffic compared
to an optimal fence set using the “Only full fence” cost function. Here
network traffic refers to the traffic in both the on-chip interconnection
network and the memory bus. We account for all the traffic due to coherence
messages. We evaluate the micro-benchmarks analyzed in the previous section
and the whole Splash-2 benchmark suite [WOT+95], running the applications from
beginnig to end, but presenting results only for the parallel phase of the
applications. All programs are fenced according to the optimal fence sets
produced by our tool as described above.

##### Simulation Environment:

We use the Wisconsin GEMS simulator [MSB+05]. We model an in-order processor
that with the Ruby cycle-accurate memory simulator (provided by GEMS) offers a
detailed timing model. The simulated system is a 64-core chip multiprocessor
implementing the SiSd protocol described in Section 2 and 32KB, 4-way, private
L1 caches and a logically shared but physically distributed L2 with 64 banks
of 256KB, 16-way each.

##### Cost of Fences:

Our automatic fence insertion tool employs different weights in order to
insert the optimal amount of fences given the cost of each fence. Here, we
calculate the weights based on an approximate cost of fences obtained by our
simulations.

The effect of fences on performance is twofold. First, there is a cost to
execute the fence instructions (fence latency); the more fences and the more
dirty blocks to self-downgrade, the higher the penalty. Second, fences affect
cache miss ratio (due to self-invalidation) and network traffic (due to extra
fetches caused by self-invalidations and write-throughs caused by self-
downgrades). The combined effect on cache misses and network traffic also
affects performance.

(a) Cycles

(b) Traffic

Figure 26. Percentage of cycles and traffic that each type of fence cost

We calculate the cost of fences in terms of execution as indicated in equation
1, where $\mathit{latency}_{\mathit{fence}}$ is the time in cycles required by
the fence, $\mathit{misses}_{\mathit{si}}$ is the number of misses caused by
self-invalidation, and $\mathit{latency}_{\mathit{miss}}$ is the average
latency of such misses. According to this equation, and considering a protocol
implementing the DoI state described in Section 2, the average percentage of
cycles (execution time) employed by each type of fence when running the
Splash2 benchmarks is the following: the cost of an llfence is 64.4%, the cost
of an ssfence is 22.4%, and the cost of a syncwr is 13.2%, as shown in Figure
26a.

$\mathit{time}_{\mathit{fence}}=\mathit{latency}_{\mathit{fence}}+\mathit{misses}_{\mathit{si}}\times\mathit{latency}_{\mathit{miss}}$
(1)

The cost of the fences in traffic is calculated as indicated in equation 2,
where $\mathit{sd}$ is the number of self-downgrades,
$\mathit{traffic}_{\mathit{wt}}$ is the traffic caused by a write-through, and
$\mathit{traffic}_{\mathit{miss}}$ is the traffic caused by a cache miss. In
percentage, the cost of the each type of fence on average in terms of traffic
is 40.4% for an llfence, 50.3% for an ssfence, and 9.3% for a syncwr, as shown
in Figure 26b. Thus, the weights assigned to fences in our tool seem
reasonable.

$\mathit{traffic}_{\mathit{fence}}=\mathit{sd}*\mathit{traffic}_{\mathit{wt}}+\mathit{misses}_{\mathit{si}}\times\mathit{traffic}_{\mathit{miss}}$
(2)

##### Cache Misses:

As mentioned, the fences affect the cache miss rate. Figure 27 shows clearly
the effect of self-invalidation and self-downgrade on misses. First we show
the misses due to cold capacity and conflict misses (_Cold-cap-conf_), which,
in general, are not affected by the type of fences. However, in some cases
reducing the self-invalidation can give the appearance of extra capacity
misses because of having a more occupied cache. The graph does not plot

(a) Micro-benchmarks

(b) Splash2 benchmarks

Figure 27. Normalized cache misses under different fence sets and protocol
states

coherence misses since fenced programs on Sisd coherence do not induce cache
misses due to coherence transactions. The second kind of miss is named as
_Bypass_. These misses are due to atomic operations which cannot use the data
in the private cache, but need to access it from the shared cache. They are
very frequent in the micro-benchmarks (Figure 27a), which are synchronization
intensive, but almost unnoticeable for the Splash2 benchmarks (Figure 27b).
Finally, we show the misses caused by self-invalidation _Self-inv_. These are
the ones which number is reduced, when applying the mixed fences, but also
when employing the DoI state, since dirty words are not invalidated.

##### Traffic:

As already mentioned, traffic is also affected by the type of fences employed.
Figure 28 shows the traffic in the on-chip network generated by these
applications. The use of llfence, ssfence, syncwr is able to reduce the
traffic requirements by 11.1% for the micro-benchmarks and 1.6% for the
Splash2 applications, on average, compared to using full fences. Additionally,
when employing the DoI state, this reduction reaches 21.3% and 1.9%, on
average, for the micro-benchmarks and the Splash2, respectively. Again, the
more synchronization is required by the applications, the more traffic can be
saved by employing mixed fences.

(a) Micro-benchmarks

(b) Splash2 benchmarks

Figure 28. Normalized network traffic under different fence sets and protocol
states

##### Execution Time:

Finally, we show the impact on execution time, which is affected by the
reductions in cache misses and traffic. Figure 29 shows simulated execution
time for both the micro-benchmarks (Figure 29a) and the Splash2 benchmarks
(Figure 29b). The use of mixed fences improves the execution time compared to
using full fences by 10.4% for the micro-benchmarks and by 1.0% for the
Splash2 benchmarks. The DoI-mixed column shows the execution time results for
the same mixed fence sets as the mixed column. But in DoI case, llfences are
implemented in GEMS using an extra L1 cache line state (the Dirty-or-Invalid
state). This feature is an architectural optimization of the SiSd protocol.
Implementing the DoI state further improves the performance of the mixed
fences, by 20.0% for the micro-benchmarks and 2.1% for the Splash2, on
average, compared to using of full fences. Mixed fences are useful for
applications with more synchronization. Applications using more
synchronization would benefit to a large extent from the use of mixed fences.

(a) Micro-benchmarks

(b) Splash2 benchmarks

Figure 29. Execution time under different fence sets and protocol states

##  8\. Conclusions and Future Work

We have presented a uniform framework for automatic fence insertion in
programs that run on architectures that provide self-invalidation and self-
downgrade. We have implemented a tool and applied it on a wide range of
benchmarks. There are several interesting directions for future work. One is
to instantiate our framework in the context of abstract interpretation and
stateless model checking. While this will compromise the optimality criterion,
it will allow more scalability and application to real program code. Another
direction is to consider robustness properties [BMM11]. In our framework, this
would mean that we consider program traces (in the sense of Shasha and Snir
[SS88]), and show that the program will not exhibit more behaviors under SiSd
than under SC. While this may cause over-fencing, it frees the user from
providing correctness specifications such as safety properties. Also, the
optimality of fence insertion can be evaluated with the number of the times
that each fence is executed. This measurement will provide more accuracy when,
for instance, fences with different weights are inserted in a loop computation
in a branching program.

##### Acknowledgment

This work was supported by the Uppsala Programming for Multicore Architectures
Research Center (UPMARC), the Swedish Board of Science project, “Rethinking
the Memory System”, the “Fundación Seneca-Agencia de Ciencia y Tecnología de
la Región de Murcia” under the project “Jóvenes Líderes en Investigación” and
European Commission FEDER funds.

## References

  * [AAC+12] Parosh Aziz Abdulla, Mohamed Faouzi Atig, Yu-Fang Chen, Carl Leonardsson, and Ahmed Rezine.  Counter-example guided fence insertion under TSO.  In TACAS, pages 204–219. Springer, 2012.
  * [ADC11] Thomas J. Ashby, Pedro Díaz, and Marcelo Cintra.  Software-based cache coherence with hardware-assisted selective self-invalidations using bloom filters.  IEEE Transactions on Computers (TC), 60(4):472–483, April 2011\.
  * [AH90] Sarita V. Adve and Mark D. Hill.  Weak ordering – a new definition.  In ISCA, pages 2–14, 1990.
  * [AKNP14] Jade Alglave, Daniel Kroening, Vincent Nimal, and Daniel Poetzl.  Don’t sit on the fence - A static analysis approach to automatic fence insertion.  In CAV, pages 508–524, 2014.
  * [BDM13] Ahmed Bouajjani, Egor Derevenetc, and Roland Meyer.  Checking and enforcing robustness against TSO.  In Programming Languages and Systems, pages 533–553. Springer, 2013\.
  * [BMM11] Ahmed Bouajjani, Roland Meyer, and Eike Möhlmann.  Deciding robustness against total store ordering.  In ICALP (2), volume 6756 of LNCS, pages 428–440. Springer, 2011.
  * [CKS+11] Byn Choi, Rakesh Komuravelli, Hyojin Sung, Robert Smolinski, Nima Honarmand, Sarita V. Adve, Vikram S. Adve, Nicholas P. Carter, and Ching-Tsun Chou.  DeNovo: Rethinking the memory hierarchy for disciplined parallelism.  In PACT, pages 155–166, 2011.
  * [CL05] David Chase and Yossi Lev.  Dynamic circular work-stealing deque.  In SPAA, pages 21–28, 2005.
  * [Dij02] E. W. Dijkstra.  Cooperating sequential processes.  2002\.
  * [DRHK15] Mahdad Davari, Alberto Ros, Erik Hagersten, and Stefanos Kaxiras.  An efficient, self-contained, on-chip, directory: DIR1-SISD.  In PACT, pages 317–330, 2015.
  * [DSS06] David Dice, Ori Shalev, and Nir Shavit.  Transactional locking II.  In DISC, volume 4167 of Lecture Notes in Computer Science, pages 194–208, 2006.
  * [GHS09] Rachid Guerraoui, Thomas A. Henzinger, and Vasu Singh.  Software transactional memory on relaxed memory models.  In Computer Aided Verification, 21st International Conference, CAV 2009, Grenoble, France, June 26 - July 2, 2009. Proceedings, pages 321–336, 2009.
  * [GHS11] Rachid Guerraoui, Thomas A. Henzinger, and Vasu Singh.  Verification of STM on relaxed memory models.  Formal Methods in System Design, 39(3):297–331, 2011.
  * [HHB+14] Derek R. Hower, Blake A. Hechtman, Bradford M. Beckmann, Benedict R. Gaster, Mark D. Hill, Steven K. Reinhardt, and David A. Wood.  Heterogeneous-race-free memory models.  In ASPLOS, pages 427–440, 2014.
  * [HS08] Maurice Herlihy and Nir Shavit.  The Art of Multiprocessor Programming.  Morgan Kaufmann Publishers Inc., San Francisco, CA, USA, 2008.
  * [KK11] Stefanos Kaxiras and Georgios Keramidas.  SARC coherence: Scaling directory cache coherence in performance and power.  IEEE Micro, 30(5):54–65, September 2011.
  * [KR13] Stefanos Kaxiras and Alberto Ros.  A new perspective for efficient virtual-cache coherence.  In ISCA, pages 535–547, 2013.
  * [KRHK16] Konstantinos Koukos, Alberto Ros, Erik Hagersten, and Stefanos Kaxiras.  Building heterogeneous unified virtual memories UVMS without the overhead.  ACM TACO, 13(1):1:1–1:22, 2016.
  * [KVY10] Michael Kuperstein, Martin Vechev, and Eran Yahav.  Automatic inference of memory fences.  In FMCAD, pages 111–119. IEEE, 2010.
  * [Lam74] Leslie Lamport.  A new solution of Dijkstra’s concurrent programming problem.  Communications of the ACM, 17, August 1974.
  * [Lam79] Leslie Lamport.  How to make a multiprocessor computer that correctly executes multiprocess programs.  IEEE Transactions on Computers (TC), 28(9):690–691, September 1979\.
  * [LNP+12] Feng Liu, Nayden Nedev, Nedyalko Prisadnikov, Martin T. Vechev, and Eran Yahav.  Dynamic synthesis for relaxed memory models.  In PLDI, pages 429–440, 2012.
  * [LW95] Alvin R. Lebeck and David A. Wood.  Dynamic self-invalidation: Reducing coherence overhead in shared-memory multiprocessors.  In ISCA, pages 48–59, 1995.
  * [MCS91] J. M. Mellor-Crummey and M. L. Scott.  Algorithms for scalable synchronization on shared-memory multiprocessors.  ACM Transactions on Computer Systems (TOCS), 9, February 1991.
  * [MLH94] Peter Magnusson, Anders Landin, and Erik Hagersten.  Queue locks on cache coherent multiprocessors.  In Proceedings of the Eighth International Parallel Processing Symposium, pages 165–171. IEEE, 1994.
  * [MSB+05] Milo M.K. Martin, Daniel J. Sorin, Bradford M. Beckmann, Michael R. Marty, Min Xu, Alaa R. Alameldeen, Kevin E. Moore, Mark D. Hill, and David A. Wood.  Multifacet’s general execution-driven multiprocessor simulator (GEMS) toolset.  Computer Architecture News, 33(4):92–99, September 2005.
  * [RDK15] Alberto Ros, Mahdad Davari, and Stefanos Kaxiras.  Hierarchical private/shared classification: the key to simple and efficient coherence for clustered cache hierarchies.  In HPCA, pages 186–197, 2015.
  * [RK12] Alberto Ros and Stefanos Kaxiras.  Complexity-effective multicore coherence.  In PACT, pages 241–252, 2012.
  * [RK15a] Alberto Ros and Stefanos Kaxiras.  Callback: Efficient synchronization without invalidation with a directory just for spin-waiting.  In ISCA, pages 427–438, 2015.
  * [RK15b] Alberto Ros and Stefanos Kaxiras.  Fast&furious: A tool for detecting covert racing.  In PARMA and DITAM, pages 1–6, 2015.
  * [RK16] Alberto Ros and Stefanos Kaxiras.  Racer: TSO consistency via race detection.  In 49th IEEE/ACM Int’l Symp. on Microarchitecture (MICRO), 2016\.
  * [SA15] Hyojin Sung and Sarita V. Adve.  DeNovoSync: Efficient support for arbitrary synchronization without writer-initiated invalidations.  In ASPLOS, pages 545–559, 2015.
  * [Sco13] Michael L. Scott.  Shared-Memory Synchronization.  Morgan & Claypool, 2013.
  * [SH96] Douglas C. Schmidt and Tim Harrison.  Double-checked locking - an optimization pattern for efficiently initializing and accessing thread-safe objects.  In PLoP, 1996.
  * [SKA13] Hyojin Sung, Rakesh Komuravelli, and Sarita V. Adve.  DeNovoND: Efficient hardware support for disciplined non-determinism.  In ASPLOS, pages 13–26, 2013.
  * [SLKR16] Christos Sakalis, Carl Leonardsson, Stefanos Kaxiras, and Alberto Ros.  Splash-3: A properly synchronized benchmark suite for contemporary research.  In ISPASS, 2016.
  * [SS88] Dennis Shasha and Marc Snir.  Efficient and correct execution of parallel programs that share memory.  ACM Transactions on Programming Languages and Systems (TOPLAS), 10(2):282–312, 1988.
  * [WOT+95] Steven Cameron Woo, Moriyoshi Ohara, Evan Torrie, Jaswinder Pal Singh, and Anoop Gupta.  The SPLASH-2 programs: Characterization and methodological considerations.  In ISCA, pages 24–36, 1995.