Jade Alglave

Luc Maranget

Susmit Sarkar

Peter Sewell

Fences in Weak Memory Models (Extended Version)

come

Fences in weak memory models (extended version)

Introduction

Most multiprocessors exhibit subtle relaxed-memory behaviour, with writes from one thread not immediately visible to all others; they do not provide sequentially consistent memory [START_REF] Lamport | How to Make a Correct Multiprocess Program Execute Correctly on a Multiprocessor[END_REF]. For some, such as x86 [START_REF]Intel 64 and IA-32 Architectures Software Developer's Manual (5 vols)[END_REF][START_REF]AMD64 Architecture Programmer's Manual. Advanced Micro Devices[END_REF][START_REF] Sarkar | The Semantics of x86-CC Multiprocessor Machine Code[END_REF][START_REF] Owens | A Better x86 Memory Model: x86-TSO[END_REF][START_REF] Sewell | x86-TSO: A rigorous and usable programmer's model for x86 multiprocessors[END_REF] and Power [25], the vendor documentation is in inevitably-ambiguous informal prose, leading to confusion. Thus we have no foundation for software verification of concurrent systems code, and no target specification for hardware verification of microarchitecture. To remedy this state of affairs, we take a firmly empirical approach, developing, in tandem, testing tools and models of multiprocessor behaviour-the test results guiding model development and the modelling suggesting interesting tests. In this paper we make five contributions:

1. We introduce a class of axiomatic memory models, defined in Coq [START_REF] Bertot | Coq'Art[END_REF], which we show how to instantiate to produce Sequential Consistency (SC), Sparc Total Store Order (TSO) [30], and a Power model (see item 4 below). 2. We describe our diy testing tool. Much discussion of memory models has been in terms of litmus tests (e.g. iriw [START_REF] Boehm | Foundations of the C++ Concurrency Memory Model[END_REF]): ad-hoc multiprocessor programs for which particular final states may be allowed on a given architecture. Given a potential violation of SC , diy systematically and automatically generates litmus tests (including classical ones such as iriw) and runs them on the hardware. These tests can be used to explore the behaviour of processor implementations and also the outcomes permitted by a model, and hence to compare the two; we illustrate this by our exploration of Power machines. 3. We use diy to generate about 800 tests, running them up to 1e12 times on three Power machines. They identified a rarely occurring implementation error in Power 5 memory barriers (for which IBM is providing a workaround), and further suggest that Power 6 does not suffer from this. 4. Based on these, and on other test results, we developed an axiomatic memory model (the CAV 2010 model ) for Power which captures several important aspects of the processor's behaviour. Notably, it describes the lack of multi-copy store atomicity [START_REF] Adve | Shared Memory Consistency Models: A Tutorial[END_REF][START_REF] Maessen | Memory Model = Instruction Reordering + Store Atomicity[END_REF], despite being in a simple global-time style rather than the per-processor timelines implied by the architecture text. It also models the ordering relaxations we observe and A-cumulative barriers [25]. The model is sound with respect to all our experimental results, though for some of the Power barriers it is weaker than one might like; we discuss this in detail. 5. We prove in Coq theorems about the strength and placement of memory barriers required to regain a strong model from a weaker model.

The experimental details and the sources and documentation of diy are available online 1 , as are the Coq development and typeset outlines of the proofs2 , which are further described in the first author's PhD thesis [START_REF] Alglave | A Shared Memory Poetics[END_REF]. This paper extends a conference paper in CAV 2010 [START_REF] Alglave | Fences in Weak Memory Models[END_REF], adding more explanation and more details of diy and of the axiomatic Power model introduced there.

Our class of models

A memory model determines whether a candidate execution of a program is valid. For example, Fig. 1(a) shows a simple litmus test, comprising an initial state (which gathers the initial values of registers and memory locations used in the test), a program in pseudo-or assembly code, and a final condition on registers and memory (we write x, y for memory locations and r1, r2 for registers). If each location initially holds 0 (henceforth we omit the initial state if so), then, e.g. on x86 processors, there are valid executions with the specified final state [START_REF] Owens | A Better x86 Memory Model: x86-TSO[END_REF].

Informal overview of our approach

We start here by explaining the concepts that we use at a high level. We then define these concepts formally in the forthcoming subsections.

Describing executions of programs

We study concurrent programs such as the one given in Fig. 1(a). Each of these programs gives an initial state describing the initial values in memory locations and registers initially, e.g. x=0; y=0 in Fig. 1(a), meaning that we suppose that the memory locations x and y hold the value 0 initially. Except when the examples are specific to our study of the Power architecture, i.e. in Sec. 6 and 7, we write the instructions in pseudo-code; for example x ← 1 is a store of value 1 into memory location x, and r1 ← y is a load from memory location y into a register r1. We depict a concurrent program as a table, where the columns are processors (e.g. P 0 and P 1 in Fig. 1(a)), and the lines are labelled with letters-for example in Fig. 1(a), the first line, which holds x ← 1, is labelled (a). We describe a candidate execution of a given program using memory events, corresponding to the memory accesses yielded by executing the instructions of the program. For example, we give in Fig. 1(b) the memory events of one candidate execution of the program of Fig. 1(a): the write event (a) W x 1 corresponds to the store x ← 1 at line (a). In this candidate execution both reads read value 0.

In addition to these memory events, a candidate execution of a program consists of several relations over them. One of these relations represents the program order as given by an unfolding of a control-flow path through the text of the program-in any execution of the program Fig. 1(a), the execution of the instruction at line (a) is program-order-before execution of the instruction at line (b). This is expressed as the po → relation between the corresponding events in Fig. 1(b). Other relations represent the interaction with memory: the reads-from relation rf → indicates which write the value of a each read event comes from; and the write serialisation ws → represents the coherence order for each location (for each location, there is a total order over the writes to that location). Reads-from edges with no source or target represent reads from the initial state or writes that appear in the final state respectively.

Defining the validity of an execution

We then define the validity of a given candidate execution as acyclicity checks of certain unions of these relations.

Many interesting candidate executions (and all the executions that we will show in this paper) contain at least one cycle, such as that depicted in Fig. 1(c). Typically, this cycle will exhibit the fact that the execution that we choose to depict is invalid in the Sequential Consistency (SC) model [START_REF] Lamport | How to Make a Correct Multiprocess Program Execute Correctly on a Multiprocessor[END_REF]. The execution in Fig. 1(c) is allowed in TSO and in Power, but not in SC, where at least one of the reads would have to read 1.

In addition, our test programs contain a constraint on the final state. For example, the program in Fig. 1(a) shows the line "Observed? r1=0;r2=0". We use several different keywords to express the final state of our programs. The keyword "Observed" (or its counterpart "Not observed") refers to empirical results. This means that we actually observed an execution satisfying the final state constraint on a given machine. When there is a question mark, as in "Observed?", this means that we question whether the outcome is observable or not on a given machine. The keyword "Allowed" (or its counterpart "Forbidden") refers to whether a given model allows (or forbids) the specified outcome. This means that we can deduce from the definition of the model that this outcome is allowed (or forbidden).

The fact that the specified final state of a given program-such as "Observed? r1=0; r2=0" in Fig. 1(a)-is observable or allowed relates to the graphs describing the executions of this program-such as the one given in Fig. 1(c).

Let us examine the Allowed/Forbidden case first. As we said above, the validity of an execution in the model we present here boils down to the presence of certain cycles in the execution graph. Thus, if an execution graph contains a cycle, then we have to examine if the model that we are studying allows some 'relaxation' of the relations that are involved in this cycle. If some relaxations are allowed, then the cycle does not forbid the execution, and the final state is allowed by the model. For example in Fig. 1(c), on a model such as SC where no relaxation is allowed, the cycle forbids the execution. On a model such as x86, where the program order between a write and a read may be relaxed, the cycle does not forbid the execution, for the program order relation (written po → in Fig. 1(c)) between (a) and (b) (and similarly (c) and (d)) is relaxed.

For the Observed/Not observed case, we have to run the test against hardware to check whether the specified final outcomes appears. If we observe a given final state, we sometimes can deduce which is the feature of the hardware-as represented by our model-that allows this outcome. For example, we were able to observe the final state of Fig. 1(a) on x86 machines. From this we deduce that the cycle in Fig. 1(c) does not forbid the execution on some x86 machines, and furthermore that the x86 model allows the reordering of write-read pairs. Of course, as usual with black-box testing, one cannot deduce anything with certainty from the absence of an empirical observation.

Events and program order

As sketched above, rather than dealing directly with programs, our models are in terms of the events E occurring in a candidate program execution. A memory event m represents a memory access, specified by its direction (write or read), its location loc(m), its value val(m), its processor proc(m), and a unique label. The store to x with value 1 marked (a) in Fig. 1(a) generates the event (a) W x 1 in Fig. 1(b). Henceforth, we write r (resp. w) for a read (resp. write) event. We write M ℓ,v (resp. R ℓ,v , W ℓ,v ) for the set of memory events (resp. reads, writes) to a location ℓ with value v (we omit ℓ and v when quantifying over all of them). A barrier instruction generates a barrier event b; we write B for the set of all such events.

→ m 2 (m 1 , m 2 ) ∈( rf → ∪ ws → ∪ fr →) (written hb-seq → in [9]) 2.5

Fig. 2 Table of relations

The models are defined in terms of binary relations over these events, and Fig. 2 has a first table of the relations we use. The relations given in Fig. 2 are entirely generic; we give some more relations that are specific to Power in Fig. 17.

As usual, the program order po → is a total order amongst the events from the same processor that never relates events from different processors. It reflects the sequential execution of instructions on a single processor: given two instruction execution instances i 1 and i 2 that generate events e 1 and e 2 , e 1 po → e 2 means that a sequential processor would execute i 1 before i 2 . When instructions may perform several memory accesses, we take intra-instruction dependencies [START_REF] Sarkar | The Semantics of x86-CC Multiprocessor Machine Code[END_REF] into account to build a total order.

We postulate a dp → relation to model the dependencies between instructions, such as data or control dependencies [25, pp. 653-668]. This relation is a subrelation of po →, and always has a read as its source.

Execution witnesses

Although po → conveys important features of program execution, e.g. branch resolution, it does not characterise an execution. To do so, we postulate, as part of the data of a candidate execution, two additional relations ws → and rf → over memory events.

Write serialisation

We assume all values written to a given location ℓ to be serialised, following a coherence order. This means, following the Power documentation [25, p.657, 1st col, last §], that all stores to a given memory location ℓ are totally ordered:

Memory coherence refers to the ordering of stores to a single location. Atomic stores to a given location are coherent if they are serialised in some order, and no processor or mechanism is able to observe any subset of those stores as occurring in a conflicting order. This property is widely assumed by modern architectures, including for example Sparc TSO [30] and x86-TSO [START_REF] Owens | A Better x86 Memory Model: x86-TSO[END_REF].

Consequently, we define ws → as the union of the coherence orders for all memory locations, which must be well formed following the wf-ws predicate:

wf-ws( ws →) ws → ⊆ ℓ (W ℓ × W ℓ ) ∧ ∀ℓ. total-order ws →, (W ℓ × W ℓ )
Reads-from map We write w rf → r to mean that r loads the value stored by w (so w and r must share the same location and value). Given a read r there exists a unique write w such that w rf → r. The write w can be an init store when r loads from the initial state. The initial store to a location x is defined as the first write in the coherence order for x. Thus, rf → must be well formed following the wf-rf predicate:

wf-rf( rf →) rf → ⊆ ℓ,v (W ℓ,v × R ℓ,v ) ∧ (∀r, ∃! w. w rf → r)
From-read map It is useful to define a derived relation fr → (as in [START_REF] Ahamad | The Power of Processor Consistency[END_REF]) which gathers all pairs of reads r and writes w such that r reads from a write that is before w in ws → (as in Fig. 3):

r fr → w ∃ w ′ . w ′ rf → r ∧ w ′ ws → w
The significance of fr → is as follows. Some of the weaknesses of multiprocessor memory models arises from the fact that a write is not necessarily made available to all potential reading threads in one atomic step. In TSO models (e.g. for Sparc and x86-TSO), this is true in a relatively benign way: the writing thread might read 'early' from its own write before that is propagated to all other threads. In more relaxed models (e.g. for Power and ARM) there may be more complex behaviour, for example with a write being made available first to the writing thread itself, then to near-neighbours of that thread (that share some level of the cache hierarchy), and later to other threads. If one thinks of a write event as representing the point in time when a write has been made available to all threads, and a read event as the point when the value of the read is determined, then reads-from rf → edges are not necessarily forwards in time (a read can have read from a write before the write is made available to all), but a from-read fr → edge, from a read to a coherence-successor of the write it read from, is necessarily forwards in time (otherwise the read would have to read from the coherence-later write).

Execution witnesses We define an execution witness X as follows:

X (E, po →, dp →, rf →, ws →)
The well-formedness predicate wf on execution witnesses is the conjunction of those for Note that an execution witness describes only one candidate execution of a program. A given program can have many candidate execution witnesses, with different control-flow paths, different values read from memory, different readsfrom relations, and different write serialisations; a memory model will permit some of these and forbid others. Consider for example the program given in Fig. 4(a). The processors P 0 and P 1 both write to the same location x. This program has two candidate executions, shown in Fig. 4(b) and (c), with different write serialisations. The one in Fig. 4(b) covers the case where P 0 's write is coherence-before P 1 's. The second one, in Fig. 4(c), covers the converse.

P 0 P 1 (a) x ← 1 (b) x ← 2 Allowed x=1 ∨ x=2
For an example of candidate executions differing in the writes that are the sources of a read-from edge, consider the program in Fig. 5(a). The processors P 0 and P 1 both write the value 1 into memory location x. The processor P 2 reads from x. Hence, this program can have at least two distinct execution witnesses, given in Fig. 5(b) and(c). The one in Fig. 5(b) covers the case where P 2 reads from P 0 . The second one, given in Fig. 5(c), covers the case where P 2 reads from P 1 .

Global Happens-Before

In the family of memory models we use in this paper, a candidate execution witness is valid if the memory events can be embedded in an acyclic global happens-before relation ghb → (together with two auxiliary conditions detailed in Sec. 2.5). Each → represents a point in global time when this write becomes visible to all processors (we say it is globally performed then); whereas the position of a read in ghb → represents the point in global time when the read takes place. Note that these are concepts associated with the model; the precise relationship between the model events and concrete microarchitectural events in processor implementations may be subtle -for example, in an implementation write might never actually be propagated to threads that do not read the associated cache line. There remain key choices as to which relations we include in ghb → (i.e. which we consider to be in global time), which leads us to define a class of models.

Init: x=0; P 0 P 1 P 2 (a) x ← 1 (b) x ← 1 (c) r1 ← x Allowed r1=1; (a) Program
Globality Writes are not necessarily made available to all processors at once, so → r ∧ proc(w) = proc(r). Some architectures allow store forwarding (or read own writes early [START_REF] Adve | Shared Memory Consistency Models: A Tutorial[END_REF]): the processor issuing a given write can read its value before any other participant accesses it. Then rfi → is not included in ghb → . Other architectures allow two processors sharing a cache to read a write issued by their neighbour w .r .t. the cache hierarchy before any other participant that does not share the same cache-a particular case of read others' writes early [START_REF] Adve | Shared Memory Consistency Models: A Tutorial[END_REF]. Then In our class of models, ws → and fr → are always included in ghb → . Indeed, the write serialisation for a given location ℓ is the order in which writes to ℓ are globally performed. Moreover, as r fr → w expresses that the write w ′ from which r reads is globally performed before w, it forces the read r to be globally performed (since a read is globally performed as soon as it is performed) before w is globally performed.

Preserved program order In any given architecture, certain pairs of events in the program order are guaranteed to occur in that order. We postulate a global relation ppo → gathering all such pairs. For example, the execution witness in Fig. 1(c) is only valid if the writes and reads to different locations on each processor have been reordered. Indeed, if these pairs were forced to be in program order, we would have a cycle in Uniprocessor First, we require each processor to respect memory coherence for each location [START_REF] Cantin | The Complexity of Verifying Memory Coherence[END_REF]. If a processor writes e.g. v to ℓ and then reads v ′ from ℓ, v ′ should not precede v in the write serialisation. We define the relation

m 1 po-loc → m 2 m 1 po → m 2 ∧ loc(m 1 ) = loc(m 2 ) uniproc(X) acyclic( com → ∪ po-loc → )
For example, in Fig. 6 (a), the final value of x shows that the write (a) is the last one in coherence order. Since Thin air Second, we rule out programs where values come out of thin air [START_REF] Manson | The Java Memory Model[END_REF]. This means that we forbid certain causal loops, following the terminology employed in the Alpha documentation [START_REF]Alpha Architecture Reference Manual[END_REF].

0 P 1 (a) x ← 1 (b) r1 ← x (c) x ← 2 (a) uniproc Forbidden: x=1; r1=1; P 0 P 1 (a) r1 ← x (c) r4 ← y r9 ← xor r1,r1 r9 ← xor r4,r4 (b) y ← 1+r9 (d) x ← 1+r9 (b) thin Forbidden: r1=1; r4=1; (a) W x 1 (b) R x 1 (c) W x 2
Consider the test given in Fig. 6 (b). In this example, the write (b) to y on P 0 is dependent on the read (a) from x on P 0 , because the xor instruction between them does a calculation on the value written by (a) in r1, and writes the result into r9, later used by (b). Similarly on P 1 , (c) and (d) are dependent. Suppose the read (a) from x on P 0 reads from the write (d) to x on P 1 , and similarly the read (c) from y on P 1 reads from the write (b) to y on P 0 , as depicted by the execution in Fig. 6 (b). In this case, the values read by (a) and (c) seem to come out of thin air, because they cannot be determined. We formalise the check that forbids such a scenario as follows: thin(X) acyclic(

rf → ∪ dp →)
All together We define the validity of an execution w .r .t. an architecture A as the conjunction of three checks independent of the architecture, namely wf(X), uniproc(X) and thin(X) with a last one that characterises the architecture:

A.valid(X)
wf(X) ∧ uniproc(X) ∧ thin(X) ∧ acyclic(ghb(X))

Comparing architectures via validity predicates

From our definition of validity arises a simple notion of comparison among architectures.

A 1 ≤ A 2 means that A 1 is weaker than A 2 : A 1 ≤ A 2 ( ppo1 → ⊆ ppo2 → ) ∧ ( grf1 → ⊆ grf2 → )
The validity of an execution is decreasing w .r .t. the strength of the predicate; i.e. a weak architecture exhibits at least all the behaviours of a stronger one:

Theorem 1 (Validity is decreasing)

∀A 1 A 2 , (A 1 ≤ A 2 ) ⇒ (∀X, A ǫ 2 .valid(X) ⇒ A ǫ 1 .valid(X))
Programs running on an architecture A ǫ 1 exhibit executions that would be valid on a stronger architecture A ǫ 2 ; we characterise all such executions as follows:

A 1 .check A2 (X) acyclic( grf2 → ∪ ws → ∪ fr → ∪ ppo2 → )
Then, we show that executions that are valid on A 1 and that satisfy this predicate are valid on A 2 and conversely:

Theorem 2 (Characterisation) ∀A 1 A 2 , (A 1 ≤ A 2 ) ⇒ (∀X, (A ǫ 1 .valid(X) ∧ A 1 .check A2 (X)) ⇔ A ǫ 2 .valid(X))
These two theorems, though fairly simple, will be useful to compare two models and to restore a strong model from a weaker one, as in Sec. 3.

Examples

We propose here alternative formulations of Sequential Consistency (SC) [START_REF] Lamport | How to Make a Correct Multiprocess Program Execute Correctly on a Multiprocessor[END_REF] and Sparc's Total Store Ordering (TSO) [30] in our framework, which we proved equivalent to the original definitions. We omit proofs and the formal details for brevity, but they can be found at http://diy.inria.fr/wmm. We write po(X) (resp. rf(X), rfe(X)) for the function extracting the po → (resp. rf →, rfe →) relation from X. We define notations to extract pairs of memory events from the program order:

MM λX. ((M × M) ∩ po(X)), RM λX. ((R × M) ∩ po(X)) and WW λX. ((W × W) ∩ po(X)).
SC allows no reordering of events ( ppo → equals po → on memory events). In addition, SC makes writes available to all processors as soon as they are issued ( rf → are global). By this we mean that write events take immediately their place in the global-happens before relation, i.e. that once they become to one processor, they are visible to all processors. Thus, there is no need for barriers, and any architecture is weaker than SC:

SC (MM , rf, λX.∅).
The following criterion characterises, as in Sec. 2.6, valid SC executions on any architecture:

A.check SC (X) = acyclic( com → ∪ po →).
Thus, the outcome of Fig. 1 will never be the result of an SC execution, as it exhibits the cycle: (a

) po → (b) fr → (c) po → (d) fr → (a).
TSO allows two relaxations [START_REF] Adve | Shared Memory Consistency Models: A Tutorial[END_REF]: write to read program order, meaning its ppo → includes all pairs but the store-load ones (ppo tso (λX. (RM (X) ∪ WW (X))) and read own write early ( rfi → are not global). We elide barrier semantics, detailed in Sec. 3:

TSO ǫ
(ppo tso , rfe, λX.∅). Sec. 2.6 shows the following criterion characterises valid executions (w .r .t. any A ≤ TSO) that would be valid on TSO ǫ , e.g. in Fig. 1:

A.check TSO (X) = acyclic( ws → ∪ fr → ∪ rfe → ∪ ppo-tso → ).

Semantics of barriers

In this section we characterise the semantics and placement in the code that barriers should have to restore a stronger model from a weaker one.

It is clearly enough to have w ab1 → r whenever w grf 2\1

→ r holds to restore store atomicity, i.e. a barrier ensuring rf → is global. But then a processor holding such a barrier placed after r would have to wait until w is globally performed before executing the read. We provide a less costly requirement: consider the case where

w rf → r po → m,
where r may take its value before w is visible to all processors. Inserting a barrier instruction that has our semantics between the instructions generating r and m only forces the processor generating r and m to delay m until w is globally performed.

We give here an intuition of the strength that the barriers of the architecture A 1 should have to restore the stronger A 2 . They should:

1. restore the pairs that are preserved in the program order on A 2 and not on A 1 , which is a static property; 2. compensate for the fact that some writes may not be globally performed at once on A 1 while they are on A 2 , which we model by (some subrelation of) rf → not being global on A 1 while it is on A 2 ; this is a dynamic property.

Formally, we write

r 2\1 → r2 → \ r1
→ for the set difference. In addition, we write

x r1 →; r2 → y ∃z. x r1 → z ∧ z r2
→ y for the sequence of two relations. Given A 1 ≤ A 2 , we define the predicate fb (fully barriered ) on executions X by

A 1 .fb A2 (X) ( ppo 2\1 → ) ∪ ( grf 2\1 → ; ppo2 → ) ⊆ ab1 →
We can then prove that the above condition on

ab1 → is sufficient to regain A ǫ 2 from A 1 :
Theorem 3 (Barrier guarantee)

∀A 1 A 2 , (A 1 ≤ A 2 ) ⇒ (∀X, A 1 .valid(X) ∧ A 1 .fb A2 (X) ⇒ A ǫ 2 .

valid(X))

The static property of barriers is expressed by the condition

ppo 2\1 → ⊆ ab1 → .
A barrier provided by A 1 should ensure that the events generated by a same processor are globally performed in program order if they are on A 2 . In this case, it is enough to insert a barrier between the instructions that generate these events.

The dynamic property of barriers is expressed by the condition

grf 2\1 → ; ppo2 → ⊆ ab1 → .
A barrier provided by A 1 should ensure store atomicity to the write events that have this property on A 2 . This is how we interpret the cumulativity of barriers, as stated by Power [25], in our framework: the A-cumulativity (resp. B-cumulativity) property applies to barriers that enforce ordering of pairs in

rf →; po → (resp. po →; rf →).
We consider a barrier that only preserves pairs in po → to be non-cumulative. Thm. 3 states that, to restore A 2 from A 1 , it suffices to insert an A-cumulative barrier between each pair of instructions such that the first one in the program order reads from a write which is to be globally performed on A 2 but is not on A 1 .

iriw P 0 P 1 P 2 P 3 (a) r1 ← x (c) r2 ← y (e) x ← 1 (f ) y ← 2 (b) r2 ← y (d) r1 ←
x Observed? 0:r1=1; 0:r2=0; 1:r2=2; 1:r1=0; Restoring SC We model an A-cumulative barrier as a function returning an ordering relation when given a placement of the barriers in the code:

(a) R x 1 (b) R y 0 (f ) W y 2 (c) R y 2 (d) R x 0 (e) W x
m 1 fenced → m 2 ∃b. m 1 po → b po → m 2 A-cumul(X, fenced → ) fenced → ∪ rf →; fenced →
The following corollary of Thm. 3 (with A 1 = A and A 2 = SC) shows that inserting such a barrier between all po → pairs restores SC :

Corollary 1 (Barriers restoring SC ) ∀A X, (A.valid(X) ∧ A-cumul(X, MM ) ⊆ ab →) ⇒ SC .valid(X)
Consider e.g. the iriw test depicted in Fig. 7. The specified outcome may be the result of a non-SC execution on a weak architecture in the absence of barriers, as shown in Fig. 7. Our A-cumulative barrier placed between each pair of reads on P 0 and P 1 forbids this outcome, as shown in Fig. 8

P 0 P 1 P 2 P 3 (a) r1 ← x (c) r2 ← y (e) x ← 1 (f ) y ← 2 fence fence (b) r2 ← y (d) r1 ←
x Observed? 0:r1=1; 0:r2=0; 1:r2=2; 1:r1=0;

(a) R x 1 (b) R y 0 (f ) W y 2 (c) R y 2 (d) R x 0 (e) W x

Informal overview of our method

We start here by explaining the idea of the method employed by diy at a high level, then give further details in the following subsections.

As we described in the previous section, the outcome of the iriw test in More precisely, a global cycle in an execution graph forbids the specified outcome of a test in the model, as we explained in Sec. 2. This means that if a machine implements exactly the studied model, then the outcome of this test should not be observed. To check this, we thus build tests from cycles in execution graphs. If the outcome of a test is observed, we conclude that the cycle from which it is generated does not actually forbid the outcome.

In addition, to make the analysis of the results of such tests feasible, we generate our cycles so that there can be only one possible reason-in the model-why the outcome can be exhibited Of course, this practice supposes that the other relations from which a cycle is built are global. We check this assumption by generating cycles where all the relations are global in the model, and run them to check that their outcomes are not observed.

Candidate Relaxations

We wrote the diy testing tool to automatically generate litmus tests that exercise relations specified by the user. When given a certain sequence of relations, diy produces tests such that one of their executions contains at least one occurrence of the given sequence. Hence, if we want to check whether the external read-from maps are relaxed on a given machine, we specify rfe → to be relaxed to diy, following the concrete syntax we give in Fig. 9.

We write Po for a program order candidate relaxation and Dp for a dependency. We handle the communication relaxations as follows: we write Rf for a read-from, Ws for a write serialisation, Fr for a from-read. We also deal with barrier candidate relaxation: thus, we write Fence for a non-cumulative barrier, ACFence for an Acumulative one, BCFence for a B-cumulative one, and ABCFence for the sequence of an A-and a B-cumulative ones.

We specify if the two accesses related by the candidate relaxation access the same location by the letter s; we use the letter d if they access different locations. We specify the directions of the accesses related by the candidate relaxation, using W for write and R for read. Note that in the case of a dependency relation Dp, we just need to specify the direction of the target access, since dependency candidate relaxations always have a read as their source, following the definition of the dp → relation given in Sec. 2.2.

For communication candidate relaxations such as Rf, Fr or Ws, we specify whether the candidate relaxation is internal (resp. external)-i.e. relating two accesses that belong to the same processor (resp. distinct processors)-by the letter i (resp. e).

Thus Rfe represents a Note that some of the candidate relaxations might be redundant. For example PosWW (two write events to the same location in program, hence on the same processor) is a particular case of Wsi (internal write serialisation). Yet, we actually care for this redundancy, for two reasons. First, this helps us covering all possibilities in enumerating test cases for model exploration. Second, it helps us to spot precisely the reason why a given test might reveal a bug in a hardware implementation. In practice, the diy tool takes as input a configuration file such as the one in Fig. 10. This configuration file forces diy to generate tests in Power assembly up to 4 processors, as specified by the -arch PPC and -nprocs 4 arguments, so that the number of relations involved in the generated cycles is 6 at most, because of the -size 6 argument. Moreover, the candidate relaxations Fre (external from-read map) and DpdR (data dependency between two reads from distinct locations) are considered global, and Rfe is considered relaxed, as specified by the -safe Fre DpdR and -relax Rfe arguments. Finally, all the tests generated by diy running on this configuration file will have the prefix rfe in their name, followed by a fresh number, as specified by the -name rfe argument.

The tool outputs x86 or Power assembly tests. More precisely, the tool internally generates cycles from the candidate relaxations supplied as argument to the -safe and -relax specifications, up to the specified bounds on cycle length and number of processors. Each cycle then commands the generation of one test.

Exercising One Relaxation at a Time

So as to make the analysis of the testing results feasible, we focus on tests which exercise a single weakness of the memory model at a time. Hence, if the outcome of a given test is exhibited, we know that the feature we tested is used by the machine on which we ran the test.

For example, suppose that we modify the test of Fig. 7 and impose dependencies between the pairs of reads on P 0 and P 1 , so that these dependencies are global, e.g. by being included in In this case the only reason why the specified outcome may arise is the nonglobality of external read-from maps. Hence, the test of Fig. 11 is significant to check whether an architecture relaxes the atomicity of stores. More generally, we say that a test built from a cycle containing global relations only and a relation r targets r, because it can exhibit its outcome only because of r being relaxed. We shall also make use of tests built from global relations only, such a test is called a safe test.

Cycle Generation

The input to diy must specify which candidate relaxations are to be assumed not relaxed (considered global, or safe) and which are to be investigated. When given a pool of safe candidate relaxations, a single potential relaxation to be investigated, and a size n (i.e. the number of arrows in the cycle, e.g. [START_REF] Ahamad | The Power of Processor Consistency[END_REF] for the iriw test of Fig. 7), diy generates cycles up to size n that contains at least one occurrence of the nonglobal candidate relaxation. If no non-global candidate relaxation is specified, diy generates cycles up to size n that contain the specified global candidate relaxations.

We do not generate tests for all these cycles: we eliminate some sequences of candidate relaxations. First, we eliminate any sequence of two candidate relaxations when the target of the first one is incompatible with the source of the second one: for example, we eliminate a sequence

Rfe

-→;

Rfe -→ because the target of the first Rfe -→ is a read, whereas the source of the second one is a write. Notice that no assembly program exists that corresponds to such cycles. However, eliminating impossible sequences early accelerates the production of cycles. More significantly, diy eliminate some additional sequences of candidate relaxations: As a result, we do not generate all cycles up to a given size. However, the executions associated to the cycles we discard (for example a cycle involving a sequence [Fr ;Ws ] feature other shorter cycles (the cycle where [Fr ;Ws ] is reduced to Fr ), which are generated.

Consider for example the test given in Fig. 12(a), which corresponds to the test of Fig. 1(a), where we added a new processor holding the store (e) y ← 2. In this case, the final state of interest to us is still the one specified in Fig. 1, i.e. r1=0; r2=0;. This final state corresponds to the execution witness given in Fig. 12 Fre -→ (a), from which we generate the test of Fig. 1(a). Thus in such a case, we would generate only the test of Fig. 1(a), and not the test of Fig. 12(a).

Code Generation

diy interprets a sequence of candidate relaxations as a cycle from which it either computes a litmus test or fails. The final condition of a generated test is a conjunction of equalities on the values held by registers and memory locations in the final state, which ensures that at least one of the execution witnesses of this test includes a cycle following the input sequence.

Algorithm

Test generation performs the following successive steps:

1. We map the edge sequence to a circular double-linked list. The cells represent memory events, with direction, location, and value fields, together with the edge starting from the event. This list represents the input cycle and will appear in at least one of the execution witnesses of the produced test. 2. A linear scan sets the directions (write or read) of the events, by comparing each target direction with the following source direction. When they are equal, the in-between cell direction is set to the common value; otherwise (e.g. Rfe; Rfe), the generation fails. 3. We pick an event e which is the target of a candidate relaxation specifying a location change. If there are none, the generation fails. Otherwise, a linear scan starting from e sets the locations of each event. At the end of the scan, if e and its predecessor have the same location (e.g.

Rfe

-→ e PodRW -→ ), the generation fails, since we picked e to correspond to a location change. 4. We cut the input cycle into maximal sequences of events with the same location, each being scanned w .r .t. the cycle order: we give the value 1 to the first write in this sequence, 2 to the second one, etc. For each location in cycle, the sequence of values 0, 1, etc. defines a certain write serialisation order, which the final condition of test will characterise (step 7 below). 5. We define significant reads as the sources of fr → edges and the targets of rf → edges. We associate each significant read with the write on the other side of the edge. In the rf → case, the value of the read is the one of its associated write. In the fr → case, the value of the read is the value of the predecessor of its associated write in ws →, i.e. by construction the value of its associated write minus 1 (see step 4). Non-significant reads do not appear in the test condition. 6. We cut the cycle into maximal sequences of events from the same processor, each being scanned, generating load instructions to (resp. stores from) fresh registers for reads (resp. writes). We insert some code implementing a dependency in front of events targeting dp → and the appropriate barrier instruction for events targeting fenced → edges. We build the initial state at this step: stores and loads take their addresses from fresh registers, and their contents (addresses of memory locations) are defined in the initial state. Part of the final condition is also built: for any significant read with value v resulting in a load instruction to register r, we add the equality r = v. 7. We complete the final condition to characterise write serialisations. The write serialisation for a given location x is defined by the sequence of values 0 (initial value of x), . . . , n, where n is the last value allocated for location x at step 4.

If n is 0 or 1 then no addition to the final condition needs to be performed, because the write serialisation is either a singleton or a pair. If n is 2, we add the equality x = 2. Otherwise (n > 2), we add an observer to the program, i.e. we add a thread performing n loads from x to registers r1, . . ., rn and add the equalities r1 = 1 ∧ . . . ∧ rn = n to the final condition.

Example

We show here how to generate a Power litmus test from a given cycle of candidate relaxations by an example. We write for the information not yet set by diy: is an undetermined event, W a write with as-yet unset location and value, and Rx a read from x with undetermined value.

1. Consider e.g. the input cycle, issued by diy's cycles generation phase, with the input being the configuration file given in Fig. 10:

(a) Rfe -→ (b) DpdR -→ (c) Fre -→ (d) Rfe -→ (e) DpdR -→ (f ) Fre -→ (a)
2. A linear scan sets the directions from the edges. Observe e.g. the last edge;

Fre -→ requires a R source and a W target:

(a)W Rfe -→ (b)R DpdR -→ (c)R Fre -→ (d)W Rfe -→ (e)R DpdR -→ (f )R Fre -→ (a)

As

DpdR -→ specifies a location change, we pick (c) to be the first event and rewrite the cycle as:

(c)R Fre -→(d)W Rfe -→(e)R DpdR -→ (f )R Fre -→(a)W Rfe -→(b)R DpdR -→ (c)
We set the locations starting from (c), with a change of location e.g. between (e) and (f ) since 5. All the reads are significant here; we set their values according to step 5:

(c)Rx0 Fre -→(d)W x1 Rfe -→(e)Rx1 DpdR -→ (f )Ry0 Fre -→(a)W y1 Rfe -→(b)Ry1 DpdR -→ (c)
6. We generate the litmus test given in Fig. 11 for Power according to the steps 6 and 7 given in Sec. 4.6.1. For example on P 0 , we add a xor instruction between the instructions lwz r1,0(r2) and lwzx r4,r3,r5 associated with the events (b) and (c) to implement the dependency required by the DpdR -→ relation between them. The events (d) and (e), associated respectively to stw r1,0(r2) on P 1 and lwz r1,0(r2) on P 2 , are specified in the cycle to be in rfe →. Hence, we specify in the final state that the register r1 on P 2 holds finally 1. Indeed the store associated with (d) writes 1 into the address x addressed by r2 on P 1 , since the contents of the register r1 on P 1 is 1 (because of the preceding li r1, 1 instruction). Since (d) rfe → (e), the load associated with (e) on P 2 reads the value 1 from the address x addressed by r2, and writes 1 into the register r2.

The test in Fig. 11 is a Power implementation of iriw [START_REF] Boehm | Foundations of the C++ Concurrency Memory Model[END_REF] with dependencies. It can be obtained by running diy on the configuration file given in Fig. 10.

Coverage

Given a test generation tool such as diy, one should ask in what sense it provides good coverage and whether it generates useful tests.

One way to assess coverage is to check that it can generate 'classical' litmus tests in the literature. We just explained how one can generate the iriw

rwc P 0 P 1 P 2 (a) x ← 1 (b) r1 ← x (d) y ← 1 (c) r2 ← y
(e) r3 ← x Observed? 1:r1=1; 1:r2=0; 2:r3=0 Fig. 13 The rwc Test and a Candidate Execution

wrc P 0 P 1 P 2 (a) x ← 1 (b) r1 ← x (d) r1 ← y (c) y ← 2
(e) r2 ← x Observed? 1:r1=1; 2:r1=2; 2:r2=0; from [START_REF] Boehm | Foundations of the C++ Concurrency Memory Model[END_REF]. The rwc test of [START_REF] Boehm | Foundations of the C++ Concurrency Memory Model[END_REF], given in Fig. 13 Fre -→, as one can deduce from the execution given in Fig. 13(b). The wrc test of [START_REF] Boehm | Foundations of the C++ Concurrency Memory Model[END_REF], given in Fig. 14 Further, it generates all the variations of such tests with different choices of barriers and dependencies (e.g. 56 variations of wrc), and several families of tests that we have not previously seen. There are some interesting classes of tests that it does not generate, e.g. tests exhibiting observable register shadowing [START_REF] Adir | Information-Flow Models for Shared Memory with an Application to the PowerPC Architecture[END_REF], where we still rely on hand-written tests.

In general, diy will be able to generate any classical litmus test, as soon as this test can be generated from a cycle of candidate relaxations as defined in Sec. 4.2, and is not subject to the restrictions described in Sec. 4.5.

Comparing directly with the tests used within processor vendors is difficult, as those are commercially sensitive. However, the fact that we have found issues in deployed processors (as detailed in Sec. 5) is indicative.

Another sense in which it is demonstrably useful (indeed, indispensable) in practice has been in our model-building work, as illustrated for example in Sec. 6.2. Our initial explorations relied on several hundred hand-written tests, and it was hard to maintain consistency and ensure coverage of these. Using diy, while we still use some hand-written tests, most of our work can be done with automatically

→ r ′ ℓ lwsync → r ′′ ℓ 11/320M 0/960M 1/21M ACLwSyncdRR wℓ rfe → r ′ ℓ lwsync → r ′′ ℓ ′ 124/400M 0/7665M 2/21M BCLwSyncsWW wℓ lwsync → w ′ ℓ rfe → r ′′ ℓ 68/400M 0/560M 2/160M BCLwSyncdWW wℓ lwsync → w ′ ℓ ′ rfe → r ′′ ℓ ′ 158/400M 0/11715M 1/21M
Fig. 15 Selected Results of the diy Experiment Matching Our Model generated tests. In addition, as we explain in our more recent work on modelling the behaviour of Power multiprocessors [START_REF] Sarkar | Understanding Power Multiprocessors[END_REF], some key issues of the model were identified with these automatically generated tests.

5 Using diy: The Phat Experiment

We ran a case study for the diy tool, the Phat Experiment, from December 2009 to January 2010. We tested three Power machines, and present here a summary of the experimental results. More details can be found online at http://diy.inria. fr/phat.

Relaxations Observed on squale, vargas and hpcx

We used diy to generate 800 Power tests and run them up to 10 12 times each on three machines: squale, a 4-processor Power G5 running Mac OS X; hpcx, a Power 5 with 16 processors per node and vargas, a Power 6 with 32 processors per node, both of them running AIX. We ran the tests supposed to exhibit relaxations, i .e. the tests targeting any possible relation of Fig. 9 that our CAV 2010 model (see Fig. 22) does not include in ghb → . We observed all of them at least on one machine, except PodRW. Not observing a given candidate relaxation does not contradict our model, since our model should authorise at least all the behaviours that we observed on hardware. We give in Fig. 15 the number of times the outcome was observed (where M stands for million). For each relaxation observed on a given machine, we write the highest number of outcomes. When a candidate relaxation was not observed, we write the total of outcomes: thus we write e.g. 0/16725M for PodRR on vargas.

For a given candidate relaxation, we generated tests with diy by writing a simple configuration file setting its relax list to this candidate relaxation, and some of the candidate relaxations that we considered to be safe. We did not observe the PodRW relaxation; but the documentation does not specify this candidate relaxation to be safe, therefore we still consider it to be relaxed.

Safe Relaxations

Following our informal model, we assumed that the candidate relaxations corresponding to ws →, fr →, dependencies and barriers were global and tested this assumption by computing safe tests in which the input cycles only include candidate relaxations that we supposed global, e.g.

SyncdWW -→ ; Wse -→; SyncdWR -→ ; Fre -→.
For each machine, we observed the number of runs required to exhibit the least frequent relaxation (e.g. 160M for BCLwSyncsWW on vargas), and ran the safe tests at least 20 times this number. The outcomes of the safe tests have not been observed on vargas and squale, which increases our confidence in the safe set we assumed.

However, hpcx does exhibit non-SC behaviours for some A-cumulativity tests (albeit rarely), including classical tests [START_REF] Boehm | Foundations of the C++ Concurrency Memory Model[END_REF] such as iriw with sync instructions on P 0 and P 1 . These results are in contradiction with our model. We summarise these contradictions in Fig. 16.

We understand that this is due to a rare erratum in the Power 5 implementation. IBM is providing a software workaround, replacing the sync barrier by a short code sequence [Personal Communication], and our testing suggests that this does regain SC behaviour for the examples in question (e.g. with 0/4e10 non-SC results for iriw). We understand also that Power 6 is not subject to the erratum, which is consistent with our testing on vargas, and that it should not affect the correctness of code using conventional lock primitives.

The CAV 2010 Axiomatic Power Model

In the light of the black-box experimental testing described in Sec. 5, we have instantiated the formalism of Sec. 2 for Power. The resulting model (which we refer to as the CAV 2010 model) captures several important aspects of the processor's behaviour:

it describes the lack of store atomicity on Power, despite being in the simple global-time style of our framework rather than the per-processor-timeline style implied by the architecture text; it also models the thread-local ordering relaxations we observe; and it models A-cumulative barriers [25].

→ m 2 (m 1 , m 2 ) ∈ ctrl → ∪ isync → ∪ dd → ∪ ( po-loc → ∩ (W × R)) + ∩ (R × M) 6.
The model is sound (modulo the anomalies described in the previous section) with respect to all our experimental results for Power G5, 5, and 6. However, for some of the Power barriers it is weaker than one might like, and for some examples it appears to be stronger than the architectural intent. We discuss this in detail in the next section. Moreover, being primarily based on black-box testing, its relationship to microarchitectural views or the architecture specifications of the processors is less clear than one might like. Accordingly, we do not regard it as definitive, but as a necessary step towards more definitive models.

Auxiliary Definitions

To define the CAV 2010 model (more specifically, to specify its preserved program order relation), we first need some auxiliary definitions to describe how dependencies and barriers arise from the instruction semantics. We give in Fig. 18 a table of the fragment of the Power instruction set that we use to describe the forthcoming examples.

Register Events

We first add register events to reflect register accesses [START_REF] Sarkar | The Semantics of x86-CC Multiprocessor Machine Code[END_REF]. Loads and stores now yield additional register events, as depicted in Fig. 19.

For example, consider two registers r1 and r2, such that r1 initially holds the value 0, r2 initially holds an address x, and x holds the value 1. In this case, an instruction lwz r1,0(r2) creates a read event Rr2x from register r2, with label (b) in Fig. 19. This event reads the address x in r2; this leads to a read event Rx1 from x labelled (a) in Fig. 19. The event (a) was previously the only event we considered. Finally, the value read from x by the event (a) being 1, the lwz

[lwz r1,0(r2)] (a) R x 1 (c) W r1 1 (b) R r2 x iico iico rf rf rf [stw r1,0(r2)] (a) W x 1 (b) R r1 1 (c) R r2 x rf iico iico rf rf
Fig. 19 Semantics of lwz and stw r1,0(r2) creates a write event W r11 to register r1 with value 1, labelled (c) in Fig. 19.

Similarly, consider two registers r1 and r2, such that r1 initially holds the value 1, r2 initially holds an address x, and x holds the value 0. In this case, an instruction stw r1,0(r2) creates a read event Rr2x from register r2, with label (c) in Fig. 19. This event reads the address x in r2. In parallel, the store creates a read event Rr11 from r1, reading 1, labelled (c) in Fig. 19. Finally, the value read from r1 by the event (b) being 1, the stw r1,0(r2) creates a write event W x1 to x with value 1, labelled (a) in Fig. 19. The event (a) previously was the only event we considered.

Intra-Instruction Causality An execution witness now includes an additional intrainstruction causality relation

iico → , as in [START_REF] Sarkar | The Semantics of x86-CC Multiprocessor Machine Code[END_REF][START_REF] Alglave | The semantics of Power and ARM multiprocessor machine code[END_REF]. For example, executing the load lwz r1, 0(r2)-which semantics is given in Fig. 19 (r2 holding the address of a memory location x containing 1)-creates three events (a) R r2 x, (b) R x 1 and (c) W r1 1, such that (a) Stores are less constrained, as depicted in Fig. 19. Indeed the read events (b) and (c) may be performed independently. However, the write event (a) determines its target x and its value 1 from the reads Read-From Map Naturally, rf → now also relates register events: we write rf-reg → the subrelation of rf → relating register stores to register loads that read their values.

Commit Events

We also add commit events in order to express branching decisions. We write C for the set of commits, and c for an element of C.

Consider for example the test given at the left of Fig. 20, written in PowerPC assembly. Suppose that the register r5 initially holds the address x, and the register r6 the address y. The lwz r1,0(r5) at line (1) and the stw r2,0(r6) at line ( 4) are separated at lines (2)-(3) by a compare and branch sequence, written cmpwi r1,0 then bne L0.

In the execution of this test, given at the right of Fig. 20, the lwz r1,0(r5) leads to the read event Rx0 from x labelled (a). The stw r2,0(r6) leads to the write event W y1 to y labelled (b). At runtime, the compare instruction of line (2) yields equality and writes its result 2 (value 2 encodes equality) in the control register CR0, as depicted by the event (f ). The conditional branch instruction reads CR0 (read event (g)) whose value determines the branching decision (commit event (h)): bne being "branch not-equal", the branch is not taken. Observe that the execution itself of the store at line (4) depends upon the branching decision. This is depicted in the execution we give here by the events yielded by this store being present and following the commit event (h) in program order. To summarise, we witness a PPC ctrl { 0:r5=x; 0:r6=y;0:r2=1; x=0; y=0; } P0 ; (1) lwz r1,0(r5) ;

(2) cmpwi r1,0 ; (3) bne L0 ; (4) stw r2,0(r6) ; L0:

;

[lwz r1,0(r5)] [cmpwi r1,0] [bne L0] [stw r2,0(r6)] (a) R x 0 (d) W r1 0 (b) W y 1 (c) R r5 x (e) R r1 0 (f ) W CR0 2 (g) R CR0 2 (h) C o mmit (i) R r2 1 (j) R

Barrier Events

We add barrier events in order to indicate the presence of a barrier in the code. We handle three barrier instructions : isync, sync and lwsync. The sync barrier is Power's heavyweight barrier, sometimes written hwsync. The lwsync barrier is a lightweight version of the sync barrier. The isync barrier is even lighter, and mainly used after branching instructions. We distinguish the corresponding events by the eponymous predicates, is-sync, is-lwsync, and is-isync.

Consider for example the test given at the left of Fig. 21, written in PowerPC assembly. Suppose that the register r5 initially holds the address x, and the register r6 the address y.

The lwz r1,0(r5) at line (1) and the lwz r2,0(r6) at line ( 5) are separated at line (2) by a compare instruction, written cmpwi r1,0, which influences the taking of the following branch at line [START_REF] Adir | Information-Flow Models for Shared Memory with an Application to the PowerPC Architecture[END_REF], written bne L0. The branch is followed by an isync barrier at line (4).

In the execution of this test we give at the right of Fig. 21, the lwz r1,0(r5) at line (1) leads to the read event Rx0 from x labelled (a). The lwz r2,0(r6) at line [START_REF] Adve | Shared Memory Consistency Models: A Tutorial[END_REF] leads to the read event Ry1 from y labelled (b). These two instructions are separated by a branch followed by an isync. This is depicted in the execution we give here by the commit event labelled (h), in po → with the isync event labelled (i). Hence the read (a) from x and the read (b) from y are globally ordered by the isync barrier, as depicted by the isync → arrow between them. Notice that the isync → notation can be slightly misleading, since an isync barrier alone between two reads does not suffice to enforce global ordering. Instead, the global ordering results from the combination of the the data dependency from the read (a) to the commit (h) and from the presence of the isync barrier between the commit (h) and the second read (b). In Fig. 21, we only depict the ordering between (a) and (b), for this corresponds to the semantics of the isync → relation as defined in Fig. 22.

Description of the Model

We now describe the preserved program order, global reads-from maps, and barrier relation of the CAV 2010 Power model. The full definition of this model is collected in Fig. 22.

Preserved Program Order

We present in Fig. 22 ) of [25, p. 661] which allow loads to be speculated if no isync is added after the branch but prevents stores from being speculated in any case.

Data Dependencies More precisely, we consider that there is a data dependency between two events, written m 1 dd → m 2 , when:

they are in rf-reg → , i .e. m 1 is a register write and m 2 a register read reading from m 1 , or they are in iico → , i .e. they both come from the same instruction and the execution of m 2 depends on m 1 , e.g. when using the value m 1 read, or there is a path of rf-reg

→ ∪

iico → between m 1 and m 2 .

Control Dependencies We consider that there is a control dependency between two events, written m 1 ctrl → m 2 , when:

m 1 is a read, -m 2 is a write, and there exists a commit event c between them in the program order, such that c has a data dependency on m 1 .

If there is a control dependency between two events m 1 and m 2 , it means that they form a read-write pair separated by a conditional jump, and that the condition of the jump is data-dependent on m 1 .

Two events separated by a conditional jump may be reordered if:

the first one is a write, or they are both reads, and there is no isync between the branch and the second read (c.f . Sec. 6.2.1, semantics of isync)

The test and the associated execution of Fig. 20 give an example of control dependency between the (a) associated to the lwz r1,0(r5) at line (1) and the write (b) associated to the stw r2,0(r6) at line [START_REF] Adir | Information-Flow Models for Shared Memory with an Application to the PowerPC Architecture[END_REF].

Semantics of the isync Barrier We now give the CAV 2010 model of the isync barrier. The ordering induced by isync is similar to a control dependency on readread pairs. We consider that two events m 1 and m 2 are ordered by an isync barrier when:

m 1 is a read, and there exists a commit event c in data dependency with m 1 , separated from m 2 by an isync barrier in the program order.

In particular, this means that two events m 1 and m 2 separated by an isync can be reordered if:

m 1 is a write, or there is no commit between m 1 and m 2 .

The test and the execution of Fig. 21 give an example of isync ordering between the read (a) associated to lwz r1,0(r5) at line [START_REF]AMD64 Architecture Programmer's Manual. Advanced Micro Devices[END_REF] and the read (b) associated to lwz r2,0(r6) at line [START_REF] Adve | Shared Memory Consistency Models: A Tutorial[END_REF].

All Together Finally, we consider that two events m 1 and m 2 are in Power's preserved program order, written m 1 ppo-ppc → m 2 when:

there is a control dependency between them, i .e. m 1 ctrl → m 2 , or they are ordered by an isync barrier, i .e. m 1 isync → m 2 , or m 1 is a read, and there is a path of

dd → ∪ ( po-loc → ∩ (W × R)) between m 1 and m 2 .
Resemblance to Sparc Relaxed Memory Order's Preserved Program Order The preserved program order that we suggest for Power is similar to the one of Sparc Relaxed Memory Order (RMO) [30, V9, p. 293]. Writing S(X) (resp. L(X)) when the memory transaction X is a store (resp. load), Sparc's documentation defines the dependence order as follows:

Dependence order is a partial order that captures the constraints that hold between instructions that access the same processor register or memory location. [. . . ] Finally, we take the intersection of (

dd → ∪ ( po-loc → ∩ (W × R)))
+ and R × W, exactly as in RMO [30, V9, p.295]. Writing M (X, Y ) when X and Y are separated by a barrier, and Xa when X accesses memory location a, Sparc's documentation defines the legality of a RMO memory order as follows: The first item indicates that RMO also only considers the dependency chains starting from a load, which explains why we take the intersection with R × M. + ∩ (R × M) part. However, we do not authorise control dependencies in such a chain. Indeed, consider the example given in Fig. 23, which we observed to be exhibited on a Power 5 for example.

A memory order [written <m] is legal [in RMO] if and only if: (1) X < d Y & L(X) ⇒ X <m Y [i .e. X
On P 0 , the lwz r1,0(r7) at line (1) is in control dependency with the stw r3,0(r9) at line [START_REF] Adve | Shared Memory Consistency Models: A Tutorial[END_REF], because of the compare and branch sequence between them (lines (2) to ( 4)). The lwz r2,0(r9) at line [START_REF] Ahamad | The Power of Processor Consistency[END_REF] is in data dependency with the lwzx r4,r10,r8 at line [START_REF] Alglave | The semantics of Power and ARM multiprocessor machine code[END_REF], because of the xor r10,r2,r2 between them, at line [START_REF] Alglave | A Shared Memory Poetics[END_REF].

Since the lwz r1,0(r7) at line (1) on P 0 reads 1 (see the final state, 0:r1=1), there is a rfe → between the stw r2,0(r7) at line (3) on P 1 and the lwz r1,0(r7) at line (1) on P 0 . Because of the A-cumulativity of the sync barrier on P 1 , the stw r1,0(r8) at line (1) on P 1 is in ab → with the lwz r1,0(r7) at line [START_REF]AMD64 Architecture Programmer's Manual. Advanced Micro Devices[END_REF]

on P 0 . dd → ( rf-reg → ∪ iico → ) + r ctrl → w ∃c ∈ C. r dd → c po → w r isync → e ∃c ∈ C. r dd → c ∧ ∃b. is-isync(b) ∧ c po → b po → e dp → ctrl → ∪ isync → ∪ dd → ∪ ( po-loc → ∩ (W × R)) + ∩ (R × M) ppo-ppc → dp → (a) Preserved program order m 1 sync → m 2 ∃b. is-sync(b) ∧ m 1 po → b po → m 2 m 1 ab-sync → m 2 m 1 sync → m 2 ∨ ∃r. m 1 rf → r ab-sync → m 2 ∨ ∃w. m 1 ab-sync → w rf → m 2 (b) Barrier sync m 1 lwsync → m 2 ∃b. is-lwsync(b) ∧ m 1 po → b po → m 2 m 1 ab-lwsync → m 2 m 1 lwsync → m 2 ∩ ((W × W) ∪ (R × M)) ∨ ∃r. m 1 rf → r ab-lwsync → m 2 ∧ m 2 ∈ W ∨ ∃w. m 1 ab-lwsync → w rf → m 2 ∧ m 1 ∈ R (c) Barrier lwsync ab-ppc → ab-sync → ∪ ab-lwsync → Power ( ppo-ppc → , ∅, ab-ppc → )
Fig. 22 The CAV 2010 Power Model { 0:r7=y; 0:r8=z; 0:r9=x; 0:r3=1; Since the lwzx r4,r10,r8 at line (8) on P 0 reads 0 (see the final state, 0:r4=0), there is a fr → between this load and the stw r1,0(r8) at line (1) on P 1 . Hence we have a cycle of relations as follows, starting from lwz r1,0(r7) at line (1) on P 0 (writing (i : j) for the instruction at line (j) on P i ):

(0 : 1) CtrldW -→ (0 : 5) PosWR -→ (0 : 6) DpdR -→ (0 : 8) Fre -→ (1 : 1) ACSyncdWW -→ (0 : 1)
Since the specified outcome is exhibited, we know that there is a subsequence of this cycle which is not global. The only possible relaxation here is the PosWR one between the stw r3,0(r9) at line ( 5) and the lwz r2,0(r9) at line [START_REF] Ahamad | The Power of Processor Consistency[END_REF]. If we added ctrl → to the transitive part of Power's ppo → , the outcome would be forbidden in our model. We deduce from this example that ctrl → cannot be included in such chains.

Read-From Maps

Internal Read-From Maps The internal read-from maps are not global, since Power allows store buffering. Running the test given in Fig. 24 Thus in this test, the only possible relaxation is rfi →. Since the outcome is exhibited, as shown in Fig. 15, we know that rfi → is actually relaxed on Power. Store buffering is a fairly common relaxation. Indeed, the models TSO, PSO, RMO and Alpha also relax their internal read-from maps, i .e. allow store buffering.

External Read-From Maps The external read-from maps are not global either, as revealed by running iriw with data dependencies (Fig. 11) on a Power machine. This test is associated with the cycle This is probably the main particularity of the Power architecture: the models SC, TSO, PSO, RMO and Alpha do not relax the atomicity of stores. Another model relaxing store atomicity may be Itanium [START_REF]A Formal Specification of Intel Itanium Processor Family Memory Ordering[END_REF]. However, we do not know whether Itanium could be described by the generic framework we presented in Sec. 2.

Barriers

The sync Barrier The sync barrier is defined in Fig. 22 (b) as a full A-and Bcumulative barrier. We saw in Cor. 1 that such a barrier restores SC from a weaker model.

The lwsync Barrier The lwsync barrier is defined in Fig. 22 (b). lwsync acts as sync except on store-load pairs, in both the base and cumulativity cases. The Power model presented here was based largely on black-box testing. It is, to the best of our knowledge and following reasonably thorough experiment, sound with respect to the Power implementations we have tested. We consider it a success: it is the first non-trivial attempt towards the formalisation of the Power architecture with cumulative barriers; is is also notable in being an axiomatic model of a non-multi-copy-atomic architecture in a global-time style. Moreover, our test generation demonstrably generates interesting and useful tests that can be used in the context of other models, and can be reused for other architectures (we have also applied it to x86).

However, as mentioned, we do not claim this model to be definitive. In particular, it gives weaker semantics for the Power lwsync barrier than it should, and (we have recently learnt) it gives stronger semantics than the architectural intent in some cases.

For the lwsync issue, consider the common programming idiom given at the left of Fig. 25 in C-like syntax: P 0 first stores the value 1 into the location x, and then communicates a pointer to x (by storing it into another location p); P 1 reads that pointer and dereference it. In the SC model, if P 1 reads x from p, one can be sure that dereferencing x will always yield 1 (i.e. will never yield 0, the initial contents of x). The Power documentation suggests that inserting a lwsync barrier between the two stores of P 0 suffices to forbid the non-SC behaviour, due to the effective address of P 1 second load depending on the value loaded by P 1 first load. Our model is unable to explain this, because our semantics for the lwsync barrier is rather weak.

To see this, consider the PowerPC example we give at the right of Fig. 25, which corresponds to the idiom, where we have replaced the "true" address dependency by a "false" one, whose effect is identical, according to the documentation. That example could, according to our Power model, exhibit the execution given in Fig. 26 since there is no cycle in ghb → . More specifically, the B-cumulativity of the lwsync The per-processor view of the memory promoted by the Power documentation helps to explain why the execution of Fig. 26 is guaranteed not to happen. Indeed, the definition of lwsync of the documentation specifies (since the pair ((a), (b)) is a write-write pair, hence an "applicable pair" for lwsync) that "the memory barrier ensures that [(a)] will be performed with respect to any processor [. . . ] before [(b)] is performed with respect to that processor [. . . ]." Hence the pair ((a), (b)) has to be seen in the same order by P 0 and P 1 , because there is a lwsync between (a) and (b). Therefore, if the read (c) on P 1 reads 1 from the write (b) on P 0 , then P 1 has also seen the write (a) to x on P 0 , hence we cannot have (d) fr → (a) as in Fig. 26. For the other issue, the model forbids the final result of a test R01 [START_REF] Sarkar | Understanding Power Multiprocessors[END_REF], which is apparently intended to be architecturally allowed. We have not observed that result in experimental testing, so this does not contradict the soundness of the model with respect to the implementations we have tested, but in principle might be an issue with respect to future Power implementations, which might permit that final result, so compilers and software verification work should not assume that it is forbidden.

More recently, we have built another Power model [START_REF] Sarkar | Understanding Power Multiprocessors[END_REF], based not just on black-box testing but also on extensive discussion with IBM staff about the relevant aspects of the microarchitecture and of the architectural intent. That model resolves both of these issues: as far as we know, it captures the architectural intent precisely, and (as far as we know) is also experimentally sound with respect to Power 6 and Power 7 implementations. However, to do so we had to abandon the attractive simplicity of the global-time axiomatic model presented here -the new model is in an abstract-machine style, with a microarchitectural flavour (e.g., with explicit speculation in the core), though abstracting from implementation detail as much as we can. That is both good and bad: the abstract-machine model may be more intuitive for practicing engineers, but is mathematically more complex to work with. Ideally, we would also have an equivalent axiomatic model.

Related Work

Formal memory models roughly fall into two classes: operational models and axiomatic models. Operational models, e.g. [START_REF] Yang | UMM: an Operational Memory Model Specification Framework with Integrated Model Checking Capability[END_REF][START_REF] Higham | Weak memory consistency models part I: Definitions and comparisons[END_REF], are abstractions of actual machines composed of idealised hardware components such as queues. They can be appealingly intuitive and offer a relatively direct path to simulation, at least in principle. Axiomatic models focus on segregating allowed and forbidden behaviours, usually by constraining various order relations on memory accesses; they are particularly well adapted for model exploration, as we do here. Several of the more formal vendor specifications have been in this style [START_REF]Alpha Architecture Reference Manual[END_REF]30,[START_REF]A Formal Specification of Intel Itanium Processor Family Memory Ordering[END_REF].

One generic axiomatic model related to ours is Nemos [START_REF] Yang | Nemos: A Framework for Axiomatic and Executable Specifications of Memory Consistency Models[END_REF]. This covers a broad range of models including Itanium as the most substantial example. Itanium is rather different to Power; we do not know whether our framework could handle such a model or whether a satisfactory Power model could be expressed in Nemos. By contrast, our framework owes much to the concept of relaxation, informally presented in [START_REF] Adve | Shared Memory Consistency Models: A Tutorial[END_REF]. As regards tools, Nemos calculates the behaviour of example programs w.r.t. to a model, but offers no support for generating or running tests on actual hardware.

Previous work on model-building based on experimental testing includes that of Collier [START_REF] Collier | Reasoning About Parallel Architectures[END_REF], Adir et al. [START_REF] Adir | Generating Concurrent Test-Programs with Collisions for Multi-Processor Verification[END_REF][START_REF] Adir | Information-Flow Models for Shared Memory with an Application to the PowerPC Architecture[END_REF], and Sarkar et al. [START_REF] Sarkar | The Semantics of x86-CC Multiprocessor Machine Code[END_REF][START_REF] Owens | A Better x86 Memory Model: x86-TSO[END_REF][START_REF] Sewell | x86-TSO: A rigorous and usable programmer's model for x86 multiprocessors[END_REF]. The former is based on hand-coded test programs and Collier's model, in which the cumulativity of the Power barriers does not seem to fit naturally. Adir et al. developed an axiomatic model for a version of Power before cumulative barriers [START_REF] Adir | Information-Flow Models for Shared Memory with an Application to the PowerPC Architecture[END_REF]; their testing [START_REF] Adir | Generating Concurrent Test-Programs with Collisions for Multi-Processor Verification[END_REF] aims to produce interesting collisions (accesses to related locations) with knowledge of the microarchitecture, using an architecture model as an oracle to determine the legal results of tests rather than (as we do) generating interesting tests from the memory model. Sarkar et al. developed models for the x86 based in part on litmus testing with hand-written tests, using a version of the same tool as we use here for running them on hardware.

Conclusion

We present here a general class of axiomatic memory models, extending smoothly from SC to very relaxed models. It even extends to a model for Power processors, which does not have store atomicity. This is despite the fact that our models are simple global-time models, without complex structures such as multiple write events per store [START_REF]A Formal Specification of Intel Itanium Processor Family Memory Ordering[END_REF], or a view order per processor [START_REF] Collier | Reasoning About Parallel Architectures[END_REF][START_REF] Adir | Information-Flow Models for Shared Memory with an Application to the PowerPC Architecture[END_REF]25,[START_REF]ARM Architecture Reference Manual (ARMv7-A and ARMv7-R)[END_REF]. Our principal validity condition is simple, just an acyclicity check of the global happens before relation. This check is already known for SC [START_REF] Landin | Race-free interconnection networks and multiprocessor consistency[END_REF], and recent verification tools use it for architectures with store buffer relaxation [START_REF] Hangal | TSOTool: A Program for Verifying Memory Systems Using the Memory Consistency Model[END_REF][START_REF] Burckhardt | Effective Program Verification for Relaxed Memory Models[END_REF].

Our model lends itself well to exploration by automatic and systematic test generation. This is a significant advance over reliance on hand-crafted litmus tests, the current state of the art. Our diy tool has discovered several interesting corner cases which would have been easy to miss in a less systematic exploration. We also believe that extensive tests of actual hardware is a crucial component of building axiomatic models, and we provide a tool suite for both generation and running of tests. Such testing can also discover problems of the implementation, and our testing revealed a rare Power 5 implementation erratum for barriers.

Our Power model captures key aspects of the behaviour of cumulative barriers. It can be used as a basis for reasoning, particularly about the placement of heavyweight barriers hwsync. However, we do not regard it as definitive: there are known tests for which the model is too weak w.r.t. our perception of the architectural intent (particularly involving the lightweight barrier lwsync) and also cases where it is too strong w.r.t. the architectural intent (though sound w.r.t. current implementations). A desirable direction for future work would be to develop an axiomatic model that is equivalent to our more recent abstract-machine model [START_REF] Sarkar | Understanding Power Multiprocessors[END_REF].

Fig. 1 A

 1 Fig. 1 A program and a candidate execution

  Fig. 3 The fr → relation is derived from ws → and rf →

Fig. 4 A

 4 Fig. 4 A program and its two different write serialisations

1 Fig. 5 A

 15 Fig. 5 A program and two possible read-from maps

rf→

  edges are not necessarily included in ghb → . Let us distinguish between internal (resp. external) rf →, when the two events in rf → are on the same (resp. distinct) processor(s), written rfi → (resp. rfe →) : w rfi → r w rf → r ∧ proc(w) = proc(r) and w rfe → r w rf

→ 2 . 5

 25 ) relation when given an execution witness. Thus, we have:A (ppo, grf , ab)We define ghb → as the union of the global relations: Validity of an execution w .r .t. an architecture We now add two sanity conditions to the above.

  to the same location in the program order, and require

ws→

  is a total order of the writes to x, we have (c) ws → (a). Similarly, the final value of r1 shows that the read (b) read its value from the write (a), hence (a) rf → (b). The uniproc check on this program formalises the fact that the cycle (a) rf → (b) po-loc → (c) ws → (a) invalidates this execution: (b) cannot read from (a) as it is a future value of x in ws →.

P

Fig. 6

 6 Fig. 6 Invalid executions according to the uniproc and thin criteria

Fig. 7

 7 Fig.7The iriw test and a non-SC execution

  . The non-cumulative property of the barrier (expressed formally by fenced → being included in the definition of Acumulative) ensures that none of the two pairs of reads can be reordered. The Acumulative property of the barrier (expressed formally by rf →; fenced → being included in the definition of A-cumulative) also ensures that the write (e) on P 2 (resp. (y) P 3 ) is globally performed before the second read (b) on P 0 (resp. (d) on P 1 ). Thus, we force a program to have an SC behaviour by fencing all pairs in po →. Yet, it would be enough to invalidate non-SC executions, by fencing only the po → pairs in the com → ∪ po → cycles of these executions. We believe the static analysis of [29] (based on compile-time approximation of com → ∪ po → cycles) applies to architectures relaxing store atomicity, if their barriers offer A-cumulativity.

  iriw

  Fig. 7 leads to the com → ∪ po → cycle depicted there. Conversely, that test can be built from the sequence The specified outcome ensures that the input cycle appears in at least one of the execution witnesses of the test. If that outcome is observed, then, in terms of our framework, at least one subsequence in the cycle is not global, i.e. not in ghb → : in the case of Fig. 7, either the po → or the rfe → relations might not be included in ghb → .

rfe→

  arrow and Fre a fre → arrow. The candidate relaxation DpdR should be read as (1) Dp, which means that we generate a dp → arrow, (2) R, which means that this arrow targets a read, and (3) d, which means that the two accesses have different source and target locations. For Power, we instantiate the barrier candidate relaxation Fence with either Sync or LwSync.

Fig. 10

 10 Fig. 10 Example Configuration File for diy

ppo→

  Fig. 11 iriw with dependencies in Power assembly

Fig. 12 A

 12 Fig. 12 A program and a candidate execution

  (b). More precisely, this final state corresponds to the cycle (a) a).Observe that the read from y at line (b) on P 0 is in fr → with the write (e) to y on P 2 , because of the final value of register r1. Moreover, in this particular execution, the write (e) to y on P 1 is in ws → before the write (c) to y on P 2 . Therefore, by definition of fr → and since ws → is transitive, we know that (b) fr → (c) as well. Thus, the final state corresponds to the shorter cycle (a) a), i.e. (a) PodWR -→ (b) Fre -→ (c) PodWR -→ (d)

DpdR-→

  specifies a location change: (c)Rx Fre -→(d)W x Rfe -→(e)Rx DpdR -→ (f )Ry Fre -→(a)W y Rfe -→(b)Ry DpdR -→ (c) 4. We cut the input cycle into maximal sequences of events with the same location (i.e. (c)(d)(e) and (f )(a)(b)), each being scanned w .r .t. the cycle order. The values then reflect the write serialisation order for the specified location:

Fig. 14

 14 Fig.14The wrc Test and a Candidate Execution

  (a) can be obtained from the cycle Rfe as shown by the execution of Fig. 14(b).

→

  relation between (a) and (b) indicates that the load instruction has to perform the read (a) from r2 before the read (b) from x. Before reading x from r2 via the event (a), the address x is undetermined. Similarly, (b) and (c) are related by iico → , since the write (c) determines the value it has to write into r1 from the value read by (b).

  (c) and (b) respectively, hence (b)

Fig. 20 A

 20 Fig. 20 A Test For Control Dependency in PowerPC Assembly

Fig. 21

 21 Fig. 21 An Example Use of the isync Barrier

  (a) the definition of ppo-ppc → , induced by lifting the ordering constraints of a processor to the global level (where ( r →) + stands for the transitive closure of a given relation r →). This is a formal presentation of the data dependencies ( dd →) and control dependencies ( ctrl → and isync →

( 3 )

 3 X and Y access the same memory location, and S(X) and L(Y ) are both true. [This corresponds to the po-loc → ∩ (W × R) part of Power's ppo → definition.] [. . . ] It is important to remember that partial ordering is transitive. The items (1) and (2) correspond to our ctrl → and dd → relations, while the item (3) corresponds to the po-loc → ∩ (W × R) part of Power's ppo → definition. Moreover, as mentioned in the excerpt above, that order should be transitive. Hence we take the transitive closure of the relation formed by the union of these two relations.

  Discussion of Power's ppo → We include in ppo → any chain of data dependencies and rfi → starting from a read, by the (( dd → ∪ ( po-loc → ∩ (W × R)))

  confirms this hypothesis. Indeed this test, generated by diy, proceeds from a cycle DpdR We know that dp → is global, since included in ppo → , and fr → is global as well.

Fre→

  is always considered global in our framework, an hypothesis which has not been invalidated by the experiment we present in Sec. 5. We also know that dp → is global in Power, since ppo → is equal to dp →. Therefore, the only possible relaxation in the test of Fig. 11 is rfe →. Since the specified outcome is exhibited as shown in Fig. 15, rfe → is relaxed.

7

  Discussion of the Model

Fig. 25 AFig. 26

 2526 Fig. 25 A Common Programming Idiom and a Corresponding Test in PowerPC Assembly

  Barrier constraints Architectures also provide barrier instructions, e.g. the Power We call a particular model of our class an architecture, written A (or A ǫ when ab → is empty). Let ppo (resp. grf , ab, ghb) be the function returning the

	sync (discussed in Sec. 3) to enforce ordering between pairs of events. We postulate
	a global relation	ab → gathering all such pairs.

Architectures ppo → (resp.

  . For example, in the cycle there can be several reasons why this cycle is not global: either relation between two reads is not preserved, or both. Hence, if we want to state precisely why a given outcome is exhibited, we need to pick one relation to test, for example

rfe →; po →; fre →; rfe →; po →; fre →, rfe → is not global, or the po → rfe →, and build a cycle where rfe → is the only non-global relation possible.

1 .

 1 For communication candidate relaxations (i.e. Ws, Fr and Rf), we do not generate the sequence [Ws ;Ws ] for it reduces to Ws in the model. Similarly, we do not generate the sequence [Ws ;Fr ], for it reduces to Fr in the model. Hence we generate only five sequences of communication candidate relaxations, namely Ws , Fr , Rf , [Ws ;Rf ] and [Fr ;Rf ]. 2. For program order candidate relaxations, we do not generate sequences [po 1 ;po 2 ] when the sequence is subsumed by another safe candidate relaxation (where po 1 and po 2 range over Po, Dp, Fence, and internal communication (i.e. Rfi, Fri and Wsi)). This means for example that, if FencedWR and Fence WW

	Init: x=0; y=0;
	P 0	P 1	P 2
	(a) x ← 1	(e) y ← 2	(c) y ← 1
	(b) r1 ← y		(d) r2 ← x
	Observed? r1=0; r2=0;

  Fig. 17Table of Power specific relations

						2.1
	sync	m 1	sync → m 2	pairs maintained by sync	6.2.3
	lwsync	m 1	lwsync → m 2	pairs maintained by lwsync	6.2.3

  (ra) let x be the address in ra; this instructions loads into rt from the address x + d p. 76 load word and zero indexed lwzx rt,ra,rb let xa be the address in ra and x b the address in rb; this instruction loads into rt from the address xa + x b ,rb let xa be the address in ra and x b the address in rb; this instruction stores from rs into the address xa + x b ,rb let va be the content of ra and v b be the content of rb; this instruction writes va xor v b into rdTable of the Power assembly instructions used in this paper

	Name	Code	Comment	Doc. [25] (p. in pdf)
	load word and zero	lwz rt,dp. 76
	store word	stw rs,d(ra) let x be the address in ra; this instruction stores	p. 81
			from rs into the address x + d
	store word indexed	stwx rs,rap. 81
	branch if not equal	bne L	checks if register cr0 (the same as the one	p. 63
			that indicates whether a stwcx. has succeeded)
			holds 0, if not branches to L
	compare word im-	cmpwi rx, v	compares the value in rx with v and writes 1 if	p. 102
	mediate		equal (resp. 0 if not) in cr
	xor	xor rd,rap. 107
	isync	isync	when placed after a bne, forms a read-write,	p. 661
			read-read non-cumulative barrier
	lwsync	lwsync	read-write, read-read and write-write A-and	p. 700
			B-cumulative barrier
	sync	sync	read-write, read-read, write-write and write-	p. 700
			read A-and B-cumulative barrier
	Fig. 18

  Two memory transactions [i .e. accesses] X and Y are dependence ordered, denoted by X < d Y , if and only if they are program ordered, [written] X <p Y , and at least one of the following conditions is true: (1) The execution of Y is conditional on X, and S(Y ) is true. [i .e. they are in control dependency: in particular, Y is a write.] (2) Y reads a register that is written by X. [This corresponds to our

	rf-reg → rela-
	tion.]

  and Y are in dependence order as defined above, and X is a read.] (2) M (X, Y ) ⇒ X <m Y [i .e. X and Y are separated by a barrier; we treat Xa <p Y a & S(Y ) ⇒ X <m Y [Y is a write, and they are both relative to the same memory location a. This corresponds to the fact that we consider

	this via	ab →, not	ppo → .]
	(3)

wsi → and fri → to be global.]

  Fig. 24 A diy PowerPC Test for the Rfi Relaxation

	PPC rfi000
	"DpdR Fre Rfi DpdR Fre Rfi"
	Cycle=DpdR Fre Rfi DpdR Fre Rfi
	Relax=Rfi
	Safe=Fre DpdR
	{
	0:r2=x; 0:r6=y;
	1:r2=y; 1:r6=x;
	}
	P0	| P1		;
	li r1,1	| li r1,1	;
	stw r1,0(r2) | stw r1,0(r2) ;
	lwz r3,0(r2) | lwz r3,0(r2) ;
	xor r4,r3,r3 | xor r4,r3,r3 ;
	lwzx r5,r4,r6 | lwzx r5,r4,r6 ;
	exists
	(0:r3=1 /\ 0:r5=0 /\ 1:r3=1 /\ 1:r5=0)
	1:r7=y; 1:r8=z; 1:r1=1; 1:r2=1;
	}
	P0		| P1	;
	(1) lwz r1,0(r7)	| stw r1,0(r8) ;
	(2) cmpwi r1,0	| sync	;
	(3) beq L0		| stw r2,0(r7) ;
	(4) L0:		|	;
	(5) stw r3,0(r9)	|	;
	(6) lwz r2,0(r9)	|	;
	(7) xor r10,r2,r2 |	;
	(8) lwzx r4,r10,r8 |	;
	exists (0:r1=1 /\ 0:r4=0)
	Fig. 23 Contradiction with the View Order Formulation

INRIA

University of Cambridge

Oxford University

http://diy.inria.fr/

http://diy.inria.fr/wmm/

Acknowledgements We thank Damien Doligez and Xavier Leroy for invaluable discussions and comments, Assia Mahboubi and Vincent Siles for advice on the Coq development, Thomas Braibant, Jules Villard and Boris Yakobowski for comments on a draft, and the anonymous referees for comments on the presentation. We thank the HPCx (UK) and IDRIS(.fr) high-performance computing services. We acknowledge support from EPSRC grants EP/F036345, EP/H005633, and EP/H027351/1, and ANR grant ANR-06-SETI-010-02.