Solver: Add individual flags to conflict sets. #4562
Conversation
|
Let me know if you want an in depth code review, but the logic description in the commit sounds good to me. |
|
Sounds fantastic. I'll try to take a look. But in any case, it's a good approach, and it should hopefully fix a few pathological cases we currently have. Looking forward to your performance test results. |
This commit changes the way that the solver tracks the variables that introduce dependencies, in order to fix some bugs that prevented the solver from tracking individual flags. I refactored Dep, the type that represents a build-depends or build-tool-depends dependency, so that it stores the package, flag, and stanza choices that introduced the dependency. That information is stored in a field of type DependencyReason. The DependencyReason is available to any solver phase that needs to create conflict sets, such as "build" or "validation". Whenever there is a conflict involving a dependency, the solver creates a conflict set and a log message using the dependency's DependencyReason. This means that the solver only needs to calculate the dependency reasons once, in IndexConversion.hs, rather than every time they are used, i.e., in Builder.hs (for goal reasons), Validate.hs, and Linking.hs. Another difference between this commit and master is the dependencies between solver variables. On master, each dependency or variable is introduced by exactly one other variable. For example, if package x has a flag y, which controls a dependency on package z, then the three variables depend on each other in a chain, x -> y -> z. If z can't be satisfied, the solver backjumps to its cause, y, and if flipping y doesn't help, it continues backjumping to y's cause, which is x. In contrast, this commit allows each dependency to be introduced by a package and any number of flags and stanzas. So z's DependencyReason would contain both x and y. Storing all flags that introduced a dependency allows the solver to correctly calculate conflict sets when there are nested conditionals. We no longer need to combine each package's flags into a single conflict set variable. This commit removes the 'simplifyVar' function and adds flag variables directly to conflict sets. See issue haskell#4391. This commit makes another minor change. In this commit and master, if a dependency appears in the if and else blocks of a conditional, the solver lifts it out of the conditional. Previously, the solver behaved as if the flag did not introduce the dependency. This commit adds the flag variable to the conflict set or error message if the dependency is involved in a conflict. This change doesn't affect correctness, but I think it improves the error messages, since it gives the whole reason that each dependency was introduced.
|
Thanks! I did some performance testing, so I think it's ready for review now. I ran the solver on all packages on Hackage and found that the change made the solver significantly slower for three packages, Hayoo, hxournal, and nerf. When I looked at the -v3 logs, I saw that the change had caused a bad goal order for Hayoo and hxournal, with this sequence of steps:
Beginning of the log from Hayoo: I made another commit after the main commit, which addresses this problem: Then I ran the solver (
Both versions of cabal hit the backjump limit in four of the cases, so they don't really tell us which version performed better. All but one of the others are improvements. I looked at a few of the logs, and, as far as I can tell, most of the improvements are due to flags being used in conflict counting. This behavior is similar to #4147, which was reverted. These differences in run time are caused by differences in goal order and/or backjumping, but I also wanted to compare performance when the solver went through similar steps on master and the branch. I found two commands that led to very similar -v3 output between the cabal versions. Presumably, package flags didn't cause many conflicts in these runs.
I took the average of three runs. There wasn't a big difference between master and the branch.
|
grayjay
changed the title
… conflict. A DependencyReason contains flags paired with values FlagTrue, FlagFalse, or FlagBoth, where FlagBoth means that the dependency was introduced by either value of the flag and was lifted out of a conditional. In the previous commit, when a dependency led to a conflict, all flags in the DependencyReason were added to the error message and conflict set. This commit avoids adding flags with value FlagBoth to the conflict set, because they can have a negative effect on goal order: After the solver encounters a conflict involving such a flag, it starts to prefer the flag when choosing goals, due to the solver's conflict counting feature. The solver shouldn't prefer the flag goal because it didn't actually need to choose the flag to see the dependency. Flags with value FlagBoth are still useful for error messages, though. I measured the performance of the last two commits by comparing commit fc3ef2a (master) with this commit. I did all testing with GHC 8.0.1 and 'index-state(hackage.haskell.org) = 2017-06-11T02:16:39Z'. I ran each version of cabal (cabal install --dry-run) on each package on Hackage and looked for packages with a difference in run time of at least 10%. Then I reran cabal on those packages to narrow down the list further (The results were noisy). Here are the average run times from five runs with the remaining packages: package master result master time (seconds) branch result branch time (seconds) speedup concraft backjump limit 5.67 backjump limit 4.89 1.16 forml backjump limit 10.26 backjump limit 8.85 1.16 hack-handler-simpleserver backjump limit 6.28 no solution 1.96 3.21 hack-middleware-clientsession backjump limit 17.86 no solution 1.95 9.14 haskore backjump limit 5.21 no solution 1.67 3.12 haskore-synthesizer no solution 23.14 no solution 2.21 10.49 language-gcl no solution 3.06 no solution 2.31 1.33 ms backjump limit 61.68 no solution 7.95 7.76 nerf solution 4.1 backjump limit 5.87 0.7 puzzle-draw solution 56.28 solution 5.31 10.6 react-haskell backjump limit 44.23 backjump limit 14.46 3.06 reflex-transformers no solution 2.18 no solution 1.9 1.15 shpider backjump limit 7.44 solution 1.88 3.95 thorn backjump limit 11.11 backjump limit 4.44 2.5 Both versions of cabal hit the backjump limit in four of the cases, so they don't really tell us which version performed better. All but one of the others are improvements. I looked at a few of the logs, and, as far as I can tell, most of the improvements are due to flags being used in conflict counting. This behavior is similar to haskell#4147, which was reverted. The log for 'nerf', the one package that had worse performance, showed that the solver chose some flags earlier, but I didn't see any other reason for the slowdown. The solver found a solution when I used '--max-backjumps -1'. These differences in run time are caused by differences in goal order and/or backjumping, but I also wanted to compare performance when the solver went through similar steps on master and the branch. I found two commands that led to very similar -v3 output between the cabal versions. Presumably, package flags didn't cause many conflicts in these runs. cabal install --dry-run --max-backjumps -1 gi-glib happstack cabal install --dry-run yesod I took the average of three runs. There wasn't a big difference between master and the branch. packages result master time (seconds) branch time (seconds) master memory (MB) branch memory (MB) gi-glib, happstack no solution 30.02 30.70 245 245 yesod solution 3.53 3.55 239 239.3
…ests. Completely randomizing the goal order exposes more bugs in backjumping than using --reorder-goals. I only applied the change to one test in this commit, because the randomization function slowed down some of the other tests significantly.
|
@grayjay This all sounds rather good. For the cases where both master and branch hit the backjump limit, would it make sense to re-run with increased / infinite backjump limit? Also, do you have any intuitive idea what's still difficult about these remaining cases? |
|
@grayjay Also, for |
I ran cabal again on those packages and
I don't know why these cases ran for so long. Interestingly, each one took less than 10 seconds with --reorder-goals. I did notice that cabal seemed to spend significant amounts of time exploring only a small number of levels, like it was thoroughly exploring subtrees. I've noticed that behavior before during long runs. I think that it can be explained by --count-conflicts moving all of the conflicting packages earlier in the goal order, so that the solver only looks at packages involved in conflicts. Here's part of the log from This log also shows that each of the last three goals is introduced by the level above, i.e, In other cases, the packages in the subtree did not seem to introduce each other in order. I think we might be able to handle the chains of dependencies by either lifting dependencies out of packages (similar to lifting |
|
@grayjay btw, one of the packages which I noticed on the matrix builder to use up a lot of solver-time is I tried solving locally with whereas without this PR, cabal gave up after 16 minutes: Here's a list of the worst solve-times from matrix.hho (w/o this PR) resulting in solver failures:
|
|
+1, merge at will. ... but I get the feeling that we should be looking towards SAT solvers/"Theorem Provers". Even assuming awful error messages, I get the feeling that Cabal would be up a couple of points in terms of "just working". That's just my (maybe-uninformed) opinion. Thoughts, anyone? |
|
@BardurArantsson There were several attempts at using a stock SAT/SMT solver (including Z3). Unfortunately, while e.g. Z3 is very fast to find some arbitrary solution (after having fed the facts into the Z3 process which takes a bit of time too), the problem is rather having the SMT solver optimize for a reasonable cost-function, as then its performance takes a substantial dive (at least for the attempts I'm aware of) to the point where the domain-specific modular cabal solver looks way better in comparison. |
|
@hvr Ah, thanks for reminding me of the intricacies. (Still +1 to this PR, btw.) Hopefully a |
|
@hvr Thanks for testing the PR on I tried out the idea I mentioned in the last comment, and it seems promising. I added information about version conflicts to the variables in conflict sets, so that the solver can determine whether each version of a package will cause the same conflicts as the previous version that it tried. If a version causes the same conflicts, then the solver can skip it. Then I reran
The new branch was also about 25% faster when solving for |
|
@grayjay btw, while you're working on the solver... how hard would it be to emit simple stats about the "solver" costs, like e.g. how much backjump-budget was required for a decision (i.e. the smallest value to pass via --max-backjumps so that the solver would give a definitive answer - instead of giving up with a non-exhaustive "don't know"?) The reason is that I want to collect such statistics in http://matrix.hackage.haskell.org in order to spot problematic cases; currently, I can only collect the rather crude metrics of runtime in seconds & memory allocations (as reported by |
|
I think the discussions about remaining problems and ideas for future improvements should not hold up merging this. It all seems rather good. It's of course very interesting to understand what it is that makes the remaining cases still difficult, and to improve further on this. But I think it is pretty clear due to the testing so far that this is overall a clear improvement. |
|
Since @kosmikus thinks that this PR is good to go, I'm merging it. |
|
Merged, thanks! |
|
Thanks everyone! I'll open issues for the other problems that we discussed when I have time. |
haskell#4562 removed one of PotentialGoal's two fields, so now it is easier to just use the other field's type, FlaggedDep QPN.
haskell#4562 removed one of PotentialGoal's two fields, so now it is easier to just use the other field's type, FlaggedDep QPN.
This PR implements #4391 and fixes #3930 and #4390. It isn't ready to be merged yet, because I need to do some performance testing. The change could have a big impact on solver run time for some packages, since it changes conflict counts. Here are the main commits:
Solver: Add individual flags to conflict sets.
This commit changes the way that the solver tracks the variables that introduce
dependencies, in order to fix some bugs that prevented the solver from tracking
individual flags. I refactored Dep, the type that represents a build-depends or
build-tool-depends dependency, so that it stores the package, flag, and stanza
choices that introduced the dependency. That information is stored in a field
of type DependencyReason. The DependencyReason is available to any solver phase
that needs to create conflict sets, such as "build" or "validation". Whenever
there is a conflict involving a dependency, the solver creates a conflict set
and a log message using the dependency's DependencyReason. This means that the
solver only needs to calculate the dependency reasons once, in
IndexConversion.hs, rather than every time they are used, i.e., in Builder.hs
(for goal reasons), Validate.hs, and Linking.hs.
Another difference between this commit and master is the dependencies between
solver variables. On master, each dependency or variable is introduced by
exactly one other variable. For example, if package x has a flag y, which
controls a dependency on package z, then the three variables depend on each
other in a chain, x -> y -> z. If z can't be satisfied, the solver backjumps
to its cause, y, and if flipping y doesn't help, it continues backjumping to y's
cause, which is x. In contrast, this commit allows each dependency to be
introduced by a package and any number of flags and stanzas. So z's
DependencyReason would contain both x and y.
Storing all flags that introduced a dependency allows the solver to correctly
calculate conflict sets when there are nested conditionals. We no longer need
to combine each package's flags into a single conflict set variable. This
commit removes the
simplifyVarfunction and adds flag variables directly toconflict sets. See issue #4391.
This commit makes another minor change. In this commit and master, if a
dependency appears in the if and else blocks of a conditional, the solver lifts
it out of the conditional. Previously, the solver behaved as if the flag did
not introduce the dependency. This commit adds the flag variable to the
conflict set or error message if the dependency is involved in a conflict. This
change doesn't affect correctness, but I think it improves the error messages,
since it gives the whole reason that each dependency was introduced.
Randomize the goal order in one of the dependency solver QuickCheck tests.
Completely randomizing the goal order exposes more bugs in backjumping than
using --reorder-goals. I only applied the change to one test in this commit,
because the randomization function slowed down some of the other tests
significantly.
Add a test case for issue #4390.
Add a test case for a stanza preference bug (#3930).
Enable stanza preferences in the solver QuickCheck tests.
Here are some examples of changes in solver error messages that also reflect the changes in behavior.
cabal install hackage-server:There are several differences:
hackage-server-0.5.0:build-hackage-buildinstead ofhackage-server-0.5.0:flag.hackage-server-0.5.0:+build-hackage-build, instead of the twohackage-server-0.5.0flags that had been chosen at that point.(conflict: hackage-server +build-hackage-build => aeson==0.6.1.*)instead of(conflict: hackage-server-0.5.0:build-hackage-build => aeson==0.6.1.*).cabal install --dry-run git-annex -v3:networkis introduced by thenetwork-uriflag, whether it is true or false./cc @kosmikus