Product lines of dataflows

Michael Lienhardt, Maurice H ter Beek, Ferruccio Damiani

► To cite this version:

Michael Lienhardt, Maurice H ter Beek, Ferruccio Damiani. Product lines of dataflows. Journal of Systems and Software, 2023, 210, pp.111928. 10.1016/j.jss.2023.111928. hal-04631042

HAL Id: hal-04631042

https://hal.science/hal-04631042v1

Submitted on 1 Jul 2024

**HAL** is a multi-disciplinary open access
archive for the deposit and dissemination of sci-
entific research documents, whether they are pub-
lished or not. The documents may come from
teaching and research institutions in France or
abroad, or from public or private research centers.

L'archive ouverte pluridisciplinaire HAL, est
destinée au dépôt et à la diffusion de documents
scientifiques de niveau recherche, publiés ou non,
émanant des établissements d'enseignement et de
recherche français ou étrangers, des laboratoires
publics ou privés.

<figure><img src="image_1.png" /></figure>

Distributed under a Creative Commons Attribution 4.0 International License
<figure><img src="image_2.png" /></figure>

Product lines of dataflows ⭐

Michael Lienhardt<sup>a,*</sup>, Maurice H. ter Beek<sup>b</sup>, Ferruccio Damiani<sup>c</sup>

<figure><img src="image_3.png" /></figure>

A B S T R A C T

Data-centric parallel programming models such as *dataflows* are well established to implement complex concurrent software. However, in a context of a configurable software, the dataflow used in its computation might vary with respect to the selected options: this happens in particular in fields such as Computational Fluid Dynamics (CFD), where the shape of the domain in which the fluid flows and the equations used to simulate the flow are all options configuring the dataflow to execute.

In this paper, we present an approach to implement product lines of dataflows, based on Delta-Oriented Programming (DOP) and term rewriting. This approach includes several analyses to check that all dataflows of a product line can be generated. Moreover, we discuss a prototype implementation of the approach and demonstrate its feasibility in practice.

1. Introduction

Over the past decades, with the end of Moore's law and the multi-
plication of parallel architectures such as multi-core CPUs and GPUs,
many data-centric programming paradigms were developed in order
to continue having always more efficient programs with such new
hardware. This trend is clearly visible in HPC where many data-centric
languages and libraries have been developed, such as Chapel (Chamber-
lain et al., 2007), StarPU (Augonnet et al., 2011), HPX (Kaiser et al.,
2014), Charm++ (Kale and Krishnan, 1993), Legion (Bauer, 2014) and
DAPP (Ben-Nun et al., 2019; Rausch et al., 2022). The core model of
data-centric computation is the *dataflow* (Kavi and Deshpande, 1991;
Roumage et al., 2022) which can be expressed as an acyclic directed
graph stating how data is generated and used by side-effect-free tasks.

While dataflows can efficiently be deployed on parallel and hetero-
geneous architectures, their structure is very static with no conditional
nor loops. Libraries like HPX (Kaiser et al., 2014) or Legion (Bauer,
2014) alleviate this restriction by extending the model with conditional
and runtime tasks creations, at the cost of a less efficient computation
model. Moreover such extensions are not well-suited to large config-
uration spaces that occur in industrial tools like elsA (Cambier et al.,
2013) and Fun3D (Anderson et al., 2023).

elsA is a tool that implements Computational Fluid Dynamics (CFD), i.e., it simulates the flow of fluids in a given input mesh and outputs information of interest to the user (e.g., the pressure that a material pushed by the fluid must be able to sustain, or some modification of its shape that would make the fluid flow more efficiently). The principle

of elsA's computation is a fixpoint loop: it executes the same code in
loop until the computed flow is close enough to what would happen in
reality. And since the loop's code could be executed millions of time,
expressing it as a dataflow would greatly improve the efficiency of elsA.

However, *elsA* has an infinite configuration space – structured into three parts – that has a huge impact on the shape of the executed dataflow. The first part of the configuration space consists of about 2000 options that configure which fluid flow computation to perform. Indeed, fluid flow is given by the Navier–Stokes equations that do not have an analytic solutions, and so hundreds of approximations of these equations have been defined, with various precision and stability characteristics: it is up to the user to decide which approximation *s/he* wants to use. The second part of the configuration space is the output information provided to the user: virtually any data could interest her/him since it depends on which phenomena *s/he’s* studying. So *s/he* must provide the list of these data to *elsA* which in turn must compute them by extending its dataflow. The last part of the configuration space is the shape of the input mesh itself. Meshes are usually structured in various *zones* (modeling the domain in which the fluids flow) and *boundaries* (modeling walls of different materials, fluid injection or extraction, or even infinite domains): fluid flow simulation must be performed on every zone of the mesh, and specific computation must be performed on each boundary depending on its type (e.g., the effect of a wall on a flow is different from the effect of a fluid injection).

In this paper, we propose an approach to automatically generate
dataflows given a configuration space close to elsA's: instead of con-
sidering an arbitrary input mesh, we consider that its variability space

<footnote><sup>a</sup> ONERA, Palaiseau, France</footnote>

<footnote><sup>b</sup> ISTI-CNR, Pisa, Italy</footnote>

<footnote><sup>c</sup> University of Turin, Turin, Italy</footnote>

<footnote>Editor: Professor Laurence Duchien.</footnote>

<footnote>* Corresponding author.
*E-mail addresses:* michael.lienhardt@onera.fr (M. Lienhardt), maurice.terbeek@isti.cnr.it (M.H ter Beek), ferruccio.damiani@unito.it (F. Damiani).</footnote>
<figure><img src="image_4.png" /><figcaption>Fig. 1. Dataflow generation pipeline.</figcaption></figure>

could be expressed with features. Our approach is structured in two main parts: first, it uses Software Product Line (SPL) techniques (Apel et al., 2013, Sect. 6.6.1) to express the variability of tasks w.r.t. the configuration space, and configures them given the options selected by the user; then, it uses term rewriting to assemble these configured tasks into a dataflow that computes the data requested by the user. Fig. 1 details the structure of our approach:

* first, we use a Domain Specific Language (DSL) duly extended with concepts from Delta-Oriented Programming (DOP) (Schaefer et al., 2010) to model the variability of the dataflow's tasks. This DSL allows us to specify which tasks, with which inputs and which outputs, are available to construct a dataflow. Then,

* given an input *Product* specifying the values of the different options, the *Product Line Flattening* process automatically generates the *Task Specification* corresponding to that specific product; then

* the *Rewriting rules Generation* process automatically translates the specification into term rewriting rules; and

* given a list of *Values to Compute*, we simply apply the generated rewriting rules on this data to obtain a correct dataflow computing these values by using the tasks available in the specification.

We presented a preliminary version of this approach in Damiani et al. (2022). In this paper, we: (i) replace the ad-hoc dependency solver with rewriting; (ii) give a precise algorithm for each step of our dataflow generation process; and (iii) add a static analysis to guarantee that, for each product, a well-formed dataflow is generated.

*Outline.* Section 2 illustrates variability on dataflows with an example from Computational Fluid Dynamics (CFD), and shows how such a dataflow can be encoded with terms in order to motivate our approach of using term rewriting. Section 3 introduces our DSL, its DOP extension, and how to use them to generate a dataflow. Section 4 describes the different analyses guaranteeing that a DSL can generate a correct dataflow for all its products. Section 5 introduces our prototype implementation and presents some benchmarks illustrating the feasibility of the approach in practice. Finally, Section 6 discusses related work, while Section 7 concludes the paper.

## 2. Running example

In this section, we present the running example that is used throughout the paper to illustrate our approach. This example is inspired from the variability and computation that occurs in *elsA* and is structured in three parts: first we introduce a simple feature model; second we present two simple dataflows that corresponds to some products of the feature model; and finally, we show how these dataflows could be encoded as terms. In this example and in the rest of the paper, we will use the Maude term rewriting language (Clavel et al., 2007) to write down terms and rewriting rules.

<figure><img src="image_5.png" /><figcaption>Fig. 2. Simple CFD feature model.</figcaption></figure>

<figure><img src="image_6.png" /><figcaption>Fig. 3. Dataflow computing Rhs with inlet, outpres selected.</figcaption></figure>

### 2.1. Feature model

Fig. 2 shows the feature model of our running example, which is structured in two main parts. The first part encodes the variability of the mesh and is identified with the **mesh** feature. A mesh always has a unique zone, and between one and three boundaries of different types: **inlet** models the injection of fluid; **outpres** models a possible output of the fluid flow; and **wall** models a wall. The second part encodes which approximation of the fluid dynamics is considered in the computation and is identified with the **model** feature. The mandatory **convective** feature only considers convective dynamics (which are triggered by pressure). The optional **diffusive** feature extends the flow dynamics by also considering its viscosity. Finally, the optional **order2** feature changes the behavior of the selected flow dynamics and asks them to have a more precise computation (i.e., instead of approximating the equations with a polynomial of degree one, they are now approximated with a polynomial of degree 2).

### 2.2. Dataflows

Fig. 3 shows the dataflow computing the value Rhs only (i.e., the update of the fluid flow fixpoint computation) while selecting the boundaries **inlet** and **outpres**, and no optional model feature. The computation starts with the data **Conservative** which models the currently computed flow on the unique zone of the mesh. Then on one side, it uses one function per boundary (resp. **inlet** and **outpres**) to compute data (resp. **BC(Inlet)** and **BC(Outpres)**) encoding the effect of these boundaries on the flow. On the other side, it uses the **primitive** function to normalize the **Conservative** data into **Primitive**. Then the functions **convectiveFluxBC** and **convectiveFlux** compute the update of the convective fluid flow respectively on the boundaries (**FxcBC**) and on the zone (**Fxc**) of the mesh. Finally, these two flows are merged with the **fluxBalance** function and normalized with the **explicitIncrement** to generate the data Rhs.

Fig. 4 shows a more complex dataflow that computes the value Rhs and the gradient (i.e., the derivative) of the pressure (which is used to identify shocks) while selecting the boundary **wall** and all optional model features. Compared to the dataflow presented in Fig. 3, this dataflow has one modified part and three additional parts (depicted in
<figure><img src="image_7.png" /><figcaption>Fig. 4. Dataflow computing Rhs and Grad(Pressure) with wall, diffusive and order2 selected.</figcaption></figure>

gray). The part that is modified corresponds to the management of the boundaries: since the boundary of the mesh only contains a wall (and not an injection and exit flow as in Fig. 3), the effect of this boundary on the flow is now modeled by the data BC(Wall), computed by the wall function. The first additional part occurs on the right of Primitive, where some new tasks appeared to compute the gradient of the pressure grad(Pressure) requested by the user: the function pressure computes the Pressure from Primitive, and then the gradient function is used to compute grad(Pressure). The second additional part is triggered by the selection of the order2 feature: the functions convectiveFlux and convectiveFluxBC now take the additional parameter grad(Primitive), computed by the gradient function applied on Primitive. The last additional part consists of the management of the diffusive flow: in addition to the convectiveFlux and convectiveFluxBC functions, the similar functions diffusiveFlux and diffusiveFluxBC were added, that take an extra input grad grad(Primitive)) (computed by the gradient function applied on grad(Primitive)).

Finally, similarly to the dataflow in Fig. 3, the function *fluxBalance* collects all the computed flows into the *Balance* data, which is then normalized with the *explicitIncrement* to generate the data Rhs.

## 2.3. Dataflows as terms

Listing 1 presents the abstract syntax that encodes a dataflow in the form of a Maude module. In this encoding, a dataflow is a DAG that contains two main kinds of nodes: data and tasks. We model these nodes with the term constructors *data* of sort *Data* and *task* of sort *Task*. A data node can either be a root of the dataflow, or be computed by a task. In both cases, data has a value (of sort *Value*). A task is identified by the ID of its function (of sort *FunctionID*) and the list of its data parameters.

1. `mod DATAFLOW is`
2. `sorts Data Task Value FunctionID DataList .`
3. `subsort Data < DataList .`
4. `op _ _ : Data DataList -> DataList [ctor] .`
5. `op _ _ : Data DataList -> DataList [ctor] .`
6. `op data : Value -> Data [ctor] .`
7. `op data : Value Task -> Data [ctor] .`
8. `op task : FunctionID DataList -> Task [ctor] .`
9. `endm`

**Listing 1:** The DATAFLOW Maude module: abstract syntax of a dataflow.

In the rest of this section, we use the DATAFLOW Maude module as a basis to encode the two dataflows in Figs. 3 and 4 into terms.

First, the Maude module EXAMPLE-CORE in Listing 2 provides the sorts and term constructors used to encode our dataflow examples. We have three sorts in this module: *Value* and *FunctionID* are the same as in the DATAFLOW module, and BC is a new sort for values held on a mesh boundary. The rest of the module is structured in three parts, each one declaring the constructor for a specific sort. First, the module declares the base values of our dataflow: *Conservative*, *Primitive*, etc. These constructors do not have any parameters, except for BC that takes a boundary value in parameter (this models the fact that these values are somewhat special), and *Grad* that takes a value in parameter (as illustrated in Fig. 4, it is indeed possible to compute the gradient of any kind of value). Second, the module declares the three BC of our example: *Inlet*, *Outpres* and *Wall*. And finally, the module declares all the *FunctionID* corresponding to functions in our dataflow.

The Maude module EXAMPLE-1 in Listing 3 encodes the dataflow of Fig. 3.

This module is structured in five parts:

1. we first include and merge the two modules performing the core declarations, i.e., DATAFLOW and EXAMPLE-CORE;

2. we then declare the term `dconservative`, which corresponds to the root node of our dataflow containing the value `Conservative`;

3. we then construct the part of the dataflow computing `Fxc`: `Primitive` (in node `dprimitive`) is computed by applying the function `primitive` on `Conservative`; and `Fxc` (in the node `dFxc`) is computed by applying the function `convectiveFlux` on `Primitive`;

4. we then construct the part of the dataflow computing `FxcBC`: `BC(Inlet)` (in the node `dinlet`) is computed by applying the function `inlet` on `Conservative`; `BC(Outpres)` (in the node `doutpres`) is computed by applying the function `outpres` on `Conservative`; and `FxcBC` (in the node `dFxcBC`) is computed by applying the function `convectiveFluxBC` on `Primitive`, `BC(Inlet)`, and `BC(Outpres)`;

5. and finally, we conclude the dataflow with the computation of the Rhs data: *Balance* (in the node `dBalance`) is computed by applying the function `fluxBalance` on `Fxc` and `FxcBC`; and `Rhs` (in the node `dRhs`) is computed by applying the function `explicitIncrement` on *Balance*.

The Maude module EXAMPLE-2 in Listing 4 encodes the dataflow of Fig. 4.
<table><caption>Listing 2: The EXAMPLE-CORE Maude module: all declarations for our running example.</caption><tr><td>1</td><td>mod EXAMPLE-CORE is</td><td>19</td><td>op Outpres : -> BC [ctor].</td></tr><tr><td>2</td><td>sort Value BC FunctionID.</td><td>20</td><td>op Wall : -> BC [ctor].</td></tr><tr><td>3</td><td></td><td>21</td><td></td></tr><tr><td>4</td><td>*** values</td><td>22</td><td>*** function ids</td></tr><tr><td>5</td><td>op Conservative : -> Value [ctor].</td><td>23</td><td>op inlet : -> FunctionID [ctor].</td></tr><tr><td>6</td><td>op Primitive : -> Value [ctor].</td><td>24</td><td>op outpres : -> FunctionID [ctor].</td></tr><tr><td>7</td><td>op Fxc : -> Value [ctor].</td><td>25</td><td>op wallslip : -> FunctionID [ctor].</td></tr><tr><td>8</td><td>op Fxd : -> Value [ctor].</td><td>26</td><td>op primitive : -> FunctionID [ctor].</td></tr><tr><td>9</td><td>op FxcBC : -> Value [ctor].</td><td>27</td><td>op pressure : -> FunctionID [ctor].</td></tr><tr><td>10</td><td>op FxdBC : -> Value [ctor].</td><td>28</td><td>op gradient : -> FunctionID [ctor].</td></tr><tr><td>11</td><td>op Balance : -> Value [ctor].</td><td>29</td><td>op convectiveFlux : -> FunctionID [ctor].</td></tr><tr><td>12</td><td>op RHS : -> Value [ctor].</td><td>30</td><td>op convectiveFluxBC : -> FunctionID [ctor].</td></tr><tr><td>13</td><td>op Pressure : -> Value [ctor].</td><td>31</td><td>op diffusiveFlux : -> FunctionID [ctor].</td></tr><tr><td>14</td><td>op BC : BC -> Value [ctor].</td><td>32</td><td>op diffusiveFluxBC : -> FunctionID [ctor].</td></tr><tr><td>15</td><td>op Grad : Value -> Value [ctor].</td><td>33</td><td>op fluxBalance : -> FunctionID [ctor].</td></tr><tr><td>16</td><td></td><td>34</td><td>op explicitIncrement : -> FunctionID [ctor].</td></tr><tr><td>17</td><td>*** BCs</td><td>35</td><td>endm</td></tr><tr><td>18</td><td>op Inlet : -> BC [ctor].</td><td></td><td></td></tr></table>

1 mod EXAMPLE-1 is
2 *** includes dataflow abstract syntax, value and function declaration
3 protecting DATAFLOW + EXAMPLE-CORE.
4
5 *** root of the dataflow
6 op dconservative : -> Data.
7 eq dconservative = data(Conservative).
8
9 *** Fxc computation
10 op dprimitive : -> Data.
11 eq dprimitive = data(Primitive, task(primitive,
12 dconservative)).
13 op dFxc : -> Data.
14 eq dFxc = data(Fxc, task(convectiveFlux, dprimitive).
15
16 *** FxcBC computation
17 op dinlet : -> Data.
18 eq dinlet = data(BC(Inlet), task(inlet,
19 dconservative)).
20 op doutpres : -> Data.
21 eq doutpres = data(BC(Outpres), task(outpres,
22 dconservative)).
23 op dFxcBC : -> Data.
24 eq dFxcBC = data(FxcBC, task(convectiveFluxBC, dprimitive
25 dinlet doutpres)).
26
27 *** Rhs computation
28 op dBalance : -> Data.
29 eq dBalance = data(Balance, task(fluxBalance, dFxc dFxcBC).
30 op dRhs : -> Data.
31 eq dRhs = data(Rhs, task(explicitIncrement, dBalance)).
32 endm

<caption>Listing 3: The EXAMPLE-1 Maude module: encodes the dataflow of Figure 3.</caption>

Since this dataflow is more complex than the one of Fig. 3, it is structured in seven parts (rather than in five parts as in Listing 3):

1. and 2. these parts are identical to the ones in Listing 3: they first include the modules DATAFLOW and EXAMPLE-CORE, and then declare the root node of our dataflow dconservative that contains the value Conservative;

3. we then construct the chain of the Primitive data and its gradients: Primitive (in node dprimitive) is computed by applying the function primitive on Conservative; Grad(Primitive) (in node dgprimitive) is computed by applying the function gradient on Primitive; and Grad(Grad(Primitive)) (in node dggprimitive) is computed by applying the function gradient a second time, on Grad(Primitive);

4. we then construct the computation of gradient of the pressure: Pressure (in node dpressure) is computed by applying the

1 mod EXAMPLE-2 is
2 *** includes dataflow abstract syntax, value and function declaration
3 protecting DATAFLOW + EXAMPLE-CORE.
4
5 *** root of the dataflow
6 op dconservative : -> Data.
7 eq dconservative = data(Conservative).
8
9 *** Primitive with gradient computation
10 op dprimitive : -> Data.
11 eq dprimitive = data(Primitive, task(primitive,
12 dconservative)).
13 op dgprimitive : -> Data.
14 eq dgprimitive = data(Grad(Primitive), task(gradient,
15 dgprimitive)).
16
17 eq dgprimitive = data(Grad(Grad(Primitive))), task(gradient,
18 dgprimitive).
19
*** Grad(Pressure) computation
20 op dpressure : -> Data.
21 eq dpressure = data(Pressure, task(pressure, dprimitive)).
22 op dgpressure : -> Data.
23 eq dgpressure = data(Grad(Pressure), task(gradient,
24 dpressure)).
25
*** Fxc and Fxd computation
26 op dFxc : -> Data.
27 eq dFxc = data(Fxc, task(convectiveFlux, dprimitive
28 dgprimitive)).
29
30 op dFxd : -> Data.
31 eq dFxd = data(Fxd, task(diffusiveFlux, dprimitive
dgprimitive)).
32
33
34 *** FxcBC and FxdBC computation
35 op dwall : -> Data.
36 eq dwall = data(BC(Wall), task(wall, dconservative)).
37 op dFxcBC : -> Data.
38 eq dFxcBC = data(FxcBC, task(convectiveFluxBC, dwall
dprimitive dgprimitive)).
39
40 op dFxdBC : -> Data.
41 eq dFxdBC = data(FxdBC, task(diffusiveFluxBC, dwall dprimitive
dgprimitive dggprimitive)).
42
43
44 *** Rhs computation
45 op dBalance : -> Data.
46 eq dBalance = data(Balance, task(fluxBalance, dFxc dFxd dFxcBC
dFxdBC)).
47
48 op dRhs : -> Data.
49 eq dRhs = data(Rhs, task(explicitIncrement, dBalance)).
50 endm

<caption>Listing 4: The EXAMPLE-2 Maude module: encodes the dataflow of Figure 4.</caption>
function pressure on Primitive; and Grad (Pressure) (in node dgpressure) is computed by applying the function gradient on Pressure;

5. we then construct the computation of the convective and diffusive flows on the zone: Fxc (in the node dFxc) is computed by applying the function convectiveFlux on Primitive and Grad (Primitive); Fxd (in the node dFxd) is computed by applying the function diffusiveFlux on Primitive, Grad (Primitive) and Grad (Grad (Primitive));

6. similarly, we construct the computation of the convective and diffusive flows on the boundary: BC(Wall) (in the node dwell) is computed by applying the function wall on Conservative; FxcBC (in the node dFxcBC) is computed by applying the function convectiveFluxBC on BC(Wall), Primitive and Grad(Primitive); FxdBC (in the node dFxdBC) is computed by applying the function diffusiveFluxBC on BC(Wall), Primitive, Grad(Primitive) and Grad(Grad(Primitive));

7. and finally, we conclude the dataflow with the computation of the Rhs data: Balance (in the node dBalance) is computed by applying the function fluxBalance on Fxc, Fxd, FxcBC and FxdBC; and Rhs (in the node dRhs) is computed by applying the function explicitIncrement on Balance.

### 3. Model

This section presents the main elements of our approach. First, we recall the concepts of signatures and terms used in rewriting. We then present our DSL without its DOP extension and describe the algorithm that transforms any DSL program into rewriting rules. Finally, we describe the full version of our DSL, and introduce the flattening algorithm that generates the variant of an input DSL program L for an input product p of the associated SPL.

#### 3.1. Dataflow term signature

As illustrated in Section 2, a signature that encodes our dataflow is structured into two parts: one part that creates the dataflow structure (with, e.g., constructors data and task) and is common to all dataflows, and one user part that declares which values and functions are available in the dataflow construction, which is specific to each dataflow.

Here, we first recall the definitions for order-sorted signatures and terms. We then define the two parts of a dataflow signature.

##### 3.1.1. Preliminary definitions

We provide some notation and a basic definition over sets and ordered sets.

**Definition 1 (S-Sorted Set).** Given a set $S$ and an $S$-indexed family $V = \{V_s\}_{s \in S}$, we write $v : s \in V$ for $v \in V_s$. Moreover, we denote by $S^\infty$ the set $\bigcup_{i=1}^\infty S^i$.

Given a partially ordered set (poset) $S = (S, <)$, an $S$-sorted set is an $S$-indexed family $V = \{V_s\}_{s \in S}$ such that $s < s'$ implies $V_s \subseteq V_{s'}$. Moreover, we add a partial order to $S^\infty$ with

$$ (s_1, \dots, s_n) < (s'_1, \dots, s'_n) \text{ iff } (\exists 1 \le i \le n, s_i < s'_i) \land (\forall 1 \le j \le n, s_j \le s'_j) $$

The following definition specifies the arity of term constructors for a given ordered set of sorts $S$.

**Definition 2 (S-Arity).** Given a poset $S = (S, <)$, an $S$-arity $A$ is a subset of $S^\infty$ such that for all $(s_1, \dots, s_n)$, $(s'_1, \dots, s'_n) \in A$ with $s_i \le s'_i$ for all $1 \le i \le n-1$, then $s_n \le s'_n$. For all $(s_1, \dots, s_n) \in A$ with $n > 1$, we write $(s_1, \dots, s_{n-1}) \to s_n$ as syntactic sugar for $(s_1, \dots, s_n)$.

The following definition introduces an order-sorted signature for a given ordered set of sorts $S$.

$$ \begin{aligned} S &::= \text{vars } (v : s)^* (F)^* & \text{Specification} \\ F &::= \text{fun } f : \text{inputs } (t)^* \text{ outputs } (t)^* & \text{Function Specification} \end{aligned} $$

<caption>Fig. 5. Static syntax of function specification.</caption>

**Definition 3 (S-Sorted Signature).** Given a poset $S = (S, <)$, an $S$-sorted signature is an $\mathcal{A}$-sorted set $F$ with $\mathcal{A}$ being an $S$-arity.

Finally, we can define the set of terms given an ordered set of sorts $S$ and a signature $F$.

**Definition 4 (S-Sorted Set of Terms).** Given a poset $S = (S, <)$, an $S$-sorted signature $F$, and an $S$-sorted set of variables $V$, the $S$-sorted set $\mathcal{T}(F, V)$ of terms is inductively defined as follows:

* $v : s \in \mathcal{T}(F, V)$ if $v : s \in V$

* $f(t_1, \dots, t_n) : s \in \mathcal{T}(F, V)$ if $t_1 : s_1, \dots, t_n : s_n \in \mathcal{T}(F, V)$, $f : s_1, \dots, s_n \to s' \in F$ and $s' \le s$.

##### 3.1.2. Dataflow

The next definition states when a signature is dataflow-safe, i.e., it is a valid user part of a dataflow signature.

**Definition 5 (Dataflow-Safe Poset and S-Sorted Signature).** A poset $S = (S, <)$ is dataflow-safe iff both of the following hold:

(1) $S$ contains Value and FunctionID

(2) $S$ contains neither Data, nor Task

An $S$-sorted signature $F$ is dataflow-safe iff for all $s \in S$, data : $Value \to s \notin F$.

**Example 1 (A Dataflow-Safe Signature).** The Maude module EXAMPLE-CORE in Listing 2 is a dataflow-safe signature.

For the remainder of this paper, we assume a given dataflow-safe ordered set $S = (S, <)$ and an $S$-sorted signature $F$.

### 3.2. Function specification

We now present the syntax of our function specification DSL, shown in Fig. 5. We use the following name categories: $f$ is a function name; $v$ is a term variable; and $s$ is a sort. Moreover, $t$ is a term.

A specification starts with the declaration of a list of term variables, which is then followed by the list of function specifications. A function has a name $f$, a list of inputs, and a list of outputs (modeled by terms of sort Value).

The declaration order of variables and functions does not matter, so we consider this syntax up to declaration reordering (this will be used later to simplify specification transformation).

**Example 2 (Dataflow Specification).** Listing 5 shows the specification for the dataflow in Figure 3.

1 // Fxc computation
2 fun primitive: inputs Conservative outputs Primitive
3 fun convectiveFlux: inputs Primitive outputs Fxc
4
5 // FxcBC computation
6 fun inlet: inputs Conservative outputs BC(Inlet)
7 fun outpres: inputs Conservative outputs BC(Outpres)
8 fun convectiveFluxBC: inputs Primitive, BC(Inlet), BC(Outpres)
    outputs FxcBC
9
10 // Rhs computation
11 fun fluxBalance: inputs Fxc, FxcBC outputs Balance
12 fun explicitIncrement: inputs Balance outputs Rhs

**Listing 5:** Function specification for the dataflow in Listing 3.
<figure><img src="image_8.png" /><figcaption>Fig. 6. Translation rules from function specifications into Maude.</figcaption></figure>

This specification starts with the functions used in the Fxc computation part of Listing 3: primitive takes the value Conservative in parameter and returns the value Primitive; and convectiveFlux takes Primitive in parameter and returns Fxc.

The second part of the specification describes the functions used in the FxcBC computation part of Listing 3: inlet takes Conservative in parameter and returns BC(Inlet); then outpres takes Conservative in parameter and returns BC(Outpres); and finally convectiveFluxBC takes Primitive, BC(Inlet), and BC(Outpres) in parameter and returns FxcBC.

Finally, the last part of the specification describes the functions used in the Rhs computation part of Listing 3: fluxBalance takes Fxc and FxcBC in parameter and returns Balance, while explicitIncrement takes Balance in parameter and returns Rhs.

### 3.3. From function specifications to Maude rewriting rules

Fig. 6 shows the rules to translate function specifications into Maude rewriting rules. The first rule takes the specification of a function *f* and for each of its outputs *o*<sub>*i*</sub>, it generates a rewriting rule that adds to any node containing *o*<sub>*i*</sub> not being computed (modeled by *data*(*o*<sub>*i*</sub>)) the task that uses *f* to compute *o*<sub>*i*</sub> (modeled by *task*(*f*, *data*(*i*<sub>*i*</sub>) ... *data*(*i*<sub>*n*</sub>)) with *i*<sub>*i*</sub>, ..., *i*<sub>*n*</sub> the inputs of *f*).

The second rule takes a complete specification, and translates it into Maude by: replacing the variables declarations by equivalent Maude declarations; and replacing all function specifications by rewriting rules.

```
1 *** Fxc computation
2 r1 data(Primitive) => data(Primitive, task(primitive,
3   data(Conservative)))
4 r1 data(Fxc) => data(Fxc, task(convectiveFlux,
5   data(Primitive)))
6
7 *** FxcBC computation
8 r1 data(BC(Inlet)) => data(BC(Inlet), task(inlet,
9   data(Conservative)))
10 r1 data(BC(Outpres)) => data(BC(Outpres), task(outpres,
11   data(Conservative)))
12 r1 data(FxcBC) =>
13   data(FxcBC, task(convectiveFluxBC, data(Primitive)
14     data(BC(Inlet)) data(BC(Outpres)))
15
16 *** Rhs computation
17 r1 data(Balance) => data(Balance, task(fluxBalance,
18   data(Fxc) data(FxcBC)))
19 r1 data(Rhs) => data(Rhs, task(explicitIncrement,
20   data(Balance)))
```

### Listing 6: Rules generated from the specification in Figure 5.

**Example 3 (Rules Generated from a Dataflow Specification).** Listing 6 shows the rules generated from the specification in Fig. 5. For clarity, we added sections in this generated set of rewriting rules to illustrate its relation to Listing 5. This generated file starts with the rewriting rules corresponding to the functions declared in the Fxc computation part of Listing 5: adding to the node *data*(*Primitive*) the task

*task*(*primitive*, *data*(*Conservative*)); and to *data*(*Fxc*) the task *task*(*convectiveFlux*, *data*(*Primitive*))).

The second part of the set describes the rewriting rules corresponding to the functions declared in the FxcBC computation part of Listing 5: it adds the task *task*(*inlet*, *data*(*Conservative*)) to the node BC(Inlet); it adds to the node BC(Outpres) the task *task*(*outpres*, *data*(*Conservative*)); and it adds to the node data(FxcBC) the following task

```
task(convectiveFluxBC,
    data(Primitive) data(BC(Inlet)) data(BC(Outpres)))
```

Finally, the last part of the specification describes rewriting rules corresponding to the functions declared in the Rhs computation part of Listing 5: adding to node *data*(*Balance*) the task *task*(*fluxBalance*, *data*(*Fxc*) *data*(*FxcBC*)); and to node data(Rhs) *task*(*task*(*explicitIncrement*, *data*(*Balance*))).

Rewriting the term *data*(*Rhs*) with these rules will give the same term *dRhs* as in EXAMPLE-1 in Listing 3. Indeed, rewriting consists of applying the rewriting rules wherever on the input term, until none can be applied anymore. First, *data*(*Rhs*) matches the pattern of the rule in Line 20: the rule is applied, resulting in the term *data*(*Rhs*, *task*(*explicitIncrement*, *data*(*Balance*))). Second, within that term, *data*(*Balance*) matches the pattern of the rule in Line 18: the rule is applied, resulting in the term

```
data(Rhs, task(explicitIncrement,
    data(Balance, task(fluxBalance,
        data(Fxc) data(FxcBC))))
```

Following this principle, the subterms *data*(*Fxc*) and *data*(*FxcBC*) will be then rewritten with the rules in lines 5 and 12 which expands further our encoding of the dataflow. Ultimately, all data and all tasks of the dataflow in EXAMPLE-1 will be added by different applications of the rules in Figure 5.

### 3.4. Specification correction

Specifications in our DSL must validate some sanity conditions to ensure that the generated rewriting rules are well formed. Next we list these conditions.

#### 3.4.1. Naming

A first standard condition is the absence of name clashes: all variables and all functions must have different names. Since this condition is standard, in the remainder we assume that it is always satisfied. This condition can be straightforwardly checked by a standard static analysis.

#### 3.4.2. Term construction

The second set of sanity conditions ensures that the left-hand side and the right-hand side of every generated rewriting rules are well sorted, with sort *data*. First, all function names must be declared in the signature *F*, with sort *FunctionID*. Moreover, the inputs and outputs of the functions need to have sort *Value* in *F*. The rules to check the sort of the input and output terms of every function specification in a DSL program are shown in Fig. 7.
$$ \frac{t \in \text{dom}(\Gamma)}{\Gamma \vdash t : \Gamma(t)} \qquad \frac{\Gamma \vdash t_i : s_i \quad f : s_1, \dots, s_n \to s \in F}{\Gamma \vdash f(t_1, \dots, t_n) : s} \\ \Gamma \vdash t_1 : s_1 \quad s_1 \leq \text{Value} \quad \dots \quad \Gamma \vdash t_m : s_m \quad s_m \leq \text{Value} \\ \frac{\Gamma \vdash \text{fun} \quad f : \text{inputs} \ t_1, \dots, t_n \quad \text{outputs} \ t_{n+1}, \dots, t_m}{v_1 : s_1, \dots, v_n : s_n \vdash F_1 \quad \dots \quad v_1 : s_1, \dots, v_n : s_n \vdash F_m} \\ \vdash \text{vars} \ v_1 : s_1, \dots, v_n : s_n \ F_1 \ \dots, F_m} $$

<caption>Fig. 7. Checking the correctness of Input/Output definition.</caption>

The first rule states that the sort of a variable is given by its declaration (stored in Γ). The second rule states that if the term constructor f has arity s<sub>1</sub>, ..., s<sub>n</sub> → s and has parameters t<sub>i</sub> of sorts s<sub>i</sub>, then f(t<sub>1</sub>, ..., t<sub>n</sub>) has sort s. The third rule states that all inputs and outputs of a function declaration must have sort (or subset of) Value. Finally, the fourth rule creates the store Γ from the variable declaration (as previously stated) and ensures that all function specifications are correct.

**Any variable in a function's input must be present in all of the function's output.** In any term rewriting system, rewriting rules should not introduce fresh variables, i.e., the variables in the right-hand side of a rule must all be present in the left-hand side. This constraint translates into our DSL by the fact that for every function specification, all variables in the inputs of the function must be declared in every output of the function. This constraint is formalized by the following equation, where $fv(t)$ denotes the set of variables in t for any term t:

$$ \forall k \in I, f v(t_k) \subseteq \bigcap_{o \in O} f v(t_o) \qquad (1) $$

**Optional: data-driven functions.** This last condition is not mandatory to ensure the correct construction of the rewriting rules, but ensures that every function specification corresponds to a data-driven function, i.e., a function's outputs only depend on its inputs. This dependency translates into our DSL by the fact that for every function specification, the variables in the function's outputs are declared in its inputs. This constraint is formalized by the following equation:

$$ \bigcup_{k \in I} f v(t_k) = \bigcup_{o \in O} f v(t_o) \qquad (2) $$

### 3.5. Variable function specification

Finally, the syntax of an SPL over function specifications is given in Fig. 8.

An SPL starts with the definition of a feature model, with features (o)* and a propositional formula $\phi$ over features. This feature model is then followed by the core of the SPL, i.e., the initial set of variables and function declarations S, using the syntax presented in Fig. 5. The rest of the SPL declares a set of deltas (Dd)* that manipulate S, and a configuration knowledge CK.

Each delta specifies a number of changes to S. A delta comprises the keyword delta followed by the delta's name, a semicolon, and a sequence of delta operations (Do)*. A delta operation Do can add/remove a function specification definition, or modify it by adding/removing inputs and outputs (via modifying operations Dm). Moreover, a delta operation can declare or remove variables.

Configuration knowledge CK provides a mapping from products to variants by describing the connection between deltas and features. First, the DAC entries specifies an activation condition $\phi$ (a propositional formula over features) for each delta in the SPL. Second, the DAO entries specify an application order between deltas: each of these entries specifies a partial order over the set of deltas in terms of a total order on disjoint subsets of delta names.

The overall delta application order < is the transitive closure of the union of these partial orders. In this paper, we assume that < is consistent (i.e., < is a partial order) and unambiguous (i.e., all the total delta

application orders that respect < generate the same variant for each product). Techniques that allow one to check that < is unambiguous are described in the literature (Bettini et al., 2013; Lienhardt and Clarke, 2012). Without loss of generality, we assume that the total order in which delta definitions are listed is compatible with <.

**Flattening rules.** Fig. 9 shows the flattening rules that, given an input SPL L and a product p of that SPL, apply the activated deltas in L in order on the core part of L. The first two rules describe the flattening process at the SPL level. Rule (SPL-1) first ensures that p is a product of the SPL (with p ⊢ φ), takes the first delta Dd of the SPL, and applies it to the core S. This application is written $[Dd][\phi'](S)$ where $\phi'$ is the activation condition of the delta Dd. Rule (SPL-2) is used when all delta have been applied (i.e., the list of deltas that are left is empty): it still ensures that p is a product of the SPL, and then simply returns the core S of the SPL.

The next two rules deal with the application of deltas. Rule (D-1) is used when the delta is activated (checked with p ⊢ φ) and contains at least one operation Do: in that case, we apply that operation on the core S (denoted by $[Do][S]$), and use this as parameter for the rest of the operations in the deltas. Rule (D-2) is used when the delta is not activated (checked with p ⊭ φ) or does not contain any operations: in that case we simply return the core S unchanged.

The next three rules describe the flattening of delta operations on functions. Rule (F-ADD) states that to add a function F to a core S, that function must not be declared already in S (this is checked by name(F) /∈ {name(F<sub>i</sub>) | 1 ≤ i ≤ n}). If this condition is validated, we return S extended with the new function. Rule (F-REM) states that to remove a function named f from a core S, that function must be present in S (this is checked with extracting from S the function F with name(F) = f). If this condition is validated, we return S without its function f. Rule (F-MOD) states that to modify a function named f in a core S, that function must be present in S (this is checked as in rule (F-REM)). If this condition is validated, we return S with its function f modified by the set of operations (Dm)*.

The next two rules deal with the delta operations on variables, and are very similar to rules (F-ADD) and (F-REM): to add a variable, that variable must not be present already in the core; and, dually, to remove a variable, that variable must be declared in the core.

Finally, the last four rules describe the flattening of modification operations Dm. Rule (I-ADD) states that to add an input to a function specification, the added term must not already be an input of that function. Rule (O-ADD) states that to add an output to a function specification, the added term must not already be an output of that function. Rule (I-REM) states that to remove an input from a function specification, the removed term must be an input of that function. Rule (O-REM) states that to remove an output from a function specification, the removed term must be an output of that function.

**Example 4 (A Delta-Oriented SPL of Dataflows).** Listing 7 presents the SPL that contains the complete specification for our running example. Lines 2–4 present the feature model of our running example, with the root feature solver, the features mesh, zone, boundary, inlet, outpres and wall for the structure of the mesh, and the features model, convective, diffusive and order2 for the computation.

Line 6 declares the variable valueV of sort Value that is used for the declaration of the gradient function.

Lines 11–19 define the base specification of all the functions working on the mesh's zone that are used in our dataflow construction: primitive takes the value Conservative in parameter and returns the value Primitive; gradient can take any value in parameter (modeled with the variable valueV), and returns the gradient of that value (modeled with the term Grad(valueV)); pressure takes the value Primitive in parameter and returns the value Pressure; the function convectiveFlux takes Primitive in parameter and returns Fxc; and, finally, diffusiveFlux takes Primitive and Grad(Primitive) in parameter and returns Fxd.
<table><caption>Fig. 8. Syntax of deltas.</caption><tr><td>L</td><td>::= features (o)* with φ; S (Dd)* CK</td><td>Software Product Line</td></tr><tr><td>Dd</td><td>::= delta d; (Do)*</td><td>Delta</td></tr><tr><td>Do</td><td>::= add F | remove f | modify f (Dm)*<br> | add var v : s | remove var v</td><td>Delta Operation</td></tr><tr><td>Dm</td><td>::= Op Cat t</td><td>Function Modification</td></tr><tr><td>Op</td><td>::= add | remove</td><td>Modification Operation</td></tr><tr><td>Cat</td><td>::= input | output</td><td>Modification Category</td></tr><tr><td>CK</td><td>::= DAC DAO</td><td>Configuration Knowledge</td></tr><tr><td>DAC</td><td>::= delta d when φ</td><td>Activation Condition</td></tr><tr><td>DAO</td><td>::= (d)<sup>+</sup>(< (d)<sup>+</sup>)<sup>+</sup></td><td>Delta Ordering</td></tr></table>

<table><caption>Fig. 9. Flattening rules.</caption><tr><td>[SPL-1]</td><td>p ⊢ φ name(Dd) = d<br>(features (o)* when φ; S Dd (Dd)* delta d when φ'; CK)<br>▷<sub>p</sub> (features (o)* when φ; [Dd][φ](S) (Dd)* CK)</td></tr><tr><td>[SPL-2]</td><td>p ⊢ φ<br>(features (o)* when φ; S CK) ▷<sub>p</sub> S</td></tr><tr><td>[D-1]</td><td>p ⊢ φ<br>[delta d; Do (Do)*][φ](S)<br>▷<sub>p</sub> [delta d; (Do)*][φ]([Do](S))</td></tr><tr><td>[D-2]</td><td>p ⊢ φ ∨ (Do)* = ε<br>[delta d; (Do)*][φ](S) ▷<sub>p</sub> S</td></tr><tr><td>[F-ADD]</td><td>name(F) ∉ {name(F<sub>i</sub>) | 1 ≤ i ≤ n}</td></tr><tr><td>[F-REM]</td><td>name(F) = f<br>[remove f] (vars (v : s)* F<sub>i</sub> ... F<sub>n</sub>) ▷<sub>p</sub> vars (v : s)* F<sub>i</sub> ... F<sub>n</sub> F</td></tr><tr><td>[F-MOD]</td><td>name(F) = f<br>[modify f (Dm)*] (vars (v : s)* F<sub>i</sub> (F)*) ▷<sub>p</sub> vars (v : s)* [(Dm)*] (F<sub>i</sub>) (F)*</td></tr><tr><td>[V-ADD]</td><td>v ∉ {v<sub>i</sub> | 1 ≤ i ≤ n}</td></tr><tr><td>[V-REM]</td><td>[add var v : s] (vars v<sub>1</sub> : s<sub>1</sub>, ..., v<sub>n</sub> : s<sub>n</sub> (F)*) ▷<sub>p</sub> vars v<sub>1</sub> : s<sub>1</sub>, ..., v<sub>n</sub> : s<sub>n</sub>, v : s (F)*</td></tr><tr><td>[I-ADD]</td><td>t ∉ {t<sub>i</sub> | 1 ≤ i ≤ n}</td></tr><tr><td>[I-REM]</td><td>[remove input t] (fun f : inputs t<sub>1</sub> ... t<sub>n</sub> outputs (t')*)<br>▷<sub>p</sub> fun f : inputs t<sub>1</sub> ... t<sub>n</sub> t outputs (t')*</td></tr><tr><td>[O-ADD]</td><td>t ∉ {t<sub>i</sub> | 1 ≤ i ≤ n}</td></tr><tr><td>[O-REM]</td><td>[add output t] (fun f : inputs (t')* outputs t<sub>1</sub> ... t<sub>n</sub>)<br>▷<sub>p</sub> fun f : inputs (t')* outputs t<sub>1</sub> ... t<sub>n</sub> t</td></tr><tr><td>[I-ADD]</td><td>t ∉ {t<sub>i</sub> | 1 ≤ i ≤ n}</td></tr><tr><td>[I-REM]</td><td>[remove input t] (fun f : inputs t (t')* outputs (t'')*)<br>▷<sub>p</sub> fun f : inputs (t')* outputs (t'')*</td></tr><tr><td>[O-ADD]</td><td>t ∉ {t<sub>i</sub> | 1 ≤ i ≤ n}</td></tr><tr><td>[O-REM]</td><td>[remove output t] (fun f : inputs (t')* outputs t (t'')*)<br>▷<sub>p</sub> fun f : inputs (t')* outputs (t'')*</td></tr></table>
1 features solver mesh zone boundary inlet outpres wall
2 model convective diffusive order2
3 with solver /\ mesh /\ boundary /\ zone /\ model /\ convective /\ (inlet /\ outpres /\ wall);
4
5
6 vars valueV: Value
7
8 /// Base Artifact
9 // functions on zone
10 fun primitive: inputs Conservative
11 outputs Primitive
12 fun gradient: inputs valueV
13 outputs Grad(valueV)
14 fun pressure: inputs Primitive
15 outputs Pressure
16 fun convectiveFlux: inputs Primitive
17 outputs Fxc
18 fun diffusiveFlux: inputs Primitive
19 Grad(Primitive) outputs Fxd
20
21 // functions on boundaries
22 fun inlet: inputs Conservative
23 outputs BC(Inlet)
24 fun outpres: inputs Conservative
25 outputs BC(Outpres)
26 fun wall: inputs Conservative
27 outputs BC(Wall)
28 fun convectiveFluxBC: inputs Primitive
29 outputs FxcBC
30 fun diffusiveFluxBC: inputs Primitive
31 Grad(Primitive) outputs FxdBC
32
33 // Rhs
34 fun fluxBalance: inputs Fxc, FxcBC
35 outputs Balance
36 fun explicitIncrement: inputs Balance
37 outputs Rhs

38 /// DELTA
39 // boundaries
40 delta d_inlet;
41 modify convectiveFluxBC
42 add input BC(Inlet)
43 modify diffusiveFluxBC
44 add input BC(Inlet)
45 delta d_outpres;
46 modify convectiveFluxBC
47 add input BC(Outpres)
48 modify diffusiveFluxBC
49 add input BC(Outpres)
50 delta d墙;
51 modify convectiveFluxBC
52 add input BC(Wall)
53 modify diffusiveFluxBC
54 add input BC(Wall)
55
56 // computation
57 delta d_diffusive;
58 modify fluxBalance
59 add input Fxd add input FxdBC
60 delta d_order2;
61 modify convectiveFlux
62 add input Grad(Primitive)
63 modify convectiveFluxBC
64 add input Grad(Primitive)
65 modify diffusiveFlux
66 add input Grad(Grad(Primitive))
67 modify diffusiveFluxBC
68 add input Grad(Grad(Primitive))
69
70 delta d_inlet when inlet;
71 delta d_outpres when outpres;
72 delta d墙 when wall;
73 delta d_diffusive when diffusive;
74 delta d_order2 when order2;

<caption>Listing 7: Complete Software Product Line of our running example.</caption>

Lines 23–31 define the base specification of all the functions working on the mesh’s boundaries that are used in our dataflow construction: inlet takes Conservative in parameter and returns BC(Inlet); outpres takes Conservative in parameter and returns BC(Outpres); wall takes Conservative in parameter and returns BC(Wall); convectiveFluxBC takes Primitive, in parameter and returns FxcBC; and diffusiveFluxBC takes Primitive, in parameter and returns FxdBC.

Finally, lines 35–37 define the base specification of the remaining functions: fluxBalance takes Fxc and FxcBC in parameter and returns Balance; while explicitIncrement takes Balance in parameter and returns Rhs.

The rest of the SPL declares the deltas that modify the base specifications with respect to the selected features.

Lines 40–44 describe the delta d_inlet that adds BC(Inlet) as input of the functions convectiveFluxBC and diffusiveFluxBC in case the feature inlet is selected. Lines 45 to 49 describe the delta d_outpres that adds BC(Outpres) as input of the functions convectiveFluxBC and diffusiveFluxBC in case the feature outpres is selected. Lines 50–54 describe the delta d墙, which adds BC(Wall) as input of the functions convectiveFluxBC and diffusiveFluxBC in case the feature wallslip is selected. Lines 57–59 state that if the user want to also compute the diffusive part of the flux (i.e., if the feature diffusive is selected), the function fluxBalance now takes two more arguments: Fxd and FxdBC. Lines 60–68 state that if the user wants to compute the flux with an order 2 precision, i.e., when the feature order2 is selected, the functions convectiveFlux and convectiveFluxBC now take also Grad(Primitive) in arguments, and the functions diffusiveFlux and diffusiveFluxBC now take also Grad(Grad(Primitive)) in arguments.

Finally, lines 70–74 define the previously described activation conditions of the deltas. No order between deltas is specified: there are no restrictions on the order in which they can be applied.

## 4. Static analysis

This section describes the different analyses ensuring the correct definition of an SPL L. These analyses are structured in three categories: the first analysis ensures that all products generate a variant by checking that the application conditions of all delta in L are validated; the second set of analyses ensures that a generated variant is well constructed, i.e., all the input and output terms are well sorted, with sort Value, and the constraints modeled by Eqs. (1) and (2) are validated; and, finally, the last analysis ensures that a dataflow can be generated from a variant by ensuring that the corresponding rewriting rules always terminate.

Most of these analyses are inspired by Damiani and Lienhardt (2016) and follow the same principle of generating a SAT constraint that is valid if and only if the analyzed property holds. The exception is the analysis of termination, which generates a universally quantified SAT constraint. Moreover, like in Damiani and Lienhardt (2016), our analysis is based on the type uniformity guideline, which is stated as follows in our context.

**Type Uniformity Guideline** Ensure that every time a variable v is declared or added, it always has the same sort.

This guideline ensures that in all variants, given that every used variable is declared, the analysis checking that the functions’ inputs and outputs are well sorted, with sort Value, is always the same and can be performed on the SPL directly with the rules already given in Fig. 7. That way, we reduce checking the term well-sortedness in variants into checking that all used variables are declared.

**Example 5 (Type Uniformity).** Our complete running example presented in Listing 7 contains only one variable valueV, declared in the base artifact with sort Value. Hence this variable always has the same sort every time it is declared, and so our running example is type uniform.
To simplify the presentation of our analysis, we consider in the rest of this section that the base artifact of an SPL is modeled by a delta named base which is always activated and always applied before the other deltas. Before we present the different analyses, we introduce a set of getters on top of which these different analyses are constructed.

### 4.1. Getters on SPLs

All our analyses are based on only two sets of getters. First, we have getters that introspect the variability of an SPL.

**Notation 1.** Given an SPL L, we denote by fm(L) the constraint over feature names corresponding to the feature model of the SPL. Moreover, we denote by act(L) the constraint stating that every delta name in L is equivalent to its activation condition.

Second, we need to relate the SPL variability to the variable names, function names, inputs, and outputs, which are manipulated during the application of the SPL's deltas. So, we first define the notion of path to have a common notation for all these manipulated elements, and then introduce the three getters we use.

**Definition 6 (Paths in an SPL).** A path is either a variable name v, a function name f, or a word of the form f. field_t.T, where f is a function name; field_t is an element of {input, output}; and T is a term of sort Value.

For a specification SPL L, we denote by P(L) the set of paths occurring in L.

**Definition 7 (Getters on Paths).** Given a specification SPL L and a path $\rho \in P(L)$, we denote by:

* add(L, $\rho$) the set of delta names d that add the path $\rho$ in L;

* rem(L, $\rho$) the set of delta names d that remove the path $\rho$ in L;

* mod(L, $\rho$) the set of delta names d that modify the path $\rho$ in L.

Moreover, given a path $\rho$, we denote by prefix($\rho$) the set of prefixes of $\rho$.

**Example 6 (Paths and Getters).** We illustrate the previous two definitions by giving the value of the path getters for the running example L presented in Listing 7. Since this list is long, we split it into 13 different parts.

1. The variable valueV corresponds to the path valueV, and since that variable is declared in the base artifact without ever being manipulated, we have add(L, valueV) = {base} and rem(L, valueV) = mod(L, valueV) = $\emptyset$.

2. The function primitive corresponds to the three paths

primitive, primitive.input Conservative,
primitive.output.Primitive

and since that function is declared in the base artifact without ever being manipulated, we have add(L, $\rho$) = {base} and rem(L, $\rho$) = mod(L, $\rho$) = $\emptyset$ for $\rho$ being any of these paths.

3. The function gradient corresponds to the three paths

gradient, gradient.input.valueV,
gradient.output.Grad(valueV)

and since that function is declared in the base artifact without ever being manipulated, we have add(L, $\rho$) = {base} and rem(L, $\rho$) = mod(L, $\rho$) = $\emptyset$ for $\rho$ being any of these paths.

4. The function pressure corresponds to the three paths

pressure, pressure.input.Primitive,
pressure.output.Pressure

and since that function is declared in the base artifact without ever being manipulated, we have add(L, $\rho$) = {base} and rem(L, $\rho$) = mod(L, $\rho$) = $\emptyset$ for $\rho$ being any of these paths.

5. The function convectiveFlux corresponds to the four paths
convectiveFlux, convectiveFlux.input.Primitive,
convectiveFlux.input.Grad(Primitive),
convectiveFlux.output.Fxc

This function is first declared in the base artifact, and then modified by the d_order2 delta, which gives:

* add(L, $\rho$) = {base} for

$$ \rho \in \left\{ \begin{array}{l} \text{convectiveFlux,} \\ \text{convectiveFlux.input.Primitive,} \\ \text{convectiveFlux.output.Fxc} \end{array} \right\} $$

* add(L, convectiveFlux.input.Grad(Primitive)) = {d_order2}

* rem(L, $\rho$) = $\emptyset$ for $\rho$ being any path related to convectiveFlux

* mod(L, convectiveFlux) = {d_order2}

6. The function diffusiveFlux corresponds to the five paths

diffusiveFlux, diffusiveFlux.input.Primitive,
diffusiveFlux.input.Grad(Primitive),
diffusiveFlux.input.Grad(Grad(Primitive)),
convectiveFlux.output.Fxd

This function is first declared in the base artifact, and then modified by the d_order2 delta, which gives:

* add(L, $\rho$) = {base} for

$$ \rho \in \left\{ \begin{array}{l} \text{diffusiveFlux, diffusiveFlux.input.Primitive,} \\ \text{diffusiveFlux.input.Grad(Primitive),} \\ \text{diffusiveFlux.output.Fxd} \end{array} \right\} $$

* add(L, diffusiveFlux.input.Grad(Grad(Primitive))) = {d_order2}

* rem(L, $\rho$) = $\emptyset$ for $\rho$ being any path related to diffusiveFlux

* mod(L, diffusiveFlux) = {d_order2}

7. The function inlet corresponds to the three paths

inlet, inlet.input.Primitive,
inlet.output.BC(Inlet)

and since that function is declared in the base artifact without ever being manipulated, we have add(L, $\rho$) = {base} and rem(L, $\rho$) = mod(L, $\rho$) = $\emptyset$ for $\rho$ being any of these paths.

8. The function outpres corresponds to the three paths

outpres, outpres.input.Primitive,
outpres.output.BC(outpres)

and since that function is declared in the base artifact without ever being manipulated, we have add(L, $\rho$) = {base} and rem(L, $\rho$) = mod(L, $\rho$) = $\emptyset$ for $\rho$ being any of these paths.

9. The function wall corresponds to the three paths

wall, wall.input.Primitive,
wall.output.BC(Wall)

and since that function is declared in the base artifact without ever being manipulated, we have add(L, $\rho$) = {base} and rem(L, $\rho$) = mod(L, $\rho$) = $\emptyset$ for $\rho$ being any of these paths.

10. The function convectiveFluxBC corresponds to the seven paths

convectiveFluxBC, convectiveFluxBC.input.Primitive,
convectiveFluxBC.input.Grad(Primitive),
convectiveFluxBC.input.BC(Inlet),
convectiveFluxBC.input.BC(Outpres),
convectiveFluxBC.input.BC(Wall),
convectiveFluxBC.output.FxcBC

This function is first declared in the base artifact, and then modified by the `d_inlet`, `d_outpres`, `d墙` and `d_order2`, deltas, which gives:

* `add(L, ρ) = {base}` for

$$ \rho \in \left\{ \begin{array}{l} \text{convectiveFluxBC.} \\ \text{convectiveFluxBC.input.Primitive,} \\ \text{convectiveFluxBC.output.FxcBC} \end{array} \right\} $$

* `add(L, convectiveFluxBC.input.BC(Inlet)) = {d_inlet}`

* `add(L, convectiveFluxBC.input.BC(Outpres)) = {d_outpres}`

* `add(L, convectiveFluxBC.input.BC(Wall)) = {d墙}`

* `add(L, convectiveFluxBC.input.Grad(Primitive)) = {d_order2}`

* `rem(L, ρ) = ∅` for ρ being any path related to `convectiveFluxBC`

* `mod(L, convectiveFluxBC) = {d_inlet, d_outpres, d墙, d_order2}`

## 11. The function `diffusiveFluxBC` corresponds to the eight paths

diffusiveFluxBC, diffusiveFluxBC.input.Primitive,
diffusiveFluxBC.input.Grad(Primitive),
diffusiveFluxBC.input.Grad(Grad(Primitive)),
diffusiveFluxBC.input.BC(Inlet),
diffusiveFluxBC.input.BC(Outpres),
diffusiveFluxBC.input.BC(Wall),
diffusiveFluxBC.output.FxcBC

This function is first declared in the base artifact, and then modified by the `d_inlet`, `d_outpres`, `d墙` and `d_order2`, deltas, which gives:

* `add(L, ρ) = {base}` for

$$ \rho \in \left\{ \begin{array}{l} \text{diffusiveFluxBC.} \\ \text{diffusiveFluxBC.input.Primitive,} \\ \text{diffusiveFluxBC.input.Grad(Primitive),} \\ \text{diffusiveFluxBC.output.FxcBC} \end{array} \right\} $$

* `add(L, diffusiveFluxBC.input.BC(Inlet)) = {d_inlet}`

* `add(L, diffusiveFluxBC.input.BC(Outpres)) = {d_outpres}`

* `add(L, diffusiveFluxBC.input.BC(Wall)) = {d墙}`

* `add(L, diffusiveFluxBC.input.Grad(Grad(Primitive))) = {d_order2}`

* `rem(L, ρ) = ∅` for ρ being any path related to `convectiveFluxBC`

* `mod(L, diffusiveFluxBC) = {d_inlet, d_outpres, d墙, d_order2}`

## 12. The function `fluxBalance` corresponds to the six paths

fluxBalance, fluxBalance.input.Fxc, fluxBalance.input.Fxd,
fluxBalance.input.FxcBC, fluxBalance.input.FxdBC,
fluxBalance.output.Balance

This function is first declared in the base artifact, and then modified by the `d_diffusive` delta, which gives:

* `add(L, ρ) = {base}` for

$$ \rho \in \left\{ \begin{array}{l} \text{fluxBalance, fluxBalance.input.Fxc,} \\ \text{fluxBalance.input.FxcBC,} \\ \text{convectiveFlux.output.Balance} \end{array} \right\} $$

* `add(L, ρ) = {d_diffusive}` for

$$ \rho \in \{\text{fluxBalance.input.Fxd, fluxBalance.input.FxdBC}\} $$

* `rem(L, ρ) = ∅` for ρ being any path related to `fluxBalance`

* `mod(L, fluxBalance) = {d_diffusive}`

## 13. Finally, the function `explicitIncrement` corresponds to the three paths

explicitIncrement,
explicitIncrement.input.Balance,
explicitIncrement.output.Rhs

and since that function is declared in the base artifact without ever being manipulated, we have `add(L, ρ) = {base}` and `rem(L, ρ) = mod(L, ρ) = ∅` for ρ being any of these paths.

## 4.2. Applicability constraints

Applicability corresponds to the fact that delta operations do not fail (i.e., they all can be applied). As previously stated, this analysis corresponds to the generation of a constraint, which comprises three validation parts: checking if delta operations adding a path are valid; checking if delta operations removing a path are valid; and checking if delta operations modifying a path are valid.

### 4.2.1. Addition operation

Given a specification SPL L, the constraint for checking that no addition operation of a path $ρ \in P(L)$ fails is as follows:

$$ \text{predADD}(L, \rho) = \bigwedge_{d \neq d'} (d \wedge d' \Rightarrow \bigvee_{d''} d'') \quad \text{with} \quad \left\{ \begin{array}{l} d, d' \in \text{add}(L, \rho), d'' \in \bigcup_{\rho' \in \text{prefix}(\rho)} \text{rem}(L, \rho') \\ \text{and } d' < d'' < d \end{array} \right. $$

This constraint states that if two deltas add the same path, then there must be a third one in between that removes it.

**Example 7 (predADD(L, ρ) Constraint).** Consider the running example L presented in Listing 7: since each path ρ in this product line is introduced only once, `add(L, ρ)` is a singleton. Hence, `predADD(L, ρ)` is true for every path in L.

### 4.2.2. Removal operation

Given a specification SPL L, the constraint for checking that no removal operation of a path $ρ \in P(L)$ fails is as follows:

$$ \text{predREM}(L, \rho) = \bigwedge_d \left( d \Rightarrow \left( \bigvee_{d''} (d'' \wedge \bigwedge_{d'} \neg d') \right) \quad \text{with} \quad \left\{ \begin{array}{l} d \in \text{rem}(L, \rho), d' \in \bigcup_{\rho' \in \text{prefix}(\rho)} \text{rem}(L, \rho'), \\ d'' \in \text{add}(L, \rho) \\ \text{and } d'' < d' < d \end{array} \right. \right) $$

This constraint states that for a removal operation to succeed (in delta d), there must be a previous delta d'' that added the path to remove, with no other delta d' in between removing it first.

**Example 8 (predREM(L, ρ) Constraint).** Consider the running example L presented in Listing 7: since this example does not contain any removal operation (i.e., `rem(L, ρ) = ∅` for all path ρ in L), `predREM(L, ρ)` is true for every path ρ in L.
### 4.2.3. Modification operation

Given a specification SPL L, the constraint for checking that no modification operation of a path $\rho \in P(L)$ fails is as follows:

$$ \text{predMOD}(L, \rho) = \bigwedge_d \left( \begin{array}{l} d \Rightarrow \left( \bigvee_{d''} (d'' \wedge \bigwedge_{d'} \neg d') \right) \\ \text{with} \left\{ \begin{array}{l} d \in \text{mod}(L, \rho), d' \in \bigcup_{\rho' \in \text{prefix}(\rho)} \text{rem}(L, \rho'), \\ d'' \in \text{add}(L, \rho) \\ \text{and } d'' < d' < d \end{array} \right. \end{array} \right) $$

This constraint has the same structure as predREM(L, $\rho$) before: for a modification operation to succeed (in delta $d$), there must be a previous delta $d''$ that added the path to remove, with no other delta $d'$ in between removing it first.

**Example 9 (predMOD(L, $\rho$) Constraint).** Consider the running example L presented in Listing 7. In Example 6, we have seen that several paths corresponding to functions are modified. And since all functions are declared in the base artifact, which is always executed before any delta, we thus have the following equalities:

$$ \begin{align*} \text{predMOD}(L, \text{convectiveFlux}) &= (d\_order2 \Rightarrow \text{base}) \\ \text{predMOD}(L, \text{diffusiveFlux}) &= (d\_order2 \Rightarrow \text{base}) \\ \text{predMOD}(L, \text{convectiveFluxBC}) &= \left( \begin{array}{l} (d\_inlet \Rightarrow \text{base}) \wedge (d\_outpres \Rightarrow \text{base}) \\ \wedge (d\_wall \Rightarrow \text{base}) \wedge (d\_order2 \Rightarrow \text{base}) \end{array} \right) \\ \text{predMOD}(L, \text{diffusiveFluxBC}) &= \left( \begin{array}{l} (d\_inlet \Rightarrow \text{base}) \wedge (d\_outpres \Rightarrow \text{base}) \\ \wedge (d\_wall \Rightarrow \text{base}) \wedge (d\_order2 \Rightarrow \text{base}) \end{array} \right) \\ \text{predMOD}(L, \text{fluxBalance}) &= (d\_diffusive \Rightarrow \text{base}) \end{align*} $$

### 4.2.4. Full applicability constraint

We can now combine all the previous constraints to ensure that all delta operations are valid:

$$ \text{predAPP}(L) = \bigwedge_{\rho \in P(L)} (\text{predADD}(L, \rho) \wedge \text{predREM}(L, \rho) \wedge \text{predMOD}(L, \rho)) $$

Finally, we can bind this constraint to the variability model of the SPL to obtain the formula

$$ (fm(L) \wedge act(L)) \Rightarrow predAPP(L) $$

This formula states that if we take a product $p$ (i.e., a model of $fm(L)$), and extend it to the set of delta's activated by $p$ (i.e., a model of $act(L)$), then if the resulting model validates the constraints, then all delta operations triggered by the product $p$ will succeed, i.e., the corresponding variant can be generated. This property is formalized in the following theorem.

**Theorem 1 (Applicability Consistency).** Consider an SPL L and the following two properties on L:

1. The constraint $(fm(L) \wedge act(L)) \Rightarrow predAPP(L)$ is valid.

2. All variants of L can be generated.

Then Property 1 is equivalent to Property 2.

**Proof.** See Appendix A.3. □

**Example 10 (Applicability Consistency).** We illustrate Theorem 1 by using the running example L presented in Listing 7. In Examples 7 and 8 we have seen that predADD(L, $\rho$) and predREM(L, $\rho$) are valid for all paths $\rho$. With Example 9, we thus have that

$$ \text{predAPP}(L) = \left( \begin{array}{l} \text{predMOD}(L, \text{convectiveFlux}) \wedge \text{predMOD}(L, \text{diffusiveFlux}) \\ \wedge \text{predMOD}(L, \text{convectiveFluxBC}) \\ \wedge \text{predMOD}(L, \text{diffusiveFluxBC}) \wedge \text{predMOD}(L, \text{fluxBalance}) \end{array} \right) $$

By removing duplicate implications, we thus have

$$ \begin{align*} \text{predAPP}(L) &= (d\_inlet \Rightarrow \text{base}) \wedge (d\_outpres \Rightarrow \text{base}) \\ &\quad \wedge (d\_wall \Rightarrow \text{base}) \wedge (d\_order2 \Rightarrow \text{base}) \\ &\quad \wedge (d\_diffusive \Rightarrow \text{base}) \end{align*} $$

On the other hand, we have by definition:

$$ \begin{align*} \text{fm}(L) &= \text{solver} \wedge \text{mesh} \wedge \text{boundary} \wedge \text{zone} \wedge \text{model} \wedge \text{convective} \\ &\quad \wedge (\text{inlet} \vee \text{outpres} \vee \text{wall}) \\ \text{act}(L) &= \text{base} \wedge (d\_inlet \Leftrightarrow \text{inlet}) \wedge (d\_outpres \Leftrightarrow \text{outpres}) \\ &\quad \wedge (d\_wall \Leftrightarrow \text{wall}) \wedge (d\_order2 \Leftrightarrow \text{order2}) \\ &\quad \wedge (d\_diffusive \Leftrightarrow \text{diffusive}) \end{align*} $$

Hence, looking at the definition of the constraint in Theorem 1, since act(L) (in the left hand side of the implication) selects the Boolean variable base, all implications in the right hand side are satisfied. This constraint is thus valid, and indeed, we can see that every product of the SPL can be generated.

Now consider an erroneous definition of the SPL: suppose that the diffusiveFlux function is declared in the d_diffusive delta instead of in the base artifact. This changes the path getters into add(L, $\rho$) = {d_diffusive} for

$$ \rho \in \left\{ \begin{array}{l} \text{diffusiveFlux, diffusiveFlux.input.Primitive,} \\ \text{diffusiveFlux.input.Grad(Primitive),} \\ \text{diffusiveFlux.output.Fxd} \end{array} \right\} $$

But more importantly in our case, predMOD(L, diffusiveFlux) is modified into

$$ d\_order2 \Rightarrow \text{False} $$

since the delta that adds diffusiveFlux (i.e., d_diffusive) may not be applied before d_order2. Consequently, the constraint in Theorem 1 is not valid in this case, because the Boolean variable d_order2 may be selected in the left hand side of the implication which leads the right hand side to be false (and indeed, the variant generation will fail for any product with the feature d_order2 selected).

### 4.3. Specification validation

The analyses presented in this section check the correct definition of the generated variants, i.e., if the input and output terms are well sorted, and if the function specifications validate Eq. (1) and optionally Eq. (2). Since these analyses manipulate the paths and the variables that are present in a variant, we first define several constraints that state the presence status of these different elements in a variant.

#### 4.3.1. Path presence

Given a specification SPL L, the fact that a path $\rho \in P(L)$ is present in a variant is given by the following constraint:

$$ \text{Pre}(L, \rho) = \bigvee_d \left( d \wedge \left( \bigwedge_{d'} \neg d \right) \right) \\ \text{with} \left\{ \begin{array}{l} d \in \text{add}(L, \rho), d' \in \bigcup_{\rho' \in \text{prefix}(\rho)} \text{rem}(L, \rho') \\ \text{and } d < d' \end{array} \right. $$

This constraint states that for $\rho$ to exist, a delta must add it with no delta removing it later. Furthermore, we denote by input(L, $f$) (by output(L, $f$), respectively) the set $\{T | f.\text{input}.T \in P(L)\}$ (the set $\{T | f.\text{output}.T \in P(L)\}$, respectively).
**Example 11 (Pre(L, ρ) Constraint).** Since our running example L in Listing 7 has no remove operation, and since add(L, ρ) is a singleton for any path ρ, we have that Pre(L, ρ) is equal to the name of the delta adding ρ for any path ρ. For instance:

Pre(L, convectiveFlux.input.Grad(Primitive)) = d_order2 and Pre(L, valueV) = base

### 4.3.2. Variable presence

Given a specification SPL L, for all function names f ∈ P(L), we define the set of term variables as follows:

$$fv(L, f) = \bigcup_{f \in \{input, output\}} \{fv(T) \mid f.f.t.T \in P(L)\}$$

For all v ∈ fv(L, f), we define:

$$PrI(L, f, v) = \bigvee_{T \in \text{input}(L,f) \land v \in f(T)} \text{Pre}(L, f.\text{input}.T)$$

$$PrO(L, f, v) = \bigvee_{T \in \text{output}(L,f) \land v \in f(T)} \text{Pre}(L, f.\text{output}.T)$$

$$AbsO(L, f, v) = \bigvee_{T \in \text{output}(L,f) \land v \notin f(T)} \text{Pre}(L, f.\text{output}.T)$$

Here, PrI(L, f, v) states when the variable v is present in an input of f; PrO(L, f, v) states when the variable v is present in an output of f; and, finally, PrO(L, f, v) states whether there are outputs of f that do not contain the variable v.

**Example 12 (Variable Presence Constraints).** Looking at Example 6, with L being the running example in Listing 7, we have that

$$fv(L, \rho) = \begin{cases} \{\text{valueV}\} & \text{if } \rho = \text{gradient} \\ \emptyset & \text{else} \end{cases}$$

Consequently, the getters PrI, PrO, and AbsO are only defined on the pair (gradient, valueV) and we have:

$$PrI(L, gradient, valueV) = PrO(L, gradient, valueV) = base$$

$$AbsO(L, gradient, valueV) = False$$

### 4.3.3. Validating function specifications

Our first analysis in this section ensures that all declarations in a variant are well sorted. First, we need to ensure that all declared functions are in the signature F, sorted with FunctionID. This check does not depend on the variability, and can be done by simply parsing the SPL and checking that every function name in the SPL is declared in F with the correct sort.

Second, we need to check that the inputs and outputs of every function specification are well sorted, with sort Value. As discussed in the beginning of this section, we use the type uniformity guideline to reduce this check to two simpler tests: first, we use the rules in Fig. 7 to check the well sortedness of the inputs and outputs on the SPL directly; and second, we check that the variables used in any term present in a variant are declared in that variant. This second test is modeled by the following constraint:

$$decl(L) = \bigwedge_{f \in P(L)} \left( \left( \bigwedge_{T \in \text{input}(L,f)} \text{Pre}(L, f.\text{input}.T) \Rightarrow \bigwedge_{v \in f(T)} \text{Pre}(L, v) \right) \wedge \right. \\ \left. \bigwedge_{T \in \text{output}(L,f)} \left( \text{Pre}(L, f.\text{output}.T) \Rightarrow \bigwedge_{v \in f(T)} \text{Pre}(L, v) \right) \right)$$

The following theorem states the property expressed by the decl predicate.

**Theorem 2 (Variable Presence).** Consider an SPL L such that all variants are generable. Moreover, consider the following two properties on L:

1. The constraint (fm(L) ∧ act(L)) ⇒ decl(L) is valid.

2. All variants of L are such that all their variables are declared.

Then Property 1 is equivalent to Property 2.

**Proof.** See Appendix A.5. ☐

**Example 13 (Variable Presence).** We illustrate Theorem 2 using the running example L presented in Listing 7. From our discussion in Example 12, we can see that

$$decl(L) = (\text{Pre}(L, \text{gradient}.\text{input}.valueV) \Rightarrow \text{Pre}(L, valueV)) \wedge (\text{Pre}(L, \text{gradient}.\text{output}).\text{Grad}(valueV)) \Rightarrow \text{Pre}(L, valueV))$$

From Example 11, we can apply the definition of Pre to get

$$decl(L) = (\text{base} \Rightarrow \text{base}) \wedge (\text{base} \Rightarrow \text{base})$$

which is valid, and so the constraint in Theorem 2 is also valid.

If instead the variable valueV were declared in the d_order2 delta, decl(L) would have been equal to d_order2 ⇒ base. And since act(L) states that base is always selected while d_order2 is not, the constraint in Theorem 2 would not be valid (and indeed, any variant generated from a product without d_order2 selected would be erroneous).

### 4.3.4. Validating Eq. (1)

The second analysis of this section ensures that Eq. (1) is validated by every function in every variant of the SPL. As before, we define this analysis with the construction of a SAT constraint, namely, given a specification SPL L, we define the following formula:

$$nFree(L) = \bigwedge_{f \in P(L)} \bigwedge_{v \in fv(L,f)} (\text{PrI}(L, f, v) \Rightarrow (\text{PrO}(L, f, v) \wedge \neg \text{AbsO}(L, f, v)))$$

This constraint states that if a function f has an input or attribute T, then the variables of T must be present in one output of f. The property expressed by this constraint is stated in the following theorem.

**Theorem 3 (Input Variable Relevance).** Consider an SPL L such that all variants are generable. Moreover, consider the following two properties on L:

1. The constraint (fm(L) ∧ act(L)) ⇒ nFree(L) is valid.

2. All variants of L validate Eq. (1) from Section 3.4.2.

Then Property 1 is equivalent to Property 2.

**Proof.** See Appendix A.5. ☐

**Example 14 (Input Variable Relevance).** We illustrate Theorem 3 using the running example L presented in Listing 7. From our discussion in Example 12, we can see that

$$nFree(L) = (\text{PrI}(L, gradient, valueV)) \Rightarrow (\text{PrO}(L, gradient, valueV) \wedge \neg \text{AbsO}(L, gradient, valueV)) \\ = \text{base} \Rightarrow (\text{base} \wedge \neg \text{False}) \\ = \text{True}$$

Consequently, the constraint in Theorem 3 is valid.

Suppose now that another variable valueVV of sort Value is declared in the delta d_order2, and that the gradient function has a second output valueVV added in the delta d_order2. Since valueVV never appears in the input of gradient, we have that

$$PrI(L, gradient, valueVV) = False$$

$$PrO(L, gradient, valueVV) = d_order2$$

$$AbsO(L, gradient, valueVV) = base$$
In this case, we thus have

$$
\begin{align*}
nFree(L) &= (\PrI(L, \text{gradient}, \text{valueV}) \Rightarrow \\
&\quad (\PrO(L, \text{gradient}, \text{valueV}) \\
&\qquad \land \neg\text{AbsO}(L, \text{gradient}, \text{valueV})) \\
&\land (\PrI(L, \text{gradient}, \text{valueVV}) \Rightarrow \\
&\quad (\PrO(L, \text{gradient}, \text{valueVV}) \\
&\qquad \land \neg\text{AbsO}(L, \text{gradient}, \text{valueVV}))) \\
&= (\text{base} \Rightarrow (\text{base} \land \neg\text{False})) \\
&\qquad \land (\text{False} \Rightarrow (\text{d_order2} \land \neg\text{base})) \\
&\equiv \text{True}
\end{align*}
$$

Consequently, the constraint in **Theorem 3** is valid also in this case: indeed, the considered modification added a new output, which is transparent for Eq. (1).

Suppose finally that the new variable valueVV is now used as an input of the function gradient when the delta d_order2 is activated. Since valueVV never appears in the output of gradient, we have that

$$
\PrI(L, \text{gradient}, \text{valueVV}) = d\_\text{order2}
$$

$$
\PrO(L, \text{gradient}, \text{valueVV}) = \text{False}
$$

$$
\text{AbsO}(L, \text{gradient}, \text{valueVV}) = \text{base}
$$

In this case, we thus have

$$
\begin{align*}
nFree(L) &= (\PrI(L, \text{gradient}, \text{valueV}) \Rightarrow \\
&\quad (\PrO(L, \text{gradient}, \text{valueV}) \\
&\qquad \land \neg\text{AbsO}(L, \text{gradient}, \text{valueV}))) \\
&\land (\PrI(L, \text{gradient}, \text{valueVV}) \Rightarrow \\
&\quad (\PrO(L, \text{gradient}, \text{valueVV}) \\
&\qquad \land \neg\text{AbsO}(L, \text{gradient}, \text{valueVV}))) \\
&= (\text{base} \Rightarrow (\text{base} \land \neg\text{False})) \\
&\qquad \land (\text{d_order2} \Rightarrow (\text{False} \land \neg\text{base})) \\
&\equiv \text{d_order2} \Rightarrow \text{False}
\end{align*}
$$

Since d_order2 may be selected in the left hand side of the constraint in **Theorem 3** (i.e., *fm(L) ∧ act(L)*), this constraint is not valid in this case. And indeed, in this case, if *d_order2* is selected, the *gradient* function has an input *valueVV* that contains a variable that is not in its outputs, invalidating Eq. (1).

4.3.5. Validating Eq. (2)

This third analysis of this section ensures that Eq. (2) is validated by every function in every variant of the SPL. As before, we define this analysis by the construction of a SAT constraint, namely, given a specification SPL L, we define the following formula:

$$
nAmbiguous(L) = \bigwedge_{f \in P(L)} \bigwedge_{v \in f \lor v(L, f)} (\PrI(L, f, v) \Leftrightarrow \PrO(L, f, v))
$$

This constraint states that for all functions *f* in a variant of the SPL, if a variable *v* is in an input or attribute, then it must also be in an output, and reciprocally. The property expressed by this constraint is stated in the following theorem.

**Theorem 4 (Output Variable Dependency).** Consider an SPL *L* such that all variants are generable. Moreover, consider the following two properties on *L*:

1. The constraint (fm(L) ∧ act(L)) ⇒ nAmbiguous(L) is valid.

2. All variants of *L* validate Eq. (2) from Section 3.4.2.

Then Property 1 is equivalent to Property 2.

**Proof.** See Appendix A.5. ☐

**Example 15 (Output Variable Dependency).** We illustrate **Theorem 4** using the running example *L* presented in Listing 7. From our discussion

in Example 12, we can see that

$$
\begin{align*}
nAmbiguous(L) &= (\PrI(L, \text{gradient}, \text{valueV}) \Leftrightarrow \\
&\quad \PrO(L, \text{gradient}, \text{valueV})) \\
&= \text{base} \Leftrightarrow \text{base} \\
&\equiv \text{True}
\end{align*}
$$

Consequently, the constraint in **Theorem 4** is valid.

Suppose now that another variable valueVV of sort Value is declared in the delta d_order2, and that the gradient function has a second output valueVV added in the delta d_order2. Since valueVV never appears in the input of gradient, we have that

$$
\PrI(L, \text{gradient}, \text{valueVV}) = \text{False}
$$

$$
\PrO(L, \text{gradient}, \text{valueVV}) = d\_\text{order2}
$$

$$
\text{AbsO}(L, \text{gradient}, \text{valueVV}) = \text{base}
$$

In this case, we thus have

$$
\begin{align*}
nAmbiguous(L) &= (\PrI(L, \text{gradient}, \text{valueV}) \Leftrightarrow \\
&\quad \PrO(L, \text{gradient}, \text{valueV})) \\
&\land (\PrI(L, \text{gradient}, \text{valueVV}) \Leftrightarrow \\
&\quad \PrO(L, \text{gradient}, \text{valueVV})) \\
&= (\text{base} \Leftrightarrow \text{base}) \land (\text{False} \Leftrightarrow \text{d\_order2}) \\
&\equiv \text{False} \Leftrightarrow \text{d\_order2}
\end{align*}
$$

Since d_order2 may be selected in the left hand side of the constraint in **Theorem 3** (i.e., *fm(L) ∧ act(L)*), this constraint is not valid in this case. And indeed, in this case, if *d_order2* is selected, the *gradient* function has an output *valueVV* that contains a variable that is not in its inputs, invalidating Eq. (2).

Suppose finally that the new variable valueVV is now used as an input of the function gradient when the delta d_order2 is activated. Since valueVV never appears in the output of gradient, we have that

$$
\PrI(L, \text{gradient}, \text{valueVV}) = d\_\text{order2}
$$

$$
\PrO(L, \text{gradient}, \text{valueVV}) = \text{False}
$$

$$
\text{AbsO}(L, \text{gradient}, \text{valueVV}) = \text{base}
$$

In this case, we thus have

$$
\begin{align*}
nAmbiguous(L) &= (\PrI(L, \text{gradient}, \text{valueV}) \Leftrightarrow \\
&\quad \PrO(L, \text{gradient}, \text{valueV})) \\
&\land (\PrI(L, \text{gradient}, \text{valueVV}) \Leftrightarrow \\
&\quad (\PrO(L, \text{gradient}, \text{valueVV})) \\
&= (\text{base} \Leftrightarrow \text{base}) \land (\text{d_order2} \Leftrightarrow \text{False}) \\
&\equiv \text{d_order2} \Leftrightarrow \text{False}
\end{align*}
$$

Since d_order2 may be selected in the left hand side of the constraint in **Theorem 3** (i.e., *fm(L) ∧ act(L)*), this constraint is not valid in this case. And indeed, in this case, if *d_order2* is selected, the *gradient* function has an input *valueVV* that contains a variable that is not in its outputs, invalidating Eq. (2).

4.4. Terminating specification

Our last analysis ensures that the set of rewriting rules derived from any variant of an SPL terminates. This property implies that for any variant of an SPL and any data to compute, a corresponding dataflow model can be generated.

Our analysis is based on (Arts and Giesl, 2000), where it is proved that the termination of a set of rewriting rules is equivalent to the existence of a well-founded, weakly monotonic, and substitution-closed partial order between some terms extracted from the rewriting rules. Such a partial order is defined as follows.

**Definition 8 (A Well-Founded, weakly Monotonic, and Substitution-Closed Partial Order).** A partial order over terms < is well-founded iff there exists no infinite sequence (*a*<sub>i</sub>)<sub>i∈N</sub> with *a*<sub>i+1</sub> < *a*<sub>i</sub>. Moreover, < is weakly monotonic iff for all terms *t*<sub>1</sub>, ..., *t*<sub>*n*</sub> ∈ *T*, *t* < *t'* implies
$f(t_1, ..., t_i, t, t_{i+1}, ..., t_n) \le f(t_1, ..., t_i, t', t_{i+1}, ..., t_n)$. Finally, $<$ is closed under substitution iff for all $(l, r) \in \le$ and all substitutions $\sigma$, it holds that $(\sigma(l), \sigma(r)) \in \le$.

In the following, if $<$ is well-founded, weakly monotonic, and substitution-closed, then we denote this by $WF(<)$.

Moreover, due to the structure of our generated rewriting rules, in our case the terms that must be ordered are the input and output of the different functions. Hence, we can define this analysis by the following constraint:

$$ \text{terminating}(L) = \exists < WF(<). $$

$$ \bigwedge_{f \in P(L)} \bigwedge_{T \in \text{output}(L, f)} \bigwedge_{T' \in \text{input}(L, f)} \left( \left( \text{Pre}(f.\text{output}.T) \wedge \text{Pre}(f.\text{input}.T') \right) \Rightarrow T' < T \right) \quad (3) $$

This constraint states that for any variant of the SPL L, there must exist a well-founded, weakly monotonic, and substitution-closed partial order $<$ such that if $T$ and $T'$ are the input and the output of a function, respectively, then $T' < T$ must hold. The property expressed by this constraint is stated in the following theorem.

**Theorem 5 (Terminating Specification).** Consider an SPL L such that all variants are generable and with all the variables declared. Moreover, consider the following two properties on L:

1. The constraint $(fm(L) \wedge act(L)) \Rightarrow terminating(L)$ is valid.

2. Each variant of L results in a terminating TRS.

Then Property 1 is equivalent to Property 2.

**Proof.** See Appendix A.6. $\square$

<figure><img src="image_9.png" /></figure>

It is important to underline that since term rewriting is Turing complete, Eq. (3) is not decidable. However, there are many sound but incomplete techniques, such as (Arts and Giesl, 2000; Hirokawa and Middeldorp, 2004; Yamada, 2022), that translate the problem of finding the partial order $<$ into SAT or into linear constraints, and these techniques typically have good results in practice. Therefore, it is possible to use these techniques to transform our constraint into an existentially quantified SAT or linear constraint problem that can be managed by existing SAT or SMT solvers.

**Example 16 (Terminating Specification).** We illustrate Theorem 5 using the running example L presented in Listing 7. Define as follows the function rank that takes in parameter terms of sort Value and returns an integer:

$$ \begin{align*} \text{rank}(\text{Conservative}) &= 1 & \text{rank}(\text{Primitive}) &= 2 \\ \text{rank}(\text{BC(Inlet)}) &= 2 & \text{rank}(\text{BC(Outpres)}) &= 2 \\ \text{rank}(\text{BC(Wall)}) &= 2 & \text{rank}(\text{Pressure}) &= 3 \\ \text{rank}(\text{Grad}(T)) &= \text{rank}(T) + 1 & \text{rank}(\text{Fxc}) &= 5 \\ \text{rank}(\text{Fxd}) &= 5 & \text{rank}(\text{FxcBC}) &= 5 & \text{rank}(\text{FxdBC}) &= 5 \\ \text{rank}(\text{Balance}) &= 6 & \text{rank}(\text{Rhs}) &= 7 \end{align*} $$

Now state that given two terms $T_1$ and $T_2$ of sort Value, we have $T_1 < T_2$ iff both: $fv(T_1) = fv(T_2)$ rank($\sigma(T_2)$) < rank($\sigma(T_2)$) with $\sigma$ mapping any variable in $fv(T_1)$ to Conservative.

We can first see that $WF(<)$ holds:

* $<$ is a partial order: it is indeed clearly irreflexive, asymmetric and transitive;

* any sequence of decreasing terms $(T_i)_i$ corresponds to a sequence of the same length of decreasing natural numbers $(rank(T_i))_i$, and since the order on natural numbers is well-founded, so is $<$;

* since $rank(Grad(T)) = rank(T) + 1$, we have $Grad(T_1) < Grad(T_2)$ for all $T_1 < T_2$; moreover, since Grad is the only term constructor that has parameters, $<$ is weakly monotonic;

* finally, we can see that $<$ is substitution-closed by induction on the structure of the terms.

We can also see that for each function declared in our running example, we have $T_1 < T_2$ for any of its inputs $T_1$ and any of its outputs $T_2$:

* for the primitive function: we have Conservative < Primitive

* for the gradient function: we have valueV < Grad(valueV)

* for the pressure function: we have Primitive < Pressure

* for the convectiveFlux function: we have

$$ \text{Primitive} < \text{Fxc}, \text{Grad}(\text{Primitive}) < \text{Fxc} $$

* for the diffusiveFlux function: we have

$$ \text{Primitive} < \text{Fxd}, \text{Grad}(\text{Primitive}) < \text{Fxd}, \text{Grad}(\text{Grad}(\text{Primitive})) < \text{Fxd} $$

* for the inlet function: we have Conservative < BC(Inlet)

* for the outpres function: we have Conservative < BC(Outpres)

* for the wall function: we have Conservative < BC(Wall)

* for the convectiveFluxBC function: we have

$$ \begin{align*} \text{BC(Inlet)} &< \text{FxcBC}, \text{BC(Outpres)} < \text{FxcBC}, \text{BC(Wall)} < \text{FxcBC}, \\ \text{Primitive} &< \text{FxcBC}, \text{Grad}(\text{Primitive}) < \text{FxcBC} \end{align*} $$

* for the diffusiveFluxBC function: we have

$$ \begin{align*} \text{BC(Inlet)} &< \text{FxdBC}, \text{BC(Outpres)} < \text{FxdBC}, \text{BC(Wall)} < \text{FxdBC}, \\ \text{Primitive} &< \text{FxdBC}, \text{Grad}(\text{Primitive}) < \text{FxdBC}, \\ \text{Grad}(\text{Grad}(\text{Primitive})) &< \text{FxdBC} \end{align*} $$

* for the fluxBalance function: we have

$$ \begin{align*} \text{Fxc} &< \text{Balance}, \text{Fxd} < \text{Balance}, \text{FxcBC} < \text{Balance}, \\ \text{FxdBC} &< \text{Balance} \end{align*} $$

* for the explicitIncrement function: we have Balance < Rhs

Hence, terminating(L) is valid, which implies that the constraint in Theorem 5 is valid as well. Following Theorem 5, we thus have that every dataflow generation request submitted to our running example would terminate.

## 5. Empirical evaluation

In this section, we evaluate the approach described in this paper on a prototype. Our evaluation focuses on the feasibility of dataflow generation: we evaluate the time used for the product line flattening and rewriting steps presented in Fig. 1 and check if our approach is quick enough to consider it for an industrial application.

We first give some insights into our prototype, present our testing protocol and the corresponding results. We conclude by discussing the threats to the validity of our experiments.

### 5.1. Prototype implementation

Our prototype was designed together with the elsA development team in order to evaluate if the approach proposed in this article could serve as a basis for a new CFD tool. We constructed our implementation around three design choices.

1. We first embedded in python3 the DSL described in Section 3. This choice was motivated by the fact that python3: (i) was already well-known by the elsA development team; (ii) is a flexible language that easily embeds DSLs; and (iii) can orchestrate complex and efficient libraries implemented in other languages.
<figure><img src="image_10.png" /><figcaption>Fig. 10. Tree version of the dataflow presented in Fig. 3.</figcaption></figure>

2. We then used the `pydop` python library (Lienhardt, 2023) to handle the variability aspect of our DSL. Indeed, this library can construct Delta-Oriented Product Lines over any python object, and was thus particularly suited for our approach, where our DSL manipulates abstract function specification and terms.

3. For the term and signature part of our DSL, we implemented an ad-hoc rewriting tool in C++. The main reason we implemented an ad-hoc tool instead of using an existing rewriting engine is because of the DAG structure of the dataflows. Indeed, existing rewriting engines like Maude create a tree instead of a DAG when applying the rewriting rules. For instance, Fig. 10 would be the dataflow generated by Maude in place of the dataflow in Fig. 3: all shared subtrees are duplicated. While this difference is not relevant semantically (two objects representing the same term are logically the same and we can easily identify the identical subtrees to construct the DAG dataflow), on large dataflows the equivalent tree version generated by existing rewriting engines would have a size that is orders of magnitude larger than the expected dataflow, and would take significantly more time to generate. Our ad-hoc tool implements a naive algorithm for rewriting rule application, but ensures that each shared term is created only once.

## 5.2. Testing protocol

Since there are no standard benchmarks for dataflow generation, we constructed 597 dataflow generation problems to evaluate. We first implemented a test product line with the `elsA` development team, which contains a subpart of the configuration space available in `elsA`. This SPL extends our running example and contains 97 features, 173 functions and 1493 deltas.

Then, following our dataflow generation pipeline presented in Fig. 1, every run of our prototype needs two inputs: a product and a value to compute. For the product, we use the *uniform random configuration generator unigen* (Chakraborty et al., 2015; Soos et al., 2020) to randomly pick 597 products of the test product line.<fnref n="1" /> For the data to compute, we simply chose the value `Rhs` in all our runs.

Finally, each of the 597 runs of our prototype were executed 10 times on a single 2.5 GHz Intel Xeon CPU with 32 GB of memory that was hosting a CentOS 8 operating system.

<figure><img src="image_11.png" /><figcaption>Fig. 11. Size of generated Dataflows – the x-axis lists the 597 generated dataflows ordered by size (i.e., number of nodes + number of edges).</figcaption></figure>

<figure><img src="image_12.png" /><figcaption>Fig. 12. Computation Time w.r.t. Dataflow Size – the x-axis lists the 597 generated Dataflows ordered by size (i.e., number of nodes + number of edges).</figcaption></figure>

## 5.3. Results

To facilitate the discussion of the experiments, the figures presenting our results use a fixed ordering of the 597 dataflow generation problems we considered along the x-axis; this ordering is determined by the size (the sum of the number of nodes and the number of edges) of the generated dataflow for a given problem.

Fig. 11 illustrates the size of the generated dataflows. The smallest generated dataflow has 129 nodes and 284 edges, while the largest has 426 nodes and 1205 edges. Moreover, in all dataflows, the number of edges is between two and three times the number of nodes. This confirms our concern discussed in Section 5.1 that many subtrees of the dataflows are shared, and so existing rewriting engines would not perform efficiently on these dataflow generation problems. Indeed, we computed the size of the trees these engines would have generated: they would contain between 26043 and 150983896 nodes with an average of 10 million nodes.

Fig. 12 presents the average computation time for the *product line flattening* and *rewriting* steps of our prototype. The product line flattening step takes between 51 ms (executing 342 deltas) and 168 ms (executing 902 deltas); and the rewriting step (performing the dataflow generation itself) takes between 2 ms and 8 ms. The difference of execution time between these two steps can be explained by the fact that the SPL part of our prototype is implemented in python while the rewriting part is implemented in C++.

Moreover while the time taken by the *product line flattening* step is bounded for a given SPL by the time needed to execute all its deltas, the *rewriting* step can take an arbitrary amount of time, since the *Value to Compute* is arbitrary. Fig. 13 shows that in our test, the execution time for this step evolves linearly w.r.t. the number of nodes in the dataflow. Hence, we believe that our approach can scale to larger dataflows.

## 5.4. Threats to validity

We now conclude this section by discussing the external and internal threats to the validity of our experiments.

<footnote n="1">¹ The version of *unigen* that was available for our tests had a bug that made the tool fail whenever we specified the number of products to generate. So we used the default behavior of the tool, which gave us the arbitrary number of 597 generated products. We also tried to use the *smarch* tool (Oh et al., 2020), but never succeeded to compile it.</footnote>
<figure><img src="image_13.png" /><figcaption>Fig. 13. Rewriting Time w.r.t. Number of Nodes – the x-axis lists the 597 generated Dataflows ordered by size (i.e., number of nodes + number of edges).</figcaption></figure>

### 5.4.1. External validity

The results of the evaluation strongly depend on the dataflow generation problems considered in our test protocol. Due to the lack of standard benchmarks, we only performed our tests on one SPL, on which we considered 597 randomly selected dataflow generation problems. We plan to investigate other dataflow generation problems: in particular, in addition to problems coming from CFD applications, we would like to study other application domains to get more insights. For instance, it would be interesting to investigate how the shape of the dataflows varies w.r.t. the application domain.

### 5.4.2. Internal validity

Our prototype is constructed on top of two separate libraries: pydop and our ad-hoc rewriting engine. Using other existing tools, like FeatureIDE (Meinicke et al., 2017) (for the SPL part of our approach) and any of the existing rewriting engines (Garavel et al., 2018) may affect the execution time of our approach. We plan to repeat the experiments using other tools for comparison.

## 6. Related work

Dataflows have a structure that is similar to statecharts and transition systems, on top of which variability has already been defined, e.g., by using DOP on statecharts, resulting in delta-statecharts (Lienhardt et al., 2018); and the annotative approach on transition systems, resulting in Featured Transition Systems (FTSs) (Classen et al., 2013; ter Beek et al., 2019, 2022). While delta-statecharts and FTSs could in principle be used for modeling the dataflow model of our running example, the variation on the value of one option could have consequences all over the dataflow since a variable function could appear in many place in a dataflow. For instance, the *grad* function is variable, with different inputs and outputs, and can be used in many different tasks. Consequently, the use of delta-statecharts or FTSs would imply that the variability of *grad* must be duplicated in every task in which it is used, which is clearly not satisfactory.

Different approaches to implement SPL on specifications and code have been proposed in the literature. In our DSL we used the delta-oriented approach. We refer to a couple of surveys (Schaefer et al., 2012; Thüm et al., 2014) for a discussion of the different approaches.

Our approach for dataflow generation was largely inspired by work on type inhabitation (Urzyczyn, 1997; Dudenhefner and Rehof, 2017; Alves and Broda, 2018), in particular (Alves and Broda, 2018) uses rewriting to generate terms of a given type. Indeed, if we consider that the *Value to Compute* in Fig. 1 is a type, then constructing a dataflow computing this value corresponds to finding a term (i.e., a composition of functions) that has this type. Finally, in Gvero et al. (2013), the authors use type inhabitation to help programmers to use complex libraries: their tool suggests expressions of the expected type constructed from the libraries' functions.

## 7. Conclusion

We presented an approach to automatically generate dataflow models in an SPL setting, based on DOP and term rewriting. We provided an analysis that allows to check that for any variant of the SPL and any data to compute, a corresponding dataflow model can be generated. Moreover, we also implemented a prototype for our approach and evaluated its execution time.

In future work, we would like to address several limitations of our current approach. First, our running example considered a mesh with at most three boundaries of different types: in practice, there can be an arbitrary number of boundaries with arbitrary types. Note that this flexibility makes it so that dataflows do not have an upper bound on their size, since there is at least one task per boundary. Consequently annotative approaches on graphs like FTS, while not being satisfactory in this work, can no longer be used.

Moreover, we would like to investigate extending our DSL with the possibility to include delta operations on the S-sorted signature. That way, we could express more easily the fact that the signature is constructed together with the rest of the variant (e.g., function declaration corresponds to adding a new term constructor of sort FunctionID) instead of having a signature that is the same for all variants of an SPL. Finally, we intend to conclude the evaluation of our approach by implementing and testing the analyses described in this paper.

## Declaration of competing interest

The authors declare that they have no known competing financial interests or personal relationships that could have appeared to influence the work reported in this paper.

## Acknowledgments

The authors would like to thank the anonymous reviewers and Chiara Oberti for their useful and constructive comments. They also would like to thank the elsA development team for its work on the test product line, in particular Bertrand Michel and Bruno Maugars. The second author acknowledges funding from the Italian MUR PRIN 2020TL3X8X project T-LADIES (Typeful Language Adaptation for Dynamic, Interacting and Evolving Systems).

## Appendix. Proofs

### A.1. Preliminary notations

Given an SPL $L$, we write:

* $spec(L)$ for the constraint $fm(L) \land act(L)$

* $predAPP^*(L)$ for the constraint $spec(L) \Rightarrow predAPP(L)$

* $decl^*(L)$ for the constraint $spec(L) \Rightarrow decl(L)$

* $nFree^*(L)$ for the constraint $spec(L) \Rightarrow nFree(L)$

* $nAmbiguous^*(L)$ for the constraint $spec(L) \Rightarrow nAmbiguous(L)$

* $terminating^*(L)$ for the constraint $spec(L) \Rightarrow terminating(L)$

### A.2. Correspondence product model

**Lemma 1.** Given a specification SPL $L$ with $\mathcal{T}$ its set of features, and a product $p$ of $L$, then there exists exactly one model $I$ of $spec(L)$ such that $p = \{o | o \in \mathcal{T} \land I(o)\}$. More precisely, $I$ is such that: (i) the domain of $I$ is the set of features $\mathcal{T}$ plus the set of delta names in $L$; (ii) all the variables corresponding to features selected for that product are set to true; (iii) all the variables corresponding to modules activated for the construction of this product's variant are set to true; and (iv) all the other variables in $dom(I)$ are set to false.

Reciprocally, if $spec(L)$ has a model $I$, then the set $\{o | o \in \mathcal{T} \land I(o)\}$ is a product of $L$.
**Proof.** This follows direct from the way the formula $\text{spec}(L)$ is constructed. □

### A.3. Proof of Theorem 1 (applicability consistency)

**Theorem 1 (Applicability Consistency).** Consider an SPL L and the following two properties on L:

1. The constraint ($fm(L) \wedge act(L)$) ⇒ predAPP(L) is valid.

2. All variants of L can be generated.

Then Property 1 is equivalent to Property 2.

**Proof.** Let first consider that L has no product: by Lemma 1, $\text{spec}(L)$ has no model, and so the constraint $\text{predAPP}^*(L)$ is valid. Moreover, since L has no product, it also has no variant, and so all of them can be generated. Hence, both Property 1 and Property 2 are valid statements.

Let us now consider that the product line has at least one product: we prove the equivalence by proving each implication independently.

$$ \text{Case 1} \Rightarrow 2 $$

Suppose chosen a specific product $p$ of L: by Lemma 1, there exists exactly one model $I$ of $\text{spec}(L)$ such that $p = \{o | o \in \mathcal{F} \wedge I(o)\}$. Because $\text{predAPP}^*(L)$ is valid and $\text{dom}(I) = f v(\text{predAPP}^*(L))$, $I$ is also a model of $\text{predAPP}(L)$. Let us now consider the sequence $d_1, \dots, d_n$ of delta that are applied to generate the variant corresponding to $p$ ($d_1$ being the core of L): we prove that for all $i \in [1..n]$ no errors occurs in the deltas $d_1, \dots, d_i$ by induction on $i$. With $i = 1$, as $d_1$ is the core of L, it only adds variables and function specifications to an empty specification. It thus trivially succeeds. Let now consider $i = j + 1$ with $d_1, \dots, d_j$ containing no errors. We have eight cases.

1. If $d_i$ contains no operations, then $d_i$ succeed for any input specification, and so $d_1, \dots, d_i$ contains no errors.

2. If $d_i$ adds a function $F$ with name($F$) = $f$: by construction $d_i \in \text{add}(L, f)$. Since $I$ is a model of $\text{predADD}(L, f)$ and $I(d_i)$ is true, we have that $I \vdash \bigwedge_{d'} d' \Rightarrow \bigvee_{d''} d''$ with $d' < d'' < d_i$, $d' \in \text{add}(L, f)$ and $d'' \in \text{rem}(L, f)$. Hence, if there exists $1 \le k \le j$ with $d_k \in \text{add}(L, f)$, there must exist $k < l \le j$ with $d_l \in \text{rem}(L, f)$. Consequently, the specification in input of $d_i$ does not contain $f$, and so the operation succeeds.

3. If $d_i$ removes a function $F$ with name($F$) = $f$: by construction $d_i \in \text{rem}(L, f)$. Since $I$ is a model of $\text{predREM}(L, f)$ and $I(d_i)$ is true, we have that $I \vdash \bigvee_{d'} d'' \wedge \bigwedge_{d'} \neg d'$ with $d'' < d' < d_i$, $d' \in \text{rem}(L, f)$ and $d'' \in \text{add}(L, f)$. Hence, there must exist $1 \le k \le j$ with $d_k \in \text{add}(L, f)$, such that no $d_j \in \text{rem}(L, f)$ with $k < l \le j$. Consequently, the specification in input of $d_i$ does contain $f$, and so the operation succeeds.

4. If $d_i$ modifies a function $F$ with name($F$) = $f$: by construction $d_i \in \text{mod}(L, f)$. Since $I$ is a model of $\text{predMOD}(L, f)$ and $I(d_i)$ is true, we have that $I \vdash \bigvee_{d'} d'' \wedge \bigwedge_{d'} \neg d'$ with $d'' < d' < d_i$, $d' \in \text{rem}(L, f)$ and $d'' \in \text{add}(L, f)$. Hence, there must exist $1 \le k \le j$ with $d_k \in \text{add}(L, f)$, such that no $d_i \in \text{rem}(L, f)$ with $k < l \le j$. Consequently, the specification in input of $d_i$ does contain $f$, and so the operation succeeds.

5. If $d_i$ adds an input $T$ in the function $f$: by construction

$$ d_i \in \text{add}(L, f.\text{input.}T) \cap \text{mod}(L, f) $$

Since $d_i \in \text{mod}(L, f)$ with Case 4 we can deduce that $f$ is in the input specification of $d_i$, and with a reasoning similar to Case 2, we can show that $T$ is not an input of $f$ in that specification. Hence the operation succeeds.

6. If $d_i$ removes an input $T$ from the function $f$: by construction

$$ d_i \in \text{rem}(L, f.\text{input.}T) \cap \text{mod}(L, f) $$

Since $d_i \in \text{mod}(L, f)$ with Case 4 we can deduce that $f$ is in the input specification of $d_i$, and with a reasoning similar to Case 3,

we can show that $T$ is an input of $f$ in that specification. Hence the operation succeeds.

7. If $d_i$ adds an output $T$ in the function $f$: by construction

$$ d_i \in \text{add}(L, f.\text{output.}T) \cap \text{mod}(L, f) $$

Since $d_i \in \text{mod}(L, f)$ with Case 4 we can deduce that $f$ is in the input specification of $d_i$, and with a reasoning similar to Case 2, we can show that $T$ is not an output of $f$ in that specification. Hence the operation succeeds.

8. If $d_i$ removes an output $T$ from the function $f$: by construction

$$ d_i \in \text{rem}(L, f.\text{output.}T) \cap \text{mod}(L, f) $$

Since $d_i \in \text{mod}(L, f)$ with Case 4 we can deduce that $f$ is in the input specification of $d_i$, and with a reasoning similar to Case 3, we can show that $T$ is an output of $f$ in that specification. Hence the operation succeeds.

Consequently, all possible operations in $d_i$ succeed, and so $d_1, \dots, d_i$ contains no errors.

$$ \text{Case 1} \Leftarrow 2 $$

We prove this result by contraposition: we assume $\text{predAPP}^*(L)$ is not valid and prove that there is one variant that cannot be generated.

Let us consider $I$ with $\text{dom}(I) = f v(\text{predAPP}^*(L))$ such that $I$ is not a model of $\text{predAPP}^*(L)$. Consequently, $I$ is a model of $\text{spec}(L)$ and by Lemma 1, $p = \{o | o \in \mathcal{F} \wedge I(o)\}$ is a product of L. Let us now consider the sequence $d_1, \dots, d_n$ of delta that are applied to generate the variant corresponding to $p$ ($d_1$ being the core of L). For all $\rho \in \mathbb{P}(L)$ we define the following sets:

$$ \begin{align*} S(\text{add}, \rho) &= \{d_i \mid \exists j \le k < l. d_j \in \text{add}(L, \rho) \wedge \forall j < k < l. d_k \notin \text{rem}(L, \rho)\} \\ S(\text{modify}, \rho) &= \{d_i \mid d_i \in \text{rem}(L, \rho) \\ & \wedge \forall 1 \le j < i. \exists j < k < l. d_j \in \text{add}(L, \rho) \wedge d_k \in \bigcup_{\rho' \in \text{prefix}(\rho)} \text{rem}(L, \rho')\} \\ S(\text{remove}, \rho) &= \{d_i \mid d_i \in \text{mod}(L, \rho) \\ & \wedge \forall 1 \le j < i. \exists j < k < l. d_j \in \text{add}(L, \rho) \wedge d_k \in \bigcup_{\rho' \in \text{prefix}(\rho)} \text{rem}(L, \rho')\} \end{align*} $$

From the definition of these sets: if there exist $\rho \in \mathbb{P}(L)$ such that $I$ does not model $\text{predADD}(L, \rho)$, then $S(\text{add}, \rho)$ is not empty; if there exist $\rho \in \mathbb{P}(L)$ such that $I$ does not model $\text{predREM}(L, \rho)$, then $S(\text{remove}, \rho)$ is not empty; and if there exist $\rho \in \mathbb{P}(L)$ such that $I$ does not model $\text{predMOD}(L, \rho)$, then $S(\text{modify}, \rho)$ is not empty; Since $I$ does not model $\text{predAPP}^*(L)$, it does not model $\text{predAPP}(L)$, which implies that the following set is not empty:

$$ S = \bigcup_{\rho \in \mathbb{P}(L)} \bigcup_{op \in \{\text{add,modify,remove}\}} S(op, \rho) $$

Let us consider $i$ minimal with $d_i \in S$: we have that $d_1, \dots, d_{i-1}$ succeeds. Let us moreover consider the first operation in $d_i$, identified by a pair $(op, \rho)$ with $op \in \{\text{add,modify,remove}\}$ and $\rho \in \mathbb{P}(L)$ such that $d_i \in S(op, \rho)$. We have three cases:

1. $op = \text{add}$. By definition of $S(\text{add}, \rho)$, we have that $d_i \in \text{add}(L, \rho)$ and there exists $d_j$ such that $j < i$ and $d_j \in \text{add}(L, \rho)$ and for all $j < k < i$, $d_k \notin \text{rem}(L, \rho)$. This means that the function specification on which $d_i$ is applied does contain $\rho$. Hence, by the Rules 1, 4, 6, and 7 of Fig. 9, $d_i$ fails.

2. $op = \text{remove}$. By definition of $S(\text{remove}, \rho)$, we have that $d_i \in \text{rem}(L, \rho)$ and for all $d_j$ such that $j < i$ and $d_j \in \text{add}(L, \rho)$, there exist $d_k$ with $j < k < i$ and $d_k \in \bigcup_{\rho' \in \text{prefix}(\rho)}$. This means that the function specification on which $d_i$ is applied does not contain $\rho$. Hence, by the Rules 2, 5, 8, and 9 of Fig. 9, $d_i$ fails.

3. $op = \text{modify}$. By definition of $S(\text{modify}, \rho)$, we have that $d_i \in \text{mod}(L, \rho)$ and for all $d_j$ such that $j < i$ and $d_j \in \text{add}(L, \rho)$, there exist $d_k$ with $j < k < i$ and $d_k \in \bigcup_{\rho' \in \text{prefix}(\rho)}$. This means that the function specification on which $d_i$ is applied does not contain $\rho$. Hence, by the third rule of Fig. 9, $d_i$ fails. □
### A.4. Presence constraints

**Lemma 2.** Given a specification SPL L with $\mathcal{F}$ its set of features and a product $p$ of L such that the corresponding variant can be generated, consider the model $I$ of spec(L) corresponding to $p$ with Lemma 1. Then for all $\rho \in \mathcal{P}(L)$, the two following statements are equivalent:

1. $I$ is a model of Pre($L, \rho$).

2. The variant corresponding to $p$ contains $\rho$.

**Proof.** We prove the equivalence by proving each implication independently.

$$ \textbf{Case 1} \Rightarrow 2 $$

Since $I$ is a model of Pre($L, \rho$), there exists $d \in \text{add}(L, \rho)$ with $I(d)$ and for each delta name $d'$ such that $d < d'$ and $d' \in \text{rem}(L, \rho)$, we have $\neg I(d')$. By construction of the sets $\text{add}(L, \rho)$ and $\text{rem}(L, \rho)$, this means that during the variant generation, $\rho$ is added by $d$ and is never removed afterward. Hence $\rho$ is present in the variant.

$$ \textbf{Case 1} \Leftarrow 2 $$

We prove this result by contraposition: we suppose that $I$ is not a model of Pre($L, \rho$) and prove that the variant cannot contain $\rho$. Since $I$ is not a model of Pre($L, \rho$), we have that for all $d \in \text{add}(L, \rho)$ with $I(d)$, there exists $d' \in \text{rem}(L, \rho)$ with $d < d'$ and $I(d')$. By construction of the sets $\text{add}(L, \rho)$ and $\text{rem}(L, \rho)$, this means that during the variant generation, every time a delta $d$ adds $\rho$, the path $\rho$ is removed afterward. Hence $\rho$ is not present in the variant. ☐

**Lemma 3.** Given a specification SPL L with $\mathcal{F}$ its set of features and a product $p$ of L such that the corresponding variant can be generated, consider moreover the model $I$ of spec(L) corresponding to $p$ with Lemma 1. Then for all $f \in \mathcal{P}(L)$ and $v \in \text{fv}(L, f)$, the two following statements are equivalent:

1. $I$ is a model of Pre($L, f, v$).

2. The variant corresponding to $p$ contains the function $f$ and one of the inputs of $f$ contains the variable $v$.

**Proof.** By construction of Pre($L, \rho$), $I$ validates it iff there exists $T \in \text{input}(L, f)$ with $v \in \text{fv}(T)$ and $I \vdash \text{Pre}(f.\text{input}.T)$. By Lemma 2, this is equivalent to $f.\text{input}.T$ being present in the generated variant. By construction of paths, this is equivalent to $f$ being included in the generated variant, and $v$ begin a variable of an input of $f$. ☐

**Lemma 4.** Given a specification SPL L with $\mathcal{F}$ its set of features and a product $p$ of L such that the corresponding variant can be generated, consider moreover the model $I$ of spec(L) corresponding to $p$ with Lemma 1. Then for all $f \in \mathcal{P}(L)$ and $v \in \text{fv}(L, f)$, the two following statements are equivalent:

1. $I$ is a model of Pre($L, f, v$).

2. The variant corresponding to $p$ contains the function $f$ and one of the outputs of $f$ contains the variable $v$.

**Proof.** This proof is similar to that of Lemma 3, replacing input by output. ☐

**Lemma 5.** Given a specification SPL L with $\mathcal{F}$ its set of features and a product $p$ of L such that the corresponding variant can be generated, consider moreover the model $I$ of spec(L) corresponding to $p$ with Lemma 1. Then for all $f \in \mathcal{P}(L)$ and $v \in \text{fv}(L, f)$, the two following statements are equivalent:

1. $I$ is a model of Pre($L, f, v$).

2. The variant corresponding to $p$ contains the function $f$ and one of the outputs of $f$ does not contain the variable $v$.

**Proof.** This proof is similar to that of Lemma 3, replacing input containing $v$ by output not containing $v$. ☐

### A.5. Specification validation: Proofs of Theorems 2 (variable presence), 3 (input variable relevance), and 4 (output variable dependency)

**Theorem 2 (Variable Presence).** Consider an SPL L such that all variants are generable. Moreover, consider the following two properties on L:

1. The constraint $(fm(L) \wedge \text{act}(L)) \Rightarrow \text{decl}(L)$ is valid.

2. All variants of L are such that all their variables are declared.

Then Property 1 is equivalent to Property 2.

**Proof.** Let us first consider that $L$ has no product: by Lemma 1, spec(L) has no model, and so the constraint decl'(L) is valid. Moreover, since $L$ has no product, it also has no variant, and so all of them have their variables declared. Hence, both Properties 1 and 2 are valid statements.

Let us now consider that the product line has at least one product: we prove the equivalence by proving each implication independently.

$$ \textbf{Case 1} \Rightarrow 2 $$

Suppose chosen a specific product $p$ of L: by Lemma 1, there exists exactly one model $I$ of spec(L) such that $p = \{o | o \in \mathcal{F} \wedge I(o)\}$. Because decl'(L) is valid and dom($I$) = $fv(decl'(L))$, $I$ is also a model of decl(L). Let us now consider a variable $v$ used in the variant corresponding to $p$: by definition, there exist in the variant a term $T$ in input or output of a function $f$ that contains $v$. Without loss of generality, let consider that $T$ is an input of $f$: by Lemma 2, we have that $I \vdash \text{Pre}(L, f.\text{input}.T)$. Hence, since $I$ is a model of decl(L), we must have $I \vdash \text{Pre}(L, v')$ for all $v' \in \text{fv}(T)$, including $v$. Consequently, by Lemma 2, we have that $v$ is declared in the variant.

$$ \textbf{Case 1} \Leftarrow 2 $$

We prove this result by contraposition: we suppose that decl'(L) is not valid and prove that there is one variant that does not declare a used variable.

Let us consider $I$ with dom($I$) = $fv(decl'(L))$ such that $I$ is not a model of decl'(L). Consequently, $I$ is a model of spec(L), not a model of decl(L), and by Lemma 1, $p = \{o | o \in \mathcal{F} \wedge I(o)\}$ is a product of L. Since $I$ is not a model of decl(L) there exists $f \in \mathcal{P}(L)$ and either:

* an input $T$ of $f$ and $v \in \text{fv}(T)$ with $I \vdash \text{Pre}(f.\text{input}.T)$ and $I \nvDash v$; or

* an output $T$ of $f$ and $v \in \text{fv}(T)$ with $I \vdash \text{Pre}(f.\text{output}.T)$ and $I \nvDash v$.

In both cases, by Lemma 1, the variant corresponding to $p$ contains a term $T$ with a variable $v$ that is not declared. ☐

**Theorem 3 (Input Variable Relevance).** Consider an SPL L such that all variants are generable. Moreover, consider the following two properties on L:

1. The constraint $(fm(L) \wedge \text{act}(L)) \Rightarrow nFree(L)$ is valid.

2. All variants of L validate Eq. (1) from Section 3.4.2.

Then Property 1 is equivalent to Property 2.

**Proof.** Let us first consider that $L$ has no product: by Lemma 1, spec(L) has no model, and so the constraint nFree'(L) is valid. Moreover, since $L$ has no product, it also has no variant, and so all of them validate Eq. (1). Hence, both Properties 1 and 2 are valid statements.

Let us now consider that the product line has at least one product: we prove the equivalence by proving each implication independently.

$$ \textbf{Case 1} \Rightarrow 2 $$

Suppose chosen a specific product $p$ of L: by Lemma 1, there exists exactly one model $I$ of spec(L) such that $p = \{o | o \in \mathcal{F} \wedge I(o)\}$. Because nFree'(L) is valid and dom($I$) = $fv(nFree'(L))$, $I$ is also a model
of nFree(L). Let us now consider f declared in the variant corresponding to p, and an input term t of f containing a variable v. By Lemma 3, I is a model of PrI(L, f, v), which implies that it is also a model of PrO(L, f, v) ∧ ¬AbsO(L, f, v). By Lemma 4 and 5, this means that there exists an output of f that contains v, and there are no output of f that does not contain that variable.

Case 1 ⇐ 2

We prove this result by contraposition: we suppose that nFree* (L) is not valid and prove that there is one variant that does not validate Eq. (1).

Let us consider *I* with dom(*I*) = *fv(nFree*\*(*L*))\* such that *I* is not a model of *nFree*\*(*L*). Consequently, *I* is a model of spec(*L*), not a model of *nFree*(*L*), and by Lemma 1, *p* = {*o* | *o* ∈ *F* ∧ *I*(*o*)} is a product of *L*. Since *I* is not a model of *nFree*(*L*) there exists *f* ∈ P(*L*) and *v* ∈ *fv*(*L*, *f*) such that *I* is a model of PrI(*L*, *f*, *v*) and at least one of the following statement holds:

* *I* does not model PrO(L, *f*, *v*) which implies by Lemma 4 that no output of *f* contains *v*; or

* *I* models AbsO(L, *f*, *v*) which implies by Lemma 5 that there exists an output of *f* that does not contain *v*. ☐

**Theorem 4 (Output Variable Dependency).** Consider an SPL L such that all variants are generable. Moreover, consider the following two properties on *L*:

1. The constraint ($fv(L) \wedge act(L) \Rightarrow nAmbiguous(L)$) is valid.

2. All variants of *L* validate Eq. (2) from Section 3.4.2.

Then Property 1 is equivalent to Property 2.

**Proof.** Let us first consider that *L* has no product: by Lemma 1, spec(*L*) has no model, and so the constraint *nAmbiguous*\*(*L*) is valid. Moreover, since *L* has no product, it also has no variant, and so all of them validate Eq. (2). Hence, both Property 1 and Property 2 are valid statements.

Let us now consider that the product line has at least one product: we prove the equivalence by proving each implication independently.

Case 1 ⇒ 2

Suppose chosen a specific product *p* of *L*: by Lemma 1, there exists exactly one model *I* of spec(*L*) such that *p* = {*o* | *o* ∈ *F* ∧ *I*(*o*)}. Because *nAmbiguous*\*(*L*) is valid and dom(*I*) = *fv(nAmbiguous*\*(*L*))\*), *I* is also a model of *nAmbiguous*(*L*). Let us now consider *f* declared in the variant corresponding to *p*, and an input term *t* of *f* containing a variable *v*. By Lemma 3, *I* is a model of PrI(*L*, *f*, *v*), which implies that it is also a model of PrO(*L*, *f*, *v*). By Lemma 4, this means that there exists an output of *f* that contains *v*. With a similar approach, we easily prove that all variables in the outputs of *f* are also in its inputs.

Case 1 ⇐ 2

We prove this result by contraposition: we assume *nAmbiguous*\*(*L*) is not valid and prove that there is one variant that does not validate Eq. (2).

Let us consider *I* with dom(*I*) = *fv(nAmbiguous*\*(*L*))\* such that *I* is not a model of *nAmbiguous*\*(*L*). Consequently, *I* is a model of spec(*L*), not a model of *nAmbiguous*(*L*), and by Lemma 1, *p* = {*o* | *o* ∈ *F* ∧ *I*(*o*)} is a product of *L*. Since *I* is not a model of *nAmbiguous*(*L*) there exists *f* ∈ P(*L*) and *v* ∈ *fv*(*L*, *f*) such that *I* models either:

* PrI(L, *f*, *v*) ∧ ¬PrO(L, *f*, *v*): by Lemma 3 and 4, this means that *v* is in an input of *f* but not in any of its outputs; or

* PrO(L, *f*, *v*) ∧ ¬PrI(L, *f*, *v*): by Lemma 3 and 4, this means that *v* is in an output of *f* but not in any of its inputs. ☐

### A.6. Proof of Theorem 5 (terminating specification)

The proof presented in this section is based on one of the main theorems of Arts and Giesl (2000). Hence, before presenting our proof,

we first present an extended version of Definition 8 that introduces a new characterization of order relations. We then recall the concept of dependency pairs, which is the core contribution of Arts and Giesl (2000). Finally, we recall the theorem on which our proof is based.

#### A.6.1. Order relations

**Definition 9 (Preorder, Partial Order, and Well-Founded Partial Order).** Given a set *A*, and a binary relation *R* ⊆ *A* × *A*. *R* is a *preorder* (a.k.a. *quasi-order*) iff it is reflexive and transitive. *R* is a *partial order* iff it is antisymmetric and transitive. Moreover, *R* is a *well-founded order* iff it is a partial order and for all infinite sequence (*a*<sub>i</sub>)<sub>i∈N</sub> there exists *i* ∈ N with (*a*<sub>i</sub>, *a*<sub>i+1</sub>) /∈ *R*.

Finally, given a preorder ≤, we write $\le_i$ the partial order $\{(x, y) \mid (x, y) \in \le \wedge (y, x) \le \le_i\}$.

**Definition 10 (Substitution-Closed Preorder Over a Set of Terms).** Given a set of terms $T = \mathcal{T}(F, V)$, a preorder relation $\le$ over $T$ is weakly *monotonic* iff $s \le t$ implies $f(s_1, \dots, s_i, s, s_{i+1}, \dots, s_n) \le f(s_1, \dots, s_i, t, s_{i+1}, \dots, s_n)$ for all $s_1, \dots, s_n \in T$. Moreover, $\le$ is *closed under substitution* iff for all $(l, r) \in \le$ and all substitution $\sigma$, $(\sigma(l), \sigma(r)) \in \le$.

#### A.6.2. Dependency pairs

**Definition 11 (T-TRS and Terminating T-TRS).** Given a set of terms $T = \mathcal{T}(F, V)$, a T-term rewriting system (T-TRS) is a set $R \subseteq T \times T$ such that for all $(l : s_i, r : s_r) \in R$, $l \notin V$, $fv(r) \subseteq fv(l)$ and $\{(s_i, s_r), (s_r, s_i)\} \cap \emptyset \neq \emptyset$.

A T-TRS *R* is *terminating* there is no infinite sequence of terms $\{(t_i)\}_{i \in \mathbb{N}}$ such that for all $i \in \mathbb{N}$, there exists a subterm $t'_i$ of $t_i$, a substitution $\sigma$ and a rewriting rule $(l, r) \in R$ such that $t'_i = \sigma(l)$ and $t_{i+1} = \sigma(r)$.

**Definition 12 (Dependency Pair of a T-TRS).** Given a set of terms $T = \mathcal{T}(F, V)$ and a term $t = f(t_1, \dots, t_n) \in T \setminus V$, the *root symbol* of $t$, written $\text{root}(t)$ is $f$. Given a T-TRS *R* and writing $F = \{F_a\}_{a \in A}$, the set of *defined symbols* in *R* is the indexed family $F[R] = \{F[R]_a\}_{a \in A}$ with

$$F[R]_a = \{f \mid f \in F_a \wedge \exists(l, r) \in R, f = \text{root}(l)\}$$

For all $a \in A$, we assume a set of fresh symbols $F[R]_a^# = \{f^# \mid f \in F[R]_a\}$, and for all terms $t = f(t_1, \dots, t_n)$ with $f \in F[R]$, we write $t^#$ for the term $f^#(t_1, \dots, t_n)$.

A dependency pair of *R* is a pair $(l^#, r^#)$ such that $(l, r') \in R$ and $r$ is a subterm of $r'$. We write DP(*R*) the set of dependency pairs of *R*.

**Theorem 6 (Arts and Giesl (2000, Theorem 7)).** Given a set of terms $T = \mathcal{T}(F, V)$ and a T-TRS *R*, *R* is terminating iff there exists a weakly *monotonic* preordering $\le$ such that both $\le$ and $\le_I$ are closed under substitution, $\le_I$ is well-founded, and both

* $r \le_I l$ for all rules $(l, r) \in R$; and

* $r \le_I l$ for all dependency pairs $(l, r) \in DP(R)$.

#### A.6.3. Proof of Theorem 5 (terminating specification)

**Lemma 6.** Given a specification SPL *L* with *F* its set of features, and a product *p* of *L* such that the corresponding variant can be generated with all its variables declared. Then the term rewriting system generated from that variant is

$$R = \{(\text{data}(o), \text{data}(o, \text{task}(f, \text{data}(i_1), \dots, \text{data}(i_n))) \mid f \in P(L) \\ \wedge I \vdash \text{Pre}(L, f, \text{output}.o) \wedge \{i_1, \dots, i_n\} = \{r \mid I \vdash \text{Pre}(L, f, \text{input}.r)\} \}$$
with *I* defined by Lemma 1. Moreover, we have

$$DP(R) = \{(\mathit{data}^{\#}(o), \mathit{data}^{\#}(i)) | \\ \exists f \in \mathcal{P}(L), I \vdash \mathit{Pre}(L, f.\mathit{output}.o) \wedge I \vdash \mathit{Pre}(L, f.\mathit{input}.i)\}$$

**Proof.** The first statement is a corollary of Lemma 2. The second one is a direct application of the definition of the dependency pairs. □

**Theorem 5 (Terminating Specification).** Consider an SPL L such that all variants are generable and with all the variables declared. Moreover, consider the following two properties on L:

1. The constraint ($fm(L) \wedge act(L)$) $\Rightarrow$ terminating(L) is valid.

2. Each variant of L results in a terminating TRS.

**Then Property 1 is equivalent to Property 2.**

**Proof.** Let us first consider that *L* has no product: by Lemma 1, spec(L) has no model, and so the constraint terminating*(L) is valid. Moreover, since *L* has no product, it also has no variant, and so all of them result in a terminating TRS. Hence, both Properties 1 and 2 are valid statements.

Let us now consider that the product line has at least one product: we prove the equivalence by proving each implication independently.

**Case 1** $\Rightarrow$ 2

Suppose chosen a specific product *p* of *L*: by Lemma 1, there exists exactly one model *I* of spec(L) such that $p = \{o | o \in \mathcal{F} \wedge I(o)\}$. Because terminating*(L) is valid and dom(*I*) = $fv(terminating*(L))$, *I* is also a model of terminating(L). Hence, there exist a partial order < on terms that is well-founded, weakly monotonic, closed under substitution and such that for all $f \in \mathcal{P}(L)$, all $t \in output(L, f)$ with $I \vdash Pre(L, f. output.t)$, and all $t' \in input(L, f)$ with $I \vdash Pre(L, f. input.t')$, we have $t' < t$. Since the *S*-sorted signature *F* is dataflow-safe, < contains no terms with data or task symbols. Let us define $\equiv$ being the transitive, reflexive closure of *R* that is closed under substitution. We moreover define the partial order $\prec$ as follows:

$$\prec = \prec \cup \{(\mathit{data}(l), \mathit{data}(r)) | (l, r) \in \prec\} \cup \{(\mathit{data}^{\#}(l), \mathit{data}^{\#}(r)) | (l, r) \in \prec\}$$

Let $\leq = \prec \cup \equiv$. By construction of *R*, it is a preorder and $t \leq = \prec$.

With Lemma 6, is thus clear that $\leq$ validates Theorem 6.

**Case 1** $\Leftarrow$ 2

Suppose chosen a specific product *p* of *L*: by Lemma 1, there exists exactly one model *I* of spec(L) such that $p = \{o | o \in \mathcal{F} \wedge I(o)\}$. Since the TRS *R* resulting of the variant corresponding to *p* terminates, we can consider the preorder $\leq$ given by Theorem 6. Let us recall that $\leq = \prec$ is a partial order on DP(*R*) that is well founded, weakly monotonic, and closed under substitution. Hence the following relation $<$ is also founded, weakly monotonic, and closed under substitution:

$$\prec = \prec \cup \{(l, r) | (\mathit{data}^{\#}(l), \mathit{data}^{\#}(r)) \in \prec\}$$

By Lemma 6, we thus have that $<$ is such that for all $f \in \mathcal{P}(L)$, all $t \in output(L, f)$ with $I \vdash Pre(L, f. output.t)$, and all $t' \in input(L, f)$ with $I \vdash Pre(L, f. input.t')$, we have $t' < t$. □

## References

Alves, S., Broda, S., 2018. A unifying framework for type inhabitation. In: Kirchner, H. (Ed.), Proceedings of the 3rd International Conference on Formal Structures for Computation and Deduction. FSCD'18, In: LIPIcs, vol. 108, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, pp. 5:1–5:16. http://dx.doi.org/10.4230/LIPIcs.FSCD.2018.5.

Anderson, W.K., Biedron, R.T., Carlson, J.-R., Derlaga, J.M., Druyor Jr., C.T., Gnoffo, P.A., Hammond, D.P., Jacobson, K.E., Jones, W.T., Kleb, B., Lee-Rausch, E.M., Nastac, G.C., Nielsen, E.J., Park, M.A., Rumsey, C.L., Thomas, J.L., Thompson, K.B., Walden, A.C., Wang, L., Wood, S.L., Wood, W.A., Diskin, B.,

Liu, Y., Zhang, X., 2023. FUN3D Manual: 14.0. 1. Tech. Rep. NASA/TM-20230004211, NASA, URL https://fun3d.larc.nasa.gov/papers/FUN3D_INTG_Manual-14.0.1.pdf.

Apel, S., Batory, D.S., Kästner, C., Saake, G., 2013. Feature-Oriented Software Product Lines: Concepts and Implementation. Springer, http://dx.doi.org/10.1007/978-3-642-37521-7.

Arts, T., Giesl, J., 2000. Termination of term rewriting using dependency pairs. Theoret. Comput. Sci. 236 (1), 133–178. http://dx.doi.org/10.1016/S0304-3975(99)00207-8.

Augonnet, C., Thibault, S., Namyst, R., Wacrenier, P.-A., 2011. StarPU: A unified platform for task scheduling on heterogeneous multicore architectures. Concur. Comput.: Pract. Exper. 23 (2), 187–198. http://dx.doi.org/10.1002/cpe.1631.

Bauer, M.E., 2014. Legion: Programming Distributed Heterogeneous Architectures with Logical Regions (Ph.D. thesis). Stanford University.

Ben-Nun, T., de Fine Licht, J., Ziogas, A.N., Schneider, T., Hoefler, T., 2019. Stateful dataflow multigraphs: A data-centric model for performance portability on heterogeneous architectures. In: Proceedings of the International Conference for High Performance Computing, Networking, Storage and Analysis. SC’19, ACM, pp. 81:1–81:14. http://dx.doi.org/10.1145/3295500.3356173.

Bettini, L., Damiani, F., Schaefer, I., 2013. Compositional type checking of delta-oriented software product lines. Acta Inform. 50 (2), 77–122. http://dx.doi.org/10.1007/s00236-012-0173-z.

Cambier, L., Heib, S., Plot, S., 2013. The Onera elsA CFD software: Input from research and feedback from industry. Mech. Ind. 14 (3), 159–174. http://dx.doi.org/10.1051/meca/2013056.

Chakraborty, S., Fremont, D.J., Meel, K.S., Seshia, S.A., Vardi, M.Y., 2015. On parallel scalable uniform SAT witness generation. In: Baier, C., Tinelli, C. (Eds.), Proceedings of the 21st International Conference on Tools and Algorithms for the Construction and Analysis of Systems. TACAS’15, In: LNCS, vol. 9035, Springer, pp. 304–319. http://dx.doi.org/10.1007/978-3-662-46681-0_25.

Chamberlain, B.L., Callahan, D., Zima, H.P., 2007. Parallel programmability and the Chapel language. Int. J. High Perform. Comput. Appl. 21 (3), 291–312. http://dx.doi.org/10.1177/1094342007078442.

Classen, A., Cordy, M., Schöbbens, P., Heymans, P., Legay, A., Raskin, J., 2013. Featured transition systems: Foundations for verifying variability-intensive systems and their application to LTL model checking. IEEE Trans. Softw. Eng. 39 (8), 1069–1089. http://dx.doi.org/10.1109/TSE.2012.86.

Clavel, M., Durán, F., Eker, S., Lincoln, P., Martí-Oliet, N., Meseguer, J., Talcott, C. (Eds.), 2007. All about maude — A high-performance logical framework: How to specify, program and verify systems in rewriting logic. LNCS, vol. 4350, Springer, http://dx.doi.org/10.1007/978-3-540-71999-1.

Damiani, F., Lienhardt, M., 2016. On Type Checking Delta-Oriented product lines. In: Ábrahám, E., Huisman, M. (Eds.), Proceedings of the 12th International Conference on Integrated Formal Methods. IFM’16, In: LNCS, vol. 9681, Springer, pp. 47–62. http://dx.doi.org/10.1007/978-3-319-33693-0_4.

Damiani, F., Lienhardt, M., Maugars, B., Michel, B., 2022. Towards a modular and variability-aware aerodynamic simulator. In: Ahrendt, W., Beckert, B., Bubel, R., Johnsen, E.B. (Eds.), The Logic of Software: A Tasting Menu of Formal Methods. In: LNCS, vol. 13360, Springer, pp. 147–172. http://dx.doi.org/10.1007/978-3-031-08166-8_8.

Dudenhefner, A., Rehof, J., 2017. The complexity of principal inhabitation. In: Miller, D. (Ed.), Proceedings of the 2nd International Conference on Formal Structures for Computation and Deduction. FSCD’17, In: LIPIcs, vol. 84, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, pp. 15:1–15:14. http://dx.doi.org/10.4230/LIPIcs.FSCD.2017.15.

Garavel, H., Tabikh, M., Arrada, I., 2018. Benchmarking implementations of term rewriting and pattern matching in algebraic, functional, and object-oriented languages: The 4th rewrite engines competition. In: Rusu, V. (Ed.), Proceedings of the 12th International Workshop on Rewriting Logic and Its Applications. WRLA’18, In: LNCS, vol. 11152, Springer, pp. 1–25. http://dx.doi.org/10.1007/978-3-319-99840-1.

Gvero, T., Kuncak, V., Kuraj, I., Piskac, R., 2013. Complete completion using types and weights. In: Proceedings of the 34th ACM SIGPLAN Conference on Programming Language Design and Implementation. PLDI’13, ACM, pp. 27–38. http://dx.doi.org/10.1145/2491956.2462192.

Hirokawa, N., Middeldorp, A., 2004. Polynomial interpretations with negative coefficients. In: Buchberger, B., Campbell, J.A. (Eds.), Proceedings of the 7th International Conference on Artificial Intelligence and Symbolic Computation. AISC’04, In: LNCS, vol. 3249, Springer, pp. 185–198. http://dx.doi.org/10.1007/978-3-540-30210-0_16.

Kaiser, H., Heller, T., Adelstein-Lelbach, B., Serio, A., Fey, D., 2014. HPX — A task based programming model in a global address space. In: Proceedings of the 8th International Conference on Partitioned Global Address Space Programming Models. PGAS’14, ACM, pp. 6:1–6:11. http://dx.doi.org/10.1145/2676870.2676883.

Kale, L.V., Krishnan, S., 1993. CHARM++: A portable concurrent object oriented system based on C++. In: Proceedings of the 8th Annual Conference on Object-Oriented Programming Systems, Languages, and Applications. OOPSL’93, ACM, pp. 91–108. http://dx.doi.org/10.1145/165854.165874.

Kavi, K.M., Deshpande, A.K., 1991. Specification of concurrent processes using a dataflow model of computation and partially ordered events. J. Syst. Softw. 16 (2), 107–120. http://dx.doi.org/10.1016/0164-1212(91)90004-P.
Lienhardt, M., 2023. PYDOP: A generic Python library for delta-oriented programming. In: Proceedings of the 27th ACM International Systems and Software Product Line Conference, Vol. B. SPLC'23, ACM, pp. 30–33. http://dx.doi.org/10.1145/3579028.3609011.

Lienhardt, M., Clarke, D., 2012. Conflict detection in delta-oriented programming. In: Margaria, T., Steffen, B. (Eds.), Proceedings of the 5th International Symposium on Leveraging Applications of Formal Methods, Verification and Validation: Technologies for Mastering Change. ISoLA'12, In: LNCS, vol. 7609, Springer, pp. 178–192. http://dx.doi.org/10.1007/978-3-642-34026-0_14.

Lienhardt, M., Damiani, F., Testa, L., Turin, G., 2018. On checking delta-oriented product lines of statecharts. Sci. Comput. Program. 166, 3–34. http://dx.doi.org/10.1016/j.scico.2018.05.007.

Meinicke, J., Thüm, T., Schröter, R., Benduhn, F., Leich, T., Saake, G., 2017. Mastering Software Variability with FeatureIDE. Springer, http://dx.doi.org/10.1007/978-3-319-61443-4.

Oh, J., Gazzillo, P., Batory, D., Heule, M., Myers, M., 2020. Scalable uniform sampling for real-world software product lines. URL https://api.semanticscholar.org/CorpusID:219699491.

Rausch, O., Ben-Nun, T., Dryden, N., Ivanov, A., Li, S., Hoefler, T., 2022. A Data-centric optimization framework for machine learning. In: Proceedings of the International Conference on Supercomputing. ICS'22, ACM, pp. 36:1–36:13. http://dx.doi.org/10.1145/3524059.3532364.

Roumage, G., Azaiez, S., Louise, S., 2022. A survey of main dataflow MoCCs for CPS design and verification. In: Proceedings of the 15th International Symposium on Embedded Multicore/Many-Core Systems-on-Chip. MCSoC'22, IEEE, pp. 1–9. http://dx.doi.org/10.1109/MCSoC57363.2022.00010.

Schaefer, I., Bettini, L., Bono, V., Damiani, F., Tanzarella, N., 2010. Delta-oriented programming of software product lines. In: Bosch, J., Lee, J. (Eds.), Proceedings of the 14th International Conference on Software Product Lines: Going Beyond. SPLC'10, In: LNCS, vol. 6287, Springer, pp. 77–91. http://dx.doi.org/10.1007/978-3-642-15579-6_6.

Schaefer, I., Rabiser, R., Clarke, D., Bettini, L., Benavides, D., Botterweck, G., Pathak, A., Trujillo, S., Villela, K., 2012. Software diversity: State of the art and perspectives. Int. J. Softw. Tools Technol. Transf. 14 (5), 477–495. http://dx.doi.org/10.1007/s10009-012-0253-y.

Soos, M., Gocht, S., Meel, K.S., 2020. Tinted, detached, and lazy CNF-XOR solving and its applications to counting and sampling. In: Lahiri, S.K., Wang, C. (Eds.), Proceedings of the 32nd International Conference on Computer Aided Verification. CAV'20, In: LNCS, vol. 12224, Springer, pp. 463–484. http://dx.doi.org/10.1007/978-3-030-53288-8_22.

ter Beek, M.H., Damiani, F., Lienhardt, M., Mazzanti, F., Paolini, L., 2019. Static analysis of featured transition systems. In: Proceedings of the 23rd International Systems and Software Product Line Conference. SPLC'19, ACM, pp. 39–51. http://dx.doi.org/10.1145/3336294.3336295.

ter Beek, M.H., Damiani, F., Lienhardt, M., Mazzanti, F., Paolini, L., 2022. Efficient static analysis and verification of featured transition systems. Empir. Softw. Eng. 22 (1), 10:1–10:43. http://dx.doi.org/10.1007/s10664-020-09930-8.

Thüm, T., Apel, S., Kästner, C., Schaefer, I., Saake, G., 2014. A classification and survey of analysis strategies for software product lines. ACM Comput. Surv. 47 (1), 6:1–6:45. http://dx.doi.org/10.1145/2580950.

Urzyczyn, P., 1997. Inhabitation in typed Lambda-Calculi (A Syntactic Approach). In: de Groote, P. (Ed.), Proceedings of the 3rd International Conference on Typed Lambda Calculi and Applications. TLCA'97, In: LNCS, vol. 1210, Springer, pp. 373–389. http://dx.doi.org/10.1007/3-540-62688-3_47.

Yamada, A., 2022. Tuple interpretations for termination of term rewriting. J. Autom. Reason. 66 (4), 667–688. http://dx.doi.org/10.1007/s10817-022-09640-4.