Towards a Formalism of Configuration Properties Propagation David Fabian1 and Radek Mařík2 and Tomáš Oberhuber3 Abstract. Software configuration often studies two issues: firstly, designed to administer the installation of large scaled networks of how to merge various software components together to create a pro- UNIX systems, or MenuConfig [16, ch. 7] which is a primary tool for gram with a fixed structure that fits the requirements, and secondly, Linux kernel configuration. Then there exist general tools like Lin- how to effectively set up the remaining (usually installation specific) uxConf [10] and Freeconf [9]. Freeconf is a unique tool as it offers a configuration options when deploying the program. Nowadays, the multi-platform and a multi-desktop configuration of applications of user demands a simple and well arranged way to set up these options, any kind. possibly through a graphical user interface (GUI). There are vari- ous tools designed to assist the user with these tasks. In this paper, a general multi-platform configuration tool Freeconf is introduced. 1.2 Configuration Properties Our technique to simplify a GUI, which has been incorporated into Many automatic configuration tools suffer from the overwhelming Freeconf, is described. This technique is based on a set of properties complexity of the user interface they generate which is a severe prob- that allow splitting the universe of configuration options into sev- lem for the user. One of the possibilities of solving this issue consists eral categories with a clear semantics and rules that control the dy- in breaking the uniform universe of keys to several categories and namics of options distribution to these categories in response to the providing the categories with an exact semantics. Then, only the keys user’s actions. The rules are currently only implemented in the source from a category which is the most interesting to the user at a given code of Freeconf as a proof-of-concept without any formal proof of moment can be displayed. The solution presented here is based on a soundness or completeness. Results from the domain of Rule-Based set of properties of keys, in other words, on a set of labels that are Constraint Programming have been applied in the paper to develop a assigned to every key and determine its membership to a category. In formal description of the rules. Table 1, there is an example of a set of possible properties for keys categorization. The last property undefined represents a set of keys 1 Introduction that do not have their value set and therefor could cause problems in the output of the configuration. In other words, this property allows While working with a software application, the user usually needs to us to describe a form of inconsistency with the instant state of the adjust a working environment to her needs. Nowadays, almost every configuration. application lets the user to perform some configuration. The aver- age user often does not understand the background of the program property meaning and expects a nice graphical user interface (GUI) to assist her. How- mandatory The key is important to the configured application and ever, there are many applications (especially in the GNU/Linux en- must be filled in. meaningful The key has sense in the present settings and its exis- vironment) that do not have any GUI whatsoever and the only way tence is not ruled out by any dependency. how to configure them is through configuration text files. A serious undefined The key finds itself in an invalid state such as that it problem of these files is that their syntax differs greatly, so the user has no value set or the value is in conflict with depen- must learn it first from the documentation. It is also necessary for dencies. the user to deeply understand the meaning of various configuration Table 1. Properties used for configuration keys categorization. options (configuration keys), their dependencies, and their possible values. Having each key as a feature, this approach resembles feature modeling [7] with extra-functional attributes. The semantics for op- 1.1 Configuration Tools erators and dependencies, however, is different. The distribution of keys into categories does not have to be static, There exist tools that address the above mentioned difficulties. Some some keys can change their roles during the configuration process are focused on a given domain (or even at one application, Linux in response to an outer activity (a dependency event, user input). A kernel is popular) like SmartFrog [2] and LCFG [1, 3] which are mechanism is needed to control the development of the categories. 1 Dept. of Mathematics, Faculty of Nuclear Sciences and For this, Freeconf uses rules to control the propagation of properties. Physical Engineering, Czech Technical University in Prague, The current set of rules in Freeconf has been constructed by hand (fabiadav@fjfi.cvut.cz). and tested only empirically; it has not been proved, whether the rules 2 Dept. of Cybernetics, Faculty of Electrical Engineering, Czech Technical University in Prague. are sound or complete. Techniques of the rule-based constraint pro- 3 Dept. of Mathematics, Faculty of Nuclear Sciences and Physical Engineer- gramming can provide a proof; however, one must first give a formal ing, Czech Technical University in Prague. description to the rules. The rest of this paper is divided as follows. In Section 2, a brief in- 3 Freeconf troduction to Rule-Based constraint programming is presented. Sec- tion 3 describes the structure of Freeconf and a set of properties used To help the user to overcome difficulties of software configuration, in the tool. Section 4 introduces the way Freeconf handles propa- the project Freeconf has been established. The purpose of this project gation of properties. Finally, Section 5 presents a formalized set of is to unify the existing configuration process and to assist the user rules, and Section 6 concludes. by automatically creating the configuration dialog window similar to one in Fig.1. The configuration process must be smooth from the point-of-view of the user: the dialog must fit nicely into the desktop 2 Rule-based Constraint Programming environment, configuration options must be presented in the logical order, and only what is crucial to fill in should be shown. To better Rule-Based constraint programming is a special case of a more gen- understand how Freeconf addresses these tasks, a short description eral constraint programming studied in [4, 8, 12, 13]. Constraint pro- of its inner structure is presented. gramming is an alternative approach to programming in which a model of a problem is declarative, and then it is solved by general or domain-specific methods. The model is formed by a set of con- straints (requirements) on variables so that acceptable variable as- signments correspond to solutions to the problem [4]. Following [8], let us assume a sequence of variables X = x1 , . . . , x n with respective domains D1 , . . . , Dn , so each xi takes its value from the set Di . Definition A constraint C on X is a pair hCR , Xi where CR is an n-ary relation over the domains Di , i.e., CR ⊆ D1 × . . . × Dn , of solutions to the constraint. Figure 1. Example of Freeconf generated configuration dialog. Definition A constraint satisfaction problem (CSP) is a triple hC, X, Di where X = x1 , . . . , xn is a finite sequence of variables with respective domains D = D1 , . . . , Dn , and C is a finite set of Client Win constraints, each on a sub-sequence of X. Client KDE Library Definition A solution to the CSP hC, X, Di is an element d ∈ D1 × . . . × Dn such that for each constraint C ∈ C on a sequence of vari- Client Console Configuration ables Y it holds d [Y ] ∈ C where d [Y ] stands for a projection of d to Dialog Package Y = xi(1) , . . . , xi(l) , i.e., d [Y ] = di(1) , . . . , di(l) . Sol (hC, X, Di) will denote the set of all solutions to the CSP hC, X, Di. Figure 2. Components of the Freeconf project. There exist general algorithms for solving a CSP [8, 14] and even entire frameworks, such as Skyblue [15], ECLiPSe [5], and Minion [11].. 3.1 Structure of Freeconf The core concept of Rule-Based programming is a rule. Rules are condition-action pairs where the condition part is used to determine The project consists of several components as shown in Fig.2. The whether the rule is applicable and the action part defines the action most important one is the Freeconf library which contains the en- to be taken [6]. A formal definition of a rule taken from [8] follows. tire functionality. The library is shared by graphical client applica- tions (clients), the sole purpose of which is to present a configuration Definition Assume that A and B are sets of constraints such that the dialog to the user. One can have many different clients, each for one constraints in A and B are on the variables X with domains D. The desktop environment. The clients are supposed to be very small (less expression B ← A is a constraint propagation rule. A is called the than a 1000 lines of code), so it should be very simple to create an- condition and B the body of the rule. Rules act as functions on CSPs. other one. To be able to configure an existing application, the library The application of a rule to a CSP with the variables X is given by needs to be provided with an appropriate configuration package. The  package is a collection of XML files that semantically describe the hC ∪ B, X, Di ifA ⊆ C, configuration file the application understands (native configuration (B ← A)(hC, X, Di) := hC, X, Di otherwise. file). It contains a list of all keys, their default values, properties and dependencies, and a rough description of what the resulting dialog The rule B ← A is correct if Sol(hA, X, Di) ⊆ Sol(hB, X, Di). should look like. Keys can be organized into configuration sections. The number of keys can vary depending on the configured applica- user. That is why another set of properties was added to Freeconf tion. Usually, configuration packages have tens to hundreds of keys, which would enable splitting keys into different categories. Thus, but some configurations utilize up to thousands of keys like in the only keys from a specific category can be shown to the user. The case of the Linux kernel. current set of properties which extends those presented in Table 1 is When a package is loaded, the library constructs three tree struc- summarized in Table 3. tures — a template tree for storing key properties, a configuration tree for storing values and handling dependencies, and a GUI tree property meaning for dialog modeling. The trees are interconnected, and one can freely static mandatory If it is true, the key is mandatory and must be always shown. traverse from one node of one tree to the matching node of another static active If it is false, the key is not visible to the tree. Leave nodes correspond to keys and their properties, the non- client. leave nodes represent configuration sections (there is always a root- dynamic mandatory This property can only be set from a depen- section present). When a client needs data for dialog construction, dency handler. If it is true, the key is manda- tory and must be shown. This property has it connects to the library through the client-library interface and ob- no meaning when the static mandatory prop- tains various properties for each node. Fig.3 shows the situation. The erty is set to false. interface forms a tree which is placed between the GUI tree in the dynamic active This property can only be set from a depen- library and the hierarchy of GUI elements (group-boxes, line edits, dency handler. If it is false, the key does not check-boxes, etc.). The client organizes the GUI elements to another have sense in the current settings. This prop- erty has no meaning when the static active tree that is very closely related to the actual look of the dialog. property is set to false. inconsistent The key does not have neither a value, nor a default value set and is dynamically manda- tory and dynamically active. empty The property is only applicable to section nodes. It states whether the section is empty, i.e., all its children are hidden. Table 3. Additional properties used for keys categorization. All static properties are stored in the package as a part of a tem- plate describing the native configuration file, while the dynamic ones library GUI tree are a part of a file describing dependencies. client tree i Mandatory property states, whether the key is important or not. n group-box t section Important keys should be visible in the dialog while non-mandatory e keys can be hidden, so the dialog becomes less confusing. The static check-box group-box r boolean section f version of this property is used for packages with no dependencies a c or for keys unaffected by any dependency. The dynamic version can, spin-box line-edit number string e as in the current version of Freeconf, override the static state only when the static mandatory property is not false (that means static Figure 3. Tree data structures and the client-library interface. The top figure non-mandatory keys are definite). shows how the client tree is transformed into a dialog form. Active property has two different semantics. In its static version, it is used to prevent the library from announcing the key to the client. In other words, if the property is set to false, the key is virtually commented out. It is easier to disable the key that way than to delete 3.2 Properties in Freeconf it from the entire package which is non-trivial. The dynamic version of this property serves the purpose of ruling out situations that do not Since the beginning of the project, every client could use the basic have sense (e.g., when the user checks the "no sound" option, setting set of properties for each key. These basic properties are presented in the "volume" option becomes nonsensical and this option should be Table 2. left out from the dialog or at least disabled). property meaning Inconsistency is a special situation when the key does not have any name Name of the key. value set, but it is important to the configured program. This can hap- label Label for the key. pen, especially when the configuration is run for the first time, and help Tooltip help text. there exist keys which do not have default value set by the creator value Value of the key or default value if no value exists. type Type of the key. It can be: boolean, number, string, of the package. When this situation occurs, the user has to be told stringlist, or section. so and must be able to solve the problem with minimum effort. It follows from the above mentioned description of the properties there Table 2. Basic properties of configuration keys. are situations where inconsistency is acceptable and the user needs not to be alerted (e.g., when the key is statically inactive). In fact, Every key type adds additional properties, e.g., a number can have there exists exactly one combination of the properties which needs a minimum, a maximum, and a step by which the value increments some user assistance (i.e., the client must be informed) — the key and decrements. String keys usually have a regular expressions asso- is dynamically mandatory, dynamically active, and inconsistent at ciated with them constraining their value. the same time. In other situations, such as when the key is only dy- While the basic set of properties would generally suffice to con- namically active but not mandatory, the key is simply left out from struct a dialog, the dialog would look overfilled and confusing to the the native output (so the native output will always contain only keys with a defined value). For this algorithm to be valid, all counter must be set to the correct Emptiness is an important property which naturally arose from the value at start time. This is called the initialization phase. All counters need of hiding non-mandatory keys. The user cannot be distracted by are set to zero, and the tree is traversed by depth-first search. Every optional keys, so those must be hidden. If there is a section containing leave node is evaluated and the existing propagation framework is only hidden keys, there is no point of displaying it. The empty prop- used to initialize all counter values. erty can help the client with hiding of unnecessary GUI elements. It is also possible to emit a global change, for instance, when the user overrides the mandatory property and enforces showing all keys which are dynamically active. In such a case, all leave nodes are 4 Properties Propagation asked to reevaluate their states similarly to the initialization phase. Freeconf maintains properties in connected tree structures as de- In fact, the initialization phase is a form of a global change. scribed in Section 3. The Freeconf library must be able to inform the clients about the state of each property in every node the client– 5 Rules library interface announces. For leave nodes, this becomes trivial. For non-leave nodes, however, the state of a property must reflect what is The above mentioned algorithm was implemented in an ad hoc man- happening in all of node’s direct successors. ner. All property evaluation procedures were tailored to the seman- tics described in Section 3. The result is a set of rules implemented as condition statements in the source code. 4.1 Propagation Mechanism The goal of this section is to bring a formal description of the resulting rules based on definitions from Section 2. To keep record of the number of properties in children nodes, ev- ery section has a set of counters, each bound to a specific property. Counters hold how many times the matching property occurs in the 5.1 Formal Description successors. For example, for the inconsistent property the "inconsis- Let K = {k1 , . . . , kn } be a set of indices for keys and S = tent count" counter exists in each section and if it is, for instance, set {s1 , . . . , sl } a set of indices for sections. Let parent : K ∪ S → to two, then there are exactly two children nodes that are inconsistent. S ∪ {∅} be a mapping returning for each key or section its parent. If a counter reaches zero, a message about the change of a property The symbol of an empty set is returned for the top-level section. All is sent to the client from the affected section. The section must also properties of keys will be modeled as Boolean variables. For exam- inform its parent (i.e., another section) about the change, so the ap- ple, dynactx will denote a dynamic active property of a key with an propriate counter of the parent can be adjusted. Similarly, a message index x ∈ K. Together with the properties from Table 3, variables must be sent whenever a nullified counter is incremented. def valsetx and valsetx will be used to describe the states where a The entire propagation schema can be seen in Fig.4. default value and a value have been set to the key, respectively. Section counters will be modeled as non-negative integer vari- section ables. As an example, inconsistcounty represents the state of an if counter = 0 then notify parent inconsistent counter in a section with an index y ∈ S. If the index is counter ∅, no action is performed. decrement Moreover, there is a Boolean variable called showallact which boolean section send message to client tree enables showing even non-mandatory properties (i.e., showing all ac- tive keys regardless of the state of the mandatory property). The list notify parent of all rules currently used in Freeconf follows. number string send message In the initialization phase, dynactx and dynmanx are set accord- to client tree ing to the static version of the properties and inconsistentx is eval- inconsistency uated for the first time. changed to false dynactx ←staticactx ∀x ∈ K Figure 4. Propagation of properties in Freeconf. Inconsistency of the bold dynmanx ←staticmanx ∀x ∈ K node has been changed. The information is propagated into the parent inconsistentx ←(¬def valsetx ∧ ¬valsetx )∧ node (dashed). The property can be further propagated. Every change is sent to the client tree also. ∧ dynmanx ∧ dynactx ∀x ∈ K When the valsetx variable changes its value, these rules are ap- When the state of a property (inconsistency in this case) has been plied to update inconsistency. changed, the node notifies its parent about the change. The parent section increments or decrements the matching counter and checks, inconsistentx ←(¬def valsetx ∧ ¬valsetx )∧ whether the counter is zero or not. If it is zero, the notification is ∧ ¬inconsistentx ∧ dynmanx ∧ propagated further up the tree. This leads to the expected behavior in ∧ dynactx ∀x ∈ K the client since every path leading to an inconsistent key is marked, so the client can render it appropriately. The top-level section (a con- figuration tab in fact) also knows about the overall state of all keys ¬inconsistentx ←¬(¬def valsetx ∧ ¬valsetx )∧ underneath and it can, for instance, forbid creating the native output ∧ inconsistentx ∀x ∈ K until all inconsistencies have been resolved. This method requires a protection mechanism against resending the same message. An ob- Whenever either dynmanx or dynactx variable changes its vious solution would be to remember the last state of each property value, the inconsistent state of the node must be reevaluated and the for every node and inform the parent only if the state changes. parent’s counter is adjusted accordingly. Clearly, a problem of the current implementation is the lack of inc(inconsistcountparent(x) ) ← formal description. All condition statements are scattered across ← dynmanx ∧ inconsistentx ∧ dynactx ∀x ∈ K the source code, and it is very complicated maintaining them even though the number of the properties is very small. The design is also not very robust since a small change in any of the conditions will dec(inconsistcountparent(x) ) ← (1) render the system non-functioning. This actually happened — one ← (dynmanx ∧ inconsistentx ∧ ¬dynactx )∨ conjunction was overwritten by mistake by a disjunction, and the client started behaving strangely. It was obvious there was a mistake ∨ (dynactx ∧ inconsistentx ∧ in a condition, but it was difficult to find it. ∧ (¬dynmanx ∨ ¬inconsistentx )) ∀x ∈ K If the inconsistcounty alters, the section must test if it is not 6 Conclusion necessary to propagate the information further. This paper introduces Freeconf, a multi-platform configuration tool, and a technique which reduces the problem of very complex graph- dec(inconsistcountparent(y) ) ∧ ¬inconsistenty ← ical user interfaces that are often generated by automatic configura- ← (inconsistcounty = 0) ∧ inconsistenty ∀y ∈ S tion tools. The technique is based on splitting configuration options into categories using properties and forming a set of rules that con- trol the dynamics of the evolution of the categories. A set of rules has inc(inconsistcountparent(y) ) ∧ inconsistenty ← been proposed to be used in Freeconf to simpify its graphical output. ← ¬(inconsistcounty = 0) ∧ ¬inconsistenty ∀y ∈ S The rules have been implemented in the source code as a proof-of- concept, and it has been empirically verified that the rules work. In The mandatoryshowny and activeshowny counters change this paper, a formal description of the rules has been presented based when a dependency alters dynmanx and dynactx , respectively. It on the theory of Rule-Based programming. The proof of soundness must be also tested whether the static equivalents to the respective and completeness of the rules is subject of future work. properties have not been set to false. 7 Acknowledgments ¬dynmanx ←¬staticmanx ∧ This work was partially supported by the project of the Stu- ∧ dynmanx ∀x ∈ K dent Grant Agency of the Czech Technical University in Prague ¬dynactx ←¬staticactx ∧ No. SGS11/161/OHK4/3T/14, 2011-13 and Research Direction ∧ dynactx ∀x ∈ K Project of the Ministry of Education of the Czech Republic No. MSM6840770010. inc(mandatoryshownparent(x) ) ←dynmanx ∀x ∈ K dec(mandatoryshownparent(x) ) ←¬dynmanx ∀x ∈ K REFERENCES inc(activeshownparent(x) ) ←dynactx ∀x ∈ K [1] Paul Anderson, LCFG: A Practical Tool for System Configuration, The dec(activeshownparent(x) ) ←¬dynactx ∀x ∈ K USENIX Association, 2008. [2] Paul Anderson, Patrick Goldsack, and Jim Paterson, ‘SmartFrog Meets The emptyy variable must be reevaluated for each section every LCFG: Autonomous Reconfiguration with Central Policy Control’, in time any of its counters (except inconsistcounty ) changes. Proceedings of the 17th USENIX conference on System administration, LISA ’03, pp. 213–222, Berkeley, CA, USA, (2003). USENIX Associ- ation. ¬emptyy ∧ dec(sectionshownparent(y) ) ← [3] Paul Anderson, Alastair Scobie, and Division Of, ‘LCFG - the Next Generation’, in UKUUG Winter Conference. UKUUG, (2002). ← emptyy ∧ ¬(sectionshowny = 0)∨ [4] K.R. Apt, Principles of Constraint Programming, Cambridge Univer- ∨ (showallact ∧ ¬(activeshowny = 0))∨ sity Press, 2003. [5] K.R. Apt and M. Wallace, Constraint Logic Programming Using ∨ (¬showallact ∧ ¬(activeshowny = 0)∧ ECLiPSe, Cambridge University Press, 2007. ∧ ¬(mandatoryshowny = 0)) ∀y ∈ S [6] Krzysztof R. Apt and Eric Monfroy, ‘Constraint Programming viewed (2) as Rule-based Programming’, CoRR, cs.AI/0003076, (2000). [7] David Benavides, Pablo Trinidad, and Antonio Ruiz-Cortés, ‘Auto- emptyy ∧ inc(sectionshownparent(y) ) ← mated reasoning on feature models’, in Proceedings of the 17th in- ternational conference on Advanced Information Systems Engineering, ← ¬emptyy ∧ ((mandatoryshowny = 0)∧ CAiSE’05, pp. 491–503, Berlin, Heidelberg, (2005). Springer-Verlag. [8] Sebastian Brand, Rule-Based Constraint Propagation Theory and Ap- ∧ (sectionshowny = 0)) ∨ ((activeshowny = 0)∧ plications, Ph.D. dissertation, 2004. ∧ (sectionshowny = 0)) ∀y ∈ S [9] David Fabian, System for Simplified Generating of Configurations, Master thesis, Faculty of Nuclear Sciences and Physical Engineering, Prague, 2011. in Czech. 5.2 Weaknesses of Freeconf Design [10] Jacques Gélinas. Linuxconf homepage, 2005. http://www.solucorp.qc.ca/linuxconf/. It can be easily seen that some of the rules are not optimal. For in- [11] Ian P. Gent, Chris Jefferson, and Ian Miguel, ‘Minion: A fast scalable stance, the second rule in 1 could be shortened by leaving out the last constraint solver’, in Proceedings of ECAI 2006, Riva del Garda, pp. 98–102. IOS Press, (2006). occurrence of inconsistentx . In 2, the rules should be mutually ex- [12] Michael Gleicher, ‘Practical issues in graphical constraints’, in Princi- clusive, but it is non-trivial showing the head formulas really behave ples and Practice of Constraint Programming, pp. 407–426. MIT Press, that way. (1995). [13] K. Marriott and P.J. Stuckey, Programming With Constraints: An Intro- duction, Mit Press, 1998. [14] Nico Roos, Yongping Ran, and H. Jaap van den Herik, ‘Combining Lo- cal Search and Constraint Propagation to Find a Minimal Change Solu- tion for a Dynamic CSP’, in Proceedings of the 9th International Con- ference on Artificial Intelligence: Methodology, Systems, and Applica- tions, AIMSA ’00, pp. 272–282, London, UK, UK, (2000). Springer- Verlag. [15] V. Saraswat and P. Van Hentenryck, Principles and Practice of Con- straint Programming: The Newport Papers, chapter The SkyBlue Con- straint Solver and Its Applications, 385–405, Mit Press, 1995. [16] Sven Vermeulen, ‘Linux sea’. http://swift.siphos.be/linux_sea, 2012.