Chukri Soueidi
email: chukri.a.soueidi@inria.fr

Yliès Falcone
email: ylies.falcone@inria.fr

Residual Runtime Verification via Reachability Analysis

Keywords: Residual Runtime Verification, Instrumentation, Parametric Monitoring, Control Flow, Runtime Overhead, Bad prefix

We leverage static verification to reduce monitoring overhead when runtime verifying a property. We present a sound and efficient analysis to statically find safe execution paths in the control flow at the intra-procedural level of programs. Such paths are guaranteed to preserve the monitored property and thus can be ignored at runtime. Our analysis guides an instrumentation tool to select program points that should be observed at runtime. The monitor is left to perform residual runtime verification for parts of the program that the analysis could not statically prove safe. Our approach does not depend on dataflow analysis, thus separating the task of residual analysis from static analysis; allowing for seamless integration with many RV frameworks and development pipelines. We implement our approach within BISM, which is a recent tool for bytecode-level instrumentation of Java programs. Our experiments on the DaCapo benchmark show a reduction in instrumentation points by a factor of 2.5 on average (reaching 9), and accordingly, a reduction in the number of runtime events by a factor of 1.8 on average (reaching 6).

Introduction

Runtime verification (RV) [START_REF] Bartocci | Introduction to runtime verification[END_REF][START_REF] Havelund | Verify your runs[END_REF][START_REF] Leucker | A brief account of runtime verification[END_REF][START_REF] Falcone | A tutorial on runtime verification[END_REF][START_REF] Falcone | A taxonomy for classifying runtime verification tools[END_REF] is a formal method that allows checking whether a run of a system respects a specification. The specification usually formalizes a correctness property and is written in a suitable formalism based for instance on temporal logic or finite-state machines. There are still many challenges in runtime verification, see [START_REF] Sánchez | A survey of challenges for runtime verification from advanced application domains (beyond software)[END_REF] for a survey. One of the most prominent and fundamental ones, hindering its wide applicability in application domains, is the runtime overhead introduced when augmenting a system with runtime verification. Overhead is caused by the instrumentation code inserted in the program to generate traces. In the case of online monitoring, overhead also comprises the evaluation of traces by the monitors.

RV can complement and has been used in combination with other formal static verification methods such as model checking [START_REF] Leucker | Sliding between model checking and runtime verification[END_REF], deductive verification [START_REF] Chimento | Starvoors: A tool for combined static and runtime verification of java[END_REF] and static analysis [START_REF] Dwyer | Residual dynamic typestate analysis exploiting static analysis p[END_REF][START_REF] Bodden | Clara: A framework for partially evaluating finitestate runtime monitors ahead of time[END_REF][START_REF] Chimento | Starvoors: A tool for combined static and runtime verification of java[END_REF][START_REF] Azzopardi | Clarva: Model-based residual verification of java programs[END_REF], as well as informal dynamic methods such as testing [START_REF] Chimento | Testing meets static and runtime verification[END_REF] and debugging [START_REF] Jakse | Interactive runtime verification -when interactive debugging meets runtime verification[END_REF]. While a complete a priori verification is ideally desirable for verifying program correctness, proving the correctness of many properties is fundamentally undecidable statically. However, static verification often relies on conservative approximations that produce sound results while sacrificing completeness. Combining static and runtime verification for a more complete verification scheme seems natural. The combination is useful in the two complementary directions. For static verification, it improves completeness by deferring verification of undecidable fragments for some properties until runtime. For RV, it reduces the overhead of monitoring by pruning parts of the program that can be statically analyzed. In this paper, we pursue the second direction.

We follow the terminology of [START_REF] Dwyer | Residual dynamic typestate analysis exploiting static analysis p[END_REF] and refer to the introduced technique as residual runtime verification. Our work is directed to handle properties that can be expressed by finite-state automata, such as typestate [START_REF] Strom | Typestate: A programming language concept for enhancing software reliability[END_REF] errors, supporting different formalisms and monitoring approaches that allow specifications with data. In such approaches, a parametric monitor receives a parametrized trace and spawns multiple monitors for different trace slices corresponding to sets of related objects [START_REF] Havelund | Monitoring Events that Carry Data[END_REF]. We see our contributions as follows. We present a sound and efficient technique to statically find "safe" execution paths in the control flow at the intra-procedural level of programs. Such paths are guaranteed to preserve the monitored property and thus can be ignored at runtime. As a result, the monitor is left to perform verification for residual parts of the program that the analysis failed to prove safe statically. Our approach, at its core, does not depend on data-flow analysis nor on a static construction of the full call graph of the program, which might be difficult and expensive to produce in practice. Thus, we separate the problem of static analysis from the residual analysis, allowing for seamless integration with the RV workflow. Instead, we analyze the control-flow graphs of single methods and rely on over-approximations of the behavior of the program. We assume that the variables generating events within one method may-alias and our analysis reasons about all possible projections of traces. We also handle instructions that may allow references to escape from methods by including them in the analysis to guarantee soundness. We demonstrate the effectiveness of our analysis when we reduce the number of instrumentation points by a factor of 2.5 on average (reaching 9), and accordingly, the number of generated events at runtime by a factor of 1.8 on average (reaching 6). Our approach is fully implemented as an extension of the instrumentation tool BISM [START_REF] Soueidi | BISM: Bytecode-Level Instrumentation for Software Monitoring[END_REF], and [START_REF] Soueidi | Capturing program models with bism[END_REF] where we presented the control-flow graph automaton, a model to abstract the program behavior at the intra-procedural level.

The rest of this paper is structured as follows. Section 2 motivates our approach with a running example. Section 3 reviews background notions. Section 4 defines the requirements for residual analysis. Section 5 describes our instantiation of residual analysis at the interprocedural level. Section 6 briefly overviews our implementation. Section 7 reports on our experiments. Section 8 reviews the related research focusing on residual analysis. Section 9 concludes and presents perspectives.

Motivating Example and Approach Overview

We first introduce our running example. We are interested in monitoring the SafeIterator property which specifies that "A collection should not be updated when an iterator associated with it is created and being used". Figure 1, shows a contrived Java method m along with its control-flow graph (CFG). It retrieves 2 lists (lines 3,4), updates them (lines 6,10,11), creates iterators (lines 7,15), and calls the "next" method on the iterator (line 14). We are interested in answering the following questions:

-Q1: Can we fully verify this program statically? If yes, then there is no need to instrument and runtime monitor it. is only decidable at runtime. To generally decide Condition (2) statically, we need to perform pointer analysis on the program that checks all calling contexts m and return whether l1 and l2 alias. In practice, we may get one of the following results about our query: the two objects must-alias, may-alias, or must-not-alias. Moreover, pointer analysis often times out and never returns a result. However, to answer Q1, we need to get the result that l1 and l2 must-not-alias, i.e., they refer to different objects in memory. This is a sufficient condition to statically ensure that m will behave correctly at runtime regardless of the control flow since the update actions on Lines 10-11 are not on the list iterated by iterator it. To answer Q2, by observing Lines 15-16, we can see that, regardless of what happens at execution, these two instructions are safe and their execution does not need to be monitored. Also, in Line 6, the instruction is safe since it updates the list before the creation of the iterator. Pointer analysis may not always conclude with a result, especially for Java programs. In addition to the inability to construct the full static call graph of the program, Java allows for dynamic class loading and reflection which often cause additional problems to pointer analysis. Our work relies on the idea that when statically analyzing cases such as the one of Condition (2), one can safely assume that such two variables mayalias, even without performing pointer-analysis. Also, we analyze methods separately and thus need to handle escaping references. Objects in the program that are relevant to the property may escape from the method to a subroutine or a return statement and produce events there. As such, we handle all instructions that may allow references to escape, such as method calls, with special escape events.

Our over-approximation might miss some positive answers to Q1, therefore missing some optimization opportunities. However, based on our observation (such as the experiments in Sec. 7), cases where one needs to perform pointer analysis such as in Condition (2) are less frequent in many Java programs. As such, our approach mainly addresses Q2 while it is also capable of answering Q1 but, in certain cases, less effectively.

Background

We recall concepts related to monitoring in general and our verification approach in particular. We assume basic familiarity with automata theory such as the definitions of a finite-state machine, words, runs, and acceptance, and refer to [START_REF] Hopcroft | Introduction to Automata Theory, Languages, and Computation[END_REF] for more details.

Monitoring

Let Σ be a set of events, Σ * and Σ ω are the sets of all finite and infinite traces over Σ, respectively. A finite trace is a sequence of events, a word in Σ, that can be modeled by a function t : [1, n] → Σ for a trace of length n. We say that an event belongs to the trace, noted e ∈ t, when e ∈ codom(t). A property ϕ is a language over Σ which is a subset of Σ * . Given a trace t in Σ * , the set of prefixes of t, noted pre(t), is defined as: pre(t) = {p ∈ Σ * | ∃s ∈ Σ * : t = ps}. The set of matching prefixes is the set of prefixes of a trace within a given language L. Definition 1 (Matching prefixes [START_REF] Bodden | Partially evaluating finite-state runtime monitors ahead of time[END_REF]). Given a language L ⊆ Σ * and a trace t ∈ Σ * , the matching prefixes of t in L is given by: match L (t) = pre(t) ∩ L.

Many monitoring techniques and approaches essentially rely on the detection of bad and good prefixes, which are intuitively the witnessing sequences allowing a monitor to conclude about monitoring the program based on the trace observed so far.

Definition 2 (Bad/Good prefixes [START_REF] Kupferman | Model checking of safety properties[END_REF]). Given a language L ⊆ Σ * of finite traces over Σ (or of infinite traces,

L ⊆ Σ ω ). A finite trace u ∈ Σ * is a bad prefix for L, if ∀w ∈ Σ * : uw / ∈ L (or ∀w ∈ Σ ω : uw / ∈ L, if L is over infinite traces). Moreover, u is a good prefix for L, if ∀w ∈ Σ * : uw ∈ L (or ∀w ∈ Σ ω : uw ∈ L, if L is over infinite traces).
The languages of bad and good prefixes are extension-closed; since every continuation of a bad or a good prefix for a language, L, by a finite word is also a bad (good) prefix for L. When monitoring at runtime, we are interested in reporting a violation/satisfaction of a property from a trace as early as possible. Matching a bad (alternatively good) prefix is sufficient to produce a final verdict since every continuation of the trace will produce the same result. For instance, the techniques in [START_REF] Bauer | Runtime verification for LTL and TLTL[END_REF][START_REF] Falcone | What can you verify and enforce at runtime?[END_REF] synthesize a monitor (as a finite-state automaton) that recognizes the good and bad prefixes of the language denoted by a temporal-logic formula or by an automaton over infinite traces. Example 1 (SafeIterator monitor). Figure 2 shows the monitor that checks for the violation of the property from Sec. 2. Event c denotes a creation of an iterator associated with a list by calling list.iterator(), event u denotes an update on a list by calling list.add(..), and event n denotes calling the next method iterator.next() on an iterator. The monitor recognizes the bad prefixes in the traces received from a running program. Note that the monitor reaches the accepting state when seeing the pattern c.n * .u + .n, as it suffices to conclude that the whole run violates the property.

Definition 3 (Property satisfaction). We say that a trace t ∈ Σ * , satisfies a property ϕ ⊆ Σ * denoted by t |= ϕ iff t ∈ ϕ. Alternatively, for a safety property ϕ with its language of bad-prefixes L, t |= ϕ iff match L (t) = ∅. And, for a co-safety property ϕ with its language of good-prefixes L , t |= ϕ iff match L (t) = ∅.

Parametric Monitoring

Monitoring is in practice performed on parametric monitors that receive events accompanied by runtime information about the objects producing them, allowing to monitor each related set of objects in the program separately. There is a myriad of different approaches to parametric monitoring that differ in the manner they interpret events with runtime information and project these to instances of monitors. See [START_REF] Chen | Parametric trace slicing and monitoring[END_REF][START_REF] Barringer | Quantified event automata: Towards expressive and efficient runtime monitors[END_REF] for example approaches and [START_REF] Havelund | Monitoring events that carry data[END_REF][START_REF] Falcone | A taxonomy for classifying runtime verification tools[END_REF] for overviews. Here, we sketch a simple and general approach to parametric monitoring that can be adapted to several existing approaches. We denote the set of variables defined by a parametric monitor by X , and the set of values that these variables can take by V . These values usually correspond to objects in the memory of the execution environment of the program. A variable binding θ : X V maps monitor parameters to their values and B is the set of all possible bindings in a program. A parametric event e θ is then a pair (e, θ) ∈ Σ × B. We denote the set of all parametric events as Σ X and a parametric trace as a word in Σ X * .

Example 2 (Parametric traces). One trace that the program from Figure 1 may generate at runtime is the following:

τ = (u, [l → o(l1)]) (c, [l → o(l1), i → o(it)]) (u, [l → o(l2)]) (u, [l → o(l2)]) (n, [l → o(l1), i → o(it)]) (c, [l → o(l1), i → o(it)]) (u, [l → o(l2)]). The event (c, [l → o(l1), i → o(it)]
) denotes the creation of an iterator, event c, where the variable l, representing the associated list, is bound to the runtime object of l1 denoted by o(l1) and the variable i, representing the created iterator, is bound to the runtime object of it denoted by o(it).

A parametric property ΛX .ϕ (notation borrowed from [START_REF] Chen | Parametric trace slicing and monitoring[END_REF]) is then defined over traces of parametric events such that ΛX .ϕ ⊆ Σ X * . To monitor each group of related objects separately, a parametric monitor slices a parametric trace according to the values bound to the monitor parameters carried within events. Slicing is achieved by projecting a trace τ on all seen bindings using a projection function denoted by τ ↓ θ . We omit the formal details here for brevity. The projection results in a set of traces, we refer to as projected traces, where each trace contains non-parametric events that correspond to related objects in the program and is sent to a monitor that was spawned specifically for that slice.

Definition 4 (Projected traces).

Given a parametric trace τ in Σ X * , the set of projected traces is denoted by Proj (τ ) ⊆ Σ * , and is defined as:

Proj (τ ) = θ ∈ B τ ↓ θ
Example 3 (Projected traces). Consider τ from Ex. 2. A parametric monitor will check at runtime the relation between o(l1) and o(l2)1 then accordingly produce

Proj (τ ) = {ucuuncu} if o(l1) = o(l2) or Proj (τ ) = {ucnc, uuu} if o(l1) = o(l2).
Definition 5 (Parametric property satisfaction). A parametric trace τ ∈ Σ X * satisfies a parametric property ΛX .ϕ denoted by:

τ |= ΛX .ϕ def = ∀t ∈ Proj (τ ) : t |= ϕ

Upward Closure

We recall the notions for subwords and their closures for regular languages. We refer to [START_REF] Karandikar | On the state complexity of closures and interiors of regular languages with subwords and superwords[END_REF] for full details and borrow their definitions. For a word x ∈ Σ * , the length of x is denoted by |x|, and for 1 ≤ i ≤ |x|, let x i denote the i-th letter of x. We denote the empty word by . A subword is obtained by removing certain letters from a word at arbitrary positions, and, a superword is obtained by inserting any number of letters into a word at arbitrary positions. We say that a word x is a subword of y, denoted by x y, equivalently y is a superword of x when there are positions 0 < p 1 < p 2 < . . . p l ≤ |y| such that x[i] = y[p i ] for all 1 ≤ i ≤ l = |x|. For Σ = {a, b, c}, we have ε ab acba. Definition 6 (Upward closure of a language). For a language L ⊆ Σ * , the upward closure of L, is denoted by ↑L and defined as {x ∈ Σ * | ∃y ∈ L : y x}.

For any language L ⊆ Σ * , we have L ⊆ ↑L. Moreover, a language L is upwardclosed if L = ↑L. For a regular language L recognized by a non-deterministic finitestate automaton (NFA), we can obtain an NFA recognizing ↑L by simply adding transitions without increasing the number of states. More precisely, given an automaton

A = (Σ, Q, δ, Q 0 , F ) recognizing L, the NFA A ↑ = (Σ, Q, δ , Q 0 , F ) recognizing ↑L
is obtained by adding a self loop on every state q ∈ Q and every letter s ∈ Σ such that δ = δ ∪ { q, s, q | q ∈ Q, s ∈ Σ}.

Programs, CFG and Instrumentation

Given a program P , let Methods be the set of all its methods, Instructions the set of all byte-code instructions, and Instructions m all instructions of a method m. The CFG m = B m , E m of m is a directed graph, where B m is the set of nodes such that each instruction is a node, and E m ⊆ B m × B m are edges that connect nodes to their successors. The instruction in a node b is denoted by b.instr, and b.entry (resp. b.exit) is a Boolean which holds if b is the entry node (resp. is an exit node) for the method. To monitor a program, we abstract its execution in a trace of events extracted at runtime. This is achieved by instrumentation, which can be modeled by the function instrument :

Instructions * Σ X * .

Residual Analysis of Parametric Properties

We aim to verify a program P against some parametric property ΛX .ϕ. The behavior of a program is abstracted by the set of parametric event traces that it can produce at runtime. Let [P ] ⊆ Σ X * be such set for a program P . The verification problem can then be stated as checking if all the traces of the program satisfy the property:

P |= ΛX .ϕ def = ∀τ ∈ [P ] : τ |= ΛX .ϕ
Any verification technique aiming to verify the program should then be able to explore all the parametric traces that the program can generate. Moreover, the technique should also be able to explore for each parametric trace τ the set of projected traces Proj (τ ) (see Sec. 3.2). However, statically, exploring the parametric traces requires full knowledge of the call graph of the program, whereas exploring projected traces requires knowledge of the aliasing relations between objects producing them. We know that obtaining such information is generally undecidable statically. Meanwhile, at runtime, this information is completely available. Yet, runtime verification incurs overhead on the execution of the program where this overhead is typically positively correlated with the size of traces. Our interest is then to statically verify parts of the program and leave a residual part for runtime verification.

Our proposed residual analysis statically identifies a set of instructions in the program, S P , that can be safely silenced/ignored at runtime from the monitor side without affecting verification. Ignoring an instruction means that there is no need to produce an event when it executes. As such, we aim to construct the residual instrumentation function residual : Instructions * → (S P → Σ X * ). Let us note Runs ⊆ Instructions * the set of all the possible runs of a program P . Instrumenting the program with residual should ideally produce shorter traces than instrument, however, for both, we should get the same monitoring verdict. We can state the condition that should be met by the residual analysis as follows:

∀r ∈ Runs : |residual(r)| ≤ |instrument(r)| ∧ residual(r) |= ΛX .ϕ ⇐⇒ instrument(r) |= ΛX .ϕ
To perform the residual analysis statically and produce the set S P , we can overapproximate the program behavior by constructing a set [ P ] ⊇ [P ]. This allows us to explore all the parametric traces that the program can produce but also traces that the program might never produce. A residual analysis should then check whether silencing some instructions does not affect the verification verdict of any trace in [ P ], and safely assumes the same effect in [P ]. Yet, given that [ P ] is an over-approximation, the analysis may suffer from false positives, which are instructions that can indeed be silenced however the analysis found the opposite. In what follows, we consider a subset [ P m ] ⊆ [ P ] for our residual analysis, these are traces that are fully produced in single methods.

Residual Analysis via Intraprocedural Reachability Analysis

We demonstrate our instantiation of the residual analysis at the intraprocedural level using reachability analysis. Recall that we avoid dataflow and pointer analysis, as such, we do not have a static call graph for the program nor the variable aliasing relation. In Sec. 5.1, we capture the behavior of a method by using its control-flow graph to construct a representative model that allows us to explore the parametric traces a method can generate. In Sec. 5.2, we deal with the over-approximations by extending the badprefix automaton to handle different projections that might be produced by a parametric trace. In Sec. 5.3, we then present the reachability analysis algorithm that finds safe and violating paths in the control-flow graph; by cutting the behavior in a model-based checking approach. Finally, in Sec. 5.4, we discuss the soundness of our analysis.

Capturing the Behavior

Our analysis treats methods separately, however, we need to be careful. If a method receives as an argument an object which is a type that is capable of producing events in the alphabet of the property, then we cannot assume any previous behavior. As such, we exclude such methods from the analysis. For the same reason, we exclude all methods that operate on static instances of the types involved.

For each method m, we map two types of instructions to events and discard all other instructions as they are irrelevant to our analysis. We keep instructions that produce events in Σ, given by the property specification. We also keep instructions that may allow any object reference to escape from the context of method m; we introduce the new escape event (#) for such instructions. Escape events are assignments to class fields, method calls that pass objects by references, in addition, to return statements that return objects [START_REF] Choi | Escape analysis for java[END_REF]. However, our analysis allows the user to specify a safe list of instructions, denoted by the set SafeList, defined over the compile type information such as method names, package and type names, and opcodes. For instance, calling System.out.print(l1.toString()) is a safe instruction. All instructions that are escape events and are not in SafeList are added to the set Esc m .

Given the alphabet of a property Σ and the control-flow graph of a method m, CFG m = B m , E m , we replace each block b in B m with b and map its instruction to an event, and construct the CFG Automaton as follows.

b .instr = b.instr.map

  i →    i if i ∈ Σ, # else if i ∈ Esc m otherwise   Definition 7 (CFG Automaton).
Given the mapped CFG m , the CFG Automaton is the non-deterministic finite-state automaton A c m = (Σ ∪ {#}, Q, δ, q 0 , F ) constructed as follows:

Q = {q b | b ∈ B m } q 0 = {q b | b ∈ B m ∧ b.entry = true } F = Q δ = { q b , s, q b | b, b ∈ E m ∧ b.instr = s}
Each node in the control-flow graph is now represented as a state in the CFG Automaton. We make all states accepting states and merge states connected with transitions. Now, by traversing the CFG Automaton, we can explore the paths that method m can take at runtime and thus the parametric traces it can produce. Example 4 (CFG Automaton). Figure 3, shows the CFG Automaton constructed from the method in Sec. 2. Each state corresponds to an instruction that we are interested in the program. Two traces can be explored from the automaton in Figure 3, t 1 = ucuuncu, which corresponds to the parametric trace τ from Ex. 2, and t 2 = ucncu.

Extending the Automaton of Bad Prefixes

We now describe how our analysis handles the over-approximations and extends the bad prefix automaton.

Handling Variables May-alias Recall from Sec. 3.2, that a parametric trace τ in Σ X * at runtime is projected into Proj (τ ) to possibly multiple traces in Σ * , depending on the aliasing relationship between the objects carried in the events. At runtime, this aliasing relationship is available for the parametric monitor to do the projection. However, statically for our residual analysis this information is not available. Our central idea in this paper is to avoid performing data-flow analysis and assume that the objects producing events in a method may-alias. For two events, our analysis should then consider the case when the objects bound to them must-alias and the case when they must-not-alias. In the former case, both events will be projected into the same trace, and in the latter, they will be projected into different traces.

Example 5 (Projected traces approximation with may-alias). Consider the trace t 1 which can be explored with the CFG Automaton from Ex. 4. At runtime, if the program takes such a control flow path, it emits a parametric trace that produces either of the projected traces from Ex. 3 depending on whether l1 and l2 alias. Since we avoid producing the aliasing relation statically and assume that l1 and l2 may alias, we should then consider in our residual analysis the disjunction of both cases. Thus the traces pt 1 = {ucuuncu, ucnc, uuu} should be checked by our residual analysis. As for t 2 from Ex. 4, by the same reasoning, the traces to be checked are pt 2 = {ucncu, ucnc, u}.

Hence for method m, the set of traces that should be checked is pt 1 ∪ pt 2 .

The CFG Automaton allows us to explore the different paths that the program can take at runtime, however, its traces are too coarse. They may be polluted with events that do not correspond to the same trace at runtime. We notice from above that this is equivalent to generating and considering all the subwords of a trace, where the real trace can be any subword of a trace that can be explored with the automaton. Thus, to safely handle the different projections, we use the upward closure, from Sec. 3.3, of the language of bad prefixes L. By using the upward closure ↑L, we can recognize a bad prefix in a full trace or any subword of it since L ⊆ ↑L, allowing us to find bad prefixes in all possible projected traces. However, we restrict the closure by removing the Σ self-loops from the initial and final states as we want to find the shortest paths that match a bad prefix.

Handling Escape Events In Sec. 5.1, when constructing the CFG automaton, we introduced the escape # events. Since our analysis analyzes each method separately, we are oblivious to what might be happening in #-transitions. We have to assume that they might produce events untracked by the method under analysis. To handle them safely, we add a #-transition in the bad prefixes automaton from each state to all of its reachable states. Intuitively, this means when # event is encountered in a path, we assume that the path is not safe anymore and that it might match a bad prefix.

Extending the Bad Prefixes Automaton

We proceed to show how we extend the automaton of bad prefixes to handle the multiple projected traces and the escape events. Definition 8 (Extended automaton of bad prefixes). Given the language of bad prefixes L(bad ϕ ) recognized by automaton A badϕ = (Σ, Q, δ, Q 0 , F ) with its extended transition function δ. The extended automaton of bad prefixes is defined as

A ↑badϕ = (Σ ∪ {#}, Q, δ , Q 0 , F ) where: δ = δ \ { q, s, q | s ∈ Σ ∧ (q ∈ F ∨ q ∈ Q 0 ) } (1) ∪ { q, s, q | s ∈ Σ ∪ {#} ∧ q ∈ Q ∧ q / ∈ Q 0 ∧ q / ∈ F } (2) ∪ { q, #, q | q, q ∈ Q ∧ ∃w ∈ Σ * : δ(q, w) = q ∧ q / ∈ F } (3)
The extended automaton has the same states. We remove the self-loops from initial and final states, as we want to find the shortest paths that match a bad prefix [START_REF] Ahrendt | Verifying object-oriented programs with key: A tutorial[END_REF]. We add the upward closure by adding Σ and # self-loops on all other states (2). We add #-transitions from each state to the reachable states from it (3).

Example 6 (A ↑badϕ for the SafeIterator property). Figure 4, shows a construction of automaton A ↑badϕ . Recall the pattern c.n * .u + .n from Ex. 1, the new automaton will now recognize such a pattern while also handling the two over-approximations above.

q 0 q 1 q 2 q 3 c,# # # # u,# Σ,# Σ,# n,#
Fig. 4: The constructed automaton A ↑badϕ .

Cutting the Behavior

We now proceed to describe how we find violating paths in the method. The idea is to traverse the constructed CFG automaton A c m state by state and check whether there is a path, starting from the visited state, that makes the extended bad prefixes automaton reach a final state. We limit the discussion here to matching bad prefixes, nevertheless, the same analysis works for matching good prefixes. However, when finding paths that match good prefixes, these will be the safe paths.

Given an automaton, A, A(q) denotes A where q is set to be the initial state. Recall that, given a finite state machine A(q) with its extended transition function δ [START_REF] Hopcroft | Introduction to Automata Theory, Languages, and Computation[END_REF], a state q is coreachable if there exists a word s ∈ Σ * such that δ(q, s) ∈ F . State q is reachable if there exists a word s ∈ Σ * such that δ(q 0 , s) = q and q 0 is an initial state.

Algorithm 1: Marking violating and safe paths

1 Given A c m = (Σ ∪ {#}, Q, δ, q0, F ), A ↑badϕ 2 Vm = ∅ // represents
all states in a violating path 3 Sm = Q // represents all states in a safe path

8 if q / ∈ visited then 9 visited = visited ∪ q 10 if q / ∈ Vm then 11 Â = A c m (q) × A ↑badϕ 12 if L( Â) = ∅ then 13 Vm = Vm ∪ {{q | (q , -) ∈ coreachable( Â)} ∩ reachable(A c m (q))} 14 foreach q in {q | q, s, q ∈ δ} do 15 work .push(q ) 16 end 17 end 18 Sm = Sm \ Vm
Algorithm 1, shows how to mark all states in A c m as either safe (in S m ) or violating (in V m ). The algorithm implements a depth-first search starting from the initial node of A c m . We maintain a work stack and visited set, in lines [START_REF] Azzopardi | Clarva: Model-based residual verification of java programs[END_REF][START_REF] Barringer | Quantified event automata: Towards expressive and efficient runtime monitors[END_REF][START_REF] Bauer | Runtime verification for LTL and TLTL[END_REF][START_REF] Bodden | Clara: A framework for partially evaluating finitestate runtime monitors ahead of time[END_REF][START_REF] Dwyer | Residual dynamic typestate analysis exploiting static analysis p[END_REF], to hold automaton states to be visited and states that were already visited, respectively. For each state q we visit, we set q as the initial node and find the intersection with the A ↑badϕ , line [START_REF] Chen | Parametric trace slicing and monitoring[END_REF].

If the intersection is not empty (line 12), we find the set of all co-reachable states in the intersection automaton. Each state in the intersection automaton  corresponds to a state in A c m and A ↑badϕ . For each coreachable state in Â, we add its corresponding state in A c m to the set V m , (line 13). We do not revisit states that are already in V m (line 10) since paths leading to a final state in A ↑badϕ are already explored by the intersection. Example 7 (Property violating states). Figure 5, shows the CFG Automaton constructed from the program from Figure 1, where states marked in red exist in a property-violating path. The red states in the automaton are the states that we need to instrument, and the green states are hidden from instrumentation. We can see that instead of instrumenting at 8 different locations, we only have to instrument at 4 locations.

For our residual analysis, for each method m we analyze, we add the instructions corresponding to the states in S m to the set S P . As for the other states in V m , their corresponding instructions will be instrumented for runtime monitoring.

Scope and Soundness of the Analysis

We first argue that our analysis only affects the traces that are fully produced in one method. Recall from Sec. 5.1, that the nodes of CFG automaton A c m correspond to instructions in method m that produce events. We use the notation ev(q) to denote the corresponding event from an automaton state, and events(t) to denote all events from a trace t. If some trace t contains events produced by instructions outside of m, then no instruction in m that produced events in t was marked safe.

Proposition 1 (Scope of the analysis). Given a parametric trace τ in [P ]:

∀t ∈ Proj (τ ), ∀m ∈ Methods : ( ∃i ∈ Instructions\Instructions m : instrument(i) ∈ t ) =⇒ { ev(q) | q ∈ S m } ∩ events(t) = ∅ Proof.
Assume that there exists some trace t that has events produced outside of m i.e. ∃i ∈ Instructions\Instructions m : instrument(i) ∈ t is true. Such traces can be split into two types. Traces that contained events before the execution of m at runtime (1), and traces that start from m but have some events that are produced outside of m at runtime (2). We will show that for both types of traces, the analysis would result in S m = ∅. Since we exclude from the analysis any method that receives a parameter of a type that generates events. Traces from (1), will not be affected by analysis. For that to happen, method m should receive the objects generating the events. Therefore, m will be excluded from the analysis resulting in S m = ∅. As for (2), any escape of an object, which might produce events outside m, is captured by the # transitions.

From the construction of the bad-prefixes automaton and Algorithm 1, such transitions will result in reaching a final state from any state in the CFG automaton, resulting in S m = ∅. Hence for both types of traces we have S m = ∅, therefore {ev(q) | q ∈ S m } ∩ events(t) = ∅ holds, and the proposition holds.

Proposition 1 in fact depends on the specification of the SafeList from Sec. 5.1. If some method was added by the user that is not safe, i.e. allows references to escape, then the proposition will not hold. From the above, we also see that our analysis only affects instructions that produce events only in traces that are collected fully in the method itself since otherwise S m = ∅. For soundness, we need to guarantee that at any run of the program, an event that we marked safe in our residual analysis does not have any effect on deciding the violation/satisfaction of the property for any projected trace at runtime. As we showed that the analysis only affects projected traces that are fully produced in one method, we only reason about single methods when discussing soundness.

Theorem 1 (Soundness of the analysis). Given a language L ⊆ Σ * and S m resulting from the analysis on method m, the analysis is sound iff

∀a 1 • • • a i • • • a n ∈ Σ + , ∀i ∈ N : match L (a 1 • • • a i • • • a n ) = match L (a 1 • • • a i-1 a i+1 • • • a n ) =⇒ a i / ∈ { ev(q) | q ∈ S m }
The condition states that given a projected trace at runtime, if we remove an event a i from it and get a different match from the new trace i.e. match L (a

1 • • • a i • • • a n ) = match L (a 1 • • • a i-1 a i+1 • • • a n ),
then our analysis must have not statically marked a i as safe (a i / ∈ { ev(q) | q ∈ S m ). Proof. The proof follows from the definition of Algorithm 1. Assume that when our analysis removes a i , then match L (a

1 • • • a i • • • a n ) = match L (a 1 • • • a i-1 a i+1 • • • a n ).
This means that a i is in an extension of a 1 • • • a i-1 that leads to a final state in the monitor of the bad-prefixes of L, or else match L (a

1 • • • a i • • • a n ) = match L (a 1 • • • a i-1 a i+1 • • • a n ).
However, if a i is in such a path, then it will be added to V m as per Line 7 of Algorithm 1 since the algorithm finds any path from a state in the CFG that reaches the final state of the automaton of bad-prefixes. Then a i is not in S m and a i / ∈ { ev(q) | q ∈ S m } holds.

Implementation

We implement our work as a plugin to the BISM [START_REF] Soueidi | BISM: Bytecode-Level Instrumentation for Software Monitoring[END_REF] Java byte-code instrumentation tool. Instrumentation directives in BISM are given with transformers, which resemble aspects of aspect-oriented programming. BISM provides a mechanism to compose multiple transformers. Transformers, in composition, are capable of controlling the visibility of instructions. For each property, we then apply two transformers to the program: the static analyzer, which performs the residual analysis with a single pass over the code of methods and hides safe instructions, and the second one to instrument the residual part for runtime monitoring. We extend BISM with a module that enables performing the residual analysis and provides automata operations. The module is used to generate the CFG automata of methods, extend the automaton for bad prefixes, and detect the property-violating execution paths.

Evaluation

We report on our evaluation of the effectiveness of our approach2 .

Experimental setup. We compare the instrumentation overhead with our residual analysis, denoted by RRV, and without the analysis, denoted by RV. We instrument with BISM the programs, in the DaCapo suite [START_REF] Blackburn | The dacapo benchmarks: Java benchmarking development and analysis[END_REF], for the monitoring of the classical SafeListIterator (P1), SafeMapIterator (P2), and SafeHasNext (P3) properties. (P2) is similar to (P1) from Sec. 2 but is concerned with Java maps. (P3) specifies that a program does not call the next method before calling the hasNext method of an iterator. We include as escape events (#) all assignments to class fields, all method calls that pass objects by references, and in addition, return statements that return objects [START_REF] Choi | Escape analysis for java[END_REF]. We include in the SafeList all calls to methods of Java classes. Other than the method calls relevant to the property and captured by instrumentation, these calls do not produce events. We note that fop is the only single-threaded benchmark, however, we can use the multi-threaded benchmarks as we checked that for the properties all the events in the projected traces are being produced within the same thread. We consider 100 runs and then calculate the mean and the standard deviation3 .

Evaluation metrics. We consider the number of affected instructions, methods, and classes by our residual analysis (RRV) and without it (RV). We also consider the improvement factor. We are also interested in evaluating the runtime overhead, that is, the performance degradation caused by instrumentation for monitoring. For runtime, we measure the execution time of the instrumented program. For used memory, we measure the used heap and non-heap memory after a forced garbage collection.

Results. In Table 1, we report the results. The table demonstrates the effectiveness of the residual analysis as it reduces the number of instrumentation points by a factor of 2.5 on average (reaching 9.19), and accordingly, a reduction in the number of generated events at runtime by a factor of 1.8 on average (reaching 6.13). We notice that the reduction of instrumentation points does not always result in a reduction of runtime events for instance with avrora with (P1), where we find methods that produce most of the events that we could not prove safe statically. We also notice that most of our missed optimizations are due to escape # events (see Sec. 5.1). The more diverse operations between events, the more missed optimization. However, the SafeList can be improved with the help of escape analysis to include more instructions that we can guarantee are safe for our analysis and accordingly reduce the number of escape events. We leave that Table 1: For each program (Bench), and property (P1), (P2), and (P3), we report # of relevant classes, methods, and instructions (Rel) producing events, number proved safe statically by our technique (Nop), # of events produced at runtime (RV) and after our analysis (RRV), improvement factor for # of instructions instrumented and events produced (Imp). K = 10 3 , M = 10 for future work as we envision adding plugins to incorporate static analysis. We also note that many of the events generated under classical instrumentation (RV) are irrelevant; they occur in methods that do not produce enough events to reach a final state in the monitor. As such, our analysis is effective in removing those from instrumentation. Figures 6 report the execution time and the memory usage for the benchmarks with all three properties combined. The figures show that RRV results in better performance in all benchmarks than classical instrumentation RV.

Related Work

Many research approaches combine static and runtime verification. We focus here on some influential and most recent tools devised for verifying general behavioral parametric properties in sequential programs via residual analysis. CLARA [START_REF] Bodden | Partially evaluating finite-state runtime monitors ahead of time[END_REF][START_REF] Bodden | Clara: A framework for partially evaluating finitestate runtime monitors ahead of time[END_REF] handles properties that can be expressed by finite-state automata by partially evaluating the runtime monitors at compile time and reducing the instrumentation points. It performs three-staged phases of analysis with increasing precision. The more precise phase uses a demand-driven pointer analysis and handles intraprocedural analysis. The first two phases of its analysis can be easily applied within our framework. However, unfortunately, CLARA is no longer maintained and so is its underlying instrumentation tool the abc compiler [START_REF] Avgustinov | Abc: An extensible aspectj compiler[END_REF]. In [START_REF] Wang | Optimizing nop-shadows typestate analysis by filtering interferential configurations[END_REF], the authors present two optimizations for [START_REF] Bodden | Partially evaluating finite-state runtime monitors ahead of time[END_REF]. One optimization identifies changeless configurations during the backward analysis; the other one uses local object information to refine the forward analysis and backward analysis of the nop-shadow analysis. CLARVA [START_REF] Azzopardi | Clarva: Model-based residual verification of java programs[END_REF] extends CLARA [START_REF] Bodden | Partially evaluating finite-state runtime monitors ahead of time[END_REF] Events and Timers [START_REF] Ahrendt | A unified approach for static and runtime verification: Framework and applications[END_REF]) where events are guarded by runtime conditions and timers. Similar to our approach, it transforms Java code into an automaton-based model and allows for the incorporation of control-flow analyses. CLARVA is capable of reducing the instrumentation points as well as reasoning about and pruning the property itself.

However, the analysis relies on constructing the callgraph of the full program and on pointer analysis using Soot [START_REF] Vallée-Rai | Soot -a java bytecode optimization framework[END_REF]. Our approach is still capable of producing optimizations with a single pass on the program and without any dependence on static analysis, separating the limitations of static analysis from the residual analysis. STARVOORS [START_REF] Chimento | Starvoors: A tool for combined static and runtime verification of java[END_REF] combines deductive theorem proving with control-flow reachability analysis allowing to target control and data-oriented properties. The formalism used for property specification is ppDATE (an extension of DATE) where the automaton states are extended with pre/post-conditions (Hoare triples). The property is reduced by pruning the transitions based on solving the triples with Java theorem prover KEY [START_REF] Ahrendt | Verifying object-oriented programs with key: A tutorial[END_REF]. STARVOORS is capable of handling control and data-oriented properties, however, it focuses on pruning the property and does not reduce the instrumentation points.

In [START_REF] Leucker | Sliding between model checking and runtime verification[END_REF][START_REF] Zhang | Runtime verification with predictive semantics[END_REF], the authors present Predictive Semantics for runtime monitoring at the intra-procedural level. In this setup, the program is analyzed, using the control flow graph (CFG) and program dependence graph (PDG), to find predictive words. Predictive words are events that will occur in sequence in a control-flow path. Then, the monitor at runtime will either receive a single event or a predictive word. This approach does not reduce the instrumentation points, hence does not reduce the overhead of instrumentation, however, it emits predictive words which may produce faster verdicts.

Conclusion and Perspectives

We introduce an analysis supporting residual runtime verification for parametric properties that can be expressed by finite-state automata. Our approach over-approximates the behavior of the program and analyzes its methods separately relying only on their control-flow graphs to statically identify safe regions. We have demonstrated the effectiveness of our approach in monitoring the bad prefixes of a property, however, our approach can also be used with good prefixes (when monitoring co-safety properties for instance). Our approach is capable of producing overhead optimizations without any dependence on a specific type of static analysis, separating the task of static analysis from the residual analysis and allowing for seamless integration with many RV frameworks. It is fully implemented and integrated within the BISM instrumentation tool, which is the state-of-the-art instrumentation tool for Java programs. We also demonstrated the significant performance benefits at runtime.

Our work lays the foundation for a residual analysis framework that, at its core, does not depend on any specific static analysis technique. Nevertheless, we plan to extend it with plugins that allow the user to easily incorporate static analysis results aiming to reduce over-approximations and increase precision. The user might opt to include static call graph construction and escape analysis for a more precise approximation of parametric traces, also data-flow pointer analysis for better approximations of projected traces. We plan to provide a language that easily integrates the results of such analysis into our residual analysis mainly via refining the safe list of instructions. We also plan to extend our approach to analyze concurrent programs and handle thread-escaping references.

Fig. 2 :

 2 Fig. 2: Monitor recognizing the language of bad prefixes for the SafeIterator property.

Fig. 3 :

 3 Fig. 3: The constructed CFG Automaton A c m

4 7 q

 7 work := q0 // represents a worklist stack 5 visited = ∅ 6 while work not empty do = work .pop()

Fig. 5 :

 5 Fig. 5: Marking property violating paths in red, and safe in green.

  to handle properties expressed by DATEs (Dynamic Automata with Execution time (ms).

  Used memory (MB).

Fig. 6 :

 6 Fig. 6: Evaluation for the three properties.

  6 .

	Bench Property # Classes # Methods # Instructions	# Events
			Rel Nop Rel Nop Rel Nop Imp RV	RRV Imp
	avrora	P1	41 14 99	56 165	86 2.09 1.36M 1.36M 1.00
	fop	P1	123 33 275 103 700 210 1.43 729K 490K 1.49
	sunflow	P1	11	2 35	15	50	15 1.43 2.55M 1.27M 2.00
	pmd	P1	86 27 200	95 420 146 1.53 4.77M 778K 6.13
	avrora	P2	41 19 111	78 160 117 3.72 353K 246K 1.43
	fop	P2	100 28 206	85 2.9K 2.6K 9.19 545K 351K 1.55
	sunflow	P2	11	6 32	24	40	26 2.86 2.55M 1.27M 2.00
	pmd	P2	81 27 168	70 392 211 2.17 3.01M 2.6M 1.16
	avrora	P3	32 11 76	33 160	79 1.98 1.5M 1.29M 1.16
	fop	P3	70	7 145	31 376	67 1.22 1.07M 882K 1.21
	sunflow	P3	8	2 12	3	29	3 1.12 3.93M 2.65M 1.48
	pmd	P3	65 21 126	48 343 115 1.50 5.64M 5.23M 1.08

This can checked with == in Java.

Implementation details and experiments can be found at https://gitlab.inria.fr/monitoring/ residual-runtime-verification-with-bism.

We use Java JDK 8u251 with 16 GB maximum heap size on an Intel Core i9-9980HK (2.4 GHz. 16 GB RAM). We use the DaCapo version 9.12-bach.


Nicolas Fournel

Antoine Fraboulet

Paul Feautrier

Embedded Software Energy Characterization: using non-intrusive measures for application source code annotation

In this paper we propose a complete system energy model based on non-intrusive measurements. This model aims at being integrated in fast cycle accurate simulation tools to give energy consumption feedback for embedded systems software programming. Estimations take into account the whole system consumption including peripherals. Experiments on a complex ARM9 platform show that our model estimates are in error by less than 10% from real system consumption, which is precise enough for source code application design, while simulation speed remains fast.

Introduction

With present day technologies, it is possible to build very small platforms with enormous processing power. However, physical laws dictate that high processing power is linked to high energy consumption. Embedded platforms are mostly used in hand-held appliances, and since battery capacity does not increase at the same pace as clock frequency, designers are faced with the problem of minimizing power requirements under performance constraints.

The first approach is the devising of low-energy hardware technologies, but this is outside the scope of this paper. The second approach is to make the best possible use of the available energy e.g. by adjusting the processing power to the instantaneous needs of the application, and by shutting down unused parts of the system. These tasks can be delegated to the hardware. However it is well known that the hardware only source of knowledge for scheduling is the past of the application; only software can anticipate future needs. Energy can also be minimized as a side effect of performance optimization. For instance, replacing a conventional Fourier transform by an FFT greatly improves the energy budget; the same can be said of data locality optimization, which aims at replacing costly main memory accesses by low-power cache accesses.

The ultimate judge in the matter of energy consumption is measurement of the finished product. However, software designers, compilers and operating systems need handier methods for assessing the quality of their designs and directing possible improvements. Hence designers need simple models which must be expressed in term of software visible events like instructions, cache hits and misses, peripheral activity and the like. There are several ways of constructing such models. One possibility is electrical simulation of the design; this method is too time-consuming for use on systems of realistic size. Another method is to interpolate/extrapolate from measurements on a prototype. This is the method we have applied in this work.

The paper is organized as follows. After reviewing state of the art techniques in section 2 we present in section 3 a methodology to build complete platform energy consumption models for software development. Section 4 presents the resulting model for an ARM9 development platform. This section also validates our model on more significant pieces of code, multimedia applications, thanks to its implementation in a fast and cycle accurate simulation tool. We then conclude and discuss future work.

Related Works

Many works focus on energy characterization of VLSI circuits. They can be organized using two main criteria: their level of hardware abstraction and the calibration method. For the first criterion, we can group the models in three main categories which are, by increasing level of abstraction, transistor/gate level models, architectural level models and finally instruction level models. Among these models there are usually three methods for building consumption models. The first method is analytical construction, the second one is simulation based, and the third is based on physical measurements.

In transistor (gate) level models, all transistor (gate) state changes are computed to give an energy consumption approximation for a VLSI component. This method is highly accurate, but a complete description of the component is needed. Models built at this level of abstraction are generally reserved to hardware designers and are very long to simulate.

Upper level of abstraction, architectural or RTL level, models the system using functional units. Each unit can be represented by a specific model adapted to its internal structure.(e.g. bit-dependent or bit-independent models for Chen et al. [START_REF] Chen | Architecture-level power estimation and design experiments[END_REF]). To be more accurate, some works like Kim et al. [START_REF] Kim | Power Aware Computing, chapter Challenges for Architectural Level Power Modeling[END_REF], subdivide the block into sub-blocks to apply different models on each sub-block. This set of models allows to extend models to a complete platform.

The highest level is instruction/system level of abstraction. At this level, models are based on events such as instructions execution ([19, 10, 13]). Tiwari et al. in [START_REF] Tiwari | Instruction level power analysis and optimization of software[END_REF] propose to characterize hardware activity down to the interinstructions energy consumption, which represents the logic switching activity between two different instructions. Others works also take into account the logic switching due to data parameters [START_REF] Steinke | An accurate and fine grain instruction-level energy model supporting software optimizations[END_REF]. Systems considered in these models are generally composed of CPU, bus and memory. Only few works focus on modeling a complete platform with peripherals. Among them, EMSIM [START_REF] Tan | EMSIM: An Energy Simulation Framework for an Embedded Operating System[END_REF] is a simulator based on Simunic et al. [START_REF] Simunic | Cycle-accurate simulation of energy consumption in embedded systems[END_REF] which includes the StrongARM SA110 energy characterization. This simulator poorly characterizes the peripherals and focuses on the microprocessor. The SoftWatt simulator proposed in [START_REF] Gurumurthi | Using complete machine simulation for software power estimation: The softwatt approach[END_REF] uses a complete system simulator based on SimOS to monitor a complex operating system and interactions among CPU, memory hierarchy and hard disk operations. Their simulator is modified to include analytical energy models and the output reports kernel and user mode energy consumption up to the operating system services. Data are sampled during simulation and dumped to log files at a coarser granularity than cycle level, leading to average power consumption figures. The closest work to ours, AEON's model [START_REF] Landsiedel | AEON: Accurate Prediction of Power Consumption in Sensor Nodes[END_REF], is a complete platform energy consumption model based on measurement and uses simulator internal energy counters. The targeted platform is an 8 bit AVR micro-controller based sensor network node that does not include CPU pipelines, complex memory hierarchy and peripherals. Our model allows the simulation of much more complex hardware architectures while being independant of simulator internals. Some other works, like SoftExplorer [START_REF] Senn | Softexplorer: estimation, characterization and optimization of the power and energy consumption at the algorithmic level[END_REF], even propose to model energy consumption by relying on higher parameters like algorithmic parameters, or application implementation parameters like variable size in Mutterja et al. [START_REF] Muttreja | Automated energy/performance macromodeling of embedded software[END_REF].

As far as calibration methods are concerned, analytical models are usually based on manufacturers data, e.g. in Simunic et al. [START_REF] Simunic | Cycle-accurate simulation of energy consumption in embedded systems[END_REF] the model is built thanks to datasheet informations. Simulation based calibration needs a full knowledge of the underlying level architecture, which means that it needs a description of low level hardware (VHDL, or Verilog descriptions). Measurement based methods only need few informations on the hardware and works like [START_REF] Tiwari | Instruction level power analysis and optimization of software[END_REF][START_REF] Contreras | XTREM: a power simulator for the Intel XScale core[END_REF] have shown that it is possible to extract internal unit consumption from system measurements.

In this paper we propose a methodology for complete platform energy consumption model construction based on simple and non-intrusive measurements. The model is built at a level of abstraction close to the system level presented before, but is extended to the complete platform by coupling it with architectural level principles presented by Kim et al. in [8]. We also take peripherals energy models and dynamic frequency and voltage scaling into account. Our model is geared toward user feedback at the application source level.

Model construction basics

We present in this section our methodology to build complete platform models. We first give more details on the structure and the parameters of the energy model. Section 4 will present the target dependent model parameters through a case study on an ARM9 based platform.

Model structure and parameters

Our choice among all the modeling methods which have been presented in Sect. 2 is to build an architectural level model, in which the system is divided into its main functional blocks at the platform based level such as CPU, interconnection bus, memory hierarchy, peripherals. . . The energy consumption of an application E app is obtained be adding all blocks consumptions E bl .

Each block can have its own energy consumption model. To have a platform model better suited for software development, we use instruction level abstraction for CPU. CPU energy consumption E CPU is described in equation ( 1).

E CPU = E insn + E cache + E MMU (1)
The energy consumption is the sum of the energy consumed by instruction execution, plus cache and MMU overheads consumptions, and consumption of all other blocks of the platform.

E app = E CPU + E bl (2)
This model aims at being integrated in a full platform cycle accurate simulation tool. The most interesting way of writing the model for this kind of purpose is to define a time slot energy consumption. The chosen time slot is the CPU instruction execution. There are two reasons for choosing this time reference. The first is that it is the finest time reference since CPU have generally the highest clock frequency in embedded platforms. Secondly, interrupt requests, the only mean for the hardware peripherals to interact with the software, are managed at the end of instructions execution. From a software point of view, there is no need to use a finer time reference to report hardware events more precisely. From a precision point of view we do not model inter-instruction switch activity nor data dependent. These parameters can be ignored at this level of abstraction as we will see in section 4.4.

The model can be rewritten in a form where the consumption of CPU and other blocks are reported for the currently executed instruction. All E * will be kept for overall application consumptions, for the sake of notation simplicity the consumption at instruction level of granularity will be noted as E * . This new model formula is expressed in the following equation:

E slot = E CPU + blocks E bl (3)
The last peculiarity in this model is the measurement based data collection. As we only get global measures for the platform consumption, we can foresee that the base consumptions of each block will not be easily distinguishable. We mean here that once the embedded system is put in its laziest state, idle state for example with all possible units powered off, the resulting consumption is considered as a base consumption regrouping the base consumption of every powered peripherals. Obviously, a part of this consumption is static power dissipation. We will call this term E base , it is important to note that this consumption is reported to the current executed instruction on the CPU. It can be expressed as in equation ( 5), as it is dependent on the instruction length l insn in terms of clock cycles. Equation (3) becomes equation ( 4).

E slot = E base + E CPU + E bl (4)
E base = l insn × E c base (5)
The CPU and other blocks consumption are then expressed as overhead against the idle state. As described in equation ( 1), CPU energy consumption is given by the executed instruction energy cost. This model can be simplified by regrouping instructions in classes as proposed in [START_REF] -C. Lee | Power analysis and minimization techniques for embedded dsp software[END_REF]. As far as other blocks are concerned, we can expand them as bus, memories and other peripherals. This is interesting since bus and memories will be subject to events generated by the processor, such as memory writes. The peripherals will be then modeled by state machines giving consumption of the peripheral during the time slot.

The last step in model construction consists in defining all possible parameters for these components. Due to the limited information available, developers do not necessarily know the behavior of intra-blocks logic. The parameters for the CPU are already selected, since it is modeled thanks to instructions consumptions. The same can be done for cache, MMU and even co-processors consumptions. The parameters for other blocks are limited to behavioral parameters (UART sending a byte) and their states such as operating modes.

Each energy cost in this model is function of the running frequency and power supply voltage to allow dynamic and frequency scaling capabilities of the platform to be modeled. An example of this is presented in the next section.

Model Construction Case Study

In this section we propose an extended example of our methodology application. This methodology was applied on a ARM based development board. This platform uses an ARM922T and usual embedded systems peripherals (e.g. UART, Timers, network interface) on the same chip. Our hardware architecture exploration shows that the platform has three distinct levels of memory, a cache, a scratchpad and main memory. All peripherals are accessible through two levels of AMBA bus. We will give details about the energy consumption model construction for this platform, then we will check the accuracy of the resulting model.

Methodology application

The complete platform modeling method presented in section 3.1 is applied on our ARM9 platform in this section. The measurement setup used for these experiments is close to the one depicted in [START_REF] Russell | Software power estimation and optimization for high performance, 32-bit embedded processors[END_REF]. We used a digitalizing oscilloscope, the shunt resistor is replaced by a current probe and we also used a voltage probe.

Calibration benchmarks. We built benchmarks to calibrate our model, more precisely our block models. The hardware exploration gives us the main blocks to be modeled, namely the CPU, the different bus levels, the memory levels, and the other peripherals such as UART, interrupt controller or timers. For example, the selected parameters for our CPU model are the CPU instructions, or possibly class of instructions, plus the caches and MMU activities. We thus built benchmarks to evaluate the cost of possible parameters, in order to select only relevant ones. Here are examples of benchmarks that were used, and their target event:

• loop-calibration: Measurement loop overhead benchmark. By running an empty loop, we can estimate the loop overhead.

• insn-XXX: Comparison of CPU instructions execution costs (add, mov, . . . ). The target instruction is executed many times inside a loop.

• XXX-access: Calibration of costs of each bus level (AHB1/2) and memory level (cache, scratchpad or main memory), depending on the address accessed.

• timer-test: Example of peripherals energy characterization, this benchmark allows us to measure the timer power consumption. It is subdivided into two benchmarks, one in which the timer is stopped and the second in which the timer is running. The structure of the loop is the same as the insn-XXX benchmark with a nop instruction.

Calibration results. Benchmark energy results examples are listed in table 1.

Full results are available in [START_REF] Fournel | Embedded Systems Energy Characterization using non-Intrusive Instrumentation[END_REF]. These results represent for each benchmark the length of the calibrated event in CPU clock cycles (second column), the per-event raw energy cost measured on the complete platform (third column) and the measurement error (fourth column). Energy costs reported here give the consumption of the complete platform for a full event execution. These raw costs have to be refined to get the final parameters.

As an example, the scratchpad memory access benchmark result (spm-access) gives the energy consumption of the CPU executing a load instruction, the bus conveying the load request and response and finally the scratchpad memory. The bus access cost includes the register accesses in the targeted peripherals since it is impossible to dissociate their costs. By removing the consumption of the CPU (one load and seven nop) and bus consumption, we finally obtain the scratchpad memory access cost. Experiments reported in [START_REF] Fournel | Embedded Systems Energy Characterization using non-Intrusive Instrumentation[END_REF] shows that the scratchpad memory does not consume more energy than a register accessed via the bus.

Other model simplifications are possible. For example, the CPU cache models are simplified by taking into account only memory access bursts in case of misses since the overhead can be neglected.

The basic model presented in section 3.1 can be rewritten, by using models simplifications obtained by calibration. We found that most instructions have the same energy consumption as long as they stay inside the CPU and that control and data logic switching between instruction execution can be neglected. Currently only ARM32 instruction set is modeled. Thumbs (16bit) instruction set can be modeled using the same benchmark methodology. In our setup, it is not possible to isolate the instruction cache consumption, which is lumped with the instruction consumption. ICache misses can be modeled as memory accesses.

We finally have a model for which CPU instructions are grouped in two classes, arithmetic and logic intra-CPU instructions, and load / store instructions. A memory load access is modeled as a load instruction, plus a bus overhead, plus a memory overhead. Peripherals energy consumption are taken into account thanks to state machines that give their consumption during instructions execution. The final model is written on equation ( 6).

E slot = E base + E insn + E bus access + E mem + E periph state (6)
E slot is the energy consumption of the instruction execution time slot, E insn is the cost of instruction given by its class cost, E bus access is the bus overhead cost for load or store instructions, E mem is the overhead for memory accesses. The last term represents the sum of the energy overhead of peripherals state. These cost are all overhead costs, since the full consumption of a peripheral cost, for example, is given by its base energy cost comprised in E base and the overhead.

Frequency Scaling. The model presented before is valid for full speed software execution. However, the Integrator CM922T has frequency scaling capabilities but no dynamic voltage scaling (DVS) capabilities, hence when frequency is reduced, energy consumption does not decrease. When repeating five benchmarks at different frequencies, we obtain the curves in Fig. 1. This figure represents the per event energy values for the five benchmarks as a function of the clock divisor, r = f ref f where f ref is the nominal frequency (198 MHz here). These curves show that energy per event increases when frequency is decreased, and this may seem counter-intuitive. To understand these results observe first that a given event, e.g. the execution of some specific instruction, entails an almost constant number of bit flips, and that each flip uses a fixed amount of energy. Hence, to a first approximation, and in the absence of voltage scaling, the energy for a given event should be a constant. However, in our platform, frequency scaling acts only on the processor and Excalibur embedded peripherals; the consumption of other peripherals and external memories is not affected. Hence, the addition of a parasitic term which is roughly proportional to the duration of the event or inversely proportional to frequency. This is clearly the case for the curves of Fig. 1.

We must underline that all five benchmarks generate activity in the modified clock domain (CPU), but not on the remaining part of the platform. On top of that, we kept all peripherals in the modified clock domain in an idle state. Hence, the event energy cost namely E evt can be an instruction execution or a bus access for example. In this consumption we can identify two types of sources. The first is the energy due to modified clock domain E mc , which is constant. The second is the one due to the remaining part of the platform E rp base . Their relation in the total consumption of event is given by relation:

E evt = E rp base × l insn × r + E mc (7)
The first term is dependent on the frequency ratio r and the instruction length l insn , whereas the second is not. Linear regressions on the results presented in Fig. 1 are shown on table 2. As shown in this table, equation (7) give a good explanation for the experiments on clock frequency variation. These results gives us an estimation of what we can consider as base energy, which is not changing against software execution. The last two columns are the events real consumption and the regression error. The value for the base energy can be approximated by the mean value 10.82 nJ per cycle (with a standard deviation of ±2.6 10 -2 ).

Large targeted architecture range

The model building method was successfully applied on a second platform. This second platform is a wireless sensor network node, a WSN430 [START_REF] Brevet | Wsn430: Ultra low power wireless module for sensor network applications[END_REF]. This system is based on a 16bits microcontroller, Ti MSP430, which has a completely different architecture compared to the ARM one. This second model construction validates the fact that the model is generic enough to be adapted on a large range of target.

On top of that, model adaptation to more complex peripherals is also verified since WSN430 embeds a wireless network interface. This interface is a good example of complex peripheral with multiple running states and dynamically modifiable parameters such as transmitting power.

Model usage

To ease their use, models obtained thanks to previous methodology are designed to be implemented in a simulation tool. The goal of such an implementation is to keep the main advantages of the model in its usage, namely simplicity and speed, and to offer higher level information on the application execution consumption.

Simulation architecture. To ensure a simple and fast usage of the model in software evaluation of energy consumption, we implemented it in a two step simulation tool as depicted on figure 2. First, this implementation extends a standard development flow for embedded systems. As can be seen on figure 2, once software is written the first step consists in application compilation to produce application binary which will be executed on final system. However the process is iterative and debug phase is a cycle where user compiles, runs application either on real platform or on a simulator to identify bugs and correct them.

The simulation tool proposed replaces the previous one to offer energy and performance information on application execution on top of helping the developper to debug it. The two steps of this tool are first a full platform simulation and secondly an analysis of the trace produced by the first step simulation.

The first step of this tool is responsible of simulating the software execution on the full hardware platform in a reliable manner. It has to be functionally correct to accurately describe platform activities for energy consumption evaluation. It is also time accurate since energy consumption is dependent of time. Activities of the hardware platform are reported in an execution trace which fed the second tool step. The trace describes on an instruction execution time basis (the slot) all activities of the hardware platform, the instruction itself and peripheral events. These slots contain information on time and cycles spent in order to allow a DVFS support on platform natively embedding this technology.

The second step, eSimu, implements the model to produce energy consumption estimations based on information in the trace. This step processes the trace to get parameters, weights them with costs given by calibration informations to obtain energy consumption of the platform during an instruction execution. On top of energy consumption evaluation, this tools processes the instruction costs to report them in a higher level metric, at the source code level.

By relying on a given format for the execution trace, we can use the same implementation of the model for different platform adaptation. All platform dependent information are contained in the execution trace and the calibration data, given as input of eSimu. On top of that, the first step of this toolchain can be made thanks to a standard simulator, provided its sources are available, by extending it with a library distributed with eSimu. This extension consists in fetching some behavior information in the simulation loop and filling corresponding structures.

However, the main drawbacks of this architecture is the execution trace size and the I/O accesses necessary to write it. This is the reason why the library proposed for trace generation can produce diverse formats ranging from an ASCII human readable format to a binary Z compressed one. For example, the simulation of 60s of the sensor node sending packets produces a 0.57 MB compressed trace whereas raw ASCII trace size would have been 114 MB large.

Result outputs.

To ease the developper result interpretation, eSimu provides three kind of results output: global information, linear trace and source code annotation.

The first one is a summary of the temporal and energetic metrics for the application execution. This type of output can be used for quick software implementation comparition. Linear traces depicts the consumption of peripherals over time, which can be used to detect energy hungry peripheral behavior or misbehavior of a peripheral. Last but not least, source code annotation is the main source of information for developpers for application optimization. The format of this input is an emerging one used in current performance analysis tool such as the open-source project Callgrind, plugin of Valgrind. Using this standard format allows to reuse existing application for visualization like Simulator Integration. Our models, the ARM Integrator and WSN430 ones, are implemented in this simulation tool suite. The first step, complete platform functional simulation, is accomplished thanks to two different simulators. For the ARM9 platform, the open-source project Skyeye [16] is extended to produce the cycle-accurate execution trace of the software. To fulfill this first task for the WSN430 platform, we augmented another simulator named WSim [START_REF] Fraboulet | Worldsens: Development and Prototyping tools for Application Specific Wireless Sensors Networks[END_REF].

For the second step of the simulation tool suite, energy evaluation, eSimu was used for both platforms. As we said before, using an execution trace allows us to implement the model in the tool in a generic manner. The implementation of the model in eSimu enforces model properties, simplicity and genericity.

Model validation

We describe here our accuracy tests experiments. Our model is implemented in a simulator, and its results were compared to physical measurements.

Validation Methodology. To check the accuracy of the resulting model, we propose here a comparition between consumption estimations of the model, thus implemented in our tool and physical measurement on the real platform. This comparition is here given for the most complex tested platform, the ARM9 The test application chosen for this model validation are widely spread multimedia applications : MP3, JPEG, JPEG2000 and MPEG2. The implementations of these four applications are Linux standard libraries. Hence they use operating system services and standard libc functions. All experiments could have been made with Linux (or even uClinux), since the simulation tools are complete enough to run these operating systems. For limited measurement duration reasons, we decided to replace these heavy OS by a lightweight one, Mutek [START_REF] Pétrot | Lightweight Implementation of the POSIX Threads API for an On-Chip MIPS Multiprocessor with VCI Interconnect[END_REF]. Linux hardware layer abstraction makes interrupt request managment too long to allow a reasonable sized image or sound to be decoded in our measure time window. Four applications are executed in the simulation tools to get estimations of their execution.

Accuracy.

Results of model estimations and physical measurements are presented in table 3. The third column reports the physical measurement results, in terms of execution duration in CPU clock cycles and in terms of energy consumption in Joules. Fourth column gives the same kind of informations concerning the simulation results. Finally, the last column gives the percentile error of simulation errors of the simulation results against the physical measurement on the Table 3: Simulators results: the results obtained for execution time and energy consumption by real hardware measurement are shown in third column, the simulation ones in fourth column. The last column gives the error percentile of the simulation target hardware platform. These results show that a 10% error rate can be achieved by our complete platform energy model. These results validate that inter-instruction costs simplification is a reasonible choice to get fast yet precise estimations of the energy consumption. These estimations are obtained in roughly less than a minute (25s for the first simulation plus 20s for the second). We think that the error rate of 10% is largely acceptable in regard of the simulation time.

Conclusion

In this paper we have explained how an accurate energy consumption model for a full embedded system can be built from external measurements and microbenchmarks. Our methodology requires a prototype platform of comparable technology. Quantitative energy data are gathered at the battery output and are translated into per instruction energy figures by data analysis. The resulting model is thus driven by the embedded software activity and can be used with a simulation execution trace as input. It is thus possible to very easily add an energy estimator to a software functional simulator so as to get feedback at the source level. As simulation tools modifications are kept at a minimum the simulation speed is not impacted. Consumption data clearly identify power hungry operations, thus offering hints for software design tradeoffs. The model built on an ARM9 based development board using this methodology achieved an error rate of less than 10 % at the source level, which is acceptable compared to its simplicity of implementation and its fast running time.

Figure 1 :

 1 Figure 1: Multiple frequencies experiments: This figure shows that the energy per event increases linearly with the clock period (fixed voltage).

Figure 2 :

 2 Figure 2: Simulation tool architecture

Figure 3 :

 3 Figure 3: Linear Trace Example

Figure 3

 3 shows an exemple of linear trace output whereas figures 4 and 5 are respectively examples of annotated call graph and source code annotation visualization with KCachegrind.

Figure 4 :

 4 Figure 4: Call graph annoted with energy consumption information visualized thanks to KCachegrind

Figure 5 :

 5 Figure 5: Source code annotation visualization obtained with the KCachegrind tool

Table 1 :

 1

	Benchmarks results for simple operation energy calibration
	bench name	length energy (nJ) error (pJ)
	loop-calibration	4	69.084	5.1777
	insn-nop	1	16.747	1.2884
	AHB1-access	6	101.33	7.7132
	AHB2-access	18	300	22.998
	Dcache-access	1	17.146	1.3007
	mem-access	40	775.44	54.551
	spm-access	8	131.72	10.168
	timer-test on(nop)	1	16.754	1.2857

Table 2 :

 2 Linear regression from curves of Fig.1based on the formula 7 Benchmark name E rp base (nJ) E mc (nJ) error (pJ)

	insn-mul	10.91	26.37	572.36
	loop-calibration	10.52	19.22	258.90
	insn-nop	10.54	6.35	105.61
	access-AHB1	11.06	36.72	1085.37
	access-AHB2	11.06	106.32	3431.46