S H Och

L M Moura

J A Velásquez

C Lacour

B Lecordier

E Domingues

Experimental and Numerical Study of Admission and Exhaust Flows in a Spark Ignition Engine

The yield of the process of gas exchange in four stroke internal combustion engines is given by volumetric efficiency, which depends on the dynamics of gases in the exhaust and intake manifolds. These gases are considered as compressible and ideal and the laws of conservation of mass, momentum and energy, 1D-transient, are applied. The numerical results are compared with time resolved measurements performed on a spark ignition single-cylinder engine. For the comparison, pressure in the combustion chamber, pressure of the gas at different locations along the pipelines and wall temperature of intake and exhaust ducts are considered. In order to validate the simulation in a large range of conditions, different engine speeds and lengths of intake and exhaust ducts have been investigated.

Introduction

The increase of price of fuels, derived from petroleum and the introduction of increasingly restrictive environmental norms, have motivated researchers to develop engines, which are more efficient and less harmful to the environment. The efficiency of internal combustion engines depends greatly on the use of inertial and pulsating phenomena, which occur in the intake and exhaust ducts. The optimization of the working conditions of internal combustion engines necessarily requires a deep analysis of the different variables involved in this process. Thus, for example, the intake and exhaust systems can be sized and have their geometrical configurations defined, according to the characteristics that one desires to privilege: fuel consumption, maximum power, torque and volumetric efficiency at low speed. The acoustic design of the intake system is a predominant topic in the study of internal naturally aspirated spark ignition engine [START_REF] Heywood | Internal Combustion Engine Fundamentals[END_REF]. The design of the inlet line requires many tests. However, the industry needs to get the project done quickly and at the lowest feasible cost of production. While testing of engines is widely used for this purpose, these tests are expensive and require the engine prototype in advanced phase of development [START_REF] Torregrosa | Combined experimental and modeling methodology for intake line evaluation in turbocharged diesel engines[END_REF]. The preliminary design of the inlet line is to minimize the pressure loss. However, one can increase the volumetric efficiency taking advantage of the pressure waves, which are generated by the process of gas exchange in the combustion chamber. In recent research tendency is to improve the utilization of the energy contained in fuels.

The study of internal combustion engines requires that the computational models adequately represent the processes of the engine. Therefore, the computational model must be verified using experimental data that can be obtained from a simplified physical model or from an  Corresponding author: stephan.och@pucpr.br Proceedings of the European Combustion Meeting 2013 engine functioning in its full complexity. When using a simplified physical model, it is necessary that the phenomena under analysis are adequately reproduced in it.

Specific Objectives

The idea is to create a computational code allowing prediction of the amount of mass that enters through the admission valves. So we can use this code for mathematical optimization of intake process.

The mass flow passing through the valve is governed by inertial and pulsating phenomena, found in the ducts of internal combustion engines. These phenomena are a function of the geometry and operating conditions of the engine. The aim of this paper is to compare experimental pressure data, obtained in a single cylinder engine with the data obtained through an unsteady 1D code. The comparison is done for different engine speeds (800 to 3000 rpm) and intake and exhaust ducts lengths (150 to 1000 mm).

The first part describes the mathematical model of the processes in the combustion chamber and the equations governing the flow in the intake and exhaust ducts. In the second part are illustrated the assembly and equipment used to obtain the experimental data. The results are given in form of graphs comparing the two responses. Finally, the conclusion section is commented and some interesting points of study and some perspectives for the following of this work are given.

Mathematical Models

A good understanding of admission processes is crucial to improve the characteristics of an engine. Actually, computer programs based in 3D-CFD (Computational Fluid Dynamics) techniques can reproduce detailed information of fluid flow. But simulation of an entire cycle of fluid flow in cylinders and manifolds, and the geometric complexity of the movement of the piston and valves make this type of simulation having a high computational cost. Normally optimization techniques of volumetric efficiency require many calculation of the objective function. Therefore simulations using 3D engine for this problem would make the analyze time too long [START_REF] De C Monteiro | Modelos Matemáticos e Computacionais para Simulação do Escoamentos em Motores de Combustão Interna[END_REF].

Models of one-dimensional gas flow are important tools in the automotive world, both in design and in optimization. These models have been widely used to reproduce the behavior of the engine in anticipation of noise emission, because they show a balance between accuracy and computation time.

The flow of gas is considered compressible, treated as one-dimensional, non-stationary, non-isentropic and the cross sectional area of the ducts may vary depending on the coordinate space [START_REF] Pearson | The Simulation dynamics in engine manifolds using non-linear symmetric difference schemes[END_REF]. It is necessary to consider the friction and heat transfer between the flow and the walls of the tube [START_REF] Payri | Analysis of numerical methods to solve onedimensional fluid-dynamic governing equations under impulsive flow in tapered ducts[END_REF]. The variation of specific heat ratio of the fluid, k, can be neglected. Applying the equations of conservation of mass, momentum and energy, leads to the following systems of equations:

Where:

{ } { ( ) } { ( ) ̇}
Where ρ is density, w is velocity, A is cross-section area, P is pressure, k is the ratio of specific heat, F f is friction force and ̇ is heat transfer per mass. One can prove that these equations form a system of hyperbolic equations and thus have three real eigenvalues, w, w+c and w-c, were c is the speed of sound. When we solve convective dominant problems, as hyperbolic conservation laws, the kind of scheme applied to the convective term becomes quite sensitive to stability and accuracy [START_REF] Kadalbajoo | A high resolution total variation diminishing scheme for hiberbolic conservation law and related problems[END_REF]. A second-order method widely used in solving the governing equations is the Lax-Wendroff two-step scheme or Richtmyer scheme. The intermediate step is done by Lax-Friedrich method. This method is first order of accuracy and explicit. The second-order is retrieved using the leap-frog method, remaining equal to:

( ) ( )
Another second order method also applied to solve the equations of the gas flow in the ducts is the MacCormarck scheme:

[( ̅ ) ( ̅ ̅ ) ̅ ]
Where the predictor step is:

̅ ( )
The time step should be chosen to ensure the stability of explicit method, therefore it must satisfy the Courant-Friedrich-Lewis condition:

(| | )
Numerical schemes of high order accuracy for hyperbolic conservation laws must overcome three difficulties: to ensure conservation of the properties, to preserve the high order accuracy in time and space and to control the generation of spurious oscillations in discontinuities [START_REF] Daru | High order one-step monotonicity-preserving schemes for unsteady compressible flow calculations[END_REF]. The literature shows the central differential schemes of second order or higher, with constant coefficients exhibiting spurious oscillations near discontinuities such as shock waves and contact surfaces [START_REF] Payri | Application of MacCormack Schemes to I.C. Engine Exhaust Noise Prediction[END_REF]. Shock waves can be found in exhaust ducts and contact surfaces can be generated by the contact of hot and cold gases [START_REF] Pearson | The Simulation dynamics in engine manifolds using non-linear symmetric difference schemes[END_REF]. One of several techniques used to capture the shock is Davis TVD scheme. This method consists in adding a diffusive term in the methods of second order, in order to damp the oscillations that appear in the presence of discontinuities.

[ ̅ ( ) ̅ ( )] ⁄ [ ̅ ( ) ̅ ( )] ⁄
Where G is called artificial viscosity and is calculated as

̅ ( ) ( )[ ( )] ( ) { ( )
and

[ ⁄ ⁄ ] [ ⁄ ⁄ ]
In the last equation the bracketed terms [ . , . ] denote the inner product. The limiter may be calculated by the following equation:

( ) { ( )
For this scheme to be stable, the time step should be reduced by 70% of Courant number.

The boundary conditions, including valves, open closed end, were found using the methods of the characteristics by the procedure presented by El-Rahman et al. [START_REF] Abd El-Rahman | Non-linear simulation of single pass perforated tube silencers based on the method of characteristics[END_REF].

The thermal process of the gas inside the combustion chamber is modeled by zero-dimensional model. This work shows the study in a single cylinder engine without combustion and without fuel injection. Applying the mass and energy balances equations and the ideal gas equation, we arrive at the following system of differential equations:

[ ( ) ( ) ]
[ ] where P, V, T, m, u, h, θ and Q are the pressure, volume, temperature, mass, internal energy, enthalpy, crankshaft angle and heat transfer, respectively. The indices ad and ex represent the enthalpy or mass flow crossing the boundary of the system through the admission and exhaust valves, respectively. The rate of heat transfer is obtained by Woschni correlation [START_REF] Woschni | A universally applicable equation for the instataneous heat transfer coefficient in the internal combustion engine[END_REF], this correlation is the most used today [START_REF] Ma | Effects of Combustion Phasing, Combustion Duration, and Their Cyclic Variations on Spark-Ignition (SI) Engine Efficiency[END_REF]. Through geometric relationships of the engine, we can calculate the volume and its derivative as a function of crankshaft angle.

The equation system above is solved by the fourthorder Runge-Kutta method. The mass flow through the valve is described by the one-dimensional, stationary, compressible, isentropic flow equation and the effects of turbulence are included in real flow through the discharge coefficient Cd, obtained experimentally [START_REF] Shapiro | The Dynamics and Thermodynamics of Compressible Fluid Flow[END_REF]. The step of crankshaft angle is obtained from the time step of gas flow solution in the intake and exhaust ducts.

Experimental Apparatus

The objective of experimental apparatus is to test the reliability of the model presented above. It is proposed to perform the measurement of gas pressure at certain points of an I.C. engine. We used the engine bench of laboratory CORIA. The engine used for this experiment was an AVL single cylinder engine, sparkignition and direct injection. Some characteristics of the combustion engine can be seen in table 1 Attached to the same shaft of the I.C. engine is an electric machine which can operate both as electric motor and brake. In this experience there was no fuel injection, so the electrical machine run the engine at a specified rotation speed. This study without combustion is a preliminary step that allows observing the pressure waves in the exhaust and intake manifolds. It also allows checking the accuracy of the computational code without some complexities that appear with combustion. As this engine does not have a long overlap region valve, it is expected to obtain results in the intake manifold not sensitive to the fact that engine is operating with or without combustion.

The engine is instrumented with an angular position sensor (encoder) AVL with precision of 0.1 degree. The measurement of the rotation speed is also done through this encoder.

The measurement of the pressure in the combustion chamber is performed using a piezoelectric pressure transducer AVL GU22C with linearity error of 56 mbar. The piezoelectric transducer captures only the rate of change of pressure over time, so its signal is integrated. In this integration process will lack a reference, which is estimated in the present work by using the thermodynamics relationships of adiabatic compression. This relationship is applied to the compression phase between two points specified and the ratio value of specific heats is also provided by AVL.

For measuring pressure inside the duct, the sensor has to be able to capture the dynamic pressure wave. This transducer should have a relatively high sensitivity in order to capture the small pressure fluctuations. So for this study was chosen a piezoresistive transducer Kistler model 4007B with the amplifier Kistler model 4618 with an adapter that allows the cooling of the transducer through a water circuit.

Test

Length of intake duct (mm)

Length of exhaust duct (mm) 1 150 400 2 550 3 1000 Table 3 -Ducts lengths configurations.

This transducer is connected also to 14-bit analogdigital convertor and its incertitude is equal to approximately 5 mbar.

In table 3 is shown the configurations of the tests. In the models, it is necessary to know the temperature profile of the wall along the pipeline. To resolve this, it was installed thermocouples in ten positions along intake and exhaust ducts. The intermediate values of temperature were obtained by linear interpolation.

Results and Discussion

In this section, a comparison of the measurements with the simulations will be presented for different ducts lengths and rotation speeds. The acronyms in all the graphs below are: LW2S for Lax-Wendroff two steps, LW2S-FL for Lax-Wendroff two steps with flux limiter and MacCor for MacCormarck method. In addition, in an engine cycle, the range of pressure variations between the process gas exchanges and closed-cycle process being very wide, to facilitate visualization and comparison of the results, on each graph, zooms in intake, exhaust and peak pressure regions has been plotted. In order to make simulation comparison possible, the same mesh size in the intake and exhaust ducts and the CFL number was considered as 0.7. For the experimental results, only the averaging of one hundred consecutive cycles are reported.

In figures 1 to 3 are faced by experimental and numerical data gas pressure inside the cylinder. In these figures, the lengths of ducts are kept the same and the rotation speed is varied in 1000, 2000 and 3000 rpm. We can visualize the maximum pressure increase with engine speed where it can be explained by the increase of mass admitted. We can also see a good agreement between the results numerical/experimental, mainly in the capture phase and frequency. We observed a small deviation in the end of compression for the LW2S-FL. This occurs in cases where this method did follow the experimental curve as seen in figure 3.

In figure 3, 4 and 5 are shown curves of cylinder pressure at constant speed (3000 rpm) and changing the length of the intake duct (150, 550 and 1000 mm). We can visualize increased the high pressure at the end of compression with increasing length of the duct. The same trend can be seen through the simulation model. This is because more mass is entering the cylinder during the intake process, as can be seen by the pressure level at the end of the admission process. We shape of the curves on admission and exhaust processes. We can also visualize the well model follows the change in Figures 678show the results of intake manifold pressure at 90 mm of inlet valves. The results were obtained with a fixed length of 550 mm and rotation speed at 1000, 2000 and 3000 rpm. We can remark the variation of pressure wave amplitude which changes with the speed. We have a good agreement when the intake valve is opened. In the case of the inlet valve is close, the correlation occurs only in lower pressure the length of the intake runner. In this case we can see that the model follow the experimental results. We have an optimal concordance during admission phase. Unfortunately there is an underestimation of magnitude pressure for the region of intake valve closed. This may have happened due to some divergence of parameters of heat transfer and/or viscosity friction in the duct.

Conclusions

The main objective of this study was to compare results obtained by a motored engine with a 1-D gas flow model. The 1-D model was solved by numerical methods for second-order well known in the literature of I.C. engines. The results of pressure in the combustion chamber and the ducts correspond well to physics found in conventional engines. In general the results of the numerical 1-D model were able to reproduce the pressure waves in ducts. In some regions there was an underestimation of the pressure, but the results of frequency and phase is positive. Note also that the 1-D model was able to capture well the pressure fluctuation even by changing the rotational speed and length of the intake duct.

For this article, some parameters were estimated using data from the literature for other I.C engines. For the sequence of work, these parameters will be studied in more detail and it is estimated that will be an improvement of the results presented here. This is a preliminary study without combustion, since the goal was to reduce the number of parameters required to know before. But we intend to extend this study to cases occurring combustion and thus closer to the real case.

With a numerical model experimentally validated, it is possible to analyze the influence of parameters related to the geometric configuration of the admission and exhaust systems (transversal section area, the variation of this area along the duct, length of the ducts, etc.) on parameters such as the volumetric efficiency and the fraction of residual gases. This model will also allow an optimization of the valves synchronism and the geometry of the admission and exhaust systems.

Figure 1 -

 1 Figure 1 -Pressure cylinder results for motored engine at 1000 rpm and 550 mm admission length duct.

Figure 2 -

 2 Figure 2 -Pressure cylinder results for motored engine at 2000 rpm and 550 mm admission length duct.

Figure 3 -

 3 Figure 3 -Pressure cylinder results for motored engine at 3000 rpm and 550 mm admission length duct.

Figure 4 -

 4 Figure 4 -Pressure cylinder results for motored engine at 3000 rpm and 150 mm admission length duct.

Figure 5 -

 5 Figure 5 -Pressure cylinder results for motored engine at 3000 rpm and 1000 mm admission length duct.

Figure 6 -Figure 7 -

 67 Figure 6 -Pressure duct (position 90 mm from valves) result for motored engine at 1000 rpm and 550 mm admission length duct.

Figure 8 -

 8 Figure 8 -Pressure duct (position 90 mm from valves) result for motored engine at 3000 rpm and 550 mm admission length duct.

Figure 9 -

 9 Figure 9 -Pressure duct (position 90 mm from valves) result for motored engine at 3000 rpm and 150 mm admission length duct.

Figure 10 -

 10 Figure 10 -Pressure duct (position 90 mm from valves) result for motored engine at 3000 rpm and 1000 mm admission length duct.

Table 2 -

 2 . An input important to the computer code is the valve opening curve. This diagram is obtained through experimental measurements of valve travel using a dial indicator. Results of measures of valves timing.

	AVL 5482 Engine
	Stroke	86 mm
	Bore	82 mm
	Rod	144 mm
	Compression Ratio	8,5
	Table 1 -Data combustion engine used in the
	experiments.
	The crank angle was obtained directly through a
	marking of degrees at the flywheel. The measurement of
	displacement valves was made at constant intervals of 5
	degrees of crankshaft except when closing the valves.
	This average was inserted into the computer code and
	intermediate values of measuring points were
	determined by linear interpolation. Table 2 shows the
	values of valves open and close obtained
	experimentally.
	Admission valve open (avo)	1º After TDC
	Admission valve close (avc)	68º After BDC
	Exhaust valve open (evo)	79º Before BDC
	Exhaust valve close (evc)	16º After TDC

Acknowledgements

The authors would like to thank CAPES (Brazil) for PhD sandwich scholarship (process number 9115/12-9).


Aurélie Hurault
email: hurault@enseeiht.fr

Philippe Quéinnec
email: queinnec@enseeiht.fr

Proving a Non-blocking Algorithm for Process Renaming with TLA +

Keywords: Formal verification, Non-blocking algorithm, TLA +

Shared-memory concurrent algorithms are well-known for being difficult to write, ill-adapted to test, and complex to prove. Waitfree concurrent objects are a subclass where a process is never prevented from progressing, whatever the other processes are doing (or not doing). Algorithms in this subclass are often non intuitive and among the most complex to prove. This paper presents the analysis and the proof of a wait-free concurrent algorithm that is used to rename processes. By its adaptive and non-blocking nature, the renaming algorithm resists to test, because of the cost of covering all its states and transitions even with a small input set. Thus, a proof has been conducted in TLA + and verified with TLAPS, the TLA + Proof System. This algorithm is itself based on the assembly of wait-free concurrent objects, the splitters, that separate processes. With just two shared variables and three assignments, a splitter seems a simple object but it is not linearizable. To avoid explicitly in-lining it and dealing with its internal state, the proof of the renaming algorithm relies on replacing the splitter with a sequential specification that is proved correct with TLAPS and verified complete by modelchecking on finite instances.

Introduction

Increase of computer performance is now obtained by multi-core multiprocessor units. Concurrent programming with locks or monitors is an old topic, and methodologies have been presented that allow developing software with few (or at least not too many) synchronization bugs. All these methodologies revolve around a blocking paradigm: identifying the condition for valid progress (e.g. exclusive access on a resource), and blocking while this condition is not true (e.g. waiting to acquire a lock). However, these approaches are inefficient under high load and are subject to deadlock when a process stops while holding a lock or an access. Non-blocking algorithms have been considered to alleviate these difficulties [START_REF] Michael | Nonblocking algorithms and preemption-safe locking on multiprogrammed shared memory multiprocessors[END_REF]. In a non-blocking algorithm, the delay or failure of a process does not prevent the progress of other processes. Subclasses of nonblocking include lock-free, where system progress is guaranteed, and wait-free, where process progress is guaranteed [START_REF] Herlihy | Wait-free synchronization[END_REF]. Thus, wait-free algorithms are the most interesting to ensure individual progress in an adversary environment. Whatever the progress of the other processes, a process will be able to progress as long as the scheduler ensures that it has access to some CPU resources. Thus, wait-free algorithms are of great importance in highly concurrent environments.

Unfortunately, wait-free algorithms are hard to design and prone to bugs. They rely on low-level instructions, such as test-and-set, compare-and-swap, or shared data structures. Among these, atomic registers [START_REF] Lamport | On interprocess communication[END_REF][START_REF] Kshemkalyani | Distributed Computing: Principles, Algorithms, and Systems[END_REF] provide strong guarantees in presence of concurrency. An atomic register is a linearizable object with two operations, read and write. Progress is guaranteed even in presence of process failure. In a system where the only shared objects between processes are atomic registers, any concurrent execution (with true parallelism) is equivalent to a sequential execution on a single processor with interleaving. This nice property is instrumental in checking and verifying a wait-free algorithm as it spares us to consider true parallelism.

Nevertheless, writing a wait-free algorithm is error-prone. Correctness is often on paper only, and cannot be certified. Lastly, testing these wait-free algorithms is difficult as they generally exhibit a large reachable state space, and execution interleaving leads to a huge number of executions to consider. Bugs are often hidden in the deepest part of the algorithm and few schedulings can trigger them. Wait-free algorithms and data structures have started being used in standard libraries (for instance the ConcurrentLinkedQueue class in Java) but their first implementations were not always exempt of bugs [JDK08].

In this paper, we present the study of Moir and Anderson renaming algorithm [START_REF] Moir | Wait-free algorithms for fast, long-lived renaming[END_REF]. The goal of this algorithm is to assign names (or identifiers) to processes such that the size of the namespace is small. This algorithm is wait-free, and is itself built upon wait-free objects, the splitters. This study has been conducted with the TLA + tools [START_REF] Lamport | The temporal logic of actions[END_REF] to provide a certified proof of the correctness of the renaming algorithm.

The contributions of this paper are:

-A mechanized proof of a wait-free renaming algorithm, based upon wait-free objects; -An approach to handle the internal wait-free objects as black boxes; -A combination of model-checking and formal proofs to verify correctness and completeness of the wait-free objects.

The TAP Artifact Evaluation Committee has reviewed the full artifact of our approach (available on [START_REF] Hurault | TLA + proof of Moir-Anderson renaming algorithm[END_REF]). The four reviewers have found it consistent with the paper and have noted that the structure of the proofs in the artifact match their description in the paper. Regarding correctness, the four proof files have all been replayed without errors. As expected, checking the completeness is more intricate, and the reviewers have reached different upper bounds depending on their computing power.

2 TLA + Specification Language and Tools

Language

TLA + [Lam02] is a formal specification language based on untyped Zermelo-Fraenkel set theory for specifying data structures, and on the temporal logic of actions (TLA) for specifying dynamic behaviors. TLA + allows specifying symbolic transition systems with variables and actions. An action is a transition predicate between a state and a successor state. It is an arbitrary first-order predicate with quantifiers, set and arithmetic operators, and functions. In an action, x denotes the value of a variable x in the origin state, and x ′ denotes its value in the next state. Expressions rely on standard first-order logic, set operators, and several arithmetic modules. Functions are primitive objects in TLA + . The application of function f to an expression e is written as f [e]. The set of functions whose domain is X and whose co-domain is a subset of Y is written as [X → Y ]. The expression domain f is the domain of the function f . The expression [x ∈ X → e] denotes the function with domain X that maps any x ∈ X to the expression e (which can include x). The notation [f except ![e 1 ] = e 2 ] is a function which is equal to the function f except at point e 1 , where its value is e 2 . A specification of a system is usually a disjunction of actions. Fairness, usually expressed as a conjunction of weak or strong fairness on actions, or more generally as an LTL property, ensures progression.

Tools

The TLA + toolbox contains the TLC model checker, the TLAPS proof assistant, and various tools such as a translator for the PlusCal Algorithm Language [Lam09] into a TLA + specification, and a pretty-printer that converts a textual TLA + specification into a L A T E X file.

PlusCal. Pluscal is an algorithm language that looks like a programming language (assignment, loop, conditional) augmented with constructs for describing concurrency and non-determinism. PlusCal is actually more expressive than a traditional programming language as its expressions are any TLA + expressions.

TLC. TLC, the TLA + Model Checker, is an enumerative explicit-state modelchecker that can check safety and liveness properties. Its parallel implementation achieves a close to linear speedup for checking safety properties. To verify a TLA + specification, TLC requires all constants (e.g. number of processes) to be instantiated.

TLA + Proof System. TLAPS, the TLA + Proof System, is a proof assistant for writing and checking TLA + proofs [START_REF] Chaudhuri | Verifying safety properties with the TLA + proof system[END_REF]. TLA + proofs are written in a hierarchical and declarative style with steps and substeps. A proof manager translates these steps in proof obligations, checks the trivial ones and uses backend provers for the other ones. These backend provers include SMT provers (CVC3 is supplied, and Z3, CVC4, VeriT and Yices are supported), a TLA + theory in Isabelle, Zenon (an automated theorem prover for first-order logic based on the tableau method), or LS4 (to prove Propositional Temporal Logic).

The Renaming Problem

The renaming problem consists in renaming processes so they have a unique name on a small space. Initially, every process is assumed to have a unique identifier on an arbitrary large space (for instance, the IP address of the computer it is running on and the memory address of its control block). The only property of these identifiers is that they allow distinguishing processes, that is they can be compared for equality. A renaming algorithm assigns a distinct value, called a name, to each process, so that no two processes have the same name and the range of these names is small with regard to their initial identifiers. This algorithm is useful as it allows to efficiently refer to a set of processes, for instance by using an array indexed with their names.

In a shared-memory context, a trivial algorithm can solve the renaming problem using a counter and a lock. To get a name, a process acquires the lock, gets the current value of the counter and increments it, and releases the lock. Then the range of names for renaming N processes is optimal with size N. This algorithm has two shortcomings: it is inefficient under high load because of contention on the lock, and it is not delay-tolerant or fault-tolerant. If a process is delayed or stops while holding the lock, the other processes have to wait for it to complete its invocation, potentially infinitely. This can happen for instance if a process is paused or swapped by the process scheduler, or in an adversary environment, when an evil process does a denial-of-service attack by holding the lock.

Several wait-free algorithms for the renaming problem have been proposed [MA95,AM99,GR10,CRR11,RR11]. In these wait-free algorithms, the lack of progress of one process has no impact on the progress of the others. In this paper, we focus on the first wait-free algorithm for renaming that has been proposed, by Moir and Anderson [MA95]. This algorithm renames up to N processes from an arbitrary large namespace to a namespace of size N (N +1) with time complexity Θ(N ). We have actually considered a more demanding variation of the original algorithm: the proven algorithm is adaptive, in the sense that the size of the resulting namespace only depends on the actual number of participants (as opposed to the maximal number of participants for non-adaptive renaming).

Informal Description

Moir and Anderson algorithm is based on a building block, the splitter (Fig. 1). A splitter is used to separate processes. When a process executes the code of a splitter, it eventually receives a value of stop, right or down. The main property is that at most one process ever receives stop, not all processes receive right and not all processes receive down. Simultaneous invocations of a splitter are possible, and its code is concurrently executed. Equipped with this splitter, the renaming algorithm consists in a half-grid of splitters (Fig. 2).

Every process starts in the (0, 0) box and follows the rule of the splitter it is on. If it receives stop, it gets the name on this splitter and ends. If it receives right (resp. down), it moves to the right (resp. down) splitter. For N processes, a half grid of N (N +1) 2 splitters ensures that every process eventually gets a unique name (on the diagonal in the worst case, which it needs N moves to reach, thus time complexity of Θ(N ), splitters being Θ(1)).

Algorithm

The renaming algorithm is given Fig. 3. Each splitter at coordinate (d, r) is implemented with two atomic registers X and Y that are shared by all processes. These registers ensure that reads and writes are atomic under concurrent access. More precisely, an atomic register is a linearizable object that has two operations read and write. Informally, linearizability means that each operation call appears to take effect instantaneously at some point between its invocation and its response. More rigorously, linearizability means that the object behaves as if all processes agree on a sequential history of operations that is correct with regard to the sequential definition of the object (i.e. a read returns the most recent written value), and such that this history does not reorder completed operations. From a proof point of view, it means that the algorithm behaves as an interleaving of atomic process actions, where an action can read or write at most one shared variable.

1 initially ∀ d,r ∈ 0..N-1, d+r < N : Y[d][r] = FALSE ∧ X[d][r] = ? 2 rename(id) 3 while (d+r < N-1 ∧ ¬ stop ) do 4 X[d][r ] := id ; 5 if Y[d][r ] 6 then r := r + 1 \ * right 7 else 8 Y[d][r ] := TRUE 9 if (X[d][r ] = id)
Initially, all the Y are false, and the X can hold any value. The variables d, r and stop are local to each process. An arbitrary number of processes (up to N ) concurrently call rename with their original ids on the large namespace. Each process individually progresses at its own speed. When it gets a stop or reaches the diagonal, it computes a return value from its coordinates in the grid, using Cantor pairing function (a bijection from N × N to N).

Proving the Renaming Algorithm with In-Line Splitters

A Focus on the Splitter

Let's consider one splitter in isolation (Fig. 4). A splitter is inherently concurrent, and it cannot be specified as a sequential object with a single operation. This is shown by contradiction. Assume there is a sequential object with a single operation that behaves as a splitter. As it is sequential, there exists a first process to invoke its operation. As this process may be alone, it must obtain stop (right and down are incorrect if it is alone). The next processes can receive either down or right, without restriction. Such a sequential object has fewer behaviors than a splitter: with a splitter, a concurrent execution allows half the processes to receive down and the other half to receive right, and none to receive stop. For instance, consider two processes that simultaneously enter the code in Fig. 4. Process 1 writes register X with its id (line 3); process 2 overwrites it with its own id; process 1 tests Y and finds it false (line 4); it checks the value of X (line 6), does not found its id, and gets down; then process 2 checks Y (line 4), finds it true, and gets right. Thus, a splitter cannot be called as a function, and its code is in-line in the code of the renaming.

Correctness Properties. The correctness properties of a splitter are:

Coherency processes are split in at least two categories, and at most one stop:

  ∀p, q ∈ P roc, dir p = stop ∧ dir q = stop ⇒ p = q ∧ ∃p ∈ P roc, dir p = right ∧ ∃p ∈ P roc, dir p = down   (1)
Termination every correct entering process eventually gets a direction:

∀p ∈ P roc

An Attempt at Proving the Renaming Algorithm

The renaming algorithm has been specified in TLA + , using PlusCal [Lam09]. The steps have been chosen such that there is at most one read or write of a shared register at each step. This leads to six atomic transitions. Even if the principle and the algorithm are quite simple (13 lines, 2 matrices of shared registers, 2 conditionals and 1 loop), the proof of the uniqueness of the names is not trivial.

Correctness Properties. The renaming algorithm must verify:

Coherency processes obtain unique names:

∀p, q ∈ P roc, p = q, (name p = ⊥ ∧ name q = ⊥ ⇒ name p = name q ) (3)

Termination every correct entering process eventually gets a name:

∀p ∈ P roc, (p enters the renaming ⇒ ♦(name p = ⊥)) (4)
Model Checking. To get an idea of the degree of interleaving, we have modelchecked both a splitter and the renaming algorithm with TLC, the TLA + model checker (Table 1). Observe that model-checking was quickly overwhelmed for the renaming algorithm. Checking with four or five processes is insufficient to get confidence in the correctness of the algorithm. Scaling from four to five processes took a lot of time (more than two days compared with less than one minute) and resources (16 GB memory and up to 110 GB disk space were required).

Proof. In the original paper, the correctness proof is given "on paper" and takes 4 pages and 12 invariants. Half of these invariants are considered trivial, and no proofs are given. Mechanically proving these trivial invariants was already challenging because of the intricate behavior of the splitters, and it was clear that a complete proof would require too much effort.

Proving the Renaming Algorithm with Linearizable Splitters

Seeing that the trivial parts of the proof were not that trivial, we decided to rethink the original algorithm:

-to reduce the interleaving, by reducing the number of step/transitions in the algorithm; -to hide the internal parts of the splitters, as much as possible; -to take advantage of the grid architecture (Fig. 2) by finding a way to make direct call to the splitters and being able to use theorems on splitters.

Making the Splitter Linearizable

To reduce interleaving and being able to see the splitter as a black box, the natural idea is the notion of atomic or linearizable objects [START_REF] Herlihy | Linearizability: a correctness condition for concurrent objects[END_REF]: a linearizable object behaves as if it is accessed sequentially, even in presence of concurrent invocations. Unfortunately, as shown in Sect. 4.1, a splitter is inherently concurrent, and it cannot be expressed as a linearizable object with one operation. However, the results of [START_REF] Castaneda | Modular machinechecked proofs of concurrent algorithms built from tasks[END_REF] state that the splitter can be transformed in an object with a sequential specification composed of two operations set and get.

A Set/Get Splitter. The specification of the splitter with two operations (set and get) is given in Fig. 5. Each of the operations is divided in an enabling condition (setenabled/getenabled ) and a construction of the new state (set/get). The set operation is enabled if the process is not already in the splitter and registers that the process is entering the splitter. The get operation corresponds to a process receiving a direction. The pre-condition of the get operation ensures that the answer is valid regarding the specification in Fig. 1 and Eq. (1). For a variable spl and a process p ∈ P roc, a well-formed usage of the module is a sequence of two TLA + actions: setenabled(spl, p) ∧ spl ′ = set(spl, p), then ∃dir ∈ {Stop, Down, Right} : getenabled(spl, p, dir) ∧ spl ′ = get(spl, p, dir).

Proofs of Correctness and Completeness.

To be useful, this version of the splitter needs to be correct and complete. The correctness is the coherency property (1) and the termination property (2). The completeness means that any correct output can be delivered by the splitter with set/get. Indeed, the goal of this version of the splitter is to be used as a black box in the renaming algorithm. The proof of the renaming algorithm will be done with the black box version, and the implementation will use a particular implementation of the splitter, for instance the one in Fig. 4. If the black box version is not complete, the proof may omit some pathological cases. Correctness. The correctness proof is done assuming that the splitter is wellused, i.e. that set is called before get and the enabling conditions of each operation are true. The proof of termination (2) is trivial: there is no loop and whatever were the return values to previous processes, a process can always get at least one valid value and thus cannot be blocked in the enabling condition getenabled. The proof of coherency (1) has been conducted with TLAPS for any number of processes (file Splitter correct proof.tla in [START_REF] Hurault | TLA + proof of Moir-Anderson renaming algorithm[END_REF]).

Completeness. Completeness of this specification has also been considered. It must be shown that all correct combinations of output values are possible. The predicate CorrectDirection(Proc, direction) states that direction is a valid output array satisfying (1), and dir is the received values of the processes. Completeness is expressed as (where EFP is the CTL (computational tree logic) temporal operator stating that there exists a branch where P is eventually true):

Completeness

∀direction ∈ [P roc → Direction] :

CorrectDirection(P roc, direction) ⇒ EF(dir = direction)
TLA + is based on LTL (linear temporal logic) and this CTL formula is not checkable. However, the negation of EFP is AG¬P , and as P is a state predicate, this corresponds to the LTL invariant ¬P . Thus, completeness can be verified in the following way. First, TLC is used to enumerate all the valid arrays of direction. Then, each of them is stated as unreachable ( ¬(. . .)), and this property is checked with TLC. A counter-example proves that the state is actually reachable. Optimisations based on symmetry have been introduced, and the completeness of the set/get splitter has been verified up to 10 processes (255877 distinct states to check for reachability, reduced to 119 with permutations, 1 h 42 min on a modern quad core laptop).

The Renaming Algorithm Using Linearizable Splitters

The renaming algorithm has been rewritten using set/get splitters. The PlusCal version of the renaming problem using set/get splitters is given in Fig. 6. The translated TLA + had to be slightly tweaked because the provers have difficulties handling except with multi-dimensional arrays, whereas the equivalent form that defines an array is fine2 .

Proof Sketch of the Coherency Property

The full proof has been conducted with TLAPS and is available online [START_REF] Hurault | TLA + proof of Moir-Anderson renaming algorithm[END_REF]. The line numbers below refer to the file Renaming.tla that holds the algorithm and its proof.

Overall Picture. The correctness property (3) states that all the processes must have distinct names (Uniqueness property in the TLA + module -line 2027). This uniqueness is guaranteed if all the processes end with different coordinates (I12 property -line 1955, whose proof (lines 1957-1979) is used to prove the Uniqueness property (lines 2030-2040)). A process ends either on the diagonal (condition d + r < N P -1 violated, line 14 in Fig. 6) or if it gets Stop in a splitter that is not on the diagonal (lines 15-17 in Fig. 6). Consider two different processes that get a name (line 28):

-they both stop in a splitter that is not on the diagonal: as at most one process can stop in a splitter, they stop in different splitters and do not have the same coordinates (StopDifferentProcessesDifferentCoordinates property -defined line 429 and proved lines 353-434); -one process stops in a splitter that is not on the diagonal, and the other one stops on the diagonal: they trivially do not have the same coordinates (StopAndDoneDiffCoord property -defined line 566 and proved lines 438-574); -they both stop on the diagonal: this is not trivial and is explained in the following (IDDX property -defined line 1851 and proved lines 577-1906). The first disjunction handles the case where the coordinates are outside the half-grid (i+j ≥ N P ), and the second one handles the case where the coordinates are inside the half-grid (i + j < N P ).

A simple induction using that processes enter a splitter (i, j) either from the splitter on top (i -1, j) or from the splitter on left (i, j -1), and that not all processes can go down or right, gives that there is at most N P -(i -1 + j) -1 + N P -(i+j -1)-1, i.e. 2 * (N P -(i+j)) processes in the splitter (i, j). This basic induction fails. As an example, consider the splitter (1, 1). To receive N P -2 processes from the splitter (0, 1), there must be at least N P -1 processes in the splitter (0, 1). It means that there is at most 1 process in the splitter (1, 0). This process, alone, stops in this splitter and no process comes from the splitter (1, 0) to the splitter (1, 1).

Since a simple induction fails, another invariant is needed (NbParticipantsBis property -line 795):

∀i, j ∈ Coord : Cardinality({p ∈ P rocSet : d[p] ≥ j ∧ r[p] ≥ i}) = 0 ∨Cardinality({p ∈ P rocSet : d[p] ≥ j ∧ r[p] ≥ i}) ≤ N P -(i + j)
This invariant considers the triangle below and to the right of (i, j), i.e. the triangle with coordinates (i, j), (N P -1i, j) and (i, N P -1j). In the following, we refer to this triangle as the (i, j) triangle.

The proof is done by proving that the property is preserved by all the transitions. For the (i, j) triangle, the two non-trivial cases are when a process in a splitter in column i -1 moves right, or a process in a splitter in line j -1 moves down. In both cases, the number of processes in the (i, j) triangle increases. These two cases are symmetric, and only the first one is discussed.

The intuition behind the proof is shown in Fig. 7.

-The induction hypothesis gives that in the (i -1, j) triangle (green in Fig. 7), there are less than N Pij + 1 processes. -The fact that self can move right ensures that there is at least another process in the splitters including or below the one of self (orange in Fig. 7). This property (2InColumnWhenRight property -line 1380) is proved thanks to another invariant that states that if at one point there is a participant in a splitter, there will always be (at least) a process in the column of the splitter (AlwaysOneInColumn property -line 1248). This last one is proved thanks to the correctness of the splitter: not all processes can go right (EnableRightExistsOtherNotRight -line 199 in the Splitter.tla file).

This means that before self moves, there is at most N Pij + 1 -2 processes in the (i, j) triangle (blue in the Fig. 7). So after the transition, there are at most N Pij + 1 -2 + 1 = N Pij processes in the (i, j) triangle. QED.

Metrics of the Proof. The first version was 3000 lines, and after cleaning (factorization into lemma and removing steps not needed by TLAPS), it consists in 2000 lines of TLAPS for the renaming, and 200 lines for the splitter, with a total of 70 lemmas and theorems, and 963 proof steps.

The splitter proofs are composed of 93 proof obligations. Among them, 43 are obvious and discharged by tlapm (the TLA + proof manager). The other 50 are proved by SMT (we use CVC3, VeriT and Z3). The renaming proof is composed of 1541 proof obligations. Among them, 914 are trivial and proved by tlapm. Among the 627 left, 108 are proved by Zenon (an automated theorem prover), 35 are proved by LS4 (temporal logic), 475 are proved by SMT and 9 are proved by Isabelle (properties on sets).

|{p ∈ ProcSet : d [p] ≥ j ∧ r [p] ≥ i -1}| ≤ NP -i -j + 1 At least 2 processes self + other |{p ∈ ProcSet : d [p] ≥ j ∧ r [p] ≥ i}| ≤ NP -i -j + 1 -2 (Green -Orange)
To check the proof, TLAPS takes 10 min on a quad core modern laptop.

Proof Sketch of the Termination Property

The second correctness property is the termination (4): every correct process eventually gets a name. To do this, we show by induction that, for each process, (d, r) lexicographically increases until either the sum reaches N P , or the process receives a Stop and terminates. Assume a process is at l0 (Fig. 6, lines 12-13), that its current value of (d, r) is (i, j) and that (d, r) has lexicographically increased until that point, meaning that it is the first time it reaches (i, j). At l0, setenabled is true as the process has not previously called set on the splitter (i, j). The process reaches l1 (line 14). At l1, the process can go to l8 and terminate (QED), or continue to l2. At l2 (lines 15-27), getenabled is true as the process has previously called setenabled on this splitter, the process has not previously called get on this splitter (first occurrence of (i, j)), and at least

                          

⇒

Renaming with concurrent splitters correctness termination (paper ) termination (paper ) Fig. 8. Summary of the approach. For each property, the verification method is given (proof with TLAPS, model-checking with TLC, proof on paper).

one of the choices {Stop, Right, Down} is enabled (the specification of a splitter (Fig. 5) guarantees that the three sets stop, down and right are disjoint, thus at least one choice is enabled). If the process gets Stop, it goes to l8 and terminates (QED); if it gets Down or Right, d or r increases, thus (d, r) becomes (i + 1, j) or (i, j + 1), and so lexicographically increases. The condition in l1 eventually becomes false, and the process reaches l8 (QED). TLAPS does not support checking liveness properties, and this proof has not been mechanically verified.

Back to the Original Algorithm

The last step to prove the original Moir-Anderson algorithm of Fig. 3 consists in putting back the concurrent splitters implemented with registers in place of the linearizable splitters with set/get. Both versions of the splitter have been proved equivalent by proving that they satisfy the same correctness properties (properties (1) and (2)) and are both complete3 . For the concurrent splitter, the proof of coherency (1) has been done in TLAPS (file Splitter register.tla in [START_REF] Hurault | TLA + proof of Moir-Anderson renaming algorithm[END_REF]). It consists in 8 lemmas and theorems that prove 17 elementary properties with 30 proof steps. The proof of termination (2) is trivial as it is straight-line code. The proof of completeness has been done by model-checking just like for the linearizable splitter (Sect. 5.1).

Regarding termination of the renaming algorithm with concurrent splitters (4), a similar argument to 5.4 shows that, for each process, (d, r) lexicographically increases until either the sum reaches N P , or the process receives a Stop and terminates.

Wait-free data structures were introduced by Herlihy [START_REF] Herlihy | Wait-free synchronization[END_REF], and then automatically derived from a sequential implementation using universal simulations [START_REF] Herlihy | A methodology for implementing highly concurrent objects[END_REF]. However, the state of the art universal construction [START_REF] Chuong | A universal construction for wait-free transaction friendly data structures[END_REF] is still far too slow compared to the hand-crafted lock-free or lock-based versions. In [START_REF] Timnat | A practical wait-free simulation for lock-free data structures[END_REF], the authors observe that wait-free implementations are notoriously hard to design and often inefficient. One approach consists in designing a lock-free data structure, and then in manually transforming it into a wait-free data structure. [START_REF] Timnat | A practical wait-free simulation for lock-free data structures[END_REF] presents a mechanical transformation of lock-free data structures to wait-free ones. The limits of this work is first, the existence of the lock-free implementation, which has to be written and proven, and secondly, that this implementation must have a normalized form to be convertible.

[GGH05] is a rare example of the certified proof of a lock-free algorithm. The proof of safety has been conducted in PVS, while the proof of progress is on paper. Building on this experience, [GH04] presents a reduction theorem that allows reasoning about a lock-free program to be designed on a higher level than the elementary synchronization primitives. Lamport's refinement mappings are used to prove that the lower-level specification correctly implements the higherlevel one. The reduction theorem has been verified with PVS.

Wait-free implementation of tasks have been mechanically proven (e.g. [ORV+10,TSR14, DGH13]). However, to the best of our knowledge, no nontrivial wait-free algorithm built upon wait-free tasks has been mechanically proved. Our intuition for this situation is that proofs cannot be made modular and compositional when using bricks which are inherently concurrent if their internal structure must be visible to take into account this concurrency. Several complex and original algorithms can be found in the literature such as Moir and Anderson renaming algorithm [MA95] that we have considered in this paper, stacks implemented with elimination trees [START_REF] Shavit | Elimination trees and the construction of pools and stacks[END_REF], lock-free queues with elimination [START_REF] Moir | Using elimination to implement scalable and lock-free FIFO queues[END_REF]. In these papers, the correctness proofs are intricate as they must consider the algorithm as a whole, including the tricky part involving wait-free objects, and they have not been mechanically checked. Our approach which exposes a more simple and sequential specification (instead of a complex concurrent implementation) seeks to alleviate this limitation.

Other works have studied the replacement of the complex implementation of part of a system with a simpler one to ease the proof. For example in [START_REF] Gu | Deep specifications and certified abstraction layers[END_REF], the authors use the notion of deep specification to verify a layer-based architecture. By taking into account the context, a given deep specification may have several implementations which all yield equivalent behaviors. Then, a proof of a whole program can be done using the deep specification of a subprogram (which is simpler than the implementations) and it will stay valid when replacing this subprogram with its implementation. Our approach is similar with a non-layered algorithm, and the set/get specification can be seen as a deep specification, adhering to the coherency property and compatible with the non-linearizable nature of the splitter.

Conclusion

Mechanically proving and certifying a wait-free algorithm built upon wait-free objects is a challenging task. An important step is the replacement of the internal wait-free objects with objects having a sequential specification. This allows a compositional approach to the proof, where theorems are proved on the internal objects and reused in the proof of the algorithm. Moreover, this black box view greatly reduces the number of control points in the algorithm, and thus the number of interleavings.

TLA + has been found well adapted for this task. It natively contains advanced data structures (sets, arrays and maps) with the usual mathematical foundations and notations. Concurrency is intrinsic, both in algorithm description and in reasoning. Tool support is adequate, allowing tests (possibly exhaustively on small models) and proofs. The hierarchical structure advocated by Lamport [START_REF] Lamport | How to write a 21st century proof[END_REF] helps in incrementally building the proofs, by focusing on the important cases of a theorem and delaying the proofs of the obvious or marginal cases. Proving a realistic algorithm such as Moir-Anderson algorithm requires various theories: numbers (coordinates in the grid), sets (cardinality and partitioning), functions (arrays), temporal logic (invariants). The hierarchical structure allows decomposing the proof of a theorem that requires several theories in steps where only one is needed. This in turn allows using the most adequate prover for this theory and simplifies automation of the proof.

A Description of the Artifact

This artifact [START_REF] Hurault | TLA + proof of Moir-Anderson renaming algorithm[END_REF] allows to replicate all the results that we claim in the paper:

-the proof of correctness of the splitter with registers, -the proof of correctness of the splitter with set/get, -the way to check the completeness of the splitter with set/get, -the way to check the completeness of the splitter with registers, -the proof of correctness of the renaming algorithm using the set/get splitter.

Combining these results implies that the renaming algorithm is correct when used with the original splitter with registers.

A.1 Requirements

Running the artifact relies on the TLA+ Toolbox and the TLA+ Proof System. Both are included in the distributed files, and a script is supplied to install them. The verification of the correctness proofs is achievable on a standard laptop, checking the completeness requires much more resources (at least a quad core with 8 GB of memory, and a 32 core computer with 16 GB was used for the largest numbers of processes).

A.2 Proofs of Correctness

The proof of correctness of Moir-Anderson renaming algorithm is built upon the four following files:

-Splitter.tla: the set/get splitter with some lemma needed for the correctness proof of the renaming; -Splitter correct proof.tla: the proof of correctness of the set/get splitter; -Renaming.tla: the Renaming algorithm and its proof of correctness; -Splitter register.tla: the splitter based on register and its proof of correctness.

One just has to load them in the toolbox and launch the verification, as explained in the artifact distribution.

A.3 Proofs of Completeness

The goal is to verify the completeness of an implementation w.r.t a property P, i.e. that all the valid (w.r.t to P) assignments of the variables are reachable in the implementation. Our approach consists in two steps: first generate all the valid assignments; then, for each of these assignments, verify that it is reachable. As we rely on TLC, the TLA + model checker, this approach works for a given number of processes.

1. Choose a number of processes; 2. generate-states nbproc Splitter config.tla

The module Splitter config.tla is used to generate all the return values that satisfy the correctness property of the splitter, for nbproc processes.

check-reachability vars XXX.tla

For each valuation (read from stdin), a module is built with an invariant invariant U nreachable ∆ = vars = valuation and it is model-checked with the specification in XXX. It should end with a violation, which proves that this state is reachable. 4. Once all states have been checked, this proves the completeness of XXX for this number of processes.

A script runall enumerates the verification of both splitter specifications for 1, 2, 3 etc. processes. One can also check a specific size.

Fig. 2 .

 2 Fig. 1. Specification of a splitter

Fig. 3 .

 3 Fig. 3. Code of the renaming algorithm

Fig. 4 .

 4 Fig. 4. Implementation of a splitter with two registers

  ∧ ∨ ans = Stop ∧ s.stop = {} valid answers ∨ ans = Right ∧ (s.right ∪ {pid }) = s.participants ∨ ans = Down ∧ (s.down ∪ {pid }) = s.participants get(s, pid , ans) case ans = Stop → [s except !.stop = {pid }] ✷ ans = Right → [s except !.right = s.right ∪ {pid }] ✷ ans = Down → [s except !.down = s.down ∪ {pid }]

Fig. 5 .

 5 Fig. 5. The TLA + set/get specification of a splitter

Fig. 6 .

 6 Fig. 6. Renaming algorithm in PlusCal using set/get splitters.

Fig. 7 .

 7 Fig. 7. Intuition behind the proof of Moir-Anderson algorithm (Color figure online)

Table 1 .

 1 Another difficulty with the splitter (and more generally with wait-free objects) is that the reachable state space is a significant part of the possible valuations of the variables. The direction variable can hold four values (the undetermined value ⊥, stop, down, right), thus the corresponding state space for N processes is 4 N . The number of valid assignments of directions that respect the property of coherency (1) is 1 : Model-checking of a Splitter with registers (left) and of the Renaming Algorithm with registers (right). NP is the number of processes, distinct states is the number of distinct states found by TLC, and depth (or diameter) is the length of the longest execution (ignoring stuttering loops). Times are wall-clock time. Experiments were conducted on a 32 core 2,1 GHz computer with 16 GB.

		Number of processes 2	3	4	5	6	7	8
		Possible assignments 16	64	256 1024 4096 16384 65536
		Valid assignments	13	52	187 646 2185 7288 24055
		Percentage		81% 81% 73% 63% 53% 44% 38%
	NP distinct states depth time
	2	98	11
	3	1389	16				NP distinct states depth time
	4	17164	21				2	142	14
	5	193115	26 2 s				3	21260	33 1 s
	6	2041458	31 15 s				4	6381732	58 56 s
	7	20675305	36 1 min 50 s			5 5183748425	90 51 h 19 min
	8	203055896	41 12 min 24 s
	9 1948989879	46 16 h 08 min

, (p enters the splitter ⇒ ♦(dir p ∈ {stop, down, right})) (2) State Space.

The percentage decrease is explained by the progressive dominance of multiple stop in the invalid assignments.

The construct [x except ![e 1 ] = e 2 ] is a shortcut for [i ∈ domain x → if i = e 1 then e 2 else x[i]].For multi-dimensional arrays, provers work better with the latest.

Another approach would have been to show a bisimulation between their transition systems. Note that it requires to exhibit a parameterized bisimulation, as we have to consider any number of concurrent invocations. We had already proved the properties on the concurrent splitter during our initial attempt at proving the renaming algorithm (Sect

. 4.2) and it seemed simpler to continue onward.