A Lalaoua
email: lalaouaadel@gmail.com

A Bouabdallah

Effect of a dipolar magnetic field on the stability of spherical Taylor vortex flow

Keywords: CFD simulation, Spherical Couette flow, Taylor vortex flow, Dipolar magnetic field

The spherical Couette flow system with imposed magnetic fields offers the possibility of exploring a wide variety of instabilities and has a major importance in the understanding of geophysics and astrophysics phenomena. The flow of an electrically conducting fluid in an annulus between two concentric rotating spheres subjected to a dipolar magnetic field is investigated numerically using a three-dimensional computational fluid dynamics (CFD). The outer sphere is stationary while the inner one rotates freely about a vertical axis through its center. The spherical shell is completely filled with liquid gallium. The numerical studies are performed for the medium gap width β=0.18, and carried out for a wide range of Hartmann numbers (Ha). It is established that the dipolar magnetic field deeply affects the onset of Taylor vortex flow and its structure in which significant topological changes on the flow configuration are observed for different Hartmann number. As Ha increases, it is found that the Taylor vortex flow regime is delayed.

Introduction

The flow patterns in an annulus between two concentric rotating spheres has a major interest in many branches of physics and technology where centrifugal force plays a dominant role. The transitional phenomena encountered in this flow are of fundamental relevance for the understanding of global processes in the planetary atmospheres as well as in astrophysical and geophysical motions. Many theoretical, experimental and numerical studies have been conducted on spherical Couette flow in order to understand the flow behavior and determine a general map of the laminarturbulent transition, Wimmer [1], Marcus and Tuckerman [START_REF] Marcus | Steady states[END_REF], Hollerbach et al. [3], Nakabayashi et al [4], Bühler [5], Yuan [6]. On the other hand, the presence of a magnetic field imposed on this flow, known as MHD spherical Couette flow, crucially affects the flow structures and the appearance of instabilities. Numerous researchers have extensively studied this problem, both numerically and experimentally under a variety of imposed fields and magnetic boundary conditions. Among these are Hollerbach [7,8], Hollerbach and Skinner [9], Schmitt et al. [10], Nataf et al. [11], Travnikov et al. [12], Gissinger et al. [13], Kaplan [14]. Numerical studies of Dormy et al. [15] and Hollerbach et al. [16] highlight the nature and structure of the flow that appear when the magnetic field lines are not parallel to the rotation axis, as for a dipolar field. The spherical Couette system has also been proposed for producing a dynamo (Cardin et al. [17], Kelley et al. [18], Sisan et al. [19]). In the present work, a numerical investigation is conducted in spherical Couette flow with an imposed dipolar magnetic field when the inner sphere rotates freely about a vertical axis through its center, from west to east with a prescribed angular velocity Ω 1 , while the outer sphere is kept stationary. The calculations are carried out for a wide range of Hartmann number (Ha). This problem has relevant applications in geophysical and astrophysical (stars, planetary interiors), where configurations similar to MHD spherical Couette flow are often encountered.

Numerical modeling

Consider the motion of a viscous incompressible fluid (liquid gallium) of kinematic viscosity , density , magnetic diffusivity  and magnetic permeability  0 contained in a spherical annulus between two rotating concentric spheres, as shown in figure 1(b). The geometry is fully determined by the gap width β = (R 2 -R 1 )/R 1 which has been kept constant and equal to 0.18 throughout this study, where R 1 and R 2 are the radii of the inner and outer spheres, respectively. Both outer and inner spheres are considered insulating. There are two dimensionless numbers that completely determine the flow behavior: the Reynolds number and Hartmann number defined as follow:

Re= ( 1 R 1 2 )/ (1) Ha= (B 0 R 1 2 )/() 1/2 (2)
Points in the domain are defined by the spherical coordinates (r, , φ) with:

[R 1 , R 2 ] with R 1  r  R 2 -Meridional Position: [0, ] with 0     -Circumferential position: φ[0, 2] with 0  φ  2
The governing equations for this problem are as follows:

.V=0 (3)
(V/t)+(V.)V= -P+ 2 V+1/ 0 ( B)  B ( 4
)
B/t=   (V  B)+  2 B (5) .B=0 (6)
Where P and V are the pressure and velocity components (u, v, w), respectively. Time is denoted by t. B is the magnetic field, which contains the imposed dipolar magnetic field B d defined as:

B d = B 0 (R 2 /r) 3 (2cos  er + sin  e  ) ( 7
)
B 0 is the intensity of the field at the equator on the outer surface of the fluid (r = R 2 ).

The boundary conditions used in this study are:

-r = R 1 , u = v = w = 0; -r = R 2 , u = v = 0 and w =  1 R 1 sin; - = 0, (u/) = v = (w/); - =, (u/) = v = (w/).
No-slip boundary conditions are applied at all walls. The spherical annulus is divided into equally spaced intervals in the meridional (θ) and circumferential (φ) directions, and is clustered in the radial (r) direction in order to refine the grids near the walls of the spheres where there is a high shear, as shown in figure 1(a). In this study, several calculations have been performed, to see the impact of the grid density on the numerical results (mesh dependence). The converged solution from the coarse mesh was interpolated for use as an initial solution for the medium mesh, and likewise the converged solution of the medium mesh was used as an initial solution for the finer mesh.

Main Results

Flow patterns

Figure 4 shows the contours of the pressure field on the outer sphere for several Hartmann number. We have firstly examined spherical Couette flow without an imposed magnetic field (Ha=0), in order to validate our numerical calculations as well as verifying the correctness of CFD code. When the Reynolds number reaches a critical value, Re c1 =980, two steady rolls appear, one on each side of the equator, called one-vortex flow. Our numerical result agrees very well, both qualitatively and quantitatively, with previous work for the same geometry [2, 4and 5]. However, when the rotational Reynolds number of the inner sphere is fixed and a magnetic field is applied to this hydrodynamical state, additional magnetohydrodynamic effects are generated. As illustrated in figure below, the inhibiting role of the magnetic field; the rolls at the equator move toward the pole when the Hartmann number is further increased. This flow mode is strongly damped by the applied field.

Tangential velocity distribution

Figure 3 shows the tangential velocity distribution at a fixed Reynolds number Re c1 =980, and Hartmann number increasing from 0 up to 4600. The velocity profiles are plotted in dimensionless form in which the tangential velocity is divided by the surface speed, and the radial distance from the wall of the inner sphere is divided by the annular gap (gap width=(r-R 1 )/d, where d is annular space between the coaxial spheres). The salient features of the numerical profiles are summarized as follow:

 For the case without imposed magnetic field, Ha =0 and Re c1 =980, the profile is monotonically decreasing and it is analogous to the laminar profile in classical Taylor-Couette flow.  At low Hartmann number, Ha=6, the profile is still monotonic but slightly deformed near the outer sphere.  As the intensity of the magnetic field is further increased, it is observed that the velocity profiles are completely deformed, having negative values in the whole annular gap. Note also that the tangential velocity becomes zero at the outer sphere.

Conclusion

We have investigated numerically the flow behavior of an electrically conducting fluid in an annular gap between two rotating concentric spheres, when the inner sphere rotates and the outer one is stationary, to a dipolar magnetic field.

The fluid field was simulated using a three-dimensional CFD, Fluent software. The specific case considered is that with a medium gap width β = 0.18 and a wide range of Hartmann number, 0 ≤Ha≤ 6000. In each case, we have increased the Hartmann number for a fixed Reynolds number, and studied the resulting balance and competition between magnetic and inertial effects. We found that increasing the Hartmann number stabilizes the flow and delayed the occurrence of the Taylor vortices at the equator.

  a) Grid discretizing the computational domain b) Spherical Couette geometry Fig. 1: Sketch of spherical Couette flow system

Fig. 2 :Fig. 3 :

 23 Fig.2: Flow patterns for different Hatmann number at fixed Reynolds number, Re c1 =980/ pressure distribution


Simon Castellan
email: simon.castellan@ens-lyon.fr

Weak memory models using event structures

In this article, we investigate a denotational semantics based on event structures for a very simple imperative and concurrent programming language. The model incorporates behaviours of weak memory models such as reordering of instructions and non-locality. Our model can then be used to dene a function from programs to their possible outcomes that can be used to give a formal semantics to a processor or a programming language.

Most of the semantic ideas come from game semantics and its recent development based on event structures, but taking advantage of the rst-order setting, we present in this paper a selfcontained simplication of these ideas.

1.

Introduction

Compiler and hardware optimizations The rst guideline to model concurrency was Lamport's sequential consistency (SC) [START_REF] Lamport | [END_REF] which states that the semantics of concurrent program is the set of its possible sequentializations, called interleavings.

This model although very simple to reason with, is nowadays disconnected from reality. To improve performance of sequential programs, compilers and processors aggressively reorder instructions concerning distinct parts of the memory. As a result, it is now common to observe executions of concurrent programs that break sequential consistency because of these optimizations. For instance, the parallel execution of the following threads on a modern processor can lead to the end result r 1 = 0 ∧ r 2 = 0 which no interleaving predicts:

a := 1 b := 1 r 1 ← b r 2 ← a
In this snippet, a and b stand for shared variables (initialized to 0) accessible to both threads while r 1 and r 2 denote registers that are thread-local. Assignments of shared variables (:=) are called stores whereas assignments from shared variables to registers (←) are called loads.

The processor (or the compiler) can decide to permute the memory operations within a thread of this program as they hit distinct variables. The sequential behaviour of each thread is not altered by this optimization but once the two threads are put in parallel this turns out to break SC.

Moreover, modern architectures have caches so that threads do not share the same view on the memory. For instance in the following example appearing in the Intel documentation:

a := 1 b := 1 r 1 ← a s 1 ← b r 2 ← b s 2 ← a
it can be observed that r 1 = s 1 = 1 but r 2 = s 2 = 0 even if the platform is not allowed to permute the memory reads on a and b of each thread.

Hardware vs software specications These optimizations create the need for a clear specication of which behaviours are allowed on a given platform. Indeed, on the one hand, processor manufacturers need to specify which behaviours assembly programs have, to provide the user with guarantees. Those specications dene a particular execution model that the processor exhibits and as a consequence we possess robust formalizations of them (see eg. [START_REF] Alglave | A formal hierarchy of weak memory models[END_REF]).

On the other hand, programming language designers need to explain the possible run-time behaviour of valid programs so users can reason (informally or formally) about it.

Because a programming language can be implemented on several architectures, and compilers should be allowed to optimize the program, those specications are much more relaxed. As a result, their formalization is often non-satisfactory: Java's specication is unsound [START_REF] Sevcík | On validity of program transformations in the Java memory model[END_REF][START_REF] Cenciarelli | The java memory model: Operationally, denotationally, axiomatically[END_REF] and C11's specication allows undesired out of thin air behaviours [START_REF] Batty | The problem of programming language concurrency semantics[END_REF].

In this article we will focus on modelling behaviours appearing in hardware specications.

Mathematical description of executions Such specications should be as formal as possible to avoid ambiguities. This requires a mathematical language in which to express the desired constraints.

Two such languages are popular: an axiomatic approach is followed by [START_REF] Mador-Haim | An axiomatic memory model for POWER multiprocessors[END_REF][START_REF] Alglave | A formal hierarchy of weak memory models[END_REF] which gives axioms satised by valid executions and an operational approach based on modeling the platform as an idealized machine [START_REF] Sarkar | Synchronising C/C++ and POWER[END_REF][START_REF] Batty | Clarifying and compiling C/C++ concurrency: from C++11 to POWER[END_REF].

In this paper we follow a dierent approach: as [START_REF] Cenciarelli | The java memory model: Operationally, denotationally, axiomatically[END_REF] we would like to develop a denotational semantics based on causality between memory events to observe concurrency as a rst-class notion and reduce the size of the model. Unlike this paper which works with an abstract structure called conguration theories, we work with event structures [START_REF] Winskel | Event structures. In Petri Nets: Central Models and Their Properties, Advances in Petri Nets[END_REF] which are a concrete representation for specic conguration theories. Event structures comprise a set of events equipped with a partial order representing causality and a binary relation denoting conict between events that are mutually exclusive. They are much more concrete and compact.

An advantage of this approach is that the resulting semantics is compositional, derived by induction on the syntax and not extracted from an operational semantics. We believe that compositional semantics and modular reasoning are key to be able to scale to large programs. Moreover, using causality instead of traces (as in eg. [START_REF] Burckhardt | Verifying local transformations on relaxed memory models[END_REF]) allows us to escape the combinatorial explosion inherent to trace-based models of concurrency.

Game semantics based on event structures A recent line of work [START_REF] Rideau | Concurrent strategies[END_REF][START_REF] Castellan | The parallel intensionally fully abstract games model of PCF[END_REF][START_REF] Castellan | La stratégie de la fourchette[END_REF] has developed a game semantics for concurrent higher-order languages based on event structures. In this article, we want to take advantage of the model and the constructions to give a semantics to a simple rst-order toy language, complex enough to illustrate the phenomenon at stake. This paper assumes no prior knowledge of these models: the construction of the model is selfcontained. Ideas and intuitions directly come from seminal papers of game semantics [START_REF] Abramsky | Full abstraction for Idealized Algol with passive expressions[END_REF][START_REF] Ghica | Angelic semantics of ne-grained concurrency[END_REF] and have been simplied in this rst-order setting. Using this technology, it is very easy to extend our model to fully-edged programming languages with functions, control, recursion, and higher-order features.

Contribution of the paper This paper explores the usage of game semantics techniques to give an event structures-based denotational account of weak memory model. In this paper, a particular model is chosen although we believe this framework can be adapted to a great variety of models.

Where the axiomatic approach species which executions are valid, our approach builds directly the correct executions. Moreover, event structures allow to represent several incompatible executions in a compact form by sharing the common parts.

A naive implementation of the model presented here as well as a few variants is available at http://iso.mor.phis.me/memory.

Outline of the paper In Section 2, we dene event structures and the constructions on them that we need in order to build our model. In Section 3, we introduce the language we study and outline the construction of the model. In Section 4, we interpret each term as a labelled event structure where the behaviour of variables is left abstract. These event structures represent the dependency between the instructions enforced by the platform. In Section 5, we explain how to wire a chosen memory model in the interpretation of Section 4 to recover a complete description of executions.

Event structures

As mentioned in the introduction, we use event structures to analyze both the concurrency and the non-determinism (due to races) inside programs.

Denitions and notations

In this article, we use event structures with binary conict:

Denition 1 (Event structures). An event structure is a tuple (S, ≤ S , # S ) where S is a set of events equipped with a partial order ≤ S (called causality of S) and a binary symmetric irreexive relation # S (called conict relation of S) satisfying the following two axioms:

• (Conict inheritance) For all s, s , s ∈ S such that s # S s and s ≤ s , then s # S s (in this case, the conict s # S s is said to be inherited from s # S s ) • (Finite causes) For all events s ∈ S, the set [s] = {s ∈ S | s ≤ s} is nite. A labelled event structure is a pair (S, lbl) where S is an event structure and lbl : S → L is a function from the events of S to a set L of labels. We will often omit the labelling function when the context is clear.

The causality of S has the following interpretation: if s ≤ s then for the event s to occur, the occurrence of s is necessary. In particular, causality is conjunctive: if s 1 ≤ s and s 2 ≤ s then the occurrences of s 1 and of s 2 are necessary to that of s. We write s S s whenever s < s and there is no events in between s and s . This relation is called the immediate causality.

The relation # S represents the non-determinism of the system: two events in conict cannot occur together in the same execution. By conict inheritance, this relation is generated by a relation of minimal conict: s S s whenever s # S s and for all s 0 ≤ s and s 0 ≤ s such that s 0 # S s 0 then s 0 = s and s 0 = s . Two events s, s ∈ S are said to be concurrent when they are incomparable for ≤ S and they are not conicting.

To give a graphical representation to a labelled event structure (S, lbl), we represent the labels,

S and

S rather than ≤ S and # S as it is more compact.

Example 1. The following event structure is the result of the interpretation in our model of the term r ← a a := 2 b := 1 (variables are initialized to zero):

Re (r=2) a Wr (2) a Wr (2) a L L R Re (r=0) a L L R
Wr (1) b There is a race to determine in which order the load and the store on a are scheduled while the store on b is independent of the other two events.

The notion of conguration (states of the system) is central in the theory.

Denition 2 (Conguration). A conguration of an event structure (S, ≤ S , # S ) is a nite subset

x of S satisfying the two conditions:

• (Down-closure) If s ∈ x then [s] ⊆ x (ie. x is down-closed for ≤) • (Consistency) If s, s ∈ x then ¬(s # S s ).
The set of congurations of S is written C (S) and is naturally ordered by inclusion. A consequence of the axioms of event structures is that if s ∈ S, [s] ⊆ S is a conguration of S.

Simple parallel composition and sum of event structures

Denition 3 (Simple parallel composition). Given two event structures S and T we form the event structure S T called the simple parallel composition of S and T , dened by:

• Events: {0} × S ∪ {1} × T (Tagged disjoint union) • Causality: ≤ S T = { (0, s), (0, s ) | s ≤ S s } ∪ {((1, t), (1, t )) | t ≤ T t } • Conict: # S T = { (0, s), (0, s ) | s # S s } ∪ {((1, t), (1, t )) | t # F t }
The parallel composition S T is the system obtained by letting the systems S and T evolve concurrently without interferences (conict or causality). As a consequence, congurations of S T are in one-to-one correspondence with pairs of congurations of S and T . Wr (2) a Wr (1) a L L R Wr (2) b Non-deterministic sums of event structures are dened similarly as parallel composition except that S and T are set in conict: executions (or congurations) are either contained in S or in T .

Denition 4 (Sum of event structures). Given two event structures S and T we form the event structure S + T dened by:

• Events: those of S T • Causality: that of S T • Conict: that of S T plus every pair ((i, s), (j, t)) with i = j. Example 3. Sums of event structures will be used to represent abstract load operations. For instance a load on a variable a whose context is not known can be represented as a sum of its possible outcomes (in any execution a given load reads only value):

R (0) a R (1) a R (2) a . . .
These operations naturally extend to labelled event structures by letting lbl S0 S1 (i, e) = lbl S0+S1 (i, e) = lbl Si (e).

Prexing and concatenation

In the following, we will often want to concatenate event structures to represent sequential composition. To allow for the instructions to be reordered we need this composition not to be completely sequential in order to break some causalities.

To that end, we introduce a relaxed concatenation operator.

Denition 5 (Concatenation). Let (S, lbl : S → L) and (T, lbl : T → L) be labelled event structures and R ⊆ L × L be a relation satisfying:

• for any t ∈ T , there is a nite number of s ∈ s such that (lbl(s), lbl(t)) ∈ R • for any t ∈ T , there does not exist s, s ∈ S such that s # S s and both s ≤ S⊗ R T t and

s ≤ S⊗ R T t.
where ≤ S⊗ R T is dened as transitive closure of ≤ S T ∪{(0, s), (1, t) | (lbl(s), lbl(t)) ∈ R}. We form the labelled event structure S ⊗ R T as follows:

• Events and labels: Those of S T

• Causality: ≤ s⊗ R T • Conict: s # s i there exists s 0 ≤ S⊗ R T s and s 0 ≤ S⊗ R T s such that s 0 # S T s 0 .
In S ⊗ R T , S and T occur concurrently except for some causalities from S to T specied by R.

An instance of this is prexing: let (S, lbl : S → L) be an event structure and l ∈ L a label. We write l • S for {l} ⊗ {l}×S S. The event structure l • S starts by doing l rst and then proceeds to do S.

Setting up the stage

In this section, we introduce the syntax for a simple concurrent imperative programming language.

We then discuss the general structure of our model.

Syntax of our language

For the purpose of this article we introduce a very simple language which features enough interesting behaviours to illustrate the model. We suppose given two disjoint sets of variable names a, b, c, . . . ∈ S for shared variables between threads and r, s, . . . ∈ R for register (thread-local) variables. The syntax is as follows:

e, e :: 1.

= { Arithmetic expressions } k ∈ N | r ∈ R | e +
Variables are initialized to zero at the beginning of an execution.

Open and closed semantics

In the rest of the paper, we show an example of a possible model based on event structures allowing for instructions reordering and non-locality.

The specication of such a model can be split into two parts:

• The processor part which explains which instructions may or may not be permuted inside a thread.

• The memory part which explains how memory operations in one thread are propagated to the others.

We believe these two parts should be cleanly separated in the model and should be independent from one another as it is implicitly the case in existing models (eg. in [START_REF] Alglave | A formal hierarchy of weak memory models[END_REF]).

The rst step is what we call open semantics: it is about computing the exact control ow of the program leaving the side eects aside. It interprets a program Γ p as if it was a pure functional program λΓ.p where the operations of read and write are kept abstract and not specied and ; is not interpreted as sequential composition but as something that allows concurrency between instructions that can be reordered. This construction is presented in Section 4.

The second step is what we call closed semantics: it applies the λΓ.p we get from the rst step to implementations of memory cells (one for each variable in Γ). Giving the semantic behaviour of these cells is exactly as giving the formal semantics of the memory: how reads and write are propagated along threads. This construction is presented in Section 5.

For each step, dierent choices can be made, corresponding to dierent architectures. In Section 4 and 5, we pick a possible choice for each component. Our semantics will map programs over a context Γ to event structures with labels in the set

L Γ = {Wr (k) a , Re (r=k) a | a ∈ Γ, k ∈ N, r ∈ R}. There is an obvious map v : L Γ → Γ dened by v(Re (r=k) a ) = a and v(Wr (k) a ) = a.
Environments To handle thread-local variables, we will use an environment to pass down their values as we compute the interpretation. An environment will be a map ρ : ∆ → N assigning to each thread-local variable a value. Such an environment extends naturally to arithmetic expressions with variables in ∆ by the following equations:

ρ(k) = k ρ(e + e ) = ρ(e) + ρ(e ).
Interpreting threads Given a thread Γ; ∆ t and an environment ρ : ∆ → N we dene a labeled event structure t ρ as follows:

• a := e; t ρ = Wr (ρ(e)) a

• t ρ we perform the write on a and then continue to t. This interpretation is very simple: threads are interpreted by sequential event structures: two events are either comparable or conicting. There is no in-thread concurrency as no instructions can be permuted.

Example 4. On the program p = (r 1 ← a; b := 1) (r 2 ← b; a := r 2 ), this gives the following event structure (N is assumed to be {0, 1} to simplify the picture):

Wr (1) b Wr (1) b

Wr (0) a Wr (1) a Re (r1=0) a L L R Re (r1=1) a L L R Re (r2=0) b L L R Re (r2=1) b L L R 4.
Open semantics

In this section we develop an open interpretation that allows permuting operations that do not target the same variable. This behaviour can be found in the Alpha architecture [START_REF] Alglave | A formal hierarchy of weak memory models[END_REF]. In particular, we forbid permuting loads from the same variable even though this optimization is sequentially valid. This particular choice is simple to present as it is uniform but the theory supports other choices.

In the semantics, we represent instructions that can be reordered by concurrent events. The goal of this section is to build a semantics similar to the one of Section 3.3 which allows for concurrency inside a thread.

Operation dependency

The challenge of this interpretation is to determine what memory operations are causally related.

Indeed, in the interpretation we want to replace the earlier denition: a ? For instance, we do not know which stores depend on r: we can only observe the value written, not the arithmetic expression actually computed. To that end, we need to enrich our labels to contain information about registers. But the problem is more subtle than that:

Example 5. We want our semantics to compute the following event structure for the program r 1 ← a; b := r 1 r 2 ← b; a := 1:

Wr (0) b Wr (1) b Re (r1=0) a L L R Re (r1=1) a L L R Re (r2=0) b Re (r2=1) b
Wr (1) a

We observe that a := 1 only generates one event where b := r 1 generates two. We have to track the dependency in r 1 of the store to b in the rst thread and duplicate accordingly the write event, while the store of the second thread is independent of r 2 and is represented by a single event.

To solve this, we need to determine how many reads an operation depends on. Moreover, we need also to track the values read, not to put causal links between results of incompatible reads. This

(ρ, Wr (k) a ) d (ρ , s) ≡ ρ ⊆ ρ ∧ v(s) = a (ρ, Re (r=k) a ) d (ρ , s) ≡ ρ ⊆ ρ ∧ r ∈ dom(ρ )
We do not need the environments to carry values of registers anymore: any operation that needs the value of a register will give rise to one event per value possibly read. However to compute which registers an operation depends on, we need to keep track of the register bindings. Indeed the thread a := e; t depends on any read on any register bound to a (ie. registers whose values are loaded from a). Therefore to dene the semantics by induction, we will maintain an environment σ : ∆ → Γ containing exactly this information.

Semantics of threads

Assume we have a thread Γ; ∆ t.

Stores Suppose t = (a := e; t ), and an environment σ : ∆ → Γ. The partial environment ρ for this thread is dened on D = fv(e) ∪ σ -1 (a) where σ -1 (a) is the set of registers bound to a in σ. We let:

t σ =   ρ:D→N ρ, Wr (ρ(e)) a   ⊗ d t σ .
(Recall that ρ(e) stands for the extension of ρ to arithmetic expressions with registers in D.) This picks a non-deterministic value for each read that has to occur before the write, performs the write and proceeds to t letting ⊗ d insert the right causalities between the writes and t .

Loads Suppose t = (r ← a; t ), and an environment σ : ∆ → Γ. This time we let D = σ -1 (a):

t σ =   n∈N ρ:D→N ρ[r ← n], Re (r=n) a   ⊗ d t σ[r←a] .
We proceed similarly to writes but we also pick non-deterministially the value that is read.

Semantics of programs

As before, given a program Γ t 1 . . . t n we let t 1 . . . t n = t 1 ∅ . . . t n ∅ . This gives the desired event structure with enough concurrency to express possible reorderings of instructions.

Having done the construction we project labels in L Γ to L Γ by forgetting the register environment: it is not needed anymore.

Example 6 (Read/Write reordering). Assume we have the thread a, b r ← a; b := 1 in the empty environment. Computing b := 1 r →a is easy as there is no dependency for this instruction in this environment: D will be empty. This yields the event structure with a single event labelled (∅, Wr (1) b ). It follows that r ← a; b := 1 = r ← a b := 1 as those events are not in d :

({r → 0}, Re (r=0) a ) ({r → 1}, Re (r=1) a ) (∅, Wr (1) b )
For the thread a, b r ← b; a := r the situation is dierent. Computing a := r r →b needs duplication as D will be {r}: the value written depends on r. This gives the following event structure n∈N ({r → n}, Wr (n) a ). The whole thread gives then:

({r → 0}, Wr (0) a ) ({r → 1}, Wr (1) a ) ({r → 0}, Re (r=0) b ) L L R ({r → 1}, Re (r=1) b ) L L R 5.

Memory models

Given the open interpretation of a program p, we would like to close it by restricting the scope of the shared variables to p the environment cannot modify it anymore1 . To do so, we need to dene formally the behaviour of the memory: which sequences of memory operations are valid according to our model? Depending on the architecture dierent behaviours can be accepted. Throughout this section, for simplicity of presentation we make one assumption: the memory behaves as a server that receives commands (reads and write) in a total order, this assumption is however non-necessary. (See section 5.4).

Denition 6 (Linear memory model). A memory model is a prex-closed subset of (L a ) * , the set of nite lists (or traces) of memory events concerning a single xed variable a.

Given a linear memory model T , we will write T (b) for a given variable b to denote the set of memory events allowed on variable b simply obtained by substituting b for a in the traces of T . Note that in order to prove theorems quantied over all memory models, one would need more axioms in order to get only meaningful memory models, but the constructions presented here do not require them.

The goal of this section is to build the closed semantics Γ p T of a program Γ p with respect to a memory model T by eliminating behaviours that are not in T . Example 7 (A sequential memory). The rst memory model that comes to mind is that of a sequential memory. Consider the grammar with non-terminal symbols (T k ) k∈N dened as follows:

T k ::= Re (r=k) a • T k | Wr (n) a • T n | .
Then the language generated by T 0 ⊆ (L a ) * gives a memory model T representing a sequential memory cell initialized to zero: a load must read the last value written to it, or zero if there has been no write to it yet.

Closed semantics with respect to a memory model

In this section, we explain how to compute the closed semantics of a program Γ p with respect to a specic memory model T ⊆ (L a ) * . We start o by examining a simple example. Wr (1) a Against the sequential memory dened above, the desired result would be (the read and write must be sequentialized in certain order):

Re

a

Wr (1) a

Wr (1) a L L R Re (r=0) a L L R
There are more events in this event structure than in the open semantics as the Wr (1) a event has been duplicated. Consider now a, b a := 1 b := 2; r ← a; b := r. We have the following open semantics:

Wr (0) b Wr (1) b Wr (1) a Wr (2)
b S 6 6 ?

A 1 1 8 Re (r=0) a L L R Re (r=1) a L L R
Computing the closed semantics involves scheduling the operations on the two variables a and b in a consistent manner, which yields a more complicated picture:

Wr (1) b

Wr (1) a

Wr (0) b Re (r=1) a L L R Re (r=0) a L L R S 6 6 ?
(

b r > > H L L R Wr (1) a L L R 2)
As a consequence of the linearity assumption, two events concerning the same memory cell are either causally comparable or in conict.

The congurations (or states) of the desired resulting event structures are easier to understand than the set of events: they always correspond to a conguration of the open semantics Γ p equipped with linearization information for each variable a ∈ Γ. Congurations of Γ p that have no possible linearizations disappear while congurations that have several per-variable linearizations yield several congurations of the result. We now make this intuition formal. Projection It will be useful to project a conguration of an event structure to a particular variable. This is done through the notion of projection: Denition 7 (Projection). Given an event structure S and a set of events V ⊆ S, we form an event structure S ↓ V as follows:

• Events: V • Causality: ≤ S ∩V 2 • Conict: # S ∩V 2
In S ↓ V only the events in V are visible while the others are thought to be occurring in background or hidden. Note that any conguration x of S induces a conguration x ∩ V of S ↓ V . Given a ∈ Γ and (S, lbl) an event structure labelled in L Γ , we write S ↓ a as a short-hand for S ↓ {s ∈ S | v(lbl s) = a} the projection of S to the memory events concerning a. Any conguration x ∈ C (S) induces a conguration x ↓ a of C (S ↓ a). Wr (1) b

Wr (2) b ¦ ] ] g V 7 7 A
This is a partial-order that can be linearized in several ways, each one representing a trace:

Denition 8 (Trace of a conguration). Let (S, lbl) be a labelled event structure. A covering chain of x ∈ C (S) is a sequence s 0 , . . . , s n ∈ S such that {s 0 , . . . , s n } = x and for all i ≤ n, {s 0 , . . . , s i } is a conguration of S. A trace of x is a sequence of the form lbl(s 0 ), . . . , lbl(s n ) where s 0 , . . . , s n is a covering chain of x.

We write tr(x) for the set of traces of x.

We can dene the desired congurations of our event structure as follows. Let Γ p be a program and write Γ p its open interpretation. We dene

S p = {(x, (t a ) a∈Γ ) | x ∈ C ( Γ t ) and ∀a ∈ Γ, t a ∈ tr(x ↓ a)}.
The set S p is naturally ordered: (x, (t a )) (y, (t a )) if x ⊆ y and for all a ∈ Γ, t a is a prex of t a . Such pairs are the congurations of our program. To get an event structure S such that (C (S), ⊆) is order-isomorphic to (S p , ), we use a construction similar to synchronized product of event structures [START_REF] Winskel | Event structure semantics for CCS and related languages[END_REF]. First, for each (x, (t a )) ∈ S p , we equip x with a partial order written ≤ (x,(ta)) : s ≤ (x,(ta)) s i ∀(x , (t a )) (x, (t a )), s ∈ x ⇒ s ∈ x This reads: s is below s within (x, (t a )) when for every sub-conguration of (x, (t a )) where s occurs, then s must occur as well.

Proposition 1 (Prime construction). For a given memory model T , the following form an event structure written Γ p T :

• Events: (x, (t a )) ∈ S p such that (x, ≤ (x,(ta)) ) has a greatest element (such a conguration is called prime). • Causality: given by restricting to the set of events.

• Conict: (x, (t a )) # (x , (t a )) when either there exist s ∈ x and s ∈ x such that s # s or there exists a ∈ Γ such that t a and t a are not comparable for the prex order. Proof. Since congurations are nite sets, any prime conguration (x, (t a )) has a nite number of elements below it for , so in particular a nite number of prime congurations.

Moreover, assume that (x, (t a )) # (x , (t a )) and (x , (t a )) (x , (t a )). If we have s ∈ x and s ∈ x such that s # s , the conict is indeed inherited as x ⊆ x . Otherwise, write b for a variable such that t b and t b are incomparable. It is easy to see that t b and t b have also to be incomparable since the prex order is a tree.

We also have that any partial order of the form (x, ≤ (x,(ta)) ) is order-isomorphic to a unique conguration of Γ p T , hence we have that (C ( Γ p T , ⊆)) is order-isomorphic to (S p , ). Closing it with the sequential memory model dened above gives the large event structure of Figure 5.2. The key point is that there are unique events corresponding to reading r 2 = 0 and s 2 = 0 and they are in (inherited from the writes) conict so the outcome r 2 = s 2 = 0 is not possible.

Re

(r1=1) a Re (s1=1) b Re (s1=1) b Re (s2=1) a L L R Re (s2=1) a Re (r2=1) b Re (r2=1) b L L R Re (r1=1) a Wr (1) b L L R I 4 4 = a a j Re (s2=1) a Re (s1=1) b Re (r1=1) a Re (r2=1) 1 Wr (1) a L L R I 4 4 = a a j Re (r2=0) b L L R Re (r1=1) a ¡ Z Z e L L R Re (r2=1) b L L R Re (s2=1) a L L R Re (s1=1) b L L R c : : D Re (s2=0) a L L R Wr (1) a @ 0 0 7 L L R I 4 4 = a a j Wr (1) b " g g n L L R I 4 4 = a a j
! f f m © _ _ h S 6 6 ? A 1 1 8 Wr (1) b ! f f m © _ _ h S 6
However, in some situations, r 2 = s 2 = 0 can be observed. This is an example of store buering exhibited by Intel processors for instance: there might be delays between one a write is available locally and when a write is available globally.

To deal with that we need to make our model thread-aware in order to distinguish events from dierent threads. We assume now our labels carry an extra integer called the thread-id indicating the origin of this event: we now let L t Γ = N × L Γ . It is straightforward to extend our open interpretation of threads to depend on a integer representing the thread's id and then dene Γ t 1 . . . t n = Γ t 1 (1) . . . Γ t n (n).

up a conguration x of t and a list of partial-orders (x a ∈ T (a)) satisfying a condition saying that the orders of x and the x a are compatible: their union does not have a cycle. For lack of space, we do not detail this construction and content ourselves with an example.

Example 12 (A simple example of non-linear memory model). Let A be the collection of partialorders labelled in L a satisfying the following two axioms: [START_REF] Abramsky | Full abstraction for Idealized Algol with passive expressions[END_REF] the projection to any thread-id gives a linear order (operations in the same thread cannot be concurrent) and [START_REF] Alglave | A formal hierarchy of weak memory models[END_REF] every chain of the form s 1 . . . s n where s 1 is minimal is in T : every read event reads the last value written or zero if there is not any. Looking back at the example 10, we see that apart from the two events Re (r1=0) Re (s2=0)

2,a

Re (s2=1)

2,a

Wr (1) 1,a © _ _ h S 6 6 ? A 1 1 8

Wr (1) 2,b © _ _ h S 6 6 ? A 1 1 8

Conclusion

In this article, we have built a translation from a simple imperative concurrent programming language to event structures representing the possible executions. This model takes advantage of concurrency to encode the possibility of instruction reordering in order to cut down the size of the representation.

We believe this representation is a short and faithful representation of all the possible behaviours of a program that could be used to give a semantics to programming languages or processors.

This translation is heavily inspired by game semantics techniques that can be simplied in this rst-order setting. This simplied approach can be easily extended to support conditionals and while loops. The original game semantics model [START_REF] Castellan | Concurrent Hyland-Ong games[END_REF][START_REF] Castellan | La stratégie de la fourchette[END_REF] however already supports a higher-order concurrent programming language at a price of increased mathematical complexity.

In the future, we would like to use this approach to handle all the existing architectures using non-linear memory models to describe compactly behaviours of modern shared memories.

Example 2 .

 2 Parallel composition can be used to describe the semantics of threads that do not interfere. For instance, we have a := 1; a := 2 b := 2 = a := 1; a := 2 b := 2 depicted as follows:

3. 3 .

 3 An example of open semantics: a sequentially consistent semantics In this subsection, we quickly illustrate what we mean by open semantics on a simple example by dening an open semantics that does not allow reordering any instructions within a thread. Coupled with a sequential memory model, this would only exhibit the sequentially consistent executions.

•

  r ← a; t ρ = n∈N Re (r=n) a • t ρ[r←n] as the context is open, the model needs to account for all possible values, formalized as a non-deterministic sum of event structures. Interpreting programs Given Γ t 1 . . . t n a program, we dene its open interpretation p as t 1 ∅ . . . t n ∅ where ∅ is the empty environment on the empty context.

a

  := e; t ρ = Wr (ρ(e)) a • t ρ which is too sequential by something using the concatenation operator ⊗ R : a := e; t ρ = Wr (ρ(e)) a ⊗ d t ρ for a well-chosen d which indicates when a label is a necessary cause to another one. We should have Wr (k) a d s whenever v(s) = a. But what about Re (r=k)

  means that our labels should now carry a partial map R N indicating which labels are used and what are their values. Dening L Γ = [R N] × L Γ , we can now dene d ⊆ L Γ × L Γ by the following equations:

Example 8 .

 8 Consider the program p = r ← a a := 1. The open semantics of p is Re (r=0) a Re (r=1) a

Example 9 .

 9 The projection of the open semantics of Example 9 gives: Wr (0) b

Figure 2 :

 2 Figure 2: Closed semantics for a strict memory model of the store buering example

6 ? A 1 1 8 (

 68 We keep events Re (r1=0) a and Re (s1=0) b because the environment can modify it.)

a

  and Re (s1=0) b that cannot appear in a partial order of A(a), all other congurations are actually partial-orders in A(a) A(b): every conguration of the open semantics has a unique minimal synchronization with A(a) A(b). Hence the synchronized product does not change anything, yielding the result: Re (r1=1)

  Figure 1: Typing rules for the language r ← a; () and a := e; () respectively. Write fv(e) for the set of register variables appearing in e. To ensure well-formedness we use a very simple type system whose judgments are of the form Γ; ∆ t for threads and Γ p for programs. The context Γ is a set of global variables and ∆ is a set of thread-local (or register) variables. Rules are given in Figure

	fv(e) ⊆ ∆	a, Γ; r, ∆ t	∆ e	a, Γ; ∆ t	Γ; t 1	. . .	Γ; t n
	∆ e	a, Γ; ∆ r ← a; t	a, Γ; ∆ a := e; t	Γ t 1 . . . t n
				(Store to a shared variable)
		| r ← a; t		(Load from a shared variable)
		| ()			(Empty thread)

e t ::= { Threads } | a := e; t p ::= { Programs } t 1 . .

. t n

We use two dierent syntactic constructs for loads and stores to make the distinction more explicit.

Moreover, the construct r ← a; t binds r to a inside t. We use the shorthands r ← a and a := e for

This operation is similar to the restriction in π-calculus.

Acknowledgements I would like to thank Pierre Clairambault and Olivier Laurent for helpful comments, Jade Alglave and Jean Pichon for introducing me to the world of memory models.

With this, we can make a linear memory model that takes into account store buering using a grammar similarly as at the beginning of Section 5. Now our symbol is indexed over pairs (ρ, k) ∈ (N → N) × N where k is the global value of the cell and ρ(ι) is the local value in thread ι. Writing ρ[ι ← x] to update environments, we dene:

Then T ≡ T (n →0),0 gives a list of traces representing a memory model allowing for store buering.

The rst axiom says that when a read fetches the value of the global memory, then this value is available to all threads. This is similar to the Value axiom of Sparc [START_REF] Alglave | A formal hierarchy of weak memory models[END_REF].

Example 11. Considering again the program of Example 10, we can now compute the closed interpretation with the memory model T . Since now we have that Wr (1) 1,a • Re (r=1)

∈ T (a), more behaviours are allowed in particular the one where r 2 = s 2 = 0. The event structure is too big to be drawn here (but can be visualized via the implementation).

Executions in our model

In our model, complete executions correspond to maximal congurations. In more detail, given a program Γ p, a possible execution of p in a memory model T is given by a conguration x of Γ p T maximal with respect to inclusion: no more events can be added to it. From such data, we discuss here how one could recover an execution witness in the sense of [START_REF] Alglave | A formal hierarchy of weak memory models[END_REF]. In the open semantics, the program order of p is already lost because of the concurrency between events that correspond to instructions that can be executed in any order. What the open semantics gives us is the preserved program order: causalities from the program that the architecture cannot break.

We show here how to recover the read-from and write-serialization maps. We have seen in Section 5.1 that congurations of Γ p correspond to pairs (x, (t a ) a∈Γ ) in S p , where x ∈ C ( Γ p ) is an event structure in the sense of [START_REF] Alglave | A formal hierarchy of weak memory models[END_REF] (up to the fact that the partial order represents the preserved program order not the actual program order, as pointed out above). Because operations on a variable a are scheduled to be operated in a total order, it follows that any non-zero read has to be preceded by a write in t a . To dene the read-from map, we need that T satises the property: any read in a trace is either with value zero or preceded by a write of this value. The T presented above do satisfy it. The write-serialization map comes for free as traces are linearly ordered.

Non-linear memory models

The reader might have noticed that the event structures drawn in the last examples are rather large and sequential. The linearity assumption on the memory model forces the behaviour on each variable to be sequential: two events are either in conict or comparable. In this section we investigate the possibility of non-linear models to keep more concurrency in the generated event structure.

Denition 9 (Non-linear memory model). A non-linear memory model is a collection of partial orders labelled on L a closed under rigid inclusion, dened as follows: q → q when the support of q is included in that of q and the identity map is order-preserving and preserves down-closed sets 2 .

Given a non-linear memory model T , computing the closed interpretation with respect to that model is more technical. The denition of Section 5.1 relies heavily on the fact that the models are linear. If they are not, one needs to use a synchronized product of event structures [START_REF] Winskel | Event structure semantics for CCS and related languages[END_REF], that will pair 2 Also called a rigid map of event structure.