SATisfaction

During pkg(5) development it has become quite clear that computing the correct set of packages to install or upgrade is a non-trivial task.  Initially, we started delivering pkg(5) with a solution engine that simply took the latest available packages.  This worked so long as we only delivered packages that were all compatible, no third party publishers existed, and users were happy staying on the bleeding edge.

Since none of these conditions were maintainable, a more sophisticated solution was essential.

 We gained some breathing room with the introduction of incorporation dependencies.  Such a dependency in a package specifies the version (at a variable level of precision) of compatibility with another package.   We have used a package full of these dependencies (termed an incorporation ) during OpenSolaris development to insure that the various operating system packages from pkg.opensolaris.org  come from the same build - that there's no way to get build 123's drivers, but build 127's IP stack.  In effect these packages define surfaces of compatible package versions, and allow package maintainers to refactor their packages, exchange content, etc. without the need for dependencies at the package level that would prevent incompatible packages from appearing on the same system.  The use of incorporations has allowed us to continue OpenSolaris development with a solver that first applied all constraints imposed by installed incorporations, and then attempted to install the latest possible packages. 

As we anticipated, however, the existing solver's deficiencies have become steadily more limiting.  Since the existing solver doesn't support back-tracking (e.g. revising a selected package version selection backwards during solution generation), trying to install third party packages that were published with different versions for various OpenSolaris releases was difficult if your machine was not running the most recent releases, and dealing with nested incorporation dependencies was impossible.  I experimented with a more conservative solver that attempted to upgrade as little as possible; this made upgrades across multiple releases painfully slow, however, and still didn't deal with newer versions being un-installable due to missing dependencies, etc.  In addition, we received multiple requests for exclude-type dependencies that would allow packages to prevent installation of incompatible packages; this was definitely outside the capabilities of our naive solver.

Conventional solvers iteratively attempt to satisfy package dependencies by walking the package dependency graph and selecting package versions to try; our experience w/ the large numbers of package being generated by biweekly (or nightly or even every push) builds indicated that such an approach would be very slow in some cases as the order of graph traversal might lead to the need to explore thousands of possible solutions.  Reading some of the research (in particular, the EDOS and ZYpp projects) indicated significant interest/progress in attacking packaging computations as boolean satisfiability problems, and we decided to try that approach.

Boolean satisfiability solvers need their problems posed in conjunctive normal form; e.g. as a conjunction (logical ANDing) of clauses containing disjunctions (logical ORed) of variables (or their negation).  By assigning the presence of a particular version of each package a unique boolean variable, we can construct clauses for dependencies and existence that allow the solver to compute solutions to our packaging problems.  For example, given four possible versions of package A, the fact that we can only install one version of a time of package A yields the following set of clauses (assigning A1 to indicate the presence of version 1 of A, and ! to represent negation and | to represent disjunction):

  • !A1 |  !A2
  • !A1 |  !A3
  • !A1 |  !A4
  • !A2 |  !A3
  • !A2 |  !A4
  • !A3 |  !A4

Clearly, large numbers of versions of a package can generate an inordinate number of clauses; more on that a bit later.

If a require dependency exists on a particular package version, indicating that that version or newer is required, clauses are generated to describe that dependency.  For example, if package B@1 depended on A@2:

  • !B1 | A2 | A3 | A4

If an optional dependency exists on a particular package version, that indicates that if that package is installed it must be at least at the specified level.  Here, we end up excluding versions we don't want.... For example, if package B@1 optional depended on A@3:

  • !B1 | !A1
  • !B1 | !A2

Our incorporate dependencies that specify the version needed also generate such exclusionary clauses.  For example, if package B@1 incorporates A@3 (e.g. if A is present it must be at version 3):

  • !B1 | !A1
  • !B1 | !A2
  • !B1 | !A4

Lastly, actual exclude dependencies indicate that if present, the depended upon package must be at the specified level or lower.  If package B@1 has a exclude dependency on A@3:

  • !B1 | !A3
  • !B1 | !A4

Once the packaging problem can be described as a series of clauses, it can be passed to a SAT solver for solution; the solver generates a set of packages that will meet the specified criteria, or declare that no solution exists.  The number of variables used in the solver is the number of package versions installed plus those considered; the number of clauses used depends on the number of versions of a package and the types of dependencies.  To minimize the size of the problem and the resulting memory footprint, we don't simply generate clauses for all possible packages and their versions; since we know that packages are not allowed (normally) to decrease in version, we eliminate from consideration earlier versions of any installed packages, and any packages excluded by incorporations we're unwilling to change.  We also eliminate duplicate packages from publishers we're not willing to consider.  This "trimming" phase is actually the most time consuming phase of generating the list of packages to install.

If all we needed was a single solution, this would be adequate; however, we'd like to find solutions that meet our definition of optimal.  We do this by finding solutions and then looking for better ones by resolving the problem w/ additional constraints excluding areas we don't consider optimal. For example, when installing a package we're willing to update other packages if needed (within incorporation constraints, of course), but we'd like to minimize such changes.  This is an area we're still exploring, and a likely topic for additional blogging.

We choose the Minisat solver as a good place to start as they had built a C version of Minisat that would be easy to link into our packaging system, which is coded in Python.  About the only changes I made were to keep track of the clauses fed to the solver, so that it is possible to cheaply revise solutions by caching copies of the current state of the solver. Introduction of the SAT solver awaited Shawn Walker's very nice catalog rewrite which added dependency information into the package catalog, as it was critical for perfomance reasons to not have to download hundreds of manifests to do package planning.  I integrated the new solver into the packaging gate for build 128 of OpenSolaris, now available from pkg.opensolaris.org/dev and other mirror repositories.

One of the interesting implications of the solver change has been that it is more difficult to determine just why there are no image-updates are available.  The previous solver would fail (badly) when encountering missing packages in dependencies, etc; the new solver just considers packages with missing dependencies as uninstallable and thus unavailable for upgrade.  Image-update will now very rarely generate any error messages, which is nice from a user aspect but makes debugging mis-configured or broken builds more difficult than before.  If you think you should be able to upgrade, try explicitly installing the version of entire (the incorporation that currently controls what software build you're running) you think you should be able to install w/ -nv as flags; this will generate much more verbose debugging output when no solution can be found, as the packaging system has some idea of what you'd like to achieve other than just "get me newer bits if you can". Generation of more useful error messages will remain an important area for further work.

Other interesting areas for further enhancements enabled by the SAT solver include constructing the entire incorporation as an incorporation of other incorporations; this will allow developers to easily run the latest kernel and older window system bits, or vice versa.  We're also considering conditional (package A requires package B if package C is installed)  and disjunction (package A requires package B or package C) dependencies to solve some of the more complex package configuration requests we've seen.



Comments:

Nearly 3 Billion devices run Java ME in the world today. Before a manufacturer can make a device commercially available, and before a service provider can add new devices to its offerings, they must perform a significant amount of testing to ensure a high-quality, reliable product that delivers customer satisfaction.

Posted by l-carnitin on December 05, 2009 at 02:35 PM PST #

Post a Comment:
Comments are closed for this entry.
About

An engineer's viewpoint on Solaris...

Search

Archives
« April 2014
SunMonTueWedThuFriSat
  
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
   
       
Today