Jiantao Qi
email: jiantao.qi@upc.edu.cn

Jolanta Swiatowska

Peter Skeldon

Philippe Marcus

Jolanta Światowska

Chromium valence change in trivalent chromium conversion coatings on aluminium deposited under applied potentials

Keywords:

The electroassisted (EA) deposition of trivalent chromium conversion coatings on aluminium is investigated with a focus on the influence of applied potential on the chromium valence state, as determined by Raman spectroscopy. The morphology and compositions of the coatings were investigated by scanning electron microscopy and energy-dispersive spectroscopy. The EA coatings were formed in naturally-oxygenated SurTec 650 chromitAl solution at constant potentials of -1.5 and -0.5 V SCE . The coatings contained chromium and zirconium constituents. The potentials resulted in net cathodic and anodic current densities, respectively, during the coating growth. Comparisons were made with coating formation at the open-circuit potential (OCP). The coating thickness increased in order -0.5 V SCE < OCP < -1.5 V SCE , a result of increasing alkalinity from the cathodic reaction that facilitates deposition of the coating constituents. Fresh coatings formed at -1.5 V SCE revealed the presence of Cr 6+ species. By contrast, Cr 6+ species were not resolved in the coating formed at -0.5 V SCE . It is proposed that less H 2 O 2 is generated at -0.5 V SCE to oxidize Cr 3+ coating species.

Introduction

Trivalent chromium conversion (TCC) coating treatments are regarded as eco-friendly replacements of toxic chromate conversion coating processes [START_REF] Kendig | Corrosion inhibition of aluminum and aluminum alloys by soluble chromates, chromate coatings, and chromate-free coatings[END_REF][START_REF] Mitton | Selected Cr(VI) replacement options for aluminum alloys: a literature survey[END_REF][START_REF] Ely | Role of post-treatment in improved corrosion behavior of trivalent chromium protection (TCP) coating deposited on aluminum alloy 2024-T3[END_REF][START_REF] Verdalet-Guardiola | Nucleation and growth mechanisms of trivalent chromium conversion coatings on 2024-T3 aluminium alloy[END_REF]. A typical trivalent bath may contain hexafluorozirconate, trivalent chromium sulphate and supplemental ingredients such as fluoride species [START_REF] Guo | Characterization of trivalent chromium process coating on AA2024-T3[END_REF][START_REF] Munson | Cross comparison of TCP conversion coating performance on aluminum alloys during neutral salt-spray and thinlayer mist accelerated degradation testing[END_REF]. The fluoride component can activate the surface by thinning the surface oxide film to promote the coating formation [START_REF] Li | The formation, structure, electrochemical properties and stability of trivalent chrome process (TCP) coatings on AA2024[END_REF]. The resultant coatings on aluminium and aluminium alloys display a two-layer coating structure, consisting of an outer Zr-/Cr-rich layer over an alumina-rich layer containing fluorine species [START_REF] Dong | Structure and composition of trivalent chromium process (TCP) films on Al alloy[END_REF][START_REF] Qi | Trivalent chromium conversion coating formation on aluminium[END_REF][START_REF] Munson | Structure and chemical composition of different variants of a commercial trivalent chromium process (TCP) coating on aluminum alloy 7075-T6[END_REF][START_REF] Viroulaud | Influence of surface pretreatments on the quality of trivalent chromium process coatings on aluminum alloy[END_REF]. However, hexavalent chromium (chromate) species have been identified by Raman spectroscopy in freshly-formed coatings on aluminium [START_REF] Qi | Trivalent chromium conversion coating formation on aluminium[END_REF][START_REF] Qi | Spectroscopic studies of chromium VI formed in the trivalent chromium conversion coatings on aluminum[END_REF]. It has been shown that the trivalent chromium can be oxidized by hydrogen peroxide generated by oxygen reduction with a 2e pathway [START_REF] Qi | Trivalent chromium conversion coating formation on aluminium[END_REF][START_REF] Qi | Chromate formed in a trivalent chromium conversion coating on aluminum[END_REF].

Li et al. [START_REF] Li | Transient formation of chromate in trivalent chromium process (TCP) coatings on AA2024 as probed by Raman spectroscopy[END_REF] evidenced chromate species preferentially formed near copper-rich particles in a TCC coated AA2024 alloy, while remaining undetectable on the particle-free matrix. This correlated with the catalytic role of the cathodic particles in H 2 O 2 formation and with the locally enhanced cathodic reactions during conversion treatment. Furthermore, more chromate was recorded on terraces near copper-rich particles during immersion in sodium sulphate solution with a small H 2 O 2 addition (0.01 v/v) compared with the absence of H 2 O 2 , confirming the effectiveness of H 2 O 2 as an oxidant of Cr 3+ species. Other work correlated H 2 O 2 generation with colorimetric measurements using the titanly reagent and revealed that fluoride in the reaction solution significantly increased H 2 O 2 formation [START_REF] Qi | Chromate formed in a trivalent chromium conversion coating on aluminum[END_REF].

Notably, Cr 6+ species were detected on TCC coated AA2024 alloy after the coating was aged in air for more than 1 h but were undetectable in freshly-formed coatings, which was attributed to insufficient dissolved oxygen in the bath [START_REF] Li | The formation, structure, electrochemical properties and stability of trivalent chrome process (TCP) coatings on AA2024[END_REF][START_REF] Li | Transient formation of chromate in trivalent chromium process (TCP) coatings on AA2024 as probed by Raman spectroscopy[END_REF]. However, a chromate component was found in freshly-formed coatings on aluminium [START_REF] Qi | Trivalent chromium conversion coating formation on aluminium[END_REF]. Of possible significance to this discrepancy, the steady open-circuit potential (OCPs) during conversion treatments of AA2024 alloy is positively shifted (to -0.8 V SCE ) compared with aluminium (-1.5 V SCE ) [START_REF] Qi | Trivalent chromium conversion coating formation on aluminium[END_REF][START_REF] Qi | Formation of a trivalent chromium conversion coating on AA2024-T351 alloy[END_REF], suggesting that reduction of oxygen to form hydrogen peroxide rather than hydroxyl ions may depend on the potential. With respect to electroassisted (EA) deposition of TCC coating formation, Dong et al. reported coatings containing zirconium and trivalent chromium oxides, similar to coatings formed under the open-circuit potential [START_REF] Dong | Structure and composition of trivalent chromium process (TCP) films on Al alloy[END_REF][START_REF] Dong | In situ evolution of trivalent chromium process passive film on Al in a corrosive aqueous environment[END_REF].

The influence of the electrochemical potential of the substrate on the formation of H 2 O 2 and Cr 6+ species during coating growth on aluminium is the focus of the present research. This factor has received little previous attention. The study specifically investigated the role of constant applied potentials of -0.5 V SCE and -1.5 V SCE during conversion treatments in a commercial TCC solution. These potentials result in net anodic and cathodic polarization of the aluminium, respectively. Scanning electron microscopy (SEM) with energy-dispersive Xray spectroscopy (EDS) was used to characterize the coatings. Additionally, the coated specimens were analysed by Raman spectroscopy to determine the chromium chemistry and its dependence on the applied potential and immersion time.

Experimental procedure

Materials and regnant

Specimens, of dimensions 30 × 12 × 0.3 mm, were cut from 99.97 % aluminium sheet, rinsed sequentially in acetone, ethanol and deionized water, then electropolished in a mixture of perchloric acid and ethanol (1:4 volumes) at 20 V for 240 s below 10 °C. They were then rinsed in ethanol and deionized water and dried in a stream of cool air.

SurTec 650 chromitAL (SurTec Corp.) was diluted with deionized water at a volume ratio of 1:4 and then 1 wt.% NaOH droplets were used to adjust the solution pH to 3.9. Inductively coupled plasmaatomic emission spectroscopy (ICP-AES) analysis of the bath, using a Perkin-Elmer Optima 5300 dual view instrument, revealed a Zr/Cr atomic ratio of 0.70 ± 0.02. The composition of SurTec 650 chromitAL is subject to commercial confidentiality, but is presumed to contain zirconium hexafluorozirconate, tri-valent chromium sulphate and fluoride constituents that are usually present in TCC baths. Consistent with the presence of such constituents, other work has shown that ZrO 2 , Cr(OH) s , CrF 3 and Cr 2 (SO 4 ) 3 are principal components of coatings formed in SurTec 650 chromitAL solution [START_REF] Qi | Trivalent chromium conversion coating formation on aluminium[END_REF].

A three-electrode cell, containing a saturated calomel electrode (Eº = 0.24 V vs NHE), a graphite cathode and a specimen with an exposed area of ∼2.25 cm 2 , was used for coating formation. Potentials were controlled by a Solarton electrochemical workstation with a Modulab software controller. First a potential of +0.5 V SCE was applied for 10 s to activate the surface and then the potential was increased to -0.5 or -1.5 V SCE for either 1200 or 2400s. The time of the coating process was selected to be the same as (1200s) or greater than (2400s) the time used in previous work that revealed chromate species in a coating formed under the OCP condition [START_REF] Qi | Trivalent chromium conversion coating formation on aluminium[END_REF][START_REF] Qi | Chromate formed in a trivalent chromium conversion coating on aluminum[END_REF]. The coated specimens were immediately removed from the cell and examined by Raman spectroscopy within 10 s to limit the possibility of oxidation of Cr 3+ species in air. In addition, potentiodynamic polarization of electropolished aluminium was performed from -2 to 0 V SCE at 1 mV/s in the SurTec 650 chromitAL solution (40 °C, pH 3.9). The specimen was first polarized at +0.5 V SCE and then the potential was immediately switched to -2.0 V SCE for the start of the potential scan. The experiments were repeated three times, revealing reproducible polarization behaviour.

Characterization methods

SEM-EDS employed a Zeiss

Ultra 55 instrument at accelerating voltages of 3 and 15 kV. Raman spectroscopy used a Renishaw 2000 Raman instrument with an argon laser (wavelength 514 nm, 12.5 mW power). Calibration utilized a silicon peak at 520 cm -1 in the static mode. For specimen examination, the extended mode from 1200 to 200 cm -1 was employed with 30 s integration and 10-time accumulation to eliminate any background noise effect.

Results and discussion

Fig. 1 presents the polarization curve for electropolished aluminium in SurTec 650 solution (40 °C, pH 3.9) scanned from -2.0 V SCE to 0 V SCE . The current density in the cathodic branch rises to a peak value of 1.02 × 10 -4 A cm -2 at -1.85 V SCE then decreases with a log-linear dependence on voltage over almost one decade of current density before decreasing steeply to zero net current density at -1.34 V SCE . The latter value compares with OCPs in the range -1.54 to -1.50 V SCE reported previously for growth of a coating over a period of 1200s in the same solution. The lower potential of zero current density in the polarization curve is due to the influence of the prior period of cathodic polarization. The decline in the magnitude of the cathodic current at potentials below -1.85 V SCE can be attributed to the contribution of an anodic current density due to activation of the aluminium substrate. The net cathodic current density at higher potentials, which arises from reduction of H + ions, water molecules and dissolved oxygen, exceeds the anodic current density due to oxidation of aluminium. The current density in the anodic branch of the polarization curve rise steeply until a potential of about -1.00 V SCE , when the slope decreases sharply and the current density then rises slowly from 4 × 10 -5 A cm -2 to about 7 × 10 -5 A cm -2 at 0.0 V SCE .

Coatings were prepared under constant potentials of -1.5 and -0.5 V SCE . At -1.5 V SCE , reduction of H + ions and dissolved oxygen can contribute to the cathodic current density. Oxygen reduction may be dominant at -0.5 V SCE as the equilibrium potential for H + reduction is close to -0.5 V SCE at the pH of the bulk solution (3.9). The former potential is close to the OCP potential for coatings formed by simple immersion in the naturally aerated solution. The current density during coating treatments for times of 1200s are shown in Fig. 2(a). The details of the first 200 s of treatment are shown in Fig. 2(b). For the treatment at -1.5 V SCE , the main features of the curve are an (i) increase in the net cathodic current density to -0.75 mA cm -2 in the first 20 s of polarization followed by a fall to -0.50 mA cm -2 after 30 s; (ii) a plateau at -0.45 mA cm -2 between 75-200 s; (iii) a decrease at a progressively reducing to a final current density of -0.26 mA cm -2 . Thus, the specimen was cathodically polarized over the whole of the treatment time. The polarization at -0.5 V SCE resulted in a net anodic current density throughout the coating process, comprising an initial rapid rise in current density to 1.8 mA cm -2 during the initial 20 s followed by a smooth decrease at a reducing rate to reach a final value of 0.4 mA cm -2 . Notably, the current density in the potentiodynamic polarization curve at -0.5 V SCE , namely 0.03 mA cm -2 , is lower than the final value of the potentiostatic curve (0.4 mA cm -2 ). It is due to the much greater coating thickness that results from the prior cathodic polarization of the specimen at the start of the polarization scan. The strong influence of cathodic polarization on the coating thickness is evident in the results from EDS analyses presented later. In addition, the curves for both -1.5 and -0.5 V SCE shows rapid increases in the current density in the first 20 s of polarization. This is probably due to thinning of the oxide film that was present on the surface of the electropolished aluminium specimens. Thereafter, growth of the coating causes the net anodic and cathodic current densities to decrease.

Fig. 3(a-d) presents scanning electron micrographs of TCC coatings formed at the OCP (≈-1.45 V SCE ) for 1200s, -0.5 V SCE for 1200 and 2400s and at -1.5 V SCE for 1200s. A smooth coating surface resulted in most regions of all coatings. However, the coatings contained cracks generated by dehydration and shrinkage of the coating material during drying. The coatings also contained deposits of solution precipitates [START_REF] Li | Transient formation of chromate in trivalent chromium process (TCP) coatings on AA2024 as probed by Raman spectroscopy[END_REF], which are evident as granular features of white appearance at the coating surface. The cracks in the coatings formed at the OCP and -1.5 V SCE for 1200s formed a continuous network. In contrast, cracks in the coating formed at -0.5 V SCE , often propagated short distances from the points of initiation and did not connect with other cracks. This difference in the crack morphology is possibly related to differing degrees of hydration of the coating material, and hence in the magnitude of the stresses caused by shrinkage of the coating, and also to differing coating thicknesses. The cracking, which has been reported previously in similar coatings [START_REF] Qi | Trivalent chromium conversion coating formation on aluminium[END_REF][START_REF] Qi | Comparative studies of thin film growth on aluminium by AFM, TEM and GDOES characterization[END_REF], is likely to have been exacerbated by exposure to vacuum of the microscope.

Fig. 4 shows results of EDS spot analyses made at an accelerating voltage of 15 kV on the surface of coatings formed at the OCP (-1.45 V SCE ), -0.5 and -1.5 V SCE for 1200s. The analyses were made remote from locations of cracks. A coating was also formed for 2400s at -0.5 V SCE . After coating formation, the specimens were immersed in deionized water for 120 s and dried in a cool-air stream. The spectra contain peaks from oxygen, aluminium, fluorine, zirconium and chromium in the coating and of carbon from adsorbed contaminant. According to previous X-ray photoelectron spectroscopy, ZrO 2 , Cr(OH) s , CrF 3 and Cr 2 (SO 4 ) 3 are the main constituents of the outer layer of the coating [START_REF] Qi | Trivalent chromium conversion coating formation on aluminium[END_REF]. Insufficient sulphur was present in the coating for the sulphur Kα peak at 2.307 keV to be clearly resolved in the spectra Fig. 4. The additional, much higher peak in the spectra originating from aluminium mainly results from X-ray generation from the aluminium substrate that dominates the contribution from aluminium in the inner alumina-rich layer of the coating, which also contains a significant amount of fluorine [START_REF] Qi | Trivalent chromium conversion coating formation on aluminium[END_REF][START_REF] Qi | Influence of water immersion posttreatment parameters on trivalent chromium conversion coatings formed on AA2024-T351 alloy[END_REF]. The SurTec solution contains hydrolysed trivalent chromium and zirconium species [START_REF] Qi | Chromate formed in a trivalent chromium conversion coating on aluminum[END_REF][START_REF] Chidambaram | The role of hexafluorozirconate in the formation of chromate conversion coatings on aluminum alloys[END_REF], which form deposits of the coating material on the aluminium surface as a result of the increases in pH that results from the reduction of H + ions and dissolved oxygen [START_REF] Dong | Structure and composition of trivalent chromium process (TCP) films on Al alloy[END_REF][START_REF] Dong | In situ evolution of trivalent chromium process passive film on Al in a corrosive aqueous environment[END_REF]. The highest peaks for fluorine, zirconium and chromium were associated with the cathodically polarized specimen coated at -1.5 V SCE for 1200s. The lowest peaks occurred for the anodically polarized specimen coated at -0.5 V SCE for 1200s. The peaks for the coating formed at the OCP for 1200s were between those of the previous coatings. Taking the height of the zirconium peak as an indicator of the coating thickness, the cathodically polarized aluminium was about 2.5 times thicker than that on the specimens coated at the OCP and about 6 times thicker than the coating formed at -0.5 V SCE . The EDS results indicate the significant increase in the rate of coating growth that can be achieved by reducing potential below the OCP. In contrast, the rate of growth is significantly lowered at potentials above the OCP. In the present instance, the rate of growth of the coating formed at -0.5 V SCE was about 2.5 times slower than at the OCP. The coating thickness of the anodically polarized specimen was increased by about a factor of two by doubling the treatment time from 1200s to 2400s [START_REF] Qi | Formation of a trivalent chromium conversion coating on AA2024-T351 alloy[END_REF]. Fig. 5 shows Raman spectra of the coated specimens treated for 1200s at the OCP, -1.5 V and -0.5 V vs SCE. In all spectra, zirconium oxide was identified by peaks at 470 and 537 cm -1 and chromium sulphate at 998 cm -1 . The peak around 810 cm -1 is associated with aluminium hydroxides [START_REF] Munson | Cross comparison of TCP conversion coating performance on aluminum alloys during neutral salt-spray and thinlayer mist accelerated degradation testing[END_REF]. The spectra for coatings formed at -1.5 V SCE and the OCP had an additional peak for Cr 6+ species at 866 cm -1 . This peak was not resolved at -0.5 V even when the treatment was extended to 2400s. After this time of treatment, the EDS analyses showed that the coating thickness was similar to that of the coating formed at the OCP. This difference in the spectra indicates the much greater presence of Cr 6+ species in the coatings formed at the more negative potentials. The chromate species result from the oxidation of Cr 3+ species by the H 2 O 2 generated by oxygen reduction, which can occur by two pathways:

O 2 + 2H + + 2e -→ H 2 O 2 (Eº = +0.44 V vs. SCE) (1)
O 2 + 4H + + 4e -→ 2H 2 O (Eº = +0.99 V vs. SCE) (2)
The relative contributions of Reactions ( 1) and ( 2) to the overall oxygen reduction current on the present specimens is unknown, but is likely to depend upon the coating composition, the presence of adsorbed species, the solution pH adjacent to the specimen surface and the electrode potential [START_REF] Qi | Comparative studies of thin film growth on aluminium by AFM, TEM and GDOES characterization[END_REF]. For instance, the oxygen reduction current due to Reaction (1) has been shown to depend upon the substrate composition and to increase at more cathodic potentials [START_REF] Qi | Comparative studies of thin film growth on aluminium by AFM, TEM and GDOES characterization[END_REF]. Cathodic polarization of aluminium can also encourage the formation of hydrogen peroxide from reaction of hydroperoxyl radicals, as follows [START_REF] Joo | Oxidative degradation of the carbothioate herbicide, molinate, using nanoscale zero-valent iron[END_REF],

(O 2 ) ads + H + + e → HO 2 % (pH < 4.8) (3)
HO 2 % + HO 2 % → H 2 O 2 + O 2 (4)
Cr 3+ oxidation in TCC coatings can be mitigated using an addition to the bath that can be preferentially oxidized by H 2 O 2 . Xia et al. [START_REF] Xia | Structure and function of ferricyanide in the formation of chromate conversion coatings on aluminum aircraft alloy[END_REF] reported the effectiveness of IrCl 6 -3/-2 , Fe +3/+2 , V +3/+2 and Fe(CN) 6 -3/-4 . For instance, the standard potentials of IrCl 6 -3/-2 and Cr 6+ /Cr 3+ are +1.02 and +1.33 V NHE respectively, and the Gibbs free energy of the IrCl 6 -3/-2 redox system is lower than that of chromium system.

Thus, IrCl 6 -3/-2 can be preferentially oxidized by H 2 O 2 . Our previous work employed Fe +3/+2 additions to the SurTec solutions to restrict Cr 6+ formation in freshly-formed TCC coatings on AA2024 alloy [START_REF] Qi | Effect of an Fe(II)modified trivalent chromium conversion process on Cr(VI) formation during coating of AA 2024 alloy[END_REF].

Conclusions

1 The present work, focused on the influence of applied potential on Cr 3+ species.

Fig. 1 .

 1 Fig. 1. Potentiodynamic polarization curve of electropolished aluminium during immersion in SurTec 650 chromitAL solution (40 °C, pH 3.9) for 2000s.

Fig. 2 .

 2 Fig. 2. (a) Current transients obtained during potentiostatic polarization of aluminium in SurTec 650 chromitAL solution (40 °C, pH 3.9) at -0.5 and -1.5 V SCE for 1200s. (b) Detail of the initial 200 s.

Fig. 3 .

 3 Fig. 3. Scanning electron micrographs of TCC coatings formed at the (a) OCP for 1200s, (b) -0.5 V SCE for 1200s, (c) -0.5 V SCE for 2400s and (c) -1.5 V SCE for 1200s.

Fig. 4 .

 4 Fig. 4. SEM/EDS spectra for fluoride, zirconium and chromium components in coatings formed on aluminium in SurTec 650 chromitAL solution (40 °C, pH 3.9) at the OCP and -0.5 and -1.5 V SCE for 1200s and -0.5 V SCE for 2400s.

Fig. 5 .

 5 Fig. 5. Raman spectra of coatings formed on aluminium in SurTec 650 chromitAL solution (40 °C, pH 3.9) at the OCP and -0.5 and -1.5 V SCE for 1200s and -0.5 V SCE for 2400s.

Acknowledgements

The authors thank the National Natural Science Fund (51701239), Shandong Natural Science Fund (ZR2017LEM005) Fundamental Research Funds for the Central Universities (18CX02128A) and the LATEST2 Programme Grant (EP/H020047/1) for the financial support of this work.

Author statement

Jiantao Qi carried out the data curation and writing-Original draft preparation; Jolanta Światowska provided the Raman methodology and validation; Peter Skeldon carried out the investigation, reviewing and editing; Philippe Marcus carried out the paper writing -reviewing and editing. All authors contributed to the interpretation of the results and to the writing of the paper.

Declaration of Competing Interest

The authors declare that they have no known competing financial interests or personal relationships that could have appeared to influence the work reported in this paper.


Gautier Berthou

Pierre-Évariste Dagand

Delphine Demange

Rémi Oudin

Tanguy Risset

Intermittent Computing with Peripherals, Formally Verified

Keywords: CCS Concepts:, Computer systems organization → Embedded systems, • General and reference → Reliability, • Software and its engineering → Checkpoint / restart, • Theory of computation → Program specifications, Program semantics Intermittent computing, Formal specification, Semantic refinement

Transiently-powered systems featuring non-volatile memory as well as external peripherals enable the development of new low-power sensor applications. However, as programmers, we are ill-equipped to reason about systems where power failures are the norm rather than the exception. A first challenge consists in being able to capture all the volatile state of the application -external peripherals includedto ensure progress. A second, more fundamental, challenge consists in specifying how power failures may interact with peripheral operations. In this paper, we propose a formal specification of intermittent computing with peripherals, an axiomatic model of interrupt-based checkpointing as well as its proof of correctness, machine-checked in the Coq proof assistant. We also illustrate our model with several systems proposed in the literature.

retrieved flows into short-term storage facilities, such as capacitors, leading to computation times on the order of thousands of cycles per run. A run denotes a continuous period of time without power failure. To ensure progress of computation across runs, system integrators often pair such devices with non-volatile memory (NVM), such as non-volatile RAM technology (FRAM, MRAM, etc.). This combination of features gave birth to intermittent computing. However, the interaction of volatile (registers, caches) and non-volatile states together with unpredictable power failures is itself a poisonous mix, dubbed the "broken time machine" [START_REF] Ransford | Nonvolatile Memory is a Broken Time Machine[END_REF].

One way to circumvent this issue consists in adding a sensor monitoring the remaining energy level [START_REF] Colin | A Reconfigurable Energy Storage Architecture for Energy-harvesting Devices[END_REF]. Before the power runs out, a hardware interrupt is triggered, which is then handled in software, leading the system to checkpoint its volatile state to NVM. Checkpoints are necessarily consistent as they result from a snapshot of the application taken at a single point in time. This offers the simplicity of static checkpointing [START_REF] Lucia | A simpler, safer programming and execution model for intermittent systems[END_REF] -where explicit checkpointing instructions are spread throughout the code -without much overhead -snapshots are acquired only when necessary.

This solution leaves a critical blind spot: external peripheral devices also contain volatile state, inaccessible from the CPU -efficiently or at all. Besides, interacting with an external device changes our expectations about the system. Consider for instance a radio transceiver peripheral. The radio device requires calibration before packet emission or reception. This takes about 100𝜇s on the device, during which the driver is busy-waiting. If a power-loss were to occur after, say, 75𝜇s, it would be functionally incorrect to resume the transceiver in calibration mode and only wait for the remaining 25𝜇s. To be correct, the calibration code sequence must execute within a single run.

Following earlier work on supporting peripherals in intermittent computation [START_REF] Arreola | RESTOP: Retaining External Peripheral State in Intermittently-Powered Sensor Systems[END_REF][START_REF] Berthou | Sytare: A Lightweight Kernel for NVRAM-Based Transiently-Powered Systems[END_REF][START_REF] Branco | Intermittent Asynchronous Peripheral Operations[END_REF][START_REF] Hester | Timely Execution on Intermittently Powered Batteryless Sensors[END_REF][START_REF] Maeng | Supporting peripherals in intermittent systems with just-in-time checkpoints[END_REF], we identify two key challenges: (C1) Peripherals add volatile and opaque state to the overall system; (C2) Peripherals have a concrete, observable impact on the environment of the system. The present work aims at providing a conceptual framework for [START_REF] Ahmed | Efficient Intermittent Computing with Differential Checkpointing[END_REF] formally expressing these two requirements; and [START_REF] Arreola | RESTOP: Retaining External Peripheral State in Intermittently-Powered Sensor Systems[END_REF] proving that a general interrupt-based checkpointing scheme meets its specification. To this end, we make the following assumptions throughout the paper: (A1) NVM is solely used to store snapshots of the application.

Conversely, application code cannot access the NVM; (A2) Checkpointing volatile state (registers, RAM, etc.) from the micro-controller (MCU) is a solved problem (e.g., Ahmed et al. [START_REF] Ahmed | Efficient Intermittent Computing with Differential Checkpointing[END_REF]) whereas the peripheral internal state is completely opaque to the application; (A3) Peripherals act upon an environment that is idempotent. A transiently-powered system may, for example, send a network packet multiple times: we expect the network protocol to gracefully handle such situations. This touches upon a fundamental assumption of transiently-powered systems in general [START_REF] Surbatovich | I/O dependent idempotence bugs in intermittent systems[END_REF]; (A4) Liveness of the application is secured by a suitably calibrated power sensor. Checkpointing needs not always succeed but it is assumed to eventually succeed. Assumption (A1) excludes some existing systems [START_REF] Hicks | Clank: Architectural Support for Intermittent Computation[END_REF][START_REF] Jayakumar | QuickRecall: A HW/SW Approach for Computing across Power Cycles in Transiently Powered Computers[END_REF][START_REF] Lucia | A simpler, safer programming and execution model for intermittent systems[END_REF][START_REF] Maeng | Alpaca: intermittent execution without checkpoints[END_REF][START_REF] Maeng | Supporting peripherals in intermittent systems with just-in-time checkpoints[END_REF][START_REF] Van Der Woude | Intermittent Computation without Hardware Support or Programmer Intervention[END_REF] from the scope of this work. Since Challenges (C1) and (C2) are orthogonal to an application's ability to access NVM, we chose to exclude it for pedagogical clarity.

We propose a general model of interrupt-based checkpointing based on these assumptions. Dealing with an external communication bus (e.g., I 2 C or SPI), we may for example suffer from a power failure right after having configured the bus to address a specific component but before actually interacting with the component. In the next run, the bus will be resumed in its default state: if we resume the application where it lost power, it will fail to proceed as desired. Instead, one resolves to log the interaction with the peripherals and replay the log upon reboot [START_REF] Arreola | RESTOP: Retaining External Peripheral State in Intermittently-Powered Sensor Systems[END_REF][START_REF] Berthou | Sytare: A Lightweight Kernel for NVRAM-Based Transiently-Powered Systems[END_REF][START_REF] Branco | Intermittent Asynchronous Peripheral Operations[END_REF]. Some operations must execute under continuous power to produce a meaningful outcome, as witnessed by our earlier radio device example. Applications must be able to specify power-continuous sections 1 , asserting that a given sequence of instructions must be executed within a single run. Fig. 1 (PLF) illustrates our proposal. Peripheral devices (DEV) are accessed through a specific API. NVM (CHKPT) enables double-buffering [START_REF] Ransford | Mementos: system support for long-running computation on RFID-scale devices[END_REF], ensuring progress. A logging mechanism (LOG) is key to restore peripherals in a consistent state. Now, this begs the question: what does it mean for our scheme to be "correct"? The application is specified (SPEC in Fig. 1) as if it was run in a continuously-powered environment. Our correctness result states that the checkpointed application behaves as prescribed by SPEC: the trace of operations emitted by peripherals is also observable in the continuous-power specification (modulo re-executions), and power-continuous sections are executed within a single run.

Our contributions are the following:

• We specify intermittent computing with peripherals (Section 2) with a labeled transition system. We strive 1 Our notion of "power-continuous section" corresponds to "atomicity" from Maeng and Lucia [START_REF] Maeng | Supporting peripherals in intermittent systems with just-in-time checkpoints[END_REF], an overloaded terminology from concurrent systems. for generality, making no assumption about the actual behavior of peripherals and allowing non-determinism, including preemptive and concurrent systems. • We give an axiomatic model of interrupt-based checkpointing (Section 3). This includes an equational specification of a logging mechanism and a persistent storage interface, thus simplifying the task of checking the validity of one's implementation to a handful of conditions. The model consists of a state machine with five states that captures the essence of checkpointing. • We state the correctness of our model with respect to its specification (Section 4). We show that peripheral operations are preserved despite power failures and that power-continuous sections are complied with.

On-going checkpoint

• We relate our model to existing systems (Section 5). Overall, the present work aims at consolidating our formal understanding of transiently-powered systems and their interaction with external peripherals. This is first and foremost a conceptual work. In particular, this paper does not provide a verification tool nor does it prove the correctness of a particular implementation: our objective is to provide system designers with a solid, actionable mental model.

All the formal definitions and results presented in this paper have been machine-checked [START_REF] Berthou | Intermittent Computing with Peripherals, Formally Verified -Companion Coq Development[END_REF] in the Coq proof assistant [START_REF]The Coq Proof Assistant[END_REF]. For readability, we have typeset our Coq definitions using set-theoretic notations. We nonetheless keep a distinct namespace per conceptual object, which follows the naming scheme NAMESPACE.object. We write NAMESPACE.t to denote abstract components whose implementation is left unspecified.

In the following, we aim to distill the essence of intermittent computing with peripherals. We focus our attention solely on the challenges raised by the combination of power failure and peripheral devices. To this end, we introduce an axiomatic programming model. To the practitioner, it may seem far removed from the assembly code that actually drives intermittent computations. This is in fact a virtue of this work: we aim at providing a conceptual framework with which to reason about intermittent computations and their interaction with peripherals. By freeing ourselves from a particular implementation, we remain non-prescriptive about orthogonal design choices, such as the treatment of concurrency, interrupts, etc. We thus offer a very liberal specification that can be readily and effectively used to check the design of a concrete implementation.

In this section, we layout our specification of intermittent computations, which ought to be met by our checkpointing model. We encourage readers to check that the behaviors they care about in their applications can be captured by our specification.

Modeling the MCU. We specify the MCU as an overarching abstraction of the CPU registers and relevant fragments of volatile memory (RAM). It encompasses all the volatile states that can efficiently be checkpointed to NVM through standard techniques [START_REF] Balsamo | Hibernus: Sustaining Computation During Intermittent Supply for Energy-Harvesting Systems[END_REF]. It does not include peripheral devices -whose treatment comes next -and non-volatile memory -which is outside the scope of our specifications, as per Assumption (A1). In the following, we let MCU.t be the set of possible MCU states. We use the variable mcu ∈ MCU.t to denote an arbitrary MCU state. We call MCU.init ∈ MCU.t the initial MCU state, just before executing the first instruction of a given application.

Modeling peripheral devices. Handling Challenge (C1) calls for a careful distinction between the physical peripherals -whose internal state cannot be accessed by the program -and the interface it exposes to the program. We therefore introduce both an abstract description of the peripheral, representing the state of the physical device, and an interface driving the evolution of the abstract device state.

We let DEV.t be the set of possible physical peripheral states, and use the variable dev ∈ DEV.t to denote an arbitrary peripheral state. We call DEV.init ∈ DEV.t the initial peripheral state, on power-up.

The idea that peripherals are manipulated through a welldefined interface is a natural one [START_REF] Branco | Intermittent Asynchronous Peripheral Operations[END_REF]. It may involve the low-level application binary interface (ABI) documented by a datasheet or the application program interface (API) provided by a high-level library. We accommodate either style by assuming that there exists a set DEV.ops of operations supported by the peripheral. Conventionally, we write op ∈ DEV.ops to denote an arbitrary operation. Given a particular device state, performing an operation has the effect of producing a new device state. The behavior of a peripheral can thus be specified through a relation - This relation plays an essential role in our formalization. It turns DEV.ops, over which the software has control, into operations over the physical device DEV.t, over which the software has no control. Our simple modeling of peripheral devices accounts for systems featuring multiple physicallydecoupled peripherals. We can simply consider the set of all available devices as a single one whose interface is the disjoint sum of their respective interfaces.

Specification. We now introduce, under the SPEC namespace, our axiomatic specification of an intermittent computation. We ask for just enough structure to address Challenge (C2). In doing so, we expose only the properties we care about, namely the expected observable behavior of programs under continuous power execution. The remaining implementation details, which are orthogonal to the correctness statement, are abstracted away.

To account for power-continuous code sections, we distinguish two execution modes in an intermittent computation: a program can either run in "user mode" (U ∈ SPEC.mode) or in "driver mode" (D ∈ SPEC.mode). A computation may be resumed at any point in user mode while it can only be resumed to the very first instruction of a sequence of instructions in driver mode. This means that a sequence of instructions in driver mode should either be executed entirely without being interrupted by a power failure, or the entire code block will be re-executed in the next run.

Example 2.1. The calibration code of the radio frequency synthesizer (discussed in the introduction) should therefore be specified as a driver mode code sequence. This ensures that the busy-wait is always executed as a whole before calibration is deemed completed. Other examples include non-immediate transactions, frequent with SPI or I 2 C buses.

Modes are thus a key ingredient to specify power-continuous sections. We write m ∈ SPEC.mode to denote an arbitrary execution mode.

Our specification should be able to describe a set of desired behaviors. Since peripherals are meant to interact with their environment, a natural notion of "behavior" is the sequence of operations performed by the device. We write SPEC.trace ≜ DEV.ops * the set of sequences of operations. We write t ∈ SPEC.trace to denote an arbitrary trace, 𝜖 to denote the empty sequence and t ; t ′ to denote a concatenation of traces. We define dev

(D, mcu, dev) t SPEC (U, mcu ′ , dev ′ ),
then mcu = mcu ′ , dev = dev ′ and t = 𝜖. This axiomatization amounts to a state machine (Fig. 2) with two states -the user and driver modes -together with four possible kinds of transitions. Specifically, Enter and Leave delineate the power-continuous sections operating on external peripherals. These two transitions are purely formal, leaving the concrete state of the application unchanged (same MCU, same device and producing an empty trace). Upon reasoning about a concrete application, we are therefore free to switch mode at any point we see fit from a logical standpoint, irrespectively of its operational behavior.

The semantics of an intermittent computation follows simply by iterating the single-step transition relation above, starting from the initial state. Formally, we define the semantics SPEC.sem as the following set of traces:

𝑡 ∈ SPEC.sem ⇔ ∃s, (U, MCU.init, DEV.init) t SPEC * s
The set SPEC.sem consists of all the admissible behaviors of the system under study. Indeed, any trace in this set corresponds to a sequence of peripheral operations performed during a continuously-powered execution.

Being a specification, the above definition of SPEC.sem deserves scrutiny. In particular, it must be expressive enough to account for the properties expected by a specific, realworld application. To fit within our framework, these properties need to be expressible in terms of traces specifying expected observations, and/or user-driver transitions specifying power-continuous sections. The following examples illustrate how our specification addresses Challenge (C2).

Example 2.2. Suppose we want to (1) sense a temperature with an analog component through an Analog-to-Digital Converter, then (2) convert that value to a human-readable format to (3) be displayed on a teletype. This program can be modeled either as a single sequence encompassing all three operations executing in mode D, or as three sequences executing in, successively, D → U → D modes, value conversion being performed in mode U. In both cases, the formal trace consists in a sensing operation followed by a display operation. However, the latter case describes an application that -subject to power failures -allows for the displayed temperature to be arbitrarily outdated, whereas the former case captures the timeliness requirement of the whole sequence of operations.

Example 2.3. Consider an application that regularly sends a thermal sensor's data in radio packets. The application sets a timer to periodically sense and send data, then waits for commands coming from the radio between packet emissions. If both the sensor and the radio devices are accessed through the same SPI bus, this SPI bus requires two different configurations (e.g., bus clock frequency), both being distinct operations in DEV.ops, to communicate with both devices.

The datasheet specifies the state of all the peripherals (SPI bus, thermal sensor, radio device, timer) upon power-up: this defines DEV.init. The radio module, when set in reception mode, may fire interrupts. Retrieving the packet should be performed in a power-continuous section (D mode) so that either the handler runs to completion in a single run (effectively receiving the radio packet), or the packet is lost in the event of a power-loss.

Note that the interaction between, say, timer and radio interrupts requires a resource locking mechanism to properly share access to the SPI bus, independently of whether the application may reboot or not. Such a mechanism is therefore orthogonal to power-continous sections.

Interrupt-based checkpointing

We now give a formal description of interrupt-based checkpointing with peripherals [START_REF] Arreola | RESTOP: Retaining External Peripheral State in Intermittently-Powered Sensor Systems[END_REF][START_REF] Berthou | Sytare: A Lightweight Kernel for NVRAM-Based Transiently-Powered Systems[END_REF][START_REF] Branco | Intermittent Asynchronous Peripheral Operations[END_REF][START_REF] Maeng | Supporting peripherals in intermittent systems with just-in-time checkpoints[END_REF]. The present model plays two roles. First, we lay out the minimal requirements to implement an interrupt-based checkpointing system. Namely, one must be able to log peripheral actions and store an image of the MCU and of the action log to NVM. Second, we provide a conceptual framework for reasoning about the correctness of such a checkpointing system. Namely, we introduce the notion of instrumented trace.

Operation logging

To restore a physical device into a previously encountered state, we must resort to the only information accessible to the program: peripheral operations. A straightforward way to achieve this objective would consist in logging every such operation. Restoring the physical device would then amount to replaying the entire log. However, such an implementation would be prohibitive both in terms of time and space, especially in an embedded system. Rather than restricting ourselves to a single inefficient implementation, we consider an abstract specification of such a log. In Section 5, we show that this interface admits several efficient implementations.

We let LOG.t to be the set of such summaries of all previous peripheral operations. An operation can be added to a given log through the function We overload notations and write LOG.log t ℓ for the sequential logging of each individual operation of a trace t = op 0 ; . . . ; op 𝑛 , i.e., LOG.log op 𝑛 (. . . (LOG.log op 0 ℓ)).

Non-volatile checkpoint storage

Checkpointing storage is the only component in our system that is persistent across reboots. Non-volatile checkpoints are represented by an abstract set CHKPT.t. Intuitively, a checkpoint contains two snapshots of the application, implementing double-buffering [START_REF] Ransford | Mementos: system support for long-running computation on RFID-scale devices[END_REF]: a stable one (the "last" valid one) and an on-going one (the "next" valid one, if checkpointing succeeds). A snapshot consists of an MCU image and a peripheral log. We write chkpt ∈ CHKPT.t to denote an arbitrary checkpointing storage.

We

nextMcu (CHKPT.saveNextMcu chkpt mcu) = mcu nextLog(CHKPT.saveNextMcu chkpt mcu) = nextLog chkpt last (CHKPT.saveNextMcu chkpt mcu) = last chkpt nextLog (CHKPT.saveNextLog chkpt ℓ) = ℓ nextMcu (CHKPT.saveNextLog chkpt ℓ) = nextMcu chkpt last (CHKPT.saveNextLog chkpt ℓ) = last chkpt
Elements of CHKPT.t constitute the only piece of state that we intend to persist across reboots.

Interrupt-based checkpointing

We now define our model of interrupt-based checkpointing under the PLF namespace, which stands for "Power-Loss & checkpoint Failure". Our model is a refinement [START_REF] Lamport | Computation and state machines[END_REF][START_REF] Leroy | A Formally Verified Compiler Back-End[END_REF][START_REF] Lynch | Forward and Backward Simulations[END_REF] of the specification given in Section 2. It is defined as a state machine that emits instrumented traces upon reaching specific transitions. The corresponding state machine is represented in Fig. 3. We explain below each of its transitions.

Instrumented traces. In this system, peripheral operations could be repeated either by the program -a run -or by the run-time system -due to a power failure. In order to relate precisely the trace produced by the transientlypowered system with a trace produced by a continuouslypowered execution of the system, it is crucial to distinguish (repeated) progress from failed attempts.

In the transiently-powered system, we must keep track of two kinds of information: (1) whether a power-continuous section has successfully completed or has been aborted due to a power failure; (2) whether the next snapshot could be set over the last one, or power ran out beforehand. We thus extend the notion of trace with four extra observable events: Information 1. A power-continuous section

• completed before a power-failure interrupt: Log ⊤ • or was interrupted due a power failure: Log ⊥ Information 2. The checkpointing

• completed before power ran out: Chkpt ⊤ • or could not complete before power ran out: Chkpt ⊥

In this model, an instrumented trace (written t) is thus a sequence of either of these events or peripheral actions:

PLF.trace ≜ ({Chkpt ⊤ , Chkpt ⊥ , Log ⊤ , Log ⊥ } ⊎ DEV.ops) *
In Section 4, we show that, from the traces produced by our checkpointing model, we can extract a meaningful subtrace of DEV.ops events that could have been produced by the specification, i.e., within a single run.

State machine transitions. We model interrupt-based checkpointing with peripherals through a relational specification of the transitions of the state machine in Fig. 3. The transition relation defined in Fig. 4 Transitions Usr, Drv, Enter and Leave are key to embedding the behavior of the continuous-power specification. They mirror their SPEC counterparts, in addition to retrieving (transition Enter) or storing (transition Leave) information to checkpointing storage, or to the volatile log (Drv). Crucially, transitions Enter, Drv and Leave keep the volatile log of operations in sync with the state of the physical device.

Transitions to PWR are responsible for producing a consistent checkpoint across the whole application (MCU and peripherals). Upon transition UsrPwr, the whole MCU is checkpointed so as to resume at the current program point. Upon transition DrvPwr, the volatile execution context is thrown away, relying on the fact that transition Enter has produced a valid checkpoint right before leaving user mode to enter the power-continuous section.

Transitions from state PWR to state OFF capture, nondeterministically, whether checkpointing succeeds or fails (transitions Chkpt-Succ and Chkpt-Fail). We also allow cases where power could run out before the power-failure interrupt is even raised. Therefore, in user mode, the state machine non-deterministically steps from state USR to either state PWR (transition UsrPwr) or state OFF (transition UsrOff). Similarly, in driver mode, the state machine non-deterministically steps from DRV to either state PWR (transition DrvPwr) or state OFF (transitions DrvOff). Either way, when the system restarts (transition Reboot), it reinstates the last MCU image and restores the peripheral's state thanks to the last stable log.

As a sanity check, we must validate our model against the physical objects it is supposed to represent. In particular, no volatile state is silently preserved across runs: chkpt

Log ⊥ PLF (PWR, chkpt) Chkpt-Succ chkpt ′ = CHKPT.set chkpt (PWR, chkpt) Chkpt ⊤ PLF (OFF, chkpt ′ ) Chkpt-Fail (PWR, chkpt) Chkpt ⊥ PLF (OFF, chkpt) Reboot mcu ′ = lastMcu chkpt dev ′ = LOG.restore(lastLog chkpt) chkpt ′ = CHKPT.reset chkpt (OFF, chkpt) 𝜖 PLF (USR, mcu ′ , dev ′ , chkpt ′ ) UsrOff (USR,

Correctness

Existing work only provides informal descriptions of what checkpointing is supposed to achieve, even in the simple setting of intermittent peripheral operations [START_REF] Arreola | RESTOP: Retaining External Peripheral State in Intermittently-Powered Sensor Systems[END_REF][START_REF] Berthou | Sytare: A Lightweight Kernel for NVRAM-Based Transiently-Powered Systems[END_REF][START_REF] Branco | Intermittent Asynchronous Peripheral Operations[END_REF][START_REF] Maeng | Supporting peripherals in intermittent systems with just-in-time checkpoints[END_REF].

Here, we relate our specification of intermittent computing with peripherals (Section 2) with our model of interruptbased checkpointing (Section 3). A benefit of this conceptual work is to lay out the key invariants relied upon by existing systems. Indeed, our work is unencumbered by the particulars of producing an MCU image (abstracted once and for all by MCU.t), or of logging peripheral operations (axiomatized once and for all by LOG.t), or even in the minutiae of transfering data to and from volatile and non-volatile state (axiomatized once and for all by CHKPT.t). By bringing conceptual clarity, we hope to provide a blueprint for future system designers.

Stuttering. Our correctness result consists in a semantic refinement [START_REF] Leroy | A Formally Verified Compiler Back-End[END_REF][START_REF] Lynch | Forward and Backward Simulations[END_REF] between the model and the specification.

We must prove that computation steps ŝ t Because of power failures, the model may re-execute some computation steps. In this case, the specification can simply be put on hold, waiting for the model to make actual progress. In technical terms, SPEC stutters [START_REF] Lamport | Computation and state machines[END_REF], i.e., it silently takes no step while the model performs wasted work.

Fig. 5 illustrates how we match, in our refinement proof, a given execution in PLF (top) with one in SPEC (bottom). As long as PLF is going to fail to complete the next checkpoint, the specification has to stutter. As soon as the next checkpoint is guaranteed to succeed, the execution in SPEC should be able to follow, in lockstep, the execution in PLF.

In our proof, we handle non-determinism in PLF by making the simulation relation depend on the future of the current PLF execution state.

Stuttering in SPEC must be handled with care. Indeed, we must make sure that it is not constantly stuttering: that would make our correctness theorem vacuously true. We therefore design a subtrace relation that precludes unwanted stuttering.

Subtrace relation. The cornerstone of our correctness result is a relation -≽ -∈ PLF.trace × SPEC.trace between instrumented traces and specification traces. Due to the potential re-execution of operations, only a subset of the DEV.ops event emitted by PLF might be emitted by SPEC, as it is exemplified on Fig. 5. Relation -≽thus needs to enforce a subtrace relation. Besides, we want to ensure that sequences of operations delineated by Enter/Leave are eventually executed within a single run.

Intuitively, given a trace t ∈ PLF.trace, we first filter all subtraces where the checkpointing succeeds, leading a trace containing events in {Log ⊤ , Log ⊥ } ⊎ DEV.ops, conventionally written as ť. We write ě for any such observable event. Then, within each of these subtraces, we select the events of power-continuous sections that completed without a power failure, thereby obtaining a trace 𝑡 ∈ SPEC.trace.

We hence define the subtrace relation -≽as a composition of two subtrace relations (defined in Fig. 6):

t ≽ t ⇔ ∃ ť, t ≽ Chkpt ť ∧ ť ≽ Log t
Relation -≽ Chkptdeals with re-execution of code upon a checkpointing failure (transition Chkpt-Fail), filtering out sub-sequences of events that end with Chkpt ⊥ , while retaining any other event leading to a Chkpt ⊤ . Similarly, relation -≽ Logdeals with re-execution of code upon a

t ≽ Chkpt ť ⇔ t ≽ Chkpt ⊤ ť ∨ t ≽ Chkpt ⊥ ť t ≽ Chkpt ť Chkpt ⊤ ; t ≽ Chkpt ⊤ ť t ≽ Chkpt ⊤ ť ě ; t ≽ Chkpt ⊤ ě ; ť 𝜖 ≽ Chkpt ⊥ 𝜖 t ≽ Chkpt ⊥ ť ě ; t ≽ Chkpt ⊥ ť t ≽ Chkpt ť Chkpt ⊥ ; t ≽ Chkpt ⊥ ť ť ≽ Log 𝑡 ⇔ ť ≽ Log ⊤ 𝑡 ∨ ť ≽ Log ⊥ 𝑡 ť ≽ Log 𝑡 Log ⊤ ; ť ≽ Log ⊤ 𝑡 ť ≽ Log ⊤ 𝑡 op ; ť ≽ Log ⊤ op ; 𝑡 𝜖 ≽ Log ⊥ 𝜖 ť ≽ Log ⊥ 𝑡 op ; ť ≽ Log ⊥ 𝑡 ť ≽ Log 𝑡 Log ⊥ ; ť ≽ Log ⊥ 𝑡 Figure 6
. Subtrace relations -≽ Chkptand -≽ Logpower-failure interrupt in driver mode (transition DrvPwr), filtering out sub-sequences of operations ending with a Log ⊥ , while retaining the remaining operations.

Example 4.1. In Fig. 5, the trace emitted by SPEC.sem is 𝑡 = op 1 ; op 2 ; op 3 and the trace emitted by PLF.sem is t = op 1 ; op 2 ; Log ⊥ ; Chkpt ⊤ ; op 1 ; op 2 ; op 3 ; Log ⊤ ; Chkpt ⊥ ; op 1 ; op 2 ; op 3 ; Log ⊤ ; Chkpt ⊤

We have t ≽ 𝑡 thanks to the intermediate subtrace ť = op 1 ; op 2 ; Log ⊥ ; op 1 ; op 2 ; op 3 ; Log ⊤ Indeed, we have t ≽ Chkpt ť by filtering out from t the checkpointing failure subtrace op 1 ; op 2 ; op 3 ; Log ⊤ ; Chkpt ⊥ . And ť ≽ Log 𝑡 by filtering out from ť the first aborted powercontinuous section op 1 ; op 2 ; Log ⊥ .

Example 4.2. We illustrate the precision of the -≽relation. For the trace t = op 1 ; op 2 ; op 3 ; Log ⊤ ; Chkpt ⊤ , only one trace t ∈ SPEC.trace satsifies t ≽ t, and it is t = op 1 ; op 2 ; op 3 . Only strict prefixes of t would have 𝜖 as a ≽-subtrace.

Correctness theorem. Our correctness theorem takes the form of a trace-refinement between the checkpointing model and the continuous-power specification: Theorem 4.3 (Correctness). For any trace t ∈ PLF.sem, there exists a trace t, such that t ∈ SPEC.sem and t ≽ t.

Informally, this statement reads as: "any behavior exhibited by the model (i.e., t ∈ PLF.sem) could have been observed with the specification (i.e., t ∈ SPEC.sem), ignoring the operations that had to be re-executed (i.e., t ≽ t)". The fact that power-continuous sections are indeed preserved by our model follows directly from the definition of -≽ -.

Note that Theorem 4.3 holds for any possible trace in the non-deterministic semantics of PLF. As long as the model does not progress, due to either an aborted power-continuous section or a checkpointing failure, the specification will stutter, emitting the empty trace 𝜖. However, our precise subtrace relation ensures, by its very definition, that any observable progress in PLF.sem is indeed reflected in SPEC.sem.

One difficulty in the proof of Theorem 4.3 is to decide whether SPEC needs to stutter or to make progress. It requires to know whether the next power failure will lead PLF to re-executing that portion of the execution. To handle this difficulty, we introduce an auxiliary oracle-semantics: nondeterminism is replaced by an oracle determining how the state machine behaves. We prove the existence of such an oracle for any possible execution in PLF.sem, and prove that the specification can simulate any possible oracle. Further details of the proof can be found in our Coq development [START_REF] Berthou | Intermittent Computing with Peripherals, Formally Verified -Companion Coq Development[END_REF].

Applications

We now relate our model to propositions from the literature, illustrating how they fit within our conceptual framework.

Restop [START_REF] Arreola | RESTOP: Retaining External Peripheral State in Intermittently-Powered Sensor Systems[END_REF]. Restop is a middleware supporting peripherals in a transiently-powered context. It specifically targets devices connected through SPI and I 2 C buses. The authors define the notion of a "peripheral instruction" ([2, §3]), akin to our set of operations (DEV.ops), as the "information required by the system to issue the operation on the peripheral".

At run-time, peripheral instructions are stored in an "instruction history table", which effectively implements our LOG.t interface as a sequence of instructions to be replayed on reboot. To keep the size of this log to a minimum, instructions are equipped with a choice of 4 semantics ([2, §3.1]): "not-save", "save", "save-but-replace", "preserve". The choice of a particular semantics reflects the effect of the instruction on the peripheral (e.g., save-but-replace expects the operation to overwrite the effect of a previous instance).

The Restop designers do not commit to a specific checkpointing scheme ("the history table can either be: (1) placed in main memory; or (2) directly located in NVM" [2, §3]). Similarly, our model supports both: our LOG.t interface leaves unspecified whether the log is physically maintained in volatile or non-volatile memory.

Sytare [START_REF] Berthou | Sytare: A Lightweight Kernel for NVRAM-Based Transiently-Powered Systems[END_REF]. Sytare is a library operating system targeting a wide range of peripherals in a transiently-powered context. Interactions with the peripherals are mediated by a system call interface ("syscall") delineating sequences of instructions allowed to interact with peripherals ("drivers", running in "kernel mode") from application code (running in "user mode"), which may only access volatile memory. The syscall interface enables the OS implementers to maintain a distinct "kernel stack" when interacting with peripherals. As a result, the system can always backtrack to the entry point of a syscall by throwing away this stack. This allows them to easily replay a syscall as a single unit of code, thus providing a power-continous section mechanism.

Sytare supports any peripheral as long as it registers an API through the syscall mechanism and exposes a "device context". A device context is a C data-structure (a struct) that records device-specific data necessary to reconfigure it upon reboot. Each operation exposed to the syscall interface updates the device context accordingly. The collection of peripherals thus defines an array of device contexts, which all together amount to our LOG.t interface. As witnessed by Fig. 4 of Berthou et al. [START_REF] Berthou | Sytare: A Lightweight Kernel for NVRAM-Based Transiently-Powered Systems[END_REF], Sytare naturally fits our model.

Karma [START_REF] Branco | Intermittent Asynchronous Peripheral Operations[END_REF]. Karma provides a run-time system to ensure consistency of peripheral state across reboots. Karma provides a mechanism to implement power-continuous sections, dubbed "atomicity" there, stating that "two options exist to integrate Karma with such a system support: i) changing the conditions that make checkpoints take place in a way to prevent executions lacking the required atomicity, or ii) rolling back executions to recover the non-atomic cases" [9, §C.2].

No assumption is made on how checkpoints are triggered (statically or dynamically). Karma proposes, in addition, an integrated task scheduler for user tasks and peripheral state updates. A peripheral state is represented by a state machine and a queue of operations that corresponds to our DEV.ops operations. After a power failure, peripheral state is restored by replaying the operations stored in the queue. To ensure atomicity of peripheral updates, Karma proposes, as Sytare does, a wrapper for peripheral driver functions. But instead of storing a device context, a procedure rolls back the code, which effectively implements power-continuous sections.

Unlike Sytare, Karma allows several tasks to access a peripheral. This is achieved through a dedicated task management system, which amounts to a specific "user mode" program, running in U mode in our model. From our formal standpoint, the difference between Sytare and Karma thus lies solely in how they instantiate (i.e., implement) the transition relation of the specification abstract machine: the former only allows the execution of a single main task whereas the latter supports several concurrent tasks. This difference is orthogonal to power failures.

Failure-atomicity run-times. In the general case, i.e., distributed systems with volatile and non-volatile RAM, ensuring correctness and consistency of execution is a complex problem because volatile and non-volatile memories are out of sync after a crash [START_REF] Shull | Defining a high-level programming model for emerging NVRAM technologies[END_REF]. New programming models are proposed using locks [START_REF] Boehm | Persistence Programming Models for Non-Volatile Memory[END_REF][START_REF] Dhruva | Atlas: Leveraging Locks for Non-Volatile Memory Consistency[END_REF] or extended transactional memory [START_REF] Coburn | NV-Heaps: Making Persistent Objects Fast and Safe with next-Generation, Non-Volatile Memories[END_REF]. These legacy software systems provide minimally invasive change to programming models and environments, hence they propose concurrency-like abstractions. These concepts have been used in the context of low-power transiently-powered sensors [START_REF] Lucia | A simpler, safer programming and execution model for intermittent systems[END_REF][START_REF] Ruppel | Transactional concurrency control for intermittent, energy-harvesting computing systems[END_REF] that use NVM both for checkpointing and for regular program storage. Currently, our specification SPEC does not account for NVM state, hence we cannot model applications that assume that part of the program memory, e.g., a stack, is in NVM.

Static and Interrupt-based checkpointing. Following the development of NVM and harvesting technologies [START_REF] Colin | A Reconfigurable Energy Storage Architecture for Energy-harvesting Devices[END_REF][START_REF] Hester | Timely Execution on Intermittently Powered Batteryless Sensors[END_REF][START_REF] Lee | A Modular 1 mm 3 Die-Stacked Sensing Platform With Low Power I 2 C Inter-Die Communication and Multi-Modal Energy Harvesting[END_REF][START_REF] Alanson | Design of an RFID-Based Battery-Free Programmable Sensing Platform[END_REF], numerous systems have been proposed to allow low-power sensors to be deployed in transiently-powered environments. Among the most well-known are chronologically: Mementos [START_REF] Ransford | Mementos: system support for long-running computation on RFID-scale devices[END_REF], QuickRecall [START_REF] Jayakumar | QuickRecall: A HW/SW Approach for Computing across Power Cycles in Transiently Powered Computers[END_REF], Hibernus [START_REF] Balsamo | Hibernus: Sustaining Computation During Intermittent Supply for Energy-Harvesting Systems[END_REF], Dino [START_REF] Lucia | A simpler, safer programming and execution model for intermittent systems[END_REF], Ratchet [START_REF] Van Der Woude | Intermittent Computation without Hardware Support or Programmer Intervention[END_REF], HarvOS [START_REF] Anwar | HarvOS: Efficient Code Instrumentation for Transiently-Powered Embedded Sensing[END_REF], Clank [START_REF] Hicks | Clank: Architectural Support for Intermittent Computation[END_REF], Alpaca [START_REF] Maeng | Alpaca: intermittent execution without checkpoints[END_REF] and Coati [START_REF] Ruppel | Transactional concurrency control for intermittent, energy-harvesting computing systems[END_REF]. Most of these systems used checkpointing. The insertion of checkpoints can be static [START_REF] Anwar | HarvOS: Efficient Code Instrumentation for Transiently-Powered Embedded Sensing[END_REF][START_REF] Lucia | A simpler, safer programming and execution model for intermittent systems[END_REF], dynamic [START_REF] Maeng | Adaptive Dynamic Checkpointing for Safe Efficient Intermittent Computing[END_REF][START_REF] Van Der Woude | Intermittent Computation without Hardware Support or Programmer Intervention[END_REF] or, when power failures can be detected by voltage drop, interrupt-based [START_REF] Balsamo | Hibernus: Sustaining Computation During Intermittent Supply for Energy-Harvesting Systems[END_REF][START_REF] Berthou | Sytare: A Lightweight Kernel for NVRAM-Based Transiently-Powered Systems[END_REF][START_REF] Jayakumar | QuickRecall: A HW/SW Approach for Computing across Power Cycles in Transiently Powered Computers[END_REF]. The IBIS tool suite [START_REF] Surbatovich | I/O dependent idempotence bugs in intermittent systems[END_REF] is able to detect, statically or dynamically, memory inconsistencies that may occur in these applications without relying on Assumption (A1) (i.e., the MCU may directly manipulate NVM).

Handling peripherals. Peripherals are not handled by classical checkpointing techniques. Peripherals are very important in embedded computing and there is also, as for memory, a state consistency problem when power is lost [START_REF] Lucia | A simpler, safer programming and execution model for intermittent systems[END_REF][START_REF] Maeng | Supporting peripherals in intermittent systems with just-in-time checkpoints[END_REF]. Few systems have proposed a complete mechanism to ensure peripheral device restoration.

Sytare [START_REF] Berthou | Peripheral state persistence for transientlypowered systems[END_REF][START_REF] Berthou | Sytare: A Lightweight Kernel for NVRAM-Based Transiently-Powered Systems[END_REF] proposed a solution to recover the state of both the processor and the peripherals. Restop [START_REF] Arreola | RESTOP: Retaining External Peripheral State in Intermittently-Powered Sensor Systems[END_REF] solves a similar problem with a middleware library for off-chip peripherals accessed by SPI or I 2 C. Karma [START_REF] Branco | Intermittent Asynchronous Peripheral Operations[END_REF] proposes another implementation. These three approaches are captured by our checkpointing model and can benefit from the modeling proposed here to verify their correctness.

Samoyed [START_REF] Maeng | Supporting peripherals in intermittent systems with just-in-time checkpoints[END_REF] proposes, under some restrictions (no interrupt allowed, stateless peripherals) to ensure peripheral state consistency by introducing user-controlled atomicity. This work makes use of NVM in application code, and hence is not captured by our current model.

Formal models, correctness proofs. Chen et al. [START_REF] Chen | Specifying Crash Safety for Storage Systems[END_REF] discuss some approaches for specifying and certifying crashsafety for a persistent file system. The FSCQ system they later verified [START_REF] Chen | Using Crash Hoare Logic for Certifying the FSCQ File System[END_REF] uses a Hoare-logic style for specifying the system: crash conditions specify the disk state right before a crash, and a recovery procedure ensures the absence of data loss. A first difference between this line of work and ours is that we consider crash-safety in systems handling peripherals. A second difference is in the general specification methodology. We adopt the so-called DSL approach [START_REF] Chen | Specifying Crash Safety for Storage Systems[END_REF]: we phrase the specification and the model in terms of state machines and prove a refinement between the two. Chajed et al. [START_REF] Chajed | Verifying Concurrent, Crash-Safe Systems with Perennial[END_REF] also derive a refinement result from the Hoare-logic style specification. As they do not handle peripherals, their refinement is a simple trace inclusion. In contrast, to derive a useful and precise correctness result, we must resort to a subtrace relation. Koskinen and Yang [21] also employ a DSL approach. Interestingly, their notion of recoverability is expressed in terms of an un-crashed program: after a crash, the program will eventually reach a state that simulates another state that an un-crashed program already reached (i.e., in the trace prefix). In our model, instrumented traces and the subtrace relation help us state simply to which prefix it corresponds.

Another line of work focuses on proving the linearizability of fine-grained concurrent data-structures subject to wholesystem crash [START_REF] Derrick | Verifying Correctness of Persistent Concurrent Data Structures[END_REF][START_REF] Izraelevitz | Linearizability of Persistent Memory Objects Under a Full-System-Crash Failure Model[END_REF]. Durable linearizability requires that upon a crash, only completed operations are guaranteed to remain visible. Buffered durable linearizability expresses that the state after the crash must be consistent, but not necessarily up-to-date. Our subtrace refinement result is similar in spirit to a buffered durable linearization property.

Conclusion

We proposed a specification of intermittent computing with peripherals, together with a model of interrupt-based checkpointing that ensures the consistency of the whole system, i.e., including peripherals, after reboot. Our model contains the minimal conditions that an implementation of checkpointing should satisfy to handle correctly peripherals. We formally proved the correctness of our model: behaviors of intermittent executions are as prescribed by a continuouslypowered specification, modulo the necessary replays of certain peripheral operations, due to reboots. Finally, we showed that our model captures three proposals satisfying our working assumptions (A1-4): Restop [START_REF] Arreola | RESTOP: Retaining External Peripheral State in Intermittently-Powered Sensor Systems[END_REF], Sytare [START_REF] Berthou | Sytare: A Lightweight Kernel for NVRAM-Based Transiently-Powered Systems[END_REF] and Karma [START_REF] Branco | Intermittent Asynchronous Peripheral Operations[END_REF].

Throughout this work, we have assumed that the application code does not interact with non-volatile memory (A1). We are currently working on extending our specification and our checkpointing model to account for NVM application state. This would allow us to model more systems from the literature [START_REF] Hicks | Clank: Architectural Support for Intermittent Computation[END_REF][START_REF] Lucia | A simpler, safer programming and execution model for intermittent systems[END_REF][START_REF] Maeng | Alpaca: intermittent execution without checkpoints[END_REF][START_REF] Maeng | Supporting peripherals in intermittent systems with just-in-time checkpoints[END_REF][START_REF] Van Der Woude | Intermittent Computation without Hardware Support or Programmer Intervention[END_REF].

Figure 1 .

 1 Figure 1. The checkpointing model (PLF) implements its continuous-power specification (SPEC)

  .t × DEV.ops × DEV.t where dev op DEV dev ′ denotes the execution of operation op in device state dev and resulting in device state dev ′ .

PLF

  ŝ′ in the model correspond to computation steps in the specification s t SPEC s ′ -which executes in a continuously-powered environment.

Figure 5 -

 5 Figure 5. Matching --SPEC

  Specification state machine the sequential execution of the trace t = op 0 ; . . . ; op 𝑛 starting from device state dev, resulting in device state dev ′ . Intermittent computations are described axiomatically. The state of the computation SPEC.state ≜ SPEC.mode × MCU.t × DEV.t consists of a mode, an MCU state and a device state. We write s ∈ SPEC.state to denote an arbitrary state. The execution of a program is specified through a single-step transition relation -

		Enter
	Usr	(U, mcu, dev)	(D, mcu, dev)	Drv
		Leave
		Figure 2.
				op 𝑛 DEV	dev ′ ,

t DEV * dev ′ ≜ dev op 0 DEV dev 0 . . . -SPEC -⊆ SPEC.state × SPEC.trace × SPEC.state that takes an input state to produce a (possibly empty) trace of observable events and a resulting state. This relation is subject to the following invariants. (Axiom-Usr): In user mode, computations do not interact with peripherals, i.e., if (U, mcu, dev) t SPEC (U, mcu ′ , dev ′ ), then dev = dev ′ and t = 𝜖; (Axiom-Drv): In driver mode, the emitted trace faithfully describes the physical evolution of the device, i.e., if (D, mcu, dev) t SPEC (D, mcu ′ , dev ′ ), then dev t DEV * dev ′ ; (Axiom-Enter): Transitions from user to driver mode are computationally transparent, i.e., if (U, mcu, dev) t SPEC (D, mcu ′ , dev ′ ), then mcu = mcu ′ , dev = dev ′ and t = 𝜖; (Axiom-Leave): Transitions from driver to user mode are computationally transparent, i.e., if

  LOG.log ∈ DEV.ops → LOG.t → LOG.t. Restoring the log, through the function LOG.restore ∈ LOG.t → DEV.t, allows recreating a peripheral state ex nihilo by replaying the log. We denote LOG.init ∈ LOG.t the initial state of the log. We write ℓ ∈ LOG.t to denote an arbitrary log. We require that function LOG.restore be consistent with LOG.init and LOG.log: (Axiom-Restore-Init) Restoring the initial log yields the initial state, i.e., LOG.restore LOG.init = DEV.init; (Axiom-Restore-Log) Given a log that faithfully represents a given device, restoring the extension of this log with a new operation gives the same peripheral state as the one obtained by running the operation on the peripheral, i.e., for all ℓ ∈ LOG.t, dev, dev ′ ∈ DEV.t, op ∈ DEV.ops, if LOG.restore ℓ = dev and dev

op DEV dev ′ , then LOG.restore (LOG.log op ℓ) = dev ′ .

  access the last snapshot through the function last ∈ CHKPT.t → MCU.t×LOG.t, and the next snapshot through next ∈ CHKPT.t → MCU.t × LOG.t. For conciseness, we also define lastMcu, lastLog, nextMcu and nextLog to directly access each individual components. The initial checkpoint CHKPT.init ∈ CHKPT.t is constructed from the image of the initial MCU and the initial log, i.e., it satisfies the equations last CHKPT.init = (MCU.init, LOG.init) and next CHKPT.init = (MCU.init, LOG.init). Double-buffering requires two operations. First, one must be able to overwrite atomically the last stable snapshot with the on-going one, effectively committing the on-going snapshot. This is provided by function CHKPT.set ∈ CHKPT.t → CHKPT.t. Second, one must be able to overwrite atomically the on-going snapshot with the last valid one, effectively resetting the on-going snapshot to the last valid one. This is provided by CHKPT.reset ∈ CHKPT.t → CHKPT.t. These functions are specified through a set of equations: last (CHKPT.set chkpt) = next chkpt next (CHKPT.set chkpt) = next chkpt next (CHKPT.reset chkpt) = last chkpt last (CHKPT.reset chkpt) = last chkpt Finally, one must be able to update the MCU image or the log stored in the next snapshot. This is respectively achieved by function CHKPT.saveNextMcu ∈ CHKPT.t → MCU.t → CHKPT.t and function CHKPT.saveNextLog ∈ CHKPT.t → LOG.t → CHKPT.t, characterized by:

  mcu, dev, chkpt) Our model faithfully accounts for checkpointing failure: Chkpt-Fail keeps the checkpointing storage intact. Our model supports power-failure interruptions in both user and driver mode. It also models the eventuality that the powerfailure interruption itself cannot complete before power goes out, through UsrOff and DrvOff. Finally, traces produced by the transition system merely record the execution, i.e., they play no role in the execution.

	Chkpt ⊥	Chkpt ⊥

PLF (OFF, chkpt) DrvOff (DRV, mcu, dev, chkpt, ℓ) PLF (OFF, chkpt)

Figure 4. Interrupt-based checkpointing model --PLF is the only piece of data that goes through OFF. Further, the physical device state, DEV.t, cannot magically be captured in non-volatile memory: only MCU.t and LOG.t can be used to produce CHKPT.t and none of these can contain a DEV.t.

Acknowledgments

We would like to thank the anonymous reviewers for their thoughtful comments. This work was supported by Inria (IPL ZEP) and the Émergence(s) program of the City of Paris.