J L Schanen

J P Ferrieux

J M Guichon

J Barbaroux

J P Keradec

A Maurel

Flyback Converter Surface Minimization: Design Procedure and Formulas

This paper gives generic formulas to account for power components surface in the design of a flyback converter. Starting from the converter requirements, key design parameters are defined, and their influence on converter surface studied. It is shown that some parameters have opposite actions, thus some trade-off must be found. On the other hand, additional constraints must be taken into account, especially losses. These ones are also evaluated using analytic formulas, and included in the design procedure. After design, the converter has been built, and compared to previous version, surface reduction is obvious.

I.

INTRODUCTION

Flyback converters are used in many low power applications. Very often, increasing power density is a key feature. For several applications, conventional PCB is used, and plugged into standardized racks. The power density increase corresponds then to a surface reduction (with often a maximum height requirement).

Designing a power converter with respect to a minimal surface means to set up an optimization strategy. The design variables must be chosen such as a minimum surface can be reached. However in the same time, other constraints must be fulfilled: external requirements obviously, but also other technological parameters, such as maximum losses in the components, or peak voltage on the semiconductors… Last, if a maximal height is required, component choice must account for this geometrical constraint.

This paper has thus the same goal as other design procedures explained in [START_REF] Wang | Expert system aided design, simulation and optimization of power converters[END_REF][START_REF] Larouci | Volume optimization of a PFC flyback structure under electromagnetic compatibility, loss and temperature constraints[END_REF]. However, the proposed method does not rely on complex computer aided methods, as expert systems or heavy time simulation. For a dedicated application, such as the Flyback converters used in this paper, a fully analytical method is available, what allows simple use in any conventional software, as a Mathcad sheet for example.

In the first section of this paper, the topology to be designed will be presented. Then, design procedure will be detailed. First, the choice of the minimum number of design parameters will be presented. Then, all physical phenomena to be accounted for during the design will be listed. Analytical expressions will be given in section IV, and exploited in section V to propose some design trade off curves. The main difficulty is that the proposed expressions must be valid for any kind of design parameters value; this means that they must handle either continuous or discontinuous conduction mode. Validation of the proposed design will be proposed in section VI.

II. CONVERTER REQUIREMENTS AND TOPOLOGY

The application illustrating our design method is a Switched Mode Power Supply (SMPS) with following requirements (for auxiliary feeding in railway (2.4A). => we defined a 12 V SMPS, and for the design, we have considered the total power on this outputThe converter topology has been chosen as a half Bridge Flyback structure (Figure 1. ), well adapted to this power range, with the advantage of recycling leakage energy, instead of dissipating it [START_REF] Wah | A novel High efficiency Flyback for PFC circuit with regenerative clamping and soft switching[END_REF]. The behaviour of this converter is well known. For 0<t<α.t, both switches are turned on: transformer is thus magnetized under voltage Ve. Output Diode is off and must handle reverse voltage (m.Ve+Vs), where Ve and Vs are input and output voltage respectively, and m the transformer ratio. At t = α.t, the two switches are turned off, demagnetization occurs first on the primary side, due to transformer leakage. This phase is neglected in the design phase, except for primary switch voltage constraint, which is imposed at Ve. Then, the conventional demagnetization on the secondary side occurs. The two switches must handle Ve+Vs/m. A reasonable assumption is that the two switches share this voltage equally. Therefore, each switch must blocks (Ve+Vs/m)/2.

III. DESIGN PROCEDURE

As briefly mentioned in the introduction, the main goal of this paper is to optimize a Flyback converter. An optimization process consists in finding a correct set of design variable values that maximize or minimize a given objective function. In our application, the converter surface will be chosen as objective. However, several constraints must be fulfilled, what leads to a non obvious problem. Usually, the designer starts from his knowledge of the converter and focuses his attention on the most critical component. In the Flyback converter, it is obviously the transformer, which is bulky and the most complex component to be designed. Therefore, the converter optimization often results in a transformer optimization, and the other components are just considered using constraints. However, the converter optimum is not reached for every component optimum, and the best solution must account for all problems simultaneously. Therefore, we first modelled the complete Flyback behaviour, expressing all waveforms and associated results in a close form. Then, the objective function (surface) and all constraints could be expressed. Starting from external requirements only (input and output voltage -Ve and Vs-and power -P-), it is thus possible to carry on the surface minimization.

The components included in surface computation will be the transformer and the output capacitor (input capacitor is designed with respect to energy tank considerations, what is out of the scope of this paper). For simplification, we considered that for the power range of interest, semiconductor devices will be implemented in a TO-220 package associated with localized heatsinks. Therefore, whatever the converter design, it won't affect the surface minimization. Thus, heatsinks and semiconductors haven't been taken into account in the surface computation. However, losses have been computed, in order to guarantee a maximal temperature on the silicon dies.

A. Design parameters definition

The objective function and all constraints are deduced from converter waveforms, either directly (for instance semiconductor peak voltage) or after data processing. As illustrated in Figure 2. , for both Continuous Conduction Mode (CCM) and Discontinuous Conduction Mode (DCM), they depend on:

• switching frequency f

• duty cycle α • Magnetizing inductance L1
• transformer ratio m = n1/n2 However, due to fixed power, input and output voltages, duty cycle can be expressed as a function of the other parameters:

α Vs m ⋅ Vs m ⋅ Ve + in CCM, and α 2 L1 ⋅ f ⋅ P ⋅ Ve 2 in DCM
The design parameters are thus only f, m and L1. To be noticed that due to the pre-regulation function of this converter, output voltage ripple is not really constraint, thus, output capacitor value is not a design parameter. After design, it just must be checked that the capacitance is not too small. In fact, the most important constraint for the capacitor is its rms current.

B. Surface computation

The aim of this paper is to minimize the surface of the passive elements. Thus, they must be evaluated as a function of the design parameters. For a given technology, the surface of the output capacitor is linked to its rms current. Based on a 35V Electrolytic capacitor serie [START_REF]Non Solid Al -electrolytic capacitors Power Long Life Snap-In[END_REF], the capacitor surface has been plotted as a function of its rms capability (Figure 3. ). It is clear from this figure that a quadratic approximation can be made, what is not quite surprising since capacitor surface is linked to its ability to evacuate the losses, which depend on the quadratic value of the rms current.

The transformer surface is obviously linked to its design. A well known design method is the area product [START_REF] Colonel Wn | Transformer and Inductor Design Handbook[END_REF]. The transformer Area Product Ae.Sf (winding area * core area) can be expressed as a function of peak primary current and rms primary and secondary currents. Analytical expression can thus be derived as a function of the three design parameters, for both CCM and DCM. For a given core series, the surface occupied by the transformer can be linked to this area product using the same idea as the one proposed in [START_REF] Odendaal | Effects of Scaling High-Frequency Transformer Parameters[END_REF] Stransf K Ae Sf ⋅ ⋅ K has been computed to 14.5, according to ETD core series. Therefore, the transformer surface is linked to the three design parameters.

β α Ve Vs m ⋅ 1 + ⎛ ⎜ ⎝ ⎞ ⎟ ⎠ ⋅ L2 L1 m 2 Diameter Surface Scapa L1 m , f , ( ) Icapaeff L1 m , f , ( ) 2 27 ⋅ 10 6 - ⋅ 0.00008 + :=

Capacitor Surface

Rms Current

C. Losses and other constraints computation

Since all peak, average and rms currents can be expressed as a function of the design parameters, semiconductor losses can be computed, using well known losses models of semiconductors: voltage drop and resistance for diode, resistance for MOSFET. Switching losses can be estimated from switching times, peak currents and voltages applied to the semiconductors [7].

For transformer losses, if the peak induction and the magnetic material are fixed, losses may be estimated from manufacturer datasheet, even if accuracy is poor. It is important to account for this parameter, because it directly impacts the working of the Flyback: a high peak induction will allow reducing the area product and thus selecting a smaller core. On the other hand, it increases losses, which must be maintained under a given value. Copper losses cannot be precisely computed, due to the difficulty of considering proximity losses. However, a maximum current density is fixed, what allows maintaining reasonable losses. An estimate using DC resistor value can also be proposed.

Another key parameter for the transformer design is linked to the airgap: this one cannot be too large otherwise, leakage will increase. Even if leakage energy is recycled in this topology, a bad coupling is not desirable. Therefore, a maximum airgap is fixed. This one depends on the core size. In fact, the ratio Core_width/Airgap is fixed. For instance, for ETD 39 [8] core, it corresponds to a 2 mm max airgap.

Capacitor losses can be computed from rms current and esr value, which may be interpolated from manufacturer datasheet, as for capacitor surface in Figure 4. However, this has not been accounted in this study, since most of the losses are generated in the semiconductor and the transformer.

Voltage overshoot on the MOSFETS and the secondary diode is linked to the normal behavior of the and to transformer ratio. It is a constraint for semiconductor choice (computed for 137V).

Duty cycle a must stay within 0.1 (minimum technologically available) and 0.5, due to half bridge topology.

D. Surface Minimization

Having expressed the passive component surface, the losses and the constraints as a function of the design parameters, a set of design parameters achieving the minimum surface, satisfying all constraints can be selected (see section V). Then, the core reference can be selected, as well as the actual capacitor.

E. Parameter adjustment

After having selected the set of parameters corresponding to a minimum surface, and fulfilling all constraints, the core of the transformer is thus chosen. However, as illustrated in Figure 4. the actual surface is always bigger than the needed area product. Therefore, once the core has been selected, a second optimization can be carried out. Design parameters are then modified to exploit this core at the best. For this purpose, two compromises can be chosen. Either the design values may be changed to reduce capacitor size, then resulting in the best possible surface using this core. Another solution is to try to improve efficiency. In this case, frequency can be reduced so that losses are reduced. This frequency decrease is achieved in conjunction with a change in magnetizing inductor L1, so that the final result still corresponds to the optimal total surface. The complete methodology is shown on Figure 5. , and will be illustrated in section VI.

IV. ANALYTICAL FORMULAS All formulas have been implemented in a Mathcad sheet. In APPENDIX are only summarized the main equations. First is shown how to express the surface area product Ae.Sf, depending on the current conduction mode. The selection of the correct formula is achieved using the appropriate relationship that can be established at the limit between these two modes.

Rms current in output capacitor can also be computed from the knowledge of current waveforms. All other equations allowing constraints evaluation can be easily obtained, especially using some formal computations available in Mathcad. V. DESIGN TRADE-OFF Before achieving the optimization, we first studied the influence of each parameter on the total surface, computed using analytical formula. Frequency increase results in a smaller surface, what is obvious (Figure 6. ). Other parameter variation exhibit more interesting behaviors: Optimum surface appears when varying transformer ratio m or magnetizing inductance L1 (Figure 7. and Figure 8. ). It is a good illustration that the Flyback optimum does not results from the transformer optimum. Indeed, the transformer surface shows a monotonous variation as a function of all parameters: decreasing with frequency, increasing with magnetizing inductance, decreasing with transformer ratio m. To help in selecting the good design parameters, the surface has been plotted as a function of magnetizing inductance L1 and transformer ratio m, for different frequencies (Figure 9. ). It can be noticed that frequency does not modify the surface shape significantly. This can be explained by the monotonous variation of the surface versus frequency (Figure 6. ).

The optimization leads to the choice of m = 1.3, L1 = 36µH and f = 40kHz for satisfying all constraints, and especially semiconductors and transformer losses. However, for this design, the selected core (ETD34) is not fully used, as illustrated Figure 11. Indeed, once the core has been chosen, the area product is fixed, and it is nonsense not to using it. Therefore, a first solution is to increase the magnetizing inductor L1 until ETD34 is fully used. This L1 increase results in a decrease of RMS current in the capacitors, and therefore a surface minimization. In Figure 10. this corresponds to L1 = 55µH with the same frequency (40kHz).

Another solution is to try to reduce losses by reducing the switching frequency. In this case, a new value of L1 must be computed in order to keep the surface minimum. The f & L1 parameters must be determined conjointly, checking that ETD34 is still used optimally. In the treated example, the solution has been found to be 30kHz -44µH (Figure 10 & Figure 11. ). This lower frequency allows reducing the thermal constraints and increasing the converter efficiency.

VI. CONVERTER REALIZATION AND TESTS

The final choice has been L1 = 44µH, m = 1.3, f = 30kHz. The transformer is built with an ETD 34 core, n1 = 23, n2 = 17, air gap has been computed at 1.5 mm and peak induction has been imposed at 220mT. This optimized design is not far from discontinuous conduction mode, what is quite reassuring since this corresponds to the minimum stored energy in the transformer.

Global efficiency has been measured to validate losses models and achieve a sensibility study (Figure 13. ). Obviously, accuracy is not very good with these design models, but the error is not so big (88% expected, 83% obtained; Remember that capacitor losses were neglected).

Compared to the initial design, a significant surface reduction has been achieved. Indeed, on the same surface as the initial power supply, keeping the same height (because the PCB was inserted in a rack), 70W has been reached, compared to 35W initially. The power density was thus doubled thanks to an optimal design. Figure 9. Surface vs magn. inductance L1 and transformer ratio m (illustration purpose only -scale not available for m and L1 axis). VII. CONCLUSION In this paper, a fully analytical modeling of a Flyback converter has been proposed and implemented in a simple Mathcad sheet. This analytical description accounts for both continuous and discontinuous conduction mode and is therefore general. Thanks to some approximations, the area of passive components (transformer and output capacitor) can be computed. Transformer surface is linked to the well known area product, whereas output capacitor surface is correlated to rms current. The global surface (transformer + capacitor) depends on 3 parameters only, and exploring the space of solutions has allowed minimizing the surface, respecting all constraints on the components. After optimization, some adjustments have to be done, in order to account for the discrete nature of core references. Several options are possible: either pure surface minimization, or improving efficiency. Therefore, the power density has been doubled compared to initial power supply. Thanks to the analytical formulas, any other compromise or optimization goal may be easily reached. For instance a new design with the best efficiency on a given surface would only take a few minutes.

f [Hz]

Stransf + Scapa [m²] Stransf + Scapa [m²] L1 [H] Stransf + Scapa [m²]
m , f , ( ) L 2 L1 m 2 ← α 2 L1 ⋅ f ⋅ Vs ⋅ I2 ⋅ Ve 2 ← T 1 f ← IL2max m Ve L1 α ⋅ T ⋅ ⎛ ⎜ ⎝ ⎞ ⎟ ⎠ ⋅ ← β α Ve Vsm ⋅ 1 + ⎛ ⎜ ⎝ ⎞ ⎟ ⎠ ⋅ ← 1 3 3 1 2 ⋅ 6 β ⋅ T ⋅ Vs ⋅ α ⋅ IL2max ⋅ L2 ⋅ 3 β ⋅ IL2max 2 ⋅ L2 2 ⋅ Vs 2 α 3 ⋅ T 2 ⋅ - + β 3 T 2 ⋅ Vs 2 ⋅ 3 β 2 ⋅ T ⋅ Vs ⋅ IL2max ⋅ L2 ⋅ - + 3 β ⋅ T 2 ⋅ Vs 2 ⋅ α 2 ⋅ 3 β 2 ⋅ T 2 ⋅ Vs 2 ⋅ α ⋅ - 6 β ⋅ IL2max ⋅ L2 2 ⋅ I2 ⋅ - + 3 β 2 ⋅ T ⋅ Vs ⋅ I2 ⋅ L2 ⋅ 6 β ⋅ T ⋅ Vs ⋅ α ⋅ I2 ⋅ L2 ⋅ - + 3 I2 2 ⋅ L2 2 ⋅ + 6 α ⋅ IL2max ⋅ L2 2 ⋅ I2 ⋅ 3 α ⋅ IL2max 2 ⋅ L2 2 ⋅ - + 3 Vs ⋅ α 2 ⋅ T ⋅ I2 ⋅ L2 ⋅ 3 Vs ⋅ α 2 ⋅ T ⋅ IL2max ⋅ L2 ⋅ - + L2 2 ⎛ ⎜ ⎜ ⎝ ⎞ ⎟ ⎟ ⎠ 1 2 ⋅ := IcapaeffCCL1 m , f , ( ) L 2 L1 m 2 ← α Vsm ⋅ Vsm ⋅ Ve + ← T 1 f ← Δi Ve L1 α ⋅ T ⋅ ← IL2max m P Veα ⋅ 1 2 Δi ⋅ + ⎛ ⎜ ⎝ ⎞ ⎟ ⎠ ⋅ ← IL2min P Veα ⋅ 1 2 Δi ⋅ - ⎛ ⎜ ⎝ ⎞ ⎟ ⎠ m ⋅ ← 1 3 3 1 2 ⋅ Vs 2 α 3 ⋅ T 2 ⋅ 3 Vs 2 ⋅ α 2 ⋅ T 2 ⋅ - 3 T ⋅ Vs ⋅ I2 ⋅ L2 ⋅ - 3 T ⋅ Vs ⋅ IL2max ⋅ L2 ⋅ 3 I2 2 ⋅ L2 2 ⋅ - 3 IL2max 2 ⋅ L2 2 ⋅ - + 6 IL2max ⋅ L2 2 ⋅ I2 ⋅ + 6 Vs ⋅ α ⋅ T ⋅ I2 ⋅ L2 ⋅ T 2 Vs 2 ⋅ - + 3 T 2 ⋅ Vs 2 ⋅ α ⋅ 6 α ⋅ IL2max ⋅ L2 2 ⋅ I2 ⋅ - + 3 α ⋅ IL2max 2 ⋅ L2 2 ⋅ 3 Vs ⋅ α 2 ⋅ T ⋅ I2 ⋅ L2 ⋅ - + 3 Vs ⋅ α 2 ⋅ T ⋅ IL2max ⋅ L2 ⋅ 6 Vs ⋅ α ⋅ T ⋅ IL2max ⋅ L2 ⋅ - + ( ) - L2 2 ⎡ ⎢ ⎢ ⎣ ⎤ ⎥ ⎥ ⎦ 1

Diode Current

Ideff L1 m , f , ( ) IdeffCC L1 m , f , ( ) L1 L1limm f , ( ) > if IdeffCD L1 m , f , ( ) otherwise :
= IdeffCC L1 m , f , ( ) L 2 L1 m 2 ← α Vs m Vs m ⋅ Ve + ⋅ ← T 1 f ← Δi Ve L1 α ⋅ T ⋅ ← IL2max m P Ve α ⋅ 1 2 Δi ⋅ + ⎛ ⎜ ⎝ ⎞ ⎟ ⎠ ⋅ ← IL2min P Ve α ⋅ 1 2 Δi ⋅ - ⎛ ⎜ ⎝ ⎞ ⎟ ⎠ m ⋅ ← 1 3 3 1 2 ⋅ 1 - α + ( ) - Vs 2 α 2 ⋅ T 2 ⋅ 2 T 2 ⋅ Vs 2 ⋅ α ⋅ - 3 Vs ⋅ α ⋅ T ⋅ IL2max ⋅ L2 ⋅ + 3 T ⋅ Vs ⋅ IL2max ⋅ L2 ⋅ - T 2 Vs 2 ⋅ + 3 IL2max 2 ⋅ L2 2 ⋅ + L2 2 ⋅ ⎡ ⎢ ⎢ ⎣ ⎤ ⎥ ⎥ ⎦ 1 2 ⋅ := * IdeffCD L1 m , f , ( ) L 2 L1 m 2 ← α 2 L1 ⋅ f ⋅ Vs ⋅ I2 ⋅ Ve 2 ← T 1 f ← IL2max m Ve L1 α ⋅ T ⋅ ⎛ ⎜ ⎝ ⎞ ⎟ ⎠ ⋅ ← β α Ve Vs m ⋅ 1 + ⎛ ⎜ ⎝ ⎞ ⎟ ⎠ ⋅ ← 1 3 3 1 2 ⋅ β 3 T 2 ⋅ Vs 2 ⋅ 3 β 2 ⋅ T 2 ⋅ Vs 2 ⋅ α ⋅ - 3 β 2 ⋅ T ⋅ Vs ⋅ IL2max ⋅ L2 ⋅ - 3 β ⋅ T 2 ⋅ Vs 2 ⋅ α 2 ⋅ + 6 β ⋅ T ⋅ Vs ⋅ α ⋅ IL2max ⋅ L2 ⋅ + 3 β ⋅ IL2max 2 ⋅ L2 2 ⋅ Vs 2 α 3 ⋅ T 2 ⋅ - 3 Vs ⋅ α 2 ⋅ T ⋅ IL2max ⋅ L2 ⋅ - 3 α ⋅ IL2max 2 ⋅ L2 2 ⋅ - + L2 2 ⎛ ⎜ ⎜ ⎝ ⎞ ⎟ ⎟ ⎠ 1 2 ⋅ := MOSFET Current IT1eff L1 m , f , ( ) IT1effCC L1 m , f , ( ) L1 L1lim m f , ( ) > if IT1effCD L1 m , f , ( ) otherwise :
= IT1effCC L1 m , f , ( ) L 2 L1 m 2 ← α Vs m Vs m ⋅ ( ) V e + ⋅ ← T 1 f ← Δi Ve L1 α ⋅ T ⋅ ← IL1min P Ve α ⋅ 1 2 Δi ⋅ - ← 1 3 3 1 2 ⋅ α T 2 α 2 ⋅ Ve 2 ⋅ 3 T ⋅ α ⋅ Ve ⋅ IL1min ⋅ L1 ⋅ + 3 IL1min 2 ⋅ L1 2 ⋅ + L1 2 ⋅ ⎛ ⎜ ⎜ ⎝ ⎞ ⎟ ⎟ ⎠ 1 2 ⋅ := IT1effCD L1 m , f , ( ) L 2 L1 m 2 ← α 2 L1 ⋅ f ⋅ Vs ⋅ I2 ⋅ Ve 2 ← T 1 f ← IL2max m Ve L1 α ⋅ T ⋅ ⎛ ⎜ ⎝ ⎞ ⎟ ⎠ ⋅ ←

  applications): -PCB size [mm*mm*mm] : 100 * 160 * 41.6 -Output Power [W] : 70 -Frequency [kHz] : 20<F<45 -Input voltage [V] : 43<V in <137=> the design was achieved for 43 V (most constraint for the current), except for MOSFET voltage, taken from 137V -Output voltage [V] : 24 (0.6A), 12 (3A), 5 (0.5A), 3.3

Figure 1 .

 1 Figure 1. Half Bridge Flyback Structure.

Figure 2 .

 2 Figure 2. Flyback Waveforms for CCM and DCM.

Figure 3 .

 3 Figure 3. Capacitor surface vs rms current (blue dotted line), and the quadratic approximation (red line), for a 35V electrolytic serie.

Figure 4 .Figure 5 .

 45 Figure 4. Surface computed from area product (vs magnetizing inductance), and the actual cores which must be chosen

Figure 6 .Figure 7 .Figure 8 .

 678 Figure 6. Influence of switching frequency on total surface (transformer + output capacitor). Curve obtained for L1 = 52µH, m =3, Bpeak = 0,22 T)

Figure 10 .Figure 11 .Figure 13 .

 101113 Figure 10. Use of Core ETD34. Comparison between optimized result (without accounting for core reference discretization), adjustment for better surface, adjustment for better efficiency.

  Authorized licensed use limited to: IMAG -Universite Joseph Fourrier. Downloaded on February 10, 2009 at 05:50 from IEEE Xplore. Restrictions apply.

  Authorized licensed use limited to: IMAG -Universite Joseph Fourrier. Downloaded on February 10, 2009 at 05:50 from IEEE Xplore. Restrictions apply.

Authorized licensed use limited to: IMAG -Universite Joseph Fourrier. Downloaded on February 10, 2009 at 05:50 from IEEE Xplore. Restrictions apply.

ACKNOWLEDGMENT

The authors would like to thank Florian PAIRE, for his very good work on this subject during his thesis. It is unfortunate that he finally did not choose to go further in the research activity. Good luck in industry !

APPENDIX: EXAMPLE OF ANALYTICAL FORMULAS USED FOR CORE SELECTION AND OUTPUT CAPACITOR RMS CURRENT CCM-DCM limit determination


Louis Potier

Maud François

Dured Dardari

Marilyne Feron

Narimène Belhatem

Estelle Nobecourt-Dupuy

Manuel Dolz

Lyse Bordier

Comparison of a new versus standard removable offloading device in patients with neuropathic diabetic foot ulcers: a French national, multicentre, open-label randomized, controlled trial


Laurence Rideau
email: laurence.rideau@inria.fr

Bernard Paul

Xavier Leroy
email: xavier.leroy@inria.fr

B P Serpette
email: bernard.serpette@inria.fr

Tilting at windmills with Coq: formal verification of a compilation algorithm for parallel moves

Keywords: Parallel move, Parallel assignment, Compilation, Compiler correctness

This article describes the formal verification of a compilation algorithm that transforms parallel moves (parallel assignments between variables) into a semanticallyequivalent sequence of elementary moves. Two different specifications of the algorithm are given: an inductive specification and a functional one, each with its correctness proofs. A functional program can then be extracted and integrated in the Compcert verified compiler.

Introduction

Parallel assignment is a programming construct found in some programming languages (Algol 68, Common Lisp) and in some compiler intermediate languages (the RTL intermediate language of the GNU Compiler Collection). A parallel assignment is written (x 1 , . . . , xn) := (e 1 , . . . , en), where the x i are variables and the e i are expressions possibly involving the variables x i . The semantics of this parallel assignment is to evaluate the expressions e 1 , . . . , en, then assign their respective values to the variables x 1 , . . . , xn. Since the left-hand side variables can occur in the right-hand side expressions, the effect of a parallel assignment is, in general, different from that of the sequence of elementary assignments x 1 := e 1 ; . . . ; xn := en. Welch [START_REF] Welch | Parallel assignment revisited[END_REF] gives examples of uses of parallel assignments.

Compiling a parallel assignment instruction amounts to finding a serialisation -a sequence of single assignments x ′ 1 = e ′ 1 ; . . . ; x ′ m = e ′ m -whose effect on the variables x i and on other program variables is the same as that of the source-level parallel assignment. Since parallel assignment includes permutation of variables (x 1 , x 2 ) = (x 2 , x 1 ) as a special case, the generated sequence of elementary assignments cannot, in general, operate in-place over the x i : additional storage is necessary under the form of temporary variables. A trivial compilation algorithm, outlined by Welch [START_REF] Welch | Parallel assignment revisited[END_REF], uses n temporaries t 1 , . . . , tn, not present in the original program: t 1 := e 1 ; . . . ; tn := en; x 1 := t 1 ; . . . ; xn := tn As shown by the example (x 1 , x 2 ) = (x 2 , x 1 ), it is possible to find more efficient sequences that use fewer than n temporaries.

Finding such sequences is difficult in general: Sethi [START_REF] Sethi | A note on implementing parallel assignment instructions[END_REF] shows that compiling a parallel assignment over n variables using at most K temporaries, where K is a constant independent of n, is an NP-hard problem. However, there exists a family of parallel assignments for which serialisation is computationally easy: parallel assignments of the form (x 1 , . . . , xn) := (y 1 , . . . , yn), where the right-hand sides y i are restricted to be variables (either the x i variables or other variables). We call these assignments parallel moves. They occur naturally in compilers when enforcing calling conventions [START_REF] Appel | Compiling with continuations[END_REF]. May [START_REF] May | The parallel assignment problem redefined[END_REF] shows another example of use of parallel moves in the context of machine code translation. It is a folklore result that parallel moves can be serialised using at most one temporary register, and in linear time [START_REF] May | The parallel assignment problem redefined[END_REF].

The purpose of this paper is to formalize a compilation algorithm for parallel moves and mechanically verify its semantic correctness, using the Coq proof assistant [START_REF]Coq development team: The Coq proof assistant[END_REF][START_REF] Bertot | Interactive Theorem Proving and Program Development -Coq'Art: The Calculus of Inductive Constructions[END_REF]. This work is part of a larger effort, the Compcert project [START_REF] Leroy | Formal certification of a compiler back-end, or: programming a compiler with a proof assistant[END_REF][START_REF] Blazy | Formal verification of a C compiler front-end[END_REF][START_REF] Bertot | A structured approach to proving compiler optimizations based on dataflow analysis[END_REF], which aims at mechanically verifying the correctness of an optimizing compiler for a subset of the C programming language. Every pass of the Compcert compiler is specified in Coq, then proved to be semantics-preserving: the observable behavior of the generated code is identical to that of the source code.

The parallel move compilation algorithm is used in the pass that enforces calling conventions for functions. Consider a source-level function call f (e 1 , . . . , en). Earlier compiler passes produces intermediate code that computes the values of the arguments e 1 , . . . , en and deposits them in locations l 1 , . . . , ln. (Locations are either processor registers or stack slots.) The function calling conventions dictate that the separatelycompiled function f expects its parameters in conventional locations l ′ 1 , . . . , l ′ n determined by the number and types of the parameters. The register allocation phase is instructed to prefer the locations l ′ 1 , . . . , l ′ n for the targets of e 1 , . . . , en, but such preferences cannot always be honored. Therefore, the pass that enforces calling conventions must, before the call, insert elementary move instructions that perform the parallel move (l ′ 1 , . . . , l ′ n ) := (l 1 , . . . , ln). Only two hardware registers (one integer register, one floating-point register) are available at this point to serve as temporaries. Therefore, the naive compilation algorithm for parallel moves will not do, and we had to implement and prove correct the space-efficient algorithm.

The formal specification and correctness proof of this compilation algorithm is challenging. Indeed, this was one of the most difficult parts of the whole Compcert development. While short and conceptually clear, the algorithm we started with (described section 3) is very imperative in nature. The underlying graph-like data structure, called windmills in this paper, is unusual. Finally, the algorithm involves non-structural recursion. We show how to tackle these difficulties by progressive refinement from a high-level, nondeterministic, relational specification of semantics-preserving transformations over windmills.

The remainder of this paper is organized as follows. Section 2 defines the windmill structure. Section 3 shows the folklore, imperative serialisation algorithm that we used as a starting point. Two inductive specifications of the algorithm follow, a nondeterministic one (section 4), and a deterministic one (section 5), with the proofs that they are correct and consistent. Section 6 derives a functional implementation from these specifications and proves consistency with the inductive specifications, termination, and correctness. Section 7 proves additional syntactic properties of the result of the compilation function. In section 8, the correctness result of section 6 is extended to the case where variables can partially overlap. Concluding remarks are presented in section 9.

The complete, commented source for the Coq development presented here is available at http://gallium.inria.fr/ ~xleroy/parallel-move/.

Definitions and notations

An elementary move is written (s → d), where the source register s and the destination register d range over a given set R of registers. Parallel moves as well as sequences of elementary moves are written as lists of moves (s 1 → d 1 ) • • • (sn → dn). The • operator denotes the concatenation of two lists. We overload it to also denote prepending a move in front of a list, (s → d) • l, and appending a move at the end of a list, l • (s → d). The empty list is written ∅.

We assume given a set T ⊆ R of temporary registers: registers that are not mentioned in the initial parallel move problem and that the compiler can use to break cycles. We also assume given a function T : R → T that associates to any register r a temporary register T (r) appropriate for saving the value of r when breaking a cycle involving r. In the simplest case, only one temporary tmp is available and T is the constant function T (r) = tmp. In more realistic cases, architectural or typing constraints may demand the use of several temporaries, for instance one integer temporary to move integer or pointer values, and one floating-point temporary to move floating-point values. In this example, T (r) selects the appropriate temporary as a function of the type of r.

A parallel move (s 1 → d 1 ) • • • (sn → dn) is well defined only if the destination registers are pairwise distinct: d i = d j if i = j. (If a register appeared twice as a destination, its final value after the parallel move would not be uniquely defined.) We call such parallel moves windmills.

Definition 1 (Windmills) A parallel move µ is a windmill if, for all l 1 , s i , d i , l 2 , s j , d j and l 3 ,

µ = l 1 • (s i → d i ) • l 2 • (s j → d j ) • l 3 ⇒ d i = d j
The name "windmill" comes from the graphical shape of the corresponding transfer relation. We can view a parallel move as a transfer relation. Each move (s i → d i ) corresponds to an edge in the graph of this relation. A parallel move is a windmill if every register has at most one predecessor for the transfer relation. Although this property is similar to the specification of forests (set of disjoint trees), it allows cycles such as (r 1 → r 2 ) • (r 2 → r 1 ). This is unlike a tree, where, by definition, there exists a unique element -the root -that has no predecessor.

The graph of the relation corresponding to a windmill is composed of cycles -the axles -whose elements are the roots of trees -the blades. Figure 1 figure shows a set of 4 windmills: the general case, the special case of a tree, a simple cycle with four registers, and the special case of a self-loop. There are two special cases of parallel move problems where serialization is straightforward. In the case of a simple cycle, i.e. an axle without any blade, the transfer relation is:

(

r 1 → r 2 ) • (r 2 → r 3 ) • • • (r n-1 → rn) • (rn → r 1 )
Serialization is done using a single temporary register t = T (r 1 ):

t := r 1 ; r 1 := rn; rn := r n-1 ; . . . ; r 3 := r 2 ; r 2 := t.

The other easy case corresponds to a transfer relation that is a tree, such as for instance

(r 1 → r 2 ) • (r 1 → r 3 ) • (r 2 → r 4 )
In this case, serialization corresponds to enumerating the edges in a bottom-up topological order: r 4 := r 2 ; r 2 := r 1 ; r 3 := r 1 .

C. May [START_REF] May | The parallel assignment problem redefined[END_REF] describes an algorithm that generalizes these two special cases. This algorithm follows the topology of the transfer relation. First, remove one by one all the edges that have no successors, emitting the corresponding sequential assignments in the same order. (In windmill terminology, this causes the blades to disappear little by little.) Eventually, all that remains are simple, disjoint cycles (windmill axles) which can be serialized using one temporary as described above.

We now consider a variant of this algorithm that processes blades and axles simultaneously, in a single pass. The algorithm is given in figure 2 in Caml syntax [START_REF] Leroy | The Objective Caml system. Software and documentation available[END_REF]. It can be read as pseudo-code knowing that a.(i) refers to the i-th element of array a.

It takes as arguments two arrays src and dst containing respectively the source registers s 1 , . . . , sn and the target registers d 1 , . . . , dn, as well as the temporary-generating function tmp. The elementary moves produced by serialization are successively printed using the C-like printf function.

The algorithm implements a kind of depth-first graph traversal using the move_one function that takes an edge (src i → dst i ) of the transfer relation as an argument. In line 9 and 10, all successors of dst i are handled. Line 17 handles the case of an already analysed edge. In the case of line 12, it is a simple recursive call. In the case of line 14, a cycle is discovered and a temporary register is used to break it. When exiting this loop on line 19, all the nodes that can be reached by dst i have been analysed, the edge (src i → dst i ) is serialized and marked as analyzed.

When a cycle is discovered, the stack of active calls to move_one correspond to the edges ((rn → r 1 ), . . . , (r 2 → r 3 ), (r 1 → r 2 )) and, at line 14, the edge (r 1 → r 2 ) is analysed again. The side effect of line 16 thus necessarily acts on the edge that started the recursion of the move_one function, i.e. the edge at the bottom of the stack. The main loop, lines 23 to 25, ensures that all edges are analyzed at least once.

Nondeterministic specification

The algorithm in figure 2 does not lend itself easily to program proof: first, it is written imperatively, making it quite removed from a mathematical specification; second, it commits to a particular strategy for solving the problem, obscuring the essential invariants for the correctness proof. In this section, we develop an abstract specification of the steps of the algorithm, and show that these steps preserve semantics. This specification is not deterministic: it does not constrain which step must be taken in a given state.

In the algorithm of figure 2, notice that every edge of the transfer relation begins in the state To_move (line 5), then takes the state Being_moved (line 8), and finally reaches the state Moved (line 21). Rather than associating a status to each edge, we will represent the current state of the compilation as three disjoint lists of edges, each list containing edges having the same status. The state is therefore a triple (µ, σ, τ ) of lists of edges: µ is the to-move list, σ the being-moved list and τ the moved list.

Each step of the algorithm will either extract an element from the to-move list µ and add it to the being-moved list σ, or remove an element of the latter and add it to the moved list τ . The to-move and being-moved lists are used as work lists; the algorithm will stop when both are empty.

The being-moved list σ is used as a stack, simulating the recursive calls to the move_one function in the imperative algorithm. In addition to pushing and popping moves from the beginning of σ, the last element of σ can also be modified when a cycle is discovered.

The last component of the state, the moved list τ , is used to accumulate the sequence of elementary moves that the imperative algorithm emits using the printf function. Moves are successively added to the front of the list τ . Therefore, the elementary moves listed in τ are to be executed from right to left.

Inference rules

The inference rules below define a rewriting relation ⊲ between states (µ, σ, τ ). Each rule describes a step that the compilation algorithm is allowed to take. A run of compilation is viewed as a sequence of rewrites from the initial state (µ, ∅, ∅) to a final state (∅, ∅, τ ), where µ is the parallel move problem we set out to compile, and reverse(τ ) is the sequence of elementary moves generated by this compilation run.

(µ 1 • (r → r) • µ 2 , σ, τ ) ⊲ (µ 1 • µ 2 , σ, τ ) [Nop]
The first rule deals with the case where the transfer relation has an edge (r → r) whose source and destination are identical. This case is specially handled at line 7 of the imperative algorithm. Note that in the imperative algorithm, this edge is not annotated as Moved and keeps the status To_move until the end of the algorithm. Nevertheless this edge cannot result from a recursive call of the function move_one because, in this case, the caller would correspond to an edge (s → r) and that would violate the fact that the transfer relation is a windmill: indeed, there would exist two different edges with the same destination. It is therefore valid to move the test of line 7 up to the level of the main loop at line 24.

(µ 1 • (s → d) • µ 2 , ∅, τ ) ⊲ (µ 1 • µ 2 , (s → d), τ ) [Start]
The [Start] rule corresponds to the first call to the move_one function at line 24. We know that in this case no edge has the status Being_Moved and this rule will thus be the only one to handle the case where the being-moved list is empty.

(µ 1 • (d → r) • µ 2 , (s → d) • σ, τ ) ⊲ (µ 1 • µ 2 , (d → r) • (s → d) • σ, τ ) [Push]
The [Push] rule corresponds to the recursive call at line 13. If the edge being analysed is (s → d) (i.e. the top of the being-moved list) and if there exists a successor (d → r) in the to-move list, the latter is transferred to to the top of the being-moved stack.

(µ, σ • (s → d), τ ) ⊲ (µ, σ • (T (s) → d), (s → T (s)) • τ ) [Loop]
The [Loop] rule corresponds to the special case at lines 15 and 16 where a cycle is discovered. This rule is of more general use. Indeed, it is not essential to check the presence of a cycle before inserting a transfer using a temporary register. Thus, lines 15 and 16 can also be moved up to the level of the main loop (line 24). The fact that one uses the temporary register only in the case of a cycle must be regarded as an optimization. The crucial issue is to make sure that a transfer through a temporary register must be used whenever a cycle arises. This is ensured by the next rule.

NoRead(µ, dn) ∧ dn = s 0 (µ, (sn → dn) • σ • (s 0 → d 0 ), τ ) ⊲ (µ, σ • (s 0 → d 0 ), (sn → dn) • τ ) [Pop]
The [Pop] rule corresponds to returning from a recursive call to the function move_one. The first premise of this rule, NoRead(µ, dn), is formally defined as

NoRead(µ, dn) def = ∀µ 1 , s, µ 2 , µ = µ 1 • (s → d) • µ 2 ⇒ s = dn.
This premise checks that the edge (sn → dn) under study no longer has its successor dn in the to-move list. It therefore prevents the [Pop] rule from being used if the value of dn is still needed. The second premise, dn = s 0 , makes sure that the [Pop] rule cannot be used if dn participates in a cycle, forcing the use of the [Loop] rule instead in the case of a cycle.

NoRead(µ, dn) (µ, (s → d), τ ) ⊲ (µ, ∅, (s → d) • τ ) [Last]
The [Last] rule corresponds to returning from the main loop at line 24. It is a special case of the [Pop] rule. As in the special case of the [Nop] rule, observe that a to-move list of the form ((r → r)) can either be eliminated by the [Nop] rule, or rewritten to itself in two steps ([Start] then [Last]), or rewritten to ((T (r) → r) • (r → T (r))) using a temporary register (rules [Start] then [Loop] then [Last]). These three results are equally valid.

Well-formedness invariant

In preparation for proving the semantic correctness of the rewriting rules, we first define a well-formedness property that acts as a crucial invariant in this proof.

Definition 2 (Invariant) A triple (µ, σ, τ ) is well-formed, written ⊢ (µ, σ, τ ), if and only if:

1. µ • σ is a windmill, in the sense of definition 1. 2. The µ list does not contain temporary registers: for all µ 1 , s, d, µ 2 ,

µ = µ 1 • (s → d) • µ 2 ⇒ (s / ∈ T ∧ d / ∈ T ).
3. The σ list can only use a temporary register as the source of its last edge: for all

σ 1 , s 0 , d 0 , σ = σ 1 • (s 0 → d 0 ) ⇒ d 0 / ∈ T
and for all σ 2 , s, d, σ 3 ,

σ 1 = σ 2 • (s → d) • σ 3 ∧ σ 3 = ∅ ⇒ (s / ∈ T ∧ d / ∈ T ). 4. The σ list is a path: σ = (r n-1 → rn) • • • (r 2 → r 3 ) • (r 1 → r 2 )
for some registers r 1 , . . . , rn.

Notice that if µ is a windmill and does not use any temporary register, then the initial triple (µ, ∅, ∅) is well-formed.

Lemma 1 (The invariant is preserved) The rewriting rules transform a wellformed triple into a well-formed triple. If S 1 ⊲ S 2 and ⊢ S 1 , then ⊢ S 2 .

Proof By case analysis on the rule that concludes S 1 ⊲ S 2 . For S 1 = (µ, σ, τ ), only the [Push] rule adds an element to σ, but the edge thus added extends the path already present in σ.

Dynamic semantics for assignments

To state semantic preservation for the rewriting relation, we need to give dynamic semantics to the parallel moves µ and the sequential moves σ and τ occurring in intermediate states. Let V be the set of run-time values for the language. The run-time state of a program is represented as an environment ρ : R → V mapping registers to their current values. Assigning value v to register r transforms the environment ρ into the environment ρ[r ← v] defined by

ρ[r ← v] = r → v r ′ → ρ(r ′ ) if r ′ = r.
(We assume that assigning to a register r preserves the values of all other registers r ′ , or in other words that r does not overlap with any other register. We will revisit this hypothesis in section 8.)

The run-time effect of a parallel move µ is to transform the current environment ρ in the environment [[µ]] // (ρ) defined as:

[[(sn → dn) • • • (s 0 → d 0 )]] // (ρ) = ρ[d 0 ← ρ(s 0 )] . . . [dn ← ρ(sn)]
In this definition parentheses are omitted, as we require that µ is a windmill. The following lemma, showing that the order of moves within µ does not matter, is intensively used in our proofs:

Lemma 2 (Independence) If µ = µ 1 • (s → d) • µ 2 is a windmill, then [[µ]] // (ρ) = [[(s → d) • µ 1 • µ 2 ]] // (ρ)
Proof By induction on µ 1 . The base case µ 1 = ∅ is trivial. For the inductive step, we need to prove that the first two elements of µ 1 can be exchanged:

(ρ[d 0 ← ρ(s 0 )])[d 1 ← ρ(s 1 )] = (ρ[d 1 ← ρ(s 1 )])[d 0 ← ρ(s 0 )].
The windmill structure of µ 1 implies that d 0 = d 1 , and therefore this equality is verified.

The run-time effect of a sequence of elementary moves τ , performed from left to right, is defined by:

[[∅]]→(ρ) = ρ [[(s → d) • τ ]]→(ρ) = [[τ ]]→(ρ[d ← ρ(s)])
The sequences of elementary moves τ appearing in the states of the rewriting relation are actually to be interpreted from right to left, or equivalently to be reversed before execution. It is therefore useful to define directly the semantics of a sequence of elementary moves τ performed from right to left: Proof Easy induction over τ . Definition 3 (Equivalent environments) We say that two environments ρ 1 and ρ 2 are equivalent, and we write ρ 1 ≡ ρ 2 , if and only if all non-temporary registers have the same values in both environments: Notice that for initial states, we have Proof By case analysis on the rule used to derive S 1 ⊲ S 2 . We write S 1 = (µ, σ, τ ).

[[∅]]←(ρ) = ρ [[(s → d) • τ ]]←(ρ) = ρ ′ [d ← ρ ′ (s)] where ρ ′ = [[τ ]]←(ρ)
ρ 1 ≡ ρ 2 def = ∀r / ∈ T , ρ 1 (r) = ρ 2 (r).
[[(µ, ∅, ∅)]](ρ) = [[µ]] // (ρ), while for final states, we have [[(∅, ∅, τ )]](ρ) = [[τ ]]←(ρ) = [[reverse(τ )]]→(ρ).
[(sn → dn) • µ • σ]] // ([[τ ]]←(ρ)) = [[µ • σ]] // ([[(sn → dn) • τ ]]←(ρ))
This equality holds provided that register dn does not appear as a source in µ • σ. For µ, this is ensured by the first premise. For σ, this follows by induction from the fact that σ is a path. The base case comes from the premise dn = s 0 . The inductive case is provided by the windmill structure of σ. Proof By induction on the number of steps.

As a corollary, we obtain the main semantic preservation theorem of this section.

Theorem 1 (Correctness of ⊲ * ) If µ is a windmill containing no temporary register, and if the triple (µ, ∅, ∅) can be rewritten into (∅, ∅, τ ) then the parallel execution of µ is equivalent to the sequential execution of reverse(τ ):

(µ, ∅, ∅) ⊲ * (∅, ∅, τ ) ⇒ [[µ]] // (ρ) ≡ [[reverse(τ )]]→(ρ).

Deterministic specification

The next step towards an effective algorithm consist in determinising the inductive rules of section 4 by ensuring that at most one rule matches a given state, and by specifying which edge to extract out of the to-move list in the rules [Nop], [Push] and [Start].

((r → r) • µ, ∅, τ ) ֒→ (µ, ∅, τ ) [Nop ′ ] s = d ((s → d) • µ, ∅, τ ) ֒→ (µ, (s → d), τ ) [Start ′ ]
The first two rules treat the case of an empty being-moved list and consider only the first element on the left of the to-move list µ.

NoRead(µ 1 , d) (µ 1 • (d → r) • µ 2 , (s → d) • σ, τ ) ֒→ (µ 1 • µ 2 , (d → r) • (s → d) • σ, τ ) [Push ′ ]
The [Push ′ ] rule treats the case in which the analysed edge has a successor in the µ list. It forces the algorithm to consider the leftmost successor found in µ.

NoRead(µ, r 0 ) (µ, (s → r 0 ) • σ • (r 0 → d), τ ) ֒→ (µ, σ • (T (r 0 ) → d), (s → r 0 ) • (r 0 → T (r 0 )) • τ ) [LoopPop] NoRead(µ, dn) ∧ dn = s 0 (µ, (sn → dn) • σ • (s 0 → d 0 ), τ ) ֒→ (µ, σ • (s 0 → d 0 ), (sn → dn) • τ ) [Pop ′ ]
These two rules treat the case where the analysed edge has no successor in the tomove list, and the being-moved list contains at least two elements. The [LoopPop] rule is the [Pop] rule in the case of a cycle. This rule, unlike the corresponding nondeterministic rules, pops the analysed edge. This ensures that every rule moves at least one edge. The termination proof in section 6 uses this fact.

NoRead(µ, d) (µ, (s → d), τ ) ֒→ (µ, ∅, (s → d) • τ ) [Last ′ ]
The [Last ′ ] rule treats the final case where the being-moved list contains only one element.

Since these deterministic rules are instances or combinations of the nondeterministic ones, the following two lemmas are trivial.

Lemma 6 (Inclusion

֒→ ⊆ ⊲ * ) If S 1 ֒→ S 2 , then S 1 ⊲ * S 2 .
Proof By case analysis. The [LoopPop] case uses the transitivity of ⊲ * .

Lemma 7 (Inclusion

֒→ * ⊆ ⊲ * ) If S 1 ֒→ * S 2 , then S 1 ⊲ * S 2 .
Proof By induction on the number of steps.

Notice that the deterministic rules implement a strategy that is slightly different from that of the imperative algorithm. Indeed, during the imperative algorithm, when a temporary register is used to break a cycle, the analysed edge can still have a successor. This is not the case for the [LoopPop] rule.

Semantic preservation for the deterministic rules follows immediately from theorem 1 and lemma 7. However, to obtain an algorithm, we still need to prove that the rules are indeed deterministic and that a normal form (i.e. the final state (∅, ∅, τ )) always exists. To do so, we now give a functional presentation of the deterministic rules.

The functional algorithm

From the deterministic rules in section 5, it is easy to build a function stepf that performs one step of rewriting. Compiling a parallel move problem, then, corresponds to iterating stepf until a final state is reached:

pmov S = match S with | ( ∅ , ∅ , _) ⇒ S | _ ⇒ pmov (stepf S) end
However, such a function definition is not accepted by Coq, because it is not structurally recursive: the recursive call is performed on stepf(S) and not on a structural subterm of S. To define the pmov function, we will use the Coq command Function, which provides a simple mechanism to define a recursive function by well-founded recursion [START_REF] Balaa | Fonctions récursives générales par itération en théorie des types[END_REF][START_REF] Barthe | Defining and reasoning about recursive functions: a practical tool for the Coq proof assistant[END_REF]. To this end, we first define the stepf function that executes one computation step, then a measure function which will be used to justify termination, and finally the theorem establishing that the measure decreases at each recursive call.

• ∅ ) l ( * s = d; rule [ Start ] * ) | State t ((s, d) • b) l ⇒ match split_move t d with | Some (t1, r, t2) ⇒ ( * t = t 1 • (d → r) • t 2 * ) State (t1 • t2) ( * rule [Push] * ) ((d, r) • (s, d) • b) l | None ⇒ match b with | ∅ ⇒ State t ∅ ((s, d) • l) ( * rule [Last] * ) | _ ⇒ if is_last_source d b ( * check if b = • (d → ) * ) then State t ( * rule [LoopPop] * ) (replace_last_source (temp d) b) ((s, d) • (d, temp d) • l) else State t b ((s, d) • l) ( * rule [Pop] * ) end end end.
Fig. 3 The one-step rewriting function

The one-step rewriting function

We define the one-step rewriting function stepf in a way that closely follows the deterministic rules of section 5. It takes a state S as argument and returns a state S ′ such that S ֒→ S ′ . The function, written in Coq syntax, is defined by case analysis in figure 3.

The first case (line 3) does not correspond to any of the inductive rules: it detects a final state (∅, ∅, τ ) and returns it unchanged. The other cases correspond to the deterministic rules indicated in comments.

The reg eq function decides whether two registers are equal or not. The split move function takes as arguments a windmill t and a register d. If this register is the source of an edge from list t, the function returns this edge (d, ) and the two remaining sub-lists. This breaks the t list into t 1 • (d, r) • t 2 like the [Push] rule does.

Finally, the replace last source function takes as argument a list b of edges and a register r, and replaces the source of the last edge of b with r: hb

• (s → d) becomes hb • (t → d), in accordance with the [LoopPop] rule.
Since the definition of the stepf function is close to the deterministic specification, the following theorem is easily proved: Lemma 8 ( Compatibility of stepf and ֒→) S ֒→ stepf(S) if S is not a final state (i.e. not of the form (∅, ∅, τ )).

Proof By case analysis on the shape of S and application of the corresponding rules for the ֒→ relation.

The general recursive function

The general recursive function consists in iterating the stepf function. To ensure termination of this function, we need a nonnegative integer measure over states that decreases at each call to the stepf function, except in the final case (∅, ∅, τ ). Examination of the deterministic rewriting rules and of the lengths of the to-move and being-moved lists reveals that:

-either an edge is removed from the to-move list and and the being-moved list is unchanged (rule [Nop]); -or an edge is transferred from the to-move list to the being-moved list (rules [Start] and [Push]); -or the to-move list remains the same while an edge is transferred from the beingmoved list to the moved list (rules [LoopPop], [Pop], and [Last]).

Therefore, either one of the to-move or being-moved lists loses one element, or one element is transferred from the former to the latter. Decrease is achieved by giving more weight to the to-move edges, as the following meas function does:

Definition 5 (The triple measure) meas(µ, σ, τ ) = 2 × length(µ) + length(σ).

Lemma 9 (Measure decreases with ֒→) If S 1 ֒→ S 2 , then meas(S 2 ) < meas(S 1 ).

Proof By case analysis on the rules of the ֒→ relation and computation of the corresponding measures.

Combining this lemma with lemma 8 (compatibility of stepf with ֒→), we obtain:

Lemma 10 (Measure decreases with stepf) If S is not a final state, i.e. not of the form (∅, ∅, τ ), then meas(stepf(S)) < meas(S).

We can then define the iterate of stepf using the Function command of Coq version 8:

Function pmov (S: State) {measure meas st} : state := if final_state S then S else pmov (stepf S).

where final state is a boolean-valued function returning true if its argument is of the form (∅, ∅, τ ) and false otherwise. Coq produces a proof obligation requiring the user to show that the recursive call to pmov is actually decreasing with respect to the meas function. This obligation is trivially proved by lemma 10. Coq then generates and automatically proves the following functional induction principle that enables us to reason over the pmov function:

(∀S, final state(S) = true ⇒ P (S, S)) ∧ (∀S, final state(S) = false ∧ P (stepf(S), pmov(stepf(S))) ⇒ P (S, pmov(stepf(S))) ⇒ (∀S, P (S, pmov(S)))

Using this induction principle and lemma 8, we obtain the correctness of pmov with respect to the deterministic specification.

Lemma 11 For all initial states S, pmov(S) is a final state (∅, ∅, τ ) such that S ֒→ * (∅, ∅, τ ).

The compilation function

To finish this development, we define the main compilation function, taking a parallel move problem as input and returning an equivalent sequence of elementary moves. Here is an alternate formulation of this theorem that can be more convenient to use. Finally, we used the Coq extraction mechanism [START_REF] Letouzey | A new extraction for Coq[END_REF] to automatically generate executable Caml code from the definition of the parmove function, thus obtaining a verified implementation of the parallel move compilation algorithm that can be integrated in the Compcert compiler back-end.

Syntactic properties of the compilation algorithm

In this section, we show a useful syntactic property of the sequences of moves generated by the parmove compilation function: the registers involved in the generated moves are not arbitrary, but either appear in the initial parallel move problem, or are results of the temporary-generating function T .

More formally, let µ 0 = (s 1 → d 1 ) • • • (sn → dn) be the initial parallel move problem. We define a property P (s → d) of elementary moves (s → d) by the following inference rules:

(s → d) ∈ µ 0 P (s → d) P (s → d) P (T (s) → d) P (s → d) P (s → T (s))
8 Extension to overlapping registers So far, we have assumed that two distinct registers never overlap: assigning one does not change the value of the other. This is not always the case in practice. For instance, some processor architectures expose hardware registers that share some of their bits. In the IA32 architecture, for example, the register AL refers to the low 8 bits of the 32-bit register EAX. Assigning to AL therefore modifies the value of EAX, and conversely.

Overlap also occurs naturally when the "registers" manipulated by the parallel move compilation algorithm include memory locations, such as variables that have been spilled to memory during register allocation, or stack locations used for parameter passing. For example, writing a 32-bit integer at offset δ in the stack also changes the values of the stack locations at offsets δ + 1, δ + 2 and δ + 3.

It is not straightforward to generalize the parallel move compilation algorithm to the case where source and destination registers can overlap arbitrarily. We will not attempt to do so in this section, but set out to show a weaker, but still useful result: the unmodified parallel move algorithm produces correct sequences of elementary assignments even if registers can in general overlap, provided destinations and sources do not overlap.

Formalising overlap

In the non-overlapping case, two registers r 1 and r 2 are either identical r 1 = r 2 or different r 1 = r 2 . When registers can overlap, we have three cases: r 1 and r 2 are either identical (r 1 = r 2 ) or completely disjoint (written r 1 ⊥ r 2 ) or different but partially overlapping (written r 1 ⊲⊳ r 2 ).

We assume given a disjointness relation ⊥ over R × R, which must be symmetric and such that r 1 ⊥ r 2 ⇒ r 1 = r 2 . We define partial overlap r 1 ⊲⊳ r 2 as (r 1 = r 2 ) ∧ ¬(r 1 ⊥ r 2 ).

In the non-overlapping case, the semantics of an assignment of value v to register r is captured by the update operation ρ[r ← v], characterized by the "good variable" property:

ρ[r ← v] = r → v r ′ → ρ(r ′ ) if r ′ = r.
To account for the possibility of overlap, we define the weak update operation ρ[r ⇐ v] by the following "weak good variable" property:

ρ[r ⇐ v] = r → v r ′ → ρ(r ′ ) if r ′ ⊥ r r ′ → undefined if r ′ ⊲⊳ r.
As suggested by the fatter arrow ⇐, weak update sets the target register r to the specified value v, but causes "collateral damage" on registers r ′ that partially overlap with r: their values after the update are undefined. Only registers r ′ that are disjoint from r keep their old values.

Using weak update instead of update, the semantics of a sequence τ of elementary moves becomes

[[∅]]⇒(ρ) = ρ [[(s → d) • τ ]]⇒(ρ) = [[τ ]]⇒(ρ[d ⇐ ρ(s)])

Effect of overlap on the parallel move algorithm

In this section, we consider a parallel move problem µ = (s 1 → d 1 ) • • • (sn → dn) and assume that the sources s 1 , . . . , sn and the destinations d 1 , . . . , dn satisfy the following hypotheses:

1. No temporaries: s i ⊥ t and d i ⊥ t for all i, j and t ∈ T . 2. Destinations are pairwise disjoint:

d i ⊥ d j if i = j.
3. Sources and destinations do not partially overlap: s i = d j ⇒ s i ⊥ d j for all i, j. 4. Distinct temporaries do not partially overlap: t 1 = t 2 ⇒ t 1 ⊥ t 2 for all t 1 , t 2 ∈ T .

As we show below, these hypotheses ensure that assigning a destination or a temporary r preserves the values of all sources, destinations and temporaries other than r.

These hypotheses are easily satisfied in our application scenario within the Compcert compiler. Hardware registers never partially overlap in the target architecture (the PowerPC processor). Properties of the register allocator ensure that the only possibility for partial overlap is between stack locations used as destinations for parameter passing, but such overlap is avoided by the calling conventions used.

Since r 1 ⊥ r 2 ⇒ r 1 = r 2 , hypothesis (1) ensures that no temporary occurs in sources and destinations, and hypothesis (2) ensures that µ is a windmill. Therefore, the initial state (µ, ∅, ∅) is well-formed.

We now set out to prove a correctness result for the sequence of elementary moves τ = parmove(µ) produced by the parallel move compilation function. Namely, we wish to show that the final values of the destinations d i are the initial values of the sources s i , and that all registers disjoint from the destinations and from the temporaries keep their initial values. To this end, we define the following relation ∼ = between environments:

ρ 1 ∼ = ρ 2 def = (∀r / ∈ D, ρ 1 (r) = ρ 2 (r))
where D is the set of registers that partially overlap with one of the destinations or one of the temporaries: In other words, ρ 1 ∼ = ρ 2 holds if ρ 1 and ρ 2 assign the same values to registers, except perhaps those registers that could be set to an undefined value as a side-effect of assigning one of the destinations or one of the temporaries.

Lemma 16 r / ∈ D if r is one of the destinations d i , or one of the sources s i , or a temporary t ∈ T .

Proof Follows from hypotheses (1) to (4).

Using the relation ∼ =, we can relate the effect of executing moves using normal, overlap-unaware update and weak, overlap-aware update. Proof By structural induction on τ , using lemma 17. Let r be a register disjoint from the destinations d i and from the temporaries T . By definition of D, r / ∈ D, therefore ρ ′ (r) = ρ 1 (r). Moreover, ρ 1 (r) = ρ(r) since r / ∈ {d 1 , . . . , dn} ∪ T . The expected result follows.

Conclusions

Using the Coq proof assistant, we have proved the correctness and termination of a compilation algorithm that serialises parallel moves. The main difficulty of this development was to find an appropriate set of atomic transitions between intermediate states of the algorithm, and prove that they preserve semantics; once this is done, the proof of the algorithm proper follows easily by refinements. The Coq development is relatively small: 580 lines of specifications and 610 lines of proof scripts.

Fig. 1

 1 Fig. 1 Examples of windmills

  Fig.2A one-pass, imperative algorithm to compile parallel moves

Lemma 3 (

 3 Reversed sequential execution) For all sequences τ of elementary moves, [[τ ]]←(ρ) = [[reverse(τ )]]→(ρ).

Definition 4 (

 4 Semantics of a triple) The dynamic semantics of the triple (µ, σ, τ ) corresponds to first executing τ sequentially from right to left, then executing µ • σ in parallel: [[(µ, σ, τ )]](ρ) = [[µ • σ]] // ([[τ ]]←(ρ)).

4. 4 Correctness

 4 Lemma 4 (One-step semantic preservation) The rewriting rules preserve the semantics of well-formed triples: if S 1 ⊲ S 2 and ⊢ S 1 , then [[S 1 ]](ρ) ≡ [[S 2 ]](ρ) for all environments ρ.

-

  Rule [Nop]: use the fact that ρ[r ← ρ(r)] = ρ. -Rules [Start] and [Push]: use the order independence lemma 2. -Rule [Loop]: exploit the fact that µ and σ do not use the temporary register introduced by the rule. -Rule [Pop]: the expected result follows from [

-

  Rule [Last]: special case of rule [Pop]. This lemma is easily extended to ⊲ * , the reflexive transitive closure of ⊲: Lemma 5 (Semantic preservation) Several steps of rewriting preserve the semantics of well-formed triples: if S 1 ⊲ * S 2 and ⊢ S 1 , then [[S 1 ]](ρ) ≡ [[S 2 ]](ρ) for all environments ρ.

Theorem 2

 2 Definition parmove (mu: moves) : moves := match pmov (State mu ∅ ∅ ) with | State _ _ tau ⇒ reverse tau end. The semantic correctness of parmove follows from the previous results. Let µ be a parallel move problem. If µ is a windmill and does not mention temporary registers, then [[parmove(µ)]]→(ρ) ≡ [[µ]] // (ρ) for all environments ρ. Proof By definition of parmove and lemma 11, we have parmove(µ) = reverse(τ ) and (µ, ∅, ∅) ֒→ * (∅, ∅, τ ). By lemma 7, this entails (µ, ∅, ∅) ⊲ * (∅, ∅, τ ). The result follows from theorem 1.

Theorem 3

 3 Let µ = (s 1 → d 1 ) • • • (sn → dn) be a parallel move problem. Assume that the d i are pairwise distinct, and that s i / ∈ T and d i / ∈ T for all i. Let τ = parmove(µ). For all initial environments ρ, the environment ρ ′ = [[τ ]]→(ρ) after executing τ sequentially is such that 1. ρ ′ (d i ) = ρ(s i ) for all i = 1, . . . , n; 2. ρ ′ (r) = ρ(r) for all registers r / ∈ {d 1 , . . . , dn} ∪ T . Proof By theorem 2, we know that ρ ′ ≡ [[µ]] // (ρ). For (1), since d i / ∈ T , we have ρ ′ (d i ) = [[µ]] // (ρ)(d i ) = ρ(s i ) by lemma 2. For (2), we have ρ ′ (r) = [[µ]] // (ρ)(r), and an easy induction on µ shows that [[µ]] // (ρ)(r) = ρ(r) for all registers r that are not destinations of µ.

=

  {r | ∃i, r ⊲⊳ d i } ∪ {r | ∃t ∈ T , r ⊲⊳ t}.

Lemma 17

 17 Consider an elementary move (s → d) where s ∈ {s 1 , . . . , sn} ∪ T and d ∈ {d 1 , . . . , dn} ∪ T . If ρ 1∼ = ρ 2 , then ρ 1 [d ← ρ 1 (s)] ∼ = ρ 2 [d ⇐ ρ 2 (s)].Proof We need to show thatρ 1 [d ← ρ 1 (s)] (r) = ρ 2 [d ⇐ ρ 2 (s)] (r) ( * )for all registers r / ∈ D. By definition of D, it must be the case that either r = d or r ⊥ d, otherwise r would partially overlap d, which is a destination or a temporary, contradicting r / ∈ D. In the first case r = d, the left-hand side of (*) is equal to ρ 1 (s) and the right-hand side to ρ 2 (s). We do have ρ 1 (s) = ρ 2 (s) by hypothesis ρ 1 ∼ = ρ 2 and the fact that s / ∈ D by lemma 16.In the second case r ⊥ d, using the good variable property and the fact that r = d, the left-hand side of (*) is equal to ρ 1 (d). Using the weak good variable property, the right-hand side is ρ 2 (d). The equalityρ 1 (d) = ρ 2 (d) follows from hypothesis ρ 1 ∼ = ρ 2 .The previous lemma extends to sequences of elementary moves, performed with normal updates on one side and with weak updates on the other side. Lemma 18 Let τ be a sequence of moves such that for all (s → d) ∈ τ , we have s ∈ {s 1 , . . . , sn} ∪ T and d ∈ {d 1 , . . . , dn} ∪ T . If ρ 1 ∼ = ρ 2 , then [[τ ]]→(ρ 1 ) = [[τ ]]⇒(ρ 2 ).

Theorem 4

 4 Let µ = (s 1 → d 1 ) • • • (sn → dn) be a parallel move problem that satisfies hypotheses (1) to[START_REF] Bertot | Interactive Theorem Proving and Program Development -Coq'Art: The Calculus of Inductive Constructions[END_REF]. Let τ = parmove(µ). For all environments ρ, writingρ ′ = [[τ ]]⇒(ρ), we have 1. ρ ′ (d i ) = ρ(s i ) for all i = 1, . . . , n; 2. ρ ′ (r) = ρ(r) for all registers r disjoint from the destinations d i and from the temporaries T . Proof Define ρ 1 = [[τ ]]→(ρ). By theorem 3, we have ρ 1 (d i ) = ρ(s i ) for all i, and ρ 1 (r) = ρ(r) for all r / ∈ {d 1 , . . . , dn} ∪ T . By lemma 14, every move (s → d) ∈ τ is such that s is either one of the sources s i or a temporary, and d is either one of the destinations d i or a temporary. Since ρ ∼ = ρ holds trivially, lemma 18 applies and shows that ρ 1 ∼ = ρ ′ . Let d i be one of the destinations. We have ρ ′ (d i ) = ρ 1 (d i ) since d i / ∈ D by lemma 16. Moreover, ρ 1 (d i ) = ρ(s i ). The expected result follows.

We extend this property pointwise to lists l of moves and to states:

Obviously, the property P holds for µ 0 and therefore for the initial state (µ 0 , ∅, ∅). Moreover, the property is preserved by every rewriting step.

Lemma 12 If S 1 ⊲ S 2 and P (S 1 ) hold, then P (S 2 ) holds.

Proof By examination of the nondeterministic rewriting rules. The result is obvious for all rules except [Loop], since these rules do not generate any new moves. The [Loop] rule replaces a move (s → d) that satisfies P with the two moves (T (s) → d) and (s → T (s)). The new moves satisfy P by application of the second and third inference rules defining P .

It follows that the result of parmove(µ 0 ) satisfies property P .

Lemma 13 For all moves (s → d) ∈ parmove(µ 0 ), the property P (s → d) holds.

Proof Follows from lemmas 7, 11 and 12.

As a first use of this lemma, we can show that for every move in the generated sequence parmove(µ 0 ), the source of this move is either a source of µ 0 or a temporary, and similarly for the destination. The approach followed in this article enabled us to slightly improve the imperative algorithm from section 3 used as a starting point. In particular, the functional algorithm looks only for cycles involving the edge that started the recursion of the move_one function (i.e. the last element of the being-moved list, whereas the imperative algorithm looks for cycles anywhere in this list. The correctness proof for the ⊲ relation implies that looking for the cycle from the bottom of the being-moved stack is sufficient: in the case for the [Pop] rule, we proved that all elements of the being-moved list except the last one cannot have the destination dn as source.

While specified in terms of parallel moves, our results can probably be extended to parallel assignments (x 1 , . . . , xn) := (e 1 , . . . , en) where every expression e i mentions at most one of the variables x j .

Although efficient in practice, neither the initial imperative algorithm nor the functional algorithm proved in this paper are optimal in the number of elementary moves produced. Consider for instance the parallel move (r 3 , r 2 , r 1 ) := (r 1 , r 1 , r 2 ). The algorithms generate a sequence of 4 moves: r 3 := r 1 ; t := r 2 ; r 2 := r 1 ; r 1 := t, where t is a temporary. However, the effect can be achieved in 3 moves, using the destination register r 3 to break the cycle: r 3 := r 1 ; r 1 := r 2 ; r 2 := r 3 . Preliminary investigations suggest that the nondeterministic specification of section 4 can be extended with one additional rule to support this use of a destination to break cycles. However, the functional algorithm would become much more complex and require backtracking, possibly leading to exponential complexity.

A direction for further work is to prove the correctness of an imperative, arraybased formulation of the parallel move compilation algorithm, similar to the algorithm given in section 3. We are considering using the Why tool [START_REF] Filliâtre | Verification of non-functional programs using interpretations in type theory[END_REF][START_REF] Filliâtre | The Why software verification tool[END_REF] to conduct this proof. It raises several difficulties. The two nested loops and the number of arrays needed (src, dst and status) imply large invariants. Moreover the proof obligations generated by Why are huge and hard to work with. Furthermore, due to the side effects over arrays, delicate non-aliasing lemmas must be proved.