Variability Encoding

This page describes the process of variability encoding. All examples are given in C. The process is very similar for JAVA. Further information and a correctness proof can be found in the following Technical Report:

Sven Apel, Hendrik Speidel, Philipp Wendler, Alexander von Rhein, and Dirk Beyer. Feature-Aware Verification. Technical Report MIP-1105, Department of Informatics and Mathematics, University of Passau, September 2011.
 

This section explains the technique of variability encoding. First, variability encoding is defined and an abstract example is presented. Then, we show that proving the safety of the variability encoded program is equivalent to proving the safety of all possible variants of a product line.

Definition

Variability encoding has been implemented by modifying FSTComposer – the composer included in FeatureHouse. It assumes at least some familiarity with superimposition – the composition method used by FSTComposer. An overview of the process is available on the FeatureHouse Homepage; for a formal definition of the composition process, the reader is referred to the following publication: SC2008.

Normally, FeatureHouse works as follows: It accepts a list of selected features and a base directory in which each feature’s code is stored in a subdirectory. This directory is called the containment hierarchy. The list of selected features (the expression file) needs to be in composition order and needs to represent a valid variant according to the feature model (i.e. feature interdependencies need to be satisfied). Then, FeatureHouse composes a variant by superimposing the feature structure trees (FSTs) of the code of the selected features. Feature structure trees are similar to abstract syntax trees (ASTs) — they represent a feature’s structure down to a certain resolution (e.g. for C a function node of an AST contains children such as statement nodes, whereas a function node of an FST contains the whole body of a function as an attribute and represents a terminal node). During composition, the resulting variant is first set to the FST describing the first feature. Then, the other features are successively superimposed on it, thereby introducing new constructs —e.g. function, structure, or variable declarations— or refining existing constructs. Two FSTs are superimposed by recursively composing matching FST nodes i.e. nodes that have the same name, type, and relative location in their FSTs. The resulting variant contains only the code of the selected features — feature selection happened at composition time.

The basic idea of variability encoding is to postpone the process of feature selection until early runtime. Then, —at application startup time— a variant is selected by setting a set of variables called feature variables. Each feature of the product line is represented by a feature variable. If set to 1, the corresponding feature is selected; if set to 0, the corresponding feature is not part of the selected variant. After initialization, feature variables are not changed. The code of a specific feature is only executed if its feature variable has been set to 1. This way the application behaves like a variant that has been composed using the traditional composition.

Generally, there are multiple ways how nodes (e.g., functions) are composed depending on the node type. Nodes are generally distinguished as nonterminal and terminal nodes. Nonterminal nodes may possess child nodes, whereas terminal nodes do not. For example with C, FeatureHouse defines a module and a structure as being nonterminal while include statements and functions are realized as terminal nodes. During composition, when two nonterminal nodes are composed, their lists of children are merged, that is, a child is either introduced into the result because it is only present in one tree or two matching children are composed. Generally, while nonterminal nodes are always composed by recursively composing their children, terminal nodes follow a strategy that is depending on the exact type of terminal node – such a strategy is called a composition rule. In C, the following composition rules are in use:

• Replacement – when superimposing two FST nodes using replacement, the newly introduced node simply replaces the other node, i.e. the old node is deleted and the new node is introduced in its stead.
• FunctionRefinement – here, the old node is given a new name (the C function is renamed but retains its return and parameter types), the new node is introduced and references to original within its body are pointed to . If no call to original is present in the refining node, FunctionRefinement behaves exactly like Replacement.

For variability encoding FunctionRefinement is exchanged for an alternative implementation to postpone the feature selection process to the early runtime of the program:

• VariabilityEncodedFunctionRefinement — if a function is to be replaced, it may still be needed by variants in which the refining feature is not present. Therefore, its function name is rewritten to , the new function node is introduced with name and a feature switch is generated with name . Calls to original within the new function are rewritten to .

A feature switch is a function that dispatches to a variants implementation of the function depending on feature being selected, e.g. for a function returning int that accepts no parameters:

int alpha() {
    //choose implementation depending on the value of feature variable of f
    if (__SELECTED_FEATURE_f) {
        return alpha_role_f();
    } else {
        return alpha_before_f();
    }
}

A specific variant of the product line can now be created by initializing the feature variables accordingly. To be able to check all variants in one run we set the feature variables to uninitialized values. The software model checker must now take all feature combinations into account. To exclude variants that do not satisfy the conditions imposed by the feature model, we encode the feature model into the feature selection process as outlined in the following pseudo code:

int main() {
    select_features();
    //feature variables are now uninitialized
    //check that selected features form a valid variant
    if (valid_product()) {
        //run the variant
        return original_main();
    }
}

This way, the model checker needs to take all valid variants (and no more) into account when checking the safety of the product line. If a bug is found in the variability encoded product line, variants that also exhibit the bug can be derived from the counterexample given by the model checker. If the variability encoded product line is safe, then so are all valid variants.

Example

In the following, the normal composition process is compared to the construction of variability encoding.

Let us assume a product line containing the three features Base, Extension1, and Extension2 that are composed in that order. Each feature contains a single C file named main.c. The contents of these files and the FSTs of the features are listed in the following table. For brevity, include directives are not shown in the FSTs. Also the order in which child nodes are depicted has been chosen for readability and does not represent the order in which nodes are placed by FSTComposer. Dotted arrows between function nodes mean that a function may call a function it points to.

Base //main.c #include <stdio.h> void action1() { puts("In action1 Base"); } void main() { action1(); } //	Extension1 //main.c void action1() { original(); puts("action1 refined by Extension1"); } //	Extension2 //main.c void action1() { puts("action1 refined by Extension2"); action2(); original(); } void action2() { puts("action2 introduced by Extension2"); } //
FST of Base	FST of Extension1	FST of Extension2

We will now compare the composition of a variant v containing Base and Extension1 to the variability encoded product line. For variability encoding, all features will be used. By selecting Base and Extension1 using the introduced feature variables a variant is produced that behaves like the traditionally composed variant v.

In the following, superimposition is denoted by and variability encoding is denoted by . Both operations are left-associative.

Composition of Base and Extension1

FST of Base Extension1.

Function main calls the implementation of action1 defined in Extension1. The call to original is rewritten to call the implementation of action1 provided by Base.

Variability Encoding

Step 1 - Base Extension1

FST of Base Extension1.

Function main calls the feature switch for Extension1. If Extension1 is not selected, the feature switch dispatches to the implementation of Base thereby skipping Extension1. If Extension1 is selected, the feature switch dispatches to the implementation of action1 provided by Extension1. Analogous to composition, this implementation calls the implementation of Base for calls to original.

Step 2 - Base Extension1 Extension2

Now, the FST of Extension2 is superimposed on the FST that has been obtained in the previous step.

The following figure illustrates the resulting FST:

FST of Base Extension1 Extension2.

As before, the refinement of action1 by Extension2 results in the addition of a feature switch, a node for the implementation of action1 provided by Extension2 and the renaming of the current implementation of action1 resulting from step one. If Extension2 is selected using its feature variable, the implementation given in Extension2 is called. If Extension2 is not selected, the feature switch of Extension1 takes over: if a function is refined by multiple features, feature switches form a cascade as a direct result of the application of the VariabilityEncodedFunctionRefinement. Therefore, if only Base and Extension1 are selected, the feature switches dispatch only to the implementations of action1 provided by these features. This configuration is depicted with the red dotted arrows in the figure above. As the feature switches and feature selection process of the variability encoded product line have no side effects other than selecting the variant, the variability encoded product line behaves like the composed variant.