Maxime Cordy

Pierre-Yves Schobbens

Patrick Heymans

Axel Legay
email: axel.legay@inria.fr

Beyond Boolean Product-Line Model Checking: Dealing with Feature Attributes and Multi-Features Technical Report

Keywords: Software Product Lines, Numeric Features, Feature Cardinalities, Model Checking, Semantics, Tools 1 Sometimes misleadingly referred to as clones in the literature [13], [14]

Model checking techniques for software product lines (SPL) are actively researched. A major limitation they currently have is the inability to deal efficiently with non-Boolean features and multi-features. An example of a non-Boolean feature is a numeric attribute such as maximum number of users which can take different numeric values across the range of SPL products. Multi-features are features that can appear several times in the same product, such as processing units which number is variable from one product to another and which can be configured independently. Both constructs are extensively used in practice but currently not supported by existing SPL model checking techniques. To overcome this limitation, we formally define a language that integrates these constructs with SPL behavioral specifications. We generalize SPL model checking algorithms correspondingly and evaluate their applicability. Our results show that the algorithms remain efficient despite the generalization.

I. INTRODUCTION

Software Product Line (SPL) engineering is an increasingly widespread software development paradigm in which similar software products are designed and developed as a family to make economies of scale [START_REF] Pohl | Software product line engineering -foundations, principles, and techniques[END_REF]. A key challenge in SPL engineering is the management of the differences between the products, aka variability. Features are first-class abstractions to model and reason on variability. They specify characteristics that may be present or absent in a product. Relations between features, like parent-child, implication and exclusion, are usually captured in a feature model (FM). Since they were first introduced by Kang et al. in 1990 [START_REF] Kang | Featureoriented domain analysis (FODA) feasibility study[END_REF], FMs became more sophisticated. For detailed surveys of FM languages see, e.g., [START_REF] Schobbens | Feature Diagrams: A Survey and A Formal Semantics[END_REF], [START_REF] Classen | A text-based approach to feature modelling: Syntax and semantics of TVL[END_REF]. In this paper we use TVL [START_REF] Classen | A text-based approach to feature modelling: Syntax and semantics of TVL[END_REF], one of the latest incarnations of FMs, due to some of its advantages: high expressiveness, formal semantics and tool support. A TVL excerpt is given in Figure 1. TVL and the example are properly introduced in Section II.

Many SPLs are complex critical systems and variability is known to be the source of additional complexity. Therefore, efficient quality assurance is paramount. Model checking is an established automated technique for verifying system behaviour. As for single systems, model checking techniques for * FNRS research fellow SPLs are actively researched [START_REF] Apel | Featureinteraction detection using feature-aware verification[END_REF]- [START_REF] Gruler | Modeling and model checking software product lines[END_REF]. Our past work [START_REF] Classen | Model checking lots of systems: efficient verification of temporal properties in software product lines[END_REF]- [START_REF] Cordy | Simulation-based abstractions for software product-line model checking[END_REF] was concerned with one of the major challenges in SPL model checking: as the number of features grows, the number of products increases exponentially. We thus proposed various techniques for efficient SPL model checking. We introduced Featured Transition Systems (FTS), a mathematical formalism to model the behaviour of SPL products in a concise manner [START_REF] Classen | Model checking lots of systems: efficient verification of temporal properties in software product lines[END_REF]. We also designed efficient algorithms that identify which products exhibit undesired behaviour. However, FTS are a fundamental formalism, not meant to be used directly by engineers. We thus proposed high-level specification languages to be used on top of FTS, notably fPromela [START_REF] Classen | Model checking software product lines with SNIP[END_REF], an SPLspecific dialect of Promela [START_REF] Holzmann | The SPIN Model Checker: Primer and Reference Manual[END_REF]. Given the large number of different products in an SPL, it is unrealistic to describe their behaviour separately. Instead, our languages associate optional behaviour with features that must (not) be present to enable it.

A fundamental limitation of existing SPL model checking approaches, including ours, is that they do not deal with numeric features, nor features appearing several times in a product, viz. multi-features 1 . Numeric (as opposed to purely Boolean) features occur in FMs in the form of attributes associated with features. An example could be Maximum number of users which can take different numeric values across the range of products. The multi-feature construct could be used to represent, e.g., processing units which number is variable from one product to another and which can be configured independently. A recent survey, dubbed by our own experience, showed that engineers commonly need these constructs [START_REF] Hubaux | Evaluating a textual feature modelling language: four industrial case studies[END_REF]. To transfer of our model checking techniques to industry, we thus have to support them. Despite evidence of their usefulness in practice, no SPL modelling tool currently supports multi-features [START_REF] Classen | A text-based approach to feature modelling: Syntax and semantics of TVL[END_REF], and SPL model checking tools support neither numeric nor multi-features.

In this paper, we propose a combined formalism that integrates TVL with fPromela to model the behaviour of SPLs with numeric attributes and multi-features. With the addition of attributes, optional behaviour can be made dependent not only on the presence or absence of features, but also on the satisfaction of arithmetic constraints over attributes. This implies a generalization of the underlying formalism, viz. FTS, and its associated model checking algorithms. We implemented the complete method on top of SNIP, an FTS-based model checker [START_REF] Classen | Model checking software product lines with SNIP[END_REF]. The addition of arithmetic constraint solving naturally lead us to use Satisfiability Modulo Theory (SMT) solvers. Still, those are more computationally expensive than solutions for purely Boolean satisfiability. Our experiments show that while multi-feature support does not constitute a threat to performance, the use of SMT solvers to support attributes drastically increases verification time. We thus also propose an alternative solution where attributes are converted into sets of Boolean variables. This latter approach turns out to be more efficient.

Structure of the paper. Section II recalls the necessary background. In Section III we expose the challenges related to multi-features and define an extension of TVL that supports them through an array-based semantics. In Section IV, we define multi-features and attributes in fPromela. The implementation and evaluation are described in Section V. Related work is discussed in Section VI.

II. BACKGROUND

The necessary concepts and background are now recalled, most of them based on our running example which is first introduced.

A. Running Example

CFDP is a highly-configurable deep-space file transfer protocol [START_REF]CCSDS File Delivery Protocol (CFDP): Blue Book[END_REF]. In the past, our team helped Spacebel, a Belgian company, to develop an implementation of CFDP as an SPL [START_REF] Boucher | Tag and prune: A pragmatic approach to software product line implementation[END_REF]. The original CFDP FM has 98 features. Here, we consider a small subset of the protocol, i.e., the ack modes it offers. The corresponding sub-FM has 14 features and yields 1,058 different valid products. We had to limit ourselves to this subset because in addition to the variability, we had to model the behaviour of the protocol's features, which is far more complex. We did that based on the protocol specification [START_REF]CCSDS File Delivery Protocol (CFDP): Blue Book[END_REF] and experimented with various SPL behavioural modelling languages. This turned out to be a difficult and time-consuming activity. The resulting models describe a communication scenario where an entity (e.g., a spacecraft) has to transfer a message to another one. Depending on the features of the protocol's instance in each entity, properties like successful transmission may or may not be satisfied during the transaction. The final model has 1,812,652 states.

B. TVL

Figure 1 shows an excerpt of the TVL model of CFDP. The equivalent graphical representation appears on its right. In both representations, the FM's fundamental structure remains a tree that reflects the parent-child hierarchy between the features. At the top of the tree lies the root feature (CF DP ). The root is always part of a product, regardless of its other features. A feature may have child features; for instance, CF DP has three: Entity, M essage and Channel. Group cardinalities define how many children a feature may have in any given product. This construct is common in FM languages, including TVL. Here, it specifies that CF DP must have exactly three children, whereas Entity must have one or two.

Group cardinalities are not to be confused with feature cardinalities [START_REF] Czarnecki | Formalizing cardinality-based feature models and their specialization[END_REF], [START_REF] Michel | A formal semantics for feature cardinalities in feature diagrams[END_REF] which specify how many instances of a feature may exist in any given product. When no feature cardinality is given, as is the case for all features in the model except Entity, the feature is implicitly assumed to occur at most once in each product. But whenever there is a need to allow a feature to have multiple instances, an explicit cardinality is added to the feature itself (as opposed to the group); we call such a feature a multi-feature. In the excerpt, the only multi-feature is Entity. It has a feature cardinality of exactly 2; hence two instances of this feature exist in each product. In our scenario, each instance corresponds to one of the two communicating spacecrafts. Defining Entity as a multi-feature allows the two spacecrafts to bear a different configuration. If Entity was a normal feature, the spacecrafts should necessarily be identical. In reality, it is more likely that they are not.

Each instance of Entity must have at least one of the following child features: Snd min (sending capabilities) and Rcv min (receiving capabilities). Under Snd min and Rcv min lie additional features, which have been omitted in the figure. Features Rcv min and M essage both have an integer attribute. The attribute timeout determines the number of communication flaws that are allowed before aborting a communication while size models the number of data packets that must be sent for the transmission to end. Feature Channel has an optional child feature Reliable, which specifies whether or not the communication channel is reliable.

In addition to the specification of the tree structure, TVL allows the definition of additional constraints (i.e., Boolean formulae) over both the features and their attributes (omitted in the figure). The semantics of an FM is usually defined as the set of valid products, i.e. products whose features satisfy all the constraints defined by the FM [START_REF] Schobbens | Feature Diagrams: A Survey and A Formal Semantics[END_REF].

C. Featured Transition Systems (FTS)

FTS [START_REF] Classen | Model checking lots of systems: efficient verification of temporal properties in software product lines[END_REF] is the formalism at the core of our model checking approach. Its main advantage over competing approaches is that it uses an explicit notion of feature, which brings performance improvements and allows one to relate errors and undesired behaviours to the exact set of products where they occur. FTS are directed graphs whose transitions are annotated with feature expressions, i.e. Boolean formulae defined over the set of features. For instance, the feature expression M essage ∧ Channel represents the set of products that have the feature M essage and the feature Channel; ¬Reliable models the set of products that do not have the feature Reliable. A product is thus able to execute a transition iff its set of features satisfies the associated feature expression. A model-checking algorithm takes that information into account while looking for error states. It can thus keep track of which products are able to execute the currently analysed behaviour. Feature expressions constitute an intuitive and flexible way to represent variability in behavioural models. In their current form, FTS do not support expressions over multi-features and attributes. Formally, they are defined as follows.

Definition 1 An FTS is a tuple (S, Act, trans, I, AP, L, d, γ), where S is a set of states, Act is a set of actions, trans is a set of transitions, I is a set of initial states, AP is a set of atomic propositions, L labels each state with the propositions it satisfies, d is an FM, and γ associates each transition to a feature expression.

D. SPL Behavioural Specification in fPromela

There are two kinds of approaches to implement (or model) SPLs [START_REF] Kästner | Granularity in software product lines[END_REF]. Compositional methods capture the effects of features in isolated modules. A desired product is then obtained by composing the right set of modules. On the contrary, annotative approaches directly adorn code/models with constraints over the features, e.g., feature expressions. These annotations express that parts of the code/model are exclusive to the set of products satisfying the formulae.

fPromela [START_REF] Classen | Model checking software product lines with SNIP[END_REF] falls into the latter category. It is an executable language based on SPIN's input syntax [START_REF] Holzmann | The SPIN Model Checker: Primer and Reference Manual[END_REF]. In an fPromela model, the behaviour of each process is described in a proctype structure. Within a process, executable statements are expressed using constructs inspired by imperative programming. Each of these can be annotated with feature expressions, such that only the products satisfying a formula are able to execute the associated statement. Let us consider the excerpt shown in Figure 2. Features are declared as Boolean fields of a user-defined structure called features. In this model, two processes of type cfdp_entity are specified. At some point, the specification of a cfdp_entity splits into two parts: one for the products satisfying the feature expression Snd min and one for the others.

The semantics of an fPromela model is an FTS. Each process is first translated into an FTS. A state corresponds to a variable valuation and a node of execution. Transitions between states are determined according to the executable img/group_cardinalities2.pdf statements. Feature expressions labelling transitions are directly derived from the fPromela model. Once all the processes have been translated, the final FTS is obtained by computing their parallel composition [START_REF] Classen | Model checking software product lines with SNIP[END_REF].

(c) Group cardi- nalities (2)
An fPromela model may include behaviour that is executable by no valid product. Let us suppose that during an execution, the model goes through a transition annotated by feature Snd min then through one annotated by its negation. The resulting execution path is inconsistent because it requires both the presence and the absence of the feature. To avoid exploring this path, we use SAT solving methods which detect non-satisfiable formulae. Similarly, an execution path may require an invalid combination of features. It is consequently not a behaviour of the SPL since it cannot occur in any valid product. Such paths are avoided by checking the feature expression associated with the path of execution against the FM [START_REF] Classen | Model checking software product lines with SNIP[END_REF].

III. ARRAY-BASED SEMANTICS FOR MULTI-FEATURES

The syntax and the semantics of attributes in TVL are already defined but the language does not support multifeatures. To overcome this, we extended the syntax as follows: unless there is exactly one instance, the cardinalities are written between brackets next to the name of the feature (see Figure 1). Additional constraints over multi-features are described further in this section. For clarity, we name TVL * our new version of TVL. Before we give it a formal semantics, we have to deal with a number of issues.

A. Challenges in the Definition of Feature Cardinalities

As explained by Michel et al. [START_REF] Michel | A formal semantics for feature cardinalities in feature diagrams[END_REF], feature cardinalities introduce semantic ambiguities. When a non-terminal feature has a maximum cardinality greater than one, two ambiguities exist regarding its group cardinalities. For instance, consider the FM in Figure 3a and the two instances shown in Figure 3b. According to the feature diagram shown in the former figure, feature A has two instances and a group cardinality of [1..2] (only one or two child features of A may exist). However, it is unclear whether the group cardinalities apply locally under each instance of A or globally for all instances of A. In other words, either each instance can have one or two child features (left diagram in Figure 3b), or there must be one or two child features of A altogether (right diagram). Since our approach is centred on multi-features, we consider the local interpretation like Michel et al. [START_REF] Michel | A formal semantics for feature cardinalities in feature diagrams[END_REF].

The second ambiguity lies in the scope of group cardinalities; see Figure 3c. In the left diagram, cardinalities restrict the number of instances of A's child features. On the contrary, in the right diagram, the two instances of B under the leftmost instance of A are counted once; in this case, cardinalities constrain the number of distinct child features. Like Michel et al. [START_REF] Michel | A formal semantics for feature cardinalities in feature diagrams[END_REF], we believe that the original intent of group cardinalities is to restrict the number of features in a product; we thus consider the second option.

Multiple interpretations are also possible for feature cardinalities. Let us consider Figure 3d. As for group cardinalities, either feature cardinalities apply globally and count the total number of instances of a feature (left diagram), or they apply locally and count the number of instances of a feature under a specific instance of its parent feature (right diagram). As before, we adopt the most local option, i.e. the latter.

Another issue concerns the identification of a feature by means of its name. In FMs without multi-features, the (relative) name of a feature works as a unique reference to that feature. This is not the case for multi-features. Let us consider again the TVL * model of CFDP (Figure 1). The relative name Snd min can refer to a child feature of either the first instance of Entity or the second one. We have to identify this instance using an "absolute" name (called fully qualified). In TVL, however, no construct exists for referring to a precise instance. Moreover, the semantics proposed by Michel et al. defines the children of a feature as a multiset of instances [START_REF] Michel | A formal semantics for feature cardinalities in feature diagrams[END_REF]. One cannot refer to a precise element of a multiset in natural language. Our SPL behaviour specification language requires this capability; the definition of Michel et al. is thus inappropriate for our purpose.

We propose to represent the children of a feature by a set of arrays of instances. In a given array, all the instances are from the same feature. Each of them is identified by an index, the first index being zero. For example, the Snd min child feature of the second instance of Entity is identified by the fully qualified name CF DP [0].Entity [START_REF] Pohl | Software product line engineering -foundations, principles, and techniques[END_REF].Snd min[0]. When the maximum number of instances of a given feature is 1, the index can be omitted; CF DP.Entity [START_REF] Pohl | Software product line engineering -foundations, principles, and techniques[END_REF].Snd min is thus equivalent to the above name. An attribute of a given instance must be referred to using its fully qualified name as well, e.g., CF DP.M essage.size.

Since we introduce multi-features in the syntax of TVL * , we must provide means to specify constraints over them, their attributes, and their number. Fully qualified names are already suitable to refer to precise instances or attributes. However, it is currently impossible to reason over a whole array. For example, one cannot express that the number of instances of a feature must not exceed the value of another feature's attribute, or that every instance of a feature must satisfy a given constraint. To address this limitation, we define the operator card which, given a fully qualified multi-feature name, returns its number of instances. E.g., card(CFDP.Entity) always returns 2. We also define two new types of constraints: forall(m){φ} and exists(m){φ}. Intuitively, they specify that for each (resp. at least one) instance of a multifeature m, the sub-tree of this instance satisfies the constraint φ. For example, the constraint forall (CF DP.Entity) {Snd_min ∨ Rcv_min} is satisfied if and only if every instance of Entity has at least one child. As we will see, a notion of context is required for defining the semantics of such formulae.

The last challenge is related to constraints over attributes. If a feature is not part of a product, references to its attributes point to an unknown value. In this case, it is undetermined how the constraint must be evaluated. Our new types of constraints already provide a solution to that problem by specifying constraints within the context of a instance. The evaluation of a constraint is thus performed under the assumption that the instance exists within its context. Still, this issue makes such descriptions error-prone.

B. Abstract Syntax TVL *

Now that the new TVL * constructs have been informally introduced, we give them an abstract syntax and a formal semantics. Note that this abstract syntax remains valid for most feature modelling languages that support multi-features and attributes, and whose diagrams follow a tree structure. r,DE,ω,λ,A,ρ,τ,Φ) where F is a non-empty set of features, r ∈ F is the root, A is the set of attributes, and:

Definition 2 A TVL * model is a tuple (F,
• DE ⊆ F × F is the decomposition (hierarchy) relation between features. For any (f, f ) ∈ DE, f is the parent and f is the child feature. By children(f ) we denote the set of child features of f . • ρ : A → F is a total function that returns the feature declaring a given attribute. • τ : A → {int, bool} assigns a type to each attribute.

• Φ is a Boolean-valued expression over the features F and the attributes A, expressing additional constraints. Furthermore, each FM must satisfy the following wellformedness rules: r exists and is unique: ω(r) = (1, 1); any terminal feature f has no child:

λ(f ) = (0, 0); DE is acyclic, that is, n 1 , .., n k ∈ N • (n k , n 1 ) ∈ DE ∧ ∀i ∈ {1..k -1} • (n i , n i+1 ) ∈ DE.
The main difference between this new syntax and that of TVL [START_REF] Classen | A text-based approach to feature modelling: Syntax and semantics of TVL[END_REF] is the definition of ω. In the latter, ω was meant to identify optional features. Here, we make it more general since it defines the cardinality of a feature. Although this difference might seem thin at first sight, we already showed in Section III-A that it raises a number of important issues. The definition of Φ is also different here, as we have introduced a new operator and two new types of constraints. For convenience, we suppose that attributes are either integer or Boolean. Enumeration types can be mapped to integer and are thus implicitly supported too. The introduction of real attributes in the syntax is straightforward, but requires additional type checking. The current version of our tools (presented further in Section V) does not support them.

As explained in Section III-A, only a fully qualified name can be used to identify a specific instance or an attribute. Formally, it is a tuple of the form (f 0 , i 0 ), (f 1 , i 1 ), . . . , (f k , i k ) ∈ (F × N) k+1 or (f 0 , i 0 ), (f 1 , i 1 ), . . . , (f k , i k ), a ∈ (F × N) k+1 × A, respectively for an instance or an attribute. A fully qualified instance name must satisfy the following. (1) The first feature is the root indexed by 0: (f 0 , i 0 ) = (r, 0); (2) the decomposition hierarchy is respected:

∀j • 0 < j ≤ k • f k ∈ children(f k-1 ); (3)
each index satisfies the cardinalities of its associated feature:

∀j • 0 < j ≤ k • w(f j ) = (n, m) ⇒ 0 ≤ i j < m. A fully qualified attribute name (f 0 , i 0 ), (f 1 , i 1 ), . . . , (f k , i k )a is valid if and only if (f 0 , i 0 ), (f 1 , i 1 ), . . . , (f k , i k ) is valid and a is an actual attribute of f k : f k ∈ ρ(a)
. From now on, we assume the validity of every fully qualified name.

C. Formal Semantics

The purpose of TVL is to define the set of valid products in an SPL, i.e. the valid combinations of features and attribute values. We mentioned before that in SPLs without attributes and multi-features, a product is uniquely identified by a set of features. For reasons explained above, this representation is not appropriate when multi-features or attributes occur in the FM. Therefore we redefine a product as a couple (F, A) where F ⊆ (F ×N) + is a set of instances and A : (F ×N) + ×A → Z ∪ { , ⊥} is a partial function that associates attributes with values. We assume that all the attributes of any instance in F have a value defined by A:

∀(f 0 , i 0 ) . . . (f k , i k ) ∈ F, a ∈ A • f k = ρ(a) • ∀ (f 0 , i 0 ) . . . (f k , i k ), a ∈ dom(A).
Conversely, for any attribute whose value is defined, F must include the corresponding feature:

∀ (f 0 , i 0 ) . . . (f k , i k ), a ∈ dom(A) ⇒ ∀(f 0 , i 0 ) . . . (f k , i k ) ∈ F.
Although we could ignore these two assumptions, they simplify the definition of the semantics.

Definition 3 Let M = (F, r, DE, ω, λ, A, ρ, τ, Φ) be a TVL * model and p = (F, A) be a product. Then p is valid according to M , noted p |= M , if and only if, for (f 0 , i 0 ) . . . (f k , i k ) ∈ F:

• F contains the root: (r, 0) ∈ F;

• F respects the decomposition hierarchy:

(f k-1 , f k ) ∈ DE;
• every instance in F has its parent in F as well:

(f 0 , i 0 ) . . . (f k-1 , i k-1 ) ∈ F; • F satisfies the group cardinalities: λ(f k ) = (n, m) ⇒ n ≤ |{(f 0 , i 0 ) . . . (f k , i k )(f k+1 , 0) ∈ F}| ≤ m;
• the ith instance of a feature exists only if the i-1th does:

i k > 0 ⇒ (f 0 , i 0 ) . . . (f k , i k -1) ∈ F; • F satisfies the feature cardinalities: ω(f k ) = (n, m) ⇒ i k < m ∧ n > 0 ⇒ (f 0 , i 0 ) . . . (f k , n -1) ∈ F ; • p satisfies the additional constraints Φ.
We consider that instances are contiguously placed in arrays, which simplifies the verification of multi-features and constraints over them.

Due to lack of space, we do not provide all the satisfaction rules for the additional constraints. However, we detail them for the constructs we have added. As explained above, the constraints of the form forall(m){φ} and exists(m){φ} introduce the notion of context, i.e., a sub-tree of the model. For the context to be well-defined, it is sufficient to know the instance it refers to.

Definition 4 Let M = (F, r, DE, ω, λ, A, ρ, τ, Φ) be a TVL * model. Then (f 0 , i 0 ) . . . (f k , i k ) ∈ (F × N) + is a context of M if it is a valid fully qualified feature name.
The initial context is the root feature. A product p = (F, A) must thus satisfy the additional constraints Φ in the context (r, 0): p |= (r,0) Φ. The context changes only when one of the above two constructs are encountered:

p |= c forall(m){φ} ⇔ ∀(c, m, i) ∈ F • p |= (c,m,i) φ, p |= c exists(m){φ} ⇔ ∃(c, m, i) ∈ F • p |= (c,m,i) φ.
Here, c merely acts as a prefix for features name. References to multi-features can occur in constraints, and express that at least one instance of the feature exists. Given our convention about array contiguity, this boils down to requiring the presence of the instance at index 0: p |= c m ⇔ (c, m, 0) ∈ F. As in TVL [START_REF] Classen | A text-based approach to feature modelling: Syntax and semantics of TVL[END_REF], the semantics of some constraints depend on the evaluation of arithmetic expressions, variables, or operators. For our new card operator, the evaluation is given by: [[card(m)]] c = |{(c, m, i) ∈ F}|. If the card operator is compared to a constant value v then the constraint can be reduced to a Boolean form:

p |= c card(m) ≥ v ⇔ (c, m, v -1) ∈ F (1)
We will also make use of this property to reduce the cost of verifying these constraints in behavioural specifications.

IV. A BEHAVIOURAL SPECIFICATION LANGUAGE FOR MULTI-FEATURES AND ATTRIBUTES

The semantics of TVL * allows us to determine which combinations of features constitute valid products. Still, we need a way to express the behaviour of these products in a concise (i.e., not individual) manner. Based on the principles of TVL * , we generalize fPromela with feature expressions supporting multi-features and attributes. Then we can verify models of this language against properties using a model checking tool (described in Section V). We name our extension fPromela * . fPromela * extends fPromela's syntax with more general data types for representing features. For example, the data structure defined for the Entity feature would be: The first field of a structure is a Boolean called is_in. Its truth value defines the presence or the absence of a feature. The structures can be nested. Hence if, say, Snd min is not a terminal feature, we can declare it as an instance of another structure. Attributes are declared as integer fields. More generally, there exists a transformation from a TVL * model to a set of fPromela * data structures. Each data structure represents a non-terminal feature, and contains one field per attribute and child feature. The type of the latter is either Boolean or another data structure, respectively if the feature is terminal or not. When the maximum cardinality of a feature is 1 < m < ∞, the feature must be declared as an m-sized array of its corresponding type: Because fPromela does not allow arrays of an unknown size, the transformation does not support infinite maximum cardinality (represented as a * in TVL * ). However, we may assume that in real cases, an upper bound can be defined.

Unlike in fPromela, the use of nested user-defined structures is compulsory in fPromela * . Indeed, a fully qualified name is required to refer to an instance (see Section III-A). fPromela * offers a simple way to represent valid fully qualified names: references to fields of the corresponding user-defined structures, starting from that of the root feature. For example, the Snd min child feature of the second instance of Entity is uniquely referred to by CFDP.Entity [START_REF] Pohl | Software product line engineering -foundations, principles, and techniques[END_REF].Snd_min. fPromela * generalizes feature expressions as well. We distinguish between static and dynamic formulae. The former specify one of the following requirements: (1) the presence or absence of a given instance (e.g., CFDP.Entity [START_REF] Pohl | Software product line engineering -foundations, principles, and techniques[END_REF].Snd_min); (2) constraints over attributes (e.g., CFDP.Message.size>0); and (3) constraints over number of instances (e.g., card(CFDP.Entity)==2). As in TVL * , the third type of constraints is subsumed by the first one when card is compared to integers (see Equation 1). We can determine the products able to execute a transition associated with a static formula without executing the fPromela * model.

On the contrary, dynamic formulae are evaluated at runtime. Typically, they define constraints over attributes and number of instances in terms of variable values. For example, one could analyse the content of a CFDP message by iterating on its size: i = 0; do :: CFDP.Message.size > i -> ... i++; :: e l s e -> break; od;

Note that for a given product, the actual size of the above model (in terms of states) depends on the value of the attribute in the product. Attributes in fPromela * are thus the key for specifying variable-size models. Instead of attributes, we could also use the number of instances of a feature. In Section V, we show that it is more efficient to verify a variable-size model rather than a set of fixed-size models, i.e. one per possible size.

Let us illustrate the last addition of fPromela * by means of the CFDP model. As mentioned before, two processes are declared and model the behaviour of two spacecrafts. These may have different configurations. In the partial model shown in Figure 2, however, we find but an ambiguous reference to feature Snd min. We have seen that the introduction of multifeatures permits the distinction between the features of the two entities. Still, we need a way to associate each process with the corresponding instance of Entity. To that aim, we define the feature context of a process as an instance of a feature. We propose two constructs to associate a context to a process. The first specifies it explicitly in the run statement of fPromela, which is used to dynamically instantiate a new process: run [CFDP.Entity [START_REF] Pohl | Software product line engineering -foundations, principles, and techniques[END_REF]] cfdp_entity(...)

The second method consists in declaring that the number of instances of a process is equal to the number of instances of a specific feature: a c t i v e [ c a r d ( CFDP . E n t i t y ) ] c f d p e n t i t y ( . . . )

In this case, the context of each instance of cfdp_entity is a distinct instance of Entity. A process cannot exist outside its associated context. Accordingly, the first transition of a process is implicitly constrained by the formula representing its context. Once defined, contexts can act as a prefix in feature expressions. For this purpose, one may use the keyword this, which points to the context of the process: i f :: this.Snd_min -> ...

:: e l s e -> ... f i ;

References to features outside the context are still possible by using fully qualified names.

More generally, one can regard contexts as an association between an fPromela * process and a FM. Thanks to them, one can describe the behaviour of parallel processes built from different SPLs. Analysing the behaviour of compositions of SPLs rather than individual SPLs is thus made possible. However, this remains out of the scope of this paper and is left for future work.

In [START_REF] Classen | Model checking software product lines with SNIP[END_REF], we defined the semantics of an fPromela model as an FTS. Since apart from feature expressions, fPromela * does not differ from fPromela, its semantics can be defined in terms of FTS where feature expressions have been generalized. We call the resulting formalism FTS * .

V. IMPLEMENTATION AND EVALUATION

Since the semantics of an fPromela * is an FTS, we may reuse algorithms based on this formalism [START_REF] Classen | Model checking lots of systems: efficient verification of temporal properties in software product lines[END_REF]- [START_REF] Cordy | Simulation-based abstractions for software product-line model checking[END_REF]. We describe how we implemented the approach on top of SNIP [START_REF] Classen | Model checking software product lines with SNIP[END_REF], which we further used to carry out experiments.

A. Tool Description

SNIP is a model checker based on the FTS formalism. Figure 4 gives an overview of its architecture. Given an fPromela model, the parser builds a program graph representing it. The semantic engine generates on-the-fly the FTS equivalent to the program graph. The verifier module checks the FTS using dedicated algorithms [START_REF] Classen | Model checking lots of systems: efficient verification of temporal properties in software product lines[END_REF], [START_REF] Cordy | Simulation-based abstractions for software product-line model checking[END_REF]. Feature handler abstracts feature formulae from their representations, whereas feature solver checks their satisfiability. The TVL library is used to compute the feature formula representing the valid products of a TVL model.

No change to the verifier module is required since it is independent of how feature formulae are represented. On the contrary, we extended or built new variants of the other modules. We updated the parser so that feature formulae are declared and referenced as user-defined data structures. We also relaxed syntactic constraints for feature formulae and modified the construction of program graphs accordingly. Dynamic formulae are handled by the semantic engine, which builds them at runtime.

Given that more general feature formulae are allowed, the previous feature handler and checker are not appropriate anymore. Both the representation and satisfiability checking of features were based on Binary Decision Diagrams (BDDs) [START_REF] Bryant | Symbolic boolean manipulation with ordered binarydecision diagrams[END_REF] and their implementation in the CUDD library 2 . While BDDs have proven their efficiency in SNIP [START_REF] Classen | Model checking software product lines with SNIP[END_REF], they are unable to represent arithmetic constraints. Multi-features alone are not a problem in this regard but feature attributes are not necessarily Boolean. Satisfiability Modulo Theory (SMT) solvers appear as natural candidates for arithmetic constraints checking. Accordingly, our new feature solver is linked to Microsoft's Z3 [START_REF] Moura | Z3: an efficient smt solver[END_REF]. Z3 implements many advanced techniques and structures for SMT solving. We thus implemented a new feature handler that relies on them. Equipped with Z3, our tool is able to check the satisfiability of formulae over both the features and their attributes. However, this comes at the price of a significant reduction in efficiency, as further experiments reveal. Consequently, we developed two variants of the tool: one equipped with CUDD and the other with Z3; the former supports only multi-features whereas the latter handles attributes as well. They are included in the last version of SNIP (http:// info.fundp.ac.be/ fts/ snip).

B. Overhead Measurement

We carried out experiments to evaluate the benefits of our approach, and to quantify the overhead that results from the additional verifications (see above) and/or the use of Z3 in place of BDD-based satisfiability solvers. The following tools are involved in the experiments: SNIP (as described in [START_REF] Classen | Model checking software product lines with SNIP[END_REF]), our BDD-based variant that supports multi-features (SNIP-MF), and our second variant equipped with Z3 (SNIP-Z3).

The addition of multi-features to fPromela * generates additional computations in the semantic engine of SNIP. Moreover, feature attributes require more general satisfiability-checking techniques, i.e., SMT solvers. These two generalizations are likely to negatively impact the performance of our tool. To quantify the resulting loss, we compare the time needed to model check three fPromela models against five properties each. The models include neither multi-features nor attributes. They are: (1) a minepump system [START_REF] Classen | Model checking lots of systems: efficient verification of temporal properties in software product lines[END_REF], [START_REF] Kramer | Conic: an integrated approach to distributed computer control systems[END_REF] (250,561 states to explore); (2) a restricted version of CFDP where attributes have received a fixed value and the two instances of Entity are regarded as a single feature (1,801,581 states to explore);

(3) an elevator model inspired from Plath and Ryan [START_REF] Plath | Feature integration using a feature construct[END_REF] (58,945,690 states to explore). We checked different kinds of properties including deadlock freedom, safety properties, and liveness properties. All benchmarks were run on a MacBook Pro with a 2,8 GHz Intel Core i7 processor and 8 GB of DDR3 RAM. We coded an automated script to execute them. To avoid random variations, we repeated each experiment several times I. We observe that multi-feature support in our BDD-based tool generates but a small increase in verification time (between 2% and 18% for Minepump; between 0% and 5% for CFDP; between 1% and 12% for Elevator). This increment does not depend on the size of the model. In every model, the increase is less than 6% for longestto-check properties. This indicates that the size of the property has no impact on the loss of performance either.

On the contrary, the Z3 variant suffers from a large performance drop. In Minepump and CFDP, the checking time ranges from to 31 times more than for the other two tools. The tool performs even worse on Elevator: the verification time is multiplied by a factor between 468 and 962. For the first and fifth properties of that model, we could not even get accurate results; according to our estimations, verifying those properties would take 24 and 15 hours, respectively. Our SMTbased tool does not scale well with the size of the model.

We carried out further analyses to explain this phenomenon. For each tool, we computed the time required for satisfiability checking and formulae manipulation (i.e., conjunction, disjunction, negation, simplification) during each experiment. In Table II we provide the time share of the two computations in percentage, for every model and property.

For SNIP and SNIP-MF, the absolute time needed for satisfiability checking (Sat) and formulae manipulation (Man) are identical. Indeed, given that all the models are free from multi-feature and attribute, the only difference between the two tools are the detection of dynamic formulae, which does not depend on Sat or Man. For these tools, it turns out that Sat constitutes but a small part of the total time (between 6% and 15%). Although this share tends to slightly increase with the size of the model, it is not a major threat to scalability. On the contrary, Man is an increasingly important part of the total time. While the time share does not grow significantly between Minepump and CFDP, it nearly doubles in the Elevator case, ranging from 38% to 53%. This indicates that managing a large number of BDDs is the main challenge for efficient BDDbased tools.

TABLE II: Share of verification time due to satisfiability checking and formula manipulation (in percentage).

In the third tool, Sat is the most costly computation. Its share is already between 73% and 82% for Minepump and CFDP, and reaches astonishing proportions in the Elevator case (about 95%). This clearly shows that expensive satisfiability checking threatens scalability. We measured the average time for a Sat computation. It amounts to 6.59 * 10 -4 seconds for SNIP-Z3 as opposed to 3.36 * 10 -7 in BDD-based tools. In every model and property, the remaining computation time is due to feature manipulations for the most part. The average time of these is 1.62 * 10 -5 seconds -as opposed to 3.68 * 10 -7 in the other tools. Together, Sat and Man always make up more than 92% of the overall verification time, and even over 95.5% in Elevator.

In our context, SMT-based solutions thus appear less efficient than BDDs. This has to be confirmed through the replacement of Z3 by other SMT solvers. Indeed, Z3 offers many facilities that we do not need. Using another solver specifically designed for our purpose might yield better results. We leave that for future work. Nevertheless, the poor performance raises the need for alternatives to SMT.

C. Explicit Attributes versus Boolean Conversion

As an alternative to Z3, we propose to transform integer attributes into a set of Boolean variables, i.e., one per attribute value. This results in a model without attribute, which can thus be checked by SNIP-MF. Each time a constraint over attributes is encountered in an fPromela * model, it is first re-written in a form where only Boolean negation and greater operators occur. For instance, the constraint CF DP.M essage.size <= 3 is converted into ¬(CF DP.M essage.size > 3). Then, a Boolean variable representing that constraint is created and replaces it. While this solution avoids the overhead of SMT solving, it reduces the performance of SNIP-MF because more variables have to be dealt with.

The following experiments aim at evaluating whether this is more efficient than the Z3-based solution. We consider the complete CFDP model and compare the time needed by ). This corroborates our previous results and tends to show that in our context, attributes conversion is more viable than SMT. This has to be confirmed through additional experiments with more specific SMT solvers, though.

D. Variable-Size Models

In Section IV, we mentioned that multi-features and attributes can represent variable-size models. Our new tools have thus the capability to verify in a single execution a set of models varying only by their size. They avoid redundant checking of common parts of these models, and are thus potentially more efficient. However, multi-feature support has an impact of performance. We must therefore evaluate if the avoidance of redundancy offsets the loss in efficiency.

We consider the sieve of Eratosthenes modelled in fPromela * . The size of the model is determined by the number of primes to compute. We compare the performance of (1) SNIP applied on models where the number of primes is fixed, and (2) SNIP-MF executed on a model where this number is equal to the number of instances of a feature. For a maximum number n, we compute the time needed by SNIP for successively checking models with 1 to n numbers to compute. Then, we execute SNIP-MF on the variable-size model.

Figure 5a shows the resulting verification times for n ranging from 30 to 48, whereas Figure 5b presents the number of explored states. Although the checking time always grows exponentially, it turns out that SNIP-MF performs increasingly better than SNIP. As illustrated in Figure 5b, this is because the former explores fewer and fewer states than the latter. However, we observe that for SNIP-MF, the verification time raises more rapidly than the number of explored states; the overhead due to multi-features has again a visible impact on the overall performance. Moreover, the benefit might not always exist. When the largest model has significantly more states than the smaller ones, the time needed to check these is negligible. In such cases, SNIP-MF might not be more efficient than SNIP applied on each model size.

VI. RELATED WORK

Other SPL model checkers equipped with specification languages exist. Plath and Ryan [START_REF] Plath | Feature integration using a feature construct[END_REF] designed fSMV in the context of feature interaction detection. This is a compositional language where features are described in separate modules. We previously developed an fSMV model checker [START_REF] Classen | Symbolic model checking of software product lines[END_REF]. Gruler et al. [START_REF] Gruler | Modeling and model checking software product lines[END_REF] extended the CCS process algebra with a variability operator that models alternative choices. Their language is however less human-readable than fPromela. Apel et al. [START_REF] Apel | Featureinteraction detection using feature-aware verification[END_REF] developed SPLVerifier, a tool chain for product-line model checking. Features are specified in separate modules written in C or Java. The framework of Asirelli et al. [START_REF] Asirelli | Formal description of variability in product families[END_REF] centred on modal transition systems does not include high-level specification languages. None of the above considers attributes and multi-features.

A few attempts to reason on FM with attributes and multifeatures exist. Czanercki et al. [START_REF] Czarnecki | Formalizing cardinality-based feature models and their specialization[END_REF] define the semantics of an FM with feature cardinalities as the semantics of a context-free grammar derived from the FM. Michel et al. [START_REF] Michel | A formal semantics for feature cardinalities in feature diagrams[END_REF] defined another semantics based on multisets. Czarnecki and Kim [START_REF] Czarnecki | Cardinality-based feature modeling and constraints: a progress report[END_REF] argue that OCL is suitable for expressing additional constraints over multi-features. Mazo et al. [START_REF] Mazo | Transforming attribute and clone-enabled feature models into constraint programs over finite domains[END_REF] use constraint logic programming to reason on FMs with multi-features and attributes. However, their procedure relies on a heavyweight transformation from visual FMs to XML, then to Gnu-Prolog's input syntax. Zhang et al. [START_REF] Zhang | A bdd-based approach to verifying clone-enabled feature models' constraints and customization[END_REF] propose a BDD-based approach for reasoning over multi-features. However, it does not support attributes and does not rely on an array-based semantics. A broader survey of feature cardinality analyses is found in [START_REF] Michel | A formal semantics for feature cardinalities in feature diagrams[END_REF].

SMT solvers are increasingly used in model checking. They have proven their usefulness in bounded model checking and verification of infinite-state and array-based systems [START_REF] Ghilardi | Mcmt: A model checker modulo theories[END_REF]. We showed that SPL model checking is another interesting application domain for SMT solvers. However, they have to be combined with heuristics in order to provide an acceptable level of performance in our context.

VII. CONCLUSION

We dealt with feature cardinalities and numeric features in SPL model checking. Multi-features and feature attributes have received little support, be it in FMs or behavioural specification languages. These constructs pose many problems of both theoretical and technical nature. Nonetheless, the definition of languages supporting them is essential. Both constructs are useful in terms of expressiveness, conciseness, and readability. In a behaviour specification, they allow the definition of variable-size models. Our experiments showed that it is easier to verify such models than successively checking the same model with different sizes. Multi-features are also useful for specifying parallel processes that differ by their configuration. To deal with them, we introduced the notion of feature context for parallel processes. More generally, contexts can relate parallel process with different FMs. Combined with feature-model composition [START_REF] Acher | Composing feature models[END_REF], this result opens the way for behavioural verification of SPL compositions. This is an interesting direction for our future work.

Handling attributes in SPL model checking is difficult. SMT solvers appeared as natural candidates to represent and reason over numeric feature formulae. However, our experiments with Microsoft's Z3 revealed that the overhead of SMT satisfiability checking is too important, which forced us to consider alternatives like converting attributes into Boolean variables. Yet, we need but a small subset of Z3's capabilities. Another solver optimised for our purpose could perform better. A complementary solution is not to check feature formulae each time it is needed. This leads to exploring more states than necessary but reduces the number of calls to the solver.

Moreover, Boolean conversion is not always practical. The behavioural models we considered do not include quantitative aspects like real-time or cost/rewards. Feature attributes in these contexts likely represent more complex forms of variability, e.g., data throughput, processor speed, or energy consumption. Model checking such SPLs requires the combination of this work with quantitative formalisms like Featured Timed Automata [START_REF] Cordy | Behavioural modelling and verification of real-time software product lines[END_REF]. This is non-trivial; several theoretical issues like decidability are expected. On the technical side, the use of SMT solvers might be a mandatory step. Still, it constitutes an interesting problem and we will most likely pursue our work in that direction.

Fig. 1 :

 1 Fig. 1: A subset of the CFDP feature model, shown in TVL and in a feature diagram.

Fig. 2 :

 2 Fig. 2: Partial CFDP model.

Fig. 3 :

 3 Fig. 3: Ambiguities introduced by feature cardinalities.

  • ω : F → N × (N ∪ { * }) gives the cardinality of each feature. If ω(f ) = (n, m) then n is the minimum cardinality of f and m its maximum cardinality. If m = * then m can be any finite value. • λ : F → N × (N ∪ { * }) indicates the decomposition operator of a feature, i.e., its group cardinalities. It follows the same pattern as ω.

  t y p e d e f _Entity { b o o l is_in; b o o l Snd_min; b o o l Rcv_min };

t y p e d e f f e a t u r e

Fig. 4 :

 4 Fig. 4: Architecture of SNIP.

Fig. 5 :

 5 Fig. 5: Benchmark results for the sieve of Eratosthenes.

TABLE I :

 I Verification times (in seconds).

		SNIP	SNIP-MF	SNIP-Z3
	Minepump #1	2.72	3.21 (+18%)	78.22 (+2,776%)
	Minepump #2	2.88	2.95 (+2%)	67.86 (+2,256%)
	Minepump #3	4.90	5.47 (+12%)	88.63 (+1,709%)
	Minepump #4	2.96	3.42 (+16%)	65.72 (+2,120%)
	Minepump #5	9.22	9.76 (+6%)	197.43 (+2,041%)
	CFDP #1	10.96	11.00 (+1%)	282.47 (+2,477%)
	CFDP #2	2.23	2.41 (+2%)	63.37 (+2,741%)
	CFDP #3	1.11	1.11 (+0%)	25.62 (+2,208%)
	CFDP #4	3.82	4.00 (+5%)	113.36 (+2,867%)
	CFDP #5	17.58	18.52 (+5%)	548.98 (+3,023%)
	Elevator #1	286.50	301.10 (+5%)	TIMEOUT
	Elevator #2	9.53	10.47 (+10%)	9,172.05 (+96,144%)
	Elevator #3	7.07	7.90 (+12%)	3,316 (+46,799%)
	Elevator #4	3.5	3.55 (+1%)	1,858.65 (+53,004%)
	Elevator #5	235.67	252.94 (+7%)	TIMEOUT
	and computed the average.
	Results are shown in Table

TABLE III :

 III Verification times for the CFDP example (in seconds). Z3 and SNIP-MF to perform the verifications. Results are shown in TableIII. It turns out that the transformation implemented in SNIP-MF yields far better results than SNIP-Z3. We observe a speedup ranging from 91.82 to 170.79. Interestingly, apart from Property #1 the difference in speed increases as the properties are longer to check (see in particular Property #5

		SNIP-MF	SNIP-Z3	Speedup
	#1	9.79	898.88	91.82
	#2	2.72	345.86	127.15
	#3	1.35	137.05	101.51
	#4	12.24	1694.61	138.45
	#5	21.44	3661.89	170.79
	SNIP-

ACKNOWLEDGEMENTS

We thank Philippe Warnon and Raphael Michel for their suggestions regarding TVL * 's syntax, as well as Andreas Classen for proofreading. This work was funded by the Fund for Scientific Research -FNRS in Belgium (project FC 91490).


Van Chan Ngo
email: chan.ngo@inria.fr

Jean-Pierre Talpin
email: jean-pierre.talpin@inria.fr

Thierry Gautier
email: thierry.gautier@inria.fr

Translation Validation for Synchronous Data-flow Specification in the SIGNAL Compiler

Keywords: Value-Graph, Graph Transformation, Formal Verification, Translation Validation, Certified Compiler, Synchronous Programs. Signal Program

We present a method to construct a validator based on translation validation approach to prove the value-equivalence of variables in the Signal compiler. The computation of output signals in a Signal program and their counterparts in the generated C code is represented by a Synchronous Data-flow Value-Graph (Sdvg). The validator proves that every output signal and its counterpart variable have the same values by transforming the Sdvg graph.

Introduction

A compiler is a large and very complex program which often consists of hundreds of thousands, if not millions, lines of code, and is divided into multiple sub-systems and modules. In addition, each compiler implements a particular algorithm in its own way. Consequently, that results in two main drawbacks regarding the formal verification of the compiler itself. First, constructing the specifications of the actual compiler implementation is a long and tedious task. Second, the correctness proof of a compiler implementation, in general, cannot be reused for another compiler.

To deal with these drawbacks of formally verifying the compiler itself, one can prove that the source program and the compiled program are semantically equivalent, which is the approach of translation validation [START_REF] Pnueli | Translation Validation[END_REF][START_REF] Pnueli | Translation validation: From Signal to C. In Correct Sytem Design Recent Insights and Advances[END_REF][START_REF] Blazy | Which C Semantics to Embed in the Front-end of a Formally Verified Compiler?. Tools and Techniques for Verification of System Infrastructure[END_REF]. The principle of translation validation is as follows: for a given input sample, the source and the compiled programs will give corresponding execution traces. These traces are equivalent if they have the same observation. An observation is a sequence (finite or infinite) of values (e.g., values of variables, arguments, returned values,...). The compilation is correct if for any input, the source and the compiled programs have observationally equivalent execution traces.

In this work, to adopt the translation validation approach, we use a valuegraph as a common semantics to represent the computation of variables in the source and compiled programs. The "correct transformation" is defined by the assertion that every output variable in the source program and the corresponding variable in the compiled program have the same values.

Signal [START_REF] Benveniste | Hybrid dynamical systems theory and the Signal language[END_REF][START_REF] Gautier | Signal, a declarative language for synchronous programming of real-time systems[END_REF] is a polychronous data-flow language that allows the specification of multi-clocked systems. Signal handles unbounded sequences of typed values (x(t)) t∈N , called signals, denoted as x. Each signal is implicitly indexed by a logical clock indicating the set of instants at which the signal is present, noted C x . At a given instant, a signal may be present where it holds a value, or absent where it holds no value (denoted by ⊥). Given two signals, they are synchronous iff they have the same clock. In Signal, a process (written P or Q) consists of the synchronous composition (noted |) of equations over signals x, y, z, written x := y op z or x := op(y, z), where op is an operator. Equations and processes are concurrent.

A Synchronous Data-flow Value-Graph symbolically represents the computation of the output signals in a Signal program and their counterparts in its generated C code. The same structures are shared in the graph, meaning that they are represented by the same subgraphs. Suppose that we want to show that an output signal and its counterpart have the same values. We simply need to check that whether they are represented by the same subgraphs, meaning they are label the same node. We manage to realize this check by transforming the graph using some rewrite rules, which is called normalizing process.

Let A and C be the source program and its generated C code. Cp denotes the unverified Signal compiler which compiles A into C = Cp(A) or a compilation error. We now associate Cp with a validator checking that for any output signal x in A and the corresponding variable x c in C, they have the same values (denoted by x = x c ). We denote this fact by C ⊑ val A. The main components of the validator are depicted in Fig. 1. It works as follows. First, a shared value-graph that represents the computation of all signals and variables in both programs is constructed. The value-graph can be considered as a generalization of symbolic evaluation. Then, the shared value-graph is transformed by applying graph rewrite rules (the normalization). The set of rewrite rules reflexes the general rules of inference of operators, or the optimizations of the compiler. For instance, consider the 3-node subgraph representing the expression (1 > 0), the normalization will transform that graph into a single node subgraph representing the value true, as it reflexes the constant folding. Finally, the validator compares the values of the output signals and the corresponding variables in the C code. For every output signal and its corresponding variable, the validator checks whether they point to the same node in the graph, meaning that their computation is represented by the same subgraph. Therefore, in the best case, when semantics has been preserved, this check has constant time complexity O(1). In fact, it is always expected that most transformations and optimizations are semantics-preserving, thus the best-case complexity is important.

Fig. 1: Sdvg Translation Validation Architecture

This work is a part of the whole work of the Signal compiler formal verification. Our approach is that we separate the concerns and prove each analysis and transformation stage of the compiler separately with respect to ad-hoc datastructures to carry the semantic information relevant to that phase.

The preservation of the semantics can be decomposed into the preservation of clock semantics at the clock calculation and Boolean abstraction phase, the preservation of data dependencies at the static scheduling phase, and valueequivalence of variables at the code generation phase. Fig. 2 shows the integration of this verification framework into the compilation process of the Signal compiler. For each phase, the validator takes the source program and its compiled counterpart, then constructs the corresponding formal models of both programs. Finally, it checks the existence of the refinement relation to prove the preservation of the considered semantics. If the result is that the relation does not exist then a "compiler bug" message is emitted. Otherwise, the compiler continues its work. The remainder of this paper is organized as follows. In Section 2, we consider the formal definition of Sdvg and the representation of a Signal program and its generated C code as a shared Sdvg. Section 3 addresses the mechanism of the verification process based on the normalization of a Sdvg. Section 4 illustrates the concept of Sdvg and the verification procedure. Section 5 terminates this paper with some related work, a conclusion and an outlook to future work.

Synchronous Data-flow Value-Graph

Let X be the set of all variables which are used to denote the signals, clocks and variables in a Signal program and its generated C code, and F be the set of function symbols. In our consideration, F contains usual logic operators (not, and, or), numerical comparison functions (<, >, =, <=, >=, /=), numerical operators (+, -, * , /), and gated φ-function [START_REF] Ballance | The Program Dependence Web: A Representation Supporting Control, Data, and Demand Driven Interpretation of Imperative Languages[END_REF]. A gated φ-function such as x = φ(c, x 1 , x 2 ) represents a branching in a program, which means x takes the value of x 1 if the condition c is satisfied, and the value of x 2 otherwise. A constant is defined as a function symbol of arity 0. A subgraph rooted at a node is used to describe the computation of the corresponding element labelled at this node. In a graph, for a node labelled by y, the set of clocks, signals or variables m N (y) = {x 0 , ..., x n } is written as a node with label {x 0 , ..., x n } y.

SDVG of SIGNAL Program

Let P be a Signal program, we write X = {x 1 , ..., x n } to denote the set of all signals in P which consists of input, output, state (corresponding to delay operator) and local signals, denoted by I, O, S and L, respectively. For each x i ∈ X, D xi denotes its domain of values, and D ⊥ xi = D xi ∪ {⊥} is the domain of values with the absent value. Then, the domain of values of X with absent value is defined as follows:

D ⊥ X = n i=1 D xi ∪ {⊥}.
For each signal x i , it is associated with a Boolean variable x i to encode its clock at a given instant t (true: x i is present at t, false: x i is absent at t), and x i with the same type as x i to encode its value. Formally, the abstract values to represent the clock and value of a signal can be represented by a gated φ-function, x i = φ( x i , x i , ⊥).

Assume that the computation of signals in processes P 1 and P 2 is represented as shared value-graphs G 1 and G 2 , respectively. Then the value-graph G of the synchronous combination process P 1 |P 2 can be defined as G = N, E, I, O, m N in which for any node labelled by x, we replace it by the subgraph that is rooted by the node labelled by x in G 1 and G 2 . Every identical subgraph is reused, in other word, we maximize sharing among graph nodes in G 1 and G 2 . Thus, the shared value-graph of P can be constructed as a combination of the sub-valuegraphs of its equations.

A Signal program is built through a set of primitive operators. Therefore, to construct the Sdvg of a Signal program, we construct a subgraph for each primitive operator. In the following, we present the value-graph corresponding to each Signal primitive operator.

Stepwise Functions Consider the equation using the stepwise functions y := f (x 1 , ..., x n ), it indicates that if all signals from x 1 to x n are defined, then the output signal y is defined by the result of the function f on the values of x 1 , ..., x n . Otherwise, it is assigned no value. Thus, the computation of y can be represented by the following gated φ-function:

y = φ(ŷ, f ( x 1 , x 2 , ..., x n ), ⊥), where ŷ ⇔ x 1 ⇔ x 2 ⇔ ... ⇔ x n (
since by definition they are synchronous). The graph representation of the stepwise functions is depicted in Fig. 3. Note that in the graph, the node labelled by { x 1 , ..., x n } ŷ means that m N (ŷ) = { x 1 , ..., x n }. In other words, the subgraph representing the computation of ŷ is also the computation of x 1 , ..., and x n . Merge Consider the equation which corresponds to the merge operator y := x default z. If the signal x is defined then the signal y is defined and holds the value of x. The signal y is assigned the value of z when the signal x is not defined and the signal z is defined. When both x and z are not defined, y holds no value. The computation of y can be represented by the following node: y = φ(ŷ, φ(x, x, z), ⊥), where ŷ ⇔ (x ∨ ẑ). The graph representation is depicted in Fig. 4. Note that in the graph, the clock ŷ is represented by the subgraph of x ∨ ẑ. The scheduling and the computations are done inside the step function. Therefore, it is natural to construct a graph of this function in order to prove that its variables and the corresponding signals have the same values. To construct the graph of the step function, the following considerations need to be studied. The generated C code in the step function consists of only the assignment and if-then statements. For each signal named x in A, it has a corresponding Boolean variable named C x in the step function. Then the computation of x is implemented by a conditional if-then statement as follows:

if (C_x) { computation(x); }
If x is an input signal then its computation is the reading operation which gets the value of x from the environment. In case x is an output signal, after computing its value, it will be written to the IO communication channel with the environment. Note that the C programs use persistent variables (e.g., variables which always have some value) to implement the Signal program A which uses volatile variables. As a result, there is a difference in the types of a signal in the Signal program and of the corresponding variable in the C code. When a signal has the absent value, ⊥, at a given instant, the corresponding C variable always has a value. This consideration implies that we have to detect when a variable in the C code such that whose value is not updated. In this case, it will be assigned the absent value, ⊥. Thus, the computation of a variable, called x c , can fully be represented by a gated φ-function x c = φ(C x c , x c , ⊥), where x c denotes the newly updated value of the variable.

In the generated C code, the computation of the variable whose clock is the master clock, which ticks every time the step function is called, and the computation of some local variables (introduced by the Signal compiler) are implemented using the following forms:

if (C_x) { computation(x); } else computation(x); // or without if-then computation(x)
It is obvious that x is always updated when the step function is invoked. The computation of such variables can be represented by a single node graph labelled by { x c } x c . That means the variable x c is always updated and holds the value x c .

Considering the following code segment, we observe that the variable x is involved in the computation of the variable y before the updating of x.

if (C_y) { y = x + 1; } // code segment if (C_x) { x = ... }
In this situation, we refer to the value of x as the previous value, denoted by m.x c . It happens when a delay operator is applied on the signal x in the Signal program. The computation of y is represented by the following gated φ-function:

y c = φ(C y c , m.x c + 1, ⊥).

Translation Validation of SDVG

In this section, we introduce the set of rewrite rules to transform the shared value-graph resulting from the previous step. This procedure is called normalizing. At the end of the normalization, for any output signal x and its corresponding variable x c in the generated C code, we check whether x and x c label the same node in the resulting graph. We also provide a method to implement the representation of synchronous data-flow value-graph and adapt the normalizing procedure with any future optimization of the compiler.

Normalizing

Once a shared value-graph is constructed for the Signal program and its generated C code, if the values of an output signal and its corresponding variable in the C code are not already equivalent (they do not point the same node in the shared value-graph), we start to normalize the graph. Given a set of term rewrite rules, the normalizing process works as described in Listing 1. The normalizing algorithm indicates that we apply the rewrite rules to each graph node individually. When there is no more rules that can be applied to the resulting graph, we maximize the shared nodes, reusing the identical subgraphs. The process terminates when there exists no more sharing or rules that can be applied.

We classify our set of rewrite rules into three basic types: general simplification rules, optimization-specific rules and synchronous rules. In the following, we shall present the rewrite rules of these types, and we assume that all nodes in our shared value-graph are typed. We write a rewrite rule in form of term rewrite rules, t l → t r , meaning that the subgraph represented by t l is replaced by the subgraph represented by t r when the rule is applied. Due to the lack of space, we only present a part of these rules, the full set of rules is shown in the appendix.

General Simplification Rules

The general simplification rules contain the rules which are related to the general rules of inference of operators, denoted by the corresponding function symbols in F . In our consideration, the operators used in the primitive stepwise functions and in the generated C code are usual logic operators, numerical comparison functions, and numerical operators. When applying these rules, we will replace a subgraph rooted at a node by a smaller subgraph. In consequence of this replacement, we will reduce the number of nodes by eliminating some unnecessary structures. The first set of rules simplifies numerical and Boolean comparison expressions. In these rules, the subgraph t represents a structure of value computing (e.g., the computation of expression b = x = true). These rules are self explanatory, for instance, with any structure represented by a subgraph t, the expression t = t can always be replaced with a single node subgraph labelled by the value true.

= (t, t) → true = (t, t) → false

The second set of general simplification rules eliminates unnecessary nodes in the graph that represent the φ-functions, where c is a Boolean expression. For instance, we consider the following rules.

φ(true, x 1 , x 2 ) → x 1 φ(c, true, false) → c φ(c, φ(c, x 1 , x 2 ), x 3 ) → φ(c, x 1 , x 3 )
The first rule replaces a φ-function with its left branch if the condition always holds the value true. The second rule operates on Boolean expressions represented by the branches. When the branches are Boolean constants and hold different values, the φ-function can be replaced with the value of the condition c. Consider a φ-function such that one of its branches is another φ-function. The third rule removes the φ-function in the branches if the conditions of the φ-functions are the same.

Optimization-specific Rules Based on the optimizations of the Signal compiler, we have a number of optimization-specific rules in a way that reflexes the effects of specific optimizations of the compiler. These rules do not always reduce the graph or make it simpler. One has to know specific optimizations of the compiler when she wants to add them to the set of rewrite rules. In our case, the set of rules for simplifying constant expressions of the Signal compiler such as:

+(cst 1 , cst 2 ) → cst, where cst = cst 1 + cst 2 ∧(cst 1 , cst 2 ) → cst, where cst = cst 1 ∧ cst 2 (cst 1 , cst 2 ) → cst
where denotes a numerical comparison function, and the Boolean value cst is the evaluation of the constant expression (cst 1 , cst 2 ) which can hold either the value false or true.

We also may add a number of rewrite rules that are derived from the list of rules of inference for propositional logic. For example, we have a group of laws for rewriting formulas with and operator, such as:

∧(x, true) → x ∧(x, ⇒ (x, y)) → x ∧ y
Synchronous Rules In addition to the general and optimization-specific rules, we also have a number of rewrite rules that are derived from the semantics of the code generation mechanism of the Signal compiler.

The first rule is that if a variable in the generated C code is always updated, then we require that the corresponding signal in the source program is present at every instant, meaning that the signal never holds the absent value. In consequence of this rewrite rule, the signal x and its value when it is present x (resp. the variable x c and its updated value x c in the generated C code) point to the same node in the shared value-graph. Every reference to x and x (resp. x c and x c ) point to the same node.

We consider the equation pz := z$1 init 0. We use the variable m.z to capture the last value of the signal z. In the generated C program, the last value of the variable z c is denoted by m.z c . The second rule is that it is required that the last values of a signal and the corresponding variable in the generated C code are the same. That means m.z = m.z c .

Finally, we add rules that mirror the relation between input signals and their corresponding variables in the generated C code. First, for any input signal x and the corresponding variable x c in the generated C code, if x is present, then the value of x which is read from the environment and the value of the variable x c after the reading statement must be equivalent. That means x c and x are represented by the same subgraph in the graph. Second, if the clock of x is also read from the environment as a parameter, then the clock of the input signal x is equivalent to the condition in which the variable x c is updated. It means that we represent x and C x c by the same subgraph. Consequently, every reference to x and C x c (resp. x and x c ) points to the same node.

Illustrative Example

Let us illustrate the verification process in Fig. 1 on the program DEC in Listing 1.2 and its generated C code DEC step() in Listing 1.3.

In the first step, we shall compute the shared value-graph for both programs to represent the computation of all signals and their corresponding variables. This graph is depicted in Fig. 5. In the second step, we shall normalize the above initial graph. Below is a potential normalization scenario, meaning that there might have more than one normalization scenario, and the validator can choose one of them. For example, given a set of rules that can be applied, the validator can apply these rules with different order. In the final step, we check that the value of the output signal and its corresponding variable in the generated code merge into a single node. In this example, we can safely conclude that the output signal N and its corresponding variable N c are equivalent since they point to the same node in the final normalized graph.

Conclusion and Related Work

There is a wide range of works for value-graph representations of expression evaluations in a program. For example, in [START_REF] Weise | Value Dependence Graphs: Representation without Taxation[END_REF], Weise et al. present a nice summary of the various types of value-graph. In our context, the value-graph is used to represent the computation of variables in both source program and its generated C code in which the identical structures are shared. We believe that this representation will reduce the required storage and make the normalizing process more efficient. Another remark is that the calculation of clocks as well as the special value, the absent value, are also represented in the shared graph.

Another related work which adopts the translation validation approach in verification of optimizations, Tristan et al. [START_REF] Tristan | Evaluating Value-graph Translation Validation for LLVM[END_REF], recently proposed a framework for translation validation of Llvm optimizer. For a function and its optimized counterpart, they construct a shared value-graph. The graph is normalized (the graph is reduced). After the normalization, if the outputs of two functions are represented by the same sub-graph, they can safely conclude that both functions are equivalent.

On the other hand, Tate et al. [START_REF] Tate | Equility Saturation: A New Approach to Optimization[END_REF] proposed a framework for translation validation. Given a function in the input program and the corresponding optimized version of the function in the output program, they compute two value-graphs to represent the computations of the variables. Then they transform the graph by adding equivalent terms through a process called equality saturation. After the saturation, if both value-graphs are the same, they can conclude that the return value of two given functions are the same. However, for translation validation purpose, our normalization process is more efficient and scalable since we can add rewrite rules into the validator that reflect what a typical compiler intends to do (e.g., a compiler will do the constant folding optimization, then we can add the rewrite rule for constant expressions such as three nodes subgraph (1 + 2) is replaced by a single node 3).

The present paper provides a verification framework to prove the valueequivalence of variables and applies this approach to the synchronous data-flow compiler Signal. With the simplicity of the graph normalization, we believe that translation validation of synchronous data-flow value-graph for the industrial compiler Signal is feasible and efficient. Moreover, the normalization process can always be extended by adding new rewrite rules. That makes the translation validation of Sdvg scalable and flexible.

We have considered sequential code generation. A possibility is to extend this framework to use with other code generation schemes including cluster code with static and dynamic scheduling, modular code, and distributed code. One path forward is the combination of this work and the work on data dependency graph in [START_REF] Ngo | Formal Verification of Compiler Transformations on Polychronous Equations[END_REF][START_REF] Ngo | Formal Verification of Synchronous Data-flow Program Transformations Toward Certified Compilers[END_REF][START_REF] Ngo | Formal Verification of a Synchronous Data-flow Compiler: from Signal to C[END_REF]. That means that we use synchronous data-flow dependency graphs and synchronous data-flow value-graphs as a common semantic framework to represent the semantics of the generated code. The formalization of the notion of "correct transformation" is defined as the refinements between two synchronous data-flow dependency graphs and in a shared value-graph as described above.

Another possibility is that we use a Smt solver to reason on the rewriting rules. For example, we recall the following rules:

φ(c 1 , φ(c 2 , x 1 , x 2 ), x 3 ) → φ(c 1 , x 1 , x 3 ) if c 1 ⇒ c 2 φ(c 1 , φ(c 2 , x 1 , x 2 ), x 3 ) → φ(c 1 , x 2 , x 3 ) if c 1 ⇒ ¬c 2
To apply these rules on a shared value-graph to reduce the nested φ-functions (e.g., from φ(c 1 , φ(c 2 , x 1 , x 2 ), x 3 ) to φ(c 1 , x 1 , x 3 )), we have to check the validity of first-order logic formulas, for instance, we check that |= (c 1 ⇒ c 2 ) and |= c 1 ⇒ ¬c 2 . We consider the use of Smt to solve the validity of the conditions as in the above rewrite rules to normalize value-graphs. Let us comment this program: ? integer F B; ! integer N : F B, N are respectively input and output signals of type integer ; F B ˆ= when (ZN <= 1): F B is accepted (or it is present) only when ZN becomes less than or equal to 1; N := F B default (ZN -1): N is set to F B when its previous value is less than or equal to 1, otherwise it is decremented by 1; ZN := N $1 init 1: defines ZN as always carrying the previous value of N (the initial value of ZN is 1); where integer ZN init 1: indicates that ZN is a local signal whose initial value is 1. Note that the clock of the output signal is more frequent than that of the input. This is illustrated in the following possible trace: Program Structure The language is modular. In particular, a process can be used as a basic pattern, by means of an interface that describes its parameters and its input and output signals. Moreover, a process can use other subprocesses, or even external parameter processes that are only known by their interfaces. For example, to emit three sequences of values (F B i ) -1, ..., 2, 1 for all three positive integer inputs F B i , with i = 1, 2, 3, one can define the following process (in which, without additional synchronizations, the three subprocesses have unrelated clocks): The rules operate on Boolean expressions represented by the branches. When one of the branches is Boolean constant, the φ-function can be replaced with a Boolean expression of the condition c and the non-constant branch. For instance, when the left branch is a constant and holds the value true, then the φ-function is replaced with the Boolean expression c ∨ x.

φ(c, x, x) → x (15)
The rule 15 removes the φ-function if all of its branches contain the same value.

A φ-function with only one branch is a special case of this rule. It indicates that there is only one path to the φ-function as happens with branch elimination.

φ(c, φ(c, x 1 , x 2 ), x 3 ) → φ(c, x 1 , x 3 ) (16) φ(c, x 1 , φ(c, x 2 , x 3 )) → φ(c, x 1 , x 3 ) (17) φ(c, φ(¬c, x 1 , x 2 ), x 3 ) → φ(c, x 2 , x 3 ) (18) φ(c, x 1 , φ(¬c, x 2 , x 3 )) → φ(c, x 1 , x 2 ) (19) φ(c 1 , φ(c 2 , x 1 , x 2 ), x 3 ) → φ(c 1 , x 1 , x 3 ) if c 1 ⇒ c 2 (20) φ(c 1 , φ(c 2 , x 1 , x 2 ), x 3 ) → φ(c 1 , x 2 , x 3 ) if c 1 ⇒ ¬c 2 (21) φ(c 1 ∧ c 2 , φ(c 1 , x 1 , x 2 ), x 3 ) → φ(c 1 ∧ c 2 , x 1 , x 3 ) (22) φ(c 1 ∧ c 2 , φ(c 2 , x 1 , x 2 ), x 3 ) → φ(c 1 ∧ c 2 , x 1 , x 3 ) (23) φ(c 1 , x 1 , φ(c 2 , x 2 , x 3 )) → φ(c 1 , x 1 , x 2 ) if ¬c 1 ⇒ c 2 (24) φ(c 1 , x 1 , φ(c 2 , x 2 , x 3 )) → φ(c 1 , x 1 , x 3 ) if ¬c 1 ⇒ ¬c 2 (25) φ(c 1 ∨ c 2 , x 1 , φ(c 1 , x 2 , x 3 )) → φ(c 1 ∨ c 2 , x 1 , x 3 ) (26) φ(c 1 ∨ c 2 , x 1 , φ(c 2 , x 2 , x 3 )) → φ(c 1 ∨ c 2 , x 1 , x 3 ) (27)
Consider a φ-function such that one of its branches is another φ-function. The rules 16 to 27 remove the φ-function in the branch if one of the following conditions is satisfied:

-The conditions of the φ-functions are the same (as in the rules 16 and 17).

-The condition of the first φ-function is equivalent to the negation of the condition of the second φ-function (as in the rules 18 and 19). -The condition of the first φ-function either implies the condition of the second φ-function or its negation (as in the rules 20 to 23). -The negation of the condition of the first φ-function either implies the condition of the second φ-function or its negation (as in the rules 24 to 27).

The following code segment in C illustrates the use of the above rewrite rules:

if (c) { a = 0; b = 0; d = a; } else { a = 1; b = 1; d = 0; } if (a == b) x = d; else x = 1; return x;
If we analyze this code segment the return value is 0. In fact, a and b have the same value in both branches of the first "if" statement. Thus in the second "if" statement the condition is always true, then x always holds the value of d which is 0. We shall apply the general simplification rules to show that the value-graph of this code segment can be transformed to the value-graph of the value 0. We represent the value-graph in form of linear notation. The value-graph of the computation of x is φ(= (a, b), d, 0). Replacing the definition of a, b and d, and normalizing this graph, we get:

x →φ(= (φ(c, 0, 1), φ(c, 0, 1)), φ(c, φ(c, 0, 1), 0), 0) φ(true, φ(c, φ(c, 0, 1), 0), 0) by ( 1) φ(c, φ(c, 0, 1), 0) by [START_REF] Gautier | Code Generation in the SACRES Project[END_REF] φ(c, 0, 0) by ( 16) 0 by [START_REF] Tate | Equility Saturation: A New Approach to Optimization[END_REF] Optimization-specific Rules Based on the optimizations of the Signal compiler, we have a number of optimization-specific rules in a way that reflexes the effects of specific optimizations of the compiler. These rules do not always reduce the graph or make it simpler. One has to know specific optimizations of the compiler when she wants to add them to the set of rewrite rules. In our case, the set of rules for simplifying constant expressions of the Signal compiler is given as follows.

-Specific rules for constant expressions with numerical operators:

+(cst
-Specific rules for constant expressions with numerical comparison functions:

(cst 1 , cst 2 ) → cst (36) consider the equation pz := z$1 init 0. We use the variable m.z to capture the last value of the signal z. In the generated C program, the last value of the variable z c is denoted by m.z c . We require that the last values of a signal and the corresponding variable in the generated C code are the same. That means m.z = m.z c .

m.x c → G 1 + m.x → G 2 → m.x c , m.x → G 1 (39)
The rule 39 indicates that for any signal x which is involved in a delay operator, and its corresponding variable in the generated C program, then it is required that the last values of x and x c are the same. Therefore, every reference to m.x c and m.x points to the same node. Finally, we add rules that mirror the relation between input signals and their corresponding variables in the generated C code. First, for any input signal x and the corresponding variable x c in the generated C code, if x is present, then the value of x which is read from the environment and the value of the variable x c after the reading statement must be equivalent. That means x c and x are represented by the same subgraph in the graph. Second, if the clock of x is also read from the environment as a parameter, then the clock of the input signal x is equivalent to the condition in which the variable x c is updated. It means that we represent x and C x c by the same subgraph.

x c → G 1 + x → G 2 → x c , x → G 1 (40) C x c → G 1 + x → G 2 → C x c , x → G 1 (41)
Consequently, every reference to x and C x c (resp. x and x c ) points to the same node.

Fig. 2 :

 2 Fig. 2: The Translation Validation for the SIGNAL Compiler

Definition 1 .

 1 A Sdvg associated with a Signal program and its generated C code is a directed graph G = N, E, I, O, l N , m N where N is a finite set of nodes that represent clocks, signals, variables, or functions. E ⊆ N × N is the set of edges that describe the computation relations between nodes. I ⊆ N is the set of input nodes that are the input signals and their corresponding variables in the generated C code. O ⊆ N is the set of output nodes that are the output signals and their corresponding variables in the generated C code. l N : N -→ X ∪ F is a mapping labeling each node with an element in X ∪ F . m N : N -→ P(N ) is a mapping labeling each node with a finite set of clocks, signals, and variables. It defines the set of equivalent clocks, signals and variables.

Fig. 3 :

 3 Fig. 3: The graphs of y := f (x 1 , ..., x n ) and y := x$1 init a

Fig. 4 :

 4 Fig. 4: The graphs of y := x default z and y := x when b

Listing 1 . 2 :

 12 DEC in Signalprocess DEC= (? integer FB; ! integer N) (| FB ˆ= when (ZN<=1) | N := FB default (ZN-1) | ZN := N$1 init 1 |) where integer ZN init 1 end; Listing 1.3: Generated C code of DEC EXTERN logical DEC_step() { C_FB = N <= 1; if (C_FB) { if (!r_DEC_FB(&FB)) return FALSE; // read input FB } if (C_FB) N = FB; else N = N -1; w_DEC_N(N); // write output N DEC_step_finalize(); return TRUE; } Note that in the C program, the variable N c ("c" is added as superscript for the C program variables, to distinguish them from the signals in the Signal program) is always updated (line (6)). In lines (2) and (6), the references to the variable N c are the references to the last value of N c denoted by m.N c . The variable F B c which corresponds to the input signal F B is updated only when the variable C F B c is true.

Fig. 5 :

 5 Fig. 5: The shared value-graph of DEC and DEC step

Fig. 6

 6 depicts the intermediate resulting graph of this normalization scenario, and Fig. 7 is the final normalized graph from the initial graph when we cannot perform any more normalization. -The clock of the output signal N is a master clock which is indicated in the generated C by the variable N c being always updated. The node { N , ZN } ∨ is rewritten into true. -By rule ∧(true, x) → x, the node { F B} ∧ is rewritten into { F B} <=. -The φ-function node representing the computation of N is removed and N points to the node { N } φ. -The φ-function node representing the computation of ZN is removed and ZN points to the node { ZN } m.N . -The nodes F B c and F B are rewritten into a single node { F B} F B c . All references to them are replaced by references to { F B} F B c . -The nodes m.N c and m.N are rewritten into a single node { m.N } m.N c . All references to them are replaced by references to { m.N } m.N c .

Fig. 6 :Fig. 7 :

 67 Fig. 6: The resulting value-graph of DEC and DEC step

  difference xˆ-y define clocks C x ∩ C y and C x \ C y , which can be rewritten as ˆx whenˆy and when (not(ˆy) default ˆx), respectively. Example The following Signal program emits a sequence of values F B, F B -1, ..., 2, 1, from each value of a positive integer signal F B coming from its environment: process DEC= (? integer FB; ! integer N) (| FB ˆ= when (ZN<=1) | N := FB default (ZN-1) | ZN := N$1 init 1 |) where integer ZN init 1 end;

  t2 t3 t4 t5 t6 t7 t8 t9 CN t0 t1 t2 t3 t4 t5 t6 t7 t8 t9

  1. / Input: G: A shared value-graph. R: The set of // rewrite rules. S: The sharing among graph nodes. // Output: The normalized graph while (∃s ∈ S or ∃r ∈ R that can be applied on G) { while (∃r ∈ R that can be applied on G) {

	for (n ∈ G)
	if (r can be applied on n)
	apply the rewrite rule to n
	}
	maximize sharing
	}
	return G
	Listing 1.1: Value-graph Normalization

/

  1 , cst 2 ) → cst, where cst = cst 1 + cst 2 (28) * (cst 1 , cst 2 ) → cst, where cst = cst 1 * cst 2 (29) -(cst 1 , cst 2 ) → cst, where cst = cst 1 -cst 2 (30) /(cst 1 , cst 2 ) → cst, where cst = cst 1 /cst 2(31)-Specific rules for constant expressions with usual logic operators:∧(cst 1 , cst 2 ) → cst, where cst = cst 1 ∧ cst 2(34)∨(cst 1 , cst 2 ) → cst, where cst = cst 1 ∨ cst 2

	¬false → true	(32)
	¬true → false	(33)

Appendix A: The Signal Language

Language Features

Data domains Data types consist of usual scalar types (Boolean, integer, float, complex, and character), enumerated types, array types, tuple types, and the special type event, subtype of the Boolean type which has only one value, true.

Operators The core language consists of two kinds of "statements" defined by the following primitive operators: first four operators on signals and last two operators on processes. The operators on signals define basic processes (with implicit clock relations) while the operators on processes are used to construct complex processes with the parallel composition operator:

-Stepwise Functions: is the process resulting of their parallel composition. This process consists of the composition of the systems of equations. The composition operator is commutative, associative, and idempotent. -Restriction: P where x, where P is a process and x is a signal, specifies a process by considering x as local variable to P (i.e., x is not accessible from outside P ).

Clock relations In addition, the language allows clock constraints to be defined explicitly by some derived operators that can be replaced by primitive operators above. For instance, to define the clock of a signal (represented as an event type signal), y :=ˆx specifies that y is the clock of x; it is equivalent to y := (x = x) in the core language. The synchronization xˆ= y means that x and y have the same clock, it can be replaced by ˆx = ˆy. The clock extraction from a Boolean signal is denoted by a unary when: when b, that is a shortcut for b when b. The clock union xˆ+ y defines a clock as the union C x ∪ C y , which can be rewritten as ˆx default ˆy. In the same way, the clock intersection x ˆ * y and the clock

Appendix B: Rewrite Rules

General Simplification Rules

The first set of general simplification rules simplifies applied numerical and Boolean comparison expressions. In these rules, the term t represents a structure of value computing (e.g., the computation of expression b = x = true). The rules 3, 4, 5, and 6 only apply on the Boolean type. These rules are self explanatory, for instance, with any structure represented by a term t, the expression t = t can always be replaced with the value true.

The second set of general simplification rules eliminates unnecessary nodes in the graph that represent the φ-functions, where c, c 1 and c 2 are Boolean expressions. For better representation, we divide this set of rules into several subsets as follows.

The rules in this set replace a φ-function with its left branch if the condition always holds the value true. Otherwise, if the condition holds the value false, it is replaced with its right branch.

The rules operate on Boolean expressions represented by the branches. When the branches are Boolean constants and hold different values, the φ-function can be replaced with the value of the condition c.

where = <, >, =, <=, >=, /=, and the Boolean value cst is the evaluation of the constant expression (cst 1 , cst 2 ) which can hold either the value false or true.

We also may add a number of rewrite rules that are derived from the list of rules of inference for propositional logic. For example, we have a group of laws for rewriting formulas with and operator, such as:

We consider the following Signal program and its generated C code, the input signal x is present when the other Boolean input signal cx holds the value true. The computation of x is represented by x = φ(x, x, ⊥), where x ⇔ cx ∧ cx. In the generated C code, the value of x is read only when the condition C cx ∧ cx is true. That is represented by x = φ(C cx, φ(cx, x, ⊥), ⊥). This observation makes us add the following rewrite rule into the systems to mirror the above rewriting of the Signal compiler.

Synchronous Rules Consider the generated C code, we observe that the value of the variable z is always updated. It holds the value of x if C x is true, otherwise it is 0. Hence, we have the following rule that mirrors the above situation.

We write x → φ(true, x, ⊥) to denote that x points to the subgraph rooted at the node labeled by φ-function. The rule 38 indicates that if a variable in the generated C code is always updated, then we require that the corresponding signal in the source program is present at every instant, meaning that the signal never holds the absent value. In consequence of this rewrite rule, the signal x and its value when it is present x (resp. the variable x c and its updated value x c in the generated C code) point to the same node in the shared value-graph. Every reference to x and x (resp. x c and x c ) point to the same node. A second synchronous rule mirrors the semantics of the delay operator. For instance, we