Nicolas Blanc

Claire Mayer-Laigle

Xavier Frank

Farhang Radjai

Jean-Yves Delenne

Evolution of grinding energy and particle size during dry ball-milling of silica sand

Keywords: Milling, agglomeration, Rittinger law, powder, grinding limit

The energy efficiency of dry fine grinding process of powders dramatically declines with decreasing particle size, and represents a growing concern in various cutting-edge technical applications for pharmaceutical and cosmetic products, advanced-ceramics, and food industry. In this paper, we report on a detailed experimental analysis of the long-term grinding behavior of silica sand as a model material in an oscillatory ball mill for a broad range of the values of vibration frequency and amount of powder. We show that the re-agglomeration of fine particles unambiguously explains the anomalous increase of grinding power consumption. We also find that the agglomeration phenomena are correlated with the volume fraction of the class of finest particles. A nonlinear comminution model is shown to capture this effect for the prediction of the evolution of the specific surface area.

Introduction

The grinding process is used extensively for the manufacture of cement, pharmaceutical and food products with various purposes such as calibrating the size of a raw product, extracting specific components or increasing the specific surface area and the reactivity of products. It is well known that the industrial grinding operations represent a major part of the total energy consumption at a global level. For example, clinker grinding consumes one third of the total energy needed for cement manufacturing [START_REF] Touil | The specific selection function effect on clinker grinding efficiency in a dry batch ball mill[END_REF]. Therefore, improving our understanding of the mechanisms underlying energy dissipation in milling operations has remained as a major challenge for the industry with * jean-yves.delenne@inrae.fr the aim of reducing their ecological footprint.

The energy consumption is affected by not only the properties and mechanical behavior of the material and the grinder technology but also the loading mode and the rate of energy supply.

The grinding device controls the way energy is supplied to the material and the dissipation mechanisms involved in the process such as friction and the viscosity of the carrier fluids. The material can be more or less brittle, dry or dense. It evolves during the grinding process with an increasing cohesive stress, defined as the additional stress induced by cohesive forces between particles, as the average particle diameter is reduced. Hence, for fine-milling, both inter-particle and intra-particle surface energies are to be overcome for grinding the material [START_REF] Tanaka | A new concept applying a final fineness value to grinding mechanism-grinding tests with frictional and impulsive force[END_REF]. In all cases, the grinding efficiency is very low. According to Schönert (cited by Tavares and King [START_REF] Tavares | Single-particle fracture under impact loading[END_REF]) only 4% to 8% of the total energy supplied is really consumed for the creation of new surfaces.

Several comminution laws have been proposed to link the consumed energy to a characteristic particle size of the powder. The popular models are those of Rittinger [START_REF] Rittinger | Lehrbuch der Aufbereitungskunde[END_REF], Bond [START_REF] Bond | The third theory of comminution[END_REF] and Kick [START_REF] Kick | Das Gesetz des proportionalen Widerstands und seine Anwendug[END_REF]. While the Bond and Kick models are mostly employed for coarse and intermediate size grinding, the Rittinger model is better suited for fine comminution [START_REF] Mucsi | Grindability of quartz in stirred media mill[END_REF]. This model assumes a linear relation between the specific surface area per unit of mass m S of the powder and the energy per unit of mass

m E : =, m m dS dE  ( 1
)
where  is a constant parameter governing the kinetic process. As the evolution of the system is controlled by the energy power input (which is generally constant),  represents the rate of production of specific surface area. Note that an alternative writing of this model is frequently employed using the median particle size 50 1/ m dS and assuming spherical particles. Chen et al. [START_REF] Chen | Energy-Based Analysis of Milling -Lactose Monohydrate[END_REF] showed for an oscillatory ball mill that the median particle diameter 50 d (and also other percentiles such as d10 and d90) were well fitted by Rittinger's model for the grinding of  -Lactose from 450 to 150µm. For experiments on spruce saw dust on the same type of mill, Karinkanta et al. [START_REF] Karinkanta | Impact-based pulverisation of dried and screened Norway spruce (Picea abies) sawdust in an oscillatory ball mill[END_REF] showed, however, that 50 d tends to deviate substantially from the linear trend for very fine milling ( < 20µm). This observation was attributed to the existence of a limit size in fracturing particles. For example, for dry silica sand milling a limit size of 1µm was observed by Mucsi [START_REF] Mucsi | Grindability of quartz in stirred media mill[END_REF]. Cho et al. [START_REF] Cho | Investigation of the grind limit in stirred-media milling[END_REF] found a limit size of 30 nm for silica sand in a stirred-media grinder where the particles were in suspension in water. The presence of water shields the inter-particle adhesion and hence it should decrease the formation of agglomerates that appear in fine dry milling [START_REF] Guzzo | The onset of particle agglomeration during the dry ultrafine grinding of limestone in a planetary ball mill[END_REF]. Other possible effects which reduce the grindability are: i) the existence of a brittle to ductile transition that slows down the cracks propagation in particles [START_REF] Boldyrev | Interrelation between fine grinding and mechanical activation[END_REF][START_REF] Kendall | The impossibility of comminuting small particles by compression[END_REF], ii) confined particles under high confinement have higher compression strength [START_REF] Renshaw | Universal behaviour in compressive failure of brittle materials[END_REF], iii) due to local interactions, a coating of grinding balls by the powder may occur, reducing thus stress transmission [START_REF] Austin | An analysis of fine dry grinding in ball mills[END_REF], iv) fine particles enhance air trapping inside the bed, leading to cushioning effects [START_REF] Austin | An analysis of fine dry grinding in ball mills[END_REF] To account for this limit size, Kano et al. fitted the variation of 50 d with a saturating exponential law [START_REF] Kano | Correlation of powder characteristics of talc during planetary ball milling with the impact energy of the balls simulated by the particle element method[END_REF]. This type of limit was also introduced in balance models [START_REF] Austin | An analysis of fine dry grinding in ball mills[END_REF][START_REF] Teke | Kinetics of dry grinding of industrial minerals: Calcite and barite[END_REF] or directly in comminution law such as in the Tanaka model [START_REF] Tanaka | A new concept applying a final fineness value to grinding mechanism-grinding tests with frictional and impulsive force[END_REF], which modifies the Rittinger model by assuming a limit surface [START_REF] Kotake | Influence of dry and wet grinding conditions on fineness and shape of particle size distribution of product in a ball mill[END_REF][START_REF] Choi | Applications of grinding kinetics analysis to fine grinding characteristics of some inorganic materials using a composite grinding media by planetary ball mill[END_REF][START_REF] Choi | Effect of grinding aids on the kinetics of fine grinding energy consumed of calcite powders by a stirred ball mill[END_REF].

In this paper, we present a detailed investigation of the dry grinding of silica sand in an oscillatory ball mill. We are interested in the evolution of specific surface area (SSA), particle size distribution, agglomerated SSA and consumed electrical energy as a function of the input grinding energy power. These measurements allow us to characterize the onset of agglomeration and its signature on the evolution of SSA as a deviation from the linear Rittinger regime and its level-off at larger input power. We also evidence the correlation of particle agglomeration with the production of very fine particles whose volume fraction increases proportionally to the SSA. We introduce a phenomenological model that accounts for the agglomeration by an extra energy dissipation term proportional to the created surface. The predicted asymptotic SSA is in agreement with previous experimental measurements in a ball mill.

Materials and Methods

Raw material

In this work, we used a commercial silica sand composed of 98.60% of pure silica for filtration applications, marketed by Euromortier. It is a sieved sand between 0. , implying that the particles are mostly crystalline and not amorphous ( amorphous 2.20



).

The commercial silica sand was sieved using a Rotex sieving machine to ensure that it was properly graded and to reduce spreading so as to achieve a nearly monodisperse population. We chose two sieves with close aperture diameters 0.8 mm and 1.0 mm and with a small size allowing us to do measurements using laser diffraction from the very beginning of grinding. After 10 min sieving, we obtained a fraction representing 10% of the total initial mass. The bulk density was measured to be between 1.4 and 1.6 g.cm -3 . The sieved material was used as input raw material in all experiments reported in this paper.

Milling device and grinding energy

Fig. 1a shows the oscillatory ball mill (Retsch ® MM400) used in this study and a scheme (Fig. 1b) representing one of its two 50 mL milling jars. Each jar is initially filled with a mass M of raw material and a single 25 mm-diameter steel ball. The jars vibrate horizontally at a frequency chosen between 3 to 30 Hz. The motion of the jar follows a quasi-straight line with a periodic signal:

( ) = sin(2 ), j x t A ft  ( 2
)
where f is the vibration frequency and t is time. The stroke amplitude of the jar was = 7.2 A mm ± 50µm independently of frequency. It was measured by means of a contactless position sensor. The electric power supplied to the device sets in motion the ball and the powder that it contains. The kinetic energy supplied in this way is consumed in the grinding process, but a large amount of power is dissipated by friction between the different mechanical parts of the device and through Joule effect in wires. It is therefore difficult to estimate the grinding energy, i.e. the energy for the comminution of particles. We may consider that grinding energy is directly related to the ball-jar collision energy. Following the work of Karinkanta et al [START_REF] Karinkanta | Impact-based pulverisation of dried and screened Norway spruce (Picea abies) sawdust in an oscillatory ball mill[END_REF], the friction between the ball and the jar is assumed to be negligible compared to the impact energy.

The maximum velocity of the jar, according to Eq. 2, is

=2 max j v A f  (3)
Since the ball is propelled by motion of the jar, its maximum velocity max b v is equal to that of the jar max j v . We assume that the ball-jar impact occurs when the ball and the jar have the same velocity max j v in opposite directions. This corresponds to a maximal impact energy

22 1 2 = ( ) = 8 ( ) max max i b j b b E m v v m A f   . The specific
( ) = = b mi m A f t Ei E t N MM  (4)
Note that the assumptions underlying this relation hold at weak filling ratio where the motion of the ball is not limited by the amount of material in the jar.

Parametric study

We performed a detailed parametric study in which the energy was changed by varying the frequency, the mass of the powder (related to the filling ratio) and the milling time. For the chosen range of frequencies, the ball has a high kinetic energy and the mechanical work is mostly transmitted through impacts of the ball onto the powder. Using a transparent jar, Chen et al. [START_REF] Chen | Energy-Based Analysis of Milling -Lactose Monohydrate[END_REF] have shown that for frequencies below 15 Hz the main loading mode is the rolling of the ball.

Therefore, we considered three frequencies above 15 Hz and up to 25 Hz with four different values of silica sand sample mass ranging from 6 to 20 g. Note that increasing the mass of product (thus the filling ratio) reduces the stroke of the ball.

All the samples were first dried in an oven at 65 °C during 24 hours. A first series of experiments were conducted at 20 Hz for different values of powder mass (6, 13, 17 and 20 g) and a second series were then conducted with a fixed mass (13 g) for two other frequencies (15 and 25 Hz). For each set of parameters, 10 independent grinding experiments were conducted for times ranging from 0.5 to 111 min.

For all these experiments, the consumed electric power P by the device was measured with a wattmeter Meteix ® PX 120 at the level of the electric grid. A laser thermometer Optris ® CT LT20 was also employed to monitor the jar surface temperature during the grinding at the center of the jar.

Characterization of the ground powder

At the scale of particles, scanning electron microscope (SEM) imaging was performed. At the scale of the bulk, the particle size distribution and specific surface area (SSA) was also determined.

Scanning electron microscopy

Observations of different samples of the ground powder were performed using a Phenom Pro-X SEM (France) equipped with a backscattered electron detector. The particles were directly fixed without coating on the sample holder using carbon adhesive tape and the images were captured at a voltage of 15 kV.

Particle size distribution

The particle size distribution was determined by Laser Diffraction (LD) using a Mastersizer 2000 (Malvern Instruments Ltd., United Kingdom) particle size analyzer coupled with the sample dispersion unit Hydro 2000S with ethanol as liquid carrier. Note that, as a large number of the studies carried out in our laboratory involve water-reactive powders, we preferred to use ethanol rather than water also for these experiments although water could have been equivalently used.

The results were quantified in volume based on the Mie theory [START_REF] Webb | A primer on particle sizing by static laser light scattering[END_REF]. From this particle size distribution, the SSA per unit of mass denoted LD S (in kg.m -2 ) was evaluated as

3 1 =, i LD i i S R    ( 5
)
where  is the density of silica, i the index grading class (between 0.02 and 2000 µm), i  is the volume fraction and i R the average radius of particles inside the size class i . For each sample, 3 measurements were done, and the standard deviation of the measurements were calculated.

To estimate the level of agglomeration in the bulk, we used ultrasounds with the following protocol:

 A first measurement is directly done on the powder (denoted LD S ).

 3 minutes of ultrasonic treatment is applied to the suspension.

 The sample is stirred at 2000 rpm during 5 minutes in order to eliminate potential bubbles.

 A second measurement is performed ( LD S
). The agglomerated surface of the powder is calculated as

= agl LD LD S S S  (6)

Measurement of the BET surface

The Brunauer-Emmett-Teller (BET) method, based on nitrogen absorption, was used as a reference measurement of the SSA. This measure, denoted below BET S , is expressed in units of mass as in the case of LD S . We used a ASAP 2460 (Micrometrics ® ) with a liquid nitrogen cooling system. Prior to measurements, the samples were degassed at 250°C during 48 hours under vacuum using a VacPrep 061 (Micrometrics ® ). Although this method provides an accurate value of the SSA, it has the disadvantage of being time-consuming and expensive (48 hours per sample for BET against 15 min with laser granulometry). For this reason, only the 20 Hz milled samples were tested by this method and used to calibrate the measurements by laser granulometer for all the tests with other values of parameters.

Results and Discussions

Particle Size distribution and specific surface area

Fig. 2 shows an example of the evolution of particle size distribution with time for a 13 g sample milled at 20 Hz. We see that, although the powder used as input was first calibrated between 0.8 and 1.0 mm, after 1.5 min of milling the particles are already broadly distributed over nearly 3 orders of magnitude. While milling, the main peak of the distribution shift from 100 µm to 2 µm.Fig. 3 shows SEM images of the powder for two values of milling duration. As evidenced by the PSD, the particles are highly polydisperse with angular polyhedral shapes. At the beginning of milling, the particles are slightly elongated with an aspect ratio between 2 and 3 (Fig. 3a). This elongation tends to decrease with time (Fig. 3b). . This difference can be attributed to the agglomeration of small particles as shown in Fig. 3c. In fact, as nitrogen molecules used in BET measurements are very small, they penetrate into the pore space inside the agglomerated particles. On the contrary, in laser diffraction an agglomerate is seen as a coarse particle.

As BET S measurements are closer to the real specific surface, all the measurements were scaled using the calibration curve of Fig. 4. To simplify notations, we will use S for the SSA evaluated according to this method.

Effect of milling conditions

In Fig. 5 all the data are plotted as a function of time. We clearly distinguish two parts on these curves: a nearly linear rapid increase at the beginning, followed by level-off at an upper limit of = SS  around 3200 m 2 kg -1 . As expected, the initial slope depends in a systematic way on the frequency and the mass of the product. We see that the milling rate increases both with the number of impacts (related to the frequency) and with the decrease of the amount of powder. of S is more energy-consuming than the linear model. An additional amount of energy is required to overcome the dissipation due to several different effects. One important effect is the increase of yield stress with decreasing particle size [START_REF] Mcdowell | On the micromechanics of crushable aggregates[END_REF], a well-known scale effect due to a decreasing probability of finding flaws above the critical size for the onset of crack propagation according to the Griffith criterion [START_REF] Herrmann | Statistical models for the fracture of disordered media[END_REF][START_REF] Laubie | Effective potentials and elastic properties in the lattice-element method: Isotropy and transverse isotropy[END_REF]. In this respect, it is also expected that an increasing amount of energy is dissipated by plastic deformations of the particle [START_REF] Kendall | The impossibility of comminuting small particles by compression[END_REF][START_REF] Hagan | Micromechanics of crack nucleation during indentations[END_REF]. Another important effect is that finer particles produced by grinding form a cushion between larger particles, thereby reducing stress concentration and thus the probability of particle fracture (cushioning effect) [START_REF] Austin | An analysis of fine dry grinding in ball mills[END_REF].

Finally, a major effect is the increase of cohesive stresses induced by surface forces in the granular bed as mean particle size declines. For micron-size particles, this internal cohesion prevails as compared with confining stresses and gravity [START_REF] Tanaka | A new concept applying a final fineness value to grinding mechanism-grinding tests with frictional and impulsive force[END_REF][START_REF] Opoczky | Fine grinding and agglomeration of silicates[END_REF][START_REF] Seville | Interparticle forces in fluidisation: a review[END_REF][START_REF] Nichols | A review of the terms agglomerate and aggregate with a recommendation for nomenclature used in powder and particle characterization[END_REF]. For this reason, an increasing amount of the grinding energy is consumed to overcome cohesive forces between particles or break the agglomerates of fine particles that form spontaneously inside the powder bed.

Modified Rittinger Model

The nonlinear evolution of the SSA can be accounted for by assuming an extra energy dissipation that is proportional to the created surface S . The Rittinger model can thus be modified as 0 =,

m dS S dE S   (8)
where 0 S (m 2 kg -1 ) is the initial SSA of the input powder,  is the maximum comminution rate corresponding to the created surface per unit of energy (expressed in m 2 MJ -1 ) and  (in m 2 MJ -1 ) is a phenomenological parameter accounting for all the dissipative effects briefly mentioned previously.

Eq. ( 8

This equation is similar to that introduced by Tanaka in 1954 [START_REF] Tanaka | A new concept applying a final fineness value to grinding mechanism-grinding tests with frictional and impulsive force[END_REF][START_REF] Kotake | Influence of dry and wet grinding conditions on fineness and shape of particle size distribution of product in a ball mill[END_REF] with a slightly different normalization.

The experimental data are well fitted ( 2 = 0.99 R with the least squared method) by the integrated form of Eq. 8:  is in good agreement (difference below 4%) with the results of Schellinger 1951 for the ball milling of silica sand [START_REF] Fuerstenau | The energy efficiency of ball milling in comminution[END_REF]. Interestingly, this value was determined from a comparison between the dissipated thermal energy (obtained by calorimetry) and the mechanical energy consumed by the mill (using a torque sensor).

0 0 ( ) = 1 1 exp m m E S E S S                (

Agglomeration

Fig. 7 shows the evolution of the agglomerated surface estimated by using Eq. 6 as a function of the SSA S . Below = S 1500 m 2 .kg -1 , the agglomerated surface is low and constant. A sudden increase of agglomeration is observed when S exceeds 1500 m 2 .kg -1 . Interestingly, this transition occurs for the same value of S for which the experimental results begin to deviate from the Rittinger model, suggesting that the decrease in grindability mainly reflects the cohesive surface forces and the resulting re-agglomeration of fine particles inside the powder. At low impact energies, the agglomerates can be visually identified at the end of the milling (Fig. 8a). For higher impact energies (20 Hz,6 g and 25 Hz,13 g), the agglomeration of particles eventually leads to clogging phenomena as observed in Fig. 8b. In order to clarify the effect of the finest particles, we studied the correlation between agglomeration and volume fraction d  of particles below a limit size d =0.5 µm. Fig. 9 shows d  as a function of S . As in Fig. 7, the curve is bilinear with a clear change in slope at S 1500 m 2 .kg -1 . This correlation suggests that the proportion of finest particles is a crucial parameter for the milling efficiency. We observe a similar agglomeration transition for even coarser particles by choosing a slightly larger value of d , but the cohesive effects are more clearly expressed for d =0.5 µm. Note also that, even if agglomeration occurs all along the milling, its hindering effect on the efficiency occurs only when the volume fraction of particles increases to a critical value, which is actually quite low (around 0.4%).

Energy consumption

In this section, we consider the electric energy consumed by the device and heat loss while milling.

Fig. 10 shows, as a function of time, the electric power P and the temperature T measured on the jar during the milling of 20 g of silica sand at 20 Hz.

For milling times below 72 min, P decreases and reaches a plateau. Although the origin of this transient is not clear, it may be attributed to a better lubrication of mechanical parts at higher temperatures. During this first phase, the temperature evolves linearly. After 72 min a sudden power drop occurs and P stabilizes to a lower value. In this regime, the temperature decreases exponentially, and eventually levels off. We also measured the effect of powder mass on energy consumption before after the the transition observed in Fig. 10. Let 1 P be the electric power consumed before the transition and 2 P the electric power after the transition. 1 P mainly contains the power consumed by the device, frictional interactions and particle breakage whereas 2 P contains also the effects of agglomeration. We therefore expect 2 P to follow the same trend as 1 P as a function of powder mass M for small values of the latter. To quantify dissipation due to the device, we also measured the electric power 0 P of the device with a jar containing a fixed weight of mass equal to the total mass of ball and product. Fig. 11 shows 0 P , 1 P and 2 P as a function of M . As powder mass is small compared to the mass of the jar, 0 P does not vary significantly with M . As expected, 1 P increases linearly with M , and 2 P follows initially 1 P , but tends to decrease as M further increases. It tends to 0 P , meaning that the ball stroke vanishes at large values of M by particle agglomeration and hence the whole dissipation is reduced to that of the device.

Figure 11: Evolution of the electric power as a function of the powder mass when the mass is fixed ( 0 P , squares), and when it is free before ( 1 P , circles) and after transition ( 2 P , triangles).

Conclusions

In this work, we preformed an extensive parametric study of the milling of silica sand using an oscillatory ball mill. We showed that the extra surface created by milling depends on the total energy supplied, and a dimensionless parameter ( m E ), representing the specific grinding energy, is the control parameter of the generated specific surface area and fully mediates the influence of all experimental parameters (frequency, ball stroke) on the grinding process.

For specific surface area above 1500 m 2 kg -1 , an increasing discrepancy with the classical Rittinger model was observed and shown to reflect the action of cohesive forces and its agglomerating effect on the class of fine particles. A modified model was shown to account for the agglomeration effect with the prediction of an asymptotic limit value of the SSA. Moreover, it was shown that the agglomeration is strongly correlated with the volume fraction of the smallest particles. The signature of the agglomeration phenomena was clearly identified from the electrical power consumed by the device.

Figure 1 :

 1 Figure 1: a) Picture of the ball mill MM400 used in experiments. b) Scheme of the grinding jar.

Figure 2 :

 2 Figure 2: Evolution of PSD with time (from 1.5 to 65 min) for 13 g of silica sand milled at 20 Hz. The feed size distribution is represented by the hatched area.

Figure 3 :

 3 Figure 3: SEM images of silica sand particles at short milling (6 g, 20 Hz) duration (30 s) (a) and at the end of the milling (29 min) (b). An example of agglomerates appearing due to cohesive interactions with finest particles at long milling time is also shown (c).

Figure 4 :

 4 Figure 4: Calibration curve BET S as a function of LD S for 13 g of silica sand milled at 20 Hz.

Figure 5 :

 5 Figure 5: Evolution of the SSA of the powder as a function of time.

Figure 6 :

 6 Figure 6: Evolution of the SSA as a function of the specific grinding energy for all experimental data. The Rittinger model (black dotted line) and a modified Rittinger model (red solid line) are shown; see text.

Figure 7 :

 7 Figure 7: Agglomerated surface (specific surface area liberated by ultrasound) as a function of the specific surface area for each specific impact energy

Figure 8 :

 8 Figure 8: Agglomerates (13 g,20 Hz) (left) and sticking powder on the jar wall (13 g, 25 Hz) (right) at the end of milling.

Figure 9 :

 9 Figure 9: Evolution of the volume fraction 0 .5  of particles of size below 0.5 µm as a function of

Figure 10 :

 10 Figure 10: Evolution of the electric power and temperature of the jar as a function of time for 20g 20Hz.

Table 1 :

 1 Percentage of power lost after the transition for a fixed frequency of 20Hz.Several experiments were also carried out for other values of the powder mass and vibration frequency. Similar trends were observed but with smaller values of energy power drop, as reported in Table1for different filling ratios. For all the experiments, this transition appears for

	a surface	S	2990	m 2 kg -1 , close to the asymptotic limit of the modified Rittinger model (
	0 / = 3140 S 	m 2 kg -1 ).

Acknowledgements

We thank Bpifrance for their financial support (ACA project).

References References


Florent Chevrou

Aurélie Hurault

Shin Nakajima

Philippe Quéinnec

A Map of Asynchronous Communication Models

Keywords: asynchronous communication, formal verification, refinements of communication models, Event-B 2 Distributed Systems 2.1 Distributed Executions

Asynchronous communication encompasses a variety of features besides the decoupling of send and receive events. Those include message-ordering policies which are often crucial to the correctness of a distributed algorithm. This paper establishes a map of communication models that exhibits the relations between them along two axes of comparison: the strength of the ordering property and the level of abstraction of the specification. This brings knowledge about which model can be substituted by another without breaking any safety property. Furthermore, it brings flexibility and ready-to-use modules when developing correct-by-construction distributed systems where model decomposition exposes the communication component. Both criteria of comparison are covered by refinement. We consider seven ordering policies and we model in Event-B these communication models at three levels of abstraction.

The proofs of refinement between all of these are mechanized in Rodin.

Introduction

A classic way to develop distributed algorithms is to start with a global goal, such as mutual exclusion or global agreement. A distributed version of the algorithm is then derived, either directly or by progressive transformation of the specification, e.g. by refinement. This approach dates back to early work by Dijkstra [START_REF] Dijkstra | EWD851b -reducing control traffic in a distributed implementation of mutual exclusion[END_REF], Chandy-Misra with UNITY [START_REF] Chandy | Parallel Program Design: A Foundation[END_REF], Back and Kurki-Suonio with action systems [START_REF] Back | Distributed cooperation with action systems[END_REF], or Lamport with TLA + [START_REF] Lamport | Specifying Systems[END_REF]. It is still bustling in the correct-by-construction community and Event-B [START_REF] Abrial | Modeling in Event-B -System and Software Engineering[END_REF] is a framework which embodies this methodology. At one point in the development process, communication is explicitly introduced, to express the flow of information from one site to another, and it eventually takes the form of message exchanges. When the development is conducted with formal verification, the properties of the communication are shown to be sufficient for the correctness of the algorithm. However, it is often unclear what are the specific properties of this communication that are necessary to ensure the correctness of the algorithm. Especially, it may be difficult to replace one communication model with another without doing again the complete proof.

The present work aims at alleviating these difficulties for asynchronous pointto-point communication with message ordering policies. These policies control message deliveries based on past events or involved peers, and their relative strength forms a hierarchy of communication models. To this end, we use simulation: if a model M 1 simulates another model M 2 , M 2 has less non-determinism, hence fewer behaviors. Thus a safety property proved under M 1 in a given system will hold if M 1 is substituted by M 2 (there is no guarantee of preservation for liveness properties). A distributed application is refined up to the point where communication is introduced. Then, model decomposition isolates the communication part and the hierarchy is used to choose an adequate ordering policy.

There exist several approaches to decomposition in Event-B [START_REF] Hoang | A survey on Event-B decomposition[END_REF]: sharedvariable [START_REF] Abrial | Refinement, decomposition, and instantiation of discrete models: Application to Event-B[END_REF], shared-event [START_REF] Butler | Decomposition structures for Event-B[END_REF] and modularization [START_REF] Iliasov | Supporting reuse in Event B development: Modularisation approach[END_REF]. Our map is well suited for shared-event decomposition, where variables are partitioned and a set of events are synchronized and shared by sub-models. During the refinement of a system, asynchronous communication appears via two events: send and receive. These events are isolated in a sub-model to be refined using the results of this paper.

Nevertheless, the proposed one-dimensional scale is not sufficient as several communication models may realize the same ordering policy. They often have little in common: some directly map the ordering property on high level data structures such as distributed executions while others will make use of ad-hoc concrete approaches (e.g. counters on messages) from which the property arises. Mapping the communication models depending on their level of abstraction completes the approach. Therefore, we draw a bidimensional map of communication models and use refinement as a common ground for the two orthogonal comparison criteria: refinement for simulation, and data refinement for concretization. Our results, summed up in the map in Figure 1, are proved and mechanized in Event-B. Regarding decomposition, this means once an ordering policy has been chosen across the simulation direction, the model can be refined across the concretization direction as part of a correct-by-construction development.

The outline of this paper is the following. Section 2 recalls basic definitions of the theory of asynchronous distributed systems and their modeling in Event-B. Section 3 presents seven communication models and proves the hierarchy of their ordering policies, based on simulation, using refinement. Section 4 presents variants of the models based on message histories, and proves that the hierarchy still holds. Section 5 refines them one step further towards practical concrete models. Section 6 discusses proof effort and localization. Section 7 provides related work.

The page http://hurault.perso.enseeiht.fr/MenagerieOfRefinements contains all the models discussed in this paper and gives indications to replay the proofs. events are ignored. The partial order is named the causal order [START_REF] Lamport | Time, clocks and the ordering of events in a distributed system[END_REF][START_REF] Raynal | Distributed Algorithms for Message-Passing Systems[END_REF], and it abstracts independent events. Events occur on peers: a labeling function states where the event e has occurred. Assuming interleaving of independent events and no true concurrency, a run is a linear extension of a distributed execution.

Let PEER be the set of peers, MESSAGE an enumerable set of messages identifiers, and COM {Send, Receive} the communication labels. Definition 1. A distributed execution (E, ≺ c , com, mes, peer) is a partially ordered set with labeling functions, where E is an enumerable set, ≺ c is a partial order on E, and com, mes and peer are labeling functions from E to COM, MESSAGE and PEER. An event e that occurs on peer(e) is either the sending or the reception (com(e)) of message mes(e). (E, ≺ c , com, mes, peer) satisfies:

no message is sent or received more than once:

∀e, e ′ ∈ E : com(e) = com(e ′ ) ∧ mes(e) = mes(e ′ ) ⇒ e = e ′ -a receive event is preceded by a send event:

∀e ∈ E : com(e) = Receive ⇒ ∃e ′ ∈ E : com(e ′ ) = Send ∧ mes(e ′ ) = mes(e) ∧ e ′ ≺ c e events occurring on the same peer are totally ordered:

∀e, e ′ ∈ E : peer(e) = peer(e ′ ) ⇒ e ≺ c e ′ ∨ e ′ ≺ c e Definition 2. A run σ = (E, ≺ c , < σ , com, mes, peer) extends a distributed execution (E, ≺ c , com, mes, peer): (E, < σ ) is a linear extension of (E, ≺ c ).

Event-B

A model in Event-B [START_REF] Abrial | Modeling in Event-B -System and Software Engineering[END_REF] is an abstract state machine containing state variables, invariants, and events (the word "event" refers either to an element of a dis-tributed execution or a part of an Event-B machine -a transition predicate -; the context hopefully makes it clear which is which). An event E parameterized by x has the form

EVENT E ANY x WHERE G(v, x) THEN A(v, x) END, where G(v, x)
is the guard of the event and A(v, x) an action changing the values of v. In this paper, actions are deterministic assignments of the form v := expr where v is a state variable. INITIALISATION specifies the initial state of a machine. A machine can be related to an Event-B context (SEES) that specifies sets, constants, axioms and theorems.

The main concept of the Event-B method is the refinement (REFINES) of machines. It consists of a refinement of the events: the guards may be weakened and the behavior must conform to the abstract event. New events refine the special event called "skip". The Rodin tool [START_REF] Abrial | Rodin: an open toolset for modelling and reasoning in Event-B[END_REF] generates proof obligations for the refinements and the preservation of the invariants by the events.

In Event-B, x 1 → x 2 denotes a pair (x 1 , x 2 ). Relations are sets of pairs. dom(r) and ran(r) denote the domain and range of a relation r. E ↔ F denotes the set of relations between E and F , E ↔ ↔ F the set of total surjective relations, and E → F total functions from E to F . The relation r 1 ; r 2 denotes the forward composition of relations r 1 and r 2 . "⊳" is the domain restriction operator such that given a relation r and a set E, E ⊳ r {x → y | x → y ∈ r ∧ x ∈ E}. "⊳ -" is the domain subtraction operator such that given a relation r and a set

E ′ , E ′ ⊳ -r {x → y | x → y ∈ r ∧ x / ∈ E ′ }. "⊳ -"
is the overriding operator such that given relations r 1 and r 2 , r 1 ⊳ -r 2 r 2 ∪ (dom(r 2 ) ⊳ -r 1 ). P(E) denotes the powerset of E.

Event-B Distributed Executions

First, we introduce each feature of asynchronous communication through a series of initial refinements: concept of "events", "happening", and "past", then the pairing of two events (communication), localization of the events (distribution) and causality (distributed executions), linearization of the executions (totally ordered runs), and eventually messages which label the exchanges. This paper skips these preliminary refinements. The resulting machine called RunWithMessages, presented in Figure 2, is a boilerplate for any asynchronous point-to-point communication model. It conforms to the distributed executions and runs of Definitions 1 and 2. By playing with the guards, other communication paradigms can be specified (e.g. synchronous communication, multicast, join).

The machine relies on sets defined in the contexts: EVENT the set of event identifiers labeled by elements of PEER, MESSAGES, and COM (Send or Receive). Events are labeled by variables peerOf, mesOf, and comOf once they are introduced in the machine (e.g. e → Send ∈ comOf ). New communication events are introduced by the actions of the two Event-B events send and receive. They are stored in the past variable and the labeling functions evolve according to the parameters of send and receive: the peer it has occurred on and the exchanged message. Additionally, variables prec (partial causal order ≺ c ) and run (total order < σ ) log the dependencies between the events which serves to specify the communication properties (including ordering policies in future machines).

: ∀ e1, e2 • e1∈ past ∧e2∈ past ∧peerOf(e1) = peerOf(e2) ⇒e1 → e2 ∈ prec ∨e2 → e1 ∈ prec inv5 : prec ⊆ run // run extends prec . inv6 : ∀ e1, e2 • e1 ∈ past ∧ e2 ∈ past ⇒ e1 → e2 ∈ run ∨e2 → e1 ∈ run // run is total . // No message is sent or received more than once. inv7 : ∀ e1,e2 • e1∈ past ∧e2∈ past ∧comOf(e1)=comOf(e2) ∧mesOf(e1)=mesOf(e2) ⇒e1 = e2 inv8 : ∀ e • e ∈ past ∧ comOf(e) = Receive // A receive event is preceded by a send event . ⇒ (∃ es • es ∈ past ∧ comOf(es) = Send ∧mesOf(e) = mesOf(es) ∧es → e ∈ prec)
EVENT send ANY e p m // New event, Peer where the event occurs, Sent message // The new event is causally after all the events that causally precede prec := prec // an event from the same peer (penultimate line ) and after all the events ∪ {e → e} // that causally precede the send event ( last line ).

WHERE grd1: e ∈ EVENT \ past ∧ p ∈ PEER ∧ m ∈ MESSAGE grd3: m ∈ MESSAGE \ ran(mesOf) // m has not already been sent THEN act1 : past := past ∪ {e} act2 : peerOf := peerOf ∪{e → p} act3 : prec := prec ∪ {e → e} ∪ {ep • ep ∈ past ∧ (∃ ep2 • ep2 ∈ past ∧ peerOf(ep2) = p ∧ep → ep2 ∈ prec) | ep → e} act4 : run := run ∪ {e → e} ∪ {ep • ep ∈ past | ep → e} act5 : mesOf := mesOf ∪{e → m} act6 : comOf := comOf ∪{e → Send} EVENT receive ANY e p m // new event; receiver; received message WHERE grd1: e ∈ EVENT \ past ∧ p ∈ PEER ∧ m ∈ MESSAGE grd6: ∀ ep • ep ∈ past ∧ comOf(ep) = Receive ⇒mesOf(ep) = m // m
∪ {ep • ep ∈ past ∧ (∃ ep2 • ep2 ∈ past ∧ peerOf(ep2) = p ∧ep → ep2 ∈ prec) | ep → e} ∪ {ep • ep ∈ past ∧ (∃ es • es ∈ past ∧ comOf(es) = Send ∧mesOf(es) = m ∧ep → es ∈ prec) | ep → e} act6 : comOf := comOf ∪{e → Receive}

Abstract Communication Models

The communication model specifies when a communication action (send or receive) is possible in order to ensure specific properties on the communication. We focus on message ordering properties (e.g. global ordering: all messages are received in their emission order). In this section, each abstract communication model is a machine based on RunWithMessages that is characterized by an ordering invariant on distributed executions or runs. We use this invariant to filter out the distributed executions and runs that do not abide to the ordering policy and keep all those that do.

The communication models constitute steps between fully asynchronous distributed communication (async) where sending and receiving a message is always possible, partially ordered communication (fifo11, causal, fifo1n, fifon1 ), totally ordered communication (fifonn), and almost synchronous communication (RSC ) where a message must be received immediately after it has been sent. We use simulation to define a hierarchy based on the strength of the delivery order. Stronger models have less non-determinism on the receptions. Machine RunWithMessages models asynchronous communication and corresponds to the async model. The other models impose more and more determinism on reception (and, for RSC, on send). The first column of Figure 1 accounts for the hierarchy of these models. Refinement is used to prove the simulation relations between the models. Note that these are not concretization refinements: no model can be called more (or less) concrete or realizable. Concretization of the communication models follow a specific path for each model and is described later.

Informal Specifications

In this paper, we study seven asynchronous point-to-point communication models. A detailed description with figures of each model is given in [START_REF] Chevrou | On the diversity of asynchronous communication[END_REF].

RSC Realizable with Synchronous Communication [START_REF] Charron-Bost | Synchronous, asynchronous, and causally ordered communication[END_REF][START_REF] Kshemkalyani | Distributed Computing: Principles, Algorithms, and Systems[END_REF]. The send event of a message is immediately followed by the receive event of this message (viewed atomically, it corresponds to synchronous communication). fifo n-n Messages are globally ordered and are delivered in their send order. fifo 1-n Messages from the same peer are delivered in their send order. fifo n-1 On a given peer, messages are received in their send order. fifo 1-1 Messages between a couple of peers are delivered in their send order.

Messages from/to different peers are independently delivered. causal Messages are delivered according to the causality of their emission [START_REF] Lamport | Time, clocks and the ordering of events in a distributed system[END_REF].

If a message m 1 is causally sent before a message m 2 (i.e. there exists a causal path from the first emission to the second one), then a peer cannot get m 2 before m 1 . async Fully Asynchronous. No order on message delivery is imposed. The machine RunWithMessages is this model.

Event-B Specifications

We consider the specifications of the communication models with events. Each communication model is characterized by an invariant that describes the ordering properties it ensures on the communication. The invariants of the models all introduce es 1 and es 2 , the send events of two distinct messages, as well as er 1 and er 2 , the corresponding receive events. The model-specific part imposes an order on the receive events (er 1 and er 2 ) based on the causal or run order of the send events (es 1 and es 2 ) and whether or not the sending or receiving peers are the same (same sending peer and same receiving peer for fifo 1-1, same sending peer for fifo 1-n, same receiving peer for fifo n-1 and causal ). For instance, the ordering invariant in the machine CausalEvent is:

// Given two transmissions of messages and the four corresponding events : es1 er1 and es2 er2 ∀ es1 , er1 , es2 , er2

• es1 ∈ past ∧ er1 ∈ past ∧ es2 ∈ past ∧ er2 ∈ past ∧ comOf(es1) = Send ∧comOf(es2) = Send ∧comOf(er1) = Receive ∧comOf(er2) = Receive ∧ mesOf(es1) = mesOf(er1) ∧ mesOf(es2) = mesOf(er2) // Model-specific part : ∧ es1 → es2 ∈ prec // If es1 CAUSALLY precedes es2 ∧ peerOf(er1) = peerOf(er2) //
and the corresponding RECEPTIONS occur on the SAME PEER ⇒ er1 → er2 ∈ run // then they must occur in the emission order .

Our next goal is to compare the communication models, by proving that some have less transitions than others (i.e. are more deterministic). Later in Sections 4 and 5, we derive more concrete specifications of these models. However, at this point, having machines that are as liberal as the ordering allows is important. Thus, the weakest preconditions of the ordering invariants are stipulated for the guards of the send and receive events. As the actions are assignments of the form var := var ∪ {• • • }, the computation of the weakest preconditions is trivial [START_REF] Dijkstra | Predicate Calculus and Program Semantics[END_REF]. As an example, Figure 3 presents the resulting structure of the CausalEvent machine with a close up on the ordering guard of the receive event.

Proofs and Invariants

The difference between the models is an invariant directly related to the order of delivery and the associated weakest precondition used as a guard on the communication events. A proof of refinement consists in proving the logical implications between these invariants. Most of the time these proofs require little manual intervention thanks to auto-provers, post-tactics, and SMT solvers.

The refinements of causal in fifo-n1 and fifo-1n need manual intervention with a specific invariant that states that two causally related events on different peers are necessary linked by (at least) one message. Informally, it means that causality between events on distinct peers only exists due to message exchanges.

∀ e1, e2 • e1 → e2 ∈ prec ∧peerOf(e1) = peerOf(e2) ⇒ (∃ es , er • e1 → es ∈ prec ∧ es → er ∈ prec ∧ er → e2 ∈ prec ∧peerOf(e1) = peerOf(es) ∧ comOf(es) = Send ∧comOf(er) = Receive ∧mesOf(es) = mesOf(er))
4 History-based Models

In this section, we take one step forwards in the direction of concretization. These new specifications share a common framework in which the ordering properties rely upon keeping track of dependent messages in histories. This makes it easier to compare them much like in the previous section. Yet, the specifications are now operational and realistic enough to be implemented and used as such.

There are two directions involved in the mapping of these communication models. First, each history-based model relates to its execution-based counterpart: it is a concretization of the latter, which means the underlying ordering properties still hold, and we use refinement to prove it in Section 4.2. For example, Fifo11History is a concretization of Fifo11Event. Second, it is expected that the history-based communication models, which model the same ordering policies, preserve the hierarchy of these ordering policies. Once again, the simulation relations (i.e. the reduction of the non-determinism of the communication events send and receive) are made explicit and proved by refinement. For instance CausalEvent is stronger than (refines) Fifo11Event and CausalHistory is stronger than (refines) Fifo11History.

: ∀ es1 , er1 , es2 , er2 • es1 ∈ past ∪ {e} ∧ er1 ∈ past ∪ {e} ∧ es2 ∈ past ∪ {e} ∧ er2 ∈ past ∪ {e} ∧ (comOf ∪ {e → Send})(es1) = Send ∧ (comOf ∪ {e → Send})(es2) = Send ∧ (comOf ∪ {e → Send})(er1) = Receive ∧ (comOf ∪ {e → Send})(er2) = Receive ∧ (mesOf ∪ {e → m})(es1) = (mesOf ∪{e → m})(er1) ∧ (mesOf ∪ {e → m})(es2) = (mesOf ∪{e → m})(er2) ∧ (peerOf ∪ {e → p})(er1) = (peerOf ∪ {e → p})(er2) ∧ es1 → es2 ∈ run ∪ {e → e} ∪ {ep • ep ∈ past | ep → e} ⇒ er1 → er2 ∈ run ∪ {e → e} ∪ {ep • ep ∈ past | ep → e} THEN //

Specifications with Histories

We consider specifications of the asynchronous point-to-point interaction models where communication occurs according to two parameterized events: send(p, m, d) (peer p sends message m to an explicit peer d) and receive(p, m) (peer p receives message m).

The models rely on a state variable net that contains messages in transit. Sent messages are labeled to carry information about the communication: the origin peer, the destination peer, and the history of the message. The history of a message is the set of messages on which it depends, i.e. the set of messages which precede it. As two notions of precedence exist (causal/execution), two kinds of message histories are defined: namely causal and global. Definition 3. (Message Histories) For a run σ = (E, ≺ c , < σ , com, mes, peer), and a message m:

hcOf (m)        m ′ ∈ M ESSAGE : ∃e, e ′ ∈ E : com(e) = Send ∧ com(e ′ ) = Send ∧ mes(e) = m ∧ mes(e ′ ) = m ′ ∧ e ′ ≺ c e        hgOf (m)        m ′ ∈ M ESSAGE : ∃e, e ′ ∈ E : com(e) = Send ∧ com(e ′ ) = Send ∧ mes(e) = m ∧ mes(e ′ ) = m ′ ∧ e ′ < σ e       
In the Event-B models, the message histories are built upon state variables hg ⊆ MESSAGE, the global history, and hc ∈ PEER → P(MESSAGE), the causal histories of each peer. When peer p sends a message m, the global history (hgOf) and the causal history (hcOf) of m are the current values of hg and of hc(p). The new message is also added to the history state variables (hg and hc(p)). The causal history hc(p) of peer p is updated when a message m is received to account for the causal relation induced by the transmission of the message from one peer to another: m and its causal history hcOf(m) are added to hc(p). The validity of these constructions with regard to the above definitions is stated as two invariants. The ordering properties of a model are determined by guards on the send and receive events that depend on the message histories, origin, and destination of a message.

Concretization

For each communication model, the refinement of the event-based model by the history-based model is split in two steps to facilitate the proofs. First, add new variables to hold histories and message destination (net, hg, hc, hgOf, hcOf, destOf), and replace the guards about events by guards about histories. Then, remove the now useless variables related to events (past, prec, run, . . . ).

As an example, Figure 4 is the resulting machine for the causal model. Its ordering invariant states that if m 1 and m 2 have the same destination, and m 1 was sent causally before m 2 (thus m 1 is in the causal history of m 2 ), then m 1 cannot be in transit when m 2 is not. This means that m 1 must be received before m 2 . Accordingly, the ordering guard for receive allows to deliver a message m if there does not exist another message m 2 in transit, with same destination, and which is in the history of m.

Data refinement consist in proving that the model-specific guards on the communication events guarantee the ordering properties on the distributed executions. The proofs rely on the ordering invariant, and wisely formulated gluing and consistency invariants. The gluing invariants relate the state variables of the abstract (events, executions) and concrete machines (network, histories). For instance, a message m 1 is in the causal history of m 2 if the send event of m 1 is causally anterior to the send event of message m 2 . The consistency invariants clarify links between the state variable of the concrete machine (e.g. if a message m 1 is in the causal history of m 2 , it is also in its global history). Besides, significant manual interventions have to be carried out to supervise the proof process as the number of state variables and invariants misdirect the automatic provers. Finding the optimal formulation (e.g. proposition vs. contraposition), through trial and error, is a large portion of the proof effort.

:= origOf ∪ {m → p} a6: destOf := destOf ∪ {m → d} a7: hgOf := hgOf ∪ {m → hg} a8: hcOf := hcOf ∪ {m → hc(p)} EVENT receive REFINES receive ANY p m WHERE intransit : m ∈ net destination : p ∈ PEER ∧ destOf(m) = p ordering : ¬ (∃ m2 • m2 ∈ net ∧ destOf(m2) = p ∧ m2 ∈ hcOf(m)) THEN a1: net := net \ {m} a2: hc(p) := hc(p) ∪ hcOf(m) ∪ {m}

Concrete Models

In the first approach, the models based on events directly translate the ordering policies of the communication models. The second approach using message histories is more concrete: the locality and transmission of data is taken into account with messages that carry their history. However, keeping trace of all the previously sent messages is still unrealistic in practice. Therefore we refine the models that use histories with concrete structures such as counters of messages or queues of messages.

Logical Clocks

Regarding the causal communication model as described in Figure 5, the causality relation can be explicit, using pruned causal histories [START_REF] Kshemkalyani | Distributed Computing: Principles, Algorithms, and Systems[END_REF] this is as costly as our version with histories), or derived from logical vector clocks of size n or matrix clocks of size n × n [START_REF] Raynal | Distributed Algorithms for Message-Passing Systems[END_REF].

:= vcOf(p) ⊳ -{p → vcOf(p)(p) + 1} act6 : rankOf(m) := vcOf(p) ⊳ -{p → vcOf(p)(p) + 1} EVENT receive REFINES receive ANY p m WHERE Tm: m ∈ net Tp: p ∈ PEER dest : destOf(m) = p order : ¬(∃m2 • m2 ∈ net \ {m} ∧ destOf(m2) = p ∧ (∀ pp • pp ∈ PEER ⇒ rankOf(m2)(pp) ≤ rankOf(m)(pp))) THEN act2 : vcOf(p) := { pp •pp ∈ PEER | pp → max({ vcOf(p)(pp), rankOf(m)(pp) })} act3 : rankOf := {m} ⊳ -rankOf INVARIANTS TrankOf: rankOf ∈ net →(PEER →N) TvcOf: vcOf ∈ PEER →(PEER →N) inv1 : ∀ m1, m2 • m1 ∈ net ∧m2 ∈ net ∧m1 = m2 ⇒ (m1 ∈ hcOf(m2) ⇒(∀ p • p ∈ PEER ⇒rankOf(m1)(p) ≤ rankOf(m2)(p))) inv2 : ∀ m1, m2 • m1 ∈ net ∧m2 ∈ net ∧m1 ∈ hcOf(m2) ⇒ rankOf(m1)(origOf(m2)) < rankOf(m2)(origOf(m2)) inv3 : ∀ m, p • m ∈ net ∧p ∈ PEER ∧m ∈ hc(p) ⇒ (∀ pp • pp ∈ PEER ⇒rankOf(m)(pp) ≤ vcOf(p)(pp))
Every peer p has a vector clock vcOf (p). For peers p and pp, vcOf (p)(pp) holds the number of send events on pp that are in the current past of peer p. When a peer sends a message, it increments its own count (vcOf (p)(p)) and piggybacks its vector with the message. At reception, a peer updates every component of its vector with the max of its current value and of the component of the received vector. Thus, vcOf (p)(pp) holds the number of messages sent by pp and known by p. A message m is in the causal history of m ′ iff every vector component of m is lower or equal than the one of m ′ (and at least one is strictly lower: distinct messages have different vectors). To ensure causal reception, a message can be delivered to a peer iff no other message exists for this peer with a lower vector.

The refinement of CausalHistory replaces the history variables with vector clocks. The events are refined to update these variables and, in the receive event, the guard built on histories is replaced with a property on the vectors. The refinement proof requires gluing invariants on causal histories and vector clocks.

Other Concretizations

As shown in Figure 1, other concrete models have been defined. The various fifo* models are easily described with counters. If n denotes the number of peers, 2 counters (fifonn), 2 × n counters (fifon1 and fifo1n), or 2 × n 2 counters (fifo11 ) are used to account for the ordinal rank of the last sent and last received messages in the system (fifonn), a peer (fifon1 and fifo1n), or a couple of peers (fifo11 ). The ranks of the last received messages determine the rank of the messages that can be received. Alternatively, message queues can be used: if n denotes the number of peers, we need a global queue (fifonn), n inbox queues (fifon1 ), n outbox queues (fifo1n), or n 2 queues (fifo11 ).

6 Additional Remarks

Proof Effort

The full menagerie holds 42 machines, 41 refinements, 329 invariants, and more than 1400 proof obligations. Once the necessary invariants are stated, the large majority of these proof obligations are automatically proved by Rodin with SMT solvers (49 manual proofs, 3.5% of the proof obligations). The main difficulties are described below.

To make the proofs automatic, the trick is to find additional invariants. For instance, to prove that RscHistory refines RscEvent, the invariant

∀ e1, e2 • e1 → e2 ∈ run ∧ comOf(e1) = Send ∧ e1 = e2 ⇒ mesOf(e1) / ∈ net
has to be made explicit (it says that if there exists at least one event after a send event e 1 , then the message sent at e 1 is no longer in transit). As expected, the discovery of the necessary invariants is the hardest part in the proofs, and the largest part of our proof effort was devoted to this point. Our methodology consists in running the automatic provers and analyzing the failure (if any).

After some case analysis of the disjunctions, a contradiction often appears in the hypotheses. This contradiction leads us to a relevant new invariant. Once stated and proved, this new invariant may, with good luck, suppress the unsuccessful branch and advance towards the fully automatic proof.

The refinements involving causal are never easy. One essential invariant is:

∀ e1, e2 • e1 → e2 ∈ prec ∧ peerOf(e1) = peerOf(e2) ⇒ (∃ es , er • e1 → es ∈ prec ∧ es → er ∈ prec ∧ er → e2 ∈ prec ∧peerOf(e1) = peerOf(es) ∧ comOf(es) = Send ∧ comOf(er) = Receive ∧ mesOf(es) = mesOf(er))
It states that two causally related events on different peers are necessarily linked by (at least) one message, or conversely, that causality between peers only arises from message exchanges. This invariant had to be manually instantiated. Lastly, concrete models need ad-hoc reasoning. For instance, Section 5.1 presents the specific invariants that are required to prove that CausalVector refines CausalHistory. These invariants are expected as they state that vector clocks encode causality. Nevertheless, the refinement proofs require to manually recall and instantiate these invariants.

Localization

The last point concerns the distributed nature of the communication models. The first abstract models, based on properties of the executions, are purely logical and offer a global point of view of the communication models. The second models, based on histories, are actually directly implementable even if costly. The third concrete models offer realistic implementations. By looking at their definitions, one can distinguish two classes of communication models. The models async, fifo11, causal and fifo1n only need meta information piggybacked with the message and local knowledge available on the peer. On the other hand, fifon1, fifonn and rsc require global shared variables, and their implementation in a distributed system requires a central coordinator or totally ordered multicast.

Related Work

Asynchronous communication models in distributed systems are studied and compared in [START_REF] Kshemkalyani | Distributed Computing: Principles, Algorithms, and Systems[END_REF] (notion of ordering paradigm), [START_REF] Charron-Bost | Synchronous, asynchronous, and causally ordered communication[END_REF] (notion of distributed computation classes), and [START_REF] Engels | A hierarchy of communication models for message sequence charts[END_REF] (for message sequence charts). Implementations of the basic communication models (causal, fifo11 ) using histories or clocks are explained in classic textbooks [START_REF] Kshemkalyani | Distributed Computing: Principles, Algorithms, and Systems[END_REF][START_REF] Raynal | Distributed Algorithms for Message-Passing Systems[END_REF]. In our previous work, we have unified and extended these results in [START_REF] Chevrou | On the diversity of asynchronous communication[END_REF]. The goal was to develop a framework to mechanically verify algorithms [START_REF] Chevrou | Automated verification of asynchronous communicating systems with TLA +[END_REF], and to give a unified description of the models. However only the communication models with message histories were specified in TLA + . All the Event-B models presented here are new, as well as the refinement relations leading to the distributed executions (Section 2), between the abstract communication models (Section 3), and between the concretizations (abstract model to history-based model to ad-hoc model, sections 4.2 and 5).

Formal verification of distributed algorithms have been conducted with success. However the hypotheses on the communication are often fuzzy or unclear and one has to dive deep into the proofs to identify them. For instance, [START_REF] Li | Active and concurrent topology maintenance[END_REF] studies the topology maintenance in structured peer-to-peer networks. Different algorithms are studied, some assume FIFO channels and some do not. It is unclear why it is required, and if it is required for all channels.

Refinement has been used to verify distributed algorithms. [START_REF] Lamport | Byzantizing Paxos by refinement[END_REF] describes the addition of Byzantine resilience to standard Paxos. The proof is conducted by refinement of the distributed non-Byzantine algorithm and has been mechanically checked with the TLA + Proof System. Another approach is presented in [START_REF] Lampson | The ABCD's of Paxos[END_REF]. Three versions of Paxos (the classic one, disk Paxos and Byzantine Paxos) are derived from an abstract, non-distributed algorithm.

The Event-B book [START_REF] Abrial | Modeling in Event-B -System and Software Engineering[END_REF] presents several examples of refinements of distributed algorithms. The simple file transfer protocol decomposes the atomic sending of a file in a sequence of send events, and uses counters to coordinate the progression. This protocol is later extended to handle loss and re-transmission with an alternating bit protocol. In this example, asynchronous communication appears implicitly during refinement, and properties of the communication are directly embedded in the resulting machine. A logical clock is used in the routing algorithm for a mobile agent to order the messages sent by a mobile agent while it moves. This example can be seen as the development of an ordered communication model down to a concrete localizable model. Lastly, the leader election on a connected graph network deals with the difficulties of splitting an atomic action (in a shared-memory model) into several actions (in a message-passing model). This creates deadlocked states (a situation called contention in the algorithm) where two nodes are each waiting for the other to progress. This development is more concerned with providing a algorithmic solution in presence of non-atomic actions, than with the development of non-atomicity (i.e. messages).

[4] presents the development by refinement of snapshot algorithms. It starts with the specification of the snapshot problem, which is by essence a global property. A generic architecture with asynchronous communication is presented, which allows the derivation of several algorithms. At one point, the set of messages (which models fully asynchronous communication) is refined by FIFO queues (which models ordered communication). This leads to a simpler snapshot algorithm, which ends being the well-known Chandy-Lamport algorithm.

[15] describes the formal derivation of an algorithm for leader election in Event-B. The abstract model is centralized, and refinement introduces distribution. The behavioral part of the communication model first comprises two events, send and receive which directly access the state variable of the other peers. Then, a new refinement introduces new variables to decouple the peers and to get a "one-to-one asynchronous communication channel".

Conclusion

This paper provides a guide for the design of the communication component in the development of distributed systems and algorithms. It considers a wide range of asynchronous communication models that enforce message-ordering properties on the system and positions each one of them on a map of refinement relations. The map, shown in Figure 1, has two dimensions: it compares the models according to the strength of the underlying ordering properties and their level of abstraction. All these models are specified and the refinements proved in Event-B which paves the way for reusing part of the mechanization in a correct-byconstruction development of a distributed system thanks to shared-event model decomposition. Our machines are indeed pluggable to any system where communication occurs according to two events send and receive with usual parameters (message, destination). A classic development process consists in introducing asynchronous communication which corresponds to our RunWithMessages machine, the root of our map, and make use of the rest of the map to strengthen the ordering policy depending on the needs, pursue the development towards the concrete practical specifications models (with counters or queues), or even substitute models afterwards knowing the safety properties are preserved. Besides, each one of the three sets of communication models we provide has its assets: the concrete models are close to practical implementations, the event-based models clearly translate the ordering policies which ease theoretical reasoning on the properties themselves, and the history-based models offer a compromise with operational descriptions that are implementable and yet remain uniform to ease formal reasoning.

Fig. 1 .

 1 Fig. 1. Map of the Asynchronous Communication Models. A black arrow means "refines". The two axis of refinement are the level of abstraction (data refinement) and the strength of the ordering policy (reduction of non-determinism).

  has not already been received grd7: ∃ es • es ∈ past ∧ comOf(es) = Send ∧mesOf(es) = m // m has been sent THEN // Same as send except act4 :

Fig. 2 .

 2 Fig. 2. Event-B Machine for Asynchronous Point-to-Point Communication

Fig. 3 .

 3 Fig. 3. Structure of the Causal Communication Model Described With Events. The machine corresponds to E_RunWithMessages with an additional ordering invariant and the associated guards.

Fig. 4 .

 4 Fig. 4. History-Based Event-B Model for Causal Communication

Fig. 5 .

 5 Fig. 5. Concrete Model for Causal Communication Using Vector Clocks

  (in the worst case,

	MACHINE H3_CausalVector
	REFINES G3_CausalHistory
	SEES E_Messages
	VARIABLES net hg origOf destOf
	rankOf // message →vector clock
	vcOf // peer →vector clock
	EVENT send REFINES send
	ANY p m d WHERE
	Tm: m ∈ MESSAGE \hg
	Tpd: p ∈ PEER ∧d ∈ PEER
	THEN
	...
	act5 : vcOf(p)