Skip to content

Commit c1189c3

Browse files
grayjaygrayjay
committed
Fix space leak in solver backjumping
This commit refactors backjumping so that it uses the 'Progress' type instead of separate references to a node's children and the conflict set calculated from those children.
1 parent 90c7772 commit c1189c3

File tree

3 files changed

+59
-115
lines changed

3 files changed

+59
-115
lines changed

‎cabal-install/Distribution/Client/Dependency/Modular/Explore.hs

Lines changed: 48 additions & 106 deletions
Original file line numberDiff line numberDiff line change
@@ -1,8 +1,6 @@
11
module Distribution.Client.Dependency.Modular.Explore where
22

3-
import Control.Applicative as A
4-
import Data.Foldable
5-
import Data.List as L
3+
import Data.Foldable as F
64
import Data.Map as M
75
import Data.Set as S
86

@@ -13,137 +11,81 @@ import Distribution.Client.Dependency.Modular.Message
1311
import Distribution.Client.Dependency.Modular.Package
1412
import Distribution.Client.Dependency.Modular.PSQ as P
1513
import Distribution.Client.Dependency.Modular.Tree
14+
import qualified Distribution.Client.Dependency.Types as T
1615

17-
-- | Backjumping.
16+
-- | This function takes the variable we're currently considering and a
17+
-- list of children's logs. Each log yields either a solution or a
18+
-- conflict set. The result is a combined log for the parent node that
19+
-- has explored a prefix of the children.
1820
--
19-
-- A tree traversal that tries to propagate conflict sets
20-
-- up the tree from the leaves, and thereby cut branches.
21-
-- All the tricky things are done in the function 'combine'.
22-
backjump :: Tree a -> Tree (Maybe (ConflictSet QPN))
23-
backjump = snd . cata go
24-
where
25-
go (FailF c fr) = (Just c, Fail c fr)
26-
go (DoneF rdm ) = (Nothing, Done rdm)
27-
go (PChoiceF qpn _ ts) = (c, PChoice qpn c (P.fromList ts'))
28-
where
29-
~(c, ts') = combine (P qpn) (P.toList ts) S.empty
30-
go (FChoiceF qfn _ b m ts) = (c, FChoice qfn c b m (P.fromList ts'))
31-
where
32-
~(c, ts') = combine (F qfn) (P.toList ts) S.empty
33-
go (SChoiceF qsn _ b ts) = (c, SChoice qsn c b (P.fromList ts'))
34-
where
35-
~(c, ts') = combine (S qsn) (P.toList ts) S.empty
36-
go (GoalChoiceF ts) = (c, GoalChoice (P.fromList ts'))
37-
where
38-
~(cs, ts') = unzip $ L.map (\ (k, (x, v)) -> (x, (k, v))) $ P.toList ts
39-
c = case cs of [] -> Nothing
40-
d : _ -> d
41-
42-
-- | The 'combine' function is at the heart of backjumping. It takes
43-
-- the variable we're currently considering, and a list of children
44-
-- annotated with their respective conflict sets, and an accumulator
45-
-- for the result conflict set. It returns a combined conflict set
46-
-- for the parent node, and a (potentially shortened) list of children
47-
-- with the annotations removed.
48-
--
49-
-- It is *essential* that we produce the results as early as possible.
50-
-- In particular, we have to produce the list of children prior to
51-
-- traversing the entire list -- otherwise we lose the desired behaviour
52-
-- of being able to traverse the tree from left to right incrementally.
21+
-- We can stop traversing the children's logs if we find an individual
22+
-- conflict set that does not contain the current variable. In this
23+
-- case, we can just lift the conflict set to the current level,
24+
-- because the current level cannot possibly have contributed to this
25+
-- conflict, so no other choice at the current level would avoid the
26+
-- conflict.
5327
--
54-
-- We can shorten the list of children if we find an individual conflict
55-
-- set that does not contain the current variable. In this case, we can
56-
-- just lift the conflict set to the current level, because the current
57-
-- level cannot possibly have contributed to this conflict, so no other
58-
-- choice at the current level would avoid the conflict.
59-
--
60-
-- If any of the children might contain a successful solution
61-
-- (indicated by Nothing), then Nothing will be the combined
62-
-- conflict set. If all children contain conflict sets, we can
28+
-- If any of the children might contain a successful solution, we can
29+
-- return it immediately. If all children contain conflict sets, we can
6330
-- take the union as the combined conflict set.
64-
combine :: Var QPN -> [(a, (Maybe (ConflictSet QPN), b))] ->
65-
ConflictSet QPN -> (Maybe (ConflictSet QPN), [(a, b)])
66-
combine _ [] c = (Just c, [])
67-
combine var ((k, ( d, v)) : xs) c = (\ ~(e, ys) -> (e, (k, v) : ys)) $
68-
case d of
69-
Just e | not (simplifyVar var `S.member` e) -> (Just e, [])
70-
| otherwise -> combine var xs (e `S.union` c)
71-
Nothing -> (Nothing, snd $ combine var xs S.empty)
72-
73-
-- | Naive backtracking exploration of the search tree. This will yield correct
74-
-- assignments only once the tree itself is validated.
75-
explore :: Alternative m => Tree a -> (Assignment -> m (Assignment, RevDepMap))
76-
explore = cata go
31+
backjump :: F.Foldable t => Var QPN -> t (ConflictSetLog a) -> ConflictSetLog a
32+
backjump var xs = F.foldr combine backjumpInfo xs S.empty
7733
where
78-
go (FailF _ _) _ = A.empty
79-
go (DoneF rdm) a = pure (a, rdm)
80-
go (PChoiceF qpn _ ts) (A pa fa sa) =
81-
asum $ -- try children in order,
82-
P.mapWithKey -- when descending ...
83-
(\ (POption k _) r -> r (A (M.insert qpn k pa) fa sa)) -- record the pkg choice
84-
ts
85-
go (FChoiceF qfn _ _ _ ts) (A pa fa sa) =
86-
asum $ -- try children in order,
87-
P.mapWithKey -- when descending ...
88-
(\ k r -> r (A pa (M.insert qfn k fa) sa)) -- record the flag choice
89-
ts
90-
go (SChoiceF qsn _ _ ts) (A pa fa sa) =
91-
asum $ -- try children in order,
92-
P.mapWithKey -- when descending ...
93-
(\ k r -> r (A pa fa (M.insert qsn k sa))) -- record the flag choice
94-
ts
95-
go (GoalChoiceF ts) a =
96-
casePSQ ts A.empty -- empty goal choice is an internal error
97-
(\ _k v _xs -> v a) -- commit to the first goal choice
34+
combine :: ConflictSetLog a
35+
-> (ConflictSet QPN -> ConflictSetLog a)
36+
-> ConflictSet QPN -> ConflictSetLog a
37+
combine (T.Done x) _ _ = T.Done x
38+
combine (T.Fail cs) f csAcc
39+
| not (simplifyVar var `S.member` cs) = backjumpInfo cs
40+
| otherwise = f (csAcc `S.union` cs)
41+
combine (T.Step m ms) f cs = T.Step m (combine ms f cs)
9842

99-
-- | Version of 'explore' that returns a 'Log'.
100-
exploreLog :: Tree (Maybe (ConflictSet QPN)) ->
101-
(Assignment -> Log Message (Assignment, RevDepMap))
43+
type ConflictSetLog = T.Progress Message (ConflictSet QPN)
44+
45+
-- | A tree traversal that simultaneously propagates conflict sets up
46+
-- the tree from the leaves and creates a log.
47+
exploreLog :: Tree a -> (Assignment -> ConflictSetLog (Assignment, RevDepMap))
10248
exploreLog = cata go
10349
where
104-
go (FailF c fr) _ = failWith (Failure c fr)
50+
go :: TreeF a (Assignment -> ConflictSetLog (Assignment, RevDepMap))
51+
-> (Assignment -> ConflictSetLog (Assignment, RevDepMap))
52+
go (FailF c fr) _ = failWith (Failure c fr) c
10553
go (DoneF rdm) a = succeedWith Success (a, rdm)
106-
go (PChoiceF qpn c ts) (A pa fa sa) =
107-
backjumpInfo c $
108-
asum $ -- try children in order,
54+
go (PChoiceF qpn _ ts) (A pa fa sa) =
55+
backjump (P qpn) $ -- try children in order,
10956
P.mapWithKey -- when descending ...
110-
(\ i@(POption k _) r -> tryWith (TryP qpn i) $ -- log and ...
57+
(\ i@(POption k _) r -> tryWith (TryP qpn i) $ -- log and ...
11158
r (A (M.insert qpn k pa) fa sa)) -- record the pkg choice
11259
ts
113-
go (FChoiceF qfn c _ _ ts) (A pa fa sa) =
114-
backjumpInfo c $
115-
asum $ -- try children in order,
60+
go (FChoiceF qfn _ _ _ ts) (A pa fa sa) =
61+
backjump (F qfn) $ -- try children in order,
11662
P.mapWithKey -- when descending ...
11763
(\ k r -> tryWith (TryF qfn k) $ -- log and ...
11864
r (A pa (M.insert qfn k fa) sa)) -- record the pkg choice
11965
ts
120-
go (SChoiceF qsn c _ ts) (A pa fa sa) =
121-
backjumpInfo c $
122-
asum $ -- try children in order,
66+
go (SChoiceF qsn _ _ ts) (A pa fa sa) =
67+
backjump (S qsn) $ -- try children in order,
12368
P.mapWithKey -- when descending ...
12469
(\ k r -> tryWith (TryS qsn k) $ -- log and ...
12570
r (A pa fa (M.insert qsn k sa))) -- record the pkg choice
12671
ts
12772
go (GoalChoiceF ts) a =
12873
casePSQ ts
129-
(failWith (Failure S.empty EmptyGoalChoice)) -- empty goal choice is an internal error
130-
(\ k v _xs -> continueWith (Next (close k)) (v a)) -- commit to the first goal choice
74+
(failWith (Failure S.empty EmptyGoalChoice) S.empty) -- empty goal choice is an internal error
75+
(\ k v _xs -> continueWith (Next (close k)) (v a)) -- commit to the first goal choice
13176

13277
-- | Add in information about pruned trees.
13378
--
13479
-- TODO: This isn't quite optimal, because we do not merely report the shape of the
13580
-- tree, but rather make assumptions about where that shape originated from. It'd be
13681
-- better if the pruning itself would leave information that we could pick up at this
13782
-- point.
138-
backjumpInfo :: Maybe (ConflictSet QPN) -> Log Message a -> Log Message a
139-
backjumpInfo c m = m <|> case c of -- important to produce 'm' before matching on 'c'!
140-
Nothing -> A.empty
141-
Just cs -> failWith (Failure cs Backjump)
83+
backjumpInfo :: ConflictSet QPN -> ConflictSetLog a
84+
backjumpInfo cs = failWith (Failure cs Backjump) cs
14285

14386
-- | Interface.
144-
exploreTree :: Alternative m => Tree a -> m (Assignment, RevDepMap)
145-
exploreTree t = explore t (A M.empty M.empty M.empty)
146-
147-
-- | Interface.
148-
exploreTreeLog :: Tree (Maybe (ConflictSet QPN)) -> Log Message (Assignment, RevDepMap)
149-
exploreTreeLog t = exploreLog t (A M.empty M.empty M.empty)
87+
backjumpAndExplore :: Tree a -> Log Message (Assignment, RevDepMap)
88+
backjumpAndExplore t = toLog $ exploreLog t (A M.empty M.empty M.empty)
89+
where
90+
toLog :: T.Progress step fail done -> Log step done
91+
toLog = T.foldProgress T.Step (const (T.Fail ())) T.Done

‎cabal-install/Distribution/Client/Dependency/Modular/Log.hs

Lines changed: 10 additions & 8 deletions
Original file line numberDiff line numberDiff line change
@@ -19,7 +19,7 @@ import Distribution.Client.Dependency.Modular.Tree (FailReason(..))
1919
-- Parameterized over the type of actual messages and the final result.
2020
type Log m a = Progress m () a
2121

22-
messages :: Progress a b c -> [a]
22+
messages :: Progress step fail done -> [step]
2323
messages = foldProgress (:) (const []) (const [])
2424

2525
-- | Postprocesses a log file. Takes as an argument a limit on allowed backjumps.
@@ -80,14 +80,16 @@ logToProgress mbj l = let
8080
go _ _ (Done s) = Done s
8181
go _ _ (Fail (_, Nothing)) = Fail ("Could not resolve dependencies; something strange happened.") -- should not happen
8282

83-
failWith :: m -> Log m a
84-
failWith m = Step m (Fail ())
83+
failWith :: step -> fail -> Progress step fail done
84+
failWith s f = Step s (Fail f)
8585

86-
succeedWith :: m -> a -> Log m a
87-
succeedWith m x = Step m (Done x)
86+
succeedWith :: step -> done -> Progress step fail done
87+
succeedWith s d = Step s (Done d)
8888

89-
continueWith :: m -> Log m a -> Log m a
89+
continueWith :: step -> Progress step fail done -> Progress step fail done
9090
continueWith = Step
9191

92-
tryWith :: Message -> Log Message a -> Log Message a
93-
tryWith m x = Step m (Step Enter x) <|> failWith Leave
92+
tryWith :: Message
93+
-> Progress Message fail done
94+
-> Progress Message fail done
95+
tryWith m = Step m . Step Enter . foldProgress Step (failWith Leave) Done

‎cabal-install/Distribution/Client/Dependency/Modular/Solver.hs

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -40,7 +40,7 @@ solve sc idx userPrefs userConstraints userGoals =
4040
prunePhase $
4141
buildPhase
4242
where
43-
explorePhase = exploreTreeLog . backjump
43+
explorePhase = backjumpAndExplore
4444
heuristicsPhase = P.firstGoal . -- after doing goal-choice heuristics, commit to the first choice (saves space)
4545
P.deferSetupChoices .
4646
P.deferWeakFlagChoices .

0 commit comments

Comments
 (0)