Cristian F • Coletti
email: cristian.coletti@ufabc.edu.br

Pierre Tisseur
email: pierre.tisseur@ufabc.edu.br

Pierre And Tisseur

Invariant Measures and Decay of Correlations for a Class of Ergodic Probabilistic Cellular Automata

Keywords: Probabilistic cellular automata, Invariant measures, Duality Decay of correlation Mathematics Subject Classification (2000) 28D99, 37A25, 60J05, 60J85, 60K35

We give new sufficient ergodicity conditions for two-state probabilistic cellular automata (PCA) of any dimension and any radius. The proof of this result is based on an extended version of the duality concept. Under these assumptions, in the one dimensional case, we study some properties of the unique invariant measure and show that it is shift-mixing. Also, the decay of correlation is studied in detail. In this sense, the extended concept of duality gives exponential decay of correlation and allows to compute explicitily all the constants involved.

Introduction

Probabilistic cellular automata (PCA) are discrete time Markov processes which have been intensely studied since at least Stavskaja and Pjatetskii-Shapiro [START_REF] Stavskaja | Homogeneous networks of spontaneously active elements[END_REF] (1968). This kind of processes have as state space a product space X = A G where A is any finite set and G is any locally finite and connected graph. In this work we will focus our attention on G = Z d and A = {0, ..., n} for some integer n ≥ 1. We may regard a PCA as an interacting particle system where particles update its states simultaneously and independently. Recall that a PCA is ergodic if there exists only one invariant measure µ and starting from any initial measure µ 0 the system converges to µ.

The aim of this paper is to use duality principles to study the ergodicity of two-states PCA. More precisely our work gives new sufficient ergodicity conditions for the expression of the PCA's local transition probabilities (see Theorem 2) and show that under these conditions the invariant measure is shift-mixing with exponential decay of correlation. Relations between the PCA and the dual process (see Lemma 4 and Lemma 2 ) also allow us to give a very simple expression of the constant of the decay of correlation as a function of the radius (of the PCA) and the transition probabilities of the PCA (see Theorem 3). Moreover the proof of Theorem 2 shows in detail how to compute the value of the invariant measure on cylinders. Results about the decay of correlation is an answer to a question raised in [START_REF] Lopez | Dualities for Multi-State Probabilistic Cellular Automata[END_REF].

The existence of a dual process satisfying the duality equation (see Definition 1 and Liggett [START_REF] Liggett | Interacting particle systems[END_REF]) gives useful information (problems in uncountable sets can be reformulated as problems in countable sets) on the PCA but is not always sufficient to prove that a PCA is ergodic. In [START_REF] Lopez | Dualities for Multi-State Probabilistic Cellular Automata[END_REF], Lopez, Sanz and Sobottka introduced an extended concept of duality (see Definition 2) and gave general results about ergodicity (see Theorem 1). They used this powerful general theory to give results on multi-state one-dimensional PCA of radius one and extended previous results about the Domany-Kinzel model (see [START_REF] Domany | Equivalence of cellular automata to ising models and directed percolation[END_REF] for an introduction and [START_REF] Konno | Dualities for a class of finite range probabilistic cellular automata in one dimension[END_REF] for extensions). Previously, in [START_REF] Konno | Self-duality for multi-state probabilistic cellular automata with finite range interactions[END_REF] Konno has given ergodicity conditions for multi-state one-dimensional PCA using self-duality equations.

Even if, in some cases, the existence of null transition probabilities allows to prove ergodicity of a certain class of PCA (see [START_REF] Konno | Dualities for a class of finite range probabilistic cellular automata in one dimension[END_REF] and [START_REF] Konno | Self-duality for multi-state probabilistic cellular automata with finite range interactions[END_REF]), it had been conjectured that in the one-dimensional case positive noise cellular automata are ergodic. However, P. Gacks, in 2000 , introduced a very complex counterexample (see [START_REF] Gacs | Reliable Cellular Automata with Self-Organization[END_REF] and [START_REF] Gray | A Reader's Guide to Gacs's "Positive Rates" Paper[END_REF]) for noisy deterministic cellular automata. In that case, the noisy one-dimensional cellular automata does not forget the past and starting from different initial distribution, the PCA may converge to different invariant measures. His result can be extended to noisy PCA with positive rates. This conjecture was formulated only in the one-dimensional case since in dimension 2 or higher, it is easier to show the existence of at least two invariant measures. For example the two dimensional Ising model [START_REF] Gray | A Reader's Guide to Gacs's "Positive Rates" Paper[END_REF] or the Toom example (see [START_REF] Toom | Stable an attractive trajectories in multicomponent systems[END_REF]) that exhibit eroder properties. From Theorem 2 there exists a subclass of attractive PCA (class C) where the noisy conjecture is verified (p(I r ) < 1 implies ergodicity).

In [START_REF] Lopez | Dualities for Multi-State Probabilistic Cellular Automata[END_REF], the authors explore some ergodic conditions for multi-state PCA. When the number of states is greater than 2, the conditions of ergodicity are rather restrictive in order to be able to give general results. More general ergodicity conditions are interesting (see [START_REF] Lopez | Dualities for Multi-State Probabilistic Cellular Automata[END_REF], Section 3.2) but seems to be very complex when the radius grows. In this paper, we restrict the study to the 2 states case, which allows to show more easily general results for PCA of any radius.

These sufficient ergodicity conditions can be compared to the Shlosman-Dobrushin condition applied to PCA (see [START_REF] Maes | Ergodicity of Probabilistic Cellular Automata: A constructive Criterion[END_REF] and [START_REF] Maes | When is an Interacting Particle System Ergodic?[END_REF]). In some examples (see section 3.1) our sufficient conditions induced by the concept of duality allow to show ergodicity and decay of correlations where the Dobrushin conditions can not be applied. Moreover, for some classes of ergodic PCA Theorem 3 gives greater constants for the decay of spatial correlation.

This paper is organized as follows. In section 2, we present the basic definitions, notations and some preliminary results. In section 3, we state the main results, Theorem 2 and Theorem 3. We prove Theorem 2 in section 4. We conclude the paper in section 5 with the proof of the decay of correlation.

2 Definitions, notations and preliminary results

Probabilistic Cellular Automata

We give a brief description of the theory of PCA.

Let A be a finite set and G a countable set. Let X = A G be endowed with the product topology. A probabilistic cellular automata is a discrete time Markov process on the state space X.

Let M (X) be the set of probability measures on X and F (X) the set of real functions on X which depend only on a finite number of coordinates of G.

The evolution of probabilistic cellular automata is given through their transition operator.

Definition 1 A local transition operator is a linear operator

P : F (X) → F (X)
such that P f ≥ 0 for all f ≥ 0 and P I = I, where I : X → X is the identity function.

Definition 2 A local transition operator is called independent if

P (ϕφ) = P (ϕ) P (φ)
for all ϕ, φ ∈ F (X) such that the finite subsets of G on which they depend do not intersect.

The independent local transition operators can be defined through the values p x (η, k) for x ∈ G, η ∈ X and k ∈ A, as

P f (η) = X f (σ) x∈G p x (η, dσ(x)), ∀f ∈ F (X),
where for all site x ∈ G, for all η, p x (η, .) is a probability measure on A.

The value p x (η, k), called transition probabilities, represent the probability that the sites x ∈ G takes the value k in the next transition if the present configuration of the system is η. For more details see Toom et al. [START_REF] Toom | Discrete local Markov Systems[END_REF], Maes and Shlosman [START_REF] Maes | Ergodicity of Probabilistic Cellular Automata: A constructive Criterion[END_REF] and Lopez and Sanz [START_REF] Lopez | Stochastic Comparison for general Probabilistic Cellular Automata[END_REF]. Let d ≥ 1 be an integer number, R a finite subset of Z d of cardinality |R| and f a map from A |R|+1 to [0, 1]. In the particular case G = Z d it follows from the discussion above that the discrete time Markov process η . = {η t (z) ∈ A : t ∈ N, z ∈ Z d } whose evolution satisfies

P [η t+1 (z) = a|η t (z + i) = b i , ∀ i ∈ R] = f (a, (b i ) i∈R ) ,
for all t ∈ N and z ∈ Z d is a well defined (discrete time) stochastic process which from now on will be called d-dimensional PCA. Here, P stands for the probability measure on A Z d induced by the family of local transition probabilities. Also, let E be the expectation operator with respect to this probability measure.

Let µ 0 be the initial distribution of the PCA. For any t ≥ 0, we call µ t the distribution of the process at time t. The measure µ t is defined on cylinder

u = N (Λ, φ) = {ξ ∈ A Z d : ξ(x) = φ(x) ∀ x ∈ Λ} for some fixed φ ∈ A Z d and Λ ⊂ Z d , |Λ| < ∞ by µ t (u) = v∈Ct µ 0 (v)P η0∈v {η t ∈ u},
where C t is the family of all cylinders of X on the coordinates of Λ ( the finite subset of Z d used to defined u).

In this paper the notation |Λ| will represent the cardinality of Λ when Λ is a finite subset of Z d . If U = N (Ξ, φ) is a cylinder set, the notation |U | will represent the cardinality |Ξ| of the set Ξ ⊂ Z d . In the one dimensional case we adopt the following notation: For any sequence of letters U = (u 0 , . . . ,

u n ) ∈ A n+1 , the set [U ] s = [u 0 . . . u n ] s := {x ∈ A Z |x(s) = u 0 , . . . , x(s + n) = u n } will be called cylinder and |U | = n + 1.

Two-state Probabilistic Cellular Automata

In order to simplify the notation we will focus our attention on two-state PCA, that is to say PCA η . on {0, 1} Z d . For any positive integer r, let us define

I r := {i = (i 1 , . . . , i d ) ∈ Z d : -r ≤ i 1 , . . . , i d ≤ r}.
Define a family of transition probabilities {p(J) : J ⊂ I r } by p(J) := P{η t+1 (z) = 1|η t (z + j) = 1 : j ∈ J}.

Note that any PCA with state space {0, 1} Z d is completely characterized by a positive integer number r called the radius of the PCA and the set of transition probabilities {p(J) : J ⊂ I r }.

The invariant probability measure

Definition 3 Let T be a measure-preserving transformation of a probability space (X, F, µ), where F is the σ-algebra generated by the cylinder sets on X.

We say that the probability measure

µ is T -mixing if ∀ U, V ∈ F lim n→∞ µ(U ∩ T -n V ) = µ(U )µ(V ).
Since the cylinder sets generate the σ-algebra F, it follows that the measure µ is T -mixing when the last relation is satisfied by any pair of cylinder sets U and V (for more details see [START_REF] Walters | An introduction to Ergodic Theory[END_REF]).

Duality

The concept of duality is a powerful tool in the theory of interacting particle system. It provides relevant information about the evolution of the process under consideration from the study of other simpler process, the dual process.

The reformulated problems may be more tractable than the original problems and some progress may be achieved. Now we give the (classical) definition of duality taken from [START_REF] Liggett | Interacting particle systems[END_REF].

if E η [H (η t , ζ)] = E ζ [H (η, ζ t )] for all η ∈ X and ζ ∈ Y .
Unfortunately, it is not true that every process has a dual. Recently, Lopez et al [START_REF] Lopez | Dualities for Multi-State Probabilistic Cellular Automata[END_REF] gave a new notion of duality which extends the previous one. More precisely, they gave the following definition.

E η0=x [H (η 1 , y)] = D(y)E ζ0=y [H (x, ζ 1 )] . (1.1)

Duality and sufficient conditions for ergodicity

In order to state our results in section 3, we need to give the spirit and some elements of the proof of the following Theorem, which appears in [START_REF] Lopez | Dualities for Multi-State Probabilistic Cellular Automata[END_REF].

Theorem

y ∈ Y} is dense in C (X), the set of continuous maps from X to R; ii) D(y) < 1 for any y / ∈ Θ, and
D := sup y∈Y:D(y)<1 {D(y)} < 1; iii) H(., θ) ≡ c(θ) for all θ ∈ Θ with D(θ) = 1; then η .

is ergodic and its unique invariant measure is determined for any

y ∈ Y by μ(y) = θ∈Θd(θ)=1 c(θ)P ξ0=y ξτ = θ , (1.2)
where τ is the hitting time of {θ ∈ Θ : D(θ) = 1} ∪ {S} for ξt and μ = lim t→∞ μt with

μt (y) = X H(x, y)dµ t (x).
Sketch of the proof. First recall that τ is the hitting time of the dual process ξ. entering an absorbing state θ ∈ Θ. If there exists a dual process ξ and a function H that satisfies the following (classical) duality equation

E η0=x H (η 1 , y) = E ξ0=y H x, ξ1 , (1.3) it is possible to show that μs (y) = X H(x, y)dµ s (x) = E ξ0=y [μ( ξs )]. If P{τ < ∞} = 1, it follows that lim s→∞ μs (y) = lim s→∞ θ∈ Θ E ξ0=y [μ( ξs )| ξt = θ, τ ≤ s]P ξ0=y { ξt = θ, τ ≤ s} + lim s→∞ E ξ0=y [μ( ξs )|τ > s]P ξ0=y {τ > s} = θ∈ Θ μ(θ)P ξ0=y { ξτ = θ}.
Finally, when the set of linear combinations of the set { H(., y)|y ⊂ Z d } is dense in C(X) (the set of continuous functions from X to R) the sequence (µ n ) n∈N converges in the weak* topology. Also, the limit measure µ does not depend on the initial measure µ 0 .

Hence, we have seen that the key point is to prove that P{τ < ∞} = 1. One way to show this, is to introduce the new type of duality (see Equation 1.1). If there exists a dual process ξ . with state space Y that verifies the new concept of duality (see Equation 1.1) then we can define a standard dual process ξ. with state space Ỹ = Y ∪ {S} and such that the set of all absorbing states is Θ = Θ ∪ {S} where Θ denote the set of all the absorbing states of ξ . . Here S is an extra absorbing state and the transition probabilities of ξ. satisfy

P ξ0=ỹ0 { ξ1 = ỹ1 } =    D(ỹ 0 )P ξ0= ỹ0 {ξ 1 = ỹ1 } , if ỹ0 , ỹ1 ∈ Y 1 -D(ỹ 0 ) , if ỹ0 ∈ Y, ỹ1 = S 1 , if ỹ0 = ỹ1 = S.
Taking H(x, y) = H(x, y) when y ∈ Y and H(x, S) = 0 we obtain that the dual process ξ. satisfies the standard duality equation 1.3 and that μ(S) = 0. Note that since D = sup y∈Y:D(y)<1 {D(y)} < 1, at each iteration the probability to enter the extra absorbing state S is positive and this implies the following result:

Lemma 1 Under the conditions of Theorem 1, for all integer i ≥ 1 one has

P(τ > i) ≤ D i .
Proof. By the Markov property we have that

P ξ0= ỹ0 {τ > i} ≤ D × P ξ0= ỹ0 {τ > i -1}.
Then, the result follows by using the mathematical induction principle. 2

Note that Lemma 1 implies that P{τ < ∞} = 1 which finishes the proof of Theorem 1.

2 Before stating the main results of this paper, we introduce one more piece of notation: let ∞ 1 ∞ denote the all one configuration, i.e.

∞ 1 ∞ = (1 Z d (x)) x∈Z d . Analougsly, ∞ 0 ∞ denote the all zero configuration.

Main Results and Examples

A PCA of radius r is called attractive if for any J ⊂ I r and j ∈ I r we have p(J ∪ {j}) ≥ p(J). We consider here the following subclass of attractive PCA. For any r ∈ N, let ℘(I r ) be the set of all subsets of I r . We say that a two-state PCA of radius r belongs to C if its transition probabilities satisfy p(J) = J ′ ⊂J λ(J ′ ) where λ is some map from ℘(I r ) → [0, 1).

The definition of the class C is constructive. The following Proposition gives sufficient conditions for an attractive PCA to belong to C. Theorem 2 Let η . be a two-states d-dimensional probabilistic cellular automaton of radius r that belongs to C. If p(I r ) < 1 then η . is an ergodic PCA and there exists a dual process ξ which satisfy equation 1.1. Moreover, for any cylinder set U we can find

(α k ∈ Z) k∈K and (Y (k) ⊂ Z d ) k∈K with |K| < ∞ such that µ(U ) = k∈K α k ∞ l=1 P ξ0=Y (k) {ξ l = ∅|ξ l-1 = ∅} .
Remark 1 Note that in some cases it is possible to exchange the role of the two states (0 ↔ 1) in order to show ergodicity using the previous results.

Corollary 1 Under the conditions in Theorem 2 we have that if λ(∅) = 0 then the unique invariant measure is δ 0 , where δ 0 is the Dirac measure on ∞ 0 ∞ . Analogously, we have that if λ(∅) = 1 then the unique invariant measure µ is δ 1 , where δ 1 is the Dirac measure on ∞ 1 ∞ .

Theorem 3 Let η . be a one-dimensional probabilistic cellular automaton ∈ C of radius r with p(I r ) =: D ∈ [0, 1). Then, the unique invariant measure µ is shift-mixing. Also, if D = 0, for any pair of cylinders

[U ] 0 = [u 0 . . . u k ] 0 , [V ] 0 = [v 0 . . . v k ′ ] 0 and t ≥ |U | + |V | we have |µ([U ] 0 ∩ σ -t [V ] 0 ) -µ([U ] 0 ) × µ([V ] 0 )| ≤ exp (-a × t) × K(U, V ),
where σ is the shift on {0, 1} Z , a = 1/2r×ln (1/D) and K(U, V ) is a constant depending only on U , V , D and r.

Remark 2 This last result can be extended to d-dimensional PCA.

Examples and comparison with known results

The Domany-Kinzel model

This is a one-dimensional PCA η . of radius r = 1 introduced in [START_REF] Domany | Equivalence of cellular automata to ising models and directed percolation[END_REF] with transition probabilities

P{η t+1 (z) = 1|η t (z -1, z, z + 1) = 000 or 010} = p(∅) = p({0}) = a 0 , P{η t+1 (z) = 1|η t (z -1, z, z + 1) = 100 or 110} = p({-1}) = p({-1, 0}) = a 1 , P{η t+1 (z) = 1|η t (z -1, z, z + 1) = 001 or 011} = p({1}) = p({0, 1}) = a 1 and P{η t+1 (z) = 1|η t (z -1, z, z + 1) = 101 or 111} = p({-1, 1}) = p({-1, 0, 1}) = a 2 ,
where, for any subset V ⊂ Z, η(V ) ∈ {0, 1} V denote the restriction of a configuration η ∈ {0, 1} Z to the set of positions in V .

Using Proposition 1 we obtain that η . ∈ C when p({-1, 1}) ≥ p({-1}) + p({1})p(∅), which is equivalent to the condition a 2 ≥ 2a 1a 0 . From Theorem 2 the PCA η . is ergodic if p(I r ) = p({-1, 0, 1}) = a 2 < 1. From Theorem 3 the unique invariant measure is shift-mixing with exponential decay of spatial correlation such that for any pair of cylinders [U ] 0 and [V ] 0 and for all t

≥ |U | + |V | we obtain |µ([U ] 0 ∩ σ -t [V ] 0 ) -µ([U ] 0 ) × µ([V ] 0 )| ≤ K exp (-(1/2 ln (1/a 2 ))t),
where K can be explicitly computed (see the end of the Proof of Theorem 3). Using Theorem 2 we can compute, for example, the measure of the cylinder [01] 0 which is

µ([01] 0 ) = µ([1] 1 ) -µ([11] 0 ) = μ({1}) -μ({0, 1}) = ∞ t=1 P ξ0={1} {ξ t = ∅|ξ t-1 = ∅} + ∞ t=1 P ξ0={0,1} {ξ t = ∅|ξ t-1 = ∅},
where ξ . is the associated dual process.

Two-dimensional example

Let η be a two-state, two-dimensional PCA of radius one. In this case are the binomial coefficients. This PCA belongs to C since for any J ⊂ I 1 we can write λ(J) = α and obtain that P (J) = J ′ ⊂J λ(J ′ ). This PCA is a kind of generalization to dimension 2 of the Domany-Kinzel model (each site has the same weight) with only one parameter. The sufficient ergodicity condition is p(I r ) < 1 which implies that α × 2 9 < 1 (α < 2 -9 ) and the constant of decay of spatial correlation is a = 1 2 ln(1/(2 9 × α)).

I 1 = {(l, k)| -1 ≤ l, k ≤ 1}

Comparison with Dobrushin condition

In [START_REF] Dobrushin | Markov processes with a large number of locally interacting components: Existence of a limit process and its ergodicity[END_REF], Dobrushin gives sufficient ergodicity conditions for interacting particule systems. Using our notation, these conditions applied to PCA can be translated as γ < 1 (see [START_REF] Maes | Ergodicity of Probabilistic Cellular Automata: A constructive Criterion[END_REF] and [START_REF] Maes | When is an Interacting Particle System Ergodic?[END_REF]), where

γ = j∈Ir sup J⊂Ir |p(J ∪ {j}) -p(J)|.
In the case of the Domany-Kinsel model, which belongs to the class C, we obtain

γ = sup J⊂Ir |p(J ∪ {-1}) -p(J)| + sup J⊂Ir |p(J ∪ {1}) -p(J)| = 2(a 2 -a 1 ) since η . ∈ C (a 2 ≥ 2a 1 -a 0 ). If a 2 < 1 (condition of Theorem 2)
and 2(a 2a 1 ) ≥ 1 the Dobrushin suficient conditions can not be applied.

For the two-dimensional example we have γ = α 9 k=1 k × C 9 k . In this case γ > p(I r ) and even if γ < 1 the constant of decay of correlation 1 2 ln(1/(p(I r )) is greater than 1 2 ln(1/(γ)), the constant of decay of correlation given in [START_REF] Maes | Ergodicity of Probabilistic Cellular Automata: A constructive Criterion[END_REF]. More generally, if a PCA belongs to C the sufficient condition p(I r ) < 1 can be rewritten as p(I r ) = J⊂Ir λ(J) < 1 and the Dobrushin sufficient condition can be rewritten as γ = J =∅, J⊂Ir λ(J) × |J| < 1.

4 Proof of Theorem 2 and Proposition 1

PCA in C and their Dual Process

In [START_REF] Lopez | Dualities for Multi-State Probabilistic Cellular Automata[END_REF], the authors give sufficient ergodicity conditions for one-dimensional multi-state PCA of radius one using a dual process satisfying equation 1.1. Here we will use an analogous dual process to give sufficient ergodicity conditions for two-state, d-dimensional PCA of radius r using the following duality equation:

E η0=x [H(η 1 , Y )] = D(Y )E ξ0=Y H[(x, ξ 1 )], (1.4)
where η . is a PCA with state space {0, 1} Z d . The state space of the dual process ξ . is the class of all finite subsets of Z d . As in [START_REF] Lopez | Dualities for Multi-State Probabilistic Cellular Automata[END_REF] we define the function H by

H(x, Y ) = 1 , if x(z) = 1, ∀z ∈ Y 0 , otherwise.
The rule for the evolution of the process ξ t is given by

ξ t+1 = ∪ z∈ξt B(z)
where for any nonempty set J ⊂ I r we have

P B(z) = {z + j|j ∈ J} = π(J) and P B(z) = ∅ = π(∅).
Then, take the function D such that D(Y ) = D |Y | for any finite subset Y ⊂ Z d , where D ∈ [0, 1]. Note that D(∅) = 1 and ∅ is the unique absorbing state for this dual process.

The functions H and μ

Note that, for this particular choice of H, we have

μ(Z d ) = X H(x, Z d )dµ(x) = µ( ∞ 1 ∞ ) = 0 and μ(∅) = X H(x, ∅)dµ(x) = µ({0, 1} Z d ) = 1,
where X = {0, 1} Z d and ∞ 1 ∞ is the all one configuration (1

Z d (x)) x∈Z d .
The following Lemma is used in the proof of Theorem 2 and Theorem 3.

Lemma 2

The set of linear combinations of {H(., y)|y

∈ Z d } is dense in C {0, 1} Z d , R , the set of continuous function from {0, 1} Z d to R. For any cylinder U = N (Λ, ϕ) ⊂ {0, 1} Z d (with Λ ⊂ Z d , |Λ| < ∞ and ϕ ∈ A Z d ) we have µ(U ) = Y (i) α i μ(Y (i)),
where

α i ∈ Z, Y (i) ⊂ Z d and max{|Y (i)|} < ∞.
Proof. For the sake of simplicity, we only give the proof for the two-state, one-dimensional case. The key point of the proof consists in showing that any cylinder [U ] t := [u 0 . . . u n ] t , (u i ∈ {0, 1} and t, n ∈ N) can be decomposed into a non-commutative sequence of subtractions and unions of intersections of cylinders of the type [START_REF] Boborowski | Functional Analysis for Probability and Stochastic Processes[END_REF] t , t ∈ Z. We denote by T ([U ] t ) this decomposition.

One way to accomplish this decomposition is to follow the following rules:

T ([1] t ) = [1] t , T ([0] t ) = {0, 1} Z d -[1] t .
Then, for all t, n ∈ Z and U = u 0 . . . u n we have

T ([U 1] t ) = T ([U ] t ) ∩ [1] t+n+2 . Thus, T ([U 0] t ) = T ([U ] t ) -T ([U ] t ) ∩ [1] t+2+n .
For instance,

T ([100] 0 ) = T ([10] 0 ) -T ([101] 0 ) = (T ([1] 0 ) -T ([11] 0 )) -(T ([10] 0 ) ∩ [1] 2 ) = [1] 0 -[11] 0 -(([1] 0 -[11] 0 ) ∩ [1] 2 ) = ([1] 0 -[11] 0 -([1] 0 ∩ [1] 2 )) ∪ [111] 0 .
Then, note that 1 [1000]0 , the characteristic function of the cylinder [1000] 0 , can be written as

1 [1000]0 (x) = 1 [1]0 (x) + 1 [111]0 (x) -1 [1]0∩[1]2 (x) -1 [11]]0 (x) = H(x, {0}) + H(x, {0, 1, 2}) -H(x, {0, 2}) -H(x, {0, 1}).
Since for any finite subset Y ⊂ Z we have

1 ∩i∈Y [1]i (x) = H(x, Y ), it follows that for all n ∈ N, t ∈ Z and U ∈ {0, 1} n 1 [U]t = α i H(x, Y (i))
. This, in turn, implies that the set of linear combinations of the set {H(.,

Y )|Y ∈ Z d } is dense in C({0, 1} Z d ).
We finish the proof by observing that for any cylinder [U ] t , we have

µ([U ] t ) = 1 [U]t (x)dµ(x) = α i H(x, Y (i))dµ(x) = α i μ(Y (i)). 2
Remark 3 Using the definition of H taken in [START_REF] Lopez | Dualities for Multi-State Probabilistic Cellular Automata[END_REF] which takes into consideration the multi-state case, it is possible to prove Proposition 2 for more general d-dimensional PCA.

Proof of Theorem 2

We first establish a sequence of equalities between the transition probabilities of the PCA (P (J)|J ∈ I r ) and the transition probabilities of the dual process ((π(J)|J ∈ I r )). We can rewrite the right hand of equation (1.4) to obtain

E η0=x [H(η 1 , Y )] = P η0=x {η 1 (z) = 1 ∀z ∈ Y }.
Hence, using the independence property of η . we get that

P η0=x {η 1 (z) = 1 ∀z ∈ Y } = z∈Y P η0=x {η 1 (z) = 1}.
For the left hand of equation 1.4 we have

E ξ0=Y [H(x, ξ 1 )] = P ξ0=Y {x(z) = 1 , ∀z ∈ ξ 1 }.
For any x ∈ {0, 1} Z d we denote by C x the set {z ∈ Z d |x(z) = 1}. Then

P ξ0=Y {x(z) = 1 ∀z ∈ ξ 1 } = P ξ0=Y {ξ 1 ⊂ C x }.
Using the independence property of the dual process we can assert that

P ξ0=Y {ξ 1 ⊂ C x } = z∈Y P{B(z) ⊂ C x }.
Finally we can rewrite equation 1.4 as

z∈Y P η0=x {η 1 (z) = 1} = D |Y | z∈Y P{B(z) ⊂ C x } = z∈Y D × P{B(z) ⊂ C x } (1.5) which implies that z∈Y p(J z ) = z∈Y D × ∆ z , (1.6)
where J z = {i -z|i ∈ {C x ∩ {j + z}|j ∈ I r and ∆ z is given by

∆ z = π(∅) + i∈Ir 1 1 (x(z + i)) × π({i}) + i,j∈Ir 1 {1} (x(z + i)) × 1 {1} ((x(z + j)) × π({i, j}) + . . . + i1,...,i k ∈Ir k l=1 1 {1} (x(z + i k )) × π({i 1 , . . . , i k }) + . . . + i∈Ir 1 {1} (x(z + i)) × π(I r ).
By simplicity of notation we write π(i 1 , . . . i k ) and p(i 1 , . . . i k ) instead of π({i 1 , . . . i k }) and p({i 1 , . . . i k }).

Since equation 1.6 is true for all x ∈ {0, 1} Z d we obtain the following equations for π(.),

p(∅) = Dπ(∅) p(i) = D[π(∅) + π(i)] p(i, j) = D[π(∅) + π(i) + π(j) + π(i, j)] p(i, j, k) = D[π(∅) + π(i) + π(j) + π(i, j) + π(i, k) + π(j, k) + π(i, j, k)]
where i, j, k ∈ I r . More generally, for any 0

≤ k ≤ |I r | -1, p(i0, ..., i k ) = D h π(∅)+ k X l=0 π(l)+. . .+ k-1 X i=0 X l 0 ,...,l i ∈{i 0 ,...,i k } π(l0, ..., li)+π(l0, l1, ..., l k ) i . (1.7)
Since

π(∅) + |Ir | k=0   l0,l1,...l k ∈Ir π(l 0 , l 1 , . . . l k )   + π(I r ) = 1,
we get that D = p(I r ).

By definition, the dual process is completely determined by the parameters 0 ≤ π(J) ≤ 1 (J ⊂ I r ). From the sequence of equations 1.7 the dual process associated with the particular functions H and D exists if the transition probabilities of the PCA satisfy p(J) = D J⊂Ir π(J) with 0 < p(I r ) ≤ I r . In this case we have that λ(J) = Dπ(J) and we claim that a PCA η . admits a dual process that satisfies the duality equation 1.1 with particular functions H and D given in section 4.1 if and only if this PCA belongs to the class C.

To show that the PCA is ergodic we need to verify the three conditions of Theorem 1. Condition i) is verified since from Lemma 2, the set of linear combinations of functions belonging to

{H(., Y ), |Y ∈ Z d } is dense in C {0, 1} Z d , R . Condition ii) is satisfied since sup Y =∅ {D(Y )} = D = p(I r ) < 1. Condition iii) follows from the fact that H(., ∅) = 1 and D(∅) = D |∅| = 1.
Since ∅ is the only absorbing state for ξ . , using Theorem 1 (equation 1.

Proof of Corollary 1

When λ(∅) = 1, starting from any initial measure µ 0 , we obtain that µ 1 = δ 1 . When λ(∅) = 0, Theorem 2 and Lemma 2 imply that for each cylinder U that does not contain the point ∞ 0 ∞ we get

µ(U ) = α i ∞ k=0 P Y0=Y (i) {Y k = ∅|Y k-1 = ∅} = 0 since π(∅) = λ(∅) p(Ir ) = 0. Finally we get that µ( ∞ 0 ∞ ) = 1-µ({0, 1} Z d -∞ 0 ∞ ) = 1 which finishes the proof. 2

Proof of Proposition 1

Since the {π(J)|J ⊂ I r } represent the transition probabilities of the dual process for all J ∈ I r one has π(J) ≥ 0 and Proposition 1 is a simple consequence of the following Lemma .

Lemma 3

The transition probabilities π() of the dual process satisfy

π(∅) = p(∅) D π(i) = p(i)-p(∅) D π(i, j) = 1 D [p(i, j) + p(∅) -p(i) -p(j)] π(i, j, k) = 1 D [p(i, j, k) -p(∅) + p(i) + p(j) + p(k) -p(i, j) -p(i, k) -p(j, k)] π(i, j, k, l) = 1
D [p(i, j, k, l) + p(∅) -P l 0 ∈{i,j,k,l} p(l0) + P {l 0 ,l 1 }⊂{i,j,k,l} p(l0, l1) -P {l 0 ,l 1 ,l 2 }⊂{i,j,k,l} p(l0, l1, l2)]

More generally, for any 0 ≤ k ≤ |I r | -1 and for any j 0 , . . . , j k ∈ I r π(j0, . . . ,

j k ) = 1 D 2 4 (-1) k+1 p(∅) + k X j=0
(-1) k-j X {l 0 ,...,l j }⊂{j 0 ,...,j k } p(l0, . . . , lj ) 3 5 .

Proof. of Lemma 3 From the proof of Theorem 2 a PCA belongs to class C if and only if the transitions probabilities p() and π() satisfy the sequence of equations 1.7. We use mathematical induction to solve the sequence of equations 1.7. For the two first iterations it is easily seen that π(∅)

= p(∅) D , π(i) = p(i)-p(0) D and π(i, j) = 1 D [p(i, j) + p(0) -p(i) -p(j)].
Then suppose that the order k is true: (1.8) Then we suppose the rank k true and use equation 1.8 to obtain that the term in p(∅) in π(j 0 , . . . , j k+1 ) is

π(j 0 , . . . j k ) = 1 D   (-1) k+1 p(∅) + k j=0 (-1) k-j (
-p(∅) - k i=0   l0,...,li∈{j0,...,j k+1 } (-1) i+1 p(∅)   = p(∅) -1 - k i=0 C k+2 i+1 (-1) i+1 = p(∅) -1 + C k+2 0 (-1) 0 + C k+2 k+2 (-1) k+2 -(1 -1) k+2 = (-1) k+2 p(∅),
where the constants C k i represent the binomial coefficients. Next we obtain that the term in l0∈{j0,...,j k+1 } p(l 0 ) in π(j 0 , . . . , j k+1 ) is equal to

- k i=0 (l0,...,li)∈{j0,...,j k+1 }   h0∈{l0,...,li} p(h 0 )   (-1) i = - l0∈{j0,...,j k+1 } p(l 0 ) k i=0 C k+1 i (-1) i = - l0∈{j0,...,j k+1 } p(l 0 ) (1 -1) k+1 -C k+1 k+1 (-1) k+1 = l0∈{j0,...,j k+1 } p(l 0 )(-1) k+1 .
Note that C k+1 i represents the number of ways to choose l 1 , . . . , l i in j 1 , . . . , j k+1 when we have chosen l 0 and j 0 . More generally, for 0 ≤ M ≤ k, the term in (l0,...,lM )∈{j0,...,j k+1 } p(l 0 , . . . , l M ) in π(j 0 , . . . , j k+1 ) is equal to

- k i=M (l0,...,li)∈{j0,...,j k+1 }   (h0,...,hM )∈{l0,...,lj } p(h 0 , . . . , h M )   (-1) i-M = - (l0,...,lM )∈{j0,...,j k+1 } p(l 0 , . . . , l M ) k-M i=0 C k+1-M i (-1) i = - (l0,...,lM )∈{j0,...,j k+1 } p(l 0 , . . . , l M ) (1 -1) k+1-M -(-1) k+1-M = ( l0
,...,lM )∈{j0,...,j k+1 } p(l 0 , . . . , l M )(-1) k+1-M .

5 Decay of Correlation

For the sake of simplicity we study the decay of correlation for PCA with state space {0, 1} Z . An extension of this result to the multi-dimensional case is straightforward but requires too much notation.

Proof of Theorem 3

The proof of Theorem 3 requires the following two results. The second one is new and is a key point for the proof of Theorem 3. The first one seems to be well known. However, its proof can not be found or at least it is quite hard to be found so we provide a proof of that result.

Recall that µ stands for the unique invariant measure of an ergodic PCA.

Proposition 2 Every invariant measure of an ergodic PCA is shift-invariant.

Lemma 4 Let [U ] 0 and [V ] 0 be two cylinders. If µ([U ] 0 ) = α i μ(A i ), µ([V ] 0 ) = β i μ(B i ) and t ≥ |U | + |V |, then µ([U ] 0 ∩ σ -t [V ] 0 ) = µ([U ] 0 ∩ [V ] t ) = α i μ(A i )( * , t) β i μ(B i ),
where

α i μ(A i )( * , t) β i μ(B i ) := i,j α i β j μ(A i ∪ {B i + t}).

Proof of Theorem 3

If D = 0, then p(∅) = 0. From Corollary 1, µ = δ 0 and µ has exponential decay of correlation. For the remainder of this proof we therefore take 0 < D = p(I r ) < 1.

For any finite subset E of Z and s ∈ Z, define E + s := {x + s : x ∈ E}. We claim that for any finite subsets E and F , if

t ≥ 2N r + |E| + |F | we have |μ(E ∪ {F + t}) -μ(E) × μ(F )| ≤ D N +1 1 1 -D .
The proof of this claim uses Theorem 1 and 2 which together say that for any finite subset E ⊂ Z, μ(E) = P η0=E {η τ = ∅}. This, in turn, implies that μ(E) = Thus, by inequality 1.9, ) . Finally, it follows from Proposition 2 that the invariant measure is shiftinvariant and that the exponential decay of correlations of cylinders implies the mixing property. Noting that µ([V 1] t ) = α i μ({B i + t} ∪ {|V | + t}) we get the desired result for the case

α i β j μ(A i ∪ {B i + s} -α i μ(A i ) × β j μ(B j )) ≤ |α i β j |D N +1
[U 1] 0 ∩ [V 1] t .
The result for the case [U 1] 0 ∩ [V 0] t follows by noting that It can also be shown that

µ([U 1] 0 ∩ [V 0] t ) = µ([U 1] 0 ∩ [V ] t ) -µ([U 1] 0 ∩ [V 1] t ) = i,
µ([U 0] 0 ∩ [V 1] t ) = [ α i μ(A i ) - α i μ(A i ∪ {|U |})] ( * , t) [ α i μ({B i + t} ∪ {|V | + t})].
Finally, using that

µ([U 0] 0 ∩ [V 0] t ) = µ([U ] 0 ∩ [V ] t ) -µ([U 1] 0 ∩ [V 0] t ) -µ([U 0] 0 ∩ [V 1] t ) -µ([U 1] 0 ∩ [V 1] t )
we can show that

µ([U 0] 0 ∩ [V 0] t ) = [ i,j α i β j μ(A i ∪ {B i + t}) - i,j α i β j μ(A i ∪ {B i + t} ∪ {|U |})]( * , t) [ i,j α i β j μ(A i ∪ {B i + t}) - i,j α i β j μ(A i ∪ {B i + t}) ∪ {|V | + t}]
which finishes the proof. 2

Final Questions i) Is there exist an ergodic PCA such that the unique invariant measure is not shift-mixing? ii) Is there exist an ergodic PCA such that the invariant measure has nonexponential decay of correlation?

Proposition 1 A(- 1 )

 11 two-state probabilistic cellular automaton η . belongs to C if its transition probabilities satisfy the following set of inequalities: (a) For any i ∈ I r , p({i}) ≥ p(∅).(b) For any 1 ≤ k ≤ |I r | -1 and for any j 0 , . . . , j k ∈ I r p({j0, . . . , j k }) ≥ (-1) k p(∅) -k+1-n X {l 0 ,...,ln}⊂{j 0 ,...,j k } p({l0, . . . ln}).

  is a square of 9 sites. The transition probabilities {p(J)|J ⊂ I 1 } of η . are defined by p(J) = α |J| k=0 C 9 k = α × 2 |J| where C l k

  2) we get that for any nonemptysetY ⊂ Z d μ(Y ) = μ(∅)P ξ0=y {ξ τ = ∅} = +∞ t=1 P ξ0=y {ξ t = ∅|ξ t-1 = ∅}.From Lemma 2, for any cylinder set U there exist α k ∈ R and Y (k) finite subset of Z d such that µ(U ) = α k μ(Y (k)), which implies the last statement of Theorem 2.

2

 2

  l0,...,lj )∈{j0,...,j k } p(l 0 , . . . l j )   .Using equation 1.7 we obtain that π(j 0 , . . . , j k+1 ) equals 1 D   p(j 0 , . . . , j k+1 )dπ(∅) -D ...,lj )∈{j0,...,j k+1 } π(l 0 , . . . , l j )

∞ k=0 PPPPPPP

 k=0 η0=E {τ = k}, where τ is the hitting time for the process η . . In fact, by Lemma 1, for any integer N > 0 we haveμ(E) -N k=0 η0=E {τ = k} ≤ D N +1 1 1 -D . Note that if s ≥ 2ri + |E| + |F |, where i is any positive integer, thenP η0=E∪{F +s} {τ = i} = P η0=E {τ = i} × i j=0 η0={F +s} {τ = j} + P η0={F +s} {τ = i} × i j=0 η0=E∪{F +s} {τ = j}. It follows that if s ≥ |E| + |F | + 2N × r, then N i=0 E0=E∪{F +s} {τ = i} = N i=0 E0=E {τ = i} × N i=0 E0={F +s} {τ = i}.This easily implies|μ(E ∪ {F + s})μ(E) × μ(F )| ≤ D N +1 1 1 -D ,(1.9)for s ≥ |E| + |F | + 2N × r, which proves our claim. By Lemma 2, for any pair of cylinders [U ] 0 and [V ] 0 , there exist finite sequences of sets (A i ) and (B i ) and finite sequences of real numbers α i and β i such thatµ([U ] 0 ) = α i μ(A i ) and µ([V ] 0 ) = β i μ(B i ).

1 1 -

 1 D for any pair of subsets A i and B j of Z and for any s ≥ |U | + |V | + 2N r.It follows from this that i,jα i β j μ A i ∪ {B i + s}i α i μ(A i ) × j β j μ(B j ) ≤ F (U, V )D N ,whereF (U, V ) = i,j |α i β j | D 1-D . Using Lemma 4, if t ≥ |U | + |V | we obtain µ [U ] 0 ∩ σ -t [V ] 0µ([U ] 0 ) × µ([V ] 0 ) ≤ K(U, V ) expt × ln (1/D) 2r , where K(U, V ) = F (U, V )D -( |U |+|V | 2r

2

 2 which finishes the proof in the case|U | = |V | = 1. Now, suppose that µ([U ] 0 ∩ σ -t [V ] 0 ) = i,j α i β j μ(A i ∪ {B i + t}) is true for |U | = |V | = n. Consider t ≥ 2n + 1 and let [U ] 0 , [V ] 0 be two cylinders such that µ([U ] 0 ) = α i μ(A i ) and µ([V ] 0 ) = β j μ(B j ). Since µ([U 1] 0 ) = α i μ(A i ∪ {|U |}), we get µ([U 1] 0 [V 1] t ) = i,j α i β j μ(A i ∪ {B j + t} ∪ {|U |, |V | + t}).

  Definition 1 Let η . and ζ . be two Markov processes with state spaces X and Y respectively, and let H (η, ζ) be a bounded measurable function on X × Y . The processes η . and ζ . are said to be dual to one another with respect to H

  j α i β j μ(A i ∪ {|U |} ∪ {B j + t}) i,j α i β j μ(A i ∪ {B j + t} ∪ {|U |, |V | + t}) = α i μ(A i ∪ {|U |})( * , t) α i μ({B i + t}) α i μ({B i + t} ∪ {|V | + t}).

Acknowledgements We would like to thank Marcelo Sobottka for a carefully reading of a previous version of this work and for many comments and suggestions. We also thank the referees for constructive remarks. During the realization of this work the first author received partial financial support from FAPESP, grant 2006/54511-2. The second author received financial support from UFABC, grant 2008.

Proof of Proposition 2.

It is sufficient to show that for any cylinder [U ] t , where U ∈ {0, 1} l for some l ∈ N , we have

). Since µ is the invariant measure of an ergodic PCA η . , there exits a sequence (µ i ) i∈N which converges in the weak* topology to µ, where µ i is the distribution of a PCA η . at time i starting from an initial distribution µ 0 . It follows that for any cylinder [U ] t we have

Since for any positive integer i we have

we can choose µ 0 as a shift-invariant probability measure. Hence, for any positive integer i and any cylinder [U ] t we have

which finishes the proof. 2

Proof of Lemma 4

We prove the lemma using the principle of mathematical induction. First we prove it for the case |U | = 1 and |V | = 1. Note that for any finite set {j 0 , . . . , j k }, with j 0 , . . . , j k ∈ Z,

and observe that for any k ≥ 1 ∈ N we have


Jade Alglave

Luc Maranget

Fences and Synchronisation in Weak Memory Models

Keywords: Weak Memory Models, Fences, Locks Fences and Synchronisation in Weak Memory Models

We present an axiomatic framework, implemented in the Coq proof assistant, to define weak memory models in terms of several parameters: local reorderings of reads and writes, and visibility of inter and intra processor communications through memory, including full store atomicity relaxation. Thereby, we give a formal hierarchy of weak memory models, in which we provide a formal study of what should be the action and placement of fences to restore a given model such as SC from a weaker one. Finally, we provide formal requirements for abstract locks that guarantee SC semantics to data race free programs, and show that a particular implementation of locks matches these requirements.

Introduction

Understanding the behaviour of a program running on a multiprocessor requires a precise definition of the underlying memory system and the behaviour of the processors involved-that is, the memory model. Previous studies [START_REF] Burckhardt | Memory model safety of programs[END_REF] have discussed the need for rigorous definitions of weak memory models, which some of the public documentations [START_REF]Intel 64 Architecture Memory Ordering White Paper[END_REF]17] lack. We provide here a generic framework, implemented in the Coq proof assistant [START_REF] Bertot | Interactive Theorem Proving and Program Development: Coq'Art: The Calculus of Inductive Constructions[END_REF], to precisely define a memory model in terms of several parameters expressing potential sources of weakness.

Weak Memory Models

Processor behaviour A simple model of a processor's behaviour in a multiprocessor context could assume a sequential order, consistent with the program order, of all the read and write events issued by this processor, as a generalisation of the uniprocessor case. However, modern architectures [20,17,[START_REF]Alpha Architecture Reference Manual[END_REF] provide relaxed memory models that do not constrain the way reads and writes are ordered as much. These constraints, or their relaxation, are often referred to as instruction reordering [START_REF] Adve | Shared memory consistency models: A tutorial[END_REF][START_REF] Maessen | Memory model = instruction reordering + store atomicity[END_REF].

Representation of memory A simple model of a shared memory could assume a single memory on which several processors operate simultaneously, with all their writes being commited to memory as soon as they are issued. Thus, the connection between processors and memory could be considered as direct: as soon as a processor writes to memory, the value written overwrites the previous value and is immediately available to all processors. This property, called store atomicity, has been advocated as valuable [START_REF] Adve | Shared memory consistency models: A tutorial[END_REF][START_REF] Maessen | Memory model = instruction reordering + store atomicity[END_REF], as it provides the guarantee that actions on such a memory are serialisable, which leads to a rather understandable memory model. However, it is not guaranteed on certain architectures [START_REF]A formal specification of Intel Itanium processor family memory ordering[END_REF]17], which relax the store atomicity constraint. This means a write is not available to all processors at once: a write could be e.g. at first initiated by a given processor, then commited to a cache, and finally to memory. This last step is called globally performed [START_REF] Dubois | Memory access dependencies in shared-memory multiprocessors[END_REF]. Even without assuming writes to be commited immediately, we suppose a total order on the globally performed writes to the same location, a property called coherence [17] that is widely assumed by modern architectures [START_REF]Alpha Architecture Reference Manual[END_REF]17,20,[START_REF]Intel 64 Architecture Memory Ordering White Paper[END_REF].

Contribution

An axiomatic generic model We define an architecture in terms of its ordering and store atomicity relaxations in Sec. 2.3, whose validity conditions are described in Sec. 2.4. We illustrate how to instantiate our model to produce Sequential Consistency (henceforth SC ) [START_REF] Lamport | How to make a correct multiprocess program execute correctly on a multiprocessor[END_REF] and Sparc TSO [20], and show equivalence with the native models, together with characterisation of executions that would be valid on these models in Sec. 2.6. Study of barriers power Most architectures provide mechanisms such as barriers-or fences-to restore SC from a weaker model. However, it is not clear how much power a barrier needs in order to do so, and where to place these constructions in the code. We examine these questions in Sec. 3.1 from a general point of view: we provide a sufficient condition on barriers to restore a stronger model from a weaker one. We refine this condition in some interesting cases in Sec. 3.2.

Atomicity Finally in Sec. 4.2, we ensure SC semantics to data-race free (henceforth drf ) programs provided specified requirements on lock and unlock primitives, and show that a particular implementation of these primitives, involving reservations such as in Alpha [START_REF]Alpha Architecture Reference Manual[END_REF] and Power [17], meets these requirements.

Our results and proofs are formalised in the Coq proof assistant; we omit the detail of proofs due to lack of space. However, the development and the sketches of the proofs are available at http://moscova.inria.fr/ ~alglave/wmm/.

2 Description of the model Fig. 1(a) shows a program written in pseudo code and a potential outcome. We will write x, y for memory locations, and r1, r2 for registers. If each location holds initially 0, this outcome may occur for example on an x86 machine since the write-read pair on each processor may be reordered [START_REF]Intel 64 Architecture Memory Ordering White Paper[END_REF]Sec. 2.3]. Such reorderings preclude the use of an interleaving semantics to reason on executions induced by weak memory models. Moreover, these reorderings affect the events generated by instructions, rather than the instructions themselves.

Basic objects

Thus, the model deals with various events occurring in an abstract execution of a multiprocessor program. We write E for the set of all events generated during a given execution.

INRIA

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 identifier. For example, consider the store to x with value 1 labelled (a) in Fig. 1(a): it generates the homonymous event in Fig. 1(b). Henceforth, we write r (resp. w) for an arbitrary read (resp. write) event. We write M (resp. R, W) for the set of memory events (resp. reads, writes).

A barrier event b is generated by each barrier (or fence) instruction; we write B for the set of all such events in a given execution.

An execution is also characterised by the program order po →, a total order amongst the events from the same processor 1 that never relates events from different processors. It reflects the sequential execution of instructions on a single processor: given two instruction 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 .

Execution witnesses

Although it conveys important features of program execution, such as branch resolution, po → is not sufficient to characterise an execution. Indeed, we need to examine where a read value originates from, and express memory coherence. Therefore, we postulate two relations over events: rf → and ws →.

Read-from map (rf ) w rf → r means that r loads the value stored by w; it implies that w and r share the same location and value. Moreover, given a read r there exists a unique write w such that w rf → r (w can be an init store when r loads from initial state). Formally, rf → must be well formed as follows, where W ℓ,v and R ℓ,v are the sets of writes and reads with location ℓ and value v:

wf-rf( rf →) rf → ⊆ ℓ,v (W ℓ,v × R ℓ,v ) ∧ ∀r, ∃!w. w rf → r
Write serialisation (ws) In a coherent memory, all values written to a given location ℓ are serialised, following a coherence order. We define ws → as the union of the coherence orders for all memory locations, which must be well formed as follows, where W ℓ is the set of writes to location ℓ:

wf-ws( ws →) ws → ⊆ ℓ (W ℓ × W ℓ ) ∧ ∀ℓ. total-order ws →, (W ℓ × W ℓ )
From-read map (fr) We call fr → the following relation, gathers all pairs of reads r and writes w such that r reads from a write that is before w in ws →:

r fr → w ∃ w ′ , w ′ rf → r ∧ w ′ ws → w
1 When instructions may perform several memory accesses, po → becomes a partial order, thus should include some intra-instruction dependencies [START_REF] Sarkar | The semantics of x86-CC multiprocessor machine code[END_REF] to build a total order.

RR n 7152

We gather the information that describes an execution into an execution witness, depicted by X:

X (E, po →, rf →, ws →)
Fig. 1(c) shows an execution witness for the test of Fig. 1(a). The load d reads the initial value of x, later overwritten by the store a. Thus, we have d fr → a, as a consequence of the serialisation of the init store to x (which comes first in ws →) and the write a. We define the well formedness predicate wf on execution witnesses, as the conjunction of the associated predicates for ws → and rf →.

Execution order

We define the order in which memory events are globally performed-the global happens-before relation, depicted by ghb → -as a partial order over all such events of a candidate execution witness, following Alpha [START_REF]Alpha Architecture Reference Manual[END_REF] or Sparc [20]. m 1 ghb → m 2 means that m 1 occurs before m 2 w.r.t. all processors. ghb → is subject to various conditions-according to architectural parameters-which we now describe.

Globality of relations

In our setting, writes are not necessarily atomic [START_REF] Adve | Shared memory consistency models: A tutorial[END_REF][START_REF] Maessen | Memory model = instruction reordering + store atomicity[END_REF] i.e. not necessarily available to all parts of the memory system-or globally performed [START_REF] Dubois | Memory access dependencies in shared-memory multiprocessors[END_REF]-at once. This determines which relations are to be considered global, i.e. included in A memory model could allow store forwarding-or read own's writes early [START_REF] Adve | Shared memory consistency models: A tutorial[END_REF] meaning the processor that issued a given write can read its value before any other participant has access to it: in that case, rfi → is not included in ghb → . A model could also allow two particular processors that share 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]. In that case, rfe → is not considered global.

Second, ws → and fr → are always global. Indeed, the coherence order for a given location is the order in which writes to this location 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 before all participants agree on the value stored by w; otherwise r could read its value from w ′ in a given processor view, and from w in another processor view.

INRIA

Preserved program order Some models ensure that certain pairs of events are to be maintained in program order w.r.t. all participants: for example, TSO [20] ensures this property for all write-write pairs. To represent these constraints, we postulate a global relation ppo → which gathers all pairs of events that are not to be reordered with respect to the program order Barriers constraints Architectures provide particular instructions-barriers or fences such as Power sync-to enforce a certain order between pairs of events, according to a particular semantics, such as the ones we define in Sec. 3. We postulate a global relation ab → that gathers all such pairs. Architecture An architecture, depicted by A, collects this information-where int and ext are booleans that determine whether We write A.ghb for the function that, given an execution witness, outputs the appropriate ghb → relation, w.r.t. A. We write A ǫ for an architecture A where we consider ab to be the function that always outputs the empty relation.

Validity of an execution with respect to an architecture

We define the validity of an execution as the conjunction of several criterions on the various relations we defined.

Uniprocessor behaviour As stated by [17, p.29], one expects a sole processor to respect the sequential execution model, which is: [. . . ] the model of program execution in which the processor appears to execute one instruction at a time, completing each instruction before beginning to execute the next instruction.

P0 P1 (a) x ← 1 (b) r1 ← x (c) x ← 2 Forbidden: x=1; r1=1; (a) W[x]=1 (b) R[x]=1 rf rf (c) W[x]=2 po:1po-loc ws Fig. 2

. Invalid execution by uniproc

We understand this as a constraint on a sole processor in a multiprocessor context: a sole processor cannot ignore memory coherence. For instance, a processor that reads a location ℓ twice cannot load values that would contradict write serialisation; or if a processor writes v to ℓ and then reads v ′ from ℓ, one expects v ′ not to precede v in coherence order. We view the sequential execution model as preventing local reordering of memory accesses to the same location and enforcing memory coherence for each processor. We first define the relation po-loc → which gathers all pairs of accesses to the same location in the program order:

m 1 po-loc → m 2 m 1 po → m 2 ∧ loc(m 1 ) = loc(m 2 )
To guarantee our executions respect the sequential execution model, we could enforce We define the validity of an execution with respect to an architecture A as the conjunction of these conditions:

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

Properties of validity

From this definition arises a very simple notion of comparison defined by a predicate among architectures:

A 1 ≤ A 2 means that A 1 is weaker than A 2 . Below, f 1 ⊆ f 2 stands for: ∀X, f 1 (X) ⊆ f 2 (X), if f 1 and f 2 are functions that INRIA
output relations over events when given an execution witness, and ⇒ is the implication over booleans:

A 1 ≤ A 2 ppo 1 ⊆ ppo 2 ∧ int 1 ⇒ int 2 ∧ ext 1 ⇒ ext 2
Validity is decreasing We prove validity of an execution to be decreasing w.r.t. the weaker predicate; thus, a weaker architecture may exhibit at least all the behaviours authorised by 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))
Monotonicity of validity Some programs running on an architecture A 1 could exhibit particular executions that would be valid on a stronger architecture A 2 ; we characterise all such by the following criterion:

A 1 . check A2 (X) acyclic( ?rf2 → ∪ ws → ∪ fr → ∪ ppo2 → )
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))

Examples

We examine here two classical models, SC [START_REF] Lamport | How to make a correct multiprocess program execute correctly on a multiprocessor[END_REF] and Sparc TSO [20]. In both cases we propose alternative formulations in our framework, which we proved equivalent to the original definitions. We omit the detail of formalism related to these equivalences due to lack of space. We first define a few convenient notations to extract pairs of memory events from the program order:

M M = (M × M) ∩ po → RM (R × M) ∩ po → W W (W × W) ∩ po →
SC is a model in which no reordering of events is allowed ( ppo → equals po → on memory events) and writes are available to all processors as soon as they are issued ( rf → are global). Thus, there is no need for barriers:

Sc.Arch (λX.M M , true, true, λX.∅)
Note that any architecture definable in our framework is weaker than Sc. Thm. 2 shows the following criterion characterises, on any architecture A, valid weak executions that are Sc:

A. check Sc (X) acyclic( hb-seq → ∪ 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.
RR n 7152 TSO is described in [START_REF] Adve | Shared memory consistency models: A tutorial[END_REF] as allowing two relaxations: write to read program order and read own's write early. We interpret the first relaxation as a ppo → relation that orders load-load, load-store and store-store pairs: ppo-tso

→

RM ∪ W W . We interpret the second relaxation as internal rf → not being global. And indeed the execution model of Sparc architectures is provided by the Value axiom of [20], which states that a read (L a for Sparc) reads from the most recent write (S a ) that is before it in the global ordering relation (≤) or in the program order (;):

V al(L a ) = V al(max ≤ a | S a ≤ L a ∨ S a ; L a })
Thus, we propose an alternative definition of Sparc TSO2 : Tso ǫ .Arch (λX.

Semantics of barriers

A program may exhibit on a weaker architecture executions that would not be valid on a stronger one. However, one may want to ensure validity on any memory model-typically SC -of a given program. Architectures provide special instructions, namely barriers, which enforce some ordering constraints in a program when present in the program order between two instructions. We consider here the question of restoring a stronger model from a weaker one by using barriers: we examine both their placement and the power they should have to do so.

Barriers guarantee

Consider two architectures A 1 ≤ A 2 . We define the predicate fb-for fully barriered -on A 1 as follows, where

r 2\1 → r2 → \ r1 →: A 1 . fb A2 (X) ( ppo 2\1 → ) ∪ ( ?rf 2\1 → ; ppo2 → ) ⊆ ab1 →
We prove that the above condition on ab1 → suffices to restore A ǫ 2 from A 1 : Theorem 3 (Barriers guarantee).

∀A 1 A 2 , (A 1 ≤ A 2 ) ⇒ (∀X, A 1 . valid(X) ∧ A 1 . fb A2 (X) ⇒ A ǫ 2 . valid(X))
This theorem provides an insight on the power the barriers provided by an architecture A 1 should have to restore a stronger one 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.

Static property of barriers is expressed by the condition

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

Dynamic property of barriers is expressed by the condition

?rf 2\1 → ;
ppo2 → : a barrier provided by A 1 should force store atomicity for the write events that have this property on A 2 . This is how we interpret the cumulativity of barriers as stated by Power [17]. We interpret furthermore the A-cumulativity (resp. Bcumulativity) property as applying 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 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 .

Note that it would suffice to have w ab1 → r whenever w

?rf 2\1
→ r holds to restore store atomicity. However, such an achievement would probably be extremely costly: it supposes that when the barrier event occurs (after r), it waits until w is globally performed, and then reads again to ensure that r is globally performed after w. Our condition does not enforce such a costly policy: given the situation w rf → r po → m, where r is not necessarily globally performed after w is, inserting a barrier between r and m-more precisely inserting a barrier instruction between the instructions generating r and m-only forces the processor that generates r and m to delay m until w is globally performed.

Restoring Sc We model an A-cumulative barrier as the following function on execution witnesses that returns an ordering relation when given a placement of barriers in the code 3 : → to express a barrier that would cumulate on some pairs, while preserving the local order of some others.

m 1 fenced → m 2 ∃b, m 1 po → b po → m 2 A-cumul(X,

RR n 7152

iriw P0 P1 P2 P3 (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 fenced (po:0) (f ) W[y]=2 fr (c) R[y]=2 (d) R[x]=0 fenced (po:1) (e) W[x]=1 fr rf A cumul rf A cumul
∀A X, (A. valid(X) ∧ A-cumul(X, M M ) ⊆ ab →) ⇒ Sc. valid(X)
Consider the example given in Fig. 3(a): the specified outcome may arise in the absence of barriers on a weak architecture, as the result of a non-Sc execution. The barrier whose semantics we designed above forbids this outcome, as shown in Fig. 3(b): when placed in between each pair of reads on the first two processors, it not only prevents their reordering, but also forces the writes from the last two processors to be globally performed before the second component of each pair of reads.

Thus, one ensures an Sc behaviour for all programs by fencing all pairs in po →. However, this would much impair performance; to restore Sc from A, it indeed suffices to invalidate non Sc executions, by fencing only the po → pairs appearing in the hb-seq → ∪ po → cycles of these executions. The static analysis of [START_REF] Shasha | Efficient and correct execution of parallel programs that share memory[END_REF] may be of considerable help, as it is based on compile-time (safe) approximation of cycles in hb-seq → ∪ po → that may arise at runtime. We believe this technique would apply to architectures with store atomicity relaxation, provided their barriers offer A-cumulativity.

Restoring Tso ǫ We design a semantics for a barrier that would restore Tso ǫ from any weaker architecture A: ∀A, A ≤ Tso ⇒ ∀X, (A. valid(X)∧ext-A-cumul(X, ppo-tso

ext-A-cumul(X,
→ ) ⊆ ab →) ⇒ Tso ǫ
. valid(X)

Considering a weaker guarantee

Consider the particular case of two architectures A 2 and A 1 with the same policy w.r.t. the store atomicity and store buffer relaxations, which we model by ext 1 = ext 2 and int 1 = int 2 . In this case, there is no need for a barrier as powerful as above to restore A 2 from A 1 : a barrier that only orders the events that surround it statically-that is, a non cumulative barrier, which action we model by non-cumul(X, fenced → ) fenced → enough. Consider the wfb predicate:

A 1 . wfb A2 (X) ppo 2\1 → ⊆ ab1 →
This states that the barriers provided by A 1 maintain the pairs that are preserved in the program order on A 2 but not on A 1 . Moreover, this guarantee applies if A 2 hinders the store buffer relaxation by its preserved program order, i.e. when rfi → ⊆ ppo2 → -which is particular to Sc-as stated in the following: Theorem 4 (Non cumulative barriers guarantee).

∀A 1 A 2 , ((A 1 ≤ A 2 ) ∧ (ext 1 = ext 2 ) ∧ ((int 1 = int 2 ) ∨ ( rfi → ⊆ ppo2 → ))) ⇒ (∀X, A 1 . valid(X) ∧ A 1 . wfb A2 (X) ⇒ A ǫ 2 . valid(X))
From Tso to Sc As ∀X, (Tso. valid(X) ∧ non-cumul(X, W R)

⊆ abTso → ) ⇒ Sc. valid(X))
From Pso to Tso ǫ We comment here on the two definitions of PSO given in Sparc documentations [20]. We first adapt the definition of [20, V8] to our framework: Pso ǫ .Arch (λX.RM , f alse, true, λX.∅)

As for Tso, we deduce from the Value axiom that external rf → is global, whereas internal is not. Thus, Tso and Pso agree on both the store atomicity and the store buffering relaxations, which allows us to apply Thm. 4: Tso ǫ is restored from Pso by inserting non cumulative barriers between all ppo-tso → \ ppo-pso → = W W pairs. And indeed, [20, V9] specifies that TSO is obtained from PSO by adding StoreStore barriers after each write.

Synchronisation Idioms

Cumulativity of barriers may be challenging to implement, or too dear, as it slows considerably the performance of a program. We examine here programming idioms that use less costly barriers, though the trade-off may not be worth it.

Atomicity

Architectures provide special instructions to ensure atomicity to a given operation, such as lwarx and stwcx. in Power [17], or ldstub in Sparc [20]. We assume special read and write events to represent the accesses performed by such instructions, which we write r * and w * . We write R * (resp. W * ) for the set of special reads (resp. writes) included in R (resp. W), and define the effect of an atomic pair as follows:

atom(r, w, ℓ) r ∈ R * ∧ w ∈ W * ∧ loc(r) = loc(w) = ℓ ∧ r = max po → ({m | m ∈ (R * ∪ W * ) ∧ m po → w}) ∧ ¬(∃w ′ , proc(w ′ ) = proc(r) ∧ loc(w ′ ) = ℓ ∧ r fr → w ′ ∧ w ′ ws → w)
Thus, we consider that two events r and w form an atomic pair w.r.t. a location ℓ-i.e. ensure atomicity to the accesses between them in po →-if:

they are both special and to ℓ, -r is the maximal special read in po → before w, and no other processor wrote to ℓ between r and w

We examine here a particular construct, Read-Modify-Write, on which crucial pieces of code such as Test-And-Set and Compare-And-Swap build. We give a generic PowerPC implementation of this construct, which would be similar in Alpha, in Fig. 4: in between the lwarx and stwcx., the code is left to the choice of the programmer, avoiding the dynamic occurrence of other lwarx and stwcx. in the execution path from (a 1 ) to (a 2 ).

The (a 1 )/(a 2 ) pair of Fig. 4 is successful when stwcx. performs its store, in which case it sets the condition register appropriately, so that the code exits the loop.

INRIA

Locks

An important use of Read-Modify-Write is made in the implementation of lock and unlock primitive that may be found in the litterature [17, Appendix B], as depicted in Fig. 5. These primitives paired together define a critical section, locked by a lock variable ℓ. We write lock ℓ → for the relation between two events in two distinct critical sections holding the same lock ℓ and Cs ℓ for the set of critical sections with lock ℓ; we write lock ℓ for the function that outputs the lock ℓ → relation when given an execution witness. We consider that m 1 lock → m 2 whenever there is a location ℓ such that m 1 By drf, we mean that each pair (e 1 , e 2 ) of competing accesses-that is, accesses to the same memory location, on different processors, at least one of which is a write-is such that each of its components is in its own critical section with the same lock variable ℓ, a property we write locked(e 1 , e 2 , ℓ):

lock ℓ → m 2 . loop: (a1) lwarx r6,0,r3 (b) cmpw r4,r6 (c) bne loop (a2) stwcx. r5,0,r3 (d) bne loop isync [...] [...] lwsync (e) stw r4,0,r3 (a) Lock (b) Unlock
compete(m 1 , m 2 ) loc(m 1 ) = loc(m 2 ) ∧ proc(m 1 ) = proc(m 2 ) ∧ (m 1 ∈ W ∨ m 2 ∈ W) locked(m 1 , m 2 , ℓ) ∃(cs 1 , cs 2 ) ∈ (Cs ℓ × Cs ℓ ), cs 1 = cs 2 ∧ m 1 ∈ cs 1 ∧ m 2 ∈ cs 2 A. drf(X) ∀m 1 m 2 , compete(m 1 , m 2 ) ⇒ (∃ℓ, locked(m 1 , m 2 , ℓ))
As stated by the following theorem, we show that if the lock → relation is:

total on pairs of events in two distinct critical sections holding the same lock, -compatible with

A. wf-lock( lock → ) (∀m 1 m 2 ℓ, (locked(m 1 , m 2 , ℓ) ⇒ (m 1 lock ℓ → m 2 ∨ m 2 lock ℓ → m 1 )∧ (∀ℓ, acyclic( lock ℓ → ∪ ghb → )) ∧ (∀ℓ, acyclic( lock ℓ → ∪ rf →)) ∧ acyclic( lock → ∪ po →) RR n 7152
∀AX, A. valid(X) ∧ A. drf(X) ∧ (∀ℓ, A. wf-lock(lock(X))) ⇒ A. check Sc (X)
An example implementation We define predicates taken and free using the atom predicate:

taken(ℓ, r) ∃w, atom(r, w, ℓ) ∧ val(r) = 0 ∧ val(w) = 1 free(ℓ, r, w) r po → w ∧ taken(ℓ, r) ∧ loc(w) = ℓ ∧ val(w) = 0
A read r takes a lock ℓ if it reads 0 from ℓ (indicating the lock was free) and it forms an atomic pair with a write w writing 1 to ℓ. Freeing the lock is the action of the next write event, if any, in po → after a taken operation: it sets the lock variable to 0, and is in po → (therefore in fr → by uniproc) after the read that read the lock as free.

With these two constructs, we define semantics for lock and unlock primitives, such as depicted in Fig. 5:

Lock(ℓ, (r, c)) taken(ℓ, r) ∧ c ∈ B ∧ r po → c Unlock(ℓ, r, (b, w)) free(ℓ, r, w) ∧ b ∈ B ∧ b po → w
A lock acquisition consists of a taken operation followed by an import barrier [17], which properties we will study in Sec. 4.2 An unlock consists of an export barrier [17] followed by a write event that frees the lock variable.

We define a critical section as a triple consisting of a lock and an unlock primitives with the same lock variable ℓ, and the set of events that are in We consider two distinct critical sections cs 1 and cs 2 with the same variable ℓ to be serialised if cs 2 Lock's read reads from cs 1 Unlock's write:

cs 1 css ℓ → cs 2 (cs 1 , cs 2 ) ∈ (Cs ℓ × Cs ℓ ) ∧ cs 1 = cs 2 ∧ ∃r 1 c 1 b 1 w 1 , ∃r 2 c 2 b 2 w 2 , w 1 rf → r 2 ∧ cs 1 = cs(ℓ, (r 1 , c 1 ), (b 1 , w 1 )) ∧ cs 2 = cs(ℓ, (r 2 , c 2 ), (b 2 , w 2 ))
Finally, we define lock ℓ → as the relation over events induced by css ℓ → , i.e. we consider two events to be ordered by lock ℓ → if they are in two distinct critical sections with same lock ℓ, the second reading from the first one, where m ∈ cs expresses the fact that m is between cs import and export barriers in po →:

m 1 lock ℓ → m 2 (∃ℓ cs 1 cs 2 , m 1 ∈ cs 1 ∧ m 2 ∈ cs 2 ∧ cs 1 css ℓ → cs 2 ) (base) ∨ (∃m, m 1 lock ℓ → m lock ℓ → m 2 )
(transitivity)

INRIA

Meeting the drf requirements

Totality of lock ℓ → We assume the existence of an init store to ℓ, which is in lock ℓ → with all critical sections to ℓ, as it is the first store in ws →, and suppose that two critical sections to ℓ cannot be nested. Moreover, when two critical sections have their Lock's read reading from the same Unlock's write, one of their Lock's write takes the lock, which invalidates the reservation of the other one: therefore, its Lock waits until the lock is free, which means it appears later in the critical sections serialisation. Thus, if two critical sections have the same antecedent, they are ordered w.r.t. one another. This is the only part of our results whose mechanisation is not (yet) complete at the time of the submission.

Import and export barriers Let us assume two events m 1 and m 2 such that m 1 lock ℓ → m 2 in the base case. Writing w 1 for the unlock's write of the critical section cs 1 that protects m 1 and r * 2 for the lock's read of the critical section cs 2 that protects m 2 , we know w 1 rf → r * 2 . Thus, if cs 1 export barrier b 1 orders write-write and read-write pairs locally, we have m

1 ab → w 1 . Moreover, if b 1 is B-cumulative, we have m 1 ab → r * 2 .
Formally, we define an export barrier as satisfying the following predicate:

export(b) ∀m 1 m 2 , (m 1 po → b po → m 2 ∧ ¬(m 1 ∈ W ∧ m 2 ∈ R)) ⇒ (m 1 ab → m 2 ) (export
∀AX, A. valid(X) ∧ A. drf(X) ∧ (lock(X) = lock → ) ⇒ A. check Sc (X)
We provide an insight on the power of import and export barriers, namely, in our model, an import barrier should order RM pairs statically; an export barrier should order M W pairs statically and both should be B-cumulative.

In Power [17], the export barrier may be either a sync or a lwsync: both of them are, to the best of our knowledge, B-cumulative, and order read-write and write-write pairs, which is compatible with our export predicate. The import barrier may be either a lwsync-which is compatible with our import predicate as it is B-cumulative and orders read-read and read-write pairs-or a sequence bne;isync, which we believe do not provide any cumulativity, though it orders INRIA the appropriate pairs statically: our model would not guarantee Sc semantics to programs with locks implemented with this sequence.

Conclusion

Minimality of the model We advocate here the fact that, though several constructions such as barriers are specific to a given architecture, most of the reasoning on memory models can be done in the same generic terms. Thus we provide a unifying framework for reasoning about and formally comparing memory models. Moreover, we highlight crucial concepts that should be precisely defined to provide formal models, namely globality of read-from maps and preserved program order. This would certainly allow us to examine the trade-offs between two models, or code portability from one architecture to another. In this respect, we tried to minimise the number of our axioms, and also their scope, to embrace a large range of memory models. For example, we chose not to enforce that values do not come out of thin air [START_REF] Manson | The Java Memory Model[END_REF], though it could be easily added to the model.

Moreover, the principal validity condition of our model is fairly simple: once ws → and rf → are available, checking the validity of a given execution resides in the acyclicity check of ghb → . This approach has been known for a long time for SC [START_REF] Landin | Race-free interconnection networks and multiprocessor consistency[END_REF], and some 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] (i.e. rfi → non global) such as TSO . We believe the present work provides alternative, machine checked, semantical foundations for these tools. More significantly, our formalism allows generalisation to even weaker memory models, that relax store atomicity (i.e.

rfe → non global).

Modeling store-atomicity relaxation We model indeed the potential non atomicity of writes by reasoning on globally performed events and considering rf → not to be global in the general case. Other models handle non atomic writes by defining, for a sole store instruction, several write events [START_REF]A formal specification of Intel Itanium processor family memory ordering[END_REF], or one 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]. The complexity of these models is in sharp contrast with the models of architectures that do not relax store atomicity, such as Sparc [20]. We believe we have shown the simplicity and elegance of Sparc style models can very well be extended to models that relax store atomicity.

Modeling Power Our style of reasoning over globally performed events may lead to a model which is too coarse-grained-by this we mean too liberal-to study very weak architectures such as Power [17] and ARM [START_REF] Arm | ARM architecture reference manual (armv7-a and armv7-r edition)[END_REF], whose semi-formal definitions adopt the one order per processor approach. Nevertheless, we believe that our work already yields significant insights for such architectures. We indeed provide formal definitions and insights on the level of sophistication of barriers required to guarantee sequential consistency and to correctly implement locks: we model cumulativity, whereas [START_REF] Adir | Information-Flow Models for Shared Memory with an Application to the PowerPC Architecture[END_REF] only models what was the state of the art at that time, i.e. non cumulative barriers.

Relaxing further some particularities of our model, namely the atomicity of reads and the existence of a coherence order per location, though widely assumed by modern architectures [20,17,[START_REF]Alpha Architecture Reference Manual[END_REF] may be discussed as we do in the following.

We interpret coherence [17] as the existence of a total order ws → of stores to the same given memory location. We advocate actually the fact that a memory is a shared memory if and only if there exists some sort of coherence on it: thus, it is possible to consider a point in time when all processors agree-possibly via a cache protocol -on the value present in a memory location. We believe a model that would have no global coherence-e.g. a per-processor coherence orderwould represent a distributed memory rather than a shared one: each processor would have the knowledge of its copy of a location, without considering the accesses performed to it by its neighbour, which contradicts the sharing of this location.

However, it may be possible to relax our coherence. We indeed force each processor to respect this order by considering ws → as being global and by requiring the uniproc condition. However, older version of Power architectures-pre Power 4-do not respect our uniproc condition, as they do not include read-read pairs in po-loc → . This supposes refined cache protocoles to provide the illusion of a coherent memory [START_REF] Adve | Shared memory consistency models: A tutorial[END_REF]: relaxing coherence may be at that cost.

Atomicity of reads

We believe a model with non atomic reads would also contradict the existence of a coherence order: in our model, this would lead to consider fr → non global. Thus, a read may read a given value in its processor view, and another one in another processor view, which would reveal the existence of distinct copies of a given location.

Fig. 1 .

 1 Fig. 1. A program and a candidate execution

  proc(w) = proc(r)w rfe → r w rf → r ∧ proc(w) = proc(r)

  Consider for instance the execution witness depicted in Fig. 1(c): it is valid only if the writes and reads to different locations appearing on each processor have been reordered. Indeed, if these pairs are maintained in program order-i.e. a ppo → b and c ppo → d-we have a cycle in ghb Therefore, an architecture that authorises the specified outcome cannot include write-read pairs to different locations in its ppo → .

  ppo and ab are functions that, given an execution witness, output the eponymous relations:A (ppo, int , ext, ab)We define ghb → as the union of the global relations, with if ext (resp int) is true, the empty relation otherwise:

Fig. 2

 2 Fig. 2 illustrates this condition. The outcome reveals the complete execution witness: we have c ws → a (by x final value) and a rf → c (by r1 final value). The

  ppo-tso → , false, true, λX.∅) Thm. 2 shows the following criterion, where as valid (w.r.t. any A ≤ Tso) executions that would be valid on Tso ǫ : A. check Tso (X) acyclic( can conclude that the outcome of Fig.1may show up on a Tso machine, as it does not exhibit any cycle in

Fig. 3 . 3 : 1 (

 331 Fig. 3. Study of iriw

→ 3 : 2 (

 32 are not considered global in Tso ǫ , there is no need to compensate them: the cumulativity power of this barrier applies only to external rf →. Furthermore, all pairs preserved by the program order in Tso ǫ are to be preserved, INRIA as depicted by the placement condition fenced → = ppo-tso → in the following corollary of Thm.Corollary Barriers restoring Tso ǫ ).

rfe→

  are considered global in both Tso and Sc, and Sc hinders the store buffering relaxation by its ppo → definition, Thm. 4 applies. Hence to restore Sc from Tso, it suffices to fence all pairs in ppo-sc → \ ppo-tso → = W R, where W R (W × R) ∩ po →, as expressed by the following corollary of Thm. 4: Corollary 3 (Barriers restoring Sc from Tso).

Fig. 4 .

 4 Fig. 4. A generic Read-Modify-Write in PowerPC assembly

Fig. 5 .

 5 Fig. 5. Lock and unlock in PowerPC , where initially r3 = ℓ, r4 = 0 and r5 = 1

  . satisfies what we call the drf requirements, drf programs have Sc semantics:

Theorem 5 (

 5 Drf requirements ensure Sc semantics to drf programs).

  po → between the barrier of the lock and the one of the unlock: cs(ℓ, (r, c), (b, w)) (Lock(ℓ, (r, c)), {e | c po → e po → b}, Unlock(ℓ, r, (b, w)))

2 ab→ m 2 2 . 1 lock → m 2 po→ m 3 . 2 ab→ m 3 . 1 ab → r * 2 .

 2221232312 ⇒ (m ab → r) (export B-cumulativity) Furthermore, if cs 2 import barrier c 2 orders read-write and read-read pairs locally, we have r * . import(b) ∀m 1 m 2 , (m 1 po → b po → m 2 ∧ m 1 ∈ R) ⇒ (m 1 ab → m 2 ) (import base) This is already enough to guarantee compatibility of lock ℓ It also guarantees compatibility of lock → and po →: as both relations are transitive, a cycle in their union leads to a cycle in lock → ; po →. Therefore, consider three events m In this case, m 3 is in po → after cs 2 import barrier, thus we have r * By B-cumulativity of cs 1 export barrier, we also have m Therefore m 1 and m 3 are in this order in (

→ m 3 Fig. 6 .∧ ∀m 1 wm 2 ,→ m 2 ) ⇒ (m 1 ab→ m 2 ) 2 ab→ m 3 1 ab → r * 2 by cs 1

 36221223121 Fig. 6. Figures on locks

RR n 7152

We elide barrier semantics, which we study in detail in Sec.

INRIA

Acknowledgments

We thank Damien Doligez, Xavier Leroy, Susmit Sarkar and Peter Sewell for invaluable discussions, Assia Mahboubi and Vincent Siles for advices on the Coq development, Jules Villard and Boris Yakobowski for comments on a draft.