Georgios Damaskinos
email: georgios.damaskinos@epfl.ch

Rachid Guerraoui
email: rachid.guerraoui@epfl.ch

Anne-Marie Kermarrec
email: anne-marie.kermarrec@epfl.ch

Vlad Nitu
email: vlad.nitu@insa-lyon.fr

Francois Taiani
email: francois.taiani@irisa.fr

FLeet: Online Federated Learning via Staleness Awareness and Performance Prediction

Keywords: CCS Concepts:, Computing methodologies → Machine learning, • Security and privacy, federated learning, online learning, asynchronous gradient descent, profiling, mobile Android devices

Federated Learning (FL) is very appealing for its privacy benefits: essentially, a global model is trained with updates computed on mobile devices while keeping the data of users local. Standard FL infrastructures are however designed to have no energy or performance impact on mobile devices, and are therefore not suitable for applications that require frequent (online) model updates, such as news recommenders.

This paper presents FLeet, the first Online FL system, acting as a middleware between the Android OS and the machine learning application. FLeet combines the privacy of Standard FL with the precision of online learning thanks to two core components: (i) I-Prof, a new lightweight profiler that predicts and controls the impact of learning tasks on mobile devices, and (ii) AdaSGD, a new adaptive learning algorithm that is resilient to delayed updates.

Our extensive evaluation shows that Online FL, as implemented by FLeet, can deliver a 2.3× quality boost compared to Standard FL, while only consuming 0.036% of the battery per day. I-Prof can accurately control the impact of learning tasks by improving the prediction accuracy up to 3.6× (computation time) and up to 19× (energy). AdaSGD outperforms alternative FL approaches by 18.4% in terms of convergence speed on heterogeneous data.

Introduction

The number of edge devices and the data produced by these devices have grown tremendously over the last 10 years. While in 2009, mobile phones only generated 0.7% of the worldwide data traffic, in 2018 this number exceeded 50% [START_REF]Percentage of all global web pages served to mobile phones from 2009 to 2018[END_REF]. This exponential growth is raising challenges both in terms of scalability and privacy. As the volume of data produced by mobile devices explodes, users expose increasingly detailed and sensitive information, which in turn becomes more costly to store, process, and protect. This dual challenge of privacy and scalability is pervasive in machine learning (ML) applications such as recommenders, image-recognition apps, and personal assistants. These ML-based application often operate on highly personal and possibly sensitive content, including conversations, geolocation, or physical traits (faces, fingerprints), and typically require tremendous volumes of data for training their underlying ML models. For example, people in the USA of age 18-24, type on average around 900 words per day (128 messages per day [START_REF]Average text messages per day[END_REF] with an average of 7 words per message [START_REF] Crushh | Average text message length[END_REF]). The Android next-word prediction service is trained on average with sequences of 4.1 words [START_REF] Hard | Federated learning for mobile keyboard prediction[END_REF] which means that each user generates around 220 training samples daily. With tens of millions or even billions of user devices [START_REF] Bonawitz | Towards Federated Learning at Scale: System Design[END_REF] scalability issues arise.

Federated Learning. To address this dual privacy and scalability challenge, large industrial players are now seeking to exploit the rising power of mobile devices to reduce the demand on their server infrastructures while, at the same time, protecting the privacy of their users. Federated Learning (FL) is a new computing paradigm (spearheaded among others by Google [START_REF] Chen | Federated Meta-Learning for Recommendation[END_REF][START_REF] Konečnỳ | Federated optimization: distributed machine learning for on-device intelligence[END_REF][START_REF] Smith | Federated multi-task learning[END_REF]) where a central server iteratively trains a global model (used by an ML-based application) without the need to centralize the data. The iterative training orchestrated by the server consists of the following synchronous steps for each update. Initially, the server selects the contributing mobile devices and sends them the latest version of the model. Each device then performs a learning task based on its local data and sends the result back to the server. The server aggregates a predefined number of results (typically a few hundreds [START_REF] Bonawitz | Towards Federated Learning at Scale: System Design[END_REF]) and finally updates the model. The server drops any results received after the update. FL is "privacy-ready" and can provide formal privacy guarantees by using standard techniques such as secure aggregation and differential privacy [START_REF] Bonawitz | Practical secure aggregation for privacy-preserving machine learning[END_REF].

The standard use of FL has so far been limited to a few lightweight and extremely privacy-sensitive services, such as next-word prediction [START_REF] Yang | Applied federated learning: Improving google keyboard query suggestions[END_REF], but its popularity is bound to grow. Privacy-related scandals continue to unfold [START_REF]NSA's PRISM[END_REF][START_REF]The Facebook and Cambridge Analytica scandal[END_REF], and new data protection regulations come into force [START_REF]California Consumer Privacy Act of 2018 (CCPA)[END_REF]76]. The popularity of FL is clearly visible in two of the most popular ML frameworks (namely TensorFlow and PyTorch) [START_REF]TensorFlow -Federated Learning[END_REF][START_REF] Ryffel | A generic framework for privacy preserving deep learning[END_REF], and also in the rise of startups such as S20.ai [START_REF][END_REF] or SNIPS (now part of Sonos) [START_REF] Snips | Snips -Using Voice to Make Technology Disappear[END_REF], which are betting on private decentralized learning.

Limitation of Standard FL. These are encouraging signs, but we argue in this paper that Standard FL [START_REF] Bonawitz | Towards Federated Learning at Scale: System Design[END_REF] is unfortunately not effective for a large segment of ML-based applications, mainly due to its constraint for high device availability: the selected mobile devices need to be idle, charging and connected to an unmetered network. This constraint removes any impact perceived by users, but also limits the availability of devices for learning tasks. Google observed lower prediction accuracy during the day as few devices fulfill this policy and these generally represent a skewed population [START_REF] Yang | Applied federated learning: Improving google keyboard query suggestions[END_REF]. With most devices available at night the model is generally updated every 24 hours. This constraint may be acceptable for some ML-based services but is problematic to what we call online learning systems, which underlie many popular applications such as news recommenders or interactive social networks (e.g., Facebook, Twitter, Linkedin). These systems involve large amounts of data with high temporality, that generally become obsolete in a matter of hours or even minutes [START_REF] Mishne | Fast data in the era of big data: Twitter's real-time related query suggestion architecture[END_REF]. To illustrate the limitation of Standard FL, consider two users, Alice and Bob, who belong to a population that trains the ML model underlying a news recommendation system (Figure 1). Bob wakes up earlier than Alice and clicks on some news articles. To deliver fresh and relevant recommendations, these clicks should be used to compute recommendations for Alice when she uses the app, slightly after Bob. In Standard FL (upper half Figure 1), the device of Bob would wait until much later (when idle, charging and connected to WiFi) to perform the learning task thus negating the value of the task results for Alice. In an online learning setup (lower half of Figure 1), the activity of Bob is rapidly incorporated into the model, thereby improving the experience of Alice. Challenges and contributions. In this paper we address the aforementioned limitation and enable Online FL. We introduce FLeet, the first FL system that specifically targets online learning, acting as a middleware between the operating system of the mobile device and the ML-based application. FLeet addresses two major problems that arise after forfeiting the high device availability constraint.

First, learning tasks may have an energy impact on mobile devices now powered on a battery. Given that learning tasks are generally compute intensive, they can quickly discharge the device battery and thereby degrade user experience. To this end, FLeet includes I-Prof ( §2.2), our new profiling tool which predicts and controls the computation time and the energy consumption of each learning task on mobile devices. The goal of I-Prof is not trivial given the high heterogeneity of the devices and the performance variability even for the same device over time [START_REF] Nishio | Client selection for federated learning with heterogeneous resources in mobile edge[END_REF] (as we show in §3).

Second, as mentioned above, synchronous training discards all late results arriving after the model is updated thus wasting the battery of the corresponding devices and their potentially useful data. Frequent model updates call for small synchronization windows that given the high performance variability, amplify this waste. We therefore replace the synchronous scheme of Standard FL with asynchronous updates. However, asynchronous updates introduce the challenge of staleness as multiple users are now free to perform learning tasks at arbitrary times. A stale result occurs when the learning task was computed on an outdated model version; meanwhile the global model has progressed to a new version. Stale results add noise to the training procedure, slow down or even prevent its convergence [START_REF] Jiang | Heterogeneityaware Distributed Parameter Servers[END_REF][START_REF] Zhang | Stalenessaware async-sgd for distributed deep learning[END_REF]. Therefore, FLeet includes AdaSGD ( §2.3), our new Stochastic Gradient Descent (SGD) algorithm that tolerates staleness by dampening the impact of outdated results. This dampening depends on (a) the past observed staleness values and (b) the similarity with past learning tasks. We fully implemented the server side and the Android client of FLeet 1 . We evaluate the potential of FLeet and show that it can increase the accuracy of a recommendation system (that employs Standard FL) by 2.3× on average, by performing the same number of updates but in a more timely (online) manner. Even though the learning tasks drain energy directly from the battery of the phone, they consume on average only 0.036% of the battery capacity of a modern smartphone per user per day. We also evaluate the components of FLeet on 40 commercial Android devices, by using popular benchmarks for image classification. Regarding I-Prof, we show that 90% of the learning tasks deviate from a fixed Service Level Objective (SLO) of 3 seconds by at most 0.75 seconds in comparison to 2.7 seconds for the competitor (the profiler of MAUI [START_REF] Cuervo | MAUI: making smartphones last longer with code offload[END_REF]). The energy deviation from an SLO of 0.075% battery drop is 0.01% for I-Prof and 0.19% for the competitor. We also show that our stalenessaware learning algorithm (AdaSGD) learns 18.4% faster than its competitor (DynSGD [START_REF] Jiang | Heterogeneityaware Distributed Parameter Servers[END_REF]) on heterogeneous data.

FLeet

FLeet incorporates two components we consider necessary in any system that has the ambition to provide both, the (a) privacy of FL and (b) the precision of online learning systems. The first component is I-Prof, a lightweight MLbased profiling mechanism that controls the computation time and energy of the learning task by using ML-based estimators. The second component of FLeet is AdaSGD, a new adaptive learning algorithm that tolerates stale updates by automatically adjusting their weight.

Architectural Overview

Similar to the implementation of Standard FL [START_REF] Bonawitz | Towards Federated Learning at Scale: System Design[END_REF], FLeet follows a client-server architecture (Figure 2) where each user hosts a worker and the service provider hosts the server (typically in the cloud). In FLeet, the worker is a library that can be used by any mobile ML-based application (e.g., a news articles application). The model training protocol of FLeet is the following (the numbers refer to Figure 2):

1 https://github.com/gdamaskinos/fleet [START_REF] Abadi | TensorFlow: A system for large-scale machine learning[END_REF] The worker requests a learning task and sends information regarding the labels of the local data along with information about the state of the mobile device. We introduce the purpose of this information in Steps 2 and 3.

(2) I-Prof employs the device information to bound the workload size (i.e., set a mini-batch size bound) that will be allocated to this worker such that the computation time and energy consumption approximate an SLO set by the service provider or negotiated with the user (details in §2.2). The mini-batch size is then set as the min(mini-batch size bound, local data size 2 ).

(3) AdaSGD computes a similarity for the requested learning task with past learning tasks in order to adapt to updates with new data (details in §2.3). ( 4) In order to prevent the computation of learning tasks with low or no utility for the learning procedure, the controller checks if both the mini-batch size and the similarity values pass certain thresholds set by the service provider. If the check fails, the request of the worker is rejected, otherwise the controller sends the model parameters and the mini-batch size to the worker and the learning task execution begins (details about setting these thresholds in §2.4).

(5) Based on the mini-batch size returned by the server, the worker samples from its locally collected data, performs the learning task (i.e., one or multiple local model updates) and sends the result (i.e., the gradient) back to the server. On the server side, AdaSGD updates the model after dynamically adapting this gradient based on its staleness and on its similarity value (details in §2.3). The above protocol maintains the key "privacy-readiness" of Standard FL: the user data never leave the device.

Workload Bound via Profiling

In Online FL, a mobile device should be able to compute model updates at any time, not only during the night, when the mobile device is idle, charging and connected to WiFi. Therefore, FLeet drops the constraint of Standard FL for high device availability. Hence, the learning task now drains energy directly from the battery of the device. Controlling the impact of a learning task on the user application in terms of energy consumption and computation time becomes crucial. To this end, FLeet incorporates a profiling mechanism that determines the workload size (i.e., the mini-batch size) appropriate for each mobile device.

Best-effort solution. To highlight the need for a specific profiling tool, we first consider a naive solution in which users process data points until they reach the SLO either in terms of computation time or energy. At this point, a worker sends back the resulting "best-effort" gradient. The service provider cannot decide beforehand whether for a given device, the cost (in terms of energy, time and bandwidth) to download the model, compute and upload the gradient is worth the benefit to the model. Updates computed on very small mini-batch sizes (by weak devices) will perturb the convergence of the overall model, and might even negate the benefit of other workers.

To illustrate this point, consider the experiment of Figure 3. The figure charts the result of training a Convolutional Neural Network on CIFAR10 [START_REF] Krizhevsky | Cifar dataset[END_REF] under different combinations of "strong" and "weak" workers. The strong workers compute on a mini-batch size of 128 while the weak workers compute on a mini-batch size of 1. We observe that even 2 weak workers are enough to cancel the benefit of distributed learning, i.e., the performance with 10 strong + 2 weak workers is the same as training with a single strong worker.

One way to avoid this issue could be to drop all the gradients computed on a mini-batch size lower than a given bound or weigh them with a tiny factor according to the size of their underlying mini-batch. This way would however waste the energy required to obtain these gradients. A profiler tool that can estimate the maximum mini-batch size (workload bound) that a worker can compute is necessary for the controller to decide whether to reject the computation request of this worker, before the gradient computation. Unfortunately, existing profiling approaches [START_REF] Carroll | An Analysis of Power Consumption in a Smartphone[END_REF][START_REF] Shaiful | A system-call based model of software energy consumption without hardware instrumentation[END_REF][START_REF] Chu | Balancing energy, latency and accuracy for mobile sensor data classification[END_REF][START_REF] Cuervo | MAUI: making smartphones last longer with code offload[END_REF][START_REF] Hao | Estimating mobile application energy consumption using program analysis[END_REF][START_REF] Kwon | Mantis: Automatic performance prediction for smartphone applications[END_REF][START_REF] Yoon | AppScope: Application Energy Metering Framework for Android Smartphone Using Kernel Activity Monitoring[END_REF] are not suitable because they are either relatively inaccurate (see §3.3) or they require privileged access (e.g., rooted Android devices) to low-level system performance counters. I-Prof. Mobile devices have a significantly lower level of parallelism in comparison with cloud servers. For example, the graphical accelerators of mobile devices generally have 10-20 cores [START_REF]Arm Mali Graphics Processing Units (GPUs[END_REF][START_REF]Adreno™ Graphics Processing Units[END_REF] while the GPUs on a server have thousands of cores [START_REF]CUDA GPUs | NVIDIA Developer[END_REF]. Given this low level of parallelism, even a relatively small mini-batch size can fill the processing pipelines. Hence, any additional workload will linearly increase the computation time and the energy consumption. Based on this observation, we built I-Prof, a lightweight profiler specifically designed for Online FL systems. We design I-Prof with three goals in mind: (a) operate effectively with data from a wide range of device types, (b) do so in a lightweight manner, i.e., introduce only a negligible latency to the learning task and (c) rely only on the data available on a stock (non-rooted) Android device. I-Prof employs an ML-based scheme to capture how the device features affect the computation time and energy consumption of the learning task. I-Prof predicts the largest mini-batch size a device can process while respecting both the time and the energy limits set by the SLO. To this aim, I-Prof uses two predictors, one for computation time and one for energy. Each predictor updates its state with data from the device information sent by the workers.

Designing such predictors is however tricky, as modern mobile phones exhibit a wide range of capabilities. For example, in a matrix multiplication benchmark, Galaxy S6 performs 7.11 Gflops whereas Galaxy S10 performs 51.4 Gflops [START_REF]Matrix multiplication benchmark[END_REF]. Figure 4 illustrates this heterogeneity on three different mobile devices by executing successive learning tasks of increasing mini-batch size ("up"). After reaching the maximum value, we let the devices cool down and execute subsequent learning tasks with decreasing mini-batch size ("down"). We present the results for the up-down part with the same color-pattern, except for Honor 10 in Figure 4(b) that we split for highlighting the difference. Figure 4 illustrates that the linear relation changes for each device and for certain devices (Honor 10, Galaxy S7) also changes with the temperature. Note that Honor 10 shows an increased variance at the end of the "up" part (Figure 4(b)) that is attributed to the high temperature of the device. The variance is significantly smaller for the "down" part.

In the following, we describe how I-Prof predicts the mini-batch size (n) given a computation time SLO3 (t S LO ). The computation time linearly increases with the workload size, i.e., t comp = α • n, where α depends on the device and its state. Considering the goal (i.e., t comp → t S LO ), the optimal mini-batch size is predicted as:

n = max 1, t S LO α (1)
I-Prof estimates the slope α from the device characteristics and operational conditions using a method that combines linear regression and online passive-aggressive learning [START_REF] Crammer | Online passive-aggressive algorithms[END_REF].

The input to this method is a set of device features based on measurements available through the Android API, namely available memory, total memory, temperature and sum of the maximum frequency over all the CPU cores. However, these features only encode the computing power of a device. For the prediction based on the energy SLO, I-Prof also needs a feature that encodes the energy efficiency of each device. We choose this additional feature as the energy consumption per non-idle CPU time 4 . We show in our evaluation ( §3.3) that these features achieve our three design goals. Given a vector of device features (x), and a vector of model parameters (θ prof ), the slope α is estimated as α = x T θ prof .

I-Prof uses a cold-start linear regression model for the first request of each user device. We pre-train the cold-start model using ordinary least squares with an offline dataset. This dataset consists of data collected by executing requests from a set of training devices with a mini-batch size increasing from 1 till a value such that the computation time reaches twice the SLO. I-Prof periodically re-trains the cold-start model after appending new data (device features). The training cost is negligible given the small number of features.

Furthermore, I-Prof creates a personalized model for every new device model (e.g., Galaxy S7) and employs it for every following request coming from this particular model. I-Prof bootstraps the new model with the first request (for which the cold-start model is used to estimate the computation time). For all the following learning tasks that result in pairs of (x (k) , α (k ) ), I-Prof incrementally updates a Passive-Aggressive (PA) model [START_REF] Crammer | Online passive-aggressive algorithms[END_REF] as:

θ (k +1) prof = θ (k) prof + f (k ) ∥x (k ) ∥ 2 v (k ) where v (k ) = siдn(α (k ) -x (k ) T θ (k )
prof )x (k) denotes the update direction, and f the loss function:

f (θ prof , x, α) = 0 if |x T θ prof -α | ≤ ϵ |x T θ prof -α | -ϵ otherwise.
(2) The parameter ϵ controls the sensitivity to prediction error and thereby the aggressiveness of the regression algorithm, i.e., the smaller the value of ϵ the larger the update for each new data instance (more aggressive).

I-Prof focuses solely on the time and energy spent during an SGD computation. Despite network costs (in particular when transferring models) having also an important impact, they fall outside the scope of this work as one can rely on prior work [START_REF] Altamimi | Energy cost models of smartphones for task offloading to the cloud[END_REF][START_REF] Liu | An empirical study of throughput prediction in mobile data networks[END_REF][START_REF] Qian | Profiling resource usage for mobile applications: a cross-layer approach[END_REF] to estimate the time and energy of network transfers within FLeet.

Adaptive Stochastic Gradient Descent

The server-driven synchronous training of Standard FL is not suitable for Online FL, as the latter requires frequent updates and needs to exploit contributions from all workers, including slow ones ( §1). Therefore, we introduce AdaSGD, 4 CPU time spent by processes executing in user or kernel mode. an asynchronous learning algorithm that is robust to stale updates. AdaSGD is responsible for aggregating the gradients sent by the workers and updating the application model (θ app ) 5 . Each update takes place after AdaSGD receives K gradients. The aggregation parameter K can be either fixed or based on a time window (e.g., update the model every 1 hour). The model update is:

θ (t +1) app = θ (t ) app -γ t K i=1 min 1, Λ(τ i ) • 1 sim(x i ) • G(θ (t i ) app , ξ i )
(3) where γ t is the learning rate, t ∈ N denotes the global logical clock (or step) of the model at the server (i.e., the number of past model updates) and t i ≤ t denotes the logical clock of the model that the worker receives. G(θ (t i ) app , ξ i ) is the gradient computed by the client w.r.t the model θ (t i ) app on the mini-batch ξ i drawn uniformly from the local dataset x i .

The workers send gradients asynchronously that can result in stale updates. The staleness of the gradient (τ i := tt i ) shows the number of model updates between the model pull and gradient push of worker i. One option is to directly apply this gradient, at the risk of slowing down or even completely preventing convergence [START_REF] Jiang | Heterogeneityaware Distributed Parameter Servers[END_REF][START_REF] Zhang | Stalenessaware async-sgd for distributed deep learning[END_REF]. The Standard FL algorithm (FedAvg [START_REF] Mcmahan | Communication-Efficient Learning of Deep Networks from Decentralized Data[END_REF]) simply drops stale gradients. However, even if computed on a stale model, the gradient may incorporate potentially valuable information. Moreover, in FLeet, the gradient computation may drain energy directly from the battery of the phone, thus making the result even more valuable. Therefore, AdaSGD utilizes even stale gradients without jeopardizing the learning process, by multiplying each gradient with an additional weight to the learning rate. This weight consists of (a) a dampening factor based on the staleness (Λ(τ i )) and (b) a boosting factor based on the user's data novelty ( 1 sim(x i ) ), that we describe in the following.

Staleness-based dampening. AdaSGD builds on prior work on staleness-aware learning that has shown promising results [START_REF] Jiang | Heterogeneityaware Distributed Parameter Servers[END_REF][START_REF] Zhang | Stalenessaware async-sgd for distributed deep learning[END_REF]. In order to accelerate learning, AdaSGD relies on a system parameter: the expected percentage of nonstragglers (denoted by s%). We highlight that this value is not a hyperparameter that needs tuning for each ML application but a system parameter that solely depends on the computing and networking characteristics of the workers, while it can be adapted dynamically [START_REF] Ouyang | Straggler detection in parallel computing systems through dynamic threshold calculation[END_REF][START_REF] Phan | A new framework for evaluating straggler detection mechanisms in mapreduce[END_REF]. We define the staleness-aware dampening factor Λ(τ ) = e -βτ , with β chosen s.t. = e -β τ thres 2 (i.e., the inverse dampening function [START_REF] Jiang | Heterogeneityaware Distributed Parameter Servers[END_REF] intersects with our exponential dampening function in τ thres 2 ), where τ thres is the s-th percentile of past staleness values. Figure 5 shows the dampening factor of AdaSGD compared to the inverse dampening function (employed by DynSGD [START_REF] Jiang | Heterogeneityaware Distributed Parameter Servers[END_REF]). Our hypothesis is that the perturbation to the learning process introduced by stale gradients, increases exponentially and not linearly with the staleness. We empirically verify the superior performance of our exponential dampening function compared to the inverse in §3.2.

As a quantile, τ thres is estimated from the staleness distribution. In practice, for the past staleness values to be representative of the actual distribution, an initial bootstrapping phase can employ the dampening factor of DynSGD. After this phase, the service provider can set s% and deploy AdaSGD. An underestimate of s% will slow down convergence, whereas an overestimate may lead to divergence. As we empirically observe ( §3.1), the staleness distribution often has a long tail. In such cases, the best choice of s% is the one that sets τ thres at the beginning of the tail.

Similarity-based boosting. In the presence of stragglers with large delays (comparing to the mean latency), staleness can grow and drive Λ(τ ) close to 0, i.e., almost neglect the gradients of these stragglers. Nevertheless, these gradients may contain valuable information. In particular, they may be computed on data that are not similar to the data used by past gradients. Hence, AdaSGD boosts these gradients by using the following similarity value:

sim(x i ) = BC(LD(x i ), LD дlobal ) (4)
where BC denotes the Bhattacharyya coefficient [START_REF]Bhattacharyya coefficient[END_REF], and LD the label distribution, that captures the importance of each gradient. We choose this coefficient given our constraints (sim(x i ) ∈ [0, 1]). For instance, given an application with 4 distinct labels and a local dataset (x i ) that has 1 example with label 0, and 2 examples with label 1: LD(x i ) = [ 1 3 , 2 3 , 0, 0]. The global label distribution (LD дlobal ) is computed on the aggregate number of previously used samples for each label. We highlight that LD is not specific to classification ML tasks; for regression tasks, LD would involve a histogram, with the length of the LD vector being equal to the number of bins instead of the number of classes.

The similarity value essentially captures how valuable the information of the gradient is. For instance, if a gradient is computed on examples of an unseen label (e.g., a very rare animal), then its similarity value is less than 1 (i.e., has information not similar to the current knowledge of the model). For the similarity computation, the server needs only the indices of the labels of the local datasets without any semantic information (e.g., label 3 corresponds to "dogs").

Implementation

The server of FLeet is implemented as a web application (deployed on an HTTP server) and the worker as an Android library. The server transfers data with the workers via Java streams by using Kryo [START_REF]Kryo[END_REF] and Gzip. In total, FLeet accounts 26913 Java LoC, 3247 C/C++ LoC and 1222 Python LoC.

Worker runtime. We design the worker of our middleware (FLeet) as a library and execute it only when the overlying ML application (Figure 2) is running in the foreground for two main reasons. First, since Android is a UI-interactive operating system, background applications have low priority so their access to system resources is heavily restricted and they are likely to be killed by the operating system to free resources for the foreground running app. Therefore, allowing the worker to run in the background would make its performance very unpredictable and thus impact the predictions of I-Prof. Second, running the worker in the foreground alleviates the impact of collocated (background) workload.

We build our main library for Convolutional Neural Networks in C++ on top of FLeet. We employ (i) the Java Native Interface (JNI) for the server, (ii) the Android NDK for the worker, (iii) an encoding scheme for transferring C++ objects through the java streams, and (iv) a thread-based parallelization scheme for the independent gradient computations of the worker. On recent mobile devices that support NEON [START_REF] Arm | SIMD ISAs | Neon[END_REF], FLeet accelerates the gradient computations by using SIMD instructions. We also port a popular deep learning library (DL4J [START_REF][END_REF]) to FLeet, to benefit from its rich ecosystem of ML algorithms. However, as DL4J is implemented in Java, we do not have full control over the resource allocation.

FLeet relies on the developer of the overlying ML application to ensure the performance isolation between the running application and the worker runtime. The worker can execute in a window of low user activity (e.g., while the user is reading an article) to minimize the impact of the overlying ML application on the predictive power of I-Prof.

Resource allocation. Allocating system resources is a very challenging task given the latency and energy constraints of mobile devices [START_REF] Ding | Generative and Multi-Phase Learning for Computer Systems Optimization[END_REF][START_REF] Mishra | CALOREE: Learning control for predictable latency and low energy[END_REF]. Our choice of employing only stock Android without root access means we can only control which cores execute the workload on the worker, with no access, for instance, to low-level advanced tuning. Given this limited control and the inherent mobile device heterogeneity, we opt for a simple yet effective scheme for allocating resources. This scheme schedules the execution only on the "big" cores for ARM big.LITTLE architectures and on all the cores otherwise. In the case of computationally intensive tasks (such as the learning tasks of FLeet), big cores are more energy efficient than LITTLE cores because they finish the computation much faster [START_REF] Greenhalgh | LITTLE Technology: The Future of Mobile[END_REF]. Regarding ARMv7 symmetric architectures with 2 and 4 cores that equip older mobile devices, the energy consumption per workload is constant regardless of the number of cores: a higher level of parallelism will consume more energy but the workload will execute faster. For this reason, our allocation policy relies on all the available cores so that we can take advantage of the embarrassingly parallel nature of the gradient computation tasks. For such tasks, we empirically show ( §3.4) that this scheme outperforms more complex alternatives [START_REF] Mishra | CALOREE: Learning control for predictable latency and low energy[END_REF].

Controller thresholds. In practice, the service provider can adopt various approaches to define the size and similarity thresholds of the controller (Figure 2). One option is A/B testing along with the gradual increase of the thresholds. In particular, the system initializes the thresholds to zero and divides the users into two groups. The first group tests the impact of the mini-batch size and the second the impact of the label similarity. Both groups gradually increase the thresholds until the impact on the service quality is considered acceptable. The server can execute this A/B testing procedure periodically, i.e., reset the thresholds after a time interval. We empirically evaluate the impact of these thresholds on prediction quality in §3.5.

Evaluation

Our evaluation consists of two main parts. First, in §3.1, we evaluate the claim that Online FL holds the potential to deliver better ML performance than Standard FL [START_REF] Bonawitz | Towards Federated Learning at Scale: System Design[END_REF] for applications that employ data with high temporality ( §1). Second, we evaluate in more detail the internal mechanisms of FLeet, namely AdaSGD ( §3.2), I-Prof ( §3.3), the resource allocation scheme ( §3.4) and the controller ( §3.5).

We deploy the server of FLeet on a machine with an Intel Xeon X3440 with four CPU cores, 16 GiB RAM and 1 Gb Ethernet, on Grid5000 [33]. The workers are deployed on a total of 40 different mobile phones that we either personally own or belong to the AWS Device Farm [7] (Oregon, USA). In §3.1, we deploy the worker on a Raspberry Pi 4 as our hashtag recommender is implemented on TensorFlow that does not yet support training on Android devices.

Online VS Standard Federated Learning

We compare Online with Standard FL on a Twitter hashtag recommender. Tweepy [START_REF] Tweepy | [END_REF] enables us to collect around 2.6 million tweets spanning across 13 successive days and located in the west coast of the USA. We preprocess these tweets (e.g., remove automatically generated tweets, remove special symbols) based on [START_REF] Dhingra | Tweet2vec: Character-based distributed representations for social media[END_REF]. We then divide the data into shards, each spanning 2 days, and divide each shard into chunks of 1 hour. We finally group the data into mini-batches based on the user id.

Our training and evaluation procedure follows an Online FL setup. Our model is a basic Recurrent Neural Network implemented on TensorFlow with 123,330 parameters [START_REF]Tensorflow text classification[END_REF], that predicts the 5 hashtags with the largest values on the output layer. The model training consists of successive gradientdescent operations, with each gradient derived from a single mini-batch (i.e., sent by a single user). Every day includes 24 mini-batches and thus 24 distinct gradient computations, while each model update uses 1 gradient. For the Online FL setup, the 24 daily updates are evenly distributed (one update every hour). Training uses the data of the previous hour and testing uses the data of the next hour. For the Standard FL setup, the 24 daily updates occur all at once (at the end of the day). Training uses the data of the previous day and testing uses the data of the next day. We highlight that under this setup, the two approaches employ the same number of gradient computations and the difference lies only in the time they perform the model updates. We also compare against a baseline model that always predicts the most popular hashtags [START_REF] Kowald | Temporal effects on hashtag reuse in twitter: A cognitive-inspired hashtag recommendation approach[END_REF][START_REF] Otsuka | Design and evaluation of a twitter hashtag recommendation system[END_REF]. We evaluate the model on the data of each chunk and reset the model at the end of each shard.

Quality boost. For assessing the quality of the hashtag recommender, we employ the F1-score @ top-5 [START_REF] Gong | Hashtag Recommendation Using Attention-Based Convolutional Neural Network[END_REF][START_REF] Kowald | Temporal effects on hashtag reuse in twitter: A cognitive-inspired hashtag recommendation approach[END_REF] to capture how many recommendations were used as hashtags (precision) and how many of the used hashtags were recommended (recall). In particular, for each tweet in the evaluation set, we compare the output of the recommender (top-5 hashtags) with the actual hashtags of the tweet, and derive the F1-score. Figure 6 shows that Online FL outperforms Standard FL in terms of F1-score, with an average boost of 2.3×. Online FL updates the model in a more timely manner, i.e., soon after the data generation time, and can thus better predict (higher F1-score) the new hashtags than Standard FL. The performance of the baseline model is quite low as the nature of the data is highly temporal [START_REF] Su Mon Kywe | On recommending hashtags in twitter networks[END_REF]. Energy impact. We measure the energy impact of the gradient computation on the Raspberry Pi worker. The Raspberry Pi has no screen; nevertheless recent trends in mobile/embedded processor design show that the processor is dominating the energy consumption, especially for compute intensive workloads such as the gradient computation [START_REF] Halpern | Mobile cpu's rise to power: Quantifying the impact of generational mobile cpu design trends on performance, energy, and user satisfaction[END_REF]. We measure the power consumption of every update of Online FL by executing the corresponding gradient computation 10 times and by taking the median energy consumption. We observe that the power depends on the batch size and increases from 1.9 Watts (idle) to 2.1 Watts (batch size of 1) and to 2.3 Watts (batch size of 100). The computation latency is 5.6 seconds for batch size of 1 and 8.4 for batch size of 100. Across all the updates of Online FL (that employ various batch sizes and result in the quality boost shown in Figure 6), we measure the average, median, 99 th percentile and maximum values of the daily energy consumption as 4, 3.3, 13.4 and 44 mWh respectively. Given that most modern smartphones have battery capacities over 11000 mWh, we argue that Online FL imposes a minor energy consumption overhead for boosting the prediction quality.

Staleness distribution. We study the staleness tion of the updates on our collected tweets, in order to set our experimental setup for evaluating AdaSGD ( §3.2). We assume that the round-trip latency per model update (gradient computation time plus network latency) follows an exponential distribution (as commonly done in the distributed learning literature [START_REF] Al | Gradient Delay Analysis in Asynchronous Distributed Optimization[END_REF][START_REF] Dutta | Shortdot: Computing large linear transforms distributedly using coded short dot products[END_REF][START_REF] Lee | Speeding up distributed machine learning using codes[END_REF][START_REF] Mitliagkas | Asynchrony begets momentum, with an application to deep learning[END_REF]). The network latency for downloading the model (123,330 parameters) and uploading the gradients is estimated to 1.1 second for 4G LTE and 3.8 seconds for 3G HSPA+ [START_REF]How fast is 4G?[END_REF]. We then estimate the average computation latency to be 6 seconds, based on our latency measurements on the Raspberry Pi. Therefore, we choose the exponential distribution with a minimum of 6 + 1.1 = 7.1 seconds and a mean of (6+1.1)+(6+3.8) 2 = 8.45 seconds. Given the exponential distribution for the round-trip latency and the timestamps of the tweets, we observe (in Figure 7) that the staleness follows a Gaussian distribution with a long tail (as assumed in [START_REF] Zhang | Stalenessaware async-sgd for distributed deep learning[END_REF]). The long tail is due the presence of certain peak times with hundreds of tweets per second.

Noteworthy, for applications such as our Twitter hashtag recommender where the user activity (and therefore the peruser data creation) is concentrated in time, the difference between Online and Standard FL in terms of communication overhead (due to the gradient-model exchange) is negligible. For applications where the per-user data creation is spread across the day, the communication overhead of Online FL grows, as each user communicates more often with the server.

AdaSGD Performance

We now dissect the performance of AdaSGD via an image classification application that involves Convolutional Neural Networks (CNNs). We choose this benchmark due to its popularity for the evaluation of SGD-based approaches [START_REF] Abadi | Deep learning with differential privacy[END_REF][START_REF] Trishul M Chilimbi | Project Adam: Building an Efficient and Scalable Deep Learning Training System[END_REF][START_REF] Kang | Neurosurgeon: Collaborative intelligence between the cloud and mobile edge[END_REF][START_REF] Mcmahan | Communication-Efficient Learning of Deep Networks from Decentralized Data[END_REF][START_REF] Zhang | Stalenessaware async-sgd for distributed deep learning[END_REF][START_REF] Zhao | Federated learning with non-iid data[END_REF]. We employ multiple scenarios involving various staleness distributions, data distributions, and a noise-based differentially private mechanism.

Image classification setup. We implement the models shown in Table 1 in FLeet6 to classify handwritten characters and colored images. We use three publicly available datasets: MNIST [START_REF] Lecun | MNIST dataset[END_REF], E-MNIST [START_REF] Cohen | EMNIST: an extension of MNIST to handwritten letters[END_REF] and CIFAR-100 [START_REF] Krizhevsky | Cifar dataset[END_REF]. MNIST consists of 70,000 examples of handwritten digits (10 classes) while E-MNIST consists of 814,255 examples of handwritten characters and digits (62 classes). CIFAR-100 consists of 60,000 colour images in 100 classes, with 600 images per class. We perform min-max scaling as a pre-processing step for the input features.

We split each dataset into training / test sets: 60,000 / 10,000 for MNIST, 697,932 / 116,323 for E-MNIST and 50,000 / 10,000 for CIFAR-100. Unless stated otherwise, we set the aggregation parameter K ( §2.3) to 1 (for maximum update frequency), the mini-batch size to 100 examples [START_REF] Behnam Neyshabur | Path-sgd: Path-normalized optimization in deep neural networks[END_REF], the ϵ (the Passive-Aggressive parameter) to 0.1 and the learning rate to 15 * 10 -4 for CIFAR-100, 8 * 10 -4 for E-MNIST, and 5 * 10 -4 for MNIST.

Since the training data present on mobile devices are typically collected by the users based on their local environment and usage, both the size and the distribution of the training data will typically heavily vary among users. Given the terminology of statistics, this means that the data are not Independent and Identically Distributed (non-IID). Following recent work on FL [START_REF] Wang | Adaptive federated learning in resource constrained edge computing systems[END_REF][START_REF] Wang | Beyond inferring class representatives: Userlevel privacy leakage from federated learning[END_REF][START_REF] Yurochkin | Bayesian Nonparametric Federated Learning of Neural Networks[END_REF][START_REF] Zhao | Federated learning with non-iid data[END_REF], we employ a non-IID version of MNIST. Based on the standard data decentralization scheme [START_REF] Mcmahan | Communication-Efficient Learning of Deep Networks from Decentralized Data[END_REF], we sort the data by the label, divide them into shards of size equal to 60000 2 * number of users , and assign 2 shards to each user. Therefore, each user will contain examples for only a few labels.

Staleness awareness setup. To be able to precisely compare AdaSGD with its competitors, we control the staleness of the updates produced by the workers of FLeet. Based on [START_REF] Zhang | Stalenessaware async-sgd for distributed deep learning[END_REF] and the shape of the staleness distribution shown in Figure 7, we employ Gaussian distributions for the staleness with two setups: D1 := N (µ = 6, σ = 2) and D2 := N (µ = 12, σ = 4), to measure the impact of increasing the staleness. We set the expected percentage of nonstragglers (s%) to 99.7%, i.e., τ thres = µ + 3σ . We evaluate the SGD algorithms on FLeet by using commercial Android devices from AWS. We evaluate the performance of AdaSGD against three learning algorithms: (i) DynSGD [START_REF] Jiang | Heterogeneityaware Distributed Parameter Servers[END_REF], a staleness-aware SGD algorithm employing an inverse dampening function (Λ(τ ) = 1 τ +1 ), that AdaSGD builds upon ( §2.3), (ii) the standard SGD algorithm with synchronous updates (SSGD) that represents the ideal (staleness-free) convergence behaviour, and (iii) FedAvg [START_REF] Mcmahan | Communication-Efficient Learning of Deep Networks from Decentralized Data[END_REF], the standard staleness-unaware SGD algorithm that is based on gradient averaging.

Staleness-based dampening. Figure 8 depicts that AdaSGD outperforms the alternative learning schemes for the non-IID version of MNIST. As expected, the stalenessfree scenario (SSGD) delivers the fastest (ideal) convergence, whereas the staleness-unaware FedAvg diverges. The comparison between the two staleness-aware algorithms (DynSGD and AdaSGD) shows that our solution (AdaSGD) better adapts the dampening factor to the noise introduced by stale gradients ( §2.3). AdaSGD reaches 80% accuracy 14.4% faster than DynSGD for D1 and 18.4% for D2. Figure 8 also depicts the impact of staleness on DynSGD and AdaSGD. We observe that the larger the staleness, the slower the convergence of both algorithms. The advantage of AdaSGD over DynSGD grows with the amount of staleness as the larger amount of noise gives more leeway to AdaSGD to benefit from its superior dampening scheme. Similarity-based boosting. We evaluate the effectiveness of the similarity-based boosting property of AdaSGD ( §2.3) in the case of long tail staleness (Figure 7). We employ the non-IID MNIST dataset, D1 (thus τ thres is 12) and set the staleness to 4 • τ thres = 48 for all the gradients computed on data with class 0. This setup essentially captures the case where a particular label is only present in stragglers. Figure 9(a) shows that AdaSGD incorporates the knowledge from class 0 much faster than DynSGD.

Figure 9(b) shows the CDF for the dampening values used to weight the gradients of Figure 9(a). We mark the two points of interest regarding the τ thres by vertical lines (as also shown in Figure 5). If AdaSGD had no similarity-based boosting, all updates related to class 0 would almost not be taken into account, as they would be nullified by the exponential dampening function, therefore leading to a model with poor predictions for this class. Given the low class similarity of the learning tasks involving class 0, AdaSGD boosts their dampening value. The second vertical line denotes the staleness value ( τ thres 2 = 6) for which AdaSGD and DynSGD give the same dampening value (0.14). The slope of each curve at this point indicates that the dampening values for DynSGD are more concentrated whereas the ones for AdaSGD are more spread around this value. IID data. Although data are more likely to be non-IID in an FL environment, the data collected on mobile devices might in some cases be IID. We thus benchmark AdaSGD under two additional datasets (E-MNIST and CIFAR-100) with the staleness following D2. Figure 10 shows that our observations from Figure 8 hold also with IID data. As with non-IID data, FedAvg diverges also in the IID setting, and AdaSGD performs better than DynSGD on both datasets.

Differential privacy. Differential privacy [START_REF] Dwork | The algorithmic foundations of differential privacy[END_REF] is a popular technique for privacy-preserving FL with formal guarantees [START_REF] Bonawitz | Practical secure aggregation for privacy-preserving machine learning[END_REF]. We thus compare AdaSGD against DynSGD in a differentially private setup by perturbing the gradients as in [START_REF] Abadi | Deep learning with differential privacy[END_REF]. We keep the previous setup (IID data with D2) and employ the MNIST dataset. Based on [START_REF] Wu | Bolt-on differential privacy for scalable stochastic gradient descent-based analytics[END_REF], we fix the probability δ = 1/N 2 = 1 with the moments accountant approach [START_REF] Abadi | Deep learning with differential privacy[END_REF] given the sampling ratio ( mini-batch size N = 100 60000 ), the noise amplitude, and the total number of iterations.

Figure 11 demonstrates that the advantage of AdaSGD over DynSGD also holds in the differentially private setup. A better privacy guarantee (i.e., smaller ϵ) slows down the convergence for both staleness-aware learning schemes.

I-Prof Performance

We compare I-Prof against the profiler of MAUI [START_REF] Cuervo | MAUI: making smartphones last longer with code offload[END_REF], a mobile device profiler aiming to identify the most energyconsuming parts of the code and offload them to the cloud. MAUI predicts the energy by using a linear regression model (similar to the global model of I-Prof) on the number of CPU cycles ( Ê = θ 0 • n), to essentially capture how the size of the workload affects the energy (as in [START_REF] Mittal | Empowering developers to estimate app energy consumption[END_REF]). We adapt the profiler of MAUI to our setup by replacing the CPU cycles with the mini-batch size for two main reasons. First, our workload has a static code path so the number of CPU cycles on a particular mobile device is directly proportional to the mini-batch size. Second, measuring the number of executed CPU cycles requires root access that is not available on AWS.

We bootstrap the global model of I-Prof and the model of MAUI by pre-training on a training dataset. To this end, we use 15 mobile devices in AWS (that are different from the ones used for the rest of the experiments), assign them learning tasks with increasing mini-batch size until the computation time becomes 2 times the SLO, and collect their device information for each task. We rely on the same methodology to evaluate energy consumption but use only 3 mobile devices in our lab, as AWS prohibits energy measurements.

For testing, we use a different set of 20 commercial mobile devices in AWS, each performing requests for the image classification application (on MNIST), starting at different timestamps (log-in events) as shown in Figure 12(a). In order to ensure a precise comparison with MAUI, we add a roundrobin dispatcher to the profiler component which alternates the requests from a given device between I-Prof and MAUI.

Computation time SLO. Figure 12(b) shows that I-Prof largely outperforms MAUI in terms of deviation from the computation time SLO. 90% of approximately 280 learning tasks deviate from an SLO of 3 seconds by at most 0.75 seconds with I-Prof and 2.7 seconds with MAUI. This is the direct outcome of our design decisions. First, I-Prof adds dynamic features (e.g., the temperature of the device) to train its global model ( §2.2). As a result, the predictions are more accurate for the first request of each user. Second, I-Prof uses a personalized model for each device that reduces the error (deviation from the SLO) with every subsequent request (Figure 12(c)). Figure 12(d) shows that the personalized models of I-Prof are able to output a wider range of mini-batch sizes that better match the capabilities of individual devices. On the contrary, MAUI relies on a simple linear regression model which has acceptable accuracy for its use-case but is inefficient when profiling heterogeneous mobile devices.

Energy SLO. To assess the ability of I-Prof to also target the energy SLO, we use the same setup as for the computation time, except on 5 mobile devices7 . We configure I-Prof with a significantly smaller error margin, ϵ = 6 * 10 -5 (Equation 2), because the linear relation (capture by α as defined in §2.2) is significantly smaller for the energy than for the computation time (as shown in Figure 4).

Figure 13 shows that I-Prof significantly outperforms MAUI in terms of deviation from the energy SLO. 90% of 36 learning tasks deviate from an SLO of 0.075% battery drop by at most 0.01% for I-Prof and 0.19% for MAUI. The observation that I-Prof is able to closely match the latency SLO, while MAUI suffers from huge deviations, holds for the energy too. The PA personalized models are able to quickly adapt to the state of the device as opposed to the linear model of MAUI that provides biased predictions.

Resource Allocation

We evaluate our resource allocation scheme ( §2.4) and compare it against CALOREE [START_REF] Mishra | CALOREE: Learning control for predictable latency and low energy[END_REF] which is a state of the art resource manager for mobile devices. The goal of CALOREE is to optimize resource allocation in order for the workload execution to meet its predefined deadline while minimizing the energy consumption. To this end, CALOREE profiles the target device by running the workload with different resource configurations (i.e., number of cores, core frequency). Since FLeet executes on non-rooted mobile devices, we can only adapt the number of big/little cores (but not their frequencies). By varying the number of cores allocated to our workload (i.e., gradient computation), we obtain the energy consumption of each possible configuration. From these configurations, CALOREE only selects those with the optimal energy consumption (the lower convex hull) which are packed in the so called performance hash table (PHT). CALOREE on new devices. In their thorough evaluation, the authors of CALOREE used the same device for training and running the workloads. Therefore, we first benchmark the performance of CALOREE when running on new devices. We employ Galaxy S7 to collect the PHT and set the minibatch size that I-Prof gives for a latency SLO of 3 seconds ( §3.3). We then run this workload with CALOREE on different mobile devices, as shown in Table 2.

The performance of CALOREE degrades significantly when running on a different device than the one used for training. The first line of Table 2 shows the baseline error when running on the same device. The error increases more than 6× for a device with similar architecture and the same vendor (Galaxy S8) and more than 32× for a device of similar architecture but different vendor (Honor 9 and 10). This significant increase for the error is due to the heterogeneity of the mobile devices which make PHTs not applicable across different device models. CALOREE vs FLeet. We evaluate the resource allocation scheme of FLeet by comparing it to the ideal environment for CALOREE, i.e., training and running on the same device (a setup nevertheless difficult to achieve in FL with millions of devices). Following the setup used for the energy SLO evaluation ( §3.3), we employ 5 devices and fix the size of the workload (mini-batch size) based on the output of I-Prof. In particular we set the mini-batch size to 280, 4320, 6720, 5280, 1200 for the devices shown in Figure 14 respectively. We set the deadline of CALOREE either equal or double than the computation latency of FLeet. We take 10 measurements and report on the median, 10th and 90th percentile.

Figure 14 shows the fact that in the ideal environment for CALOREE and even with double the time budget (giving more flexibility to CALOREE), FLeet has comparable energy consumption. Since gradient computation is a compute intensive task with high temporal and spacial cache locality, the configuration changes performed by CALOREE negatively impact the execution time and cancel any energy saved by its advanced resource allocation scheme. Additionally, the fewer configuration knobs available on non-rooted Android devices limit the full potential of CALOREE.

Learning Task Assignment Control

The controller of FLeet employs a threshold to prune learning tasks and thus control the trade-off between the cost of the gradient computations and the model prediction quality. This threshold can be based either on the mini-batch size or on the similarity values (Figure 2). To evaluate this trade-off, we employ non-IID MNIST with the mini-batch size following a Gaussian distribution N (µ = 100, σ = 33) (based on the distribution of the output of I-Prof shown in Figure 12(d)), and set the threshold to the nth percentile of the past values. Figure 15 illustrates that a threshold on the mini-batch size is more effective in pruning the less useful gradient computations than a threshold on the similarity. Figure 15(a) shows that even dropping up to 39.2% of the gradients (with the smallest mini-batch size) has a negligible impact on the accuracy (less than 2.2%). Figure 15(b) shows that one can drop 17% of the most similar gradients with an accuracy impact of 4.8%.

Related Work

Distributed ML. Adam [START_REF] Trishul M Chilimbi | Project Adam: Building an Efficient and Scalable Deep Learning Training System[END_REF] and TensorFlow [START_REF] Abadi | TensorFlow: A system for large-scale machine learning[END_REF] adopt the parameter server architecture [START_REF] Li | Scaling distributed machine learning with the parameter server[END_REF] for scaling out on high-end machines, and typically require cross-worker communication. FLeet also follows the parameter server architecture, by maintaining a global model on the server. However, FLeet avoids cross-worker communication, which is impractical for mobile workers due to the device churn.

A common approach for large-scale ML is to control the amount of staleness for boosting convergence [START_REF] Cui | Exploiting Bounded Staleness to Speed Up Big Data Analytics[END_REF][START_REF] Qiao | Litz: Elastic framework for high-performance distributed machine learning[END_REF]. In Online FL, staleness cannot be controlled as this would impact the model update frequency. The workers perform learning tasks asynchronously with end-to-end latencies that can differ significantly (due to device heterogeneity and network variability) or even become infinite (user disconnects).

Petuum [START_REF] Eric P Xing | Petuum: A New Platform for Distributed Machine Learning on Big Data[END_REF] and TensorFlow handle faults (worker crashes) by checkpointing and repartitioning the model across the workers whenever failures are detected. In a setting with mobile devices, such failures may appear very often, thus increasing the overhead for checkpointing and repartitioning. FLeet does not require any fault-tolerance mechanism for its workers, as from a global learning perspective, they can be viewed as stateless.

Federated learning. In order to minimize the impact on mobile devices, Standard FL algorithms [START_REF] Bonawitz | Towards Federated Learning at Scale: System Design[END_REF][START_REF] Jeong | Communication-Efficient On-Device Machine Learning: Federated Distillation and Augmentation under Non-IID Private Data[END_REF][START_REF] Mcmahan | Communication-Efficient Learning of Deep Networks from Decentralized Data[END_REF][START_REF] Smith | Federated multi-task learning[END_REF] require the learning task to be executed only when the devices are idle, plugged in, and on a free wireless connection. However, in §3.1, we have shown that these requirements may drastically impact the performance of some applications. Noteworthy, techniques for reducing the communication overhead [START_REF] Jeong | Communication-Efficient On-Device Machine Learning: Federated Distillation and Augmentation under Non-IID Private Data[END_REF] or increasing the robustness against adversarial users [START_REF] Damaskinos | Aggregathor: Byzantine machine learning via robust gradient aggregation[END_REF][START_REF] Damaskinos | Asynchronous Byzantine Machine Learning (the case of SGD)[END_REF], are orthogonal to the online characteristic so they can be adapted for AdaSGD, and plugged into FLeet.

Performance prediction for mobile devices. Estimating the computation time or energy consumption of an application running on a mobile device is a very broad area of research. Existing approaches [START_REF] Carroll | An Analysis of Power Consumption in a Smartphone[END_REF][START_REF] Shaiful | A system-call based model of software energy consumption without hardware instrumentation[END_REF][START_REF] Chu | Balancing energy, latency and accuracy for mobile sensor data classification[END_REF][START_REF] Hao | Estimating mobile application energy consumption using program analysis[END_REF][START_REF] Kwon | Mantis: Automatic performance prediction for smartphone applications[END_REF][START_REF] Yoon | AppScope: Application Energy Metering Framework for Android Smartphone Using Kernel Activity Monitoring[END_REF] target multiple applications generally executing on a single device. They typically benchmark the device or monitor hardware and OS-level counters that require root access. In contrast, FLeet targets a single application executing in the same way across a large range of devices. I-Prof poses a negligible overhead, as it employs features only from the standard Android API to enable Online FL, and requires no benchmarking of new devices. I-Prof is designed to make predictions for unknown devices.

Neurosurgeon [START_REF] Kang | Neurosurgeon: Collaborative intelligence between the cloud and mobile edge[END_REF] is a scheduler that minimizes the endto-end computation time of inference tasks (whereas FLeet focuses on training tasks), by choosing the optimal partition for a neural network and offloading computations to the cloud. The profiler of Neurosurgeon only uses workloadspecific features (e.g., number of filters or neurons) to estimate computation time and energy, and ignores devicespecific features. By contrast, mobile phones, as targeted by I-Prof8 , exhibit a wide range of device-specific characteristics that significantly impact their latency and energy consumption (Figure 4).

Systems such as CALOREE [START_REF] Mishra | CALOREE: Learning control for predictable latency and low energy[END_REF] and LEO [START_REF] Mishra | A probabilistic graphical model-based approach for minimizing energy under performance constraints[END_REF] profile mobile devices under different system configurations and train an ML model to determine the ones that minimize the energy consumption. They rely on a control loop to switch between these configurations such that the application does not miss the preset deadline. Due to the restrictions of the standard Android API, the available knobs are limited in our setup. For our application (i.e., gradient computation), we show that a simple resource allocation scheme ( §2.4) is preferable even in comparison with an ideal execution model.

Concluding Remarks

This paper presented FLeet, the first system that enables online ML at the edge. FLeet employs I-Prof, a new MLbased profiler which determines the ML workload that each device can perform within predefined energy and computation time SLOs. FLeet also makes use of AdaSGD, a new staleness-aware learning algorithm that is optimized for Online FL. We showed the performance of I-Prof and AdaSGD on commercial Android devices with popular benchmarks. I-Prof can be used for any iterative computation with embarrassingly-parallel CPU-bound tasks while AdaSGD is specific to gradient-descent and thus ML applications. In our performance evaluation we do not focus on network and scalability aspects that are orthogonal to our work and addressed in existing literature. We also highlight that transferring the label and device information (Figure 2) poses a negligible network overhead compared to transferring the relatively large FL learning models. Finally, addressing biases is an important problem even in cloud-based online ML (not only FL) that we also do not address in this work. For Online FL we arguably need to keep some of these biases (e.g., recommend more politics to people that wake up earlier). Of course diversity is also crucial.

Although we believe FLeet to represent a significant advance for online learning at the edge, there is still room for improvement. First, for the energy prediction, I-Prof requires access to the CPU usage that is considered as a security flaw on some Android builds and thus not exposed to all applications. In this case, I-Prof requires a set of additional permissions that belong to services from Android Runtime. Second, the transfer of the label distribution from the worker to the server introduces a potential privacy leakage. However, we highlight that the server has access only to the indices of the labels and not their values. In this paper, we focus on the protection of the input features and mention the possibility to deactivate the similarity-based boosting feature of AdaSGD in the case that this leakage is detrimental. We plan to investigate noise addition techniques for bounding this leakage [START_REF] Dwork | The algorithmic foundations of differential privacy[END_REF] in our future work. Finally, theoretically proving the convergence of AdaSGD is non-trivial due to the unbounded staleness and the non Independent and Identically Distributed (non-IID) datasets among the workers. In this respect, a dissimilarity assumption similar to [START_REF] Li | Federated optimization for heterogeneous networks[END_REF] may facilitate the derivation of the proof.

Figure 1 .

 1 Figure 1. Online FL enables frequent updates without requiring idle-charging-WiFi connected mobile devices.

Figure 2 .

 2 Figure 2. The architecture of FLeet.

Figure 3 .

 3 Figure 3. Motivation for lower bounding the mini-batch size. The noise introduced by weak workers (i.e., with small mini-batch sizes) may be detrimental to learning.

Figure 4 .

 4 Figure 4. The linear relation between the computation time and the mini-batch size depends on the specific device, and may even vary for the same device, depending on operation conditions such temperature.

Figure 5 .

 5 Figure 5. Gradient scaling schemes of SGD algorithms. AdaSGD, proposed in this paper, dampens stale gradients with an exponentially decreasing function (Λ(τ )) based on the expected percentage of non-stragglers (τ thres := s-th percentile of staleness values), and boosts the gradient of the straggler (τ = 48) due to its low similarity (sim(x i )).

1

 1

Figure 6 .

 6 Figure 6. Online FL boosts Twitter hashtag recommendations by an average of 2.3× comparing to Standard FL.

Figure 7 .

 7 Figure 7. Staleness distribution of collected tweets follows a Gaussian distribution (τ < 65) with a long tail (τ > 65).

Figure 8 .

 8 Figure 8. Impact of staleness on learning.

Figure 9 .

 9 Figure 9. Impact of long tail staleness on learning.

Figure 10 .

 10 Figure 10. Staleness awareness with IID data.

Figure 11 .

 11 Figure 11. Staleness awareness with differential privacy.

Figure 12 .Figure 13 .

 1213 Figure 12. I-Prof outperforms MAUI and drives the computation time closer to the SLO.

Figure 14 .

 14 Figure 14. Resource allocation of FLeet vs. CALOREE.

  Based on similarity

Figure 15 .

 15 Figure 15. Threshold-based pruning.

Table 1 .

 1 CNN parameters.

	Dataset	Parameters Input	Conv1 Pool1 Conv2 Pool2 FC1 FC2 FC3
	MNIST	Kernel size Strides	28×28×1	5×5×8 1×1	3×3 3×3	5×5×48 1×1	2×2 2×2	10 --
	E-MNIST	Kernel size Strides	28×28×1	5×5×10 1×1	2×2 2×2	5×5×10 1×1	2×2 2×2	15 62 -
	CIFAR-100	Kernel size Strides	32×32×3	3×3×16 1×1	3×3 2×2	3×3×64 1×1	4×4 4×4	384 192 100

Table 2 .

 2 Performance of CALOREE[START_REF] Mishra | CALOREE: Learning control for predictable latency and low energy[END_REF] on new devices.

	Running device Deadline error (%)
	Galaxy S7	1.4
	Galaxy S8	9
	Honor 9	46
	Honor 10	255

The prediction method given an energy SLO is the same.

Not to be confused with the model of the profiler (θ prof ).

We implement the CNN for E-MNIST on DL4J and the rest on our default CNN library.

AWS prohibits energy measurements so we only rely on devices available in our lab, listed in their log-in order: Honor 10, Galaxy S8, Galaxy S7, Galaxy S4 mini, Xperia E3.

In their in-depth experimental evaluation the authors of[START_REF] Kang | Neurosurgeon: Collaborative intelligence between the cloud and mobile edge[END_REF] consider a single hardware platform and not Android mobile devices.

Acknowledgments

We thank Dr. Sonia Ben-Mokhtar, our shepherd Prof. Christine Julien, our colleagues from the DCL laboratory at EPFL and the anonymous reviewers, for their helpful feedback. This work was supported by the EPFL-Inria International Lab and by the French ANR project PAMELA n. ANR-16-CE23-0016.


Laetitia Gibart

Gilles Bernot

Hélène Collavizza

Jean-Paul Comet

TotemBioNet Enrichment Methodology: Application to the Qualitative Regulatory Network of the Cell Metabolism

Keywords: Formal Methods, Regulatory Networks, R. Thomas' Modelling, Parameter Identification, Model Enrichment

When designing a biological regulatory network, new information or wet experiments can require adding variables or interactions, inside a previously validated model. They can result in complete reconsiderations of established behaviours. Fortunately, formal methods allow for fully automated verification of properties, and TotemBioNet is an efficient software integrating a collection of formal approaches for regulatory networks. It allowed us to develop a multidisciplinary methodology for designing large dynamical models in an incremental way, including non regression proofs (preservation of important biological properties).

INTRODUCTION

In the '70s, qualitative modelling of biological regulatory networks [START_REF] Thomas | Boolean formalization of genetic control circuits[END_REF][START_REF] Glass | Classification of biological networks by their qualitative dynamics[END_REF] has led to significant advances in the understanding of the main causalities of some observed cell behaviours. Models were handmade, and parameter identification mainly used simulations [START_REF] Gonzalez | GINsim: a software suite for the qualitative modelling, simulation and analysis of regulatory networks[END_REF]. In the early 2000s, formal methods automated the identification of parameters, managing as a whole the exhaustive sets of suited parameter settings [START_REF] Bernot | Application of formal methods to biological regulatory networks: extending Thomas' asynchronous logical approach with temporal logic[END_REF]. Software platforms handling formal methods [START_REF] Khalis | The SMBioNet method for discovering models of gene regulatory networks[END_REF][START_REF] Batt | Model checking genetic regulatory networks using GNA and CADP[END_REF][START_REF] Paulevé | Pint: A static analyzer for transient dynamics of qualitative networks with ipython interface[END_REF] have made it possible to design regulatory graphs, where numerous parameter values are compatible with the biological knowledge, where simulations are helpless, and where the slightest modification can have huge consequences [START_REF] Gebser | Repair and prediction (under inconsistency) in large biological networks with answer set programming[END_REF][START_REF] Khoodeeram | An Ockham razor model of energy metabolism[END_REF][START_REF] Naldi | The CoLoMoTo interactive notebook: accessible and reproducible computational analyses for qualitative biological networks[END_REF].

Enrichments of models do not preserve previously established properties [START_REF] Bernot | Behaviour preservation of a biological regulatory network when embedded into a larger network[END_REF][START_REF] Siebert | Deriving behavior of boolean bioregulatory networks from subnetwork dynamics[END_REF][START_REF] Mabrouki | Embedding of biological regulatory networks and property preservation[END_REF]. Nonetheless, in practice, the only way to design big regulatory models is to enrich previously validated models. So, we are moving into an era where intensive verifications of formal properties play the role that simulations played for handmade models: Model revision becomes the current practice [START_REF] Gouveia | Model Revision of Logical Regulatory Networks Using Logic-Based Tools[END_REF]. We describe here a methodology to efficiently design large validated models by successive small enrichments of previously validated ones. It uses TotemBioNet, a software that offers opti-mized management of the exhaustive set of parameter values compatible with biological knowledge [START_REF] Boyenval | What is a cell cycle checkpoint? the Totem-BioNet answer[END_REF]. Here, we describe our methodology and we give a (very small but representative) example of enrichment.It starts from one of the largest regulatory network model using the multivalued Thomas framework [START_REF] Snoussi | Qualitative dynamics of piecewiselinear differential equations: a discrete mapping approach[END_REF], namely the generic regulation of the cell metabolism [START_REF] Khoodeeram | An Ockham razor model of energy metabolism[END_REF]. It abstracts the relationships between the main actors of the metabolism in such a way that, for example, the Crabtree/Warburg effects can be studied, and their main causalities understood. The model considers biomass as a whole, without distinguishing between nucleic acids, proteins or lipids. Here, we simply show how to distinguish between lipidic and non lipidic biomass, so that the enrichment example is small enough to focus on the TotemBioNet method rather than describing detailed biological regulations.

Section 2 reminds the Thomas approach and the formal methods implemented in TotemBioNet. Section 3 presents our methodology, including the role of different kinds of behaviour "property matrices" that greatly aid decision making for model design. Section 4 shows the illustrating example.

TotemBioNet RATIONALS

TotemBioNet assists the design of R. Thomas' qualitative regulatory network models. It handles all the possible parameterizations, which is the key point of the modelling process.

Thomas' Modelling Framework

A regulatory network is a labelled directed graph in which vertices are variables (represented by circles) or multiplexes (rectangles). Variables abstract biological entities (gene products, biological functions or metabolic pathways) and multiplexes contain formulas that encode situations where a group of variables (inputs of multiplexes) influence the evolution of some variables (outputs of multiplexes), the simplest multiplexes being the formations of complexes (the formula contains a simple conjunction). In Fig. 1 the multiplex PBM abstracts the biomass production, it targets variables BM (BioMass) and ATP. It is activated when at least one of the multiplexes AAS, LS or PPP is activated. Among others, AAS abstracts the amino acid synthesis process. It summarizes the elements necessary for the de novo production of amino acids [START_REF] Berg | A genetically modified Hoare logic[END_REF]: nitrogen and carbon donors (DNC 2), a large amount of NADH (NADH 2) and ATP (AT P 1) (necessary for these anabolic processes). This can be expressed by the following formula: (DNC 2)&(AT P 1)&(NADH 2). Each variable has a domain of variation made of a small number of discrete levels and the dynamics of the model is deduced from the regulatory network and a set of kinetic parameters K ... (simply "parameters" in the sequel). Formally, the presence of an activator or the absence of an inhibitor of a variable x is called a resource, and the exhaustive list ω of its resources defines the discrete level towards which x is temporarily attracted, denoted K x,ω . If x has p possible resources then it has 2 p parameters. Lastly, when the set of effective resources of a variable increases, this cannot lead to decreasing its level [START_REF] Snoussi | Qualitative dynamics of piecewiselinear differential equations: a discrete mapping approach[END_REF]: ω ⊂ ω ⇒ K x,ω K x,ω , which can be used to reduce the number of parametrisations to consider.

Selection Technics

TotemBioNet inherits from SMBioNet [START_REF] Bernot | Application of formal methods to biological regulatory networks: extending Thomas' asynchronous logical approach with temporal logic[END_REF] and combines two filtering approaches to identify the exhaustive set of models consistent with biological knowledge: "genetically modified Hoare logic" and temporal logic.

Hoare Logic. Biological experiments prove that a set of traces must exist in the model. The genetically modified Hoare logic [START_REF] Berg | A genetically modified Hoare logic[END_REF][START_REF] Folschette | The Hoare-fol Tool[END_REF] produces the constraint on parameters that characterizes the models in which these traces exist. We firstly transcript the observed experimental traces into a so-called Hoare triple (observed pre-condition, path and post-condition) and Hoare logic constructs the weakest pre-condition that must be fulfilled. This constraint throws away parameter values which do not enable the observed traces.

Temporal Logic. Most of biological knowledge do not translate directly into Hoare logic, such as epigenetic phenomena, homeostasis, (non-)reachability of certain states, some events that always happen after others (but not necessarily right after), etc. To formalize this general knowledge, it is preferable to use temporal logic. [START_REF] Bernot | Application of formal methods to biological regulatory networks: extending Thomas' asynchronous logical approach with temporal logic[END_REF][START_REF] Goldfeder | BRE:IN -A Backend for Reasoning About Interaction Networks with Temporal Logic[END_REF] and several other authors have chosen CTL due to the efficiency of its model checking algorithm, and its ability to capture the non-deterministic choices of Thomas' theory.

Mixing Both Approaches. TotemBioNet inputs are: an influence graph, any knowledge on the parameter values, and properties on the dynamics of the system expressed using CTL or Hoare logic. It first computes the weakest pre-condition (wp) using genetically modified Hoare logic. Then, it efficiently enumerates all parametrisations satisfying wp, and generates input files for the model checker NuSMV [START_REF] Cimatti | NuSMV 2: An opensource tool for symbolic model checking[END_REF]. Each file contains the conjunction of CTL formulas and an automaton that encodes the model for the considered parametrisation.

TotemBioNet 1 , comes with many examples, including those of the present paper. It allows one to describe the influence graph with yEd graph editor 2 . A typical session consists in building the influence graph using yEd, in automatically generating the associated input file and then adding temporal properties and Hoare triples. TotemBioNet generates all parametrisations, labelled with "OK" when the dynamic properties are verified, and if not with all the properties which are not satisfied (see Fig.

G ≥ 1 ¬(PC≥1 ∧ ¬(L≥1)) yes M i no simple contraints
contraints wp

(M i |= Φ) M i |= wp
Figure 2: TotemBioNet processing flow [START_REF] Boyenval | What is a cell cycle checkpoint? the Totem-BioNet answer[END_REF].

3 TotemBioNet ENRICHMENT FRAMEWORK

Modelling Context

We proceed by successive small enrichments of the model under design. At each step, we start from a regulatory network model together with a set of parameter settings (non empty but of reasonable size) that is considered relevant w.r.t. biological knowledge and expertise. For the new enrichment, it is essential to keep track of the fundamental properties of the previously designed network models and to guarantee that they are preserved (possibly reformulated or enriched). Our TotemBioNet enrichment framework relies on a Modelling context, formed by: IG: An Influence Graph that describes the influence of each variable and multiplex in the system, BK: Some Biological Knowledge on the dynamics of the system, collected from biologists and literature, and given in natural language, PM: A Property Matrix that formalizes, (CTL or Hoare logic) the dynamics under different conditions. These formalisations are a translation of BK, PS: A set of Parameter Settings that govern system's dynamics. Some of them may be identified from BK by the modeller, others are automatically selected by TotemBioNet to satisfy PM formulas.

The couple (BK,PM) is the cornerstone for the reliability of the enrichment process: all along this process, PM is updated according to BK, and formal verification methods are applied to PM.

Property Matrices

Each column of a Property Matrix (Fig. 3-top) is a variable 3 whose behaviours are described in the column. Each row is an experimental condition and a box in the matrix can be filled by a conjunction of CTL formulas and Hoare triples that formalizes BK. The experimental conditions are fixed via a set of environment variables which are sources of regulations but never target of a regulation. Their constant values can differ from one experimental condition to another.

Along our enrichment workflow, Property Matrices (PM) have two different usages, validation or prediction, as detailed below:

(1)Validation Property Matrices (Fig. 3-middle) are PM where the biologist has certainty on the properties, via literature or wet experiments, and the modeller is confident in the translation into logical formulas. When an enrichment is done, all the properties of the enriched version of a Validation PM must be satisfied. By analogy with software engineering, a Validation PM can be seen as a set of non regression tests, (2)Prediction Property Matrices (Fig. 3-bottom) focus on fixed parameter settings. They are PM whose properties have been automatically generated and validated with TotemBioNet from simple property patterns such as oscillations, homeostasis, attraction basins and so on. There are as many prediction property matrices as parameter settings: a subset of selected prediction property matrices can then become the starting point of a new enrichment process.

Fig. 3 shows a schematic vision of the usage of PMs along an enrichment of a model, where some variables have been added/removed. A Validation PM may be sparse, as the set of established biological properties is generally small. At the opposite, a Prediction PM is entirely filled, but some of the discovered properties can be of little relevance. This is why the multidisciplinary dialogue is crucial and the increments of BK are often suggested by the prediction PMs, possibly asking for new biological experiments.

Enrichment Workflow

Initial Model. The TotemBioNet enrichment workflow starts with an initial modelling context (top of Fig. 4). It contains a Validation PM that will be enriched. The challenge is to design an enriched modelling context that ensures non regression w.r.t. the initial validation matrix.

Enrichment Design. The design of an enriched modelling context lies on a dialogue between the biologist and the modeller (Fig. 4-middle). The biologist describes the Enriched Biological Knowledge (EBK) and the modeller propagates it by enriching the Influence Graph (IG) or the Property Matrix (PM) (they become EIG and EPM). A modification of IG may induce a modification of the validation matrix, for example by changing the level of an homeostasis. It may also induce new parameters, thus TotemBioNet is run to identify the unknown parameters that validate EPM. If there is no such parameters, the modelling is inconsistent and has to be corrected. If there are too many parameter settings, the modelling is not precise enough to be a good candidate for predicting new relevant biological properties (Occam's razor). Thus the process goes back to a dialogue for refining the model. When a reasonably small number of parameter settings validate EPM, the biologist takes the final decision: return to improve the models and design a better enrichment, or continue the workflow.

Test and Validation of an Enriched Modelling

Context. When a set of parameter settings has been selected as the best compromise, tests and validations begin (Fig. 4-bottom). An instanciated modelling context is then built for each parameter setting. The dynamic behaviours controlled by these settings ensure a non regression of the initial modelling, but they may also exhibit some behavioural properties that differ from one model to another. Thus the matrix com-pletion functionality of TotemBioNet is called on each instantiated model. TotemBioNet establishes a set of properties on each variable in each context4 , which are added to the matrix, as predictions. Lastly, the biologist and the modeller select the most interesting contexts according to phenotypes, possibly with the help of new biological experiments. This set of contexts is the starting point of another enrichment.

ILLUSTRATING EXAMPLE

This section illustrates the enrichment steps of Fig 4 .  The cell metabolism can be viewed as an energy balance where all metabolic pathways (linked series of chemical reactions) are regulated according to nutrient cell intake. They can be anabolic (producing biomass compounds) and catabolic (that degrade large compounds to produce energy). The anabolic and catabolic balance is fine-tuned in the cell.

Within this context, an abstract and qualitative model of the metabolism regulation was developed [START_REF] Khoodeeram | An Ockham razor model of energy metabolism[END_REF] to understand how activity level of biological pathways in combination with nutrient can influence Warburg/Crabtree effect. This effect appears in all cell types from yeast to human: It leads the cells to go from one catabolic process (respiration) to another (fermentation). Since 2017, in order to focus on cancer in human cells in correlation with the cell cycle, we made several enrichments of the model to better reflect key metabolic pathways (glycolysis, oxidative respiration, Krebs cycle), nutrient (oxygen or glucose), key molecular components (biomass) and regulators (key-cofactors).

The following subsections correspond respectively to the top, middle and bottom parts of Fig. 4.

Initial Model and its Limits

The enrichment starts from the model whose IG is given in Fig. 5: biomass was represented by a unique variable BM that covered all cell growth components (lipids, nucleic acids for genetic material and amino acids for proteins). Fig. 1 is an extract from Fig. 5 that focuses on BM: the multiplexes PPP, AAS and LS abstract anabolic pathways respectively producing nucleic acids, amino acids and lipids [START_REF] Axelrod | Chapter 3 -glycolysis[END_REF][START_REF] Berg | A genetically modified Hoare logic[END_REF][START_REF] Stein | Lipid synthesis, intracellular transport, storage, and secretion[END_REF]. If one of them is activated, biomass production (PBM) is on: PBM is the inclusive disjunction of PPP and AAS and

LS (AAS|PPP|LS).

When PBM is a resource of BM, biomass will become present in the cell5 .

Table 1: Subpart of the Initial validation matrix. "0" means tend toward 0, "Osc" means oscillations with arbitrary boundaries and "!" stands for the negation.

Initial validation matrix

Environment Behaviour OXYG GLC IN AA ATP BM FERM KREBS PHOX 0 0 0 0 0 0 0 0 0 1 0 Osc !0 0 1 1 1 Osc !0 0 Osc Osc 1 2 2 Osc !0 !0 Osc
Table 1 is a subpart of the validation matrix of this initial model. The column BM, for example, requires obvious properties, e.g. absence of biomass if the cell does not receive any nutrient, and so on. BM participates in Box, which abstracts the βoxidation pathway, referring to the catabolic process of lipids [START_REF] Wakil | Chapter I -fatty acid metabolism[END_REF]. Unfortunately, this IG implies that β-oxidation could be activated without any lipids input. Indeed Box is satisfied when BM is activated by PPP (nucleic acids) or AAS (amino acids) through PBM: this behaviour proves that considering biomass as a whole is a too coarse abstraction for an adaptation to human cells. So, separating lipid biomass from the other compounds is our next enrichment.

Enriched Modelling Context Design

EBK: Enriched Biological Knowledge. It lists all biological information needed to separate lipids from the rest of the biomass: lipids are produced by synthesis and degraded by β-oxidation. Amino acids synthesis produces proteins, and PPP (Pentose Phosphate Pathway) produces nucleic acids for genetic material.

Figure 5: Influence graph (IG) of the initial modelling context: variables in red are the main metabolic processes (glycolysis, Krebs cycle, oxydative phosphorylation), yellow ones are the main cofactors (ATP/ADP and NADH/NAD+ ratios, oxygen, amino acid donors), biomass is in blue, environment variables are white (oxygen intake, glucose, nutrients...) and rectangle multiplexes formalize their interactions. For more details see [START_REF] Khoodeeram | An Ockham razor model of energy metabolism[END_REF] who defined the first IG of the cell metabolism regulation and its whole parameter setting.

Each kind of biomass production needs ATP for energy. All of this is added to initial BK to obtain EBK.

EIG: Enriched Influence Graph. Accordingly, we modify Fig. 1 into Fig. 6. It focuses on what has been modified: the biomass variable and its surrounding multiplexes. In the EIG (Fig. 6) BM has been split into BL (lipids biomass) and BnL (non lipidic compounds). BL participates in Box and is regulated by LS. BnL resources are PPP and AAS. In the multiplex Box the variable BM is replaced by the variable BL, which solves the problem mentioned in Subsection 4.1. Lastly, both BL and BnL productions consume ATP, thus regulate it negatively.

EPS: Enriched Parameter Settings. Our EIG leads to new parameters that need to be identified. BL and BnL have two resources each, so there are (2 2 + 2 2 = 8) new parameters (see Section 2.1). Moreover ATP gains one resource (5 resources in the EIG in- stead of 4 in IG). It increases the number of ATP parameters to 2 5 = 32. Among them, 16 are ineffective due to unsatisfiability of some resource combinations, and the 6 identified parameters which do not involve new resources are kept. Finally, it remains 18 parame-ters to identify for ATP. Thus, we have 26 parameters to identify. Thought experiments can be useful. For instance, to identify the parameter K BnL,∅ , we assume that both pentose phosphate pathway (PPP) and amino acids synthesis (AAS) are inactive (the set of Bnl resources is ∅). We try to foresee toward which value would BnL go if these conditions persist: neither genetic material nor proteins are produced, thus K BnL,∅ = 0. Most of the time EBK is not sufficient to allow the parameter identifications (many thought experiments are inconclusive). In such cases TotemBioNet will test all possible parameter settings. All in all 5 out of the 26 parameters were not identified.

EPM: Validation Enriched Properties Matrix. It summarizes the dynamical behaviours of variables, according to EBK. The only modifications affect BM (Table 2). It is replaced by both columns BnL and BL and they are filled from EBK: For example without any intake of glucose, no compounds are synthesized so BnL and BL tend towards 0.

0 0 0 0 0 0 0 0 0 1 0 Osc !0 0 1 1 1 Osc !0 !0 0 Osc Osc 1 2 2 Osc !0 !0 !0 Osc

TotemBioNet Test and Validation

We test with TotemBioNet the enriched modelling context created above, taking into consideration EBK, EIG, EPS, EPM. The 5 unidentified parameters from EPS give rise to only 15 instantiated modelling contexts (where each parameter has a unique value). We obtain 15 prediction matrices such as Table 3 where all empty boxes of validation-EPM are automatically completed using TotemBioNet. They allow modellers and biologists to eliminate parameter settings which exhibit non credible behaviours.

Table 3: Sub part of one of the 15 prediction EPMs."Osc(0-1)" means oscillations between level 0 and 1 of the variable.

Enriched Prediction matrix

Environment Behaviour OXYG GLC IN AA ATP BnL BL FERM KREBS PHOX 0 0 0 0 0 0 0 0 0 0 1 0 Osc(0-2) Osc(0-1) 0 Osc(0-1) 0 0 1 1 1 Osc(0-2) Osc(0-1) Osc(0-1) 0 Osc(0-1) Osc(0-1) 1 2 2
Osc(0-2) Osc(0-1) Osc(0-1) Osc(0-1) Osc(0-2) Osc(0-1)

For our example, the 15 prediction EPMs exhibit interestingly different behaviour for the variables BL and BnL. Here, none of the models have aberrant predictions, so we keep this enriched modelling context for the next enrichment step. Nevertheless, in general some of these different behaviours can contradict established biological knowledge or suggest new biological experiments.

CONCLUSION

We defined an incremental methodology for developing large formal models of biological regulatory networks. Starting from an initial formal model, the enrichment is first described in natural language EBK, then the formalisation of this information leads to the EIG, EPS and validation EPM. Our process involves, at each round of this methodology, a manageable number of parameter settings.

In practice, we observe that after a few enrichment steps, the ab initio design of the enriched model, without using the proposed methodology, would be impossible. The example outlined in this article (that contains notably more than 100 parameters) would lead to a number of parametrizations (1.45 × 10 60 ) that is so huge that TotemBioNet or any similar platform would have taken more that 4.6 × 10 50 years of computation to model check them, at the rate of 100 proofs per second! One of the key points of our incremental methodology consists in limiting, at each enrichment step, the number of parameter settings to enumerate, preserving a maximum number of known parameters from the previously validated model. EPS and validation EPM in an enriched modelling context allow TotemBioNet to drastically reduce the number of total parameters to identify, with a negligible computation time: The parameters for which the resources do not change (according to the new interpretation) remain at the same value, and the new ones can partly be identified by thought experiments.

Moreover, following our methodology, getting too many parameter settings for an enriched modelling context, simply means that the enrichment step is too ambitious to be manageable. In such a case we reassess the informal enrichment EBK to address a less ambitious enrichment. Conversely, when no coherent parameter setting is obtained, this is generally due to a construction error in the enriched modelling context which has also to be reassessed. In our methodology, this loop of reassessment is made possible owing to the remarkably efficient TotemBioNet platform.

We currently use this methodology for the metabolism regulation in cancer cells, when cells acquire new functioning during the Epithelialmesenchymal transition. In practice, the informal BK plays a crucial role for assisting interactions between biologists and modellers, not only in the design of the enrichment but also, in order to keep track of interpretations made in previous contexts. Last but not least, at each step the choice of a sensible subset of parameter settings often suggest new biological experiments that are particularly revealing.

Figure 1 :

 1 Figure 1: A part of influence graph: representation of variables and multiplexes (focus on BM in Figure 5).

Figure 3 :

 3 Figure 3: Schematic vision of Property Matrices (PM). Top: initial validation PM. Middle: enriched validation PM where var-3 has been divided into var-3A and var-3B leading to the generation of purple properties prop-3A-1 and prop-3B-1 from the initial property prop-3-1. Bottom: prediction PM where yellow properties have been automatically generated.

Figure 4 :

 4 Figure 4: TotemBioNet Enrichment Framework. The quadruplet of a modelling context is represented by a box containing: a yellow trapeze (IG), a blue bubble (BK), a grey rectangle (PM) and a green parallelogram (PS). The prefix E means an Enrichment of one part of the quadruplet.

Figure 6 :

 6 Figure 6: Enrichment of the influence graph of Fig. 1: BM has been split into Bnl and BL.

Table 2 :

 2 Subpart of the validation EPM.

		Enriched validation matrix
	Environment	Behaviour
	OXYG GLC IN AA ATP BnL BL FERM KREBS PHOX
	0

Currently, only oscillations, homeostasis, and stable states are implemented in prediction property matrices but enriching this range of properties is not difficult.

Because the applicable parameter is K BM,PBM = 1 in the current parameter setting

ACKNOWLEDGEMENTS

We are fully indebted to Sophie Vasseur and Fabienne Marchai-Guillaumond from INSERM CRCM, for fruitful collaborations which helped us to design the methodology. We warmly thank Jean-Yves Trosset and Rajeev Khoodeeram without whom the initial model of metabolism regulation would not exist.

//gitlab.com/totembionet/totembionet 2 https://www.yworks.