Clément Mailhé

Stéphane Gorsse

Boèce Thirion

Elena Palomo

Marie Duquesne

High-throughput experiment for the rapid screening of organic phase change materials

Keywords: Infrared thermography, Phase diagram, DSC, Ternary systems, Eutectic transition

Introduction

Phase diagrams are essential tools in materials science. They define areas of existence of phases according to pressure, temperature, and chemical composition for pure and multi-component systems of materials [START_REF] Campbell | Phase Diagrams: Understanding the Basics[END_REF]. Their establishment hence provides valuable information to the scientist, often decisive depending on the field of application [START_REF] Dubost | Industrial applications and determination of equilibrium phase diagrams for light alloys[END_REF][START_REF] Research | Applications of Phase Diagrams in Metallurgy and Ceramics: Proceedings of a Workshop Held at the National Bureau of Standards[END_REF][START_REF] Pelton | Thermodynamics and phase diagrams of materials Phase transform mater[END_REF]. Standard experimental methods are categorized as either static or dynamic and rely on the observation of a material property (structural, physical, thermal, chemical …) at different temperature levels (static) or during a temperature profile (dynamic) [START_REF] Inden | Experimental determination of phase diagrams[END_REF]. For multi-component systems of materials, the determination of an accurate phase diagram requires a large number of experiments making the phase diagram establishment process a rather time-consuming task. Indeed, traditional methods are only able to perform single sample characterization which is not competitive in an industrial development context. The use of phase change materials (PCM) in thermal energy storage (TES) is a good example to illustrate the benefits of phase diagrams. Indeed, the thermal behavior and melting temperature of PCMs are critical properties that can be tailored using blends instead of single component PCMs. It is then of great importance with respect to the performance of finding blends without solidification interval, i.e. with congruent melting or eutectic. Therefore, phase diagrams are the road map to select blends with the desired melting temperature and solidification behavior. However, the exploration of the vast compositional space of multicomponent systems requires a large number of samples (e.g. 231 for a ternary system and 1771 for quaternary system with a 5 mol% step increment) [START_REF] Gorsse | From high-entropy alloys to complex concentrated alloys[END_REF]. To speed up the exploration, we need high throughput techniques that can be automated, parallelized, and miniaturized [START_REF] Miracle | New strategies and tests to accelerate discovery and development of multi-principal element structural alloys[END_REF], which is not the case for the most common techniques being used such as differential scanning calorimetry (DSC), differential thermal analysis (DTA), or X-ray powder diffraction (XRD) [START_REF] Campbell | Phase Diagrams: Understanding the Basics[END_REF][START_REF] Dubost | Industrial applications and determination of equilibrium phase diagrams for light alloys[END_REF][START_REF] Inden | Experimental determination of phase diagrams[END_REF][START_REF] Höhne | Differential Scanning Calorimetry: An Introduction for Practitioners[END_REF][START_REF] Sarge | Calorimetry: fundamentals, instrumentation and applications[END_REF][START_REF][END_REF][START_REF] Lewis | Fourier transform infrared spectroscopy in the study of lipid phase transitions in model and biological membranes: practical considerations[END_REF][START_REF] Zheng | An infrared spectroscopy study of the phase transition in solid ammonia[END_REF]. To address this issue, modeling tools are commonly employed to predict multi-component phase diagrams from known lower-order subcomponent systems [START_REF] Kroupa | Modelling of phase diagrams and thermodynamic properties using Calphad method-development of thermodynamic databases[END_REF][START_REF] Kattner | The Calphad method and its role in material and process development[END_REF]. While this approach is well developed for metals and alloys, organic materials are still poorly described in the literature and thermodynamic databases are not currently available for these systems. In order to overcome the limits of traditional methods, a high throughput technique based on infrared thermography (IRT method) was developed. Its application for the assessment of binary phase diagrams has shown interesting results for mixtures of sugar alcohols [START_REF] Del Barrio | Infrared thermography method for fast estimation of phase diagrams[END_REF] and of fatty acids and fatty alcohols [START_REF] Mailhé | Phase diagrams of fatty acids as biosourced phase change materials for thermal energy storage[END_REF], respectively [START_REF] Del Barrio | Infrared thermography method for fast estimation of phase diagrams[END_REF][START_REF] Mailhé | Phase diagrams of fatty acids as biosourced phase change materials for thermal energy storage[END_REF]. It allowed for the rapid screening of the liquidus temperature in a single 2-h experiment while traditional methods would require weeks of measurements. Due to its promising aspect, the method is currently undergoing a campaign of parametric studies [START_REF] Mailhé | Improved infrared thermography method for fast estimation of complex phase diagrams[END_REF][START_REF] Mailhé | Performance analysis of the infrared thermography method for complex phase diagrams estimation[END_REF][START_REF] Mailhé | A fast and low-cost dynamic calorimetric method for phase diagram estimation of binary systems[END_REF] to enhance and optimize its performance. As the more components, a system includes the more timeconsuming the phase diagram establishment process is, the IRT method might be of increasing interest with the growing complexity of the system.

In this paper, we present high-throughput experiments that allow simultaneous measurement of the liquid-solid transition temperatures of several blends, and to quickly establish the liquidus surface of multi-component systems. Our method combines materials libraries with discrete compositions and rapid tests enabling to accelerate the screening tests. This approach is applied to the fatty acids (FA) ternary system with Lauric acid, Myristic acid, and Palmitic acid. The validity of the results is discussed by comparison with DSC measurements and with data from the literature.

Materials and methods

Materials

The ternary system studied in this work is the Lauric acid + Myristic acid + Palmitic acid system. Information regarding the properties of the pure compounds is given in Table 1. Indicated melting temperatures and their corresponding standard deviation are obtained by DSC following the protocol described hereafter. Temperature ranges found in the literature [START_REF] Kenisarin | Thermophysical properties of some organic phase change materials for latent heat storage. A review[END_REF][START_REF] Maximo | On the solid-liquid equilibrium of binary mixtures of fatty alcohols and fatty acids[END_REF][START_REF] Costa | Solid-liquid equilibrium of binary fatty acid mixtures[END_REF][START_REF] Zhang | Thermophysical properties of some fatty acids/surfactants as phase change slurries for thermal energy storage[END_REF][START_REF] Kahwaji | Fatty acids and related phase change materials for reliable thermal energy storage at moderate temperatures[END_REF][START_REF] Zhang | Thermal studies on the solid-liquid phase transition in binary systems of fatty acids[END_REF][START_REF] Cedeño | Measurements of temperature and melting heat of some pure fatty acids and their binary and ternary mixtures by differential scanning calorimetry[END_REF][START_REF] Schaake | Thermodynamic properties of the normal alkanoic acids II. Molar heat capacities of seven even-numbered normal alkanoic acids[END_REF][START_REF] Hobi Bordón Sosa | Solid-liquid equilibrium of binary systems containing fatty acids and fatty alcohols using differential scanning calorimetry[END_REF][START_REF] Han | Thermal properties and stabilities of the eutectic mixture: 1,6-hexanediol/lauric acid as a phase change material for thermal energy storage[END_REF] are also stated for comparison.

Each binary system obtainable from the 3 materials considered has already been studied with the IRT method [START_REF] Duquesne | Biosourced organic materials for latent heat storage: An economic and ecofriendly alternative[END_REF][START_REF] Mailhé | Applications of an infrared thermography method for solid-liquid equilibria modeling of organic binary systems[END_REF] and the results obtained have been validated by comparison with DSC measurements and literature data. With a 5 mol% increment, the number of samples to be studied is 231 (171 to be studied in this work and the 60 other samples being studied for the establishment of the binary systems phase diagrams in previous work [START_REF] Duquesne | Biosourced organic materials for latent heat storage: An economic and ecofriendly alternative[END_REF][START_REF] Mailhé | Applications of an infrared thermography method for solid-liquid equilibria modeling of organic binary systems[END_REF]). Although this number may still appear high for standard methods such as DSC, analyzing all the samples can be managed in a matter of hours with the IRT method.

The preparation of each sample is made using a MET-TLER TOLEDO weighing scale with a 0.03 mg uncertainty. Batches of 200 mg are prepared by first weighing the first compound in its solidified form after being melted in an aluminum weighing pan and then weighing the second compound following the same process.

IRT method

A recent innovative high-throughput technique based on infrared thermography has recently proven to be particularly adapted for the fast establishment of phase diagrams of binary systems of organic materials [START_REF] Del Barrio | Infrared thermography method for fast estimation of phase diagrams[END_REF][START_REF] Mailhé | Phase diagrams of fatty acids as biosourced phase change materials for thermal energy storage[END_REF][START_REF] Mailhé | Improved infrared thermography method for fast estimation of complex phase diagrams[END_REF][START_REF] Mailhé | Performance analysis of the infrared thermography method for complex phase diagrams estimation[END_REF][START_REF] Mailhé | A fast and low-cost dynamic calorimetric method for phase diagram estimation of binary systems[END_REF][START_REF] Mailhé | Applications of an infrared thermography method for solid-liquid equilibria modeling of organic binary systems[END_REF]. The infrared thermography (IRT) method has successfully provided the phase diagrams of sugar alcohols, fatty acids, and fatty alcohols binary systems in a single experiment of less than two hours. Its advantage resides in its ability to study multiple samples at a time, hence greatly accelerating the step of phase change characterization. The process of phase diagram establishment requires the study of an extensive amount of compositions. If for binary systems a reliable determination can be made based on a manageable number of samples, the requirements become increasingly demanding as new compounds are added to the system. In that frame, the IRT method, whose efficiency has already been demonstrated for binary systems [START_REF] Del Barrio | Infrared thermography method for fast estimation of phase diagrams[END_REF][START_REF] Mailhé | Phase diagrams of fatty acids as biosourced phase change materials for thermal energy storage[END_REF][START_REF] Mailhé | Improved infrared thermography method for fast estimation of complex phase diagrams[END_REF][START_REF] Mailhé | Performance analysis of the infrared thermography method for complex phase diagrams estimation[END_REF][START_REF] Mailhé | A fast and low-cost dynamic calorimetric method for phase diagram estimation of binary systems[END_REF][START_REF] Mailhé | Applications of an infrared thermography method for solid-liquid equilibria modeling of organic binary systems[END_REF], could prove to be of great interest for the phase diagram establishment of systems including more than two compounds. It could also effectively participate in the large gathering of experimental data, supplying modeling databases with useful information regarding organic materials. The principle of the method has been thoroughly described in [START_REF] Del Barrio | Infrared thermography method for fast estimation of phase diagrams[END_REF] resulting from various studies [START_REF] Duquesne | Experimental analysis of heterogeneous nucleation in undercooled melts by infrared thermography[END_REF] dedicated to the study of phase transition processes for the study and development of phase change materials. The presented experimental parameters have been chosen according to the results obtained in these previous studies. The readers are encouraged to consult these studies for an in-depth understanding of the choices made regarding the operating conditions. Multiple samples of the system of materials are deposited in the form of droplets onto a thermally conductive plate. This plate is then submitted to a slow heating ramp monitored with a thermocouple placed on the support plate. In this study, the heating rate is set at 1 °C min -1 from 20 to 75 °C in order to encompass the majority of occurring transitions. An infrared camera placed above the plate simultaneously records the thermal scene as the samples are submitted to the ramp. The camera used in this work is the FLIR X6580SC, and the acquisition rate is set at 7 Hz. An image sequence is then obtained containing the data of 30 to 40 samples at a time in a single experiment lasting less than 2 h. Considering the 5 mol% increment chosen for this work, the 171 samples can all be studied within 12 h of experiments. Figure 1 presents a scheme of the experimental setup.

As only the data of the samples is useful and as each sample is represented by hundreds of pixels, image, and signal processing techniques are applied prior to analyzing the data in order to facilitate the interpretation of the results. As explained in [START_REF] Del Barrio | Infrared thermography method for fast estimation of phase diagrams[END_REF], the structure modifications occurring during the phase change process induce a variation of the emissivity of the material. This change in emissivity can then be noticed in the infrared signal recorded by the camera and consequently lead to the identification of phase transitions. The detail of applied processes is available in [START_REF] Del Barrio | Infrared thermography method for fast estimation of phase diagrams[END_REF]. Following their implementation, the data interpretation for each sample consists in detecting abrupt trend changes in 2-3 eigenfunctions, attributed to phase transitions. The eigenfunctions are obtained through a singular value decomposition (SVD), which is a common tool in signal processing when dealing with large multi-variable datasets that allow separating variables and highlighting variations in the raw data.

Figure 2a shows the raw infrared signals for a sample of pure Palmitic acid. As is, the signals are not manageable and cannot allow for a reliable interpretation of transition temperatures. In that case, a transition can either be misplaced or lost in the great amount of data gathered. After SVD, we notice in Fig. 2b that the first three eigenfunctions show easily identifiable variations which greatly facilitates the interpretation. As demonstrated in [START_REF] Del Barrio | Infrared thermography method for fast estimation of phase diagrams[END_REF], the first three eigenfunctions are sufficient to detect most occurring transitions, the first eigenfunction generally being a representation of the average signal while the other two express variations from it. This consideration is all the more valid when several transitions occurring successively have to be distinguished in the cluster of data (which is often the case for mixture samples).

Validation

The IRT method is an emerging technique whose results are to be validated by measurements obtained by established standard methods. The most commonly used for phase diagram establishment is DSC. It is consequently the technique used in this work to validate the results obtained with the IRT method as well as the results extracted from literature.

The device used is a DSC 131 model provided by SETARAM, calibrated for reliable measurements in the 20-330 °C range using Gallium (Purity: 99.9999%), Indium (Purity: 99.995%), Tin (Purity: 99.999%), and Lead (Purity: 99.999%). The samples passing through the DSC come from the same batches used for the samples of the IRT experiment. A total of 22 compositions are chosen in order to provide an adequate depiction of the ternary phase diagram as analyzing all the samples studied in the IRT experiment would not be possible due to the time-consuming aspect of the DSC. For each sample, a mass between 10 and 15 mg is weighed and placed in 30 µL aluminum crucibles and 3 heating-cooling cycles are performed at 1 °C min -1 in order to match the operating conditions of the IRT method. Each cycle begins at 20 °C and ends at 75 °C to be sure encompass most occurring transitions. The first cycle is used The interpretation of the DSC curves is made based on the guidelines in [START_REF] Boettinger | NIST Recommended practice guide: DTA and heat-flux DSC measurements of alloy melting and freezing[END_REF] stating that for transitions temperatures, the onset temperature is considered if a clear baseline can be identified and the peak temperature is chosen otherwise.

The liquidus temperatures for 22 blends extracted from IRT and DSC, respectively, are compared in Fig. 3. This graphical representation highlights the good agreement that has been found so far between both techniques.

Results and discussion

Figure 4a shows the complex surface connecting the 231 liquidus temperatures obtained by IRT for the LA + MA + PA ternary system. In ternary systems, the liquidus surface bounds two-phase Liquid + Solid (L + S) fields. Considering that the binary sub-systems involved in this ternary include eutectic and peritectic reactions [START_REF] Duquesne | Biosourced organic materials for latent heat storage: An economic and ecofriendly alternative[END_REF][START_REF] Costa | The solid-liquid phase diagrams of binary mixtures of even saturated fatty acids differing by six carbon atoms[END_REF][START_REF] Costa | The solid-liquid phase diagrams of binary mixtures of consecutive, even saturated fatty acids[END_REF][START_REF] Costa | The solid-liquid phase diagrams of binary mixtures of consecutive, even saturated fatty acids: differing by four carbon atoms[END_REF], there are numerous twophase regions (L + S) whose edges meet to form a common line bounding three-phase regions. The most obvious that can be identified in Fig. 4a is the eutectic valleys emerging from the neighboring binary eutectic reactions L = LA + PA, L = LA + MA, and L = MA + PA. Another interesting feature in Fig. 4a is the presence of a minimum at around 32 °C corresponding to the lowest melting point of the ternary system at 70 mol%LA + 20 mol%MA + 10 mol%PA. This reveals the occurrence of either an isomorphous congruent minimum melting or a ternary eutectic reaction L = LA + MA + PA.

In addition to the liquidus surface, the IRT method evidenced isothermal transitions spanning over large composition ranges at around 32, 37, and 51 °C (Fig. 4b). In ternary systems, 2-dimensional isothermal regions connect the compositions of phases participating in four-phase equilibriums. Even though it is not possible to extract the compositions of the phases from Fig. 4b, the isotherm detected at around 32 °C in the LA-rich compositional space allows discriminating the type of phase transition that occurs at this minimum melting temperature as a ternary eutectic transformation. The nature of the other ternary four-phase equilibrium at 37 and 51 °C cannot be determined with the current data, however, the peritectic reactions extending from the binary sub-systems suggest that ternary four-phase equilibrium are class II, i.e. intermediate between eutectic and peritectic equilibriums, and/or class III, i.e. ternary equivalent of peritectic equilibrium. The work presented in [START_REF] Ke | Phase diagrams, eutectic mass ratios and thermal energy storage properties of multiple fatty acid eutectics as novel solidliquid phase change materials for storage and retrieval of thermal energy[END_REF] shows a DSC-determined ternary eutectic composition of 67.13 mol%LA + 22.83 mo l%MA + 10.05 mol%PA with a melting point around 31 °C. Further DSC analyses aiming at corroborating the observations made with the IRT method, confirm the existence of a eutectic reaction at this composition (67 mol%LA + 23 mol %MA + 10 mol%PA) and with a melting point matching the one obtained with IRT (Table 2). In addition, the previously mentioned 37 °C isothermal region has successfully been retrieved with DSC measurements, at a temperature level consistent with IRT observations. On the other hand, the thermal event at 51 °C is only detected with the IRT method. The detection appears to be rather reliable considering the small standard deviation but its presence cannot yet be confirmed by DSC. This detection is however, not surprising as similar observations are also made for the binary systems in previous works [START_REF] Duquesne | Biosourced organic materials for latent heat storage: An economic and ecofriendly alternative[END_REF][START_REF] Mailhé | Applications of an infrared thermography method for solid-liquid equilibria modeling of organic binary systems[END_REF].

The author in [START_REF] Ke | Phase diagrams, eutectic mass ratios and thermal energy storage properties of multiple fatty acid eutectics as novel solidliquid phase change materials for storage and retrieval of thermal energy[END_REF] attempts predicting eutectic compositions of multi-compounds systems with thermodynamic modeling. For this system, the predicted eutectic composition for this system was 58.69 mol%LA + 28.68 mol%MA + 12.63 mol%PA which is far off the actual composition determined experimentally. This deviation highlights the limits of modeling techniques and the need for cost-effective and time-efficient experimental methods such as IRT.

With the encouraging results obtained for the establishment of a ternary phase diagram with the IRT method, we can conclude that this method can allow the rapid and efficient screening of complex multi-component systems. The transition detection with the IRT method indeed appears to be quite reliable with a retrieved liquidus showing no discontinuities and isothermal regions detected with acceptable standard deviations, within range of standard DSC measurements and spanning over several distinct With T tr1 the average transition temperature of transition n°1 in °C, tr1 the standard deviation of the transition temperature for the transition n°1 and the n number of samples for which the transition has been detected

experiments. Now that the proof of concept is done, we can proceed to the screening of other ternary / quaternary systems in order to explore their employability in various applications

Conclusions

In this work, we have shown that the IRT method is an effective high-throughput technique allowing the automatic, rapid, and low-cost characterization of a broad spectrum of discrete compositions of a blend. It has been successfully implemented for the rapid screening of an LA + MA + PA ternary blend. Its phase diagram obtained in this work consisted of 171 data sets obtained in less than 12 h of experiments which is considerably less than the time that would have been required with the use of standard methods (weeks/ months). An isotherm detected around 32 °C in the LA-rich compositional space suggested the occurrence of a ternary eutectic reaction whose location, both in terms of temperature and composition, was confirmed and found to match literature data and DSC measurements. At this eutectic composition, the ternary system behaves like a single phase with a congruent fusion. Being able to rapidly obtain both the eutectic composition and its melting temperature is a tremendous asset of the IRT method. Indeed, it enables the easy identification of material properties in temperature-based applications such as thermal energy storage and motivates the choice to either further study the composition or continue the screening of other systems. This technique also allows for rapid exploration of the phase diagram: reconstruction of the liquidus surface, identification of the eutectic, 4-phase equilibrium. Both pave the way for the modeling and prediction of phase diagrams in these systems and for the rapid screening of the composition space in the search of suitable blends in a wide range of applications.

Fig. 1

 1 Fig. 1 Scheme of the experimental setup

Fig. 2 aFig. 3

 23 Fig. 2 a Raw infrared signals for a sample of Palmitic acid; b First three time-eigenfunctions for the same sample.

Fig. 4

 4 Fig. 4 Phase diagram reconstruction from IRT. a Liquidus surface temperature map of the ternary system LA + MA + PA obtained 231 samples simultaneously analyzed by the IRT method. The DSC results, represented by large circles, are superimposed on the liquidus surface. The same colormap is used for both methods to show the coincidence. The smaller white and gray circles represent invariant

Table 1

 1 Properties

	compounds studied	of the pure	Material	Acronym	Supplier	Purity/%	Melting temperature/°C
							This work	[20-29]
			Lauric acid	LA	Acros Organics	99	43.40 ± 0.11	42.44-45.29
			Myristic acid	MA	Acros Organics	99	53.48 ± 0.04	55.23-55.58
			Palmitic acid	PA	Sigma-Aldrich	99	62.14 ± 0.02	61.45-64.35

Table 2

 2 Average temperature, standard deviation, and number of samples for the isothermal transitions detected with the IRT method and DSC measurements

Acknowledgements This work is carried out in the frame of SUDOKET project and is co-funded by the Interreg Sudoe Programme through the European Regional Development Fund (ERDF). The authors acknowledge them as well as the financial support of Region Nouvelle Aquitaine for subsidizing BioMCP project (Project-2017-1R10209-13023). We also would like to thank CNRS for promoting the I2M Bordeaux-CICe exchanges in the framework of the PICS PHASE-IR project. The authors would also like to thank Valérie Thouard for the administrative and financial management over SUDOKET Project.

Publisher's Note Springer Nature remains neutral with regard to jurisdictional claims in published maps and institutional affiliations.


Mathieu Laurent
email: mathieu.laurent@ens-rennes.fr

Emmanuelle Saillard
email: emmanuelle.saillard@inria.fr

Martin Quinson
email: martin.quinson@ens-rennes.fr

The MPI BUGS INITIATIVE: a Framework for MPI Verification Tools Evaluation

Keywords: Verification, MPI, Benchmarks, Tools

Ensuring the correctness of MPI programs becomes as challenging and important as achieving the best performance. Many tools have been proposed in the literature to detect incorrect usages of MPI in a given program. However, the limited set of code samples each tool provides and the lack of metadata stating the intent of each test make it difficult to assess the strengths and limitations of these tools. In this paper, we present the MPI BUGS INITIATIVE, a complete collection of MPI codes to assess the status of MPI verification tools. We introduce a classification of MPI errors and provide correct and incorrect codes covering many MPI features and our categorization of errors. The resulting suite comprises 1,668 codes, each coming with a well-formatted header that clarifies the intent of each code and specifies how to execute and evaluate it. We evaluated the completeness of the MPI BUGS INITIATIVE against eight stateof-the-art MPI verification tools.

I. INTRODUCTION

In the recent past, the vast majority of MPI applications were exhibiting rigid communication patterns and deterministic executions, to ensure both maximal performance and correctness. The focus of programmers was solely on the application performance, as application correctness was simple to test. As modern computing facilities reach tremendous dimensions, it becomes near to impossible to ensure perfectly stable and homogeneous hardware conditions, even over shorter execution time spans. Nowadays, large MPI applications must cope with variations in the environment through dynamic and non-deterministic execution patterns. As a result, the correctness of MPI programs of increasing complexity and size becomes as challenging and important as achieving the best performance [START_REF] Gopalakrishnan | Formal Analysis of MPI-Based Parallel Programs[END_REF].

MPI programs can exhibit many types of errors, that can be either classical synchronization errors (leading to deadlocks and data races) or more specific, such as mismatches between the parameters of corresponding MPI calls (data type or root of collective communications). Some MPI calls also introduce specific restrictions. For example, collective operations must be called in the same order by all processes, resource handlers should be freed appropriately, and remote memory access (RMA) fences must be correctly paired. Some potential MPI faults are more subtle, depending on obscure conditions. For example, two concurrent blocking sends from A to B and from B to A may or may not result in a deadlock depending on whether the data fits in the system buffers. MPI portability introduces another set of challenges, where a given application can fail only with some specific MPI implementations.

Many tools have been proposed in the literature to detect errors in MPI programs, leveraging diverse approaches such as static analysis [START_REF] Ma | Detecting Thread-Safety Violations in Hybrid OpenMP/MPI Programs[END_REF]- [START_REF] Siegel | Automatic Formal Verification of MPI-Based Parallel Programs[END_REF], dynamic analysis [START_REF] Böhm | State-space reduction of nondeterministically synchronizing systems applicable to deadlock detection in MPI[END_REF]- [START_REF] Pham | Verifying MPI Applications with Mc SimGrid[END_REF], or symbolic analysis [START_REF] Siegel | CIVL: the concurrency intermediate verification language[END_REF]- [START_REF] Yu | Symbolic Verification of Message Passing Interface Programs[END_REF]. Some of these approaches are better suited to detect some classes of errors, and authors may further specialize their tool to a subset of the potential errors. This situation makes it very difficult to evaluate the proposed tools, both for the users wanting to select the tool fitting their needs, but also for the authors wanting their tool to meet users' needs. One could rely on the test suites provided by each tool, but the lack of metadata often obfuscates the intent of each test. It is thus hard to judge whether a given sample collection properly covers the possible errors or is merely a set of redundant tests for a very specific error class. In this paper, we present the MPI BUGS INITIATIVE (MBI), a systematic and practical methodology to assess the status of MPI verification tools. This work makes the following contributions:

• We introduce a new classification of MPI errors depending on their root cause. • We propose a collection of codes covering the core features of MPI (point-to-point, collectives, etc.) and more advanced features, such as RMA. We provide both correct and incorrect codes to cover our error classification; • We use our methodology to assess and compare eight state-of-the-art verification tools from the literature. The rest of the paper is organized as follows. Section II discusses related work on existing MPI test suites and MPI tools comparison. Section III describes our methodology, centered around a classification of MPI errors and features. Section IV details the corresponding suite of MPI sample codes. Section V uses this methodology on existing verification tools while Section VI summarizes our findings and future work.

II. RELATED WORK

Assessing the quality of the MPI runtime implementations is a significant concern for decades, resulting in countless tools and benchmarks on the Internet. Most of the works described in the scientific literature focus on the performance of MPI implementations [START_REF] Reussner | SKaMPI: A detailed, accurate MPI benchmark[END_REF], or a subset of features [START_REF] Hoefler | Implementation and Performance Analysis of Non-Blocking Collective Operations for MPI[END_REF], [START_REF] Dosanjh | RMA-MT: A benchmark suite for assessing MPI multithreaded RMA performance[END_REF]. Thoroughly testing the correctness and standards conformance of the MPI implementations is an engineering challenge of its own [START_REF] Hursey | An Extensible Framework for Distributed Testing of MPI Implementations[END_REF]. On the application side, many tracing and profiling tools have been proposed. Several surveys propose a qualitative assessment of such MPI profilers and debuggers, through an empirical evaluation of the graphical interface, the documentation, the usefulness of the provided feedback, etc [START_REF] Moore | Review of performance analysis tools for MPI parallel programs[END_REF]- [START_REF] Luecke | Comparing Allinea's and Intel's performance tools for HPC[END_REF]. Our work in contrast aims at constituting an automated test suite providing a quantitative evaluation of correctness assessment tools.

The Run-Time Error Detection suite (RTED - [START_REF] Luecke | The Importance of Run-Time Error Detection[END_REF]) is very relevant, even if dated, to our work (the code samples can only be found from the Internet Archive project). It aims at proposing a quantitative evaluation of the runtime feedback to programming errors in several contexts. The authors gathered ten thousand code samples, organized in four suites containing serial, MPI, OpenMP, or UPC codes. The MPI suite proposes 1,942 code samples (in C, C++, or Fortran 90) falling into 10 categories: buffer out of bounds, buffer overlap, data type errors, rank errors, other argument errors, wrong order of MPI calls, negative message length, deadlocks, race conditions, implementation-dependent errors (such as potential deadlocks and race conditions). Each code contains exactly one described error, but no correct code is provided. Surprisingly, this work was almost never referenced in the context of MPI correctness. To the best of our knowledge, the only references to RTED in a context including MPI seems to be [START_REF] Alghamdi | Software testing techniques for parallel systems: A survey[END_REF], a survey misrepresenting RTED as being limited to OpenMP.

Our goals are similar but not perfectly aligned with the ones of the RTED benchmark. First, RTED is strongly focused on the quality of the produced error diagnosis while we are more interested in quantifying the error detection ability of the tools. The RTED harness does not report the tests for which the tool fails to produce a diagnosis, hiding the fact that some tools only support a small subset of MPI. Since RTED does not contain any correct code, it is also unable to evaluate whether a given tool tends to diagnose errors in correct codes. Second, the chosen error categories also denote a differing focus. Some of the RTED categories target the MPI runtime and check the buffer and memory handling or enforce that no message length is negative. Issues requiring a global view (deadlocks and message races) constitute a common concern between RTED and our work, as both are difficult to detect in production settings and often require external tools. Errors resulting from the dynamic communication patterns that become prevalent on modern systems (such as potential synchronization issues) are badly represented in RTED. Similarly, RTED is limited to MPI-2 features while we propose tests of the RMA features in MPI-3. Third, RTED exhibits a very strong bias toward dynamic analysis. "The tests were written so that the information needed to detect the error is not available at compile-time" [21, p3], deliberately defeating static and symbolic analysis. Our work does not have such a methodological bias and was successfully used to evaluate tools relying on static, dynamic, or symbolic analysis.

In [START_REF] Hong | Evaluation of Model Checkers by Verifying Message Passing Programs[END_REF], the authors present a benchmark to evaluate the ability of general-purpose model checkers to find deadlocks in MPI programs. [START_REF] Yu | Symbolic Verification of Message Passing Interface Programs[END_REF] is used to automatically extract models from the considered MPI programs. Mutation techniques [START_REF] Yu | Combining Symbolic Execution and Model Checking to Verify MPI Programs[END_REF], [START_REF] Just | Efficient Mutation Analysis by Propagating and Partitioning Infected Execution States[END_REF] are used to generate several thousands of models by injecting artificial errors into the 10 considered MPI applications, and the resulting models are translated in the formalism of the tested model checkers (PAT, FDR, Spin, PRISM, and NuSMV). The impressive amount of models included in this benchmark is hindered by the fact that the redundancy between these models is not evaluated. Besides, this collection seems to be limited to point-to-point MPI communications only.

MPI verification tools are usually evaluated separately, without being compared to the literature. Hermes [START_REF] Khanna | Dynamic symbolic verification of MPI programs[END_REF] is an exception, as the authors experimentally compared their tool to several competing solutions (ISP [START_REF] Vakkalanka | ISP: a tool for model checking MPI programs[END_REF], Mopper [START_REF] Forejt | Precise Predictive Analysis for Discovering Communication Deadlocks in MPI Programs[END_REF], Aislinn [START_REF] Böhm | State-space reduction of nondeterministically synchronizing systems applicable to deadlock detection in MPI[END_REF], and CIVL [START_REF] Siegel | CIVL: the concurrency intermediate verification language[END_REF]). This study is unfortunately limited to the detection of deadlocks in MPI programs.

MPI-CorrBench [START_REF] Lehr | MPI-CorrBench: Towards an MPI Correctness Benchmark Suite[END_REF] is a recent MPI benchmark suite containing 510 small-scale programs and 3 mini-apps with errors. The proposed programs fall in four categories: correct code, erroneous arguments, erroneous program flow, and mismatching arguments across communicator. This benchmarks are used to compare four tools from the literature (MUST, ITAC, MPI-Check and PARCOACH). The main differences with the MPI BUGS INITIATIVE is that our error categorization contains more kind of errors (e.g. covering message races, resource leaks and concurrency issues), and that we evaluate eight tools, but the MBI does not contain tests of the size of a miniapp. As a result, the MPI-CorrBench and MBI efforts are very complementary.

We believe that the MPI BUGS INITIATIVE will be highly beneficial to the potential users and tool authors targetting. This effort results from the collaboration of two unrelated teams developing such tools, and we reported several issues found through our work to the authors of the other tools. We hope that others will join this effort in the future.

III. METHODOLOGY

The MBI main goal is to measure the qualitative and quantitative performance of MPI verification tools in a reproducible and automatic way. With that goal in mind, we first identify errors that can arise in MPI programs and classify them following the errors taxonomy described in [START_REF] Desouza | Automated, Scalable Debugging of MPI Programs with Intel Message Checker[END_REF]. To automate the evaluation and ensure our benchmark suite is representative of real-world applications, we annotate all programs with the expected error, if any, and feature labels.

For each tool, we provide the number of errors correctly reported (TP), missed (FN), incorrectly reported (FP) and the number of programs correctly detected as error-free (TN). We also compute five standard metrics that define tools performance [START_REF] Verma | Enhancing DataRaceBench for Evaluating Data Race Detection Tools[END_REF], [START_REF] Cifuentes | BegBunch: Benchmarking for C bug detection tools[END_REF]: Recall, Specificity, Precision, Accuracy, and F1 score. Recall is the ratio of true positives out of the total number of correctly and incorrectly reported errors while Specificity gives the ratio of true negatives out of the total number of true negatives and false positives. The precision metric is the ratio of true positives out of the total number of errors reported. Accuracy measures the tool ability to correctly report out of all positive and false reports. Finally, the F1 score corresponds to the harmonic mean of precision and recall. In addition to these standard metrics, we define two new metrics to evaluate tools ability to draw a diagnostic on codes (Conclusiveness) and to compile codes (Coverage).

for (i = 0; i < OP_COUNT; i++) MPI_Op_create(myOP, 1, &newop[i]); (g

A. Feature Labels

We define 7 feature labels representing the way MPI processes exchange messages. Each label is either set to Yes: use of the feature, or Lacking: the feature is missing. The list of all feature labels is given in Table I (first three columns) and a full description of each one is detailed below. Note that a code can have multiple features.

1) Point-to-point: base calls and nonblocking: A pointto-point communication involves two MPI processes. It can be either blocking (i.e., the call returns when the resources of the communication can be reused), referred as base calls, or nonblocking (i.e., the call returns as soon as it can), referred as nonblocking. An MPI nonblocking operation is composed of two procedure calls: an initialization of the form MPI_I<operation> (e.g., MPI_Isend) and a completion (MPI_Wait or MPI_Test ). Between these two operations, the data buffer is in a vulnerable state. A misuse of blocking and nonblocking point-to-point communications includes unbalanced communications (e.g., a send without a corresponding receive operation) and the use of invalid arguments. When using nonblocking point-to-point communication, an error can also occur if a completion call is missing, the buffer involved in the communication is modified before the operation is completed or if requests are not correctly used.

2) Point-to-point: persistent: Persistent communication is composed of four procedure calls. The first procedure initiates the communication (e.g., MPI_Send_init). The second procedure starts the communication (e.g., MPI_Start). The third and fourth procedures respectively complete and free the operation. A persistent communication is misused when called with invalid arguments, if the completion operation is missing or if the buffer involved in the communication is modified between the start and the completion calls.

3) Collective: base calls and nonblocking: A collective is a communication that involves all processes in a communicator. These labels are restricted to usual collectives communication only (e.g., MPI_Barrier, MPI_Bcast, MPI_Ireduce). The MPI specification requires that all processes of a communicator have the same sequence of blocking and nonblocking collectives. These operations are incorrect if communication buffers overlap, if all processes in a communicator do not call the same collectives in the same order, or if collectives are called with incompatible or invalid arguments. Note that it is not allowed to match a blocking collective with its nonblocking counterpart; such situation is erroneous.

4) Collective: tools: This label comprises communicator and group management operations (e.g., MPI_Comm_create/free), topology creation operations like MPI_Cart_create that virtually organize processes in a multi dimensional grid, and datatypes and operators creation operations (e.g., MPI_Op_create to create operators for use in reduce functions). These operations must be called by all processes in the involved communicator otherwise a deadlock can occur. Furthermore, these operations are incorrect in case of improper construction and/or destruction of the MPI resource or if they are called with invalid arguments.

5) RMA: The Remote Memory Access (RMA) allows processes to expose a part of their memory (called window) in order to perform one-sided communications (e.g., MPI_Get). These communications are performed inside an epoch to ensure synchronizations. MPI RMA defines two kind of synchronization: active synchronization where the target takes part in the epoch creation (e.g., with MPI_Win_fence) and passive synchronization (e.g., with MPI_Win_lock and MPI_Win_unlock) where the target does not take part of the epoch creation. A misuse of RMA communication includes wrong RMA initialization/destruction operation usage (e.g., if MPI_Win_create is not called by all processes), a concurrency in memory accesses inside an epoch or a onesided communication called with invalid arguments (e.g., if the target memory that is not part of the window).

B. Error Labels

Many errors can occur in a MPI program. Based on what was proposed in previous work [START_REF] Luecke | The Importance of Run-Time Error Detection[END_REF], [START_REF] Desouza | Automated, Scalable Debugging of MPI Programs with Intel Message Checker[END_REF], we define 8 types of errors that can occur in a MPI program depending on the root cause: Invalid Parameter, Resource Leak, Request Lifecycle, Local Concurrency, Message Race, Parameter Matching, Call Ordering and Global Concurrency. These errors are categorized according to the scope in which they manifest: single call, single process and multi-processes.

1) Errors in single calls: These errors are only related to local MPI functions and can be detected by only analyzing the parameters of a given MPI function.

a) Invalid Parameters: This category contains errors such as invalid root, communicator, operator, datatype, tag or buffer length. The use of invalid parameters in MPI functions is incorrect and is reported by the MPI runtime.

In Figure 1d, processes call a reduce function with process 22 as root. If the program is launched with less than 23 processes, the root would be invalid. For this code, the MPI runtime reports the following message: MPI_ERR_ROOT: invalid root.

2) Errors local to a process: These errors often consist of an inconsistency between the local context of a process and the parameters to a given MPI call in that process. Detecting them thus requires analysis of local process information. a) Resource Leak: Any improper destruction of MPI resources (e.g., datatype, request, communicators) leads to a resource leaking. As an example, the code snippet in Figure 1g constructs OP_COUNT MPI operators without freeing them.

b) Request Lifecycle: Request lifecycle is used for a missing wait or start function. Figure 1f shows a nonblocking reduce function that does not have a MPI_Wait associated. c) Local Concurrency: A local concurrency occurs when a process accesses a memory region that is being read or written. This type of error is easy to produce with nonblocking and one-sided communication. For RMA operations, we consider concurrency errors inside an epoch and within a process. Figure 1b gives an example of a local memory consistency error within an epoch: Two operations are accessing variable buf, the Put operation reads buf while a store writes on buf.

3) Multi-processes errors: The next four errors result from multiple processes of the application, either local to a given communicator or globally.

a) Message Race: The use of wildcard receive calls can lead to nondeterministic matching with potential senders at runtime. An example is presented in Figure 1a. In this code, a deadlock arises if P0 receives from P2 first. We label these situations as message races.

b) Parameter Matching: Parameter matching corresponds to MPI calls matched with incompatible arguments. This happens for example when each rank gives its ID as root in a broadcast function as illustrated in Figure 1e. This code results either in a numerical instability or a deadlock, depending on the MPI implementation. c) Call Ordering: Different scenarios can lead to a call mismatch: Any pattern causing a cyclic dependency (e.g., send-receive cycle) and a point-to-point or collective mismatch.

d) Global Concurrency: Global concurrency occurs when two or more processes access the same memory region and at least one access is a write. Such errors are produced with RMA operations inside an epoch and between processes. Figure 1c shows an example of two conflicting MPI_Put operations. Processes 0 and 2 access the same window buffer X, located on process 1.

IV. THE MPI BUGS INITIATIVE

We built the MPI BUGS INITIATIVE to cover all errors and features categorization described in the previous section. Particular attention was paid to ensure the suite is representative and complete.

A. Benchmark Description

All codes in MBI are automatically generated from Python scripts to ensure a systematic coverage of the errors and features. Our benchmark contains 1, 668 original programs. 986 programs have errors and 682 are known to be errorfree. Note that error-free programs are important for false

B. Features and Errors Coverage

As mentioned in section III-B, the occurrence of an error may depend on several parameters including the MPI implementation, the number of processes, the system buffering and the program input data. We associate each code in the benchmark to one test. A test corresponds to an execution command line with specific parameters including the number of processes. Table I gives the number of correct and incorrect programs using each feature (a program can have multiple feature labels) and Table II shows the feature usage among all correct and incorrect codes. The last row of table II depicts the total number of correct programs and incorrect programs per error. It is worth mentioning that some features are irrelevant to some errors (e.g., RMA operations cannot produce a Request Lifecycle error). It may be observed that all MPI features are represented in the benchmark with a predominance of basic collectives and point-to-point operations which correspond to the most used features in HPC applications [START_REF] Laguna | A Large-Scale Study of MPI Usage in Open-Source HPC Applications[END_REF].

V. TOOLS COMPARISON

We use the MBI to evaluate Aislinn (v3.12), CIVL (v1.20), ISP (v0.3.1), ITAC [START_REF]Intel Trace Analyzer and Collector[END_REF] [START_REF] Krammer | Runtime checking of MPI applications with MARMOT[END_REF] and Umpire [START_REF] Vetter | Dynamic Software Testing of MPI Applications with Umpire[END_REF]. It intercepts all MPI operations to perform online checking. It is based on GTI (generic tool infrastructure) and can detect multiple errors like deadlocks, type mismatches or resource leaking. Intel Trace Analyzer and Collector (ITAC) uses a similar approach to MUST. It is implemented as a library that performs error detection at runtime and records error reports for later analysis. PARallel COntrol flow Anomaly CHecker (PARCOACH) combines a static analysis with a code instrumentation to detect misuse of MPI collectives [START_REF] Huchant | PAR-COACH Extension for a Full-Interprocedural Collectives Verification[END_REF] as well as nonblocking and persistent communications [START_REF] Nguyen | PARCOACH Extension for Static MPI Nonblocking and Persistent Communication Validation[END_REF]. Although it uses a precise data-and control-flow interprocedural analysis to pinpoint root cause problems, it may lead to many false positives. In this work we only consider the PARCOACH static phase which is implemented as a LLVM pass.

A. Experimentation Setup

The experiments were performed in a Docker image with Ubuntu version 20.04 containing all tools dependencies, except for Aislinn which was run with Ubuntu 18.04 due to dependency issues in the newer Ubuntu version and MPI-SV which was run with Ubuntu 14.04.6 (we use the docker image provided by the authors). All tests use at most 6 processes to produce the expected errors. The use of Docker facilitates the benchmark modifications and the installation of the tools we have selected. All results were obtained with MPICH v3. [START_REF] Nguyen | PARCOACH Extension for Static MPI Nonblocking and Persistent Communication Validation[END_REF] Aislinn 385 0 0 297 42 0 0 112 0 0 16 0 6 0 0 12 24 0 5 8 24 11 22 40 0 0 4 0 367 4 0 277 12 0 0 0 CIVL 534 14 1 133 100 47 3 4 13 1 0 2 18 0 0 0 37 0 0 0 58 21 0 18 3 0 0 1 521 5 3 119 12 0 0 0 ISP 0 1 479 202 0 5 8 141 0 0 8 8 0 0 12 6 0 0 21 16 0 1 19 77 0 0 0 4 0 1 6 641 0 0 12 0 ITAC 0 0 0 682 0 0 2 152 0 0 14 2 0 0 4 14 0 0 24 13 0 0 3 94 0 0 1 3 0 0 0 648 0 0 12 0 Mc SimGrid 0 7 0 675 0 12 0 142 0 0 2 14 0 0 2 16 0 18 14 5 0 0 4 93 0 0 0 4 0 4 261 383 0 12 0 0 MPI-SV 494 3 4 181 36 16 94 8 0 0 16 0 12 0 5 1 11 18 8 0 31 0 55 11 0 0 4 0 459 4 83 102 0 12 0 0 MUST 0 0 1 681 0 4 0 150 0 0 0 16 0 0 4 14 0 0 32 5 0 0 0 97 0 0 3 1 0 5 0 643 0 0 12 0 PARCOACH 441 0 182 59 36 0 118 0 0 0 16 0 11 0 7 0 17 0 20 0 28 0 69 0 0 0 4 0 407 0 24 217 4 0 8 0 Ideal tool 0 0 0 682 0 0 0 154 0 0 0 16 0 0 0 18 0 0 0 37 0 0 0 97 0 0 0 4 0 0 0 648 0 0 0 12 One big challenge is to automate the evaluation and comparison of tools that use different techniques and outputs. To address this issue, we analyze the output of each tool independently and we have developed a Python script that associates messages reported by the tools with our errors categorization (e.g., a tool can state an error in many different ways but still be understandable by a user). More specifically, a runner compiles each tool except CIVL which is distributed in an executable form. Each program in the MBI is then compiled and executed with specific parameters as defined in programs header. To deal with time out, we limit the execution of each test at 5 minutes. This is a reasonable threshold as our tests do not take much time. All outputs are registered and analyzed by the runner: it searches for particular keywords specific to each tool. For instance, the message "Fatal error in PMPI_Cart_get: Invalid topology" from ISP is labelled with Invalid Parameter and any warning emitted by PARCOACH is considered as a Call Matching error.

B. Qualitative and Performance Evaluation

Table III shows the results of each tool on all tests per error category. For each error, we report the number of Build errors (i.e., number of codes that did not compile), Runtime errors (i.e., number of codes that did not execute), the number of False Negative (the tool did not detect the error) and the number of True Positive (the tool detected the expected error). For correct codes, we report the number of Build errors and Runtime errors but also the number of False Positive (the tool reported an error on a correct code) and True Negative (the tool detected no error on a correct code). This allows to pinpoint specific features not supported by tools and highlight what errors a given tool can detect. In the The first thing to notice is how hard it is to cover everything. Actually, no tool is able to detect all errors in the MBI programs and they all return false positives or negatives. Call ordering is the most commonly detected error type, not necessarily because it is the easiest, but certainly because it is the most common result of a MPI feature misuse. ITAC is the best performing tool with the highest overall accuracy, followed closely by MUST. ITAC and MUST both detect a wide range of errors and outperform on several types of errors: ITAC has the best results for correct execution, invalid parameter and call ordering while MUST is the best to detect resource leak and parameter matching. Despite achieving well on some error types, MUST appears to be bad on message races and local and global concurrency and ITAC has difficulties to find resource leak and global concurrency errors. Overall, table III recognizes a lack of RMA support (responsible of global concurrency) in all tools which could be something to improve. Mc SimGrid and ISP seem to be a good compromise with a few number of compilation and runtime errors and a large detection of many kind of errors. They fail on less than 1% of the tests. ISP does well on local concurrency detection and Mc SimGrid is the best on request lifecycle and message race. Aislinn reports about 46% of errors, detects 44% of correct tests and fails on 52% of codes. Few features are supported by CIVL, MPI-SV and PARCOACH. CIVL syntactic analysis returns a compilation failure on 78% of the tests. As it is focused on collective mismatch detection, PARCOACH returns a lot of false negatives and few true negatives. It fails on 57% and is able to detect 22% of errors. Note that recent work from [START_REF] Nguyen | PARCOACH Extension for Static MPI Nonblocking and Persistent Communication Validation[END_REF] on point-to-point and persistent operations are not integrated to the latest version of the tool yet. MPI-SV detects 12% of errors and 27% of correct codes and fails on 63% of the tests. These results are related to the use of the multithreaded library for MPI-1 called AzequiaMPI [START_REF] Rico-Gallego | A Pthreads-Based MPI-1 Implementation for MMU-Less Machines[END_REF]. All results are available on the MBI website with meta-data on the tests links to every test execution log. Our goal is to provide a precise feedback to help developers improve their tools.

The tools capacity to cover many errors is strongly related to the precision of their feedback. Indeed, Table III is built using a precise study of the messages returned by all tools. Aislinn and MUST both generate html outputs with execution graphs. On the opposite, the other tools require more effort to understand what is detected. We plan to work with tools developers in order to consolidate our study. To begin, we already report issues we found to tools developers. We also reported an error related to asynchronous collectives in MPICH. Beyond being able to detect errors, a tool should be capable of helping the developer to correct programs quickly. Experience has shown that few tools can precisely pinpoint what caused an error.

Our evaluation tends to reveal how user-friendly and easy to use the tools are. MUST is one of the easiest tools to use: a code is compiled with an usual compiler and launched with a single command line (mustrun). CIVL follows a comparable workflow, directly working on the source code. The other tools require a specific compiling pass and a run-time execution. Even if this isn't an issue while performing over a single file, it may harden the task of testing bigger projects.

VI. CONCLUSION

In this paper, we present the MPI BUGS INITIATIVE, an MPI benchmark suite for the evaluation of MPI bugfinding and verification tools. We propose a new classification of MPI errors based on their root causes. Our benchmark provides both correct and incorrect code samples to cover this classification. Each code comes with a well-formatted header describing its intent and specifying how to test it. We used our benchmark on eight major state-of-the-art MPI verification tools: Aislinn, CIVL, ISP, ITAC, Mc SimGrid, MPI-SV, MUST, and PARCOACH. The evaluation compares the tools in terms of error coverage. Our results show that no tool is currently able to support all MPI features and detect all classes of errors. In our findings, ITAC achieves the best scores on the overall accuracy metric. The code samples and tools evaluated in this work have been dockerized with our test harness to improve the reproducibility of our findings. We plan to integrate more tools in our initiative and organize an MPI verification tools contest to stimulate tools development. We hope that the MPI BUGS INITIATIVE will foster the verification and bug-finding tools that the users need to tame the application complexity induced by the large-scale and dynamic modern platforms. The MPI BUGS INITIATIVE is an ongoing effort to build a comprehensive correctness benchmark suite and can be extended in many ways. First, we will add missing MPI features such as MPI IO and extend our errors categorization with errors depending on the buffer mode. Then, we intent to add new codes to further improve our coverage of features and errors. This could be achieved by using mutants or machine learning techniques. Finally, we plan to add larger codes to evaluate the tools scalability, either through larger synthetic codes or through a collection of real bugs in full-scale applications.

)Fig. 1 :

 1 Fig. 1: Examples of different erroneous situations.

TABLE I :

 I List of MPI feature labels. The two last columns give the number of correct and incorrect programs using the labels (codes may use several labels). P2P and COLL respectively stand for point-to-point and collective.

	P0 recv(any) send(0) send(0) P1 P2 send(1) recv(0) recv(any)	P0 Win_fence buf[0]=8 Put(buf,1,X)	P1 window buffer X Win_fence	P0 Win_lock_all Put(buf1,1,X)	P1 window buffer X Win_lock_all	P2 Win_lock_all Put(buf2,1,X)
	(a) Potential send-recv cycle (Message	Win_fence	Win_fence	Win_unlock_all Win_unlock_all	Win_unlock_all
	Race)	(b) RMA datarace (Local Concurrency)	(c) Conflicting Put operations (Global Concurrency)

int root = 22; MPI_Comm com = MPI_COMM_WORLD; MPI_Reduce(&myrank,&sum,1,MPI_INT,MPI_SUM,root,com); (d) Root not in the communicator (Invalid Parameter) MPI_Comm com = MPI_COMM_WORLD; MPI_Datatype conti; ... MPI_Bcast(outbuf, 6 / (3 -rank), conti, rank, com); (e) Root mismatch in a broadcast function (Parameter Matching) ... MPI_Ireduce(&sum, &val, 1, MPI_INT, MPI_SUM, root, MPI_COMM_WORLD, &req); ... MPI_Request_free(&req); (f) Missing wait (Request Lifecycle) void myOP(void * in,void * inout,int * len,MPI_Datatype * dptr); MPI_Op newop[OP_COUNT];

TABLE II :

 II Errors classification. Numbers indicate the number of codes with the feature and the error. The last row shows the number of correct codes with each feature (a code can have multiple features). positives reporting. All codes are written in C and have a formatted header providing a textual description of the problem, the list of MPI features used, the expected errors, and how to evaluate them. Each incorrect code produces only one error: all codes were verified with the Valgrind tool and we manually checked the output of all bug finding tools. We made the suite extensible so new codes, errors and features can easily be added. The MBI can be downloaded from https://gitlab.com/MpiBugsInitiative.

  To do so, it realizes a symbolic execution with Partial Order Techniques. Aislinn supports both zero and infinite buffering modes. CIVL combines symbolic execution and model checking to detect communication deadlocks. It can detect data races and assertion violations but does not support nonblocking operations. Like CIVL, MPI-SV uses symbolic execution and model checking to detect communication deadlocks in MPI programs. ISP checks if a program satisfies a given property (e.g., liveness, communication determinism) by considering all possible executions. Like all model checkers, it faces a state space explosion problem. Mc SimGrid is a model checker integrated to SimGrid, a framework mostly dedicated to predicting the performance of distributed applications. It explores all the possible execution paths of an MPI application, starting from an initial application configuration with a fixed set of inputs. Mc SimGrid verifies safety properties, liveness properties, and other properties such as communication determinism. MUST is the successor of Marmot

	(v2021.3), Mc SimGrid [9] (v3.28),
	MPI-SV [13] (v1), MUST (v1.6) and PARCOACH (v1.2) as
	they are active projects, available and use different techniques.
	Aislinn focuses on deadlock detection caused by run-time
	scheduling problem among operations.

  .2.

		Correct			Invalid		Resource	Request			Local		Parameter	Message		Call			Global
		execution			parameter			leak		lifecycle	concurrency	matching		race			ordering		concurrency
	Build error	Runtime error	False Positive	True Negative	Build error	Runtime error	False Negative	True Positive	Build error	Runtime error	False Negative	True Positive	Build error	Runtime error	False Negative	True Positive	Build error	Runtime error	False Negative	True Positive	Build error	Runtime error	False Negative	True Positive	Build error	Runtime error	False Negative	True Positive	Build error	Runtime error	False Negative	True Positive	Build error	Runtime error	False Negative	True Positive

TABLE III :

 III Results of each tool per error category.

	Tool	Errors CE TO RE TP TN FP FN Coverage Conclusiveness Specificity Recall Precision F1 Score accuracy Results Robustness Usefulness Overall
	Aislinn	860 0 15 449 297 0 47	0.4844	0.4754	1	0.9052	1	0.7644	0.4472
	CIVL	1296 0 88 144 133 1	6	0.223	0.1703	0.9925	0.96	0.9931	0.9381	0.1661
	ISP	0	7 1 893 202 479 86	1	0.9952	0.2966 0.9122 0.6509	0.2535	0.6565
	ITAC	0	0 0 926 682 0 60	1	1	1	0.9391	1	0.8256	0.964
	Mc SimGrid 0	0 53 657 675 0 283	1	0.9682	1	0.6989	1	0.8319	0.7986
	MPI-SV	1043 0 53 122 181 4 265 0.3747	0.3429	0.9784 0.3152 0.9683	0.517	0.1817
	MUST	0	4 5 926 681 1 51	1	0.9946	0.9985 0.9478 0.9989	0.8277	0.9634
	PARCOACH 944 0 0 217 59 182 266 0.4341	0.4341	0.2448 0.4493 0.5439	0.2225	0.1655
	Ideal tool	0	0 0 986 682 0	0	1	1	1	1	1	1	1

TABLE IV :

 IV Tools Evaluation against the MPI BUGS INITIATIVE benchmark.

	Result	Meaning	Result	Meaning
	True Positive (TP)	Error correctly detected.	Compilation Error (CE)	The code uses a feature not supported by the tool.
	False Negative (FN)	Error missed.	Timeout (TO)	Timeout (limit: 300s).
	False Positive (FP)	Correct code reported as faulty.	Runtime Error (RE)	Tool failure during the evaluation of this code.
	True Negative (TN)	Correct code reported as such.	Total	Total = CE+RE+TO + TP+FP + TN+FN
	Metric	Definition and meaning
	Coverage	Ability to compile codes. Cov = 1 -CE total
	Conclusiveness	Ability to draw a diagnostic on codes. Cc = 1 -CE+RE+T O total
	Specificity	Ability to not find errors in correct codes. S =	T N T N +F P
	Recall	Ability to find existing errors. R =	T P T P +F N
	Precision	Potential confidence when a code is reported as correct. P =	T P T P +F P
	F1 Score	Overall bug-finding quality. F 1 = 2×P ×R P +R
	Overall accuracy	Proportion of correct diagnostics over all tests. A = T P +T N total

TABLE V :

 V Results, Metrics and Abbreviations used. Metrics do not account for codes leading to a tool error.

  table, results in bold indicate which tool has the best results for a type of error. The Errors columns of table IV regroup the number of compilation errors (Build), Timeouts and runtime errors (failure). The Results columns gather the total number of True positive (TP), False negative (FN), False positive (FP), and True negative (TN) per tool. The last row of the table depicts results an ideal tool would have. Basically, an ideal tool should have no error, false positive or false negative and detect all correct tests as true negatives and all incorrect tests as true positives. Table IV also gives the Coverage, Conclusiveness, Recall, Specificity, Precision, F1 Score and Overall Accuracy results. How to compute these metrics is detailed in Table V.

A. Software availability and dependencies

The MPI Bugs Initiative (MBI) is available on Gitlab at https://gitlab.com/MpiBugsInitiative. The source code of all evaluated tools is available in the MBI repository, that is self contained. No additional files are needed beside of the Ubuntu online repositories that are used automatically.

B. Installation

We use Docker to facilitate our benchmark modifications and the installation of the tools we have selected. A user can launch all tests outside the docker image by using the ./test-all command, that runs all steps described below.

The MBI experiments were performed in a Docker image with Ubuntu version 20.04 containing all tools dependencies, except for Aislinn which was run with Ubuntu version 18.04 due to dependency issues in the newer Ubuntu version and MPI-SV which was run in the docker image provided by the authors. A user can create the MBI docker image from the provided Dockerfile as follows:

docker build -f Dockerfile -t mbi:latest . docker run -it mbi bash Once inside the docker, the /MBI/MBI.py script provides a centralized interface to all tool-specific scripts (located under /MBI/scripts/tools/<tool>.py). It handles both the data provenance (producing execution logs for all tools) and the data analysis (producing figures out of the logs)

C. Data provenance

The source code of all tools are included in the Docker image, and they are compiled on need. The binaries are persistent out of the Docker environment, as a cache mechanism.

The test cases are generated using the following command:

python3 ./MBI.py -c generate One can either run the tests for all tools, or chose a specific tool as follows:

python3 ./MBI.py -c run python3 ./MBI.py -c run -x <tool> All logs are produced under /MBI/logs/<tool>, that is persistent out of the Docker. In each directory, the following files are produced for the data analysis: • test name.txt: that contains the tool output for that test • test name.elapsed: that gives the wallclock time In addition, a test name.md5sum file is used to detect changes in the test codes, and cache the test results when the code is unmodified.

D. Data analysis

Once all logs are in cache, the LaTeX tables included in this article are regenerated as follows:

python3 ./MBI.py -c latex This is an error-prone component, and we manually checked the results on all generated codes, also comparing the observed outcomes of all bug-finding tools.

A web dashboard can be generated to explore the logs in cache as follows.

python3 ./MBI.py -c html

This is useful to debug the tool-specific scripts that parse the textual output of that tool, i.e. the component in charge of categorizing a given run as either as 'True Positive', 'False Negative' and so on. This dashboard provides two views presented in Figure 2. The upper part gives a quick glance on the categorization of each tool and test code (using colored icons), while the lower part allows to see the detail of all logs. This tool is only described in this reproducibility section, as it is meant as an internal tool to ensure the quality of the tool-specific parsers.

E. Continuous Integration

We rely on GitLab Continuous Integration features to enforce the reproducibility of the provided tooling. All results can be visualized at https://mpibugsinitiative.gitlab.io/ MpiBugsInitiative/. MPI-SV and ITAC are not included in this dashboard, because of a technical difficulty. They fail with a SIGILL error when executed in the docker-in-docker settings that is mandated gitlab-ci. They must be run manually to produce the logs.