Review NP-complete Library Versioning Problem

While investigating the relationship between modules, their versions and mutual dependencies I came across one hard problem: Given a repository of modules (like the one provided by maven), select such configuration of the module versions so all their dependencies are satisfied.

After a little bit of thinking I concluded that this is NP-complete problem. I have even written down a proof.
I guess many LtU members are qualified to review the proof for soundness. Would you be so kind and tell me if there is anything wrong with it? Thanks.

Visit the proof.

Comment viewing options

Select your preferred way to display the comments and click "Save settings" to activate your changes.

I'm concerned

The proof doesn't mean much in practice unless natural development of libraries or repositories leads to a situation like the one you describe. My suspicion is that the domain of the Library Versioning Problem simply doesn't allow the generality your conversion from 3SAT requires.

[Edit: A point made later by Matt helps illustrate this concern. It is not the case that supposedly 'compatible' modules like Fx(1,1), Fx(1,2), and Fx(1,3) can export entirely distinct interfaces Ma, Mb, and Mc.]

Otherwise, the structure of the proof looks okay.

Known

I haven't looked at your proof, but similar problems in Hackage are also understood to be NP-complete. I believe that Hackage and Maven-like products offer very similar dependency specification, so I expect the result is general.

I don't know exactly what you mean by "such configuration of the module versions." It sounds like you may mean a maximal consistent subset? If so, you should note that the seemingly much easier problem of "is it possible to install a single package?" is also NP-complete, in general.

It doesn't seem like hard instances occur in practice...

Happens in Practise

First of all, thank you all for your comments. I'll adjust the text to avoid traps you have been drawn to.

I'd like to argue with the claim that it does not occur much in practise. I have two answers:

  • yes, it does not occur in the most frequently used libraries and guess why!
  • no, it does occur more often to be considered harmless.

Obviously it is not the NP-complete problem that manifests itself in the real life. Its symptoms are manifested. Except being beaten by such symptoms in our own NetBeans development, I found a nice article Preserving Backward Compatibility about troubles with library reuse in Subversion. The incompatible changes in Apache Portable Runtime are exactly the symptoms of the NP-complete problem. If there is another library that relies on APR (and I am sure it is) then the parallel use of subversion (as a library) and such library is heavily limited (if they each rely on different incompatible version).

Symptoms of such problems are more common in libraries that are not yet popular enough. Their developers may not yet be trained in keeping backward compatibility. However the more popular your library becomes the more you will care. As a result often used libraries are developed in compatible way. Finding whether module dependencies can be satisfied in a repository with only compatible versions is obviously trivial.

But imagine glibc developers went mad and published an incompatible version. As that library is used by everyone, there would be quite a lot of NP-complete problems to solve.

My proof can also be seen as an advertisement for importance of backward compatibility. While we keep it, we live in a simple world, as soon as we start to release big bang incompatible revisions, we'll encounter the NP complexity.

The incompatible changes in

The incompatible changes in Apache Portable Runtime are exactly the symptoms of the NP-complete problem.

I am not familiar with these incompatible changes. More detail would be appreciated.

The Subversion article you pointed to was very high-level and theoretical, and didn't really discuss much about real examples of "troubles with library reuse in Subversion". About the only issue the article gave was clients using different protocols from Subversions standard current protocol. Even then this issue is poorly explained and not developed. You have to wonder if the author knows what the real problem is or not.

glibc is certainly changed from time to time. Most recently an example would be mallinfo. What you have to realize is that more often than not these changes aren't so rapid (a major reason why glibc is used so universally). When things DO change, it often suggests a change in the structure of the problem domain. Changes like mallinfo are even rarer: design flaws.

Bottom line: No one is interested in solving problems that don't need solving, so show us why this needs solving and can't just be avoided using good development processes complimented by tools using heuristics faithful to those dev processes.

mallinfo & good engineering

Where's the mallinfo incompatible change? As far as I can read the link, new method has been added, but the text does not seem to contain any warning about the old method being removed. My understanding is that the method stays in the library and does what it used to do. Just in some, new situations, its behaviour is not absolutely correct/valuable.

Perfectly backward compatible. If everyone followed good API design practices this way, there would be no NP-complete problems of this kind to solve.

Btw. when talking about tools. I should mention that the automated tools for checking binary backward compatibility are quite useful. There is Sigtest for Java and another tool for C/C++. Those help eliminate the NP problem before it arises.

My understanding is that the

My understanding is that the method stays in the library and is just useless in some situations (while behaving the same as it behaved in previous versions).

This statement is self-contradictory. Can you clarify?

Where's the mallinfo incompatible change?

Look at the subsystem as a whole.

The paradox of backward compatibility

As the page on backward compatibility that you linked says:

Of course, there is some flexibility here, as at some point you have to be able to say, "This behavior is a bug, so we changed it"; otherwise, there is little point in releasing new versions of your software.

But really, what good is that? If your library's clients contain code to work around a known bug (and most serious programs have such workarounds in them), what happens when you fix the bug? You have broken backward compatibility, that's what. And yet the whole idea of backward compatibility is "Always use the current library; it has the bug fixes you need"; but what about the bug fixes you don't need and don't want? If you have to change your code to use the new library, it's not backward compatible, by definition.

This comes up not so much with libraries as with protocols, where clients and providers often belong to mutually suspicious organizations with completely independent upgrade cycles.

The client geek says: "I asked for service version 2.1, and I should get exactly what 2.1 has always provided."

The server geek replies "But the data delivered by 2.1 is complete @#$*! So we deliver 2.2 when you ask for 2.1; it's only sensible. That's the whole point of minor versions."

Client geek: "You think I don't know that? I already have workarounds in place, and what's more, they're hard-coded into Gadgetron model 2055. You think all my customers are going to field-upgrade it [if it even is field-upgradeable]? They're going to get bad data, and they're going to blame me!"

Server geek goes off grumbling "So they should". But it's the real user who suffers.

If your library's clients

If your library's clients contain code to work around a known bug (and most serious programs have such workarounds in them), what happens when you fix the bug? You have broken backward compatibility, that's what.

I'd say what you did was fixed a bug in your code which revealed a bug in the client code. If client code performs 'work-arounds' to a bug without performing a test to see if the bug exists, that's a bug in the client code.

Server Geek is exactly right to blame Client Geek when Client Geek codes to the implementation rather than to the documentation. Client Geek took advantage of what Server Geek was offering, then violated the contracts describing said service. Client Geek had other options, such as coordinating with Server Geek to fix the problem, or to implement the service without introducing a dependency, or to renegotiate the contract to ensure fully bug-compatible service was maintained for so many years so his clients don't suffer.

Anyhow, there are multiple levels of backward compatibility described on the page linked. Functional compatibility is 'same result' which would suggest bug-compatibility. It seems to me there's a missing level - interface compatibility - that suggests persons who programmed to the interface (preconditions and postconditions) will continue to have results compatible with the documentation. Even more general are source compatibility (can re-compile) and binary compatibility (can link new object without re-compile).

Real world example:

the new open flag, O_PONIES --- unreasonable file system assumptions desired.

(Supposedly b/c KDE developers didn't read POSIX, ever, and assumed ext3 would always be the fs KDE uses).

Here is the problem. Client Geek will never acknowledge, or perhaps even understand, that Server Geek is right.

Blaming customers is big no-no

Blaming customers is wrong strategy to win their hearts. Thus blaming client geek is wrong. The whole fault needs to be on the shoulders of the server geek. Btw. thanks for your(?) comments on the talk page.

Where do you draw the line?

Do you go the Old Microsoft route and have an entire division in the company dedicated to making sure Sim City 2000 and Adobe Illustrator work on the next version of Windows despite using undocumented features or whatever else chicanery?

Manager to Structural Engineer: "Sorry, you can't blame the welder that this will likely collapse even if it his fault. Find some way to make this thing stable and sturdy. I heard about this thing software developers do to give customers pink ponies..."

Blaming customers is wrong

Blaming customers is wrong strategy to win their hearts. Thus blaming client geek is wrong.

Sorry, Jaroslav, but that attitude strikes me a bit like "don't blame the customers who vandalize your store; sure, they broke the social contract for participating in your service, but you won't win their hearts by blaming them!".

You should make it clear to your customers which behavior they can assume will remain consistent in future versions. If they then violate the contract, you can blame them. You can be polite about it. I.e. you can provide a press release to the effect of "yes, this could break some code, but our customers have been told to code to the interface and we believe that most of them have done so. If they coded to the interface, their projects will automatically reap the benefits of this upgrade."

By putting the responsibility where it belongs you send a clear message: pay attention to the documentation.

Chances are, a few people will mess it up the first time. They'll be a little upset at needing to redo some work. A few of them might even abandon you as a service provider, running off to whatever they view as 'greener pastures'. But no pain, no gain, right? You can't keep everyone happy all the time: fact is, if you have multiple customers, you'll win some and lose some based on nearly ANY decision you make. Even forking for different customers can piss customers off that expected to share expenditure for upgrades. And if you have only one customer, you've already set yourself up for oblivion.

By taking a stand, you'll ensure that everyone gets the message clearly. Your service will then have a great deal more freedom to advance and repair itself over time. Even better: you can take advantage of this freedom to give clients better opportunity to propose fixes and changes that remain within specification.

The future couldn't last. We nailed it to the past... -- Savatage

Vandalism vs. peaceful shopping

I have nothing against blaming those who misbehave. If you are using a library in a wrong way and it does not work, well, then OK. It won't work for you. If you are vandalizing a store, you are unlikely to buy anything.

However I when I use some library in strange/unexpected way and it works, then I want this to work in next version too. If I buy a motorbike in a store and return back to apply warranty, I do not want to hear: "we are no longer in motorbike business, go away, now we sell only refrigerators". That would be unfair blaming.

Documentation is indeed important. If something is clearly marked as "don't do this", then I should not do it. Defensive design is even better. If a type is not supposed to be subclassed, then it is better to make it final than write into documentation that is should not be subclassed.

If a method does accept int but only in certain range, then throwing assertion errors is OK. But this has to be done since introduction of such method.

However forgetting to be defensive or to provide a warning in first version and later trying to justify incompatible change by saying "this class was not intended for subclassing" or "this parameter was obviously out of range" is clearly not acceptable for me.

Whatever is not forbidden, is allowed. Library designers deserve to be blamed for violating this rule.

Whatever is not forbidden,

Whatever is not forbidden, is allowed. Library designers deserve to be blamed for violating this rule.

Okay. But if the documentation states - or even implies - "do not depend on undocumented behavior", that should be taken as a claim of: "whatever is not explicitly documented, will break later." And library clients deserve to be blamed when their code breaks as a result of depending on undocumented behavior.

I agree with "defensive" programming of the library or protocol - primarily as a basis for security, I favor capability security designs. But not all languages and situations allow this to be done, at least without sacrificing performance and other desirable properties.

When I use some library in strange/unexpected way and it works, then I want this to work in next version too

If you use the library in a strange/unexpected way, and it works, but you for some reason expect the next version to have the same implementation quirks, then you've earned whatever your naivete bought you.

Perhaps you should load the library with the O_PONIES option.

Wow !

What started as a call for a review of a proof ends up in a layman discussion about how to lead an IT business and respond dogmatically to environmental conditions ( customer requirements, users demands, ...), reflecting behaviors in terms of "right" and "wrong" (!), which reinforces prejudices about the brash naivety of techie positivism.

Is this still the LtU we want to read?

Touché.

Touché.

Correct.

I guess I got the answer I was looking for regarding my proof. Thanks.

If there remains anyone who wants to continue to discuss who's fault wrong API usage is you can do so elsewhere.

Thanks again for your comments.

This is a misinterpretation of my anecdote

Client Geek began by coding to the documentation, but the data he got was erroneous ("complete @#$%", as Server Geek says). Let us say Server Geek is providing a stock-pricing service, only in 2.1 all stock prices are too high by 100. Client Geek noticed that GOOG was being priced at 554 instead of 454 (I wish!). Server Geek being a bit slow to fix this problem, Client Geek worked around it by subtracting 100 from all prices and shipped by his deadline. There is, obviously, no way to test whether this bug exists, short of subscribing to two services.

Server Geek, working to his deadlines, was dealing with something else and didn't even prioritize the problem until a few hundred different Client Geeks reported it. Then he fixed it and upped the version number to 2.2, which broke Client Geek's code. It's too late for Client Geek to conditionalize his code at this point, because it has shipped.

The fault here is entirely Server Geek's, but everyone is quick to put the blame on Client Geek. What does that tell us about our own assumptions?

(I just introduced clients and servers as an intuition pump; the issue works the same with field-upgraded libraries invoked by programs that are not field-upgraded.)

Spin the finger...

The fault here is entirely Server Geek's, but everyone is quick to put the blame on Client Geek. What does that tell us about our own assumptions?

The error in 2.1 is clearly Server Geek's. The work-around is Client Geek's error. The apparent lack of communication between the two entities is certainly an error on both their parts - e.g. the Client Geek didn't establish a contract to maintain a bug-compatible version of the service on a dedicated port.

What does putting the blame entirely on Server Geek tell us about your assumptions?

I have no joke, I would just like

I have no joke, I would just like to point out that Eclipse's p2 provisioning system apparently uses a SAT solver for dependency resolution, and that there was apparently some consideration of using a SAT solver for OSGi runtime dependency resolution.

Known problem

Research yum, rpm, apt, or other package management solutions for various ways to deal with this issue, both in logical design and satisfiability optimization (using heuristics). It turns out wth heuristics you can usually get good results. By logical design, I mean "the best way an engineer can solve a problem is to avoid it", or at least I like to think so.

The results of the EDOS

The results of the EDOS projects could be relevant. They include a statement of NP-completeness, and a review of the (flaws of) the algorithm used by existing package managers ('survey and state of the art' section).

Cyclic dependencies

The problem seems solvable in O(N), where N is the number of modules versions, as long as there are no cyclic dependencies between modules (assuming bounded dependencies per module). Further, if you start with a DAG and add a cycle forming edge to some module, it would seem to require only a single search over the versions of that module to resolve, and disjoint cycles combine complexity linearly. This seems like an obvious way to characterize the 'bad' dependency graphs and to explain why we don't generally see this in practice.

Not a cyclic dependency problem

It isn't a simple dependency-graph problem, Matt, due to the existence of incompatible modules. Incompatibilities, expressed in the problem as difference in "major" version numbers, can force a naive algorithm to backtrack and try again whenever it selects two mutually incompatible modules. It's worth noting that the conversion from 3SAT described in the proof involves no cycles.

In practice, heuristics will probably rapidly resolve the problem in 99%+ of all cases. If simple heuristics can't solve the problem, that should probably raise a flag; one must question how development of a project might lead to such a thing.

Ah thanks

I was considering the wrong problem

That an algorithm uses

That an algorithm uses backtracking doesn't imply it is in O(2^n). Backtracking parsers for example can be linearized using memoization.

Not a proof

The set {A} already satisfies the conditions for being a configuration. Same with {A, B} where A >> B or B >> A or both.

Your definition is not strict enough to exclude non-trivial solutions.

And please! Use your own terminology consistently and don't suddenly start to talk about "modules" when you formally introduced entities you called "APIs".

Wording was confusing

But there was a 3rd satisfaction condition:

if A>>B(x,y) and A>>B(p,q) then it must be the case that (x == p) and (q == y).

I had to read it a few times before grokking the purpose of that third condition, since it wasn't clearly worded like other conditions.

Combined with the conditions requiring equal-major version plus minor-version greater than or equal to the dependency requirement, the trivial solutions are excluded.

The actual error in my

The actual error in my remark was that I overlooked that all B(x,y) in M with A >> B(x,y) have to be considered. So just forget about this complaint. Maybe I find something else :)

Be consistent!

And please! Use your own terminology consistently and don't suddenly start to talk about "modules" when you formally introduced entities you called "APIs".And please! Use your own terminology consistently and don't suddenly start to talk about "modules" when you formally introduced entities you called "APIs".

Improved, thanks.

Fine. Although a formal

Fine.

Although a formal definition is necessary for a formal proof and I was wrong about my initial concerns, the description is very terse and it is not easy to see where the problem actually lies ( truth of an assertion is one thing, insight into a problem another one - the major reason why mathematicians dislike computer generated proofs for anything but tedious manual labor ).

My take on the configuration problem is this.

When we start with a module A we can create the transitive closure of all possible module dependencies. This is a dependency graph which is too big to be useful because it contains all modules in all versions. We need a rule according to which we select a single version of a module. The best criterion is always the one by which we select the module with the highest possible version number.

This is not problematic when dependencies are kept local: when A depends on B and C(x1, _) and B depends on C(x2, _) then a dependency conflict can always be avoided when B doesn't export names of C(x2, _). The interface is kept small. But when B exports C symbols they are also visible in A. So the initial choice of C(x1,_) may be invalid when selecting B with a C(x2, _) dependency. So we have to revise our choices. In the worst case none of the C dependencies of A fits together with the C dependencies of B. We have to expect that all admissible C dependencies of A have to be matched against those of B. This propagates along the whole transitive dependency closure and is the intuitive reason why determining whether A has a valid dependency graph ( configuration ) is NP-complete.

When our dependency model contains only one of the relational operators ">" and ">>" then we might rule out valid configurations in case of ">>" or permit invalid ones in case of ">". Choosing ">" might work under the optimistic assumption of keeping the interface small. The configuration problem becomes linear then. But when we give up on it, we run into NP-completeness and what's worse, we invalidate otherwise valid configurations.

I'd nevertheless recommend to start with the pessimistic assumption even though the computational overhead is considerable and let the library author incrementally improve by manually inserting ">" where this is appropriate.

EDOS

There were a few papers in 2006 on the EDOS site about using a SAT solver for checking repository consistency. IIRC, one of them also used a reduction to 3SAT.

NP or not...

It's not clear to me what you're trying to show, so let me give some solutions to different situations.

Let's create a directed graph (V,E), where each vertex in V is a pair (API,version) and an edge in E is a dependency relationship (this is, an edge exists iff two (API,version) modules are compatible)..

  • You can find if dependencies are satisfied within V (if your set of APIs is complete) by creating an equivalent undirected graph and finding the connected components in linear time.
  • You can see if there're cyclic dependencies in linear time with a topological sort. Then you'll end up with a DAG which is easier to maintain, as you say in your book.
  • (API,version) removal: If you're trying to find a subset X of V so that (V-X,E) is cyclic-free then that's a Feedback vertex set problem, which is NP complete.
  • Dependency removal: If you're trying to find a subset X of E so that (V,E-X) is cyclic-free then that's a Feedback arc set problem, which is NP complete as well (it's polynomic for undirected graphs, though). A "Fast FAS" algorithm used in graph drawing can be found here.
  • Given an initial (API,version) vertex you may want to find a subset X of V that satisfies all dependencies (in linear time).
  • Given again an initial (API,version) vertex and the X set of vertices above you may want to find which "most modern" dependencies best connect your original vertex. I think you'll end up again in NP territory because you may reduce that to the travel salesman problem.

You are confusing...

...issues of dependency and compatibility.

an edge in E is a dependency relationship (this is, an edge exists iff two (API,version) modules are compatible)

You are confusing too

You are confusing too

The mapping to graph is wrong

As dmbarbour said, but not explained, the mapping of the version and dependencies problem to graph that you propose is wrong.

this is, an edge exists iff two (API,version) modules are compatible

(n, x.y) is compatible vertex with vertex (m, u.v) iff n == m && x == u && y >= v

Dependencies represent the necessary environment of a given module/vertex. That is something else than compatibility.

The Gallium project at Inria

The Gallium project at Inria has interesting results on formal management of software dependencies.

This paper (from the EDOS project that bluestorm has mentioned previously) has interesting results. They also map vertices to package names + versions, and have edges for both dependencies and conflicts (fig. 2).

One of the results of that paper (Theorem 1, p. 11) is:

Theorem 1 (Package installability is an NP-complete problem). Checking whether a single package
P can be installed, given a repository R, is NP-complete

But that's a different problem from "select(ing) such configuration of the module versions so all their dependencies are satisfied". I still think that verifying if all dependencies in a repository are satisfied can be solved in polynomical time.

I don't understand

Ok, I read and now understand the setup. In your correspondence to SAT you introduce compatible modules F_{u,v} which re-export incompatible modules M_{x,y}. I don't understand how the Fs can be compatible if they re-export incompatible things. Can you clarify this?

Clarification

For each variable Vk in the SAT problem, there is a distinct pair of modules: Mk(1,0) and Mk(2,0). It's worth noting that Mk is completely distinct from M(k+1) and M(k-1).

Now, the Fi(1,1)..Fi(1,X) corresponds to a given clause in the CNF form. The module T only needs one of those, not all of them. Each clause has a distinct 'i'.

So, supposing there were only two clauses:

 (va or ~vb or ~vc) and (~va or ~vb or vc)

This corresponds to:

  F1(1,1) >> Ma(1,0)
  F1(1,2) >> Mb(2,0)
  F1(1,3) >> Mc(2,0)
  F2(1,1) >> Ma(2,0)
  F2(1,2) >> Mb(2,0)
  F2(1,3) >> Mc(1,0)
  T(1,0) >> F1(1,0)
  T(1,0) >> F2(1,0)

Now, note that there is no F1(1,0) and no F2(1,0). But F1(1,1) and F1(1,2) and F1(1,3) can each satisfy F1(1,0) because they're all "minor" versions of the same module.

An incompatibility will exist if and only if there exists some k such that T(1,0) must export Mk(1,0) and Mk(2,0) simultaneously. This corresponds 3SAT being unsatisfiable if and only if there exists some k such that vk must be held true and false simultaneously.

Clearly the 3SAT problem can be solved by:

    (va  and ~vb) 
 or (va  and  vc) 
 or (~vb and  vc)

This corresponds to T(1,0) loading modules:

    (F1(1,1) and F2(1,2)) (which loads Ma(1,0) and Mb(2,0))
 or (F1(1,1) and F2(1,3)) (which loads Ma(1,0) and Mc(1,0))
 or (F1(1,2) and F2(1,3)) (which loads Mb(2,0) and Mc(1,0))

Hopefully that clarifies how Fs can be compatible even if some of them export incompatible things.

Different interfaces?

It's worth noting that Mk is completely distinct from M(k+1) and M(k-1).

Yes, good point. I shouldn't have refered to them as 'incompatible modules' when I really just mean 'different'.

But F1(1,1) and F1(1,2) and F1(1,3) can each satisfy F1(1,0) because they're all "minor" versions of the same module.

My point is that they don't have the same interface, though, because they re-export different things. This would seem to me to make them incompatible. If minor versions are only supposed to be backward compatible (within the same major version), it still looks like this is a bad encoding since F1(1,2) doesn't at least have the re-exports of F1(1,1). What am I missing?

Objection to Realism

Since you're objecting to the realism of the translation, I agree. See my first post on this subject. Your particular argument against that realism - that F1(1,1), F1(1,2), and F1(1,3) are each exporting largely distinct interfaces and thus shouldn't be 'minor versions' of one another - is a good one.

Transitivity of incompatible change

In Chapter 10, Cooperating with Other APIs of my book I even talk about transitivity of incompatible change. If a re-exported API changes incompatibly, so must all its re-exporters. How could I forget to mention that in the context of the proof!?

Well, I probably have not mentioned that because it does not apply to this proof. The F_{1.1} and F_{1.2} and F_{1.3} depend on completely different M^a, M^b and M^c. It is not the case that there would be F_{1.1} depending on M^a_{1.0} and F_{1.2} depending on M^a_{2.0} (such 3-OR would be v & not(v) which is a tautology and we can ignore it).

But you are right that: if F_{1.1} is re-exporting some M^a and F_{1.2} is re-exporting another M^b, how can F_{1.2} be compatible with F_{1.1}? Hardly.

That probably does not disqualify the proof, but it may lead us to define some easily decidable condition on real repositories that would prevent conversion of 3SAT to such repositories. I can think of using Signature Testing tools. Those can verify that a module in version F_{1.2} is really binary compatible with F_{1.1} and if not force its re-numbering to F_{2.0} before accepting it to the repository. Congratulation, you probably discovered new way to fight with NP-Completeness in library versioning area.

PS: Of course, Signature tests are only good if we are talking about binary compatibility, they cannot help us with functional one.

Realistic in some module containers

This comment is inspired by a note that Equinox is using SAT4J solver. The module system behind Equinox has its own specifics and surprisingly it allows following setup:

Each M^i_{1.0} would export two packages (think of each M^i as a different implementation of the same API, plus some specifics):

package a; public class API {}
package b; public class Mi {} // the i would be a variable
package b; public class Version10 {}

Each M^i_{2.0} would export compatible package a and incompatible package b:

package a; public class API {}
package b; public class Mi {} // the i would be a variable
package b; public class Version20 {}

now the F_{1.i} and would have just one object:

package f; public class F extends a.API {}

Thus the F_{1.3} is quite compatible with F_{1.2} and it is compatible with F_{1.1}. All have the same class F which extends a.API and the signature of a.API is in each case the same. This is true in spite of the fact that the each two versions of M^i are itself different and incompatible.

Moreover Equinox allows F to import just a part of the M^i - only single package a. As a result it seems that this is perfectly valid setup for that module system. The question for the Equinox to solve is which of all the available M^i implementations to choose. Computing the answer is then NP-Complete, hence the need for SAT4J.

If you think this can't be real, then you are probably wrong. I too find some features of the system behind Equinox weird. But at the end I am not the author of that module system. Our NetBeans Runtime Container does not allow tricks like this.

Terminology

Thus the F_{1.3} is quite compatible with F_{1.2} and it is compatible with F_{1.1}

The class F contained in F_{1.3} may be compatible with the class F contained in F_{1.2}, but the class F is not the only thing contained in the module F_{1.i} and I would consider the modules incompatible.

Re-export a part of a module

You are right, if we always treat module as a unit. The module F_{1.3} would then re-export whole M^i and this compound set of APIs would be different to compound set of F_{1.2} re-exporting some other M^j. I am aware of that and thus I used "quite compatible" not "compatible".

But if a module can be split into smaller parts (and Equinox allows to import and re-export just a single package from M^i), then the compound view of F_{1.3} is the same as F_{1.2}. They are fully "compatible".

I don't know how much the partial re-export of a module is useful, but it is clear it is quite dangerous (e.g. allows the NP-Complete problem to really appear in real life).

This just showed up on the

This relevant paper just showed up on the programming subreddit:

Strongly-typed languages rely on link-time checks to ensure that type safety is not violated at the borders of compilation units. Such checks entail very fine-grained dependencies among compilation units, which are at odds with the implicit assumption of backward compatibility that is relied upon by common library packaging techniques adopted by FOSS (Free and Open Source Software) package-based distributions. As a consequence, package managers are often unable to prevent users to install a set of libraries which cannot be linked together.

We discuss how to guarantee link-time compatibility using inter-package relationships; in doing so, we take into account real-life maintainability problems such as support for automatic package rebuild and manageability of ABI (Application Binary Interface) strings by humans. We present the dh_ocaml implementation of the proposed solution, which is currently in use in the Debian distribution to safely deploy more than 300 OCaml-related packages.

Remarks (overdue)

Seems a solid result, some overdue remarks/questions.

Isn't NP-hardness shown instead of NP-completeness? [Just add that it takes polynomial time to verify a solution.]

The result only holds for a very stringent definition of a module system. [I.e., an assumption that incompatible modules cannot be installed at the same time may not hold for all languages.]

Even if NP-complete, it is very unlikely any 'hard' problem will be encoded, so I expect almost all problems can be solved in microseconds - which isn't a lot for a library problem. [The result just implies that simple DFS may not be the best candidate for a calculating a solution, but a DPLL solver (adoption) or a constraint solver will probably calculate a solution very fast.]