Static analysis of software component repositories : from Debian to Opam
By Roberto Di Cosmo on Wednesday, May 21 2014, 14:44 - Mancoosi - Permalink
Component repositories are becoming an essential part of the Free Software landscape, and grow at a steady pace. Ensuring their quality is of paramount importance, and is a difficult task. One natural question to ask when performing quality assurance is the following : what are the components p in a given repository R that cannot be properly installed?. Unfortunately, there can be many reasons why an installation may fail, and some of these will only be detected on the particular environment of the final user, no matter what amount of testing one tries to do beforehand.
But there is a full class of reasons, related to package interdependencies, that can be found by performing a static analysis of repositories, with no testing at all. This static analysis, originally designed for GNU/Linux distributions, is of general interested, and we are now introducing it for the Opam ecosystem.
Checking installability is an NP-complete problem ...
To help GNU/Linux distributions in their quality assurance work, in the framework of the EDOS and Mancoosi project we focused on the following question : what are the components p in a given repository R that cannot be installed because of dependency problems?
.
It turned out that solving dependencies to install a package is a problem equivalent to satisfying a Boolean formula, as described in the original ASE paper of 2006, and is hence an NP-complete problem. This was a surprising limitative results, and since there are tens of thousands of packages in a typical Debian distribution, finding all non installable packages in a repository may have seemed a daunting task.
... but in practice we can solve it quite efficiently ...
In practice, though, the structure of the dependency graph is well behaved, and an efficient SAT solver due to Jerôme Vouillon can process an entire Debian repository in just a few seconds.
Hence, it has been possible to provide a valuable tool to the Debian Quality Assurance team: Jerôme Vouillon's edos-debcheck (and a companion tool edos-rpmcheck for RPM distributions) was inclued in Debian, and in 2006, Fabio Mancinelli and Ralf Treinen showed these tools during the Debian Quality Assurance meeting. Under Spain's sun, Ralf Treinen set up a service built around edos-debcheck at edos.debian.net to provide daily updates on the status of dependency issues for all packages in Debian. There was also a nice graphical overview in terms of weather
, that summarised the status of each suite. Since 2008, this service has been running on machines provided by Mancoosi.
... and generically!
The technology used to perform such tests evolved over time, and is now incorporated into the Dose library, where one can find the latest tool dose-distcheck that can analyse not only Debian or RPM-based package repositories, but any repository described using the CUDF format normalised during the Mancoosi project.
Welcome to the Opam Weather Service
So, we are quite proud to announce that now at Irill we started hosting a similar quality assurance service for Opam, the new OCaml package manager.
You can find the results of the static analysis of the repository, performed daily, on ows.irill.org, where for each package and version you can see whether it is installable, or not, and when it is not installable, find an explanation of the reasons why this happen.
This service will help improve the quality of the Opam repository over time, allowing package maintainers to easily identify the reasons of any dependency issue.
You are welcome to link to this service, using permanent URLs of the shape http://ows.irill.org/table.html#PACKAGENAME or http://ows.irill.org/table.html#PACKAGENAME.PACKAGEVERSION that will lead you to the relevant table entries reporting the latest analysis results for the package of your choice.
We are very grateful to the fine people at OCamlPro that helped us set up and test this service, which they also announced here.
What next?
We plan to add new features to this service over time, exporting to Opam the many static analysis developed over the years for GNU/Linux distributions, so stay tuned for new exciting announcements over the next months!
Acknowledgements
This service is built on top of theory, technology and tools that were developed over the years by many bright and proactive people: we are deeply grateful to Pietro Abate, Jaap Boender, Ralf Treinen, Jerôme Vouillon and Stefano Zacchiroli for their dedicated contributions.