Jérôme Vouillon
email: jerome.vouillon@pps.jussieu.fr

Roberto Di Cosmo
email: roberto@dicosmo.org

On Software Component Co-Installability (extended version)

Modern software systems are built by composing components drawn from large repositories, whose size and complexity is increasing at a very fast pace. A fundamental challenge for the maintainability and the scalability of such software systems is the ability to quickly identify the components that can or cannot be installed together: this is the co-installability problem, which is related to boolean satisfiability and is known to be algorithmically hard. This paper develops a novel theoretical framework, based on formally certified. semantic preserving graph-theoretic transformations, that allows to associate to each concrete component repository a much smaller one with a simpler structure, but with equivalent co-installability properties. This smaller repository can be represented graphically, giving a concise view of the co-installability issues in the original repository, or used as a basis for various algorithms related to co-installability, like the efficient computation of strong conflicts between components. The proofs contained in this work have been machine checked in Coq.

INTRODUCTION

The mainstream adoption of free and open source software (FOSS) has widely popularised component-based software architectures, maintained in a distributed fashion and evolving at a very quick pace. Components are typically made available via a repository, and each of these components is equipped with metadata, such as dependencies and conflicts, used to specify concisely the contexts in which a component can or cannot be installed.

A typical example of the metadata attached to a component, taken from the Debian GNU/Linux distribution, is shown in Example 1: the logical language used for expressing dependencies and conflicts is quite powerful, as it allows conjunctions (symbol ','), disjunctions (symbol '|') and version constraints.

In most frameworks, determining whether a single component can be installed at all is already an NP-Complete problem, albeit the concrete instances arising in real-world systems, like GNU/Linux distributions, Eclipse plugins or OSGI component repositories, turn out to be tractable [START_REF] Mancinelli | Managing the complexity of large free and open source package-based software distributions[END_REF][START_REF] Tucker | Opium: Optimal package install/uninstall manager[END_REF]3]. For the maintenance of component repositories, though, more sophisticated analyses are required. This includes identifying for each component the other components in the repository that it absolutely needs [START_REF] Abate | Strong dependencies between software components[END_REF], and those that it can never be installed with [START_REF] Di Cosmo | Using strong conflicts to detect quality issues in component-based complex systems[END_REF].

More generally, a fundamental challenge for component based software maintainability is the study of the problem of co-installability of components, that involves identifying and visualising the relevant sets of components that can or cannot be installed together.

Indeed, from a maintenance point of view, one needs to identify which components cannot be installed together, in order to check whether these incompatibilities are justified or due to erroneous dependencies. The dependency graph is also too rich for end users, which are interested in having a given set of functionalities provided by some components (for instance, they want a word processor and a Web browser) but do not care about the additional components also installed. This is illustrated by the fact that some package managers keep track of these additional components and automatically remove them when they are no more needed.

The sheer size of current mainstream repositories, with tens of thousands of components and hundreds of thousands of relations, makes it completely unfeasible to study such properties of a repository directly: visualising such large graphs is both technically challenging, and of little interest, as one would need to follow recursively a large number of dependency and conflict relations to understand how components relate to one other. In this paper, we develop a novel theoretical framework, based on formally certified. semantic preserving graph-theoretic transformations, that allows to associate to each concrete component repository a much smaller repository with a simpler structure, but with equivalent co-installability properties. This smaller repository can be represented graphically, giving a concise view of the co-installability issues in the original repository, or used as a basis for various algorithms related to co-installability, like the efficient computation of the strong conflicts defined in [START_REF] Di Cosmo | Using strong conflicts to detect quality issues in component-based complex systems[END_REF].

We identified several bugs in the Debian distribution using the present work. For instance, the harden-servers package, meant to prevent the installation of unsafe packages, was in conflict with packages proftpd et sendmail but did not prevent the installation of the corresponding binaries which were in fact in packages proftpd-base et sendmailbin (the first two packages were actually transitional packages used to ease the upgrade from a previous release).

The paper is organised as follows: Section 2 recalls the basic notions about packages and dependencies, and overviews the repository transformation developed in the paper, which achieves impressive results on real-world GNU/Linux distributions (Section 3). The technical development follows: repositories are equipped with a partial order in Section 4, put into a flattened form in Sections 5, 6 and 7, simplified by removing irrelevant dependencies and conflicts in Section 8 and quotiented in Section 9. Finally, we show how to draw a simplified graph of the kernel of a repository in Section 11. We discuss related works, and conclude in Section 13.

OVERALL APPROACH

While the concrete details may vary from one technology to the other, the core metadata associated to component based systems always allows to express a few fundamental properties: a component, called package in the following, may depend on a combination of components, expressed as a conjunction of disjunctions of components, and a component may conflict with a combination of components, expressed as a conjunction of components.

Extra properties like provides (e.g. postfix-tls in Example 1), or versioned constraints (e.g. libc6 (>= 2.7) in Example 1) can be easily preprocessed out [START_REF] Mancinelli | Managing the complexity of large free and open source package-based software distributions[END_REF], so that one can focus on a core dependency system that contains a binary symmetric conflict relation, and a dependency function D(π) = {{π 1 1 , ..., π 1 n 1 }, ..., {π k 1 , ..., π k n k }} that is satisfied when for each i at least one of the π i j is installed. An example repository in this core dependency system is depicted in Figure 1, that also introduces the graphical notation used in the paper: package a has two dependencies, and can be installed only if, first, either package b or package c is installed, and second, package f is installed; package c conflicts with b and f : neither packages b and c, nor packages c and f , can be installed simultaneously; package d depends on package e, which in turn depends on both f and g.

Repositories

We follow the notations of earlier works [START_REF] Mancinelli | Managing the complexity of large free and open source package-based software distributions[END_REF][START_REF] Treinen | Solving package dependencies: from EDOS to Mancoosi[END_REF][START_REF] Di Cosmo | Report on formal mangement of software dependencies[END_REF][START_REF] Di Cosmo | Maintaining large software distributions: new challenges from the FOSS era[END_REF], that we recall here. A repository is a tuple R = (P , D, C ) where P is a finite set of packages, D : P → P(P(P )) is the dependency function (we write P(X) for the set of subsets of X), and C , a symmetric irreflexive relation over P , is the conflict relation. An installation I of a repository (P , D, C ) is a subset of P . An installation I is healthy when the following holds:

• abundance: every package has what it needs. Formally, for every package π ∈ I , and for every dependency d ∈ D(π), we have d ∩ I = ∅.

• peace: no two packages conflict, that is, C ∩(I ×I ) = ∅.

We call dependency a set of packages d included in D(π) for some package π ∈ P . One can give a logical interpretation of the dependency function and the conflict relation. The logical variables are the packages π ∈ P . A set of packages d ∈ P(P ) is interpreted as a disjunction:

d = π∈d π.
A set of set of packages D(π) ∈ P(P(P )) is interpreted as a conjunction:

D(π) = d∈D(π) d .
A dependency function D is then interpreted as the set of formulas of the shape:

π =⇒ D(π)
where π ranges over P , which can also be written:

π =⇒ 1≤i≤n 1≤j≤m i πi,j with D(π) = {di | 1 ≤ i ≤ n} and di = {πi,j | 1 ≤ j ≤ mi}.
A conflict relation C is interpreted as the set of formulas ¬π ∨ ¬π ′ for (π, π ′ ) ∈ C . A healthy installation is an assignment which simultaneously satisfies all these formulas.

Co-Installability

A package π is installable in a repository if it is included in a healthy installation I of this repository. A set of packages Π are co-installable in a repository if they are all included in some healthy installation I of the repository.

Checking co-installability has been shown equivalent to SAT by taking advantage of the logical interpretation of repositories [START_REF] Mancinelli | Managing the complexity of large free and open source package-based software distributions[END_REF]. However, our experience is that this problem is easy in practice: SAT-solver based tools are currently used routinely to identify non-installable components on repositories that contains dozens of thousands of packages, and hundreds of thousands of dependencies and conflicts.

Extracting a Co-Installability Kernel

Identifying all the sets of components that cannot be installed together is way more complex: even if we limit ourselves to the simplest case of sets of non co-installable components of size 2 (also known as strong conflicts), testing all possible pairs of packages is not a viable option, as the package number is in the tens of thousands. Even using all the optimisations described in [START_REF] Di Cosmo | Using strong conflicts to detect quality issues in component-based complex systems[END_REF], the computation takes almost a week on a modern workstation.

In the present work, we lay down the essential theoretical basis and algorithmic insight for tackling this non coinstallability problem: the fundamental idea is to extract from the component repository a kernel repository which is equivalent to the original one, as far as co-installability is concerned, but which turns out in practice to be orders of magnitude smaller, and easily manageable.

The key steps of our approach are now summarised. The effect of each step on the example repository of Figure 1 is shown in Figure 2.

Flattening.

The recursive nature of dependencies is convenient for package developers, as it allows them to describe the dependencies among the different packages very concisely, in a modular way. To study the properties of a repository, though, it is way more convenient to use only a special flattened form D of dependency functions that directly describes all dependencies of each package: if 1 1 , ..., π k 1 1 }, ...{π 1 n , ..., π kn n }}, then the packages π j i are all the packages relevant for installing package π, and only them.

D(π) = {{π
Any dependency function can be converted in this form by a sort of transitive closure that expands the dependencies of each intermediate package, and then converts the result again in a conjunction of disjunctions using distributivity: on our running example, this amounts to adding a dependency from d to f , and one from d to g (Figure 2b).

This transformation has some similarity with the conversion of logical formulae to conjunctive normal form, and is likewise subject to exponential blow-up (see for instance [START_REF] Buning | Propositional logic: Deduction and algorithms[END_REF]): the dependency function of the repository in Figure 3 has size 3n, and when expanded, gives rise to a repository whose dependency function has size 2 n . This is a strong limiting result, but we are only interested in studying co-installability of packages, so we need not fully maintain the logical equivalence of repositories. In particular, we can prune the expanded dependency function by removing any dependency containing a package with no conflicts without changing the co-installability property. In practice, this suffices to avoid the exponential blow-up. On our running example, this pruning phase removes the dependencies from d to e, from d to g and from e to g, leading to the repository of Figure 2c.

We take a further action to render the repository more homogeneous: we add a self dependency to each package with conflicts. This sort of reflexive closure will be very useful when quotienting the repository, in a later phase. (There is no point in adding self dependencies to other packages as they would be removed by pruning.) We then find it convenient to draw the repository using a two-level structure: on the top, we have all packages; on the bottom, we have packages with conflicts; dependencies connects the top layer to the bottom layer; conflicts are between packages on the bottom layer. On our running example, this leads to the repository of Figure 2d.

The three phases of expansion, pruning and addition of self dependencies can be performed in a single pass, and we thereafter use the term flattening to denote all of them.

Elimination of irrelevant dependencies and conflicts.

As a second phase, we identify several classes of dependencies and conflicts that are irrelevant as far as co-installability is concerned, and remove them. In Figure 4, we can see some interesting examples (more are given in Section 8), in all of which the disjunctive dependency connecting package a to packages b and c can be dropped:

(a) if some branches of a disjunction are forced by a stronger dependency, all other branches can be dropped;

(b) a package with no conflict can be added to any installation, so dependencies on such a package are always satisfiable and all disjunctive dependencies containing it can be simplified out (this is the pruning defined above);

(c) if a package has a disjunctive dependency containing a package (here, b) that conflicts only with other packages in this dependency (here, c), this dependency is always satisfiable and can be dropped: either a package con- In Figure 5, the conflict between packages a and b is implied by the conflict between packages c and d and can be dropped.

Proving the soundness of such simplifications is far from trivial: in general, one has to rely on a peculiar structure of the repository to justify that a dependency can be removed, but removing a dependency may modify this very structure. Therefore, a suitable invariant has to be found, that allows to remove most, if not all, irrelevant dependencies.

On our example repository, the disjunctive dependency from package a to packages b and c, corresponding to Figure 4c, can be removed, yielding the repository of Figure 2e.

Quotienting equivalent packages.

It is now quite evident looking at Figure 2e, that packages a, d, e and f are, as far as co-installability is concerned, really equivalent: they share the very same set of dependencies (notice that this fact is easily detectable on the graph thanks to the self dependency of package f introduced during the flattening phase).

As many packages in a repository share the same behaviour with respect to co-installability, it is useful to quotient the final repository, identifying these packages; this step contributes greatly in reducing the size of the repository, as can be seen on our running example in Figure 2f.

After removing self dependencies, one gets the final repository of Figure 2g, where it is now quite easy to see which package can be installed with which other package, and which package cannot.

EXPERIMENTAL RESULTS

The transformations described in this paper have been proven correct, and all the proofs have been certified in Coq [START_REF] Coq | The Coq Proof Assistant Reference Manual -Version V8[END_REF]. An OCaml program implementing these transformations has been run on several mainstream GNU/Linux distributions: Debian testing (full suite, amd64, snapshot taken August 22, 2010), Ubuntu 10.10 (main suite, x386) and Mandriva 2010.1 (main suite, x386). Running time were measured on a machine using a Intel Core 2 Duo Processor E6600 at 2.4GHz. The relevant statistics of the results are given on Table 1.

We can notice that the number of packages is greatly reduced: many packages share the same behaviour as far as co-installability is concerned, and the quotienting phase identifies them. In particular, many packages can always be installed, which is good news for the GNU/Linux distributions; they are thus mapped to a single equivalence class. The number of dependencies is reduced even more: many dependencies are not relevant to co-installability, and are removed by our transformations. The simplification shown in Figure 4c turns out to be essential; for example, in Debian, thousands of packages depend on debconf which depends on either debconf-i18n or debconf-english, these two last packages being mutually exclusive: removing the disjunctive dependency hugely reduces the size of the final repository.

As for conflicts, we notice that distributions contain only few of them, which explains that flattening is practical; most of them cannot be removed.

Finally, to each package p in a repository one can associate its cone, the set of packages that are reachable from p by following the dependency relations; the cone size of a package is typically quite large (Figure 6): two third of the packages have a cone of more than a hundred packages. On the other hand, after simplification, two third of the package equivalence classes have a cone of size one, meaning that they do not depend on any other package than themselves.

After simplification, the Ubuntu distribution fits on a letter size paper (see Figure 14 in Section 12) and can be easily inspected visually for errors. The corresponding graph for the Debian distribution is much larger, but it is our experience that it can still be displayed in a usable way with a suitable graph viewer: the visualisation of the Debian co-installability kernel can be tested online at http: //ocsigen.org/js_of_ocaml/graph/.

As a consequence of the small size of the kernel extracted from a repository, many analyses can be performed very quickly. For example, it is easy to compute on the coinstallability kernel of a repository the pairs of packages that can never be installed together, known as strong conflicts [START_REF] Di Cosmo | Using strong conflicts to detect quality issues in component-based complex systems[END_REF], which is the simplest case of co-installability. On the same data as [START_REF] Di Cosmo | Using strong conflicts to detect quality issues in component-based complex systems[END_REF], the computation takes a few seconds, instead of the several days reported there. This time is in fact included in the running times of Table 1 as we use this information when drawing the simplified repository to emphasise pack-

ORDERING REPOSITORIES

A large part of our work consists of finding constraints that can be removed while leaving co-installability invariant. We make the idea of removing constraints precise by defining a preorder on repositories.

We first define a preorder on dependency functions: D ⊑ D ′ iff for every package π, for every dependency d ∈ D(π), there exists a dependency d ′ ∈ D ′ (π) such that d ′ ⊆ d. As an example, the dependency function D of the repository shown in Figure 7a is subsumed by the dependency function D ′ of the repository shown in Figure 7b. This preorder corresponds exactly to the converse of logical implication: D ⊑ D ′ if and only if the formulas D ′ (π) =⇒ D(π) can be derived for all packages π ∈ P .

The preorder induces an equivalence relation over dependency functions, and a canonical representative of an equivalence class can be defined by taking the element which is point-wise the smallest. Given a dependency function D, its canonical representative can be explicitly defined as:

D ′ (π) = {d ∈ D(π) | ∀d ′ ∈ D(π), d ′ ⊆ d =⇒ d ′ = d}.
This provides a first way to simplify the dependency function (illustrated by Figure 4a), and our implementation aggressively put all dependencies in canonical form.

We can now define a preorder on repositories: (P , D, C ) ⊑ (P ′ , D ′ , C ′ ) if and only if:

P = P ′ , D ⊑ D ′ , C ⊆ C ′ .
Given two repositories related under this preorder, going from the right hand side one to the left hand side one consists in removing conflicts or relaxing dependencies, thus making it easier to install packages.

Theorem 2. When (P , D, C ) ⊑ (P ′ , D ′ , C ′ ), any healthy installation I of repository (P ′ , D ′ , C ′ ) is also a healthy installation of repository (P , D, C ).

(Proof p. )

FLATTENING DEPENDENCIES

The flattened form of a dependency function, whose intuition has been given in the introduction, is formally defined as follows; given a repository (P , D, C ), the flattened dependency function D is the smallest function (with respect to point-wise inclusion) such that:

Refl (π, π ′ ) ∈ C {π} ∈ D(π) Trans {π1, . . . , πn} ∈ D(π) d1 ∈ D(π1) . . . dn ∈ D(πn) 1≤i≤n di ∈ D(π)
As the above rules are monotonous, such a function D exists.

The rule Trans expands the intermediate dependencies of a package π and converts the result back into a conjunction of disjunctions; this rule silently drops circular dependencies: adding a dependency {π} ∈ D(π) has no effect on D(π).

The rule Refl is designed to capture precisely the two properties we have outlined informally in the introduction: on one hand, we want to keep in D(π) only dependencies on packages with at least a conflict (we prove in the next section that they are enough for keeping co-installability invariant); on the other hand, we want D(π) to contain explicitly all the packages that are needed to install package π (so, if π has a conflict, it will also be an explicit dependency of itself).

The application of the transformation on the repository of Figure 1 gives the following result (illustrated by Figure 2e):

D D a {{b, c}, {f }} {{b, c}, {f }} b ∅ {{b}} c ∅ {{c}} d {{e}} {{f }} e {{f }, {g}} {{f }} f ∅ {{f }} g ∅ ∅
Packages d, e and f now have the same dependencies, which reflects the intuition that they behave the same way as far as co-installability is concerned.

STRONGLY FLAT REPOSITORIES

A flattened repository satisfies two properties (Theorem 3 below): a reflexivity property (if a package has a conflict, then it depends on itself), and a transitivity property (dependencies are stable under composition). Co-installability in such repositories, that we call strongly flat, can be shown equivalent to a more convenient property, that we call weak co-installability (Theorem 4); this is instrumental to prove the key result of this section: a set of packages are coinstallable in a repository if and only if they are co-installable in the corresponding flattened repository (Theorem 6).

We define precisely these two properties and study repositories that satisfies them.

We define the composition D ; D ′ of two dependency functions over a set of packages P as the smallest function (with respect to point-wise inclusion) such that for every package π ∈ P , for every set {π1, . . . , πn} ∈ D(π), for every sets di ∈ D ′ (πi), we have 1≤i≤n di ∈ (D ; D ′ )(π).

To any conflict relation C , we associate a dependency function ∆C defined as follows:

∆C (π) = {{π}} if (π, π ′ ) ∈ C for some π ′ ∈ P ∅ otherwise A repository (P , D, C
) is strongly flat when the following conditions hold:

• reflexivity: ∆C ⊑ D (every package with conflict depends on itself);

• transitivity: D ; D ⊑ D (dependencies are closed under composition).

The flattening transformation produces strongly flat repositories. Intuitively, strongly flat repositories have a two level structure. Looking for instance at Figure 2e, we find all packages on the top layer, and typically only packages with conflicts (that we refer to as features in the following) at the bottom layer: thanks to transitivity, everything a package π may need to be installed is fully described by D(π), without recursive traversal of dependencies; and thanks to reflexivity, conflicts need only be considered on the image of D.

We can take advantage of this to define a more convenient way of capturing co-installability:

A configuration is a pair (I , F ) of a set I of packages and a set F of features; we say that it is healthy when the following conditions hold:

• abundance: every package has what it needs. Formally, for every package π ∈ I , and for every dependency d ∈ D(π), we have d ∩ F = ∅.

• peace: no two features conflict, that is,

C ∩(F ×F ) = ∅.
This is subtly different from the homonymous definitions regarding installations. Conflicts are only checked in F , and abundance only checked for packages in I w.r.t. F ; the sets F and I might as well be disjoint, here. A set of packages Π are weakly co-installable if there exists a set of features F ⊆ P such that the configuration (Π, F ) is healthy. In general, this is a weaker notion. In strongly flat repositories, though, the two notions are equivalent. Theorem 4. Any set of packages Π weakly co-installable in a strongly flat repository are also co-installable.

(Proof p. )
It is interesting to remark that the result of the flattening operation can be mathematically characterised as follows.

Lemma 5. The flattened dependency function D associated to a repository (P , D, C ) is the least dependency function D ′ (for preorder ⊑, and up to equivalence) such that:

• ∆C ⊑ D ′ • D ; D ′ ⊑ D ′ . (Proof p. )
The essential result of this section is that co-installability is left invariant by flattening. Theorem 6. Let (P , D, C ) be a repository. Let D be the corresponding flattened dependency function. Let Π be a set of packages. The following propositions are equivalent:

1. Π is co-installable in (P , D, C ); 2. Π is weakly co-installable in (P , D, C ); 3. Π is co-installable in (P , D, C ).
(Proof p. )

FLAT REPOSITORIES

In this section, we focus on a particular class ∇C ⊆ P(P ) of dependencies that can be safely removed (Theorem 11). Removing these dependencies may destroy the strongly flat structure of a repository, but we introduce the weaker notion of flat repository which is preserved (Theorem 11), and for which co-installability and weak co-installability still coincide (Theorem 10), thus enabling further simplifications introduced in Section 8.

We want to capture in the class ∇C a set of dependencies that have the following two key properties: always satisfiable any healthy configuration in the repository can be extended to satisfy these dependencies, so they are irrelevant for co-installability and we can remove them; formally, this means that if d ∈ ∇C , then for all F ∈ P(P ) maximal with respect to set inclusion such that C ∩ (F × F ) = ∅, we have d ∩ F = ∅; monotony a dependency which is in ∇C must still be always satisfiable even if we remove some conflicts from the repository; formally, if

C ′ ⊆ C , then ∇C ⊆ ∇ C ′ .
The monotony property is necessary, because in the next section we introduce further simplifications that remove redundant conflicts. We want to be sure that removing a conflict later on does not invalidate the decision taken here of removing a dependency, as illustrated in Figure 8: the disjunctive dependency on packages b and c can always be satisfied because the conflict between d and e prevents the simultaneous installation of d and e; but this dependency is not in ∇C since it is no longer satisfiable if the conflict between d and e is removed. This leads to the following: Definition 7. Given a repository (P , D, C ), the set ∇C is the largest set such that d ∈ ∇C if and only if, for all C ′ ⊆ C , for all F ∈ P(P ) maximal with respect to set inclusion such that C ′ ∩ (F × F ) = ∅, we have d ∩ F = ∅.

We can give a more explicit characterisation of the elements of ∇C : these are exactly the dependencies that contain at least a package having only internal conflicts, like in Figure 4c. Theorem 8. Let (P , D, C ) be a repository. The set ∇C is the set of dependencies d such that there exists a package π ∈ d such that, for all pairs (π, π ′ ) ∈ C , we have π ′ ∈ d.

(Proof p. )
Notice that, if a dependency d contains a package π with no conflict, then it is in ∇C ; so ∇C also contains the redundant dependencies shown in Figure 4b.

As we shall see, weak co-installability is left invariant by the transformation that removes the elements of set ∇C from a dependency function D of a strongly flat repository. But, in general, the strongly flat property is lost, so we need a weaker notion that is preserved by this simplification. We start by defining a coarser preorder on dependency functions that ignores dependencies in ∇C : Flat repositories have a series of good properties: they include strongly flat repositories, co-installability and weak co-installability still coincide, removing ∇C preserves flatness and keeps co-installability invariant. One can still reason on flat repositories, as far as coinstallability is concerned, as if their dependency function was transitive: just choose installations (I , F ) where F is maximal, and then any dependency obtained by composition is satisfied, even when it is not explicitly in the dependency function. (For strongly flat repositories, this holds for arbitrary sets F .)

D ≺C D ′ if

IRRELEVANT CONSTRAINTS

We review now several classes of dependencies and conflicts that are redundant and can be simplified out.

Clearly Irrelevant Dependencies

The results of the previous section let us remove the dependencies in ∇C from a flat repository while leaving weak co-installability invariant and keeping the repository flat.

Conflict Covered Dependencies

An example of another very interesting class of irrelevant dependencies is shown in Figure 9, where the dependency for package a can always be satisfied despite the conflict between packages e and f (we assume the other packages in this dependency also have conflicts, not explicited, so the dependency cannot be obviously removed): indeed, for this conflict to be relevant for the dependency, f needs to be installed; but if f is installed, at least one of packages c and d is installed as well, and thus the dependency is satisfied without needing to install e. This generalizes to the case where package e is in conflict with several packages with the same property as package f .

More formally, we say that a dependency d is conflict covered at π if it contains a package π such that for all (π, π ′ ) ∈ C , there exists a dependency d ′ ∈ D(π ′ ) such that d ′ ⊆ d \ {π}. Removing one such dependency leave co-installability invariant. Unfortunately, removing such dependencies may destroy the flatness of the repository, so we remove them one after another, in a greedy way, and only after checking that flatness is preserved by using the following result.

• d ⊆ {π}; • for all d ′ ∈ (D ′ ; D ′ )(π), we have d ⊆ d ′ . (Proof p. )
In practice, it can be simpler to get all possible dependencies d ′ above by taking all dependencies d ′′ ∈ D(π)\{d, {π}} and composing them with dependencies in D.

The graph reduction rule defined by this simplification has unsolvable critical pairs, so the result of this simplification could depend on the order of removal. In practice, though, we remove all instances present in the initial repository.

Redundant Conflicts

We consider some of the conflicts that can be removed from a repository while leaving co-installability invariant. A conflicting pair (π1, π ′ 1 ) ∈ C is redundant if there exists a dependency d ∈ D(π1) such that for all π2 ∈ d, there exists a package π ′ 2 such that:

• (π2, π ′ 2 ) ∈ C ; • {π1, π ′ 1 } = {π2, π ′ 2 }; • there exists d ′ ∈ D(π2) such that d ′ ⊆ {π ′ 2 }.
Redundant conflicts can be removed, but only one at a time: for example, if two conflicts are considered redundant thanks to the existence of one another, then removing both of them simultaneously is incorrect. Lemma 14. Let (P , D, C ) be a repository. Let (π1, π2) be a redundant conflict in this repository. Any healthy installation of repository (P , D, C \ {(π1, π2), (π2, π1)}) is healthy in repository (P , D, C ).

(Proof p. )
Removing redundant conflicts involves a trade off. On one side, it may allow to remove some additional dependencies; on the other, it can also break some interesting structures. In Figure 10, the conflict between b and c is redundant, but removing it breaks the clique a, b, c, which is useful when drawing a simplified graph.

Dependence on Conflicting Packages

A special configuration may surface in the repository during simplification when the initial repository contains broken packages, as depicted in Figure 11 be installed, and leaving such a configuration in the repository would pollute the graphical representation. In this case, we mark explicitly package a as broken by replacing its dependencies by the empty dependency ∅. All conflicts involving a can then be also removed, as they are redundant (Section 8.3). The transformation preserves healthiness.

Lemma 15. Let π be a package not installable in some repository (P , D, C ). Let D ′ be the dependency function that coincide with D for all packages but π and such that D ′ (π) = {∅}. Any healthy installation of repository (P , D, C ) is also healthy in repository (P , D ′ , C ).

(Proof p. )
The flatness of the repository may be destroyed, as some of the removed dependencies may be involved in transitivity. Thus, after applying such simplification, flattening should be performed again.

QUOTIENTING THE SET OF PACKAGES

In real-world repositories, many packages share the same behaviour as far as co-installability is concerned: for example, a lot of packages can always be installed, and some groups of packages only conflicts with a single other package.

In this section, we define an equivalence relation between packages, and show that the quotient w.r.t. this relation preserves all the good properties of a repository. We define two packages as equivalent in a repository (P , D, C ) if they have the same dependencies:

π ≡ π ′ if and only if D(π) = D(π ′ ).
We write [π] for the equivalence class of package π, and extend this definition to set of packages: [Π] = {[π] | π ∈ Π}. The quotient repository (P ′ , D ′ , C ′ ) of a repository (P , D, C ) is naturally defined as follows:

• P ′ is the set of all equivalence classes:

P ′ = P /≡ = {[π] | π ∈ P }; • the dependency function D ′ is such that D ′ ([π]) = {[d] | d ∈ D(π)} for all π ∈ P ;
• the conflict relation C ′ is defined by

C ′ = {([π], [π ′ ]) | (π, π ′ ) ∈ C }.
If the original repository does not contain dependencies of the form of Figure 11 nor redundant conflicts, then the quotient repository is indeed a repository (the key point to check is irreflexivity of the conflict relation). (Proof p. )

REFLEXIVE TRANSITIVE REDUCTION

It would not be suitable to graph directly a repository after flattening as it would be polluted by dependencies which are not informative: due to reflexivity, we have packages π where {π} ∈ D(π), and some dependencies can be deduced from others by transitivity. Thus, we perform a kind of reflexive transitive reduction of the dependency function: given a repository (P , D, C ), we find a minimal dependency function D ′ with the same flattening (that is, D = D ′ ).

Because of disjunctive dependencies, the complexity of finding an optimal solution is high [START_REF] Ausiello | Graph algorithms for functional dependency manipulation[END_REF][START_REF] Ausiello | Minimal representation of directed hypergraphs[END_REF], in constract with the case of reflexive transitive reduction for graphs. As this is mostly a cosmetic issue for us, we use a simple non-optimal algorithm. As a first step, we iteratively remove dependencies which are implied from other dependencies by transitivity, in a greedy way. The second step is to remove all self dependencies, that is, dependencies d ∈ D(π) such that π ∈ d. Co-installability is left invariant by these operations.

PUTTING ALL TOGETHER

We now have all the ingredients at hand to perform on any repository (P, D, C) the transformations that allow to produce the final repository, which is suitable both for drawing a simplified graph, or performing efficiently various analysis related to co-installability.

Extracting a Co-Installability Kernel

The complete algorithm is shown in Figure 12. We first flatten the initial repository (Section 5), canonise the dependency function (Section 4), and remove the clearly irrelevant ). In our implementation, all these operations are performed simultaneously: this is significantly more efficient, as we have less dependencies to consider while flattening. Then, we set the dependencies of broken packages of the form of Figure 11 to the empty dependency ∅ (Section 8.4), and we remove redundant conflicts (Section 8.3). As changing the dependencies of broken packages may break flatness and removing may grow ∇C , these fives steps are iterated until no change occurs. The process terminates as at each iteration either D(π) is set to {∅} for a package π or a conflict is removed. In practice, only two iterations are performed: more iterations are only needed in unlikely configurations where dealing with a broken package exposes another package as broken. Finally, we remove the conflict covered dependencies that can be safely dropped (Section 8.2) and the repository is quotiented (Section 9). By combining the results of the previous sections, we obtain the fundamental result on the simplification performed by the algorithm.

Theorem 21. The transformation performed by the simplification algorithm leaves co-installability invariant. This algorithm produces a flat repository.

(Proof p. )

As noticed above, on a repository with no broken package, it is not necessary to iterate the flattening phase, so the algorithm could run slighly faster; but finding all broken packages is slower than performing the whole simplification, as it requires to call a SAT solver repeatedly on large problems. On the other hand, repositories with good quality control should contain no broken packages, and a simpler version of the simplification algorithm could be used on them.

Drawing a Simplified Graph

Before drawing the final repository, we perform the transitive reflexive reduction of Section 10. The structure of the graph is then passed as input to the dot program of the Graphviz toolkit [START_REF] Ellson | Graphviz -open source graph drawing tools[END_REF] that performs the layout.

It is important to name nodes using meaningful representatives of each equivalence class: we give preference to packages π that are directly involved in conflicts, as they have more chances to be relevant for the repository maintainers; these are easy to find by checking if {π} ∈ D(π).

There can be many packages all mutually in conflict. For instance, this is the case of all mailer agents in Debian. We identify maximal such cliques and draw them in a more concise way, as shown in Figure 13.

We compute strong conflicts [START_REF] Di Cosmo | Using strong conflicts to detect quality issues in component-based complex systems[END_REF] (non-coinstallable pairs of packages) and use this information to emphasise packages that prevent the installation of many other packages.

VISUALIZING UBUNTU

In Figure 14 we can see the result of applying the simplifications described in this paper to the main section of release 10.10 of the Ubuntu GNU/Linux distribution; solid arrows indicate dependencies, dotted lines indicate conflicts, and conflict cliques are represented with a node containing a # connected with dotted lines to all packages in the clique. Of the thousands of packages, and dozens of thousands of relationships, only a handful are left, and it is possible to read interesting information directly on the graph.

We give here just a couple of examples. The isolated node in the middle left stands for 7049 packages that are always installable. The five conflict cliques are justified, as they all correspond to incompatible implementations of libraries which are compiled with different backends. One can see that package libjpeg8-dev is in conflict with 28 other packages, which is likely to make it unconvenient to use. The core package ubuntu-desktop is in conflict with a number of packages. These packages should either be removed from the main section, or the dependencies should be revised. For instance, packages foomatic-db and libgd2noxpm should probably be removed. On the other hand, package libsdl1.2debian-all provides a superset of the functionalities of libsdl1.2debian-pulseaudio. Thus, it should not be in conflict with ubuntu-desktop. Overall, there are few issues with this repository. Our tool is most useful for detecting issues proactively when the distribution is in flux (during alpha and beta stages).

RELATED AND FUTURE WORK

Many relevant research issues stem from the concrete and widespread applications of software component repositories: identifying components that can never be installable has been shown NP-complete, but tractable in practice [START_REF] Mancinelli | Managing the complexity of large free and open source package-based software distributions[END_REF], and there is currently very active research on computing installations that optimise some given objective functions, organised around the Mancoosi International Solver Competition (http://www.mancoosi.org/misc-2010/); determining what other components a package will always need [START_REF] Abate | Strong dependencies between software components[END_REF] and what pairs of packages are incompatible [START_REF] Di Cosmo | Using strong conflicts to detect quality issues in component-based complex systems[END_REF] have been shown to be relevant for quality assurance in package repositories; finally, since feature diagrams, used in software product lines, can be encoded as component repositories [START_REF] Leipert | Feature diagrams as package dependencies[END_REF], all the problems related to configuration management can be equivalently stated in terms of repositories.

Connections between component repositories and boolean satisfiability and constraint solving have been made only a few years ago in the framework of GNU/Linux distributions [START_REF] Mancinelli | Managing the complexity of large free and open source package-based software distributions[END_REF][START_REF] Tucker | Opium: Optimal package install/uninstall manager[END_REF] and the Eclipse platform [3], but these connections, and other recent developments such as [START_REF] Abate | Strong dependencies between software components[END_REF][START_REF] Di Cosmo | Using strong conflicts to detect quality issues in component-based complex systems[END_REF] do not exploit the special structure of the dependencies and conflicts found in a repository.

The underlying structure of software component repositories exposed here can also be seen as a generalisation of some known mathematical structures : prime event structure [START_REF] Winskel | Event structures[END_REF] correspond to repositories without loops and disjunctions; directed hypergraphs [START_REF] Ausiello | Graph algorithms for functional dependency manipulation[END_REF] correspond to repositories without conflict arcs, and Dual Horn theories correspond to repositories with conflicts [START_REF] Dowling | Linear-time algorithms for testing the satisfiability of propositional horn formulae[END_REF]. In this paper, we have developed a theory and algorithms to extract from a repository a co-installability kernel, which can be seen as a minimal representation of the dependency and conflict relations: despite the apparent simplicity of the definition of the problem, and the intuitive appealing of the hypergraph transformations we have developed, the proofs of the crucial properties turned out to be surprisingly complex, so we decided to machine check them using Coq [START_REF] Coq | The Coq Proof Assistant Reference Manual -Version V8[END_REF], and a long version of this paper containing all the proofs is available online as http://www.dicosmo.org/Papers/coinstallability.pdf.

The results presented here pave the way to attacking significantly more complex problems concerning software component repositories. More generally, we believe this work clearly shows the interest of the mathematical objects underlying software repositories, which turn out to be amenable to an elegant formal treatment and of high practical interest.

Artifact evaluation: the tool coinst implemeting the analysis described in this article has been evaluated by the ESEC/FSE Artifact Evaluation Committee, and it has be found to exceed expectations.

Figure 1 :

 1 Figure 1: Graphical depiction of a repository

Figure 2 :

 2 Figure 2: Transformations of a repository (added dependencies are in bold, dotted ones are removed in the next phase)

Figure 3 :

 3 Figure 3: Repository that blows-up when flattened

Figure 5 :

 5 Figure 4: Some irrelevant dependencies a b c d #

Figure 6 :

 6 Figure 6: Distribution of cone size (Debian testing)

Figure 7 :

 7 Figure 7: An example of dependency functions related by the preorder

Theorem 3 .

 3 Let (P , D, C ) be a repository. Let D be the corresponding flattened dependency function. The repository (P , D, C ) is strongly flat. (Proof p. )

Figure 8 :

 8 Figure 8: Illustration of monotony requirement

  and only if for every package π, for every dependency d ∈ D(π), either d ∈ ∇C or there exists a dependency d ′ ∈ D ′ (π) such that d ′ ⊆ d. A repository (P , D, C ) is flat when it satisfies the following properties: • reflexivity: ∆C ≺C D; • transitivity: D ; D ≺C D.

Lemma 9 .

 9 Any strongly flat repository is flat. (Proof p. ) Theorem 10. Any set of packages Π weakly co-installable in a flat repository are co-installable in this repository. (Proof p. ) Theorem 11. Let (P , D, C ) be a flat repository and D ′ be the dependency function such that D ′ (π) = D(π) \ ∇C for all π ∈ P . The repository (P , D ′ , C ) is flat, and coinstallability is left invariant by this transformation. (Proof p. )

Lemma 12 .

 12 Let (P , D, C ) be a flat repository, d be a conflict covered dependency, and D ′ be the dependency function obtained by removing d from D. Any set of packages weakly co-installable in (P , D ′ , C ) is weakly co-installable in (P , D, C ).

  Figure 9: Dependency covered by the conflict requirements.

Lemma 13 .

 13 Let (P , D, C ) be a flat repository. Let π ∈ P and d ∈ D. Let D ′ be the dependency function D where the dependency d of package π has been removed. If the following two conditions hold, then (P , D ′ , C ) is flat.

Figure 11 :

 11 Figure 11: Dependence on conflicting package

Lemma 16 .

 16 Let (P , D, C ) be a flat repository such that, for all π ∈ P and for all d ∈ D(π), if d ⊆ {π ′ } for some π ′ ∈ P , then (π, π ′ ) ∈ C . Its quotient is indeed a repository.

(Figure 12 :

 12 Figure 12: Simplifying the repository.

Lemma 19 .

 19 Let (P , D, C ) be a repository. Let π ∈ P be a package and d ∈ D(π) be a dependency of this package. Let D ′ = D \ {π → d} be the dependency function D where the dependency has been removed. If d ∈ (D ′ ; D ′ )(π) then any healthy installation I of repository (P , D ′ , C ) is a healthy installation of repository (P , D, C ). (Proof p. ) Lemma 20. Let (P , D, C ) be a repository. Let D ′ be the dependency function defined by D ′ (π) = {d ∈ D | π ∈ d}. Any healthy installation I of repository (P , D ′ , C ) is also a healthy installation of repository (P , D, C ).

(

  Proof p. )

Figure 13 :

 13 Figure 13: Conflict clique

Figure 14 :

 14 Figure 14: Output graph for Ubuntu 10.10 (main)

Table 1 :

 1 Repository sizes

					Debian	Ubuntu	Mandriva
					before	after	before	after	before	after
	Packages			28919	1038	7277	100	7601	84
	Dependencies		124246	619	31069	29	38599	8
	Conflicts			1146	985	82	60	78	62
	Median cone size	38	1	38	1	59	1
	Avg. cone size		66	1.7	84	1.3	153	1.1
	Max. cone size	1134	15	842	4	1016	5
	Running time (s)		10.6		1.19	11.6
	Cone size	100 150 200 300 250 50 0	0	10000 Package count 20000

Debian GNU/Linux distribution (http: // www. debian. org

APPENDIX

This appendix contains all the proofs of the lemmas and theorems stated in the body of the article, as well as some auxiliary lemmas which are needed in the proofs. Auxiliary material appearing only in the appendix has numbers that are higher than in the paper, and appear hence out of order: this is necessary to avoid disrupting the numbering of lemmas and theorems in the body of the article.

A. PROOF OF THE MAIN RESULTS

Remark 22. Let (P , D, C ) and (P ′ , D ′ , C ′ ) be two repositories. If any healthy installation I of repository (P , D, C ) is a healthy installation of repository (P ′ , D ′ , C ′ ), then any co-installable set of packages Π in repository (P , D, C ) is a co-installable set of packages in repository (P ′ , D ′ , C ′ ).

Proof: Immediate ✷

The preorder ⊑ is coarser than point-wise inclusion:

Remark 23. If, for all π ∈ P , D(π) ⊆ D ′ (π), then D ⊑ D ′ .

We write ∼ for the equivalence relation associated to the relation ⊑.

Proof of Theorem 2

We suppose that I is a healthy installation of (P ′ , D ′ , C ′ ) and prove that I is a healthy installation of (P , D, C ).

We first prove abundance. Let π ∈ I and d ∈ D(π). As D ⊑ D ′ , there exists d ′ ∈ D ′ (π) such that d ′ ⊆ d. As I is a healthy installation of (P ′ , D ′ , C ′ ), by abundance, d ′ ∩I = ∅. Hence, d ∩ I = ∅ as wanted.

We now prove peace. As I is a healthy installation of (P ′ , D ′ , C ′ ), we have C ′ ∩ (I × I ) = ∅. On the other hand, C ⊆ C ′ . Hence, C ∩ (I × I ) = ∅ as wanted.

Proof of Theorem 3

Reflexivity, that is ∆C ⊑ D, is a direct consequence of rule Refl.

We now show transitivity, that is D ; D ⊑ D. Let π ∈ P and d ∈ ( D ; D)(π). By definition of composition, there exists d ′ = {π1, . . . , πn} ∈ D(π) and sets di ∈ D(πi) such that d = 1≤i≤n di. We need to show that there exists

The proof is by induction on a derivation of d ′ ∈ D(π). We have two cases.

• Case Refl. There exists π ′ ∈ P such that (π, π ′ ) ∈ C , and d ′ = {π}. We have, d = d1 ∈ D(π1) = D(π), hence we can take d ′′ = d.

• Case Trans. There exists a set {π ′ 1 , . . . π ′ m } ∈ D(π) and sets d ′ j ∈ D(π ′ j ) such that d ′ = 1≤j≤m d ′ j . Besides, by induction hypothesis, for all j, if one can find packages π k j and dependencies d k j such that d ′ j = {π 1 j , . . . , π p j j }, and d k j ∈ D(π k j ), then there exists d ′′ j ∈ D(π ′ j ) such that d ′′ j ⊆ 1≤k≤p j d k j . We have d ′ j ⊆ d ′ . Hence we can choose for each indices j and k an index i such that π k j = πi. Then, we take d k j = di. We therefore have dependencies

But, as d ′ = 1≤j≤m di, the packages π k j ranges over all the distinct packages πi. Hence, the dependencies d k j ranges over all dependencies di, and we have d ′′ ⊆ 1≤i≤n di as wanted. ✷

Remark 24. The two following properties hold:

• an installation I is healthy iff the configuration (I , I ) is healthy;

If a set of packages Π are co-installable, then they are also weakly co-installable. Proof: Suppose the set of packages Π are co-installable. By definition, there exists a healthy installation F such that Π ⊆ F . We terminate the proof by using in turn both properties in Remark 24. The configuration (F , F ) is healthy. Hence, by anti-monotony of the definition of healthiness, (Π, F ) is healthy. ✷

We present here two technical lemmas needed in the proof of Theorem 6.

Lemma 26. Let (P , D, C ) be a repository such that ∆C ⊑ D. Let (I , F ) be a healthy configuration. For every package Proof: We consider a set of packages Π which are weakly co-installable in (P , D ′ , C ). This means that there exists a set of packages F such that the configuration (Π, F ) is healthy in (P , D ′ , C ). We then consider a maximal set of packages I such that Π ⊆ I and the configuration (I , F ) is healthy in (P , D ′ , C ). We can conclude if we prove that I is healthy in (P , D, C ).

We first prove abundance. We take π ∈ I and d = {π1, . . . , πn} ∈ D(π) and need to prove that d ∩ I = ∅. We want to show that we can find π ′′ ∈ d such that (I ∪{π ′′ }, F ), is healthy. Indeed, then, by maximality of I , we have π ′′ ∈ I . Hence, d ∩ I = ∅ as wanted. The package π ′′ should be such that, for all d ′′ ∈ D(π ′′ ), we have d ′′ ∩F = ∅. The proof is by contradiction. Suppose that for all i, there exists di

This contradicts the fact that π ∈ I and (I , F ) is healthy. Hence the existence of a suitable package π ′′ which allow us to finish the proof of abundance.

We now prove peace by contradiction. Suppose that C ∩ (I × I ) = ∅, that is, there exists π ∈ I and π ′ ∈ I such that (π, π ′ ) ∈ C . As (I , F ) is healthy, we have π ∈ F and π ′ ∈ F by Lemma 26, and then (π, π ′ ) ∈ C by peace. We reach a contradiction, hence C ∩ (I × I ) = ∅. ✷

Proof of Theorem 4

This is an immediate consequence of Lemma 27, taking D = D ′ .

Proof of Lemma 5

Clearly, the flattened dependency function satisfies these equations. Let D ′ be another dependency function satisfying the equations. We want to prove that, for all π ∈ P , D(π) ⊑ D ′ (π). By unfolding the definition of the preorder, this can be rephrased as: for all π ∈ P , for all d ∈ D(π), there exists 2) implies (1) by Lemmas 27 and 5. We now assume (1) and prove (3). By definition, there exists a healthy installation I of repository (P , D, C ) such that Π ⊆ I . We can just show that I is also a healthy installation of repository (P , D, C ). Peace is immediate. We prove abundance. We consider π ∈ P and d ∈ D(π). We need to show that if π ∈ I , then d ∩ I = ∅. The proof is by induction on a derivation of d ∈ D(π). We have two cases.

• Case Refl. We have d = {π}. Hence, if π ∈ I then d ∩ I = {π} = ∅.

• Case Trans. We have {π1, . . . , πn} ∈ D(π) and d = 1≤i≤n di where di ∈ D(πi) and, if πi ∈ I , then di∩I = ∅ (induction hypothesis). Let us assume π ∈ I . By abundance, as {π1, . . . , πn} ∈ D(π), there must exists some i such that πi ∈ I . Then, di ∩ I = ∅, and thus d ∩ I = ∅. ✷

Proof of Theorem 8

We first assume that there exists no package π ∈ d such that, for all pairs (π, π ′ ) ∈ C , we have π ′ ∈ d. We show that then d ∈ ∇C . Let C ′ be the set of conflicts in C that cross d:

Clearly, this is a conflict relation (it is symmetric and irreflexive). We consider the set of features

If we can now prove that the set F is a maximal set satisfying this property, we can conclude. Indeed, then, as d ∩ F = ∅, the set d is not in ∇C . We consider a strictly larger set of features F ′ and show that it does not satisfies the property. The set F ′ must contain at least a package π in dependency d. But then, by assumption, there exists π

We now assume that there exists a package π ∈ d such that, for all pairs (π, We write ≈ for the associated equivalence relation.

Remark 29. The following implications hold:

Proof: Immediate. ✷

Proof of Lemma 9

This is a direct consequence of Remark 29.

by Remark 29. On the other hand, we have C ′ ⊆ C . Hence, for all π ∈ P , we have ∆ C ′ (π) ⊆ ∆C (π). Thus, ∆ C ′ ⊑ ∆C by Remark 23, and finally ∆ C ′ ≺ C ′ ∆C by Remark 29. We conclude by transitivity of ≺ C ′ .

We now show transitivity, that is,

Similarly, for all i, there exists di ∈ D(πi) such that di ⊆ d ′ i . By transitivity in (P , D, C ), either 1≤i≤n di ∈ ∇C or there exists d 1 ∈ D(π 0 ) such that d 1 ⊆ 1≤i≤n di. In the first case, we have 1≤i≤n di ⊆ 1≤i≤n d ′ i = d 0 . Then, as ∇C is upward-closed (Remark 28) and C ′ ⊆ C , we have d 0 ∈ ∇C ⊆ ∇ C ′ as wanted. In the second case, we have

This is what we wanted to prove. Otherwise, we have

Proof of Theorem 10

The proof follow the proof of Lemma 10, with minor modifications. Let (P , D, C ) be a flat repository. Let Π be a set of packages weakly co-installable in (P , D, C ). There exists a set of packages F such that the configuration (Π, F ) is healthy in (P , D, C ). We assume that F is a maximal set of packages satisfying this property. We then consider a maximal set of packages I such that Π ⊆ I and the configuration (I , F ) is healthy in (P , D, C ). We can conclude if we prove that I is healthy in (P , D, C ).

We first prove abundance. We take π ∈ I and d = {π1, . . . , πn} ∈ D(π) and need to prove that d ∩ I = ∅. We want to show that we can find π ′′ ∈ d such that (I ∪{π ′′ }, F ), is healthy. Indeed, then, by maximality of I , we have π ′′ ∈ I . Hence, d ∩ I = ∅ as wanted. The package π ′′ should be such that, for all d ′′ ∈ D(π ′′ ), we have d ′′ ∩ F = ∅. The proof is by contradiction. Suppose that for all i, there exists di ∈ D(πi) such that di ∩ F = ∅. As D ; D ≺C D, either 1≤i≤n di ∈ ∇C or there exists d ′ ∈ D(π) such that d ′ ⊆ 1≤i≤n di. In the first case, by maximality of F and definition of ∇C , ( 1≤i≤n di) ∩ F = ∅. This contradicts the assumption that di ∩ F = ∅ for all i. In the second case, we have d ′ ∩ F ⊆ 1≤i≤n di = ∅. This contradicts the fact that π ∈ I and (I , F ) is healthy. Hence the existence of a suitable package π ′′ which allow us to finish the proof of abundance.

We now prove peace by contradiction. Suppose that C ∩ (I × I ) = ∅, that is, there exists π ∈ I and π ′ ∈ I such that (π, π ′ ) ∈ C . As (I , F ) is healthy, we have π ∈ F and π ′ ∈ F by Lemma 26, and then (π, π ′ ) ∈ C by peace. We reach a contradiction, hence C ∩ (I × I ) = ∅.

Lemma 32. If (P , D, C ) ≺ (P ′ , D ′ , C ′ ), then any set of packages Π weakly co-installable in repository (P ′ , D ′ , C ′ ) is weakly co-installable in repository (P , D, C ).

Proof: We assume that (P , D, C ) ≺ (P ′ , D ′ , C ′ ) and that the set of packages Π is weakly co-installable in (P ′ , D ′ , C ′ ). There exists a set of packages F such that (Π, F ) is a healthy configuration in (P ′ , D ′ , C ′ ). In particular, we have

There exists thus a set of packages

Proof of Theorem 11

Flatness is a consequence of Lemmas 31 and 33. Invariance is a consequence of Theorem 10, and Lemmas 32 and 33.

The following technical lemma is a crucial tool for reasoning on flat repositories. It states that a stronger form of transitivity where dependencies are not fully composed holds for flat repositories.

Lemma 34. Let (P , D, C ) be a flat repository, π ∈ P , d ∈ D(π). Let Π = {π1, . . . , πn} be a subset of d. We assume that, for all i, there exists di ∈ D(πi). Then, there exists

Proof: Suppose that there exists π ′ ∈ d \ Π such that {π ′ } ∈ ∇C (that is, by Theorem 8, package π ′ conflicts with no package). Then we can take d ′ = {π ′ } and conclude. Thus, we can assume that, for all π ′ ∈ d \ Π, there exists π ′′ ∈ P such that (π ′ , π ′′ ) ∈ C .

We show that for all π ′ ∈ d we can find Let π ′ ∈ d. If π ′ = πi for some i, we can take d ′ = di. Otherwise, π ′ ∈ d \ Π. We have assumed that there exists π ′′ such that (π ′ , π ′′ ) ∈ C . By Remark 30, there exists In the following, we will write D \ {π → d} for the dependency function D where the dependency d of package π has been removed. Formally,

Proof of Lemma 12

Let d0 ∈ D(π0) be one of these dependencies. There exists π1 ∈ d0 such that for all (π1, π) ∈ C , there exists a dependency d ∈ D(π) such that d ⊆ d0 \ {π1}. Let D ′ = D \ {π0 → d0} be the dependency function with this dependency removed. Let Π be a weakly co-installable set of packages in the repository (P , D ′ , C ). There exists a set of features F such that (Π, F ) is a healthy configuration of (P , D ′ , C ). We consider a maximal such a set F (with respect to inclusion). Clearly, the set F is then maximal such that C ∩ (F × F ) = ∅. If d0 ∩ F = ∅, then (Π, F ) is a healthy configuration of (P , D, C ) as well, as wanted. We now consider the case where d0 ∩ F = ∅. Let

We show that (Π, F ′ ) is a healthy configuration of (P , D, C ). Peace is clear. We need to show abundance. Let π ∈ I and d ∈ D(π). We want to show that d∩F ′ = ∅. If π1 ∈ d, this is the case. We can thus assume that π1 ∈ d. In particular, this means that d = d0, and therefore, by abundance, d ∩ F = ∅. The remainder of the proof is by contradiction. We assume that d ∩ F ′ = ∅. We consider the packages π i such that d ∩ F = {π 1 , . . . π n }. We have π i ∈ F \ F ′ . Thus, for all i, we have (π1, π i ) ∈ C , and therefore, by assumption, there exists

From this, on the one hand, as π1 ∈ d, we can see that π1 ∈ d ′ , and therefore d ′ = d. Hence, d ′ ∈ D ′ (π) ∪ ∇C . By abundance and maximality of F , we get

We reach a contraction, which completes the proof.

Proof of Lemma 13

We first prove reflexivity, that is, ∆C ≺C D ′ . Let π ′ ∈ P and d ′ ∈ ∆C (π ′ ). We show that either d ′ ∈ ∇C , or there exists

Proof of Lemma 14

Let Π be a healthy set of packages of repository (P , D, C \ {(π1, π2), (π2, π1)}). We show that it is healthy in repository (P , D, C ). Abundance is clear. We prove peace, that is, C ∩ (Π×Π) = ∅. We have by hypothesis (C \{(π1, π2), (π2, π1)}))∩ (Π×Π) = ∅. Thus, we can conclude if packages π1 and π2 are not both in Π. The proof is by contradiction: we assume the packages are in Π and reach a contradiction. By abundance in the initial repository, for all a dependency d ∈ D(π1), there exists a package π ′ 1 ∈ d ∩ Π. Then, by definition of redundant conflicts, there exists a dependency d1 ∈ D(π1),

Π. This contradicts peace in the initial repository. Hence the result.

Proof of Lemma 15

Let I be an healthy installation of repository (P , D, C ). We show that it is an healthy installation of repository (P , D ′ , C ). Clearly, peace is satisfied and abundance is satisfied for all packages distinct from π. We now show abundance for package π. As D ′ (π) = ∅, this reduces to showing that π ∈ I . This is indeed the case as π is not installable in the initial repository.

Proof of Lemma 16

Let (P ′ , D ′ , C ′ ) be the tentative quotiented repository associated to repository (P , D, C ), as defined above. The result is clear, except for irreflexivity of C ′ , which we show below. We assume that (π ′ , π ′ ) ∈ C ′ for some package π ′ ∈ P ′ and reach a contradiction. By definition of C ′ , there exists π1 ∈ P and π2 ∈ P such that π ′ = [π1] = [π2] and (π1, π2) ∈ C . By Remark 30, there exists a dependency d ∈ D(π2) such that d ⊆ {π2}. By definition of quotienting, D(π1) = D(π2), and thus d ∈ D(π1). But then, by hypothesis, we should have (π1, π2) ∈ C . Hence a contradiction, as wanted.

Remark 36. Let (P , D, C ) be a repository. Let (I , F ) be a healthy configuration of repository (P , D, C ). We assume that the set F is a maximal set (with respect to inclusion) satisfying this property. Then, for all packages π in P \ F , there exists a package π ′ such that (π, π ′ ) ∈ C .

Proof: We have {π} ∈ ∇C . Indeed, otherwise, we would have, by definition, {π} ∩ F = ∅, and thus π ∈ F . Then, by Theorem 8, there exists π ′ such that (π, π ′ ) ∈ C . ✷ Lemma 37. Let (P , D, C ) be a flat repository. Let (I , F ) be a healthy configuration of repository (P , D, C ). We assume that the set F is a maximal set (with respect to inclusion) satisfying this property. Let π ∈ P \ F . Let π ′ ∈ P such that D(π ′ ) = D(π) (in other words, π ′ ∈ [π]). Then, there exists d ∈ D(π ′ ) such that d ⊆ {π}.

Proof: By Remark 36, there exists π ′′ such that (π, π ′′ ) ∈ C . By Remark 30, there exists d ∈ D(π) such that d ⊆ {π}. We have D(π ′ ) = D(π ′ ), hence the result. ✷ Lemma 38. Let (P , D, C ) be a repository. Let (P ′ , D ′ , C ′ ) be the corresponding quotient repository. Let (I , F ) be a healthy configuration of repository (P , D, C ). We assume that the set F is a maximal set (with respect to inclusion) satisfying this property. Then ([I ], [F ]) is a healthy configuration of repository (P ′ , D ′ , C ′ ). (We write F for the complement P \ F of set F .) Otherwise, for all package π ∈ d0 ∩ F , there exists a package π ′ ∈ [π] \ F . By Lemma 37, there also exists a dependency d ∈ D(π) such that d ⊆ {π ′ }, and therefore d ∩ F = ∅. We can apply Lemma 34 to compose d0 with all these dependencies. Hence, there exists d ′ ∈ D(π0) ∪ ∇C such that d ′ ∩ F = ∅. But by abundance and maximality of F , we should have d ′ ∩ F = ∅. We reach a contradiction. Hence, this second case is actually not possible.

We now show peace. The proof is by contradiction. Suppose that peace does not hold. Then, there exists π

Proof of Theorem 17

This is a direct consequence of Lemmas 38 and 39.

Proof of Theorem 18

Let (P , D, C ) be a flat repository. We show that its quotient repository (P ′ , D ′ , C ′ ) is also flat. We first prove reflexivity, that is, ∆C ≺C D ′ . It is sufficient to prove that ∆C ⊑ D ′ . Let π1, π2 ∈ P such that ([π1], [π2]) ∈ C ′ . We need to prove that there exists a dependency

We now prove transitivity, that is,

Let di be dependencies such that

C (where ∇ ′ C is our class of always satisfiable dependencies for the quotiented repository) or there exists

Proof of Lemma 19

Let I be a healthy installation of (P , D ′ , C ). We show that it is a healthy installation of (P , D, C ). Peace is clear. We prove abundance.

Let

Proof of Lemma 20

Let I be a healthy installation of (P , D ′ , C ). We show that it is a healthy installation of (P , D, C ). Peace is clear. We prove abundance.

Let π ∈ I and d ∈ D(π). We need to show that d ∩ I = ∅. If π ∈ d, this is the case. Otherwise, d ∈ D ′ (π), and we can conclude by healthiness of I in (P , D ′ , C ).

Proof of Theorem 21

First, the quotienting operation performed at the end indeed produces a repository, as the hypothesis of Lemma 16 are satisfied: if ∅ ∈ D(π), then package π has no conflicts thanks to redundant conflict removal; if {π ′ } ∈ D(π), then (π, π ′ ) ∈ C thanks to the dependency strengthening of clearly broken packages. These two properties are preserved by dependency removal.

We now show that once the loop in Figure 12 is exited, the repository remains flat. Indeed, flattening produces a flat repository (Theorem 3 and Lemma 9), which remains flat by canonisation and removal of dependencies in ∇C (Remark 29, Lemmas 31 and 33). Then, the removal of conflict cover dependencies is defined so as to preserve flatness, and quotienting preserves flatness (Lemma 18).

To show that co-installability is left invariant, we rely heavily on the equivalence between co-installability and weak co-installability in flat repositories (Lemma 25 and Theorem 10), which let us use weak co-installability preservation results to prove co-installability preservation. We also use the fact that healthiness preservation implies coinstallability preservation (Remark 22). Then, co-installability is left invariant by flattening (Theorem 6), canonisation (Theorem 2), removal of dependencies in ∇C (Theorem 11), de-pendency strengthening of clearly broken packages (Lemma 15 and Theorem 2), removal of redundant conflicts (Lemma 14 and Theorem 2), removal of conflict covered dependencies (Lemma 12) and Theorem 2), and quotienting (Theorem 17).