1. INTRODUCTION
The design and configuration of software and hardware systems has a long tradition as a key discipline in computer science and artificial intelligence (AI). A configuration (task) is “characterized through a set of components, a description of their properties, namely attributes and possible attribute values, connection points (ports), and constraints on legal configurations” (Felfernig et al., Reference Felfernig, Friedrich and Jannach2000, p. 450). The Alliance for Telecommunications Industry Solutions (2000) defines configuration as the arrangement of functional units according to their nature, number, and chief characteristics where functional units may encompass any form of component (e.g., integrated circuits, software programs, or building parts in a car). A configuration task means the process of setting up admissible arrangements under certain criteria of optimality (e.g., minimal number of components or preferences when connecting components).
Important criteria for the solution of a configuration task are the computation of the components to be included in the solution, the type of information on each of these components, the way the components are connected, and the values for the attributes of each component (Mailharro, Reference Mailharro1998).
Existing methods and results in AI tackle a broad spectrum of applications. However, especially in an engineering context we are faced with unique challenges. The complexity and size of real-world systems is steadily increasing (e.g., the number of transistors in recent multicore processors or the number of product configurations in the automotive sector). As a consequence, there is a big demand for efficient techniques in configuration that scale well with large systems consisting of tens of thousands of components and even more interactions among them.
Tool support for assisting the engineer in designing such large systems is fundamental as manual handling and inspection becomes inherently complex. Moreover, the engineer has to deal with a diverse set of configuration tasks: checking the consistency of component systems, reasoning over system properties, finding minimal models, repairing inconsistent configurations due to modifications in the original design, or finding a viable layout for components under physical constraints. Numerous additional constraints like subclassing or equational constraints on links between components might occur depending on the modeled scenario.
Proper handling of such tasks requires rigorous techniques, known as formal methods in computer science. Unfortunately, a main drawback of powerful formal methods is the so-called knowledge acquisition bottleneck because the design engineer must have a substantial mathematical background for understanding and applying a formal methodology correctly. Another drawback of such machinery is their high computational complexity (Stumptner, Reference Stumptner, Friedrich and Haselböck1998; Falkner et al., Reference Falkner, Haselböck, Schenner and Schreiner2011) on larger use cases.
Consequently, lightweight formal methods have been proposed (Jackson & Wing, Reference Jackson and Wing1996) to ease the implementation of formal techniques in real-world systems, to tackle the knowledge acquisition bottleneck, and to allow reasoning in a (semi)automatic way. Lightweight formal methods are characterized by “partiality and focused application” (Jackson & Wing, Reference Jackson and Wing1996). That means full formalization of complete systems with all properties is not tractable owing to the expressiveness of employed formalisms and their inherent complexity. Instead, we should focus on relevant properties and employ efficient methods to check them. In the end, the success of formal methods (lightweight or not) will also depend on whether the engineer is comfortable with using them in his design environment.
The Unified Modeling Language (UML; Object Management Group, 2011) is one of the most prominent modeling frameworks, and it has also been increasingly used for the design of component systems for configuration (Felfernig et al., Reference Felfernig, Friedrich and Jannach2000, Reference Felfernig, Friedrich, Jannach and Zanker2002, Reference Felfernig, Friedrich, Jannach, Stumptner and Zanker2003; Falkner et al., Reference Falkner, Feinerer, Salzer and Schenner2010). A range of techniques for formal reasoning on UML diagrams exists; however, basically all of them are computationally quite expensive because they use expressive formalisms (like first-order logic) for capturing the intended semantics of UML. This is especially relevant when dealing with numerical constraints that are very common in configuration (e.g., relating the number of components that are allowed to interact with each other).
Following the spirit of lightweight formal methods and combining them with widely used modeling frameworks like UML, we therefore recently proposed to use integer linear programming (ILP) by translating the most basic constructs (classes, associations, and multiplicities) of UML class diagrams to Diophantine inequalities (Feinerer, Reference Feinerer2007; Feinerer & Salzer, Reference Feinerer and Salzer2007), that is, inequalities over variables with integer domain. Although addressing important basic aspects, several open issues have been identified that are highly relevant in real-world configuration applications (Falkner et al., Reference Falkner, Feinerer, Salzer and Schenner2010) but are not yet fully dealt with, including subclassing, partial configurations, and immediate feedback.
Thus, our primary objectives are lightweight formal methods for solving a configuration task supporting the full range of language elements necessary for modeling real-world applications, which are highly efficient and which scale well with large systems in the hardware and software domains. To achieve these goals, the main contributions of this paper are a unified theory using ILP principles that allows us to model real-world configuration scenarios and constraints and an experiment consisting of two large-scale applications with benchmarks to show the applicability of our approach. We see our approach as a further step toward exploring tractable cases in configuration (in contrast to the NP-hardness of configuration in general) and providing intuitive interfaces toward achieving this goal.
Solving an ILP corresponds to checking the consistency of a configuration (i.e., can the system of inequalities be solved at all) and to finding optimized models (because we will minimize a corresponding objective function). Partial configurations can be used as initial solutions in an ILP (the number of existing components corresponds to the variable values in the ILP), and immediate feedback is possible because the variables in the solution of the ILP correspond to components in a configuration. Note that we ignore attributes of components in our approach. Connecting the components computed by the ILP is not covered in this paper; however, an algorithm based on uniform distribution of links by Feinerer (Reference Feinerer2007) can be used for generating a topology (i.e., how components are linked) from an ILP solution.
Because the generation of an ILP is automatic for the main constructs of a given UML class diagram, we are able to provide an intuitive interface. UML class diagrams can be easily created and maintained with any standard compliant diagram editor. Customized plug-ins and tools can directly display inconsistencies detected by our underlying ILP methods. This gives us a visual representation that is easy to use and interpret for a broad range of users owing to UML standard compliance. Nonetheless, we have an exact syntax and semantics for formal reasoning under the hood by restricting the allowed language elements to a well-defined subset of UML class diagrams.
The two applications presented in this paper are configuration tasks in the context of package management for the Debian GNU/Linux operating system and for the Linux kernel. Both applications were chosen because their sources are publicly available, which allows for better reproducible research (compared to many examples that are limited in distribution because they come from an industrial setting with restrictive permissions); are large scale with thousands of components; and are of interest to a broad audience (e.g., package management is a core task in every Debian GNU/Linux installation worldwide).
The remainder of this paper is structured as follows. Section 2 demonstrates how central concepts necessary for configuration can be modeled with UML class diagrams or similar modeling frameworks. Section 3 shows how to translate such diagrams to an integer linear program and how to encode concept hierarchies, multiple links, and conflicts as linear constraints. This forms a unified theory that can be solved with any ILP solver. Section 4 describes both application settings and how they are modeled in our framework, and Section 5 shows a benchmark experiment and evaluates our ILP approach for both applications. Section 6 puts our work in context with related work, and Section 7 presents our conclusions.
2. MODELING SYSTEMS FOR CONFIGURATION
Before configuring technical systems, an engineer needs to have an exact specification of its underlying structure. The main work consists of specifying functional units and components and their interrelationships. Numerous additional constraints can be added once the fundamental interactions are clear. Modeling entities and their relationships has a long history in computer science, with entity relationship (Chen, Reference Chen1976) diagrams and UML (Object Management Group, 2011) diagrams as the most commonly used formalisms nowadays. Because of their widespread use over the last decades and the availability of a multitude of (both commercial and open source) modeling tools, most engineers are familiar with such frameworks. Using such a formalism is therefore a natural and conservative starting point when modeling systems of interest as the basis for configuration (Felfernig et al., Reference Felfernig, Friedrich and Jannach2000).
2.1. General case
Consider the example depicted in Figure 1. It models two components, C and D. Each component C must have between between m 1 and m 2 partners of type D, and each component D must have between n 1 and n 2 partners of type C in turn. In UML terminology, C and D are classes, the relationship between them is denoted as an association, and the numerical intervals constraining the association are called multiplicities or cardinalities.
Two classes, C and D, a binary association between them, and multiplicities restricting the number of allowed links.
Such a diagram already captures our intuition about the desired semantics. However, there are several hidden intricacies.
2.2. Lower bound constraints
Without additional constraints, any formal reasoner will refrain from instantiating any objects at all when searching for minimal models. This is because UML diagrams do not implicitly enforce the existence of individual objects. This can be easily fixed with a constraint stating there needs to be at least one C object, for example, expressed in the Object Constraint Language (OCL; Object Management Group, 2012):
$$\hbox{context C inv\colon \;C.allInstances\lpar \rpar }- \gt \hbox{size\lpar \rpar }\gt 0.$$2.3. Multiple links
Next, it makes a difference whether we allow multiple links between the same objects or not. In some cases it is desirable, like multiple redundant network cables between two switches, whereas often it is not and an indication of a design error. UML allows us to change this behavior via the multiplicity attribute “(non)unique.” The default is unique, which forbids (or ignores) multiple links between the same objects, and we stay with this convention when not otherwise explicitly stated.
When mixing unique and nonunique on the same association, there are subtleties with the semantics of a valid instance of the UML class diagram. Consider Figure 1 and assume that n 1 = 1, n 2 = 2, m 1 = 3, and m 2 = 4 and that the end of the association near D is marked as nonunique. Then Figure 2 shows a valid instance with only two D objects (note that m 1 = 3). This is because c 1 has three different links to objects of class D and is not necessarily connected with three different objects, corresponding to the nonunique attribute. Consequently, we recommend avoiding mixed associations unless the designer is aware of the underlying semantics of such constructs. Instead, associations with symmetric attributes (i.e., either unique or nonunique on all association ends) can be used to model a broad class of constructs.
A valid instance of Figure 1 for n 1 = 1, n 2 = 2, m 1 = 3, m 2 = 4, when the end of the association near D is marked as nonunique.
Besides the basics of managing functional units and their relationships, several additional features are necessary to allow an engineer to model realistic systems for configuration, like handling mutually exclusive components or conflict handling.
2.4. Subclassing
Subclassing relates similar components in a hierarchy, typically with a single superclass and multiple inherited subclasses. When modeling component systems, subclassing is primarily used to express disjunction in either the normal (logical or) or the exclusive (logical xor) form.
Consider Figure 3, which depicts the situation that two (sub)classes, C 1 and C 2, share a common structure and are thus related to the common superclass C via a generalization in UML. The idea behind this construct is that either C 1 or C 2 can be used when somebody asks for a component of type C. If it is allowed that both C 1 and C 2 are instantiated at the same time, we can use the diagram as is. Otherwise, the additional UML constraint {xor} needs to be added (in the form of a dashed line between the associations connecting C 1 with C and C 2 with C).
Generalization with superclass C and two subclasses, C 1 and C 2.
2.5. Conflicts
Similarly to the constraint that only one out of multiple components can be chosen, some may be incompatible with others. For example, in an automotive scenario, we may not be allowed to mix tires of different types for safety reasons, or installing two different software libraries providing an overlapping set of files may destroy a working operating system setup.
A possible way to encode such a constraint is depicted in Figure 4. The key feature is the 0..0 multiplicity that states that each C object must have 0 links to objects of class D. This directly corresponds to incompatibility. Alternatively, separate constraints outside of the UML diagram may be used to avoid a blow up in the diagram if many incompatible cases are relevant to an application. For example, the OCL constraint
$$\eqalign{\hbox{context C inv\colon \;C.allInstances\lpar \rpar }- \gt \hbox{size\lpar \rpar } \gt 0 \cr \hbox{implies D.allInstances\lpar \rpar }- \gt \hbox{size\lpar \rpar } =0}$$states that once there is at least one object of type C, then no object of type D is allowed to be instantiated.
A binary association modeling a conflict between the two classes, C and D, via a 0..0 multiplicity.
3. ILP
In the previous section, we identified central concepts in configuration and how they can be modeled in an entity relationship inspired framework like UML. Now we will translate all constructs to linear inequalities forming a unified ILP theory. The semantics induced by the translation is compliant with the UML specification if not explicitly stated otherwise.
Our idea is based on some initial work by Lenzerini and Nobili (Reference Lenzerini and Nobili1990) and extensions by Feinerer and Salzer (Reference Feinerer and Salzer2007) that translate a binary association to two linear inequalities adhering to the multiplicity constraints.
3.1. General case
A binary association as exemplified in Figure 1 is mapped to
$$\eqalign{&m_1\times \vert C \vert \le n_2 \times \vert D \vert\comma \; \cr &n_1 \times \vert D \vert \le m_2 \times \vert C \vert\comma \;}$$where |C| and |D| denote the number of C and D objects, respectively. The main observation for correctness of the above translation is that the number of links, l, between the two classes, C and D, is bounded by
$$\eqalign{&m_1 \times \vert C \vert \le l \le m_2 \times \vert C \vert\comma \; \cr &n_1 \times \vert D \vert \le l \le n_2 \times \vert D \vert.}$$Combining these two inequalities results in the above translation.
3.2. Lower bound constraints
Enforcing that individual classes get instantiated at all enforces us to use lower bound constraints. For example, for Figure 1, a valid solution is |C| = 0 and |D| = 0 because all constraints are satisfied (which is easily verified by inserting |C| = |D| = 0 in the inequalities from the previous paragraph). However, normally this is not the desired semantics. Instead, we want to enforce that there is a least one component of type C that maps to the following simple ILP constraint
$$\vert C \vert \ge 1.$$3.3. Multiple links
Inequalities from the general case hold in the presence of the nonunique UML attribute because their correctness relies on an argumentation of involved links. To ensure uniqueness among objects, we need additional constraints stating that links must end with mutually different partner objects. In Figure 1 the association has no explicit attribute markers and thus defaults to unique on both association ends. We obtain
$$\eqalign{&\vert C \vert \gt 0 \rightarrow \vert D \vert \ge m_1\comma \; \cr &\vert D \vert \gt 0 \rightarrow \vert C \vert \ge n_1.}$$This ensures that if at least one C or D object gets instantiated, there are enough different (i.e., m 1 and n 1) D and C objects available for linking. Note that there is an implication involved in these formula that at first glance is not compatible with standard ILP. However, in our case, we can easily remedy this by solving our ILP and checking the preconditions afterward. Because all preconditions are of the form |X| > 0, this can be instantly checked from the ILP solution, and a new (augmented by the right-hand sides of above formulas) ILP is started with the old solution as its initial starting value. Because the inequalities presented so far form a solution space that can be monotonically processed by increasing variable values, this trick works without backtracking. As a result, the compound running time of the old and new ILP linearly corresponds to an ILP where it is known in advance whether the preconditions fire or not.
The inequalities presented so far can be efficiently solved by mapping them to a directed weighted graph. The variables form its nodes, and each inequality relating two variables induces an edge with a weight proportional to the coefficients of the variables. Over such a weighted directed graph a variant of the Floyd-Warshall (Floyd, Reference Floyd1962) algorithm can be used to compute all shortest paths in the polynomial time of O(V 3), where V stands for the total number of variables of all inequalities. These paths can be used for obtaining rational solutions that in turn can easily be translated into a (not necessarily minimal) integer solution. Note that this is not in contrast to the general NP-hardness of ILP. The reason is that we have no constraints of the form m × |C| + n × |D| ≤ k (with m, n, and k as positive integers) yet in our formulation. Note that the same strategy of building a graph also works for n-ary associations as long as all n ends of the association have the same uniqueness attribute.
Alternatively, any standard ILP solver can be used to obtain the minimal integer solution directly.
3.4. Subclassing
When modeling a generalization as depicted in Figure 3, we first have to decide on the semantics when there is a connection from C to another class, D. One interpretation is that C is a placeholder and D is connected to either C 1 or C 2. This means that C does not get instantiated at all (and as such |C| = 0). Alternatively, D can connect to C, and C is connected to either C 1 or C 2. Without loss of generality, we stick with the latter convention because we prefer to model associations explicitly (e.g., between D and C 1 with a separate association if there is a direct correspondence between them without using the generalization). The superclass C can be seen as a virtual coordinator that might ease the actual linking of components considerably. Superclasses can also easily be discarded if there is no need for them in the final solution (e.g., in the hardware domain where only subclasses are likely to be instantiated).
We observe the property that in Figure 3 each C can have zero or one C 1 partner objects, but a single C 1 (if it exists) must have exactly a single distinct C object. The same argument holds for C with C 2. The property is formalized to
$$\eqalign{&0 \times \vert C \vert \le 1 \times \vert C_1 \vert\comma \; \cr &1 \times \vert C_1 \vert \le 1 \times \vert C \vert \comma \; \cr &0\times \vert C \vert \le 1 \times \vert C_2 \vert\comma \; \cr &1 \times \vert C_2 \vert \le 1 \times \vert C \vert\comma \;}$$which simplifies to
$$\vert C_i \vert \le \vert C \vert\comma \;$$for i = 1, 2. This directly corresponds to our intuition that we need at least as many C coordinator objects such that there are no “useless” C 1 or C 2 objects that do not take part in the generalization.
Note that the sharing of a single C object by both an object of class C 1 and an object of class C 2 is allowed. This property models nondisjoint classification of individuals within a conceptual hierarchy, like a disjunction in classical propositional logic.
Thus far we have only ensured that there are enough “coordinators” of class C. This does not suffice because we have to provide enough subclasses (either C 1 or C 2) that can be used in the generalization for the superclass C. The following constraint models (summing up over all C i and C objects) that we can use C 1, C 2, or both together as a subclass for C:
$$\vert C_1 \vert + \vert C_2 \vert \ge \vert C \vert.$$If we restrict the setting to exclusive or ({xor} in UML terminology), then either C 1 or C 2 must exactly match with a single C. Consequently, we obtain
$$\vert C_1 \vert + \vert C_2 \vert = \vert C \vert\comma \;$$stating that we need enough C i for matching C objects but not more. This forbids object sharing and thus models disjunction in exclusive form.
We can easily generalize this setting to multiple subclasses C i with i > 2 by considering the additional objects in the sums on the left-hand sides of the above (in)equalities.
3.5. Conflicts
If we model conflicts as outlined in Figure 4 and translate this directly via our standard approach, we obtain
$$\eqalign{&0 \times \vert C \vert \le n_2 \times \vert D \vert\comma \; \cr &n_1\times \vert D \vert \le 0 \times \vert C \vert.}$$The first inequality is a tautology because we only allow nonnegative multiplicities (i.e., n 2 ≥ 0) and nonnegative numbers of classes (|D| ≥ 0), which thus can be removed without side effects.
The second inequality forbids any D object if n 1 > 0. This is semantically correct because when n 1 = 0 then there are isolated D objects allowed that need not be related to C objects at all. For the more typical case when a D object must a have connection to a C object (i.e., n 1 > 0), then instantiating a D object would mean we also need a C object. This in turn would violate our initial constraint that a C object must not be linked to a D object.
A subtle modification of the desired semantics could be that we want to allow D objects without connection to C objects, but as soon as there exists a single C object, we forbid Ds at all. This models a situation where we want to use parts of category C or D throughout our whole configuration but never allow them to occur together. Such a constraint can be expressed via
$$\vert C \vert \gt 0 \rightarrow \vert D \vert =0.$$To avoid the implication, we might be tempted to use
$$\vert C \vert \times \vert D \vert =0\comma \;$$which enforces that once we use parts of one category no objects of the other class are allowed. Unfortunately, this is a nonlinear constraint that we will not use because we restrict our theory to linear integer programming for performance reasons.
Fortunately, we know that C is only included in a minimal solution if absolutely necessary (as otherwise minimality is violated). The same argument holds for D. Consequently, we know that a solution containing both C and D is invalid and can be instantly rejected. This observation allows us to handle the implication efficiently, with a similar argument as when dealing with the UML “unique” attribute for multiple links.
4. APPLICATIONS
This section describes two applications: one in the context of Debian package management and configuration and one in the Linux kernel configuration.
4.1. Debian package configuration
The Debian GNU/Linux operating system (http://www.debian.org) is one of the most prominent free and open source distributions in the Linux ecosystem. With its more than 29,000 packages, it provides a vast amount of available software out of the box that allows the user to set up individually customized package collections or even new distributions like Ubuntu (http://www.ubuntu.com). The variability (i.e., the number of possible combinations of interacting packages) is very high, and consequently a sophisticated packaging system (like the Advanced Packaging Tool available at http://packages.qa.debian.org/a/apt.html) managing all packages and their interdependencies in an installation is necessary.
Each Debian package typically has metadata providing the following information:
• Package: a unique name of the package.
• Version: a unique string identifying the version.
• Depends: a list of packages that must be installed for proper functionality. Alternatives are allowed such that, for example, only one of multiple packages must be installed providing some core functions.
• Conflicts: a list of packages that must not be installed at the same time.
• Description: a short (up to several lines) text description of the package and its main functionality.
The following excerpt shows an example for the Debian package emacs23-nox (Emacs without support for graphical environments), listing the individual metadata entries:
Package: emacs23-nox
Version: 23.3+1–1
Depends: emacs23-bin-common (= 23.3+1–1), libasound2 (> 1.0.18), libc6 (>= 2.3.6–6~), libdbus-1–3 (>= 1.1.1), libgpm2 (>= 1.20.4), libncurses5 (>= 5.5–5~)
Suggests: emacs23-common-non-dfsg
Conflicts: emacs23, emacs23-gtk, emacs23-lucid
Description: The GNU Emacs editor (without X support) GNU Emacs is the extensible self-documenting text editor. This package contains a version of Emacs compiled without support for X.
4.1.1. ILP formulation
Given a Debian package, we extract its metadata and generate an integer linear program modeling the interrelationships between packages as outlined in the metadata:
• Package is mapped to a variable in the ILP and corresponds to a class in our UML representation. If and only if the package is part of the input specification by the user, we enforce a lower bound of 1 (assuming we consider package C at the moment):
$$\vert C \vert \ge 1.$$In addition, we disallow multiple installation of the same package with the same version. That is, we need a Boolean range, either the package is installed or not:
$$\eqalign{&\vert C \vert \ge 0\comma \; \cr &\vert C \vert \le1.}$$• Version is used together with the package name if the package name alone is ambiguous. Versioned dependencies (i.e., when a dependency requires certain versions of a package) are not natively supported in our formulation.
• Depends means all package dependencies will introduce new variables (if not already present) of the Boolean range as modeled above. Note that we do not enforce a lower bound because otherwise this would include all packages irrelevant of their necessity (alternatives may allow for only one choice out of multiple packages).
Next the dependencies are represented by 0..1―1..1 associations in our UML class diagram, which directly correspond to following ILP (assuming that C depends on D):
$$\vert C \vert - \vert D \vert \le0\comma \;$$which follows by inserting n 1 = 0 and n 2 = m 1 = m 2 = 1 in our general case inequalities. In cases where we deal with alternatives (e.g., assuming that C depends either on D or E whereas D and E may be both installed at the same time as long as no explicit conflict relation is stated), we obtain
$$\vert C \vert - \vert D \vert - \vert E \vert \le 0.$$Virtual packages (i.e., packages that are logical placeholders for packages with common functionality) could be modeled using subclassing with the virtual package as superclass and the concrete packages as subclasses.
• Conflicts are expressed by the following inequality (assuming C conflicts with D):
$$\vert C \vert + \vert D \vert \le 1.$$This encoding works as we operate only on the Boolean range. No packages at all would be correct, also either C or D, but not both together. This models exactly our desired semantics in this setting.
Finally, we glue all of these inequalities together by an objective function including all classes, which gets minimized:
Minimize
$$\vert C \vert + \vert D \vert + \vert E \vert.$$A main advantage of this objective function and ILP in general is that we can easily add coefficients (weights) that model the importance of the individual variables. For example, for package management we could use the package size (e.g., rounded to MB) as a weighting coefficient, which would mean that smaller packages get preferred over bigger ones.
For the example of the emacs23-nox package, this yields (only one or two inequalities of each category are shown for compact presentation):
Minimize
$$\displaystyle{\hbox{emacs23-nox}+{\hbox {emacs23-bin-common}+{\hbox {libasound2}+\cdot \cdot \cdot$$such that
$$\matrix{&\hbox{emacs23-nox}-\hbox{emacs23-bin-common} \le0\comma \; \cr &\hbox{emacs23-nox}-\hbox{libasound2} \le 0\comma \; \cr &\hbox{emacs23-nox}+{\hbox {emacs23}} \le 1\comma \; \cr &\hbox{emacs23-nox}+{\hbox {emacs23-gtk}} \le1\comma \; \cr &0\le \hbox{emacs23-nox} \le 1\comma \; \cr &\hbox{emacs23-nox} \ge 1.}$$The first and second side condition models the dependencies, the third and forth models the conflicts, the fifth states the Boolean range, and the sixth one enforces the selected package to be installed.
4.1.2. Implementation
For our experiment, we used the testing release of the Debian GNU/Linux operating system using its main (http://ftp.debian.org/debian/ testing main) and security (http://security.debian.org/ testing/updates main) repositories in June 2011.
We implemented the previously presented approach for Debian package management in two ways. We use a graphical user interface (GUI) tool called CLEWS (Niederbrucker & Sisel, Reference Niederbrucker and Sisel2011) capable of manipulating UML diagrams. It was developed as a prototype implementing our lightweight formal methods approach using ILP. We recently extended its functionality by using its application programming interface (API) in the context of software product configuration (Feinerer, Reference Feinerer2011). Based on this initial work, we now consider Debian GNU/Linux package configuration and subsequently Linux kernel configuration as shown in this paper.
CLEWS is a pure Java program and provides a Java API. However, to extract the Debian GNU/Linux package information, we used a C++ library of the APT package management tool shipped with Debian. To match both ends, we used the Java Native Interface where we call Java routines for creating classes and associations in the underlying UML diagrams managed by CLEWS. The advantage of using CLEWS is that it allows us to graphically investigate the modeled scenario and rearrange associations and classes and enables a direct translation to an ILP.
Our second implementation avoids the intermediate step of an additional tool like CLEWS and directly translates the package dependency information into an ILP. Again we extract the Debian package metadata via the APT C++ library. Now we use the Mixed ILP solver lp_solve (http://lpsolve.sourceforge.net) and its C API to directly create an ILP.
4.2. Linux kernel configuration
The configuration of a Linux kernel is mainly done by choosing whether certain drivers are directly included in the kernel, are loaded when necessary as modules, or are excluded. This somehow resembles a tristate logic (yes, module, no) inherent to Linux kernel configuration. The whole set of dependencies (i.e., which drivers or modules depend on others, which conflict with others, etc.) is written down in a set of so-called Kconfig files. Several hundred of them exist, typically with a single one in each subdirectory of the kernel source code. Normally each subdirectory contains a specific driver or system architecture, and basically all Kconfig files could be merged to a single large one containing the whole metadata representing constraints of the kernel configuration.
In its full form, Kconfig files are quite complex because they allow different syntax for the same semantics. For example, dependencies might be included because of encapsulating menu entries or may be rewritten with conditional if statements. Conceptually, all these constructs can be broken down to a basic set of primitive operations as follows:
• Config: This defines a configuration option.
• Tristate/string: This defines the type of the configuration option. We are mainly interested in Boolean and/or tristate conditions.
• Depends: This is a set of dependent configuration options. It is noteworthy that dependencies can be combined with expressions like conjunction (&&), disjunction (‖), or even negation (!). That is, conflicts can be implicitly encoded in the dependencies section.
• Selects: These are reverse dependencies. That is, the dependency is in the opposite direction and enforces the existence of a configuration option that is selected.
Besides these constructs, there are input prompts that are mainly useful for graphical configuration tools to decide which options are shown to the user, default values if the user does not make a decision on a specific option, numerical ranges for input values, help texts, comments, and whole menus that allow hierarchies and encapsulation of config options.
The following excerpt shows an example of a Kconfig file for the configuration option X86_VSMP from the x86 architecture (arch/x86/Kconfig) subdirectory:
config X86_VSMP
bool “ScaleMP vSMP”
select PARAVIRT_GUEST
select PARAVIRT
depends on X86_64 && PCI
depends on X86_EXTENDED_PLATFORM
—help—
Support for ScaleMP vSMP systems. Say “Y” here if this kernel is supposed to run on these EM64T-based machines. Only choose this option if you have one of these machines.
4.2.1. ILP formulation
We translate primitive Kconfig entries as shown before to the following inequalities, which form the side conditions of the generated ILP:
• Config: Each configuration option corresponds to a class in our UML representation or a variable in the underlying ILP. We enforce a minimal bound of 1 for entries chosen by the end user (e.g., for a config option C):
Clearly, the lower bound must not be used for automatically chosen options that are not enforced by direct user input.
$$\vert C \vert \ge 1.$$• Tristate/string: To simplify our experiment, we only consider Boolean options. That is, we map tristate logic to Boolean by assigning yes and module to yes and no to no. This corresponds to the idea that we want to build a minimal kernel in the sense that it is complete (i.e., no dynamic loading of modules necessary) but it does not use more drivers than absolutely necessary for correct operation:
Tristate options could be implemented via subclassing, with a superclass representing a state for inclusion in the solution and two subclasses for yes and module.$$0\le \vert C \vert \le 1.$$• Depends: We mainly distinguish between the three cases: conjunction, disjunction, and negation. Normal dependencies and those formed by conjunction can be expressed in the same way as we did with Debian packages (assuming C depends on both D and E):
$$\eqalign{&\vert C \vert - \vert D \vert \le 0\comma \; \cr &\vert C \vert - \vert E \vert \le 0.}$$For disjunction, we reuse
$$C \vert - \vert D \vert - \vert E \vert \le 0\comma \;$$whereas negation maps to (assuming C conflicts with D)
$$\vert C \vert + \vert D \vert \le 1.$$The latter works because for the Linux kernel configuration it does not make sense to include the same driver multiple times.
Note that, in principle, arbitrary complex expressions (mainly due to the existence of subexpressions that may be layered) may exist. Consequently, expressions need to be flattened out first to fall into the above categories.
• Selects: Analogous to classical dependencies, we model reverse dependencies by
assuming that C selects D in this example. The correctness is immediate again by using m 1 = 0 and n 1 = n 2 = m 2 = 1 for the general case inequalities.$$\vert D \vert \le \vert C \vert\comma \;$$
4.2.2. Implementation
For our experiment we used a vanilla Linux kernel version 2.6.39-rc4 (available at http://www.kernel.org). We start out with a Python parser for Linux Kernel config files called Kconfiglib (http://dl.dropbox.com/u/10406197/kconfiglib.html) version v3. Kconfiglib is capable of reading in all Kconfig files of a source tree, extracting their information, and bringing it in a format that can be more easily accessed in a streamlined way via Python. This allows us to restrict our attention to a basic set of primitive operators. Our implementation processes only the conjunctions reported by Kconfiglib after it has flattened out the constraints in order to uniformly access the Kernel configuration. We use Kconfiglib to create an intermediate XML format that can be easily accessed via C++. This way we can reuse parts of the implementation we already have and use for Debian package extraction. Similarly, we can create a UML class diagram both by interfacing CLEWS (Niederbrucker & Sisel, Reference Niederbrucker and Sisel2011) with its Java API via Java Native Interface and by directly creating an ILP in the lp_solve format.
5. EVALUATION
We evaluate the performance of our approach by a benchmark experiment that has two main objectives for investigation. First, we have to ensure that the generated solutions are reasonable. This means we have some sort of empirical evidence of the applicability of our theory presented so far in practical use. Note that we do not claim our approach to be “complete” in the sense that we are able to model all settings in both application domains. Nonetheless, we argue that our approach works for a broad class of the most common constraints yielding reasonable solutions. Second, we are interested in the performance of our generated ILPs because we argue that the translation of configuration problems to ILPs is lightweight and effective for real-world examples.
For the Debian package configuration use case, we check the correctness by generating an ILP for input packages that are a small proper subset of actually installed packages on a real working Debian system. Consequently, the solution of the ILP will include a lot of dependencies that should still be a subset of the actual system, however. We compare this solution with the list of installed packages on the real system and check dependencies with a package management tool like aptitude.
The multitude of generated constraints correspond to conjunctions of dependencies and some simple dependencies selecting either one or the other dependency. Both virtual packages and versioned dependencies are ignored. A possible implementation for versioned dependencies is to create a symbolic class for each relevant combination of package and version number. For simple relations between versioned packages, this works sufficiently. For complex version dependencies, this approach generates an overhead in the number of necessary variables of the ILP. There is also a negative impact on the overall usability because these superfluous variables occur in the final solution reported back to the user.
For the Linux kernel configuration we start with a set of manually chosen symbols that resemble some typical components of a configuration for a x86 PC. Based on these input symbols, an ILP is generated modeling the dependencies as logical conjunctions. Its solution now includes a list of kernel symbols modeling its dependencies as reported by Kconfiglib. We checked its quality by comparing it to the results obtained when doing a classical manual kernel configuration (with standard tools like make xconfig in the kernel source tree). We note that our generated ILP does not fully comply with the solutions proposed by the Linux standard tools. This is expected because we concentrate on conjunctive dependencies and neglect other features like string handling or variable ranges. Still, manual comparison shows that the produced results look similar to the solutions by standard tools and capture the main features. That is, our solution is a reasonable starting point for configurations that get manually fine-tuned later on.
To evaluate the scalability and runtime performance of our generated ILPs, we start with a fixed number of input packages (in the Debian setting) or input kernel symbols (in the Linux kernel setting) and measure its runtime for solution. We use this as a base line. Note that all dependencies must be available to our tool and potentially be processed because we do not know in advance which will be relevant for the input packages/symbols. Now we stepwise increase the number of input packages/symbols. This means that likely a higher amount of dependencies needs to be processed and more inequalities will be generated.
Figure 5 and Figure 6 depict the runtimes of lp_solve in seconds for the generated integer linear programs. In Figure 5 we see a linear scaling behavior when increasing the number of packages to be processed as input by the user. The runtime is in the range of 10–20 s for amounts of packages that already go beyond any typical installation. Figure 6 shows the situation for the processing time of the ILP for kernel configuration. The total runtime is only a few seconds where we see almost a (sub)linear scaling behavior. We are not completely sure why there is a decrease in runtime in the range of 2000–3000 input symbols. A possible explanation could be that because the runtime is under 1 s, small differences in memory allocation might cause this effect. Note that each experiment was run several times to exclude unreproducible effects caused by singular events. Another explanation could be that once a certain amount of symbols is included in the solution set, most conjunctive dependencies are automatically fulfilled. This avoids a stepwise increase in the number of individual symbols, resulting in rather expensive rechecking of multiple dependency constraints.
Runtime of lp_solve in the Debian GNU/Linux setting.
Runtime of lp_solve for the Linux kernel configuration.
The figures depict the mean runtimes averaged over all runs. The runs were conducted on low-end to middle-class PC hardware (two cores, 3 GB RAM), so the results should be even faster on more recent or dedicated hardware.
When using a GUI tool like CLEWS, the main constraining factors are the graphical components of the Java runtime. The actual translation of the UML diagram to inequalities is quite fast (a few seconds); however, displaying its results can take more time (tens of seconds). Nevertheless, for realistic examples consisting of hundreds of classes and associations between them (instead of several thousands), such GUI tools work reasonable well.
6. RELATED WORK
The representation of configuration problems in UML has some history. Felfernig et al. (Reference Felfernig, Friedrich and Jannach2000) use it as domain-specific language for the construction of knowledge-based configuration systems. The UML constructs are then transformed to logical sentences in order to solve the configuration task. Later Felfernig et al. (Reference Felfernig, Friedrich, Jannach and Zanker2002, Reference Felfernig, Friedrich, Jannach, Stumptner and Zanker2003) used UML and OCL for configuration knowledge base development and maintenance. Another framework following an object-oriented paradigm is described by Mailharro (Reference Mailharro1998). A configuration problem is considered both as a classification problem and as a constraint satisfaction problem (CSP). Stumptner et al. (Reference Stumptner, Friedrich and Haselböck1998) and Fleischanderl et al. (Reference Fleischanderl, Friedrich, Haselböck, Schreiner and Stumptner1998) extended the standard CSP model and work also with knowledge bases written in an object-oriented representation language. The presented papers cover relatively large fractions in the “configuration universe.” A translation to logics or CSP seems natural. However, such an expressive power comes at the price of higher complexity such that “almost any practical applications of configurators crucially depend on the application of search heuristics” (Felfernig et al., Reference Felfernig, Friedrich, Jannach, Stumptner and Zanker2003, p. 44). In contrast, we identify our ILP approach, which works only with a limited set of design constructs, as more lightweight and driven for efficiency on standard configuration tasks.
Soininen et al. (Reference Soininen, Tiihonen, Männistö and Sulonen1998) build a general ontology of product configuration covering connection-, resource-, structure-, and function-oriented approaches. Our approach can be seen in the spirit of the resource-based paradigm where “components … are modeled as abstract resources, and each technical entity is characterized by the type and amounts of resources it supplies, consumes, and uses” (Heinrich & Jüngst, Reference Heinrich and Jüngst1991, p. 19).
Recently, there was a dedicated Special Issue on configuration in AI EDAM (Felfernig et al., Reference Felfernig, Stumptner and Tiihonen2011) with contributions on a variety of aspects of configuration. Several high-quality approaches have been presented that typically solve a specific problem very well.
Mayer et al. (Reference Mayer, Stumptner, Killisperger and Grossmann2011) propose a configuration method for work processes. The key challenge is that paths and subprocesses in a work process cannot be handled adequately with existing methodology. As remedy, they extend constraint-based configuration methods to model certain aspects in UML.
Felfernig and Schubert (Reference Felfernig and Schubert2011) deal with personalized diagnoses for inconsistent user requirements. They introduce an algorithm capable of giving detailed and informative feedback when inconsistent requirements are detected. This is in analogy to our ILP approach because we can identify inconsistent parts in UML class diagrams and give instant and useful feedback to the user (Feinerer, Reference Feinerer2007). Our feature is even implemented in CLEWS (Niederbrucker & Sisel, Reference Niederbrucker and Sisel2011), which highlights inconsistent paths via red lines and allows the user to modify the design.
Nevertheless, Falkner et al. (Reference Falkner, Haselböck, Schenner and Schreiner2011) observe that although many individual approaches in AI achieve superior results in subfields of configuration, they are often hard to use for general-purpose modeling and reach their limits in scalability.
Consequently, lightweight approaches that scale well and are capable of modeling real-world applications as identified by Falkner et al. (Reference Falkner, Feinerer, Salzer and Schenner2010) are necessary. We fill this gap by the unified ILP theory presented in this paper, significantly extending previous work on this topic (Feinerer & Salzer, Reference Feinerer and Salzer2007).
In the context of package management, there are promising results by Tucker et al. (Reference Tucker, Shuffelton, Jhala and Lerner2007) that deal with the install problem, minimum install problem, and uninstall problem. They encode the install problem and the uninstall problem utilizing SAT formulas, and the minimum install problem with SAT and pseudo-Boolean constraints to encode integer costs. The latter can be transformed to an ILP. Janota et al. (Reference Janota, Lynce, Manquinho and Marques-Silva2012) tackle the software package upgradability problem by using an encoding based on weighted partial MaxSAT formulas, which they solve with weighted partial MaxSAT solvers and optimization pseudo-Boolean solvers. Abate et al. (Reference Abate, Di Cosmo, Treinen and Zacchiroli2011) present a modular package manager, which could be used as a framework for our approach. There is also mancoosi, a European research project in the 7th Research Framework Programme of the European Commission, which deals with managing software complexity and package management. It should be noted that our ILP approach is not directly comparable to tailored approaches as presented by Tucker et al. (Reference Tucker, Shuffelton, Jhala and Lerner2007) and Janota et al. (Reference Janota, Lynce, Manquinho and Marques-Silva2012). They are natively capable of handling more complex input cases, like dependencies on specific versions of packages, which are not dealt with in our experiment. Their solutions are more complete; however, their scalability depends heavily on the complexity and structure of the encoded dependencies.
For Linux kernel configuration, Sincero et al. (Reference Sincero, Schirmeier, Schröder-Preikschat and Spinczyk2007) propose to see the configuration problem as a software product line utilizing methodology of this field. Zengler and Küchlin (Reference Zengler and Küchlin2010) encode the Linux kernel configuration as a SAT problem. In addition to our approach, they are capable of handling tristate variables, complex expressions on dependencies and selections, and menu blocks. Another difference is that they are mainly interested in finding sets of valid configurations and testing for satisfiability of a given configuration. For enumerating valid partial configurations when using SAT-solvers, Voronov et al. (Reference Voronov, Åkesson and Ekstedt2011) propose techniques employing binary decision diagrams. Complementary, our ILP approach has built-in support for minimizing variable values and therefore for finding minimal configurations.
Our approach of using UML as a design language and its mostly automatic translation to ILP aims at a broad range of configuration scenarios. The major focus lies in an intuitive interface and lightweight formal methods to handle standard configuration use cases in an efficient manner. Clearly, this implies that specialized solutions tailored for a specific application domain are more expressive and thus can provide better (in terms of completeness) solutions.
7. CONCLUSION
Due to the success of AI methods in configuration, we saw a steady increase in their usage for real-world applications for a broad range of domains. However, the complexity and size of the problems have been growing. One of the key challenges is to choose a matching technology that is expressive enough to model realistic scenarios but which can be handled efficiently. Only the latter allows us to scale the applied methodology to realistic problems consisting of thousands of components and even more interactions. In this paper, we proposed a unified theory based upon ILP. We showed how to model important concepts as identified in the literature via UML class diagrams and corresponding constraints, and how this terminology can be translated into an ILP. This idea is general enough to be applied to other object-oriented formalisms. ILP is known for its performance because certain subclasses are of polynomial time complexity and there is a wide range of excellent solvers available despite its NP-completeness in the general case. Within our formulation, polynomial algorithms exist as long we have no upper bounds for sums over two variables because this results in indeterminism whether one or the other variable needs to be increased, and backtracking if not successful.
Consequently, we argue that with our approach, a broad class of configuration problems can be modeled and we gain reasoning support via lightweight formal methods. The ILP formulation is especially suited for configuration problems with large conjunctive dependencies and few conflicts and occasional subclassing. The advantage over logics and SAT-based techniques is that minimizing an objective function is a primary objective that is central in configuration tasks. By contrast, in logics nontrivial techniques have to be employed for finite model reasoning and minimizing variables over integer ranges.
We evaluated our approach with two real-world large-scale examples: Debian GNU/Linux package management and the Linux kernel configuration. The aim of both applications was to show that our approach allows for an intuitive modeling of the configuration task when dealing with the core features of the respective domain. We expect our approach to work when scaled on larger problem instances. We argue that both aims are fulfilled. However, it should be clear that specific tools tailored for the application domain are typically better in terms of expressive power in order to cover all aspects of the configuration task. We observe this for both Debian package management and the Linux kernel configuration. In the end, it boils down to finding the right balance between needed features and the underlying expressive power of the constructs. For example, when handling tristate values via subclassing, there might be low overhead by the construction itself but the construct might be triggered very often; or when the application domain exhibits constraints mainly consisting of disjunctions instead of conjunctions; or how subclassing and hierarchies are implemented (for a discussion see, e.g., Maraee & Balaban, Reference Maraee and Balaban2007; or Männistö et al., Reference Männistö, Peltonen, Soininen and Sulonen2001).
ILP and SAT seem to be well suited for a diverse field of configuration tasks where each technique has its unique advantages. We think the next step toward more efficiency in configuration lies in the combination of various approaches into a hybrid framework to get the best from multiple worlds. For example, in the context of package management, a viable way to handle versioned dependencies is to use ILP as a building block that is called multiple times but with different subsets of variables. Because version conflicts are rare, this “outsourcing” of some constraints seems promising instead of forcing everything into a single large ILP.
As future work, we are working on identifying more complex constraints in large configuration applications given by our project partners at Siemens AG and how they can be modeled efficiently. We aim for highly efficient configuration tools with a wide range of formal methods support such that design engineers can model their settings in a natural way and get immediate feedback on design errors. Again a hybrid approach appears to be the most promising way toward achieving this goal.
ACKNOWLEDGMENTS
We thank the anonymous reviewers for their constructive and insightful comments.
Ingo Feinerer has been an Assistant Professor at the Vienna University of Technology since 2008. He received a PhD in computer science from the Vienna University of Technology and a PhD in business administration from the Vienna University of Economics and Business. In 2007 he was postdoctoral visiting scholar at the Computer Science Department of Carnegie Mellon University. His expertise and research interests comprise efficient methods for configuration, formal methods, text mining, and databases.
