Marion Guthmuller

Gabriel Corona

Martin Quinson

System-level State Equality Detection for the Formal Dynamic Verification of Legacy Distributed Applications

The ever increasing complexity of distributed systems mandates to formally verify their design and implementation. Unfortunately, the common approaches and existing tools to formally establish the correctness of these systems remain hardly applicable to most legacy HPC applications, that are commonly written in Fortran or C/C++, using the MPI standard.

This work addresses the problem of automatically detecting at system-level the equality of the application's state. This allows to automatically verify safety and liveness properties on legacy HPC applications. We present how this state equality detection can be achieved without any source code static analysis, but at runtime using memory introspection and classical debugging techniques.

We demonstrate the effectiveness of our approach through the exhaustive verification of several programs from the MPICH3 test suite and through the partial termination analysis of some applications from the Competition on Software Verification (SV-COMP).

Introduction

Model checking is an appealing automated technique to establish the correctness of distributed systems. But applying this technique to legacy applications requires a complete model of the application. Manually building such models is error-prone and labor-intensive. Keeping the resulting model up to date when the real application is modified constitutes another challenge. A guided approach such as the CEGAR abstraction/refinement methodology [START_REF] Clarke | Counterexample-Guided Abstraction Refinement[END_REF] can ease this modeling step, but the user still needs a high level of expertise in formal methods. Source code static analysis [START_REF] Engler | Static Analysis Versus Model Checking for Bug Finding[END_REF] can automatically reconstruct a model, thus removing the burden induced by the modeling step. This interesting approach is used in many existing tools [START_REF] Ball | A Decade of Software Model Checking with SLAM[END_REF][START_REF] Beyer | The Software Model Checker Blast: Applications to Software Engineering[END_REF][START_REF] Gurfinkel | YASM: A Software Model-checker for Verification and Refutation[END_REF]. Our work is in line with another approach called formal dynamic verification (or execution-based model checking), where the model is not explicitly known but only implicitly explored through the actual execution of the real application. The verification is thus performed on the concrete implementation of the application. In some sense, it is orthogonal with the static analysis, as static analysis and dynamic verification gather complementary but not redundant information: these approaches could be combined in the same tool.

Ultimately, our goal is to dynamically verify unmodified legacy distributed applications composed of sequential processes interacting through message passing. Certifying the whole MPI applicative stack is beyond our scope because it would require to also certify the runtime and environment while we only consider the application to be executed in this environment. This may not be sufficient for the most critical applications, but this already allows to find issues in real code.

We build upon the SimGrid framework, initially intended to assess the performance of distributed applications [START_REF] Casanova | Versatile, Scalable, and Accurate Simulation of Distributed Applications and Platforms[END_REF], and upon the SimGridMC module to dynamically verify the correctness of these applications [START_REF] Merz | Verification Support for a Multi-API Simulation Platform[END_REF]. It exhaustively explores the execution paths that the verified application could follow from a initial situation provided by the user. The considered non-deterministic choices consist in the message reception order: when two messages A and B are in flight, the verification consists in first exploring the execution path where the message A is delivered before B. The application is then rewinded to explore the execution path where B is delivered first. Since we work with legacy applications, the state consists in the heap, the stacks and all global variables. Each transition encompasses a message reception by a process, and its sequential execution up to the next message exchange. The sequential execution blocks are supposed to be deterministic. We believe that these assumptions are realistic and sufficient for mono-threaded MPI-like computational applications, which outcome typically only depends on the input data provided in the initial state and on the message delivery order. Leveraging the simulator architecture to fold the verified application into a single local process makes it easier to inspect, checkpoint and rewind the complete system state. The state space explosion problem is mitigated through Dynamic Partial Ordering Reduction (DPOR) [START_REF] Merz | Verification Support for a Multi-API Simulation Platform[END_REF].

In the current work, we tackle the problem of comparing system-level states of arbitrary legacy applications written in Fortran or C/C++. Detecting state equalities is mandatory to detect infinite executions and cycles, and makes it possible to verify liveness properties. Specifically, this article makes the following contributions: we detail the challenges posed by the system-level state equality detection. We propose solutions to mitigate each of those difficulties, leveraging debugging techniques to retrieve semantic information on the application. We show the practical effectiveness of our proposal through several sets of experiments: we detect liveness violations in a custom MPI code; we show the absence of infinite execution paths in programs from a Software Verification Competition; we exhaustively explore an infinite-time MPI application as well as several of the MPI applications from the official MPICH3 testsuite.

The remainder of this article is organized as follows: Section 2 presents why state equality is an important problem for the formal verification of legacy applications. Section 3 details our contribution, which is evaluated in Section 4. Section 5 presents the related work while Section 6 concludes this article.

State Equality for the Formal Verification of Legacy Applications

Prior to this work, SimGridMC was stateless: only the system's initial state was checkpointed. When rewinding the application, the initial state was first restored and then all transitions leading to the desired state were replayed. This section presents several use cases of the state equality in the context of the formal verification of legacy distributed applications.

Efficiently Verifying HPC Programs and State Equality Reduction

The stateless approach was satisfying in the considered context of Peerto-Peer (P2P) protocols, but it is less adapted to HPC applications, as the computations make the execution path highly time-consuming in this case. It is then interesting to checkpoint more states to directly restore the desired state instead of reconstructing it iteratively. Another advantage of the stateful exploration is to reduce the size of the explored state space by cutting the exploration when reaching a state that was already explored. In principle, this reduction technique is complementary to other ones such as DPOR.

The first limitation of the existing stateful verification tools is that they either only save parts of the system state after decomposition [START_REF] Saissi | Efficient Verification of Distributed Protocols Using Stateful Model Checking[END_REF] or only save a bitstate hash of each reachable state rather than the full state [START_REF] Holzmann | An Analysis of Bitstate Hashing[END_REF]. This is probably due to classical memory space restrictions, but not saving the intermediate states forces to recompute them on need. Nowadays, some computers are equipped with terabytes of memory. This makes it possible (and thus appealing) to checkpoint and analyze the whole memory state of medium-size applications, or smaller instances of legacy HPC applications.

Another limitation of the existing stateful verification tools is that they target abstract models. Adapting these techniques to legacy HPC applications is technically very challenging because we usually lack the abstract model of these applications that are typically written in Fortran or C/C++. Instead of adapting bitstate hash techniques to legacy applications, we checkpoint the full application state: the heap, the stacks and the sections containing the global variables are copied. Capturing thousands to million of states, as required by typical verifications, can rapidly exhaust the available memory. In many applications, only a small part of the memory changes between consecutive states. In some applications 99% of the memory pages do not change between consecutive states. Our snapshots are thus compacted by exploiting the similarity between states: identical memory pages (ie, memory segments of size 4KiB) are shared between snapshots.

Verifying Arbitrary Liveness Properties on Legacy Code

The execution loops detected by the state equality mechanism constitute non-progressive cycles. They play a central role in the verification of liveness properties, since the counterexample to liveness properties are infinite paths. If the application state size is bounded (in particular, if the stack size is bounded), most infinite paths contain such an execution loop. Liveness properties are then verified through the search of acceptance cycles in the Cartesian product of the application with a Büchi automaton encoding the negation of the verified property. If found, such an acceptance cycle denotes an infinite execution path which constitutes a counterexample to the property.

This approach can sometimes be used to falsify the program termination using the property "Always, Eventually, the program terminates". If it is naturally impossible to solve the Halting Problem in all generality, it remains sometimes possible to prove whether a given program terminates or not [START_REF] Cook | Proving Program Termination[END_REF]. Dynamic verification can check the termination of any finite protocol, although sometimes inefficiently. It could also correctly diagnose applications that do not terminate because of non-progressive cycles, provided that these cycles are detected. This approach fails on applications which do not terminate but whose state changes infinitely often, which is consistent with the indecidability of the Halting Problem.

MaceMC [START_REF] Killian | Mace: Language Support for Building Distributed Systems[END_REF] is the verification tool that comes closest to our work since it is able to verify some liveness properties on concrete implementations of distributed systems. Instead of detecting the acceptance cycles, it looks for the so-called critical transition that plunged the property into a violation. The exploration performance is then improved using state hashing. This approach remains however limited to the restricted set of liveness properties that can be expressed as ♦p (Always Eventually p) where p is a logical predicate, while detecting acceptance cycles can be used to verify arbitrary properties that can be expressed using the Linear Time Logic (LTL X ).

Verifying (infinite-time) Cyclic Protocols

Non-progressive cycles constitute an inherent part of a whole class of applications, such as the cyclic protocols which react to external periodic events, as most P2P protocols do.

Stateless DPOR cannot study such systems because even if it reduces the amount of explored interleavings by detecting the independent actions, it does not detect all execution cycles. The state space is still infinite after the DPOR and thus cannot be explored explicitly during a dynamic verification. On the contrary, a state equality reduction cuts the repetitive patterns of the application behavior, which permits the exhaustive verification of cyclic protocols.

System-level State Equality Detection

The stateful verification mandated by the previously presented use cases requires to efficiently determine at system-level whether two given application states are semantically equal or not. All relevant memory area must be included in this comparison, including global variables, the heap, the simulated processes' stacks, as well as the simulator's network state.

Comparing memory byte per byte is not sufficient to detect the state equality, as it detects many syntactic differences that are not significant to the application semantic. For example, the numerical values of pointers on different memory areas are syntactically different while the pointed memory areas could be semantically equivalent. Such false negative must be avoided by all means, as the tool could fail to detect some state equalities, possibly leading to the nondetection of property violations. The key to a better state equality detection lies in the ability to introspect the memory and to reconstruct the semantic of bits.

For Java applications, the whole memory is handled by the virtual machine. Using the meta-data known to the JVM, it is thus possible to reconstruct the semantic of each byte in memory, making it possible to detect system state equalities. However, this would probably require to modify the JVM directly, as Java introspection is more intended to explore the values of objects' content rather than exploring the meaning of memory locations. Adding the needed meta-data and keeping them in sync in the whole JVM source code constitutes a daunting task, but remains feasible [START_REF] Havelund | Model Checking Java Programs using Java PathFinder[END_REF].

However, Java is rarely used in the context of HPC applications using MPI, calling for another approach that would be applicable to C/C++ applications. In [START_REF] Fonseca | Finding Complex Concurrency Bugs in Large Multi-threaded Applications[END_REF], the user must provide a hashing function that can be used to detect the state equalities. Detecting system state equalities is easier when the complete data semantic is known, but this remains a burdensome and highly error-prone task, hardly adaptable to complex systems. In the following, we propose a generic solution which operates at the operating system level. Instead of specifying the segments of memory that are relevant to the system's semantic, we start by considering the whole system memory, and optionally ignore some sections that are known to be irrelevant.

SimGridMC relies on SimGrid to fold the distributed MPI application into a single UNIX process, where each MPI rank is executed as a thread. The network state is captured by the simulator, and is expressed in the process's memory. This process is then formally verified by SimGridMC, which lives as a separate UNIX process interacting with the SimGrid library in the verified process through a pair of network sockets.

Figure 1 represents the system state that we consider: it aggregates the application's global variables, the application's heap and the stack of each MPI rank. At the OS-level, all data are stored in several memory segments, that our state comparison algorithm consider sequentially.

In the following, we detail our approach using Linux as an example, but our implementation was successfully ported to FreeBSD. Porting our code to other operating systems is certainly possible, even if it would be somehow harder for non-Unix systems.

In the remainder of this section, we detail the causes of the syntactic differences that defeat the byte per byte comparison of memory segments. For each of these challenges, we show how additional information could be retrieved from the system, and leveraged to rebuild the needed semantic information. For some of these difficulties, we must rely on heuristics that could conclude on the difference of semantically equal states. This must be avoided when possible, as this could jeopardize the soundness of the verification process. That is why we do not aim at certifying the verified applications, but rather at finding bugs that are hard to detect on real applications.

Uninitialized Data and Memory Overprovisioning

The first source of syntactic differences that are not relevant to the semantic equality lies in uninitialized data. In contrast to Java, the memory handed over to the user is not initialized by the C/C++ runtime because of performance concerns. This is true for the blocks allocated on the heap (that still contain the content of their previous use), and also for the stack (which still contains the frames of returned functions).

In addition, most dynamic memory allocation libraries (such as malloc implementations) allocate memory chunks whose sizes are powers of two to avoid the memory fragmentation. For example, a memory area of 64 bytes will be used to serve a request of 48 bytes. It is expected that the application only uses the requested area while the extra area remains unused (Fig. 2). In our context, this memory overprovisioning may result in irrelevant byte differences that are not trivial to address at the application level, as the extra memory area are not directly known to the application but still contain the arbitrary data, written by the previous use of that chunk. SimGridMC provides a specific implementation of malloc to address both problems of uninitialized heap area and heap over-provisioning. A first approach for heap over-provisioning is to only consider the user-requested area during the state comparison and to ignore the extra memory. But this would not work for applications that exhibit small buffer overflows. Indeed, if the application accidentally overflows from the requested area while remaining within the bounds of the corresponding malloc chunk, the problem will remain usually harmless, but our analysis would fail to capture the whole state. Instead, we address this issue by filling each newly allocated area with zeroes before handing it to the application. This ensures that every value is specified while remaining robust to limited buffer overflows. Although SimGridMC is not initially intended to detect this kind of bug, we could add an option to detect and report heap overflows, e.g. with mprotected pages located after each allocated block. Similarly, zeroing memory areas may hide bugs resulting from undefined behaviors and other tools and approaches should be used to track these issues.

Uninitialized data and memory over-provisioning also occur within the processes' stacks. The local variables may remain unset by the user program while the memory occupied by a stack frame is not zeroed out by the system when a function returns. We circumvent this problem by only considering the stack area that is in active stack frames and optionally by zeroing out the stack frame at the beginning of each function. This is currently implemented by modifying the assembly code generated by the compiler before giving it to the assembler: a script estimates the size of the stack frame of each function by parsing its assembly code, and adds assembly instructions that zero out the stack frame at the beginning of the function. This script has been used with both GCC and Clang for C, C++ and Fortran input. It is currently implemented for x86 64 only but could easily be ported to other targets. This post-processing must be done for the whole application and the simulator, or it could be completely omitted if the user code initialize all local variables when declaring them.

Sparse Memory and Padding Bytes

The compiler enforces memory alignment constraints to speed up the data movements between the memory and the CPU registers. The address of each variable must be a multiple of its size. For example, short integers (of size 2 bytes) must reside at even addresses. This results in sparse memory layouts with padding bytes added between the variables (as depicted on Fig. 3), leading to irrelevant syntactic differences if the values of those padding bytes are compared. On some platforms, it is possible to disable these padding bytes, using the #pragma pack(1) compiler directive. But the resulting major performance impact mandates for other solutions because misaligned data requires several cycles to move from memory to the CPU registers.

In the heap, our solution to the previous issue happens to address that problem too, since the padding bytes are zeroed out and thus specified. This remains problematic in the stack despite zeroing it out for two reasons. First, each stack frame is protected by the system against buffer overflow and stack smashing security attacks through the addition of arbitrary data in the stack by the system. Any change to this data is interpreted by the system as a security attack. If integrated to the comparison, this arbitrary data could defeat the state equality detection. In addition, several local variables can share the same location in the stack memory if they do not exist at the same time of the program flow. This may lead to temporarily unused memory areas in the stack.

Our approach is to focus on the actual data stored on the stack and to ignore the unspecified values and padding bytes. We retrieve the needed information from the debugging symbols using two complementary libraries: libunwind1 is used to analyze the content of each stack frame and retrieve the address and type of local variables. The memory layout of each encountered data type (size and alignment constraints) is in turn retrieved from the DWARF2 -formatted debugging information. This information is generated by the compiler so that debuggers such as gdb can reconstruct the memory layout of the debugged process. Our implementation works on Linux and FreeBSD only, but this approach is portable to other systems. The DWARF format is also used on MacOS X while Windows provide the same information under another format.

The DWARF information alone is sufficient to rebuild a fine-grain semantic of each byte in the global segment. Coupled with libunwind, it is sufficient for the stack segments. It is however not sufficient to reconstruct the semantic for the heap, as the user can cast the allocated data to arbitrary types. This difficulty is addressed in the following section.

Heap Dynamic Semantic Comparison

The last and most difficult technical lock of system-state state comparison is due to the fact that the order in which memory blocks are allocated rarely matters to the application semantic while it greatly impacts their actual location in memory. Fig. 4 depicts two heaps that are semantically equivalent despite their different block orderings. The content of blocks 0x30, 0x40 and 0x50 are syntactically different, but these differences come from the fact that the block 0x30 of one heap corresponds to the block 0x40 of the other heap. The semantic of these heaps is perfectly equivalent for the application.

Such situation often occurs in our context because the block ordering stems from the order of malloc requests, which changes when the process execution order changes, as in the dynamic verification.

Moreover, the numerical value of a pointer remains unchanged in C when the pointed area is freed. As the system may reallocate the previously freed memory, the pointed data may be completely different. It is a good habit as a programmer to set the pointer variables to NULL in this case, but this is not requested by the C standards. The manual detection of these dangling pointers by the user is however essential to the soundness of our approach, as the comparison of unrelated memory areas leads to the non-detection of the system state equality.

Even if there is no dangling pointer, detecting the semantic equality between heaps in which blocks were reordered remains hard. We cannot directly leverage DWARF debugging information, as the considered memory is allocated during the execution and thus unknown at compile time when this information is produced. Type aliasing of heap data is also a common practice that defeats the formal identification of the data types. In [START_REF] Iosif | Symmetry Reductions for Model Checking of Concurrent Dynamic Software[END_REF], the author presents a heap canonicalization algorithm that can reorder the blocks in a canonical form to ease heap comparison. This approach relies on a garbage collecting mechanism in a language where all references to allocated data are clearly known to the system. A mark-and-sweep algorithm is then conducted from all variables down to the blocks. The graph traversal is deterministic by construction, and the blocks are reordered on-the-fly into a canonical form.

This approach cannot be applied as is to our context because we cannot assume that the verified application uses one of the existing garbage collector for C/C++. We can retrieve the references located in local and global variables according to their DWARF signature, but we will probably miss some references located in heap blocks as we lack any semantic information on the content of these blocks.

Because of these missing references, it is impossible to move memory blocks: any reference still pointing to an old block location would cause the application to abort immediately.

It is still possible to compare two given states on the fly using a mark-and-sweep approach. Starting from the global and local pointer variables (identified through libunwind and DWARF), all heap blocks that are reachable through identified pointers are marked as equivalent in both states. We perform a partial mark-and-sweep, starting from the variables we know and iterating on data for which we have the debugging information. This traversal can have several outcomes. It first stops when an inexplicable difference is found, indicating that both states differ. It may also manage to match all blocks, despite their potentially different location in both heaps, proving equality of both states' semantic.

But this traversal can only be a heuristic because of the missing typing information. First and foremost, we lack any typing information about the data on the heap. Then, the actual datatype may be unknown or hidden by void* type aliasing. Finally, local variables may be hidden at some execution points because of scoping rules within the function, hiding some valuable starts for the mark-and-sweep traversal.

It is thus possible that some blocks allocated on the heap were not considered during the traversal, because the pointer to them were not identified as such because of missing typing information. The remaining blocks are then compared byte per byte. If we find a difference, we attempt to explain this as a pointer difference: in each heap, we read the aligned 8 bytes that contain the differing byte as a pointer. If each value corresponds to the address of a valid heap block, the comparison iterates recursively on the designated blocks.

The comparison algorithm can detect dangling pointers in some cases (when they point to unallocated heap blocks or above the top of the stack). Better detection of dangling pointers could be achieved by avoiding to reallocate heap blocks as long as they are reachable.

The practical effectiveness of this heuristic is evaluated in Section 4.

User-identified Irrelevant Differences

Specific variables and memory areas can also be explicitly ignored during the comparison. The user indicates to ignore the step number in a cyclic protocol, the value of an iterator in a loop or any value that he considers irrelevant to its state. A different system behavior resulting from the value of the counter will be detected in the other memory areas, while this counter could be ignored.

The same mechanism is used to mask irrelevant differences caused by the simulator internals, such as the total amount of messages sent during the simulation or other similar statistics. Determining the sections to be manually marked as irrelevant can be very tedious. In the future, we plan to issue a warning when two states differ only by a very little amount of bytes, allowing the user to check whether this difference must be marked manually or not.

Summary

Table 1 summarizes the difficulties encountered during the system-level comparison of state equality, and the solution that we propose in each case for both the heap and the stack. As a final optimization, we test first and foremost several efficient criteria such as the total amount of allocated blocks, allocated data, and stack sizes of all processes. This allows to eliminate many candidate states even before traversing the heaps.

Experimental Evaluation

This section evaluates our contribution through three sets of experiments which illustrate the motivating examples of Section 2 that leverage state equality detection in the context of dynamic verification of legacy applications. Section 4.1 focuses on the exhaustive verification of several applications distributed as part of the MPICH3 testsuite. Section 4.2 then evaluates the tool's ability to detect two kinds of liveness violation: on a custom MPI application and the termination of a program. Section 4.3 demonstrates how state equality detection enables the exhaustive exploration of cyclic applications whose behavior is regular but not bounded in time.

We used SimGrid (60,000 lines of code -git version d8710e), as our contribution is integrated to the public version of this framework. These experiments were conducted on a Intel(R) Xeon(R) CPU E7540 @ 2.00GHz, RAM 512GiB, 48 cores, with debian wheezy environment 3.2.0-4-amd64 and 3 extra packages (cmake 2.8.9, libunwind7, and gfortran 4.7.2).

In all subsequent tables, '#P' is the total amount of processes in the studied application, '# States' corresponds to the number of expanded states before finding the counterexample (or the total number of states in the case of exhaustive exploration), and 'Depth' is the depth in which the counterexample has been found (only for the verification of a liveness property).

Exhaustive Verification of MPICH3 Testcases

This first experiment focuses on the MPICH3 testsuite3 . This testsuite allows to test the standard compliance of any MPI implementation. Not all of the tested features are currently implemented in SimGrid so we eliminated the corresponding tests. We verified several applications from this testsuite, each of them lasting about 1,300 lines written in C or Fortran. These tests were not modified from their original version. In particular, we did not manually mark any sections as irrelevant, as presented in Section 3.4. Since our tool is written in C and C++ itself, these experiments demonstrate our ability to verify programs written in C/C++ or Fortran.

Our verification algorithm consisted in exploring every orders of network message delivery that respect the causal constraint. We consider the blocks between message exchanges as atomic. We took one snapshot of the whole application after each message exchange, sharing identical pages between snapshots to reduce the memory consumption. We compared each snapshot to all others using the contribution presented in this work, and then searched for non-progressive cycles (i.e., livelocks) in the resulting graph.

Table 2 compares the performance of the exploration (with and without state equality reduction) for these applications while verifying this simple liveness property. The DPOR reduction was not activated in these experiments since our current DPOR implementation is not neither compatible with liveness properties nor with our implementation of the state equality reduction. We managed to exhaustively explore the state space of these applications for up to 6 processes (no error has been found during these explorations). These results clearly demonstrate the necessity of the state reduction to exhaustively explore the state space of even basic tests with few processes.

Dynamic verification of liveness properties

This experimentation part is divided into two experiments. We demonstrate firstly the ability of our tool to detect a liveness violation on a custom MPI application. Then we study the termination on some programs from the Competition on Software Verification (SV-COMP).

Custom Implementation of Centralized Mutual Exclusion

The first experiment uses a custom MPI implementation of the centralized mutual exclusion algorithm (about 100 lines of code), where a coordinator grants infinitely often a mutex to the clients that request it. We introduce an error so that one of the clients never gets the requested critical section (its requests are discarded). We verify the following liveness property: (r → ♦cs) (any process that makes a request (r) must eventually obtain the critical section (cs)). Since one client never gets the cs, this property is actually violated.

This example is the only case where we had to manually mark a given variable as irrelevant to the comparison (see Section 3.4). We ignored a field in a data structure returned by MPI. In this specific case, this could probably be automatized in the future.

A counterexample is accordingly found by our tool. The duration of this exploration can vary from few seconds if the violation in on the first explored branch, to several hours if the violation is in another branch. Table 3 presents the worst case results, when the buggy process is the last one. With such infinitetime applications, a stateful exploration is mandatory to detect and avoid nonprogressive cycles that could prevent the verification from terminating.

Program Termination of SV Competition

The second experiment for the dynamic verification of liveness properties focuses on a very specific liveness property: "Always, Eventually, the program terminates". As explained previously, detecting a non-progressive cycle (that is, a cycle of infinite length composed of a finite amount of states) is enough to determine that the program will never terminate. Note that a program without any non-progressive cycle can still fail to terminate, which is consistent with the fact that the Halting Problem is undecidable.

To study this liveness property, we selected some test cases of the Software Verification Competition (SV-COMP), which aims at assessing the state of the art in the field of software verification. The competitors of SV-COMP are usually based on static analysis, but we wanted to evaluate whether the same results could be obtained through dynamic analysis. Since our code can only verify MPI applications, we modified the benchmarks to add second MPI rank observing the system progress. For each applicative step taken by the worker rank while actually running the benchmark, a MPI message is sent to the observer. This makes the system observable by SimGridMC without changing the semantic of the original benchmark.

The Program Termination category of SV-COMP'15 entails 18 test cases that exhibits a non termination. 14 of these tests present an infinite state space, for example with an integer variable that is incremented at each step. Even if static analysis tools can handle such programs, our approach is not effective as it is not possible to explore explicitly and exhaustively such state space. As a result, these cases were not included in our evaluation.

The remaining tests are rather simple: two of them (WhileTrue and Madrid) are infinite loops containing only constant affectations. The third one (Rota-tion180) permutes three values while alternating their sign. In the fourth one (NonTerminationSimple5), a variable is randomly either incremented or decremented at each step of an infinite loop.

Our tool manages to find the non-progressive cycle in a matter of seconds in each of these cases involving only a few states, but for the last program. NonTerminationSimple5 presents several different infinite execution paths: the variable can iterate over an infinite amount of values if it is constantly incremented (resp. decremented). The variable can also infinitely loop over only 2 values if it is alternatively incremented and decremented. Our tool detects the second case when limiting the maximum exploration depth so that the second branch of the second alternative gets explored (increasing after decreasing, or the opposite).

Similarly to the 14 tests that were not included in this evaluation, the first kind of infinite execution path presented by NonTerminationSimple5 entails an infinite amount of different states. This defeats our approach of dynamic verification of termination, as it is based on the detection of execution loops leading to previously evaluated states. This is a clear limitation over the scope of our verification methodology, somewhat reducing our impact on this use case. This limitation should be balanced with the versatility of liveness properties that can be verified, which can be much more complex than the termination property. In addition, this limitation does not reduce the effectiveness of the state equality detection presented in this article, that can also be leveraged in the other use cases and that perfectly works in this evaluation when it is applicable.

Stateful exhaustive exploration of infinite-time application

The goal of this experiment is to prove the applicability of our approach to cyclic applications. To that extent, we use a modified version of the centralized mutual exclusion algorithm used previously. The bug was removed, and the processes were modified to loop forever, requesting (resp. granting) the critical section at each step.

We could exhaustively verify this infinite protocol in four minutes for 3 processes (8,216 states found, 1 GiB) and almost 18h for 4 processes (480,997 states found, 49 GiB).

Related work

Since this work leverages dynamic analysis techniques, we do not discuss approaches based on static analysis. These orthogonal approaches could be used jointly to benefit both several sources of information during the verification.

Many tools exploit dynamic analysis either for the verification of C programs [START_REF] Cousot | The ASTRE É Analyzer[END_REF][START_REF] Beyer | The Software Model Checker Blast: Applications to Software Engineering[END_REF][START_REF] Bagnara | On the Design of Generic Static Analyzers for Modern Imperative Languages[END_REF] with abstract interpretation in some cases and focused on memory-related errors [START_REF] Dudka | Predator: A Tool for Verification of Low-Level List Manipulation[END_REF][START_REF] Clarke | A Tool for Checking ANSI-C Programs[END_REF] or in particular for the termination analysis [START_REF] Falke | Termination Analysis of C Programs Using Compiler Intermediate Languages[END_REF][START_REF] Alias | Rank: a tool to check program termination and computational complexity[END_REF]. This approach is also commonly used for Java [START_REF] Havelund | Model Checking Java Programs using Java PathFinder[END_REF] or object-based program analysis, with a garbage collection mechanism [START_REF] Aan De Brugh | MoonWalker: Verification of[END_REF]. As explained in Section 3, it is easier to implement this approach for languages served by a virtual machine, as the meta-data known to the virtual machine are precious in this context. The semantic of any byte of memory is known to the VM, that can in particular retrieve and follow pointers. This operation is much harder in our case. Our heuristic must deal with generic pointers, invisible variables, dangling pointers and otherwise unknown pointers, that cannot happen with a garbage collector.

To the best of our knowledge, our contribution is the first extension of the heap canonicalization algorithm proposed in [START_REF] Iosif | Symmetry Reductions for Model Checking of Concurrent Dynamic Software[END_REF] to languages without automatic garbage collection. Strictly speaking, this is not a heap canonicalization algorithm, as it does not change the order of blocks in memory, but it fulfills the same need for heap semantic comparison. Our approach allows to perform the verification on the actual program memory without using state vectors. This direct use of the actual state can reduce the risk of abstraction errors. This state equality comparison is a major technical lock to the formal verification of HPC applications. Although the need of such methods is well acknowledged in this context [START_REF] Gopalakrishnan | Formal Analysis of MPIbased Parallel Programs[END_REF], there exist few verification tools for MPI applications. To the best of our knowledge, MPI-CHECK [START_REF] Luecke | MPI-CHECK: a Tool for Checking Fortran 90 MPI Programs[END_REF] is the only verification tool of Fortran 90 MPI programs. Thanks to compile-time and runtime tests, it detects deadlocks and some inconsistencies in MPI calls such as negative message lengths. But the exploration is not exhaustive and the achieved tests are limited. Gauss [START_REF] Palmer | Gauss: A Framework for Verifying Scientific Computing Software[END_REF] and MPI-Spin [START_REF] Siegel | Model Checking Nonblocking MPI Programs[END_REF] are model extractors for MPI applications which can then be checked with Zing [START_REF] Andrews | Zing: A Model Checker for Concurrent Software[END_REF] and SPIN [START_REF] Holzmann | the Spin Model Checker: Primer and Reference Manual[END_REF] respectively.

Finally, ISP [START_REF] Vo | Formal Verification of Practical MPI Programs[END_REF] and its distributed counterpart DAMPI [START_REF] Vo | A Scalable and Distributed Dynamic Formal Verifier for MPI Programs[END_REF] are dynamic verifiers specifically tailored for the verification of MPI applications written in C. They check for deadlock and local assertion violations without requiring users to manually model their code. ISP hijacks the PMPI profiling interface that is normally intended for tracing tools to gather information about the MPI calls. ISP mediates these MPI calls and performs the dynamic verification at that level. A distributed protocol is then used between nodes to determine which messages should be delayed within the "profiling" call, and which ones can be proceed (after being rewritten).

This approach leads however to two major drawbacks. First, collective operations are seen as atomic calls from the profiling interface perspective. The point-to-point communications that compose these collectives are completely invisible at this level. It means that unlike SimGridMC, ISP cannot properly verify collective operations, that must be assumed intrinsically correct. This seems unfortunate given the current momentum on asynchronous group collectives, that are known to be error-prone to implement [START_REF] Gopalakrishnan | Formal Analysis of MPIbased Parallel Programs[END_REF]. Moreover, the real execution of the application on a real distributed platform may pose subtle challenges to ensure that the simulation is reproducible. Likewise, rewriting the MPI calls may change the synchronization semantic, that may depend on the buffer sizes in some border cases [START_REF] Ahn | Overcoming Extreme-scale Reproducibility Challenges Through a Unified, Targeted, and Multilevel Toolset[END_REF]. SimGridMC is based on the versatile SimGrid framework instead which is reproducible by design. It is much easier to observe and control the distributed system when it is folded into a unique system process, resulting in simpler and thus more robust setups.

Conclusion and Future Work

System state equality detection is essential for the dynamic verification of applications. It is important to verify arbitrary liveness properties, to explore exhaustively infinite cyclic protocols and constitutes an efficient reduction mechanism during stateful explorations. Detecting system state equalities is however much harder with legacy distributed applications than with abstract models.

In this article, we detailed the root causes of these difficulties, and proposed various solutions leveraging debugging information and tools. We presented a heuristic to detect the state equality of an application at system-level. Even if missing typing information may lead to false negative, this memory introspection technique is to the best of our knowledge the first solution to reconstruct semantic information about systems that use programming languages without automatic garbage collection.

Despite its apparent simplicity, our heuristic proves efficient in practice. It was evaluated on the dynamic formal verification of several properties on various test cases from the official MPICH3 testsuite. We were able to actually verify and exhaustively explore these legacy distributed applications.

This contribution is integrated in the SimGrid framework 4 , making it possible to jointly evaluate the correctness and performance of distributed applications.

Our approach cannot be used for certification but only for bug finding as it relies on a heuristic. The improvement beyond prior work on verifying unmodified legacy HPC programs is many-fold: any safety or liveness property can be verified, and some class of infinite time-applications can be verified. These properties can be assessed on arbitrary C/C++ or Fortran mono-threaded applications based on MPI, using only the debugging symbols. This may be applicable even if the source code is not available.

In the future, we want to combine our approach with other classical methods to increase the amount of available information during the reduction. For example, visibility information that can be extracted from instrumentation are mandatory to combine the DPOR and stateful reductions [START_REF] Yang | Efficient Stateful Dynamic Partial Order Reduction[END_REF]. Memory graphs that can be reconstructed from static analysis would help extending the applicability of our approach to multithreaded MPI applications. We also want to evaluate complex MPI code, such as the asynchronous collective calls implemented in MPICH and OpenMPI or even full MPI applications.

Figure 1 :

 1 Figure 1: Memory layout of a process.

Figure 2 :

 2 Figure 2: Memory allocation with overprovisioning.

Figure 3 :

 3 Figure 3: Data memory alignment is preserved by adding unused padding bytes.

Figure 4 :

 4 Figure 4: Two heaps syntactically different but semantically identical.

Table 1 :

 1 Summary of issues and solutions for the system-level state equality detection.

	Issue	Heap solution	Stack solution
	Overprovisioning	memset 0	Stack pointer detection
	Uninitialized data	memset 0	Stack cleaner by binary code modification
	Padding bytes	memset 0	DWARF + libunwind
	Syntactic differences	Dynamic semantic comparison	N/A (sequential access)
	Irrelevant differences	Ignore explicit areas	DWARF + libunwind + ignore

Table 2 :

 2 Verification of the liveness property stating that there is no non-progressive cycles, applied to several MPI applications from MPICH3 testsuite.

Table 3 :

 3 Verification of the property (r → ♦cs) on a bugged mutual exclusion (worse case).

	# P	# States	Time	Memory Depth
	3	101	2,5 s	0.35 GiB	94
	4	287	3 s	0.37 GiB	267
	5	960	5,5 s	0.62 GiB	890
	8	68,128	18 min 40 s	5 GiB	62,831
	10	> 200,000	> 1 h	> 16 GiB	-

http://www.nongnu.org/libunwind/

http://www.dwarfstd.org/

The MPICH project: http://www.mpich.org

SimGrid is freely available from http://simgrid.org/

Acknowledgments

This work was partially funded by the ANR project SONGS (ANR-11-INFRA-13). Some experiments were carried out using the Grid'5000 experimental testbed, being developed under the Inria ALADDIN development action with support from CNRS, RENATER and several Universities as well as other funding bodies (see https://www.grid5000.fr/). The authors would like to thank Matthieu Volat for his precious help to port this work to the FreeBSD operating system.


Benjamin Camus
email: benjamin.camus@inria.fr

Anne-Cécile Orgerie
email: anne-cecile.orgerie@irisa.fr

Martin Quinson
email: martin.quinson@irisa.fr

Co-simulation of FMUs and Distributed Applications with SimGrid

Keywords: Computing methodologies → Discrete-event simulation, Simulation tools, Continuous simulation, Distributed programming languages, • Computer systems organization → Embedded and cyber-physical systems, co-simulation, FMI, distributed system, cyber-physical system

The Functional Mock-up Interface (FMI) standard is becoming an essential solution for co-simulation. In this paper, we address a specific issue which arises in the context of Distributed Cyber-Physical System (DCPS) co-simulation where Functional Mock-up Units (FMU) need to interact with distributed application models. The core of the problem is that, in general, complex distributed application behaviors cannot be easily and accurately captured by a modeling formalism but are instead directly specified using a standard programming language. As a consequence, the model of a distributed application is often a concurrent program. The challenge is then to bridge the gap between this programmatic description and the equation-based framework of FMI in order to make FMUs interact with concurrent programs. In this article, we show how we use the unique model of execution of the SimGrid simulation platform to tackle this issue. The platform manages the co-evolution and the interaction between IT models and the different concurrent processes which compose a distributed application code. Thus, SimGrid offers a framework to mix models and concurrent programs. We show then how we specify an FMU as a SimGrid model to solve the DCPS co-simulation issues. Compared to other works of the literature, our solution is not limited to a specific use case and benefits from the versatility and scalability of SimGrid.

INTRODUCTION

Cyber-Physical Systems (CPS) can be defined as "physical and engineered systems whose operations are monitored, coordinated, controlled and integrated by a computing and communication core" [START_REF] Ragunathan (raj) Rajkumar | Cyber-physical Systems: The Next Computing Revolution[END_REF]. In this article, we focus on a specific (although common) class of CPS called Distributed-CPS (DCPS) that are CPS equipped with a geographically distributed computing application -i.e. an application that consists of several concurrent processes, possibly remotely located, and interacting through message exchanges. Such systems include notably smart-grid [START_REF] Mittal | A System-of-systems Approach for Integrated Energy Systems Modeling and Simulation[END_REF], smart-home [START_REF] Gilpin | Co-simulation Solution using AA4MM-FMI applied to Smart Space Heating Models[END_REF], cloud infrastructure [START_REF] Fontoura | Energy-Efficient, Thermal-Aware Modeling and Simulation of Datacenters: The CoolEmAll Approach and Evaluation Results[END_REF] and smart-city [START_REF] Wang | Towards Generalized Co-simulation of Urban Energy Systems[END_REF].

In most cases, a Modeling and Simulation (M&S) process is required to design and study DCPS systems. However, several expert skills belonging to different scientific fields may be required. In this multidisciplinary approach, each domain comes with its own try and tested models and tools. The challenge is then to have a unified approach with a set of heterogeneous M&S tools (i.e. models and simulation pieces of software). A growing strategy to tackle this challenge is co-simulation [START_REF] Gomes | Co-simulation: State of the art[END_REF] which consists in coupling different standalone M&S tools, so that they simulate the whole system together. The advantages of co-simulation include that [START_REF] Akoush | Predicting the Performance of Virtual Machine Migration[END_REF] it enables to study the global behavior of the system, (2) it enforces a clear separation of concerns in the M&S process and (3) it enables to reuse and factorize efforts put into the development and validation of M&S tools. Yet, co-simulation raises two main challenges. First, managing interoperability [START_REF] Saikou | Understanding interoperability[END_REF] consists in ensuring that simulation software codesthat may have different API and be written in different programming languages -can exchange usable data during the simulation. Then, the multi-paradigm challenge [START_REF] Vangheluwe | An introduction to multi-paradigm modelling and simulation[END_REF] requires to bridge he different modeling formalisms that are used by the M&S tools. In the case of CPS, this often implies managing a hybrid simulation that combines discrete dynamics (for the computing systems) and continuous dynamics (for the physical systems) [START_REF] Francois | Combined continuous/discrete system simulation languages-usefulness, experiences and future development[END_REF].

Since 2010, the Functional Mock-up Interface (FMI) standard [START_REF] Blochwitz | Functional mockup interface 2.0: The standard for tool independent exchange of simulation models[END_REF] of the Modelica Association is becoming an essential solution toward co-simulation. It offers a unified framework and an API to control equation-based models of multiphysical systems (e.g. electrical, mechanical, thermal systems). The strength of the standard is that it is supported by over 100 M&S tools 1 . These tools enable [START_REF] Akoush | Predicting the Performance of Virtual Machine Migration[END_REF] to design a model and export it as an FMU (Functional Mock-up Unit) -i.e. a simulation unit compliant with FMI- [START_REF] Appel | Continuation-passing, Closurepassing Style[END_REF] and/or to import and use an FMU as a component in their modeling environment. Several frameworks have been proposed to perform co-simulation of FMUs [START_REF] Bastian | Master for Co-Simulation Using FMI[END_REF][START_REF] Cremona | FIDE -An FMI Integrated Development Environment[END_REF][START_REF] Galtier | FMI-Based Distributed Multi-Simulation with DACCOSIM[END_REF], and to integrate continuous FMUs into discrete event formalism environments [START_REF] Camus | Hybrid Co-simulation of FMUs using DEV&DESS in MECSYCO[END_REF][START_REF] Denil | Explicit Semantic Adaptation of Hybrid Formalisms for FMI Co-simulation[END_REF][START_REF] Muller | Linking FMI-based components with discrete event systems[END_REF].

In this paper, we address another issue which arises in the context of DCPS co-simulation where FMU components need to interact with distributed application models. The core of the problem is that, in general, complex distributed application behaviors cannot be easily and accurately captured by a modeling formalism (e.g. finite automata) [START_REF] Casanova | Versatile, Scalable, and Accurate Simulation of Distributed Applications and Platforms[END_REF]. Instead, the most common approach consists in directly specifying a distributed application using a standard programming language. As a consequence, the model of a distributed application corresponds often a concurrent program which runs on a single computer. The challenge is then to bridge the gap between this programmatic description and the equation-based framework of FMI in order to make FMUs interact with concurrent programs. Considering the diversity of DCPS previously cited, an ad-hoc solution should be avoided in favor of a more versatile approach.

In this article, we show how we use the unique execution model of the SimGrid M&S platform [START_REF] Casanova | Versatile, Scalable, and Accurate Simulation of Distributed Applications and Platforms[END_REF] -and more precisely its concept of separated entities' virtualization-to tackle this issue. SimGrid is a versatile platform for the simulation of distributed systems which embeds a set of rigorously validated IT models (e.g. CPU, IP network, disk, energy consumption). The platform manages the co-evolution and the interaction between these models and the different concurrent processes which compose a distributed application code. Thus, SimGrid offers a framework to mix models and concurrent programs. Our contribution is then to specify an FMU as a SimGrid model to ease the simulation of DCPS. Compared to other works in the literature [START_REF] Camus | A Stochastic Approach for Optimizing Green Energy Consumption in Distributed Clouds[END_REF][START_REF] Gilpin | Co-simulation Solution using AA4MM-FMI applied to Smart Space Heating Models[END_REF][START_REF] Mittal | A System-of-systems Approach for Integrated Energy Systems Modeling and Simulation[END_REF][START_REF] Wang | Towards Generalized Co-simulation of Urban Energy Systems[END_REF], our solution is not limited to a specific use case and benefits from the versatility of SimGrid and its validated IT models.

The rest of the article is organized as follow. In Section 2, we describe for illustration purpose the simple yet representative use-case of a chiller failure in a data-center. This use-case illustrates all along the article the challenges of DCPS simulation and our contributions. Section 3 presents the FMI standard and the SimGrid platform. Section 4 details how we integrate FMU into the SimGrid framework. Finally, Section 5 shows how we validate our proposition with the co-simulation of our use-case.

REPRESENTATIVE USE CASE

For illustration purpose, we consider the simulation of a failure in the chiller of a data-center (DC) called DC1. We consider that the failure occurs when the chiller demand (which depends on the heat dissipation induced by computations) becomes too high. After the failure occurrence, a 1 according to http://fmi-standard.org safety mechanism shuts down the power supply if the temperature becomes too high to preserve machines. We want to simulate the computing processes which cause and handle the failure. This requires to model both the distributed application deployed in the DC, and the physical processes of heat transfers.

This use case is representative because it implies:

(1) coupling different M&S tools (OpenModelica and Sim-Grid), (2) which use different modeling paradigms (algebraic/differential/discrete equations and concurrent programs), (3) with discrete (distributed application execution) and continuous (the temperature evolution) dynamics in interaction (the distributed application changes the computers' heat dissipation, and the room temperature triggers power shutdown that kills the running programs).

In the following we describe the different models, their co-simulation and the faced challenges.

Physical system of the DC

To describe the nominal behavior of the physical systems, shown in Figure 1, we use a simplified version of the model of [START_REF] Fontoura | Energy-Efficient, Thermal-Aware Modeling and Simulation of Datacenters: The CoolEmAll Approach and Evaluation Results[END_REF]. We consider a Computer Room Air Handler (CRAH) that sends an airflow through the computing units (called Physical Machines -PM) racks to cool the DC. Thanks to the chiller, the inlet air temperature is always equal to the same temperature 𝑇𝑅 𝑖𝑛 (𝑡). As the air passes through the rack, its temperature increases because of the heat dissipation of the DC 𝑄𝐷𝐶 (𝑡). This quantity is defined as follows:

𝑄𝐷𝐶 (𝑡) = 𝑃 𝑙𝑜𝑎𝑑 𝐷𝐶 (𝑡) + 𝑄 𝑜𝑡ℎ𝑒𝑟𝑠 𝐷𝐶 (𝑡) (1)
𝑃 𝑙𝑜𝑎𝑑 𝐷𝐶 (𝑡) is an input of the model which corresponds to the power consumption and heat dissipation of the PMs. 𝑄 𝑜𝑡ℎ𝑒𝑟𝑠 𝐷 𝐶 (𝑡) corresponds to the heat dissipation of the other devices of the DC (e.g. lighting, Power Distribution Unit) and is equal to:

𝑄 𝑜𝑡ℎ𝑒𝑟𝑠 𝐷𝐶 (𝑡) = 𝛼 × 𝑃 𝑙𝑜𝑎𝑑 𝐷𝐶 (𝑡) (2)
Considering the mass of the air in the room 𝑚𝑎𝑖𝑟 and its specific heat 𝐶𝑝, the outlet air temperature 𝑇𝑅 𝑜𝑢𝑡 (𝑡) corresponds to:

𝑇𝑅 𝑜𝑢𝑡 (𝑡) = 𝑇𝑅 𝑖𝑛 + 𝑄𝐷𝐶 (𝑡) 𝑚𝑎𝑖𝑟 × 𝐶𝑝 (3)
The cooling demand of the chiller 𝑄 𝑐𝑜𝑜𝑙𝑖𝑛𝑔 (𝑡) is defined as follows:

𝑄 𝑐𝑜𝑜𝑙𝑖𝑛𝑔 (𝑡) = 𝑄𝐷𝐶 (𝑡)/𝜂𝑐𝑐 (4)
With 𝜂𝑐𝑐, the inefficiency in the coil of the CRAH.

When the chiller stops working, the inlet and outlet air temperatures become equal and they start increasing according to the following equation:

𝑑𝑇𝑅 𝑜𝑢𝑡 𝑑𝑡 = 𝑄𝐷𝐶 (𝑡) 𝑚𝑎𝑖𝑟 × 𝐶𝑝 (5)
A boolean discrete variable 𝑝𝑜𝑤𝑒𝑟 determines the status of the power supply in DC1. It is initially set to 1 meaning that power supply is working. When the temperature reaches a critical threshold 𝑡𝑒𝑚𝑝𝑇 ℎ𝑟𝑒𝑠ℎ𝑜𝑙𝑑, the power supply is shut down -i.e. 𝑝𝑜𝑤𝑒𝑟 = 0. The following discrete equation models the behavior of the safety mechanism:

when 𝑇𝑅 𝑜𝑢𝑡 (𝑡) >= 𝑡𝑒𝑚𝑝𝑇 ℎ𝑟𝑒𝑠ℎ𝑜𝑙𝑑 then 𝑝𝑜𝑤𝑒𝑟 = 0 [START_REF] Camus | A Stochastic Approach for Optimizing Green Energy Consumption in Distributed Clouds[END_REF] The status of the chiller is modeled by a boolean variable 𝑐ℎ𝑖𝑙𝑙𝑒𝑟. The chiller is initially in state 1, meaning that it is working. When the load of the chiller reaches a critical threshold 𝑐𝑟𝑖𝑡𝑖𝑐𝑎𝑙𝐿𝑜𝑎𝑑, the failure occurs and the status of the chiller switches to 0, meaning that it stops working. This is modeled by the following discrete equation: when 𝑄 𝑐𝑜𝑜𝑙𝑖𝑛𝑔 (𝑡) >= 𝑐𝑟𝑖𝑡𝑖𝑐𝑎𝑙𝐿𝑜𝑎𝑑 then 𝑐ℎ𝑖𝑙𝑙𝑒𝑟 = 0 [START_REF] Camus | Hybrid Co-simulation of FMUs using DEV&DESS in MECSYCO[END_REF] The expected behavior of the system is that when the chiller is working, the inlet temperature remains constant and the load of the chiller varies with the power consumption of the computing units. When that computing load is too high, the chiller load will eventually reach the critical threshold, inducing a chiller failure. The room temperature will then increase with a rate proportional to the PMs' power consumption. Once the temperature reaches the critical threshold, the power supply is shut down, stopping all computing units.

Distributed application of the DC

We consider a scheduling algorithm which sequentially deploys Virtual Machines (VM) on the PM of the data center DC1, while another data center DC2 is used as a backup solution. The whole IT system is shown in Figure 2.

Each VM is a computer system emulation which requires a given amount of the computing resources (i.e. CPU and memory) of its PM to execute. When creating a VM, the user specifies its size -i.e the maximum amount of computing resources it can use on the PM. Thus, several VMs can run on a single PM with sufficient resources. We consider for the sake of simplicity that a VM always runs at full capacity The scheduler behavior corresponds to a simple first-fit algorithm (described by Algorithm 1). We consider that it takes 10 seconds to deploy a VM on a PM. PMs consume 0W when turned off. When turned on, we use the power consumption model of [START_REF] Li | Opportunistic Scheduling in Clouds Partially Powered by Green Energy[END_REF] which is based on real watt-meter measurements and consider a PM to consumes 97W when idle, 128W when using 1 core, and 220W when working at full capacity. As shown in Figure 3, the power consumption of a PM depends linearly on its CPU usage between 1 core used and max [START_REF] Heinrich | Predicting the Energy Consumption of MPI Applications at Scale Using a Single Node[END_REF]. As a consequence, with Algorithm 1 the power consumption of DC1 will increase with the number of deployed VMs. for pm1 in pmList2 do if pm1 as enough cores available to run vm then migrate vm on pm1 if pm0 is empty then shut down pm0 end if break end if end for end for A probe monitors the chiller status. When a failure is detected, the probe sends a message through an IP network to an emergency manager deployed in another DC called DC2. Upon reception, the emergency manager kills the scheduling algorithm to stop the deployment of VMs in DC1. It also immediately shuts down unused PMs to limit the room temperature. Then, the emergency manager relocate the VMs to DC2, to save as many as possible of them before the power supply shutdown. We perform live migrations of VM to ensure a continuity of service. With a live migration, the memory of a VM is progressively sent to the destination PM while the VM is running on the source PM. Once the transfer is done, the VM is shut down on the source PM and restarted on the destination PM. The time to migrate a VM strongly depends on the memory transfer time [START_REF] Akoush | Predicting the Performance of Virtual Machine Migration[END_REF]. The manager shuts down the PM once all its VMs are migrated. The behavior of the emergency manager is described by Algorithm 2.

The distributed application is then composed of several processes, namely the scheduling algorithm, the emergency manager processes, all the VM deployed on the PM, and the probe monitoring the chiller. We implement this application in SimGrid, and rely on its IT models of IP network, CPU usage and energy consumption for the simulation.

Co-simulation challenges

To study the considered use-case, we employ dedicated simulation tools: OpenModelica for the equation-based chiller failure model, and SimGrid for the distributed application and its power consumption over the DC. We need to couple our OpenModelica and SimGrid models as shown in Figure 4. The PM power consumption computed by SimGrid is used as input (i.e. 𝑃 𝑙𝑜𝑎𝑑 𝐷𝐶 (𝑡)) of the physical models of OpenModelica. On the other side, any change to the model's discrete variables (i.e. 𝑐ℎ𝑖𝑙𝑙𝑒𝑟 and 𝑝𝑜𝑤𝑒𝑟) triggers events in the distributed application.

This coupling rises the following issues:

• How to manage interoperability between OpenModelica and SimGrid ? • How to make the distributed application processes co-evolve with the physical system models ? • How to manage interactions between the computing processes and the physical models ? • How to detect discrete state changes in the continuous system evolution, and trigger the induced discrete events in the distributed application ?

In the following, we detail the FMI standard and the SimGrid platform that we want to combine to address these issues.

CONTEXT 3.1 The FMI standard

FMI [START_REF] Blochwitz | Functional mockup interface 2.0: The standard for tool independent exchange of simulation models[END_REF] aims at proposing a generic way to export, import and control equation-based models and their solvers. Using FMI, a model which may be composed of a mixture of differential, algebraic and discrete-time equations, can be exported under a standard format as an FMU. This FMU is a black-box (thus protecting the intellectual property of the model) with input and output ports which correspond to the input and output variables of the model. Each FMU can then be controlled FMI provides two ways of exporting and importing a model: FMI for co-simulation (FMI-CS) and FMI for model-exchange (FMI-ME). With FMI-ME (depicted in Figure 5), only the model (i.e. the equations) is exported. Thus an FMU-ME requires a numerical solver in order to be simulated. As a consequence, this export mode is mainly interesting in the context of model exchanges between equation-based tools, which is out of the scope of this article.

With FMI-CS (depicted in Figure 6), a model is exported with a passive solver that can be controlled by any M&S environment importing this FMU-CS. Because they do not require any external solver, FMU-CS can be integrated into a discrete M&S environments. This fits particularly well into our context of DCPS simulation. In the following, we detail this FMI-CS standard and its limits to make our proposition fully understandable for non-specialist.

The co-evolution of an FMU-CS with its environment is based on the concept of communication points. These communication points, which have to be set by the environment of the FMU, correspond to points in the simulated time where (1) the FMU simulation must be stopped, and (2) exchanges of data can be performed between the FMUs and its environment. Between two communication points, an FMU evolves independently of its environment.

From a software perspective, the FMU interface is composed of a set of C functions, and an XML file. The C functions control the FMU, whereas the XML file describes the FMU capacities and interface. More precisely, the XML file describes names, types (i.e. Real/Integer/Boolean/String), variability (constant/discrete/continuous) and causality (input/output/parameter) of the variables. The C interface enables to control an FMU-CS with the following operations [START_REF]Functional Mock-up Interface for Model Exchange and Co-Simulation -Version 2.0[END_REF]:

• a doStep integrates the FMU until a given communication point. Note that, an FMU may enforce fixed communication step-size. This limitation is then specified in the FMU description file. In this case, if the step-size required by doStep is not compatible with the fixed step-size, the method will fail to execute. • a getOutput gets the current outputs of the FMU.

• a setInput sets the inputs of the FMU. In case of instantaneous dependencies between inputs and outputs, this method may change the outputs of the FMU. Depending on the FMU, a doStep of duration 0 may also be required to update outputs. • getState and setState are optional operations used to export/import the model state. They enable to perform a rollback during the simulation of the model. In its current state, FMI-CS is not yet fully compliant with hybrid simulation requirements [START_REF] Broman | Determinate Composition of FMUs for Co-simulation[END_REF][START_REF] Cremona | FIDE -An FMI Integrated Development Environment[END_REF][START_REF] Tavella | Toward an Hybrid Co-simulation with the FMI-CS Standard[END_REF]. In particular, an FMU only supports continuous and piecewise continuous input/output time signals. As a consequence, an FMU-CS cannot produce discrete event signals which are essential to communicate with event-based models. Also, the date of the next discrete event cannot be obtained from a FMU-CS. Although the scheduled 2.1 extension of the standard might solve this issue2 , we need to adapt to this constraint in the meantime.

In the model of our use-case, we use FMI-CS to export our thermal system model as an FMU using the dedicated features of OpenModelica. Thus, we obtain a simulation unit (shown in Figure 7) which is ready to interact and co-evolve with other models in different M&S environments. However, due to the limitation of the standard, the exact dates of the power supply shutdown and the chiller failure cannot be known in advance from the FMU. Also, the FMU is not able to trigger an event at these moments to notify the distributed application.

The SimGrid Platform

SimGrid [START_REF] Casanova | Versatile, Scalable, and Accurate Simulation of Distributed Applications and Platforms[END_REF] is a versatile platform dedicated to the scalable simulation of distributed applications and platforms. It can notably be used to study cluster, grid, peer-to-peer, Cloud, wide/local-area networks. It is grounded on sound simulation models of CPUs [START_REF] Velho | Accurate and Fast Simulations of Large-Scale Distributed Computing Systems[END_REF], TCP/IP networks [START_REF] Velho | On the Validity of Flow-level TCP Network Models for Grid and Cloud Simulations[END_REF], VMs [START_REF] Hirofuchi | SimGrid VM: Virtual Machine Support for a Simulation Framework of Distributed Systems[END_REF], and energy consumption [START_REF] Heinrich | Predicting the Energy Consumption of MPI Applications at Scale Using a Single Node[END_REF] which are theoretically sound and experimentally assessed. Using these models, SimGrid accurately simulates the resources usage (i.e. CPU and bandwidth sharing), the execution time and the energy consumption of a distributed application code. Thus, platform enables to simulate the behavior of a distributed system on a singlecomputer. SimGrid has grounded over 200 scientific works. SimGrid is implemented in C/C++ and available in open source at http://simgrid.org.

The SimGrid models are used to determine:

(1) how much computing resources are allocated to each action of the distributed application, e.g. how much bandwidth is used by each data transfer. (2) when each action ends, e.g. when do the data transfers end.

The SimGrid models are based on the discrete event paradigm, where an internal event corresponds to the completion of an action. Each model can be controlled using two operations:

• updateModel() updates the model to the current simulated time. • nextEvent() get the of the next internal event of the model.

SimGrid compartmentalizes the execution of the distributed processes to strictly manage their co-evolution and interactions with the models. This design, where each interaction of the processes with their environment is strictly mediated by a kernel is highly inspired from the classical design of an Operating System. To that extend, SimGrid gives a dedicated execution context to each process of the distributed application. These execution contexts can be implemented either with classical threads or with lighter continuations [START_REF] Appel | Continuation-passing, Closurepassing Style[END_REF] mechanisms. This architecture, depicted in Figures 8 and9, was first introduced to enable the parallel execution of the user processes [START_REF] Quinson | Parallel Simulation of Peer-to-Peer Systems[END_REF] without relying of fine-grain locking of the simulator internals. It also enables the formal verification of legacy distributed applications, since their interactions with their environment are strictly controlled by the framework when they run within the simulator [START_REF] Pham | Verifying MPI Applications with SimGridMC[END_REF].

During a typical SimGrid simulation, all user processes are conceptually executed in parallel (in practice, parallelism can be disabled on user request). A simulation kernel, which has its own execution context, is in charge of:

(1) managing the simulation state (e.g. the simulation clock), (2) coordinating the processes and models' executions, and (3) mediating interactions between user code and models. Some process actions can modify the state of a model. In our use case, examples of such actions include: starting a VM, sending data through the network, using CPU, migrating a VM and turning off a PM. When a process wants to perform an action that modifies the state of a model, it needs to use the simcall mechanism of the kernel. This mechanism is the equivalent of a system call in a classical OS. It causes the process to be blocked until the requested action ends in the simulation. As a consequence (1) the simulation clock may change between the time when a process is blocked and resumed by a simcall, and (2) every process computation that occurs between two simcalls are considered to be instantaneous in the simulated time.

When all processes are blocked at given simulation time, a context switch is performed to the kernel in order to move forward simulation time. The kernel first sequentially (and in a deterministic order) changes the models' states according to the requests made by the processes. Then, following a discrete event logic, it synchronizes the models and processes executions by:

(1) calling the nextEvent method of each model in order to determine the time of the earliest internal event;

(2) updating the simulation clock and sequentially calling the updateModel method of all the models in order to move forward the simulation to the earliest internal event time; (3) eventually resuming the processes whose simcalls ends.

This step cause a context switch to the processes.

The Figure 8 summarizes this simulation behavior. Thanks to this unique model of execution, SimGrid can mix simulation models with distributed application code in order to perform scalable and deterministic simulation. We propose to take advantage of this feature in our context of DCPS simulation, by embedding each FMU-CS into a dedicated SimGrid model. In the following, we detail this proposition.

CONTRIBUTION

As shown in Figure 10, our approach is to import FMU-CS into a dedicated model which is added in the SimGrid simulation kernel. The kernel can then control the FMU like any other model. Note that with this mechanism, several FMUs can be imported in SimGrid, each of them being associated with a dedicated model. All the FMUs can then interact separately with the distributed application processes.

In traditional discrete event and multi-physical equationbased tools, such as an FMU co-simulation master, or Open-Modelica, the input/output connections between an FMU and its environment are determined a priori at the model design time. Moreover, these links are in general hardwired and cannot be changed at run-time. In order to integrate FMU-CS in the SimGrid environment, we use a more flexible interaction mechanism which can handle the complexity of concurrent program behavior. Indeed, any of the computing processes is likely to interact with an FMU. Moreover, some of these processes may be created or killed during the simulation. As a consequence, with some complex concurrent code, it is very difficult -if not impossible-to determine a priori the interactions between each process and an FMU.

In the following, we detail how the FMU execution is coordinated with the distributed application (Section 4.1), how FMUs and distributed programs interact (Section 4.2), and how we overcome the FMI-CS limitation in terms of hybrid simulation (Section 4.3).

We rely on FMI++ [START_REF] Widl | The FMI++ library: A high-level utility package for FMI for model exchange[END_REF] to implement our solution. This library provides high-level functionalities to load and manipulate FMUs in order to ease their integration in discrete simulation tools.

Coordination of FMU and distributed application

When the updateModel method of this SimGrid model is called by the kernel, it performs a doStep in order to move forward the FMU to the desired simulation time. This mechanism enables then to coordinate the simulations of the FMU and the distributed application.

In order to simulate our use-case, we can then import the FMU of our thermal system model in SimGrid. The thermal system will then co-evolve with the distributed application running in the data-centers.

Note that, as the SimGrid kernel performs discrete event simulations, our synchronization mechanism requires the FMU to support variable communication step-sizes. To handle an FMU that does not comply with this constraint, we can use the dedicated FixedStepSizeFMU wrapper of FMI++. This wrapper, implements a fixed step-size simulation algorithm that positions the FMU as close as possible to the required communication point. This may induce inaccurate results as the model synchronization is not perfectly done. However, this inaccuracy is inherent to fixed-step size simulation models.

Continuous input and output interactions

To enable flexible interactions between the FMUs and the distributed applications, we make all the input and output ports of all the FMUs imported in SimGrid accessible to all the running processes. We extend the SimGrid API with two methods that can be used by the processes in order to interact with the FMUs:

• getReal/Integer/Boolean/String(string name) returns the current value of the variable name. sets the value of the variable name to value. If needed, the doStep parameter can be set to true in order to perform a doStep of duration 0 to update the FMU outputs. As it modifies the state of the FMU -which is now considered as a SimGrid model-this function triggers a SimGrid simcall. The inputs of the FMU is then set within the kernel context of SimGrid in order to maintain a deterministic simulation execution. This simcall ends at the same simulation time, making the set operations instantaneous from the simulation point of view. In our use-case, we use these methods to update the PM power consumption in the FMU with the value computed by SimGrid. The Algorithms 3 and 4 show how we easily extends the Algorithms 1 and 2 for this purpose. We also design a simple sampling process behavior (shown in Algorithm 5) to observe the continuous state trajectory of the FMU (i.e. the evolution of the temperature in DC1) during the simulation.

Algorithm 3: Extension (in red) of the scheduling algorithm in order to interact with the FMU.

while DC1 is not full do Let pmList be the list of PM of DC1.

for pm in pmList do if pm as enough cores available to run a VM then deploy VM on pm Let 𝑝 be the current power consumption of DC1. setReal("𝑃 𝑙𝑜𝑎𝑑 𝐷𝐶 ",𝑝) break end if end for end while

discrete event interaction

In order to comply with the requirements of hybrid modeling, we have to overcome the limitations of FMI-CS in terms of discrete event behavior (introduced in Section 3.1). We design an event triggering mechanism which emulates discrete event output signals from the continuous output of the FMU. Thanks to this mechanism, discrete changes in the FMU (e.g. the chiller failure and power supply shutdown in our use case) can then be notified to the distributed application.

We extend the SimGrid API with the following method:

registerEvent(bool (*condition)(vector<string>), void (*callback)(vector<string>), vector<std::string> parameters)

This method registers an event notification request to the SimGrid model that embeds the FMU. This mechanism enables flexible interactions between the FMU and the distributed application since any process of the distributed application can use it at any simulated time. Moreover, each process is free to specify in which conditions the event occurs by specifying the condition function. Each process also sets Algorithm 4: Extension (in red) of the emergency algorithm to interact with the FMU.

wait for emergency message shutdown unused PM in DC1 Let 𝑝 be the current power consumption of DC1. setReal("𝑃 𝑙𝑜𝑎𝑑 𝐷𝐶 ",𝑝) Let deployedVM be the list of all VM deployed on DC1.

for vm in deployedVM do Let pm0 be the PM of vm.

Let pmList be the list of PM of DC2. for pm1 in pmList2 do if pm1 as enough cores available to run vm then migrate vm on pm1 if pm0 is empty then shutdown pm0 end if Update 𝑝. setReal("𝑃 𝑙𝑜𝑎𝑑 𝐷𝐶 ",𝑝) break end if end for end for Algorithm 5: sampling algorithm which monitors the temperature evolution.

while true do double temp = getReal("𝑇𝑅 𝑜𝑢𝑡 ") save the value of temp in output log wait x seconds end while what is its impact on the distributed application by specifying the callback method. For instance, this effect can range from simple logging activity to process kill, creation, resuming or suspending. When executed, both condition and callback receive parameters as input.

Each time registerEvent is called by a process, an instantaneous simcall, in terms of simulated time, is triggered to ensure a deterministic simulation, and the event notification request is stored in the SimGrid model which contains the FMU. The event conditions are evaluated immediately and after each modification of the FMU state -i.e. after each call to setReal/Integer/Boolean/String and updateModel. When the condition is satisfied, the associated callback function is executed to propagate the event effect in the distributed application. The event notification request is then deleted (but note that the callback function is free to register another similar request).

When at least one event notification request is pending, we use a classical lookahead exploration strategy in order to accurately determine the occurrence time of events. This strategy, shown in Figure 11, consists in scheduling internal events at regular intervals (using the nextEvent method of the SimGrid model) in order to frequently check if an event has occur in the FMU. The fixed delay between these intervals corresponds to the lookahead of the model. It is determined by the user at the FMU import time. Setting the lookahead is about finding a trade-off between accuracy and performance, as both determine the event detection precision, and the frequency of event checks. A known limitation of this strategy is that it may miss some event occurrences if the lookahead is too large (as shown in Figure 12). We could have used other event detection algorithms that may be more accurate and efficient (like bisectional search, regular falsi or the Illinois algorithm [START_REF] Moler | Are We There Yet? Zero Crossing and Event Handling for Differential Equations[END_REF]). However, these strategies are less generic as they are only compliant with FMUs which implement the optional rollback features [START_REF] Camus | Co-simulation of cyber-physical systems using a DEVS wrapping strategy in the MECSYCO middleware[END_REF]. As soon as there are no pending event notification requests, the SimGrid model containing the FMU stops scheduling internal events.

Getting back to our use-case, we can use this mechanism to handle the events related to the chiller failure and the power supply shutdown. The behavior of the probe that waits for the chiller failure and sends a message to the emergency manager is formalized by the Algorithm 6. This algorithm uses a zeroValue condition function that returns true when the 𝑐ℎ𝑖𝑙𝑙𝑒𝑟 output variable of the FMU is equal to 0, and a wakeMeUp callback function that simply resumes the probe process execution. In order to manage the power supply shutdown, we register an event notification at the beginning of the simulation with a condition function that detects when 𝑝𝑜𝑤𝑒𝑟 = 0, and a callback function that creates the PM shutdown process.

EVALUATION

To evaluate our solution, we perform the co-simulation of our use-case and study the simulation results. In the following, we detail how we validate our solution. We first describes Algorithm 6: algorithm of the probe detecting chiller failure.

registerEvent(zeroValue,wakeMeUp,nullptr) suspend the execution of this process send the message to the emergency manager our experimental scenario in Table 1. Then, we detail and interpret the simulation results in Section 5.1. Finally, we detail our validation process in Section 5.2.

Results interpretation

Figure 13 shows the simulation results of our co-simulation with SimGrid: the power consumption of the system, the temperature of DC1, the status of the chiller, and the power supply over time. We can see that from simulation time 0 to time 260, the power consumption of DC1 (computed by SimGrid) and the chiller load (computed by the FMU-CS) increase progressively. This is due to the scheduling algorithm (Algorithm 1) that is deploying VM every 10 seconds.

At time 260, the chiller load exceeds the critical load of 23,000 W and the chiller stops functioning. As a consequence, the chiller load falls immediately down to 0, the temperature starts increasing, and the probe sends a message to notify this issue. After a transmission delay simulated by the TCP model of SimGrid, this message is received at time 260.263 by the emergency manager (Algorithm 2) which immediately shutdowns the unused PM in DC1. As a consequence, the power consumption of DC1 decreases suddenly from 17,310 W to 9,668.8 W.

Then, from time 260.263 to time 846.614, the emergency manager migrates VMs from DC1 to DC2. This causes an increase of the power consumption of DC2 and a decrease of the power consumption of DC1. Note that the power consumption of DC1 changes at a faster rate than the power consumption of DC2. This is due to the PM shutdowns performed by the emergency manager in DC1. We can see that, by transferring the computation load from DC1 to DC2, the emergency manager progressively limits the temperature increase in DC1. However this is not sufficient and, at time 846.614, the temperature reaches the critical threshold of 40°C and the power supply of DC1 is shut down. This event is successfully propagated to SimGrid as all the PMs are immediately turned off and the total power consumption rapidly reaches 0. These results are in complete accordance with the expected behavior.

Validation

As shown in Figure 14, to validate this co-simulation, we compare these results with the trajectory generated by a monolithic simulation performed with OpenModelica. As it is not possible to model and simulate our IT system in Modelica, we use the power consumption traces generated by SimGrid as input of OpenModelica. We found similar simulation results. Because it immediately depends on the PM power consumption, the chiller failure occurs at the exact same simulation time. The power shutdown occurs less than 0.001 second earlier in the OpenModelica simulation. This is accordance with our expectations because it corresponds to the event detection precision (i.e. the lookahead) that we set in our co-simulation.

In order to test our capacity to handle several FMUs, we split our physical model into two FMUs. The first FMU embeds the equation 7 and corresponds to the chiller failure model. The second FMU contains the other equations of the physical model. We modify the Algorithm 3 and 4 to update the two FMU inputs. The event notification request related to the chiller failure (resp. power supply shutdown) is now registered in the first (resp. second) FMU. The co-simulation results obtained are again similar to the monolithic simulation. Therefore, these experiments demonstrates the validity of our solution.

CONCLUSION

In this article, we detailed how FMU-CS are integrated into the SimGrid platform in order to manage the co-simulation of multi-physical models and concurrent programs. Our contribution consists in embedding FMUs into a dedicated SimGrid model. We proposed an extension of the SimGrid API that enables flexible interactions between FMU and concurrent program. In particular, we defined a dynamic generation mechanism of discrete event signals that overcomes the limitations of FMU in terms of hybrid simulation. We experimentally validated our solution by demonstrating that our co-simulation of a chiller failure in a data-center gives similar results when compared to a monolithic simulation.

From a software perspective, it is important to note that our solution does not require any extension of the SimGrid simulation kernel. It corresponds then to a SimGrid plug-in. All our code is open-source and it will be soon integrated in the SimGrid distribution.

Our solution has several advantages: • versatility: we can import models from the numerous multi-physical M&S tools that support the FMI-CS standard. Also, we benefit from the validated IT models of SimGrid and its diversity of application contexts. Thus, FMU-CS can now interact with Grids, Clouds, High Performance Computing infrastructures or Peerto-Peer systems. • reproducibility: we benefit from the OS-based simulation architecture of SimGrid that ensures deterministic co-simulation between FMUs and concurrent programs. • scalability: thanks to the optimized model of execution of SimGrid, FMU-CS can simultaneously interact with a very large amount a concurrent processes.

A limit of our approach is that we rely on a lookahead algorithm to detect event occurrences in the FMU. This strategy may be less efficient and accurate than other algorithms of the literature but it is more generic in term of FMU integration. Also, we are able to import simultaneously several FMUs into SimGrid and make them interact with concurrent processes. However, the potential interactions between these FMU have to be handled in an ad-hoc way. Considering the complexity of FMU interactions which often require numerical methods (e.g. algebraic loop resolution, numerical error estimation) a more generic and automatic solution is required.

In future work, we plan to extend our proposition in order to integrate tools that support the FMU-ME standard. We also plan to implement other event-detection algorithms to increase the accuracy and performance of our co-simulations. As soon as they will be available, we want to take advantage of the new FMI 2.1 extensions for hybrid simulation. Finally, we plan to use this work in order to simulate green computing systems where Smart-Grid models interact with distributed cloud infrastructures.

Figure 1 :

 1 Figure 1: Physical model of the data-center.

Figure 2 :

 2 Figure 2: IT model of the data-centers.

Figure 3 :

 3 Figure 3: Consumption model of the PM.

Algorithm 1 :

 1 Scheduling algorithm to deploy VM in DC1 while DC1 is not full do Let pmList be the list of PM of DC1. for pm in pmList do if pm as enough cores available to run a VM then deploy VM on pm break end if end for end while(a) Global system studied. (b) Data exchanges between SimGrid and OpenModelica (OM)

Figure 4 :

 4 Figure 4: Co-simulation of the chiller failure.

Figure 5 :

 5 Figure 5: FMI for model-exchange.

Figure 6 :

 6 Figure 6: FMI for co-simulation.

Figure 7 :

 7 Figure 7: Block diagram view of the thermal system model of our use-case, exported as an FMU.

Figure 8 :

 8 Figure 8: Example of simulation execution in Sim-Grid (according to the real time).

Figure 9 :

 9 Figure 9: Simulation architecture of SimGrid.

Figure 10 :

 10 Figure 10: Integration of FMU into the simulation architecture of SimGrid.

Figure 11 :

 11 Figure 11: Example of event detection with the lookahead strategy.

Figure 12 :

 12 Figure 12: Example of undetected event occurrence with the lookahead strategy.

Figure 13 :

 13 Figure 13: Simulation results of the use-case.

Figure 14 :

 14 Figure 14: Validation process.

Table 1 :

 1 Experimental conditions.

	Domain	Parameters	Value
		inlet air temperature 𝑇𝑅 𝑖𝑛	24	°C
		mass of the air in the room 𝑚𝑎𝑖𝑟	294 kg
		specific heat	1.006 kJ/kg
	Physical system model	cooling inefficiency	0.9
		chiller critical load 𝑐𝑟𝑖𝑡𝑖𝑐𝑎𝑙𝐿𝑜𝑎𝑑	23 kW
		temperature threshold 𝑡𝑒𝑚𝑝𝑇 ℎ𝑟𝑒𝑠ℎ𝑜𝑙𝑑	40	°C
		ratio of the other devices in the total DC heat dissipation	0.2
		number of PM in each DC	129
		PM core size	12
		PM maximum power consumption	220 W
		PM power consumption when using 1 core	128 W
	IT model	PM idle power consumption	97 W
		PM off power consumption	0 W
		VM RAM size	3 Go
		VM core size	6
		VM deployment time (i.e. delay between two deployments)	10 sec
	Co-simulation	lookahead value (i.e. event detection precision)	0.01 sec

according to http://fmi-standard.org/downloads/ as of 24. Jan 2018.