A Bechikh

Y Maalej

I Tawfiq

Fiber reinforced polymers use limitations and remedies -Quick review

Keywords: Fiber reinforced polymers, Adhesion properties, Surface treatment, Structural bonding, Durability, Aging, Fire, Temperature, Moisture

Fiber reinforced polymers (FRPs) are increasingly being used and implemented in many industrial fields such as transportation, automotive, aerospace aviation and civil engineering due to their low cost, light weight and high mechanical properties. Yet the use of such complex materials could sometimes be limited by their surface poor adhesion properties and low resistance to severe environmental conditions such as moisture and temperature. The aim of this research is to highlight organic composite use barriers and so far founded solutions.

Introduction

Composite is the assembly of two or more immiscible materials. In general, there is a discontinuous phase distributed in a continuous phase. Discontinuous phase plays the role of inclusions. This phase usually has mechanical properties superior to the continuous phase that plays the role of the matrix. The matrix maintains inclusions' geometrical disposition and enables applied stress distribution. Composite materials are very heterogeneous and strongly anisotropic. Their properties depend on components properties, inclusions geometrical distribution and inclusion/matrix interface nature. The most communally used composites are polymers reinforced with synthetic fibers such as glace, aramid and carbon fibers [START_REF] Castani É | Structures en matériaux composites stratifiés. Mécanique -Fonctions et composants mécaniques[END_REF]. Bio-composites, mainly polymers reinforced with natural fibers like hemp and flax fibers are gradually being included in the industry. Fiber reinforced polymers (FRPs) are characterized by a brittle and a linearly elastic behavior up to failure and a high tensile strength in fiber direction [START_REF] Böer | Independent environmental effects on durability of fiber-reinforced polymer wraps in civil applications: A review[END_REF][START_REF] Schmidt | Mechanical anchorage of frp tendons -a literature review[END_REF]. Composites could be custom tailored in order to increase their strength by modifying the fiber content or their geometrical distribution [START_REF] Pil | Why are designers fascinated by flax and hemp fibre composites?[END_REF][START_REF] Yan | Flax fibre and its composites -a review[END_REF][START_REF] Xu | Flax fiber-reinforced composite lattice cores: A low-cost and recyclable approach[END_REF]. Due to their lightweight, good corrosion resistance, non-conductivity and failure elongated strain, FRPs have been used as alternative reinforcements for steel in civil engineering structural application [START_REF] Jabbar | Replacement of steel rebars by gfrp rebars in the concrete structures[END_REF][START_REF] Sheikh | Replacement of steel with gfrp for sustainable reinforced concrete[END_REF]. Glace fiber reinforced polymers (GFRPs) are one of the more cost effective FRP products commercially available with significant cost advantage over stainless steel. The combination of GFRP and steel bars as column reinforcements was also proven to be effective [START_REF] Sheikh | Replacement of steel with gfrp for sustainable reinforced concrete[END_REF]. Yet the use of composite materials in this field could sometimes be limited by their low compressive stress and low resistance to fire and temperature [START_REF] Tabatabaei | Strength of compression lap-spliced gfrp bars in concrete columns with different splice lengths[END_REF][START_REF] Correia | A review of the fire behaviour of pultruded gfrp structural profiles for civil engineering applications[END_REF][START_REF] Hajiloo | Mechanical properties of gfrp reinforcing bars at high temperatures[END_REF][START_REF] Hawileh | Thermal analysis of gfrp-reinforced continuous concrete decks subjected to top fire[END_REF][START_REF] Zhang | Experimental study and theoretical analysis on axial compressive behavior of concrete columns reinforced with gfrp bars and pva fibers[END_REF]. Joining processes are unavoidable in manufacturing fiber reinforced polymers especially those with complex geometries. Structural bonding is the most used and profitable composite assembling technology. Nevertheless, composites' poor adhesion properties at their raw state limited the use of this technique in hybrid structures. Surface treatment before bonding is essential in order to enhance composites' surface quality. Another problematic issue for composites' industrial implementation is their low resistance to severe environmental conditions such as moisture and high temperature [START_REF] Böer | Independent environmental effects on durability of fiber-reinforced polymer wraps in civil applications: A review[END_REF][START_REF] Hunter-Alarcón | Effect of the natural aging process on the shear strength of frp composite single lap joints[END_REF][START_REF] Kabir | Pull-out strengths of gfrp-concrete bond exposed to applied environmental conditions[END_REF]. Aging is a complicated problem for composite materials that usually leads to their mechanical properties degradation thus reducing their service life by inducing premature and catastrophic failure modes. Fiber reinforced polymers use limitations and their so far founded solutions are discussed in this paper.

2 Moisture effect on fiber reinforced polymers (FRPs)

Moisture is one of the most damaging factors to organic composites. It affects all of its components starting from the matrix and the fibers to the fiber-matrix interface. Matrix is the primary victim of water absorption due to the hydrophilic nature of many widely used resins [START_REF] Kabir | Pull-out strengths of gfrp-concrete bond exposed to applied environmental conditions[END_REF]. A research carried out by Chilali et al. [START_REF] Chilali | Effect of water ageing on the load-unload cyclic behaviour of flax fibre-reinforced thermoplastic and thermosetting composites[END_REF] revealed that thermostat composites absorb more water than thermoplastic composites. Resin water absorption usually results in its plasticization, swelling, hydrolysis, and fiber debonding. Plasticization and hydrolysis are irreversible phenomena that can change both the stiffness and the strength of the polymer.

Many studies [START_REF] Böer | Independent environmental effects on durability of fiber-reinforced polymer wraps in civil applications: A review[END_REF][START_REF] Hunter-Alarcón | Effect of the natural aging process on the shear strength of frp composite single lap joints[END_REF] have reported the decrease of FRPs maximum load, fracture toughness and Young's modulus due to water absorption. Synthetic fibers, such as glass and carbon fibers, are hardly affected by humidity. Hence, aging resistance of polymers reinforced with synthetic fibers depends mainly on the resin permeability and cracking resistance. Composites' weakness to moisture is located at the matrix-fiber interface. Due to fiber water non-absorption and some resin hydrophilic nature, a differential swelling could occur causing residual stress. Fiber reinforced polymers aging resistance could be enhanced by increas-ing fiber-matrix adhesion strength using fiber surface chemical treatments such as silane [START_REF] Rahman | 5 -tensile properties of natural and synthetic fiber-reinforced polymer composites[END_REF][START_REF] Xie | Silane coupling agents used for natural fiber/polymer composites: A review[END_REF], epoxy [START_REF] Kyutoku | Effect of surface treatment of cellulose fiber (cf) on durability of pla/cf biocomposites[END_REF] and poly methacrylic acid [START_REF] Semitekolos | Advanced carbon fibre composites via poly methacrylic acid surface treatment; surface analysis and mechanical properties investigation[END_REF]. Synthetic fiber based composites have higher water aging resistance compared to bio-composites [START_REF] Wroblewski | Durability of bond between concrete beams and frp composites made of flax and glass fibers[END_REF]. This is mainly due to the hydrophilic nature of natural fibers. Natural fibers based composites hybridization with GFRP, CFRP or BFRP was proven to be a good solution for this problem [START_REF] Flynn | Hybridized carbon and flax fiber composites for tailored performance[END_REF][START_REF] Almansour | Investigation into mode ii interlaminar fracture toughness characteristics of flax/basalt reinforced vinyl ester hybrid composites[END_REF][START_REF] Saidane | Damage mechanisms assessment of hybrid flax-glass fibre composites using acoustic emission[END_REF][START_REF] Živković | Influence of moisture absorption on the impact properties of flax, basalt and hybrid flax/basalt fiber reinforced green composites[END_REF]. Carbon fibers have a higher resistance to moisture than aramid and glace fibers [START_REF] Böer | Independent environmental effects on durability of fiber-reinforced polymer wraps in civil applications: A review[END_REF]. Water absorption usually increases with the increase of temperature and the presence of external stress. Interlayer delamination is the most critical deterioration mode for organic composites. The rupture can occur in the matrix, between plies, and at the fiber-matrix interface level.

3 Fiber reinforced polymers behavior under high temperature and fire

Synthetic fibers can maintain their strength at relatively high temperature. Yet, most polymers are vulnerable at much lower temperature due to their low glace transition temperature Tg. Hajiloo et al. [START_REF] Hajiloo | Mechanical properties of gfrp reinforcing bars at high temperatures[END_REF] studied GFRP reinforced bars mechanical behavior under severe conditions. All bars lost their strength and stiffness at elevated temperature. Another study [START_REF] Kabir | Pull-out strengths of gfrp-concrete bond exposed to applied environmental conditions[END_REF] revealed that high temperature could enhance GFRPs' strength when it is under the material's Tg. Exposed to heat, GFRP components can ignite and sustain flaming combustion during a short time period [START_REF] Correia | A review of the fire behaviour of pultruded gfrp structural profiles for civil engineering applications[END_REF]. The flames spread depends on several factors essentially the resin type and flammability and the fiber content. The decomposition of the composite polymeric matrix releases fine soot particles and non-combustible fiber micro-fragments that may induce dense smoke. Hawileh et al [START_REF] Hawileh | Thermal analysis of gfrp-reinforced continuous concrete decks subjected to top fire[END_REF] carried out a numerical study in order to investigate the behavior of continuous concrete decks doubly reinforced with top and bottom GFRP bars subjected to top surface fire. The study revealed that the top concrete cover thickness is the most important parameter that influences the fire resistance of GFRP reinforced concrete slabs when exposed to top fire loading.

Composite surface treatment before bonding

At their raw state, composite materials have poor surface adhesion properties [START_REF] Baldan | Adhesion phenomena in bonded joints[END_REF]. Hence surface treatment before bonding is necessary in order to improve the surface quality. Mechanical surface treatment such as sanding [START_REF] Yang | The influence of surface treatment on the tensile properties of carbon fiber-reinforced epoxy compositesbonded joints[END_REF][START_REF] Sorrentino | Surface treatment of cfrp: influence on single lap joint performances[END_REF], sandblasting [START_REF] Sorrentino | Surface treatment of cfrp: influence on single lap joint performances[END_REF], peel ply [START_REF] Bénard | Peel ply surface treatment for composite assemblies: Chemistry and morphology effects[END_REF][START_REF] Bénard | Influence of fibre reinforcement and peel ply surface treatment towards adhesion of composite surfaces[END_REF][START_REF] Sorrentino | Surface treatment of cfrp: influence on single lap joint performances[END_REF] and milling [START_REF] Ghalme | Parameter optimization in milling of glass fiber reinforced plastic (gfrp) using doe-taguchi method[END_REF] improve mechanical anchoring between joined materials by roughening the surface, creating more areas for bonding and enhancing the surface free energy. Chemical surface treatment such as plasma and corona discharge [START_REF] Blackman | The plasma treatment of thermoplastic fibre composites for adhesive bonding[END_REF] reinforce high energy chemical interactions between the composite and the adhesive. Peel ply is a no-complicated low cost surface treatment. The effect of this treatment depends on the peel ply fabric nature, its grammage and fiber size. Polyamide tear-off fabrics were proven to provide more adhesion strength to composite bonded structures than polyester tear-off fabrics [START_REF] Bénard | Peel ply surface treatment for composite assemblies: Chemistry and morphology effects[END_REF][START_REF] Bénard | Influence of fibre reinforcement and peel ply surface treatment towards adhesion of composite surfaces[END_REF]. Peel ply generates homogeneous surface with regular and controlled roughness. Materials with regular surface topography were reported to have high adhesion properties [START_REF] Huang | Experimental investigation of the strength of polymer-steel direct adhesion (psda) joints with micro-structures ablated by laser[END_REF]. Peel ply fiber remainings could cause surface defects and weaken the bonded substrates adhesion [START_REF] Sorrentino | Surface treatment of cfrp: influence on single lap joint performances[END_REF]. Hence, cleaning the surface after treatment is highly recommended. Abrasion treatments such as sanding and sandblasting were also proven to highly improve the adhesion properties of composite materials. The effect of these treatments depends on the abrasive grains grit size [START_REF] Yang | The influence of surface treatment on the tensile properties of carbon fiber-reinforced epoxy compositesbonded joints[END_REF][START_REF] Bechikh | Sandblasting parameter variation effect on galvanized steel surface chemical composition, roughness and free energy[END_REF]. Sanding and sandblasting were reported to cause fiber exposure at the treated surface level and in some cases fiber damage and sand residues. Milling could also be used as a surface treatment for composite materials [START_REF] Ghalme | Parameter optimization in milling of glass fiber reinforced plastic (gfrp) using doe-taguchi method[END_REF]. Similar to sandblasting, the effect of this treatment depends on machining parameters.


Bogdan Nicolae
email: bogdan.nicolae@acm.org

DataStates: Towards Lightweight Data Models for Deep Learning

Keywords: deep learning, state preservation, clone, model reuse

A key emerging pattern in deep learning applications is the need to capture intermediate DNN model snapshots and preserve or clone them to explore a large number of alternative training and/or inference paths. However, with increasing model complexity and new training approaches that mix data, model, pipeline and layer-wise parallelism, this pattern is challenging to address in a scalable and efficient manner. To this end, this position paper advocates for rethinking how to represent and manipulate DNN learning models. It relies on a broader notion of data states, a collection of annotated, potentially distributed data sets (tensors in the case of DNN models) that AI applications can capture at key moments during the runtime and revisit/reuse later. Instead explicitly interacting with the storage layer (e.g., write to a file), users can "tag" DNN models at key moments during runtime with metadata that expresses attributes and persistency/movement semantics. A highperformance runtime is the responsible to interpret the metadata and perform the necessary actions in the background, while offering a rich interface to find data states of interest. Using this approach has benefits at several levels: new capabilities, performance portability, high performance and scalability.

Introduction

Deep learning applications are rapidly gaining traction both in industry and scientific computing. A key driver for this trend has been the unprecedented accumulation of big data, which exposes plentiful learning opportunities thanks to its massive size and variety. Unsurprisingly, there has been significant interest to adopt deep learning at very large scale on supercomputing infrastructures in a wide range of scientific areas: fusion energy science, computational fluid dynamics, lattice quantum chromodynamics, virtual drug response prediction, cancer research, etc.

Initially, scientific applications have gradually adopted deep learning more or less in an ad-hoc fashion: searching for the best deep neural network (DNN) model configuration and hyperparameters through trial-and-error, studying the tolerance to outliers by training with and without certain datasets, etc. Often, the lack of explainability, i.e., being able to understand why a DNN model learned certain patterns and what correlations can be made between these patterns and the training datasets was overlooked if the results were satisfactory. However, with increasing complexity of the DNN models and the explosion of the training datasets, such a trend is not sustainable. Scientific applications are particularly affected by this because they are often mission-critical (e.g., a patient misdiagnosis can have severe consequences), unlike many industrial applications (e.g., a misclassification of a picture as a dog instead of a cat is mostly harmless).

In a quest to solve this challenge, systematic approaches are beginning to emerge: guided model discovery where the DNN architecture [START_REF] Real | Large-scale evolution of image classifiers[END_REF] and hyperparameters [START_REF] Balaprakash | Scalable reinforcement-learning-based neural architecture search for cancer deep learning research[END_REF] are automatically identified, sensitivity analysis [START_REF] Shu | Sensitivity analysis of deep neural networks[END_REF], which is used to identify what parts/layers of the DNN model and/or training samples are the most influential the learning process and how robust the DNN model is regarding tolerance to outliers or transfer learning (i.e., ability to reuse the learned patterns to solve related problems), etc.

All these approaches rely on several fundamental data management abilities: (1) capture intermediate snapshots of the DNN model in order to study its evolution in time and potentially reuse it later; (2) clone a DNN model whose training has progressed up to a point into many parallel alternatives where slight variations are introduced; (3) apply the FAIR principles [START_REF]The fair guiding principles for scientific data management and stewardship[END_REF] (findable, accessible, interoperable, reusable) to the snapshots, to make it easy to navigate through their evolution and/or search for interesting snapshots that can be reused.

However, with increasing complexity and sizes of DNN models and training data, a mix of data parallel, model parallel, pipeline parallel and layer-wise parallel approaches are emerging to speed-up the training process. In this context, a training instance is not a single process anymore, but an entire group of tightly coupled processes that are distributed across many devices and/or compute nodes of large scale HPC infrastructures. Such groups of processes collaboratively work on a shared, distributed DNN model state, exhibiting specific properties and access patterns. In addition, HPC data centers are increasingly equipped with complex heterogeneous storage stacks (multi-level memory hierarchies on compute nodes, distributed caches and burst buffers, key-value stores, parallel file systems, etc.). Under such circumstances, the fundamental data management abilities mentioned above become highly challenging to implement in a scalable and efficient manner.

In this position paper we advocate for DataStates, a new data model that addresses the aforementioned challenges by rethinking how to represent and manipulate scientific datasets. At its core is the notion of a data state, which is a collection of annotated, potentially distributed data structures that applications can capture at key moments during the runtime and revisit/reuse later. Instead explicitly interacting with the storage layer (e.g., to save the dataset into a file), users define such coupled datasets and "tag" them at key moments during runtime with metadata that expresses attributes and persistency/movement semantics. Tagging triggers asynchronous, high performance I/O strategies that run in the background and capture a consistent snapshot of the datasets and associated metadata into the lineage, a history that records the evolution of the snapshots. Using dedicated primitives, users can easily navigate the lineage to identify and revisit snapshots of interest (based on attributes and/or content) and roll back or evolve the lineage in a different parallel direction.

Using this approach, clone and revisit of DNN model states become lightweight primitives focused on high performance, scalability and FAIR capabilities, which not only accelerates existing approaches for model exploration, sensitivity analysis and explainability, but also encourages new algorithms and techniques that can take advantage of frequent reuse of intermediate DNN models. We summarize our contributions as follows:

-We discuss a series of challenges and opportunities that arise in the context of deep learning, where a mix of data parallel, model parallel, pipeline parallel and layer-wise parallel approaches are increasingly applied to improve the performance and scalability of the training (Section 2). -We introduce an overview of DataStates, the data model and runtime we advocate in this paper. We insist both on how the notion of data states can be used as a fundamental abstraction to capture, search for and reuse intermediate datasets, as well as the advantages of such an abstraction (Section 3). -We position DataStates in the context of state-of-art, insisting both on the gaps filled by our approach and the complementarity that can be achieved by using DataStates in conjunction in other approaches (Section 4).

Background

Deep learning approaches have evolved from independent training and inference into complex workflows (Figure 1): they involve training sample pre-processing and augmentation (e.g., create more training samples by stretching or rotating images), model discovery (both DNN architecture and hyperparameters), training and validation of the inference, sensitivity analysis used to explain the model and/or influence the data pre-processing and model discovery. In this context, there is a need to explore a large number of alternatives, which applies for each step of the workflow. For example, model discovery strategies based on evolutionary techniques [START_REF] Real | Large-scale evolution of image classifiers[END_REF] (such as genetic algorithms) need to maintain a large population of promising DNN model individuals, which are combined and/or mutated in the hope of obtaining better individuals. Training a DNN model may also involve alternatives, especially in the case of reinforcement learning [START_REF] Zhang | Deep residual reinforcement learning[END_REF], where there are multiple variations of environments and alternative actions possible. DNN models with early exits [START_REF] Teerapittayanon | Branchynet: Fast inference via early exiting from deep neural networks[END_REF] are becoming increasingly popular: in this case, the inference can take alternative shorter (and thus faster) paths through the model layers when they provide sufficient accuracy (e.g., nonambiguous regions in a classification problem). Sensitivity analysis [START_REF] Shu | Sensitivity analysis of deep neural networks[END_REF] needs to explore many alternative training paths that include/exclude certain training samples and/or layers in order to understand their impact. For example, CAN-DLE [START_REF] Wozniak | Candle/supervisor: A workflow framework for machine learning applied to cancer research[END_REF] (Cancer Deep Learning Environment) employs an approach where the Such alternatives introduce the need for advanced data management approaches: capture intermediate DNN model/layer snapshots as the training (or inference) progresses and then either preserve them for later study/revisiting, or clone them for the purpose of forking the training (or inference) into different parallel directions. To make these snapshots usable, several capabilities related to the FAIR principles (findable, accessible, interoperable, reusable) are needed: automatically capture the evolution of the snapshots, expose their properties, enable search based on such properties, reshape the snapshots on-the-fly to adapt to a new context where it needs to be used.

However, providing such advanced data management capabilities is challenging, because DNN training approaches are constantly being adapted to take advantage of large-scale infrastructures. In this context, the most widely used technique is synchronous data-parallel training. It creates replicas of the DNN model on multiple workers, each of which is placed on a different device and/or compute node. We denote such workers as ranks, which is the terminology typically used in high performance computing (HPC). The idea is to train each replica in parallel with a different mini-batch, which can be done in an embarrassingly parallel fashion during the forward pass on all ranks. Then, during back-propagation, the weights are not updated based on the local gradients, but using global average gradients computed across all ranks using all-reduce operations. This effectively results in all ranks learning the same pattern, to which each individual rank has contributed. The process is illustrated in Figure 2(a).

Model parallelism [START_REF] Dean | Large scale distributed deep networks[END_REF] is another complementary approach (Figure 3). It works by partitioning the DNN model across multiple ranks, each of which is running on a different device and/or compute node. This solves the problem of large DNN models that do not fit in the memory of a rank, but requires data transfers between operations and disallows parallelism within an operation.

Pipeline parallelism [START_REF] Narayanan | Pipedream: Generalized pipeline parallelism for dnn training[END_REF] combines model parallelism with data parallelism. The idea is to partition the DNN model into stages, each of which is made of one or more layers (and can be replicated like in the case of data-parallelism). Each stage is assigned to a different rank, which effectively form a pipeline (Figure 2(b)). Unlike data and model parallelism, where only one mini-batch is active at a given moment for the whole duration of the training step, pipeline parallelism injects multiple mini-batches into the stages one after the other: during the forward pass, each stage sends the output activations to the next stage, while simultaneously starting to process another mini-batch. Similarly, after completing the backward-propagation for a mini-batch, each stage sends the gradients to the previous stage and begins to process another mini-batch.

DL algorithms take advantage of multi-core and hybrid architectures (e.g., CPUs + GPUs) to parallelize the gradient computation and weight updates. Specifically, once a rank has finished computing the local gradients for a layer, it immediately proceeds to compute the local gradients of the previous layer. At the same time, it waits for all other ranks to finish computing their local gradients for the same layer, then updates the weights (based on the average gradients obtained using all-reduce in the case of data-parallelism). This is called layer-wise parallelism. Another way of reasoning about this process is by means of a DAG (directed acyclic graph), where each layer is a pipeline: compute local gradients, average gradients globally, update weights. The local gradient computation of each layer is a dependency for both the local gradient computation of the previous layer and the rest of the pipeline: once it is complete, both paths in the DAG can be executed in parallel.

As a consequence, the distributed nature of DNN model snapshots and the complex multi-level parallelism considerations make the problem of capturing and preserving/cloning intermediate DNN model snapshots non-trivial. This is further augmented by the need to adopt the FAIR principles and the increasingly complex heterogeneous storage stacks [START_REF] Lockwood | Storage 2020: A vision for the future of hpc storage[END_REF] that are deployed in modern HPC data centers. Nevertheless, there are also significant opportunities in this space: according to our previous study [START_REF] Li | Understanding scalability and finegrain parallelism of synchronous data parallel training[END_REF], the combination of data parallelism and layer-wise parallelism leads to subtle delays that can be exploited to to overlap the back-propagation with fine-grain asynchronous data management operations in the background, which can significantly reduce their overhead. We demonstrated the feasibility of this idea both for DNN model checkpointing [START_REF] Nicolae | Deepfreeze: Towards scalable asynchronous checkpointing of deep learning models[END_REF] and DNN model cloning [START_REF] Nicolae | DeepClone: Lightweight State Replication of Deep Learning Models for Data Parallel Training[END_REF], obtaining an overhead reduction of an order of magnitude compared with other state-of-art alternatives.

DataStates: An Overview

In this section, we introduce the main ideas and principles behind DataStates, the data model we advocate in this paper.

In a nutshell, a data state is a collection of annotated, potentially distributed data structures that applications can capture at key moments during the runtime. For the purpose of this work, we assume such distributed data structures to represent the DNN model state. The application indicates such key moments explicitly (noting that automation of this process opens an interesting research question). More formally, a data state is tuple (C, M s , M a ) that defines a content C and any associated metadata M s and M a . We differentiate between summary metadata (denoted M s ), used to label and/or summarize C, and actionable metadata (denoted M a ), used to express intents over how C is managed. These intents take the form of hints (e.g., access pattern) and/or properties (e.g., durability, scope, relationship to other data states). Users do not care how the intent is materialized: it is the job of the DataStates runtime to formulate an appropriate plan through a series of actions, which in our case refer to persisting, caching and fetching a data state. This is a general principle: new intents and action plans can be added as needed.

Many distributed ranks (owners) can share the same data state and mutate it collaboratively by updating its content and/or metadata. We assume the owners are directly responsible for concurrency control and consistency, which in our case is transparently handled by the deep learning frameworks. When the owners reach a key moment during runtime (e.g., an epoch of the training has finished), they tag the data state. This triggers a transition into a new data state. From the owner's perspective, nothing changed: they can continue working on C as usual. Meanwhile, in the background, the runtime applies the action plan corresponding to M a for the original data state as it was at the moment of tagging. The runtime guarantees that any side effects due to the action plan are tied to the original data state and do not affect the new data state (which may trigger internal temporary copies during tagging or copy-on-write). A data state that was tagged is stable if its action plan completed successfully and unstable otherwise. It is illegal to access unstable states, but the runtime offers support to query about their status and wait for them to become stable.

Both the data states and the transitions between them are recorded into the lineage, which keeps the evolution of the data states. The lineage exposes primitives to navigate (i.e., move to a successor or predecessor) and to search (i.e., find data states that satisfy given properties) the lineage. Applications can use such primitives to discover and visit interesting data states. For example, this can be used to follow the evolution of tagged DNN model states during training or to search for previously tagged intermediate DNN models based on their accuracy and/or other attributes. Furthermore, each data state can be part of one or more scopes, which are explicitly specified in M a . To avoid the explosion of storage space utilization, non-critical data states that have gone out of scope (e.g., non-critical or locally relevant intermediate DNN models) and their transitions can be pruned from the lineage as needed. Pruning is subject to garbage collection algorithms, but can also be triggered explicitly through a dedicated primitive.

The lineage can be combined with two additional powerful primitives: fork and reshape. Both of them are similar to tagging (i.e., they trigger a transition to a new data state and the execution of an asynchronous action plan) but with important differences. Fork creates a clone of the data state on an entirely different set of processes and "splits" the lineage into two independent directions that can evolve separately. For example, fork can be used to explore an alternative direction for training a DNN model (e.g., using different hyper-parameters and/or training samples). Reshape enables the processes to change the layout and/or distribution of C, by specifying appropriate attributes in M a . Specifically, this refers to operations such as migrate (to different processes) and shuffle (i.e., ex-change pieces of C between processes, which is a common pattern in distributed training of DNN models). Combined with tagging and search/navigation, these two primitives allow flexible strategies to explore multiple parallel evolutions and revisit/reuse previous data states. Note the versatility of reshape, which can be extended with multiple other patterns. For example, data states could be used to record a lineage for Tensorflow [START_REF] Abadi | TensorFlow: Large-scale machine learning on heterogeneous systems[END_REF] by introducing support for tensor operations: slice, rebalance, stack, etc.

This approach has several advantages. First, it introduces native constructs that addresses the FAIR (findable, accessible, inter-operable, reusable) principles [START_REF]The fair guiding principles for scientific data management and stewardship[END_REF]: (1) findability is directly enabled by the lineage through navigation and search capabilities; (2) accessibility is enabled in a declarative fashion by specifying the desired intent (thus freeing applications from having to worry where their data is and how to bring it where it is needed); (3) inter-operability hiding the implementation of the I/O strategies from the user (thus eliminating differences in the interpretation of actionable metadata); (4) reusability is naturally facilitated by a single, unified view of all data states and the relationship between them, which can be revisited as desired.

Second, the separation of the intents from the actual implementation of the constraints and desired effects they represent is an important step towards performance portability, i.e., avoiding the need to customize the application codes on each machine to account for differences in performance characteristics, custom vendor APIs, etc. Specifically, since data states capture the intent only, action plans can be customized for a dedicated supercomputing infrastructure, potentially taking advantage of differences in architecture, performance characteristics of heterogeneous storage and vendor-specific features in order to introduce specific optimizations.

Third, the design of DataStates is lightweight and data-centric. DataStates is focused on the evolution of data and metadata alone, leaving other components to worry about computational and synchronization aspects. The data states are wrapping in-memory user data structures directly and are close to their intended life-cycle, therefore minimizing overheads related to data movements (which is not the case when using external repositories). Furthermore, DataStates masks the data management overhead asynchronously in the background, therefore minimizing the interruption of the application. Combined with clever interleaving of such asynchronous operations at fine-granularity during the backpropagation, this approach becomes crucial in facilitating the goal of achieving high performance and scalability.

Related Work and Positioning

Checkpoint-restart is a well researched HPC pattern relevant in the context of clone and revisit. In this regard, multi-level checkpointing, as adopted by frameworks such as SCR [START_REF] Moody | Design, modeling, and evaluation of a scalable multi-level checkpointing system[END_REF] and FTI [START_REF] Bautista-Gomez | FTI: High performance fault tolerance interface for hybrid systems[END_REF], is a popular approach that leverages complementary strategies adapted for HPC storage hierarchies. VELOC [START_REF] Nicolae | VeloC: Towards high performance adaptive asynchronous checkpointing at large scale[END_REF][START_REF] Tseng | Towards portable online prediction of network utilization using MPI-level monitoring[END_REF] takes this approach further by introducing asynchronous techniques to apply such complementary strategies in the background. When the checkpoints of different processes have similar content, techniques such as [START_REF] Nicolae | Towards Scalable Checkpoint Restart: A Collective Inline Memory Contents Deduplication Proposal[END_REF][START_REF] Nicolae | Leveraging naturally distributed data redundancy to reduce collective I/O replication overhead[END_REF] can be applied to complement multi-level checkpointing. However, redundancy is detected onthe-fly, which can be an unnecessary overhead for clone and revisit (e.g., model replicas are known to be identical for data-parallel training). Dedicated checkpointing techniques for deep learning are rudimentary: TensorFlow checkpoints model to files in its SavedModel format,1 or in HDF5 files through Keras. 2These file-based methods, while simple and adapted for single-node training, are becoming a bottleneck when scaling data-parallel training to a large number of compute nodes. Our own previous work [START_REF] Nicolae | Deepfreeze: Towards scalable asynchronous checkpointing of deep learning models[END_REF][START_REF] Nicolae | DeepClone: Lightweight State Replication of Deep Learning Models for Data Parallel Training[END_REF] introduced scalable approaches to address these limitations. Although not flexible enough in the general clone and revisit scenarios, they can be used as a building block for DataStates.

In a quest to achieve scalability and flexibility, HPC storage stacks have become increasingly heterogeneous [START_REF] Lockwood | Storage 2020: A vision for the future of hpc storage[END_REF]. In addition to parallel file systems, modern supercomputers feature a variety of additional storage subsystems (e.g., burst buffers [START_REF] Cao | To share or not to share: Comparing burst buffer architectures[END_REF] or key-value stores such as DAOS [START_REF] Lofstead | Daos and friends: A proposal for an exascale storage system[END_REF]) and deep memory hierarchies (HBM, DDRAM, NVM). Such storage subsystems focus on raw I/O performance acceleration by implementing low-level read/write or put/get abstractions. They complement well the rigid POSIX model used by parallel file systems (e.g., lack of efficient support for fine-grained I/O operations and concurrency control). However, this is not enough to implement the high-level capabilities necessary for clone and revisit. Furthermore, the large diversity of services leads to added complexity and limited sharing and reuse potential because of the lack of performance portability.

In the big data community, Spark [START_REF] Zaharia | Spark: Cluster computing with working sets[END_REF][START_REF] Shanahan | Large scale distributed data science using apache spark[END_REF] has gained considerable traction as a generic analytics framework. Part of its success lies in the functional data processing model that hides the details of parallelism from the user, enabling ease of use and performance portability through high-level in-memory transformations. Notable in this context is the concept of RDDs [START_REF] Zaharia | Resilient distributed datasets: A fault-tolerant abstraction for in-memory cluster computing[END_REF] (Resilient Distributed Data Sets), which are Spark's abstraction for intermediate data. Despite efforts to leverage heterogeneous storage for RDDs (e.g., Apache Ignite [START_REF] Bhuiyan | High Performance In-memory Computing with Apache Ignite[END_REF]), they are tied to the rigid programming model of Spark, which emphasizes loosely coupled patterns and high-level languages that trade off performance for productivity. Therefore, such abstractions are unsuitable for the HPC ecosystem, which emphasizes high performance and scalability, tightly-coupled patterns and hybrid programming models.

Provenance tracking and reproducibility is another area closely related to DataStates. In the HPC ecosystem, EMPRESS [START_REF] Lawson | Empress: extensible metadata provider for extreme-scale scientific simulations[END_REF] aims to provide an alternative to rudimentary attribute capabilities offered by HDF5 and NetCDF through extensible metadata. This broadens the scope beyond single files or applicationspecific formats, but does not feature a lineage. In the Spark ecosystem, RDDs feature a computation-centric lineage that records what data transformations were applied. This lineage is hidden from the application and used internally to recompute RDDs (e.g., in case of failures or need to reuse). By contrast, DataStates has the opposite goal: a lineage that records actual data snapshots annotated with metadata (thus avoiding expensive recomputation), which is exposed to the application and used as a tool to revisit previous states. In itself, this is already a powerful introspection mechanism that aids provenance tracking and reproducibility. Of course, there is value in combining both approaches to create a complete picture. Unfortunately, capturing the computational context in the HPC ecosystem is nontrivial, as it involves a large number of libraries and runtimes. Containers are one possible solution and are used by approaches such as Data Pallets [START_REF] Lofstead | Data pallets: Containerizing storage for reproducibility and traceability[END_REF]. DataStates can complement well such efforts.

Versioning and revision control systems (e.g. SVN [START_REF] Collins-Sussman | The subversion project: Buiding a better cvs[END_REF], GIT [START_REF] Chacon | Pro Git. Apress[END_REF], Mercurial [START_REF] Bernard | Mercurial-revision control approximated[END_REF]) are widely used to keep track of changes to source code during software development. They feature native support for data-centric provenance: users can keep track of successive changes and revisit, roll-back, branch, merge, etc. They also feature an entire array of space-efficient techniques to store only incremental differences. However, these optimizations are designed for text data (mostly source code) and are not designed for high-performance and scalability (they assume each user has room to maintain a whole local copy of the repository). Systems were proposed before to address this issue: For example, BlobSeer [START_REF] Nicolae | BlobSeer: Nextgeneration data management for large scale infrastructures[END_REF] is a distributed data store for binary large objects that manages intermediate snapshots much like revision control systems. However, it was not designed to handle heterogeneous data and metadata (its abstraction is a blob, i.e., a large sequence of bytes): largely, it behaves like a key-value store with versioning support, therefore missing support to search and navigate the history.

Repositories for VM images [START_REF] Saurabh | Vm image repository and distribution models for federated clouds: State of the art, possible directions and open issues[END_REF] and containers (e.g. Docker [START_REF] Merkel | Docker: Lightweight linux containers for consistent development and deployment[END_REF]) are an industry standard to facilitate collaboration and sharing between multiple users for computational environments. In a similar spirit, recent efforts such as DLHub [START_REF] Chard | Publishing and serving machine learning models with dlhub[END_REF] aim to build model repositories for deep learning applications: users publish, discover and share full models, including dependencies (e.g., Python environment), into executable servables (that may include Docker images, Amazon S3 buckets, etc.) through REST APIs. DataStates also focuses on enabling search and reuse semantics, but from a different perspective: it introduces a general data model (useful beyond deep learning), lightweight (HPC-oriented) and data life-cycle oriented (mix ephemeral with persistent data, leverage local storage and in-situ capabilities, data-centric lineage). This is more appropriate for the DNN model clone and revisit scenarios we target, where an external repository can become a bottleneck. On the other hand, DataStates is well complemented by approaches like DLHub, as they can handle security and other aspects needed to enable multi-user sharing beyond a single supercomputer.

Conclusions

In this position paper we have introduced DataStates, a new data model that exposes high-level primitives to capture, fork, search and reuse of scientific datasets. Such high-level primitives are especially important for an efficient implementa-tion of many deep learning scenarios that involve the need to capture intermediate DNN models and explore a large number of alternative training and/or inference paths.

Despite increasing complexity due to distributed DNN model state, as well as a mix of distributed training approaches (data, model, pipeline, layer-wise parallel), DataStates is well positioned to leverage the opportunity such circumstances present, especially with respect to overlapping the back-propagation phase of training with asynchronous fine-grain operation in the background in order to progress on data management aspects with minimal overhead on an ongoing training. Additionally, DataStates has three other advantages: it brings FAIR (findable, accessible, inter-operable, reusable) semantics to deep learning frameworks, it enables performance portability by separating data management intents (defined by the user) from actions necessary to satisfy them, it enables high performance and scalability by introducing lightweight, in-situ data manipulation semantics that are close to the data life-cycle of DNN models.

Encouraged by promising initial results, especially for the related problem of scalable checkpointing and cloning of DNN models for data-parallel training approaches, we plan to illustrate in future work the benefits of DataStates in the context of deep learning.

Fig. 1 .

 1 Fig. 1. Structure of a modern deep learning workflow

  (a) Data parallelism: DNN model is replicated, local gradients are averaged. (b) Pipeline parallelism: DNN model partitioned and distributed as stages (full layers).

Fig. 2 .

 2 Fig. 2. Data parallelism vs. pipeline parallelism (adapted from [19])

Fig. 3 .

 3 Fig. 3. Model parallelism: DNN model is partitioned and distributed

https://www.tensorflow.org/guide/saved model

https://www.tensorflow.org/guide/keras/save and serialize

Acknowledgments

This material is based upon work supported by the U.S. Department of Energy (DOE), Office of Science, Office of Advanced Scientific Computing Research, under Contract DE-AC02-06CH11357.


Claus Traulsen

Jérôme Cornet

Matthieu Moy

Florence Maraninchi

A SystemC/TLM semantics in Promela and its possible applications

SystemC has become a de-facto standard for the modeling of systems-on-a-chip, at various levels of abstraction, including the so-called transaction level (TL). Verifying properties of a TL model requires that SystemC be translated into some formally defined language for which there exist verification back-ends. Since SystemC has no formal semantics, this includes a careful encoding of the SystemC scheduler, which has both synchronous and asynchronous features, and a notion of time. In a previous work, we described LusSy [14] a complete chain from Sys-temC to a synchronous formalism and its associated verification tools. In this paper, we describe the encoding of the SystemC scheduler into a asynchronous formalism, namely Promela (the input language for Spin). We comment on the possible uses of this new encoding, and compare it with the synchronous encoding.

Introduction

SystemC [START_REF]IEEE 1666: SystemC Language Reference Manual[END_REF] is a C++ library/language used for the description of Systems-ona-Chip (SoCs) at different levels of abstraction, from cycle-accurate to purely functional models. It comes with a simulation environment, and is becoming a de facto standard in the SoCs industry. SystemC is being increasingly used for writing the Transaction Level Models (TLM) [START_REF]Transaction Level Modeling with SystemC, TLM Concepts and Applications for Embedded Systems[END_REF] that allow embedded software development on a virtual prototype of the final chip.

A TL model written in SystemC is based on an architecture, i.e., a set of components and connections between them. Components behave in parallel. Each component has typed connection ports. Its behavior is given by a set of communicating processes programmed in full C++ and managed by a non-preemptive scheduler. Synchronization mechanisms include events, which can be waited for or notified. A process can yield back to the scheduler either by waiting for an event or by waiting for a given period of time to elapse.

Communications between modules proceed by function calls traversing components or communications channels (for instance bus models). At the transaction level, such function calls are used to model two types of communication: transactions (atomic exchange of data between modules) and interrupts.

Since the TL models become to be considered as reference models in the SoC design flow, it is necessary to validate properties at this level of abstraction. This is currently done by intensive testing, but formal verification is being investigated for some years now, in both industry and academia. However, the definition of SystemC, while being an IEEE norm, lacks formal semantics. Some work on verifying properties of SoC assume that they are described in some parallel formalism inspired by SystemC. Sometimes this formalism only reflects the register-transfer-level (RTL) and cannot be used to express the specificities of a TL model. Formal verification for RTL designs has been studied a lot, and providing such analysis for designs written in SystemC does not bring new results. Moreover, even if the formalism reflects the transaction level of abstraction, it is often quite far from real SystemC designs (see Section 5).

We are interested in verifying properties of real SystemC designs, at the transaction level. This requires that SystemC and TLM-specific features be translated into some formally defined language for which there exists verification back-ends. This includes a careful encoding of the SystemC scheduler, which has both synchronous and asynchronous features, and a notion of time.

Choosing the formal language in which to translate SystemC is important because it often restricts the set of verification back-ends that can be applied. If we translate SystemC into a symbolic synchronous formalism, we have access to tools like the Lustre [START_REF] Halbwachs | Programming and verifying critical systems by means of the synchronous data-flow programming language lustre[END_REF], SMV [START_REF] Mcmillan | The SMV system[END_REF] or Esterel [START_REF] Berry | The foundations of Esterel. Proof, Language and Interaction: Essays in Honour of Robin Milner[END_REF] tool-chains; if we translate it into an asynchronous formalism, we have access to Spin [START_REF] Holzmann | The SPIN Model Checker[END_REF], IF [3], etc. Since the semantics of SystemC processes is neither entirely synchronous, nor entirely asynchronous, any choice implies some encoding. The encoding itself may be responsible for a significant part of the model size.

Another important point is the way time is interpreted. Since SystemC contains explicit constructs to wait for time, the translation into the input language of a timed-model checker like IF [3] or UPPAAL [START_REF] Kim | Uppaal in a Nutshell[END_REF] could seem to be an appropriate choice. However, we do not need the full expressive power of timed automata to encode SystemC, and using timed automata would imply to pay the price of the symbolic analysis needed for clocks in the verification back-ends. Consequently, we will choose a discrete interpretation of time in SystemC, and encode timers into some ordinary variables.

In a previous work [START_REF] Moy | LusSy: an open Tool for the Analysis of Systems-on-a-Chip at the Transaction Level[END_REF][START_REF] Moy | Techniques and Tools for the Verification of Systems-on-a-Chip at the Transaction Level[END_REF], we described a complete chain from SystemC to a synchronous formalism. It is based upon a systematic encoding of SystemC processes into a flavor of synchronous automata. In such a case, SystemC processes are encoded one by one into automata, communicating with an additional automaton that encodes the scheduler specification. The automata corresponding to the user processes are produced specifically to communicate with this scheduler automaton, using additional synchronous signals and the instantaneous dialogue mechanism available in a pure synchronous semantics. The set of automata can then be translated into several synchronous formalisms (SMV [START_REF] Mcmillan | The SMV system[END_REF] input, Lustre), without computing the intrinsic products between them, hence delegating the potential state explosion to the verification back-ends that are better equipped to tackle the problem. Another good property of the translation into Lustre is that we get something executable. It means that we can, at least, compare the Lustre encoding with the official SystemC semantics, on benchmark programs.

However, the encoding into a synchronous formalism renders manual reading difficult, and the amount of additional synchronizations needed to reflect the semantics of SystemC can be put in question again.

Another approach would be to define a direct semantics by using an adhoc product to represent the effect of the scheduler. While the latter approach produces more readable results, the fact is that existing verification tools can not deal directly with ad-hoc products, but usually with well-known formalisms.

In this paper, we explore the encoding of the SystemC scheduler into an asynchronous formalism, namely Promela, the input language for the tool Spin. The translation into Promela, which has a well defined semantics, is another way to give a formal semantics to SystemC/TLM. Thanks to the simulator provided with Spin, the semantics is also executable, and it will be possible to test the faithfulness of the semantics w.r.t. the official scheduler.

So far, we experimented our translations for model-checking and intensive testing of properties like deadlocks and assertions.

The alternative encoding of SystemC into an asynchronous formalism will also allow the comparison of the two verification chains, with respect to the size of the models, the power of the verification tools, etc. In other words, we try to answer the following questions: for a given SystemC model, and a given property of it, is it more efficient to use a synchronous verification chain, or an asynchronous one? It may depend on the type of property.

The rest of the paper is structured as follows: Section 2 gives an short introduction to TL modeling with SystemC. Section 3 describes the translation and Section 4 how to use it for verification. We consider related work in Section 5 and conclude in Section 6.

Transaction Level Modeling with SystemC

Subset of SystemC

We briefly describe the main characteristics of SystemC, when used for transaction level models.

Globally, a TLM component, or module, is an encapsulated piece of code that contains active code (processes to be scheduled by the global scheduler) and passive code (functions offered to the external world, that will be called from a process of another component, by a control flow transfer). Inside such a component, the processes and the functions may share variables and events in order to synchronize with each other. Note that a function code and an active process are conceptually in parallel, since the function will be called by another flow of control.

In SystemC, the architecture of the platform is built by a piece of code (the so-called elaboration phase that runs first), but this is conceptually equivalent to a quite traditional architecture-description-language (ADL) that connects the ports exposed by the components.

Communications between modules proceed by function calls traversing components or communications channels (for instance bus models). SystemC provides built-in primitive communications channels such as sc_signal to model hardware signals at the Register Transfer Level of abstraction. Synchronization associated with the communications is performed by events and shared variables inside modules and/or channels.

Since we are only interested in modeling at transaction level, we make some strong assumptions on the SystemC code we analyze. We assume that we never use a built-in primitive channel or the synchronous update mechanism, which are used for RTL modeling. We consider two types of communications between modules: transactions and interrupts. Both types use blocking function calls (i.e., the caller is blocked until the callee terminate its code) implemented using the SystemC TLM Library [START_REF]SystemC Transaction Level Modeling Library 1[END_REF]. Interrupts proceed directly to the target module whereas transaction have to pass through a bus model that routes them to the corresponding target module, depending on the transaction address.

A Simple Example

Consider the simple example in Figure 1, consisting of two modules. The first module contains a process that waits for an event e1. After receiving the event, it waits an additional 7ns, before performing some action α. Here α is the abstraction of some real, local computation, an alternative way to see this is: the computation α takes 7ns. When α is finished, the first process will trigger an interrupt in the second module, by calling the function g. The first module also offers an interrupt port by the function f , which will notify the local event e1. Similarly, the second module contains a process that waits 5ns before performing β (or performs β, which takes 5ns). Thereafter it will trigger the interrupt in the first module, and wait for the event e2, i.e., for an interrupt that triggers the function g. The two processes will always be executed in lockstep. While this example is trivial, it contains the relevant parts of a TL model: waiting for event notification, waiting for time and function calls to other modules, which are used to model transactions and interrupts.

There exist three difficulties when defining the semantics of SystemC:

1. The non-preemptive scheduler: we have to ensure that a running process is not interrupted by any other process unless it explicitly relinquishes the control back to the scheduler, by performing a wait either on time or on an event. 2. The SystemC scheduler ensures that time can only elapse when no process is eligible (while SystemC has no control on real time, the simulation time is merely a counter that the scheduler can decide to increment or not). 3. Function call communications: they are used for both interrupts and transactions. A process P performing a function call communication lets its control flow go outside its component to finally reach the destination component where a function is executed. The execution of P may continue only after the function call is finished. This means that if the receiver's function performs a wait() statement, P will yield the control back to the scheduler, and when elected again will resume its execution in the receiver's function.

3 Expressing SystemC semantics in Promela

General Ideas

The Architecture First, we will abstract from the architecture description part. In a real SystemC design, the function that is actually called when a process P in a module M executes an instruction port.f() is determined by the link between the port port of M and a port p' on another module M containing a function f associated with p .

In the rest of the paper, we will consider that the architecture is hard coded in the function names. In other words, we will consider a process P calling a function f , and another module containing f .

Pre-processing for Functions The modeling of a SystemC program into Promela transforms each process and each function into a Promela process. SystemC distinguishes several types of processes (SC_THREAD, SC_METHOD, etc.). We consider here the use of SC_THREAD, which is the most general, since the encoding will not benefit from the restrictions enforced on the other types of processes.

We assume that we have performed a preprocessing on the SystemC program ensuring the following property: Each function is called by at most one process. The preprocessing consists in duplicating and renaming functions which are called multiple times. We ignore recursive calls, which is sound for transaction level models (communications functions are not used to compute values). Function parameters and return values are not represented but can be taken into account by using global variables for both.

To avoid such a pre-processing copy of the functions, we would need to use a formalism in which a single object can model a process that is being executed in several distinct instances at the same time. Petri nets would do the job, but the verification tools that are able to deal with such models (symbolically, without expanding the model) are usually more complex than Spin, and they are tailored for the cases where the number of copies is not known statically. In our case, since the number of copies of a function is indeed known statically, we do not need the expressive power of Petri nets, and the expansion can be performed before the verification tool is called.

We also assume that only one process waits for each event. Removing this limitation is a matter of encoding. n processes waiting for an event e can be transformed into n processes each waiting for its own event e i .

All time values appearing in the SystemC model must be integer multiples of some basic time granularity. We also assume that all variables can be declared globally, without any naming conflicts. All these restrictions can again be ensured by simple preprocessing of the SystemC program.

Intuitive Idea: Representation with Automata

Our translation to Promela can also be seen as a translation into a set of automata. Each process and each function is translated into one automaton. Guards and effects of transitions can either be the usual tests and assignments to Boolean or integer variables, or they can consider clocks. Clocks can either be tested for equality with a constant or a variable, or they can be set to 0.

The automata derived from Module 1 of the simple example can be found in Figure 2. They simply reflect the control structure of the SystemC code. The automata then have to be asynchronously interleaved, respecting the non-preemptive specification of the scheduler. To obtain this, the automata have two different kinds of states, which we represent as black and white states. Black states represent local control flow: when an automaton is in a black state, it may not be preempted by the scheduler. White states basically represent wait statements: when an automaton is in a white state, it can be preempted, hence interleaved with any other process. A special case is the one of function calls, which directly transfer the control to the automaton that implements the function. This means we have to synchronize the transitions labeled by call (resp. ret) with the corresponding transition labeled by begin (resp. end).

Since we are mainly interested in the synchronization between different modules, we will not describe all the possible data processing inside the modules. This abstracted code could also be represented by encoding its control flow using only black states. The key elements of SystemC are translated in the following way: wait(e, k ns)

wait(e)
1 X:=0 2 /e:=1 3 [X=k] {e=0} f() 1 ... begin(f) 2 end(f) port.f() 1 call(f) ret(f)

Detailed Encoding

In the following we will show how our encoding in Promela deals with the three problematic parts of SystemC: non-preemptive scheduling, time-elapse and function calls.

Non-preemptive scheduling We distinguish between control points where the scheduler may transfer the control to another process (white states), and internal control points (black states) of one process. The non-preemptive execution of one automaton is realized with an additional shared variable M of type int. This variable can take the value 0, to mean that any processes can perform one step, or N , to mean that the process number N is the only one to be activated. A graphical representation and the actual Spin encoding are shown in Figure 3. This variable is set to 0 by each process that performs a wait. Otherwise, a process sets M to its own identifier, to indicate that it will take an additional step. For function calls, M is used to transfer the control to another process explicitly without the possibility of any other interleaving. We also considered a different encoding that only relied on atomic sections in Promela to model non preemptivity. We sketch the problems with that approach in Section 3.5.

For simple examples, the use of an extra variable for ensuring atomicity is surely not efficient. We could use the atomic statement in Promela to ensure that no process can interleave a black state. In the trivial example in Figure 2, where each black state has exactly one incoming and one outgoing transition, we could also merge these and remove the black states all-together. But since the atomic behavior represented by the black states may be any complex controlflow, connected to white states by multiple in-and outgoing transitions, this simplification is not possible in the general case. Clocks For every process that waits for time, we declare a clock (see Figure 4). Since time is considered discrete, every clock is represented by an integer. A dedicated clock_update process increments the clocks synchronously as soon as no other process can run, which is tested using Promela's timeout statement. Hence time will never elapse if there is a instantaneous loop, i.e., when there exists a cycle in the automaton which never performs a wait. Before a wait occurs, the process resets the corresponding clock to zero. We flag for each clock X whether the corresponding process is currently waiting on it, with a Boolean variable X_used. A clock is reset to zero when no process waits for it, and it is never increased in this time (it is a dead variable). Hence, the values of the clock are in the range between 0 and the value of the corresponding wait. Additionally, a call sets M to the id of the automaton that implements f . Similarly, end sets M back to the value of the caller. Since each function is called by at most one process, this value is unique. Simply setting M, without using F is not sufficient, because we have to make sure that the caller is blocked until the function is completed. Since the function might perform a wait, the scheduler could otherwise decide to execute the caller again too early. Similarly, we have to prevent the function from being executed without being called.

If no process call a function, we could simply remove the function. On the other hand, it might be the case that our model is only partially defined, that is: one or several modules of the system are not known, and considered as blackboxes (possibly with Byzantine behavior). In this case, we can give an over approximation of the possible behavior of unknown modules, by assuming that a called function can take an arbitrary time, and that each process may call any function at any time. This is reflected by the macro state between call and ret.

Functions are used both to model interrupts and transactions in TLM. The call representing an interrupt is directly done to another module. On the other hand, transactions are handled by a bus that a routing depending on the transaction's address. In the examples, we forget about the bus, and for each transaction directly call the recipient component's function. This simplification assumes we have determined manually to which component each transaction is addressed. In the general case, the code responsible for routing, as well as specific bus behavior can be taken into account by modeling the functions and processes inside the bus, as automata, like any other component. We would then need at least an address parameter for each transaction function calls.

Simple Example

The global definitions and the clock update for the example can be found in Figure 6. First the scheduling variable is declared. The macro myturn is an abbreviation to indicate that an automaton is enabled, i.e., it is either itself in a black state, or all automata are in white states. Since we do not have variables in the example, we only need to declare the variables for the events. Additionally, we have a integer value and a Boolean flag for each clock, indicating whether we are currently waiting for the clock. Time may elapse, i.e., the update_clock process is enabled, when no other process can perform a step, all processes are in a white state and at least one process waits on time. Using X=X+X_used to update time assures that time will only elapse for a clock that is used. The Promela code for Module 1 can be found in Figure 7. Each process has a variable to store its active state and its id. We could also use the process id that is automatically assigned by Spin, but using a new value makes it easier to compute the id for function calls, without increasing the number of reachable states. The translation of the automata is straightforward. transition becomes an atomic action, that first tests whether the automata can run, i.e., it is in the right state and the guard evaluates to true. Thereafter the effect of the transition is performed and the new state is set. At last, the scheduling variable is set according to whether the new state is black or white and whether a function call or termination is performed. Since a clock is explicitly set to 0 before each wait, and only at such a point, we also set the clock to "used" when leaving state 3. Similarly, when state 4 is left, we declare the clock as "not used anymore". Labels that abstract real, local computations like alpha are printed.The code for Module 2 can be found in Figure 8.

a

Validation of the Semantics

The main benefit of a semantics for SystemC in Promela is the possibility to formally reason about properties of the model. But the simulation of the semantics is also very important.

Since SystemC itself is executable, having an executable semantics does not look like a big gain. But since we are performing some abstractions and transformations on the model, the simple possibility to execute the semantics and compare the resulting traces with the original SystemC model gives us confidence in the validity of the approach. See appendix B of [START_REF] Moy | Techniques and Tools for the Verification of Systems-on-a-Chip at the Transaction Level[END_REF] for an example on the problems that can occur when using a non-executable language to give semantics to a model. This worked very well, for our first encoding, which did not use gotos. However, we tried another expression of the semantics using a combination of atomicity and jumps (see section 3.5), which lead to unexpected results.

The scheduling of the parallel processes in the model is non-deterministic according to the SystemC specification. In practice, it depends on the implementation of the SystemC scheduler. An interactive simulation of the Promela model makes these choices explicit, by prompting the user.

Alternative Encoding

We also considered another encoding, which completely relied on Promela's atomic sections to model non-preemption. Each state was transformed into a goto label, followed by an atomic section that contained all outgoing transitions. Additionally, all black states where combined in one atomic section, including the labels. The semantics of Promela ensures that a jump from inside an atomic section to a label which is also contained in an atomic section preserves atomicity. The first problem with this encoding is, that we have to inline all functions, in order to tell to which point the function returns. But we have the benefit that we do not need the variable M for the scheduling, or the variables to hold the current state of each process. Furthermore, the implementation with gotos is much more efficient than using a loop with a non-deterministic choice.

But the main problem with this encoding is that the simulator of Spin interleaves jumps from atomic section to another atomic section (although the documentation and the prover do the opposite). While Spin proves properties that rely on the fact that such jumps are atomic, it also generates traces that violate the property.

The combination of gotos and atomic sections also make it impossible to use partial order reduction. Intuitively, goto m1 and atomic{goto m1} are equivalent when m1 is inside an atomic section, because a single statement is always atomic and every possible interleaving that could occur after the goto could as well occur before it. However, for the explicit atomic, Spin will not allow any interleaving neither after nor before the goto, when partial order reduction is enabled.

bool X =0; active proctype A (){ assert ( X ==0); } active proctype B (){ X =1; atomic { goto m0 }; atomic { skip ; : X =0 } } Fig. 9. A program, which verification depends on whether partial order reduction is enabled.

Consider for example the program in Figure 9. The assertion is violated, when B just executes X=1 before A is executed. Spin finds this error, when the program is verified without partial order reduction, while it proves that all assertions hold when partial order reduction is enabled.

Because of these problems, this encoding does not have the benefits of an executable semantics. That the output of a verification depends on verification parameters which should not affect them, makes it hard to understand, why a specific behavior is possible or not. Therefore, we choose the not so efficient, but more robust encoding as the default.

Verification

Generic Properties

There are a number of properties that should hold for every TL model. First, it should never deadlock. A deadlock might, for example, occur when a process is waiting for an event that is never notified. A deadlock in the SystemC model corresponds directly to the fact that all Promela processes are blocked. With Spin, this can be checked by verifying that no "invalid end states" exist, which is built in the prover. Since we only increase time when at least one process performs a wait on time, it can never be the case that the clock_update process runs forever, which would make it impossible for Spin to detect a deadlock. On the other hand, when all processes terminate, the update_clock process will be blocked. Therefore, we explicitly declare this states as a valid end state.

A deadlock might occur in the simple example in Figure 1, if we remove the wait(5, SC_NS) from the second process. Then the scheduler can choose to execute the second process first, and let it notify the event without a process waiting for it (this is indeed a common error for SystemC programmers). In the following, both processes wait for events, but none is ever notified.

Another property we want to assure, is that no process runs forever without yielding. This can be expressed by the formula ♦M = 0. For models with clocks, we can also check that time will always elapse, using the formula ♦enabled(update clock). Of course, these last two properties are liveness formula and can only be checked if all abstractions preserve them (over-approximations of the behaviors preserve safety properties, but do not preserve liveness properties, in general). For the simple example, we do not need to perform any abstractions at all. If, however, the model becomes too large, the first abstraction that comes to mind is to remove all clocks, and to change every clock-guard to true. This implies that a process might halt in an arbitrary number of steps before a guard. But the property that a thread is monopolizing the behavior, is independent of the clocks, so the property can still be verified.

These tests work very well on the small example both with the possible deadlock and without. The proof is almost instantaneous, and the number of states remains small. We also checked these properties for the sub-set of a realworld mpeg decoding platform, which modeled the synchronization between the different components, with good results: All tests were performed on a Intel Celeron with 2.80GHz and 1GB RAM.

Checking Assertions

Checking assertions in the TL model is straightforward. Assertions are simply inserted at the corresponding transition, and directly written into the Spin code. So far, we are mainly using assertions to check that some part of the model is never executed. This could also be modeled using specific error states. Since assertions are always safety properties, they are not effected by possible abstractions.

Benchmarks

Our test model consists of a chain of modules. The first module triggers an interrupt in the next one. This interrupt notifies an event, allowing the module to trigger an interrupt in the next module, and so on. The last module contains an assertion, which is either always false (bug) or always true (no-bug). The latter forces Spin to compute the whole state space when checking for invalid assertions. The normal encoding uses the global variable M, to assure atomicity, while the goto version is our alternative encoding. In order to allow all intended behavior, we disabled partial oder reduction when checking the encoding with goto. The entry NT, for not tested, indicates that we had abort the checking for lack of memory. Both encoding find the bug very fast.

# modules

When computing the whole state space, we see that the encoding using gotos is more efficient, but the number of states increases exponentially for both encodings. This is due to the increase of white states. We can solve the bug by waiting before the notification, in order to make sure that no event is lost. While this makes the model completely deterministic, the number of states is still growing exponentially. Adding deterministic, local computations, increases the number of reachable states linear for the normal encoding, and not at all for the encoding with gotos.

Comments on Performance

There are two possible sources for state explosion, making the model too large for automatic verification: the clocks and the interleaving between the processes. Modeling time by integers is usually not a good idea. However, our clocks are always bounded by the time of the corresponding wait, which is usually a rather small value, and since the clocks are updated synchronously, the actual increase of the state space is moderate. The size of the state space depends on the maximum time a process waits for, and the number of unrelated wait statements in parallel processes.

One way to cope with the state explosion is to use Spin not for formal verification, but for intensive testing. This is encouraged by the fact, that in the benchmark the existing bugs were found very fast. This also allows to use more efficient algorithms in Spin, like hash-compact search, which only give approximate results.

On the other hand, our benchmark shows that introducing white states lead to state-explosion, while introducing black states has only a minor impact. Typical case-studies contain mostly control-flow, and only a few waits; therefore we are confident that we can model check programs of interesting size with our approach.

The problem of SystemC having no official formal semantics is not new. Most of the research work studying SystemC in a formal context starts giving it a semantics in another well-defined formalism.

A number of other approaches have been proposed for the description of heterogeneous hardware/software systems with an emphasis on formal analysis. See, for instance, Metropolis. In this type of approach, the (formal) definition of the description language is part of the game. Other works like SystemC FL [START_REF] Man | Formal communication semantics of systemC F L . In DSD[END_REF] define a new language from scratch, but claim its similarity with SystemC. As opposed to SystemC, SystemC FL doesn't have a non-preemptive scheduler, doesn't seem to manage a notion of "event" (which is the basic synchronization primitive on top of which everything else is built in SystemC),. . . Our approach is different. We want to deal with actual SystemC code, and the actual SystemC semantics.

An early work on SystemC semantics is [START_REF] Hoffmann | The simulation semantics of systemC[END_REF], where the semantics is expressed in terms of Abstract State Machines. It only models SystemC 1.0 which was the only available at that time, and has an inaccurate model of the scheduler: in their model, the processes are executed in parallel whereas the language reference manual explicitly says the opposite.

[17] does the same with another formalism (denotational semantics). It models only a very strict subset of SystemC, with explicit limitation both on the kind of processes and on the content of processes (only wait statements and assignments are modeled, without a notion of control-flow).

While those approaches are theoretically interesting, the fact that the target formalism is abstract limits the possible applications: one can reason "on paper" about denotational semantics and abstract state machines, but until these formalism get a concrete syntax and an associated toolkit, these reasonings will not be automatizable or verifiable automatically. Furthermore, the question of the faithfulness of the semantics is not solved: starting from a language without a formally-defined semantics, one can not do anything better than examining the proposed semantics and just "claim" its faithfulness.

The approach followed by CheckSyC [START_REF] Drechsler | CheckSyC: an efficient property checker for rtl SystemC designs[END_REF] goes one step further, providing a complete chain from the SystemC source code to a proof engine. They get relatively good experimental results. However, this work do not target the same SystemC subset as we do: we are not interested in RTL synthesizable programs, but target the transaction level model.

We already experimented with the connection of SystemC to a proof engine. The first output of this work was the tool-chain LusSy [START_REF] Moy | Techniques and Tools for the Verification of Systems-on-a-Chip at the Transaction Level[END_REF]. Starting from a Sys-temC program, we use a SystemC front-end to parse it, generate an intermediate representation called HPIOM made of communicating, synchronous automata. We can then generate Lustre or SMV code to connect to a variety of proof engines. The connection to Lustre provides both provability and executability. The work presented here differs on several points: the first one is that LusSy uses a SystemC-independent intermediate formalism, and models the details of the scheduler using an explicit automaton. As opposed to this, we are using here a representation with automata in which the notion of non-preemption is built-in. The details of the scheduler do not need to appear in a separate automaton, but are defined by the product. The second difference is that LusSy uses a synchronous formalism, while we are experimenting here with Spin, which is asynchronous.

[18] describes a general approach to extract a behavioral type from a system using the polychronous model of computation (using Signal [START_REF] Benveniste | Synchronous programming with events and relations: the Signal language and its semantics[END_REF] as a support language). This applies to languages and execution models such as Java, Sys-temC and SpecC. Their starting point is the GNU SSA (static single assignment) form, which is the intermediate representation in GCC, since version 4.0. The SSA form has the interesting property that each basic block in the abstract syntax tree can be executed in a single clock tick in Signal, leading to an elegant encoding of the SystemC code.

Further Work and Conclusion

We have presented a way of translating TL models written in SystemC into Promela. This is one way of giving a formal semantics to SystemC. We use this encoding to perform verification of TL models, like checking for deadlocks and assertions.

The asynchronous encoding seems to be worth further investigation, compared to a synchronous one. When translating SystemC to a synchronous framework, the atomicity between two white states is obtained by a quite complex synchronisation between the automata for the processes, and the automata that represents the scheduler. Conversely, when translating SystemC to Promela, the atomicity is built-in. Therefore, if the number of white states is small compared to the number of black states, the formal verification should be easier for the asynchronous encoding On the other hand, translating SystemC into Lustre or SMV has the advantage of producing a symbolic description of the system that can be exploited by symbolic model-checkers and abstract-interpretation tools.

The use of Spin is probably better for bug tracking, while the use of a symbolic tool is probably better for performing aggressive abstractions and approximate property verification.

Right now, the transformation from SystemC to Promela is manual. While interesting as a first approach to the problem, it would be necessary to implement the principles presented here in a complete tool-chain to apply the approach on a larger case study and compare it with the synchronous encoding. This would mean to reuse a front-end like Pinapa [START_REF] Moy | Pinapa: An extraction tool for systemc descriptions of systems-on-a-chip[END_REF], that we developed for LusSy, a transformation into a structure representing the particular form of automata used here, and a Spin code generator. We already have a prototype for the data structure and the code generator, but the biggest part of the work is the transformation from the actual SystemC code.

Fig. 1 .

 1 Fig. 1. A simple example of a TL model with two modules.

Fig. 2 .

 2 Fig. 2. Automata for Module 1

Fig. 3 .

 3 Fig. 3. Representation of non-preemption in Promela. The next value of M depends on the color of the next state.

  i v e p r o c t y p e update_clock (){ end : do :: atomic { timeout && M ==0 && X_used -> X = X + X_used ;} od } . . . a c t i v e p r o c t y p e A (){ do :: atomic { myturn && state ==1 -> X =0; X_used =1; M =0; state =2} :: atomic { myturn && state ==2 && X =10 -> X =0; X_used =0;. . .} . . .

Fig. 4 .

 4 Fig. 4. Representation of clocks, which are needed to wait for time, as an automaton and in Promela. The process update_clock lets time elapse synchronously for all processes.

Function calls

  For each function f , a global Boolean variable F is introduced. The effects of f are transformed into calling f : F := 1 returning from the call: {F == 0} begin of the declaration of f : {F == 1} end of the declaration: F := 0 This is illustrated by Figure 5.

Fig. 5 .

 5 Fig. 5. Representation of function calls in Promela. Assume that the caller has the identifier 1 and the function has identifier 2.

Fig. 6 .

 6 Fig. 6. Global definitions and the process for synchronous time elapse.

Fig. 7 .

 7 Fig. 7. Promela code for Module 1 with the function f

Fig. 8 .

 8 Fig. 8. Promela code for Module 2 with the function g

  without bug with bug mpeg [s] states [s] states [s] states deadlock < 0.1 35 < 0.1 9 < 0.1 126 no yielding < 0.1 49 < 0.1 55 < 0.1 209 time elapse < 0.1 57 < 0.1 9 < 0.1 226