LoCoCo on Saturday, July 10th

09:00‑10:00 Invited Talk
Location: IF 1.16
09:00 Carsten Sinz (University of Karlsruhe)
Software Configuration: What can we learn from Product Configuration?

Systems to configure complex products like automobiles or machinery have been around for quite a while, and are nowadays used routinely by many companies. Both interactive systems (used, e.g., for on-line sales) and batch systems (to control the production process, where no user interaction is permitted) are in common use. In this talk we will give an overview on formalisms, systems and algorithms that are currently used in product configuration. We will also present two concrete product configuration systems from the automotive and medical devices industries, and relate them to current research in software configuration.

10:30‑12:30 Session 1
Location: IF 1.16
10:30 Claude Michel and Michel Rueher
Handling software upgradeability problems with MILP solvers

Upgradeability problems are a critical issue in modern operating systems. The problem consists in finding the ``best'' solution according to some criteria, to install, remove or upgrade packages in a given installation. This is a difficult problem: the complexity of the upgradeability problem is NP complete and modern OS contain a huge number of packages (often more than 20 000 packages in a Linux distribution). Moreover, several optimization criteria have to be considered, e.g., stability, memory efficiency, network efficiency. In this paper we investigate the capabilities of MILP solvers to handle this problem. We show that MILP solvers are very efficient when the resolution is based on a linear combination of the criteria. Experiments done on real benchmarks show that the best MILP solvers outperform CP solvers and that they are significantly better than Pseudo Boolean solvers.

11:00 Josep Argelich, Daniel Le Berre, Ines Lynce, Joao Marques-Silva and Pascal Rapicault
Solving Linux Upgradeability Problems Using Boolean Optimization

Managing the software complexity of package-based systems can be regarded as one of the main challenges in software architectures. Upgrades are required on a short time basis and systems are expected to be reliable and consistent after that. For each package in the system, a set of dependencies and a set of conflicts have to be taken into account. Although this problem is computationally hard to solve, efficient tools are required. In the best scenario, the solutions provided should also be optimal in order to better fulfill users requirements and expectations. This paper describes two different tools, both based on Boolean satisfiability (SAT), for solving Linux upgradeability problems. The problem instances used in the evaluation of these tools were mainly obtained from real environments, and are subject to two different lexicographic optimization criteria. The developed tools can provide optimal solutions for many of the instances, but a few challenges remain. Moreover, it is our understanding that this problem has many similarities with other configuration problems, and therefore the same techniques can be used in other domains.

11:30 Paulo Trezentos
Comparison of PBO solvers in a dependency solving domain

Linux package managers have to deal with dependencies / conflicts of packages required to install by the user. As a NP-complete problem this is a hard task to solve. Several approaches are being pursued. Apt-pbo is a package manager based on apt project that encodes the dependency solving as a Pseudo-boolean problem. This paper presents an introduction to the comparison of different PBO solvers and their effectiveness for the given encoded problems.

12:00 Emmanuel Ohayon, Matthieu Lemerre and Vincent David
CONFIGEN: A tool for management of configuration options

This paper introduces CONFIGEN, a tool that helps modularizing software. CONFIGEN allows the developer to select a set of elementary components for his software through an interactive interface. Configuration files for use by C/assembly code and Makefiles are then automatically generated, and we successfully used it as a helper tool for complex system software refactoring. CONFIGEN is based on propositional logic, and its implementation faces hard theoretical problems.

14:00‑15:00 Session 2
Location: IF 1.16
14:00 Andreas Kübler, Christoph Zengler and Wolfgang Küchlin
Model Counting in Product Configuration

We describe how to use propositional model counting for a quantitative analysis of product configuration data. Our approach computes valuable meta information such as the total number of valid configurations or the relative frequency of components. This information can be used to assess the severity of documentation errors or to measure documentation quality. As an application example we show how we apply these methods to product documentation formulas of the Mercedes-Benz line of vehicles. In order to process these large formulas we developed and implemented a new model counter for non-CNF formulas. Our model counter can process formulas, the CNF representations of which could not be processed up till now.

14:30 Roberto Di Cosmo and Ralf Treinen (Université Paris-Diderot)
Result of the MISC Competition

Outcome of the first international competition of solvers for package/component installation and upgrade problems organised by the <a href=www.mancoosi.org>Mancoosi project organises the . Instances of these problems are given by a set of currently installed or available software packages, with complex relations between them like dependencies, conflicts, and features. The problem instances used in the competition are expressed in a language called CUDF that allows to express relationships between components like they are known for instance in GNU/Linux distributions, or for Eclipse plugins. We are not only interested in finding some solution to such a problem, but in finding the best solution according to two different optimization criteria. Participating solvers will be judged by the correctness of the solution, the quality of the solution according to the respective optimization criteria, and speed. For further details please consult <a href=http://www.mancoosi.org/misc-2010/>http://www.mancoosi.org/misc-2010/</a>.