Skip to content

Fix space leak in solver backjumping #2916

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Merged
merged 2 commits into from
Mar 4, 2016
Merged

Fix space leak in solver backjumping #2916

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
2 commits
Select commit Hold shift + click to select a range
37f28f2
Fix space leaks in dependency solver logging.
grayjay Nov 6, 2015
8923a46
Fix space leak in solver backjumping
grayjay Nov 8, 2015
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
128 changes: 50 additions & 78 deletions cabal-install/Distribution/Client/Dependency/Modular/Explore.hs
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -1,11 +1,9 @@
module Distribution.Client.Dependency.Modular.Explore
( backjump
, exploreTreeLog
, backjumpAndExplore
) where

import Control.Applicative as A
import Data.Foldable
import Data.List as L
import Data.Foldable as F
import Data.Map as M
import Data.Set as S

Expand All @@ -16,107 +14,81 @@ import Distribution.Client.Dependency.Modular.Message
import Distribution.Client.Dependency.Modular.Package
import qualified Distribution.Client.Dependency.Modular.PSQ as P
import Distribution.Client.Dependency.Modular.Tree
import qualified Distribution.Client.Dependency.Types as T

-- | Backjumping.
-- | This function takes the variable we're currently considering and a
-- list of children's logs. Each log yields either a solution or a
-- conflict set. The result is a combined log for the parent node that
-- has explored a prefix of the children.
--
-- A tree traversal that tries to propagate conflict sets
-- up the tree from the leaves, and thereby cut branches.
-- All the tricky things are done in the function 'combine'.
backjump :: Tree a -> Tree (Maybe (ConflictSet QPN))
backjump = snd . cata go
where
go (FailF c fr) = (Just c, Fail c fr)
go (DoneF rdm ) = (Nothing, Done rdm)
go (PChoiceF qpn _ ts) = (c, PChoice qpn c (P.fromList ts'))
where
~(c, ts') = combine (P qpn) (P.toList ts) S.empty
go (FChoiceF qfn _ b m ts) = (c, FChoice qfn c b m (P.fromList ts'))
where
~(c, ts') = combine (F qfn) (P.toList ts) S.empty
go (SChoiceF qsn _ b ts) = (c, SChoice qsn c b (P.fromList ts'))
where
~(c, ts') = combine (S qsn) (P.toList ts) S.empty
go (GoalChoiceF ts) = (c, GoalChoice (P.fromList ts'))
where
~(cs, ts') = unzip $ L.map (\ (k, (x, v)) -> (x, (k, v))) $ P.toList ts
c = case cs of [] -> Nothing
d : _ -> d

-- | The 'combine' function is at the heart of backjumping. It takes
-- the variable we're currently considering, and a list of children
-- annotated with their respective conflict sets, and an accumulator
-- for the result conflict set. It returns a combined conflict set
-- for the parent node, and a (potentially shortened) list of children
-- with the annotations removed.
--
-- It is *essential* that we produce the results as early as possible.
-- In particular, we have to produce the list of children prior to
-- traversing the entire list -- otherwise we lose the desired behaviour
-- of being able to traverse the tree from left to right incrementally.
--
-- We can shorten the list of children if we find an individual conflict
-- set that does not contain the current variable. In this case, we can
-- just lift the conflict set to the current level, because the current
-- level cannot possibly have contributed to this conflict, so no other
-- choice at the current level would avoid the conflict.
-- We can stop traversing the children's logs if we find an individual
-- conflict set that does not contain the current variable. In this
-- case, we can just lift the conflict set to the current level,
-- because the current level cannot possibly have contributed to this
-- conflict, so no other choice at the current level would avoid the
-- conflict.
--
-- If any of the children might contain a successful solution
-- (indicated by Nothing), then Nothing will be the combined
-- conflict set. If all children contain conflict sets, we can
-- If any of the children might contain a successful solution, we can
-- return it immediately. If all children contain conflict sets, we can
-- take the union as the combined conflict set.
combine :: Var QPN -> [(a, (Maybe (ConflictSet QPN), b))] ->
ConflictSet QPN -> (Maybe (ConflictSet QPN), [(a, b)])
combine _ [] c = (Just c, [])
combine var ((k, ( d, v)) : xs) c = (\ ~(e, ys) -> (e, (k, v) : ys)) $
case d of
Just e | not (simplifyVar var `S.member` e) -> (Just e, [])
| otherwise -> combine var xs (e `S.union` c)
Nothing -> (Nothing, snd $ combine var xs S.empty)
backjump :: F.Foldable t => Var QPN -> t (ConflictSetLog a) -> ConflictSetLog a
backjump var xs = F.foldr combine backjumpInfo xs S.empty
where
combine :: ConflictSetLog a
-> (ConflictSet QPN -> ConflictSetLog a)
-> ConflictSet QPN -> ConflictSetLog a
combine (T.Done x) _ _ = T.Done x
combine (T.Fail cs) f csAcc
| not (simplifyVar var `S.member` cs) = backjumpInfo cs
| otherwise = f (csAcc `S.union` cs)
combine (T.Step m ms) f cs = T.Step m (combine ms f cs)

type ConflictSetLog = T.Progress Message (ConflictSet QPN)

-- | Version of 'explore' that returns a 'Log'.
exploreLog :: Tree (Maybe (ConflictSet QPN)) ->
(Assignment -> Log Message (Assignment, RevDepMap))
-- | A tree traversal that simultaneously propagates conflict sets up
-- the tree from the leaves and creates a log.
exploreLog :: Tree a -> (Assignment -> ConflictSetLog (Assignment, RevDepMap))
exploreLog = cata go
where
go (FailF c fr) _ = failWith (Failure c fr)
go :: TreeF a (Assignment -> ConflictSetLog (Assignment, RevDepMap))
-> (Assignment -> ConflictSetLog (Assignment, RevDepMap))
go (FailF c fr) _ = failWith (Failure c fr) c
go (DoneF rdm) a = succeedWith Success (a, rdm)
go (PChoiceF qpn c ts) (A pa fa sa) =
backjumpInfo c $
asum $ -- try children in order,
go (PChoiceF qpn _ ts) (A pa fa sa) =
backjump (P qpn) $ -- try children in order,
P.mapWithKey -- when descending ...
(\ i@(POption k _) r -> tryWith (TryP qpn i) $ -- log and ...
(\ i@(POption k _) r -> tryWith (TryP qpn i) $ -- log and ...
r (A (M.insert qpn k pa) fa sa)) -- record the pkg choice
ts
go (FChoiceF qfn c _ _ ts) (A pa fa sa) =
backjumpInfo c $
asum $ -- try children in order,
go (FChoiceF qfn _ _ _ ts) (A pa fa sa) =
backjump (F qfn) $ -- try children in order,
P.mapWithKey -- when descending ...
(\ k r -> tryWith (TryF qfn k) $ -- log and ...
r (A pa (M.insert qfn k fa) sa)) -- record the pkg choice
ts
go (SChoiceF qsn c _ ts) (A pa fa sa) =
backjumpInfo c $
asum $ -- try children in order,
go (SChoiceF qsn _ _ ts) (A pa fa sa) =
backjump (S qsn) $ -- try children in order,
P.mapWithKey -- when descending ...
(\ k r -> tryWith (TryS qsn k) $ -- log and ...
r (A pa fa (M.insert qsn k sa))) -- record the pkg choice
ts
go (GoalChoiceF ts) a =
P.casePSQ ts
(failWith (Failure S.empty EmptyGoalChoice)) -- empty goal choice is an internal error
(\ k v _xs -> continueWith (Next (close k)) (v a)) -- commit to the first goal choice
(failWith (Failure S.empty EmptyGoalChoice) S.empty) -- empty goal choice is an internal error
(\ k v _xs -> continueWith (Next (close k)) (v a)) -- commit to the first goal choice

-- | Add in information about pruned trees.
--
-- TODO: This isn't quite optimal, because we do not merely report the shape of the
-- tree, but rather make assumptions about where that shape originated from. It'd be
-- better if the pruning itself would leave information that we could pick up at this
-- point.
Copy link
Collaborator Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I'm not sure if this comment still applies to this function after I changed it.

backjumpInfo :: Maybe (ConflictSet QPN) -> Log Message a -> Log Message a
backjumpInfo c m = m <|> case c of -- important to produce 'm' before matching on 'c'!
Nothing -> A.empty
Just cs -> failWith (Failure cs Backjump)
backjumpInfo :: ConflictSet QPN -> ConflictSetLog a
backjumpInfo cs = failWith (Failure cs Backjump) cs

-- | Interface.
exploreTreeLog :: Tree (Maybe (ConflictSet QPN)) -> Log Message (Assignment, RevDepMap)
exploreTreeLog t = exploreLog t (A M.empty M.empty M.empty)
backjumpAndExplore :: Tree a -> Log Message (Assignment, RevDepMap)
backjumpAndExplore t = toLog $ exploreLog t (A M.empty M.empty M.empty)
where
toLog :: T.Progress step fail done -> Log step done
toLog = T.foldProgress T.Step (const (T.Fail ())) T.Done
134 changes: 64 additions & 70 deletions cabal-install/Distribution/Client/Dependency/Modular/Log.hs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -9,6 +9,7 @@ module Distribution.Client.Dependency.Modular.Log

import Control.Applicative
import Data.List as L
import Data.Maybe (isNothing)
import Data.Set as S

import Distribution.Client.Dependency.Types -- from Cabal
Expand All @@ -25,88 +26,81 @@ import Distribution.Client.Dependency.Modular.Tree (FailReason(..))
-- Parameterized over the type of actual messages and the final result.
type Log m a = Progress m () a

-- | Turns a log into a list of messages paired with a final result. A final result
-- of 'Nothing' indicates failure. A final result of 'Just' indicates success.
-- Keep in mind that forcing the second component of the returned pair will force the
-- entire log.
runLog :: Log m a -> ([m], Maybe a)
runLog (Done x) = ([], Just x)
runLog (Fail _) = ([], Nothing)
runLog (Step m p) = let
(ms, r) = runLog p
in
(m : ms, r)
messages :: Progress step fail done -> [step]
messages = foldProgress (:) (const []) (const [])

-- | Postprocesses a log file. Takes as an argument a limit on allowed backjumps.
-- If the limit is 'Nothing', then infinitely many backjumps are allowed. If the
-- limit is 'Just 0', backtracking is completely disabled.
logToProgress :: Maybe Int -> Log Message a -> Progress String String a
logToProgress mbj l = let
(ms, s) = runLog l
-- 'Nothing' for 's' means search tree exhaustively searched and failed
(es, e) = proc 0 ms -- catch first error (always)
-- 'Nothing' in 'e' means no backjump found
(ns, t) = case mbj of
Nothing -> (ms, Nothing)
Just n -> proc n ms
-- 'Nothing' in 't' means backjump limit not reached
-- prefer first error over later error
(exh, r) = case t of
-- backjump limit not reached
Nothing -> case s of
Nothing -> (True, e) -- failed after exhaustive search
Just _ -> (True, Nothing) -- success
-- backjump limit reached; prefer first error
Just _ -> (False, e) -- failed after backjump limit was reached
es = proc (Just 0) l -- catch first error (always)
ms = useFirstError (proc mbj l)
in go es es -- trace for first error
(showMessages (const True) True ns) -- shortened run
r s exh
(showMessages (const True) True ms) -- run with backjump limit applied
where
-- Proc takes the allowed number of backjumps and a list of messages and explores the
-- message list until the maximum number of backjumps has been reached. The log until
-- that point as well as whether we have encountered an error or not are returned.
proc :: Int -> [Message] -> ([Message], Maybe (ConflictSet QPN))
proc _ [] = ([], Nothing)
proc n ( Failure cs Backjump : xs@(Leave : Failure cs' Backjump : _))
| cs == cs' = proc n xs -- repeated backjumps count as one
proc 0 ( Failure cs Backjump : _ ) = ([], Just cs)
proc n (x@(Failure _ Backjump) : xs) = (\ ~(ys, r) -> (x : ys, r)) (proc (n - 1) xs)
proc n (x : xs) = (\ ~(ys, r) -> (x : ys, r)) (proc n xs)
-- Proc takes the allowed number of backjumps and a 'Progress' and explores the
-- messages until the maximum number of backjumps has been reached. It filters out
-- and ignores repeated backjumps. If proc reaches the backjump limit, it truncates
-- the 'Progress' and ends it with the last conflict set. Otherwise, it leaves the
-- original success result or replaces the original failure with 'Nothing'.
proc :: Maybe Int -> Progress Message a b -> Progress Message (Maybe (ConflictSet QPN)) b
proc _ (Done x) = Done x
proc _ (Fail _) = Fail Nothing
proc mbj' (Step (Failure cs Backjump) xs@(Step Leave (Step (Failure cs' Backjump) _)))
| cs == cs' = proc mbj' xs -- repeated backjumps count as one
proc (Just 0) (Step (Failure cs Backjump) _) = Fail (Just cs)
proc (Just n) (Step x@(Failure _ Backjump) xs) = Step x (proc (Just (n - 1)) xs)
proc mbj' (Step x xs) = Step x (proc mbj' xs)

-- This function takes a lot of arguments. The first two are both supposed to be
-- the log up to the first error. That's the error that will always be printed in
-- case we do not find a solution. We pass this log twice, because we evaluate it
-- in parallel with the full log, but we also want to retain the reference to its
-- beginning for when we print it. This trick prevents a space leak!
--
-- The third argument is the full log, the fifth and six error conditions.
-- The seventh argument indicates whether the search was exhaustive.
-- Sets the conflict set from the first backjump as the final error, and records
-- whether the search was exhaustive.
useFirstError :: Progress Message (Maybe (ConflictSet QPN)) b
-> Progress Message (Bool, Maybe (ConflictSet QPN)) b
useFirstError = replace Nothing
where
replace _ (Done x) = Done x
replace cs' (Fail cs) = -- 'Nothing' means backjump limit not reached.
-- Prefer first error over later error.
Fail (isNothing cs, cs' <|> cs)
replace Nothing (Step x@(Failure cs Backjump) xs) = Step x $ replace (Just cs) xs
replace cs' (Step x xs) = Step x $ replace cs' xs

-- The first two arguments are both supposed to be the log up to the first error.
-- That's the error that will always be printed in case we do not find a solution.
-- We pass this log twice, because we evaluate it in parallel with the full log,
-- but we also want to retain the reference to its beginning for when we print it.
-- This trick prevents a space leak!
--
-- The order of arguments is important! In particular 's' must not be evaluated
-- unless absolutely necessary. It contains the final result, and if we shortcut
-- with an error due to backjumping, evaluating 's' would still require traversing
-- the entire tree.
go ms (_ : ns) (x : xs) r s exh = Step x (go ms ns xs r s exh)
go ms [] (x : xs) r s exh = Step x (go ms [] xs r s exh)
go ms _ [] (Just cs) _ exh = Fail $
"Could not resolve dependencies:\n" ++
unlines (showMessages (L.foldr (\ v _ -> v `S.member` cs) True) False ms) ++
(if exh then "Dependency tree exhaustively searched.\n"
else "Backjump limit reached (" ++ currlimit mbj ++
"change with --max-backjumps or try to run with --reorder-goals).\n")
where currlimit (Just n) = "currently " ++ show n ++ ", "
currlimit Nothing = ""
go _ _ [] _ (Just s) _ = Done s
go _ _ [] _ _ _ = Fail ("Could not resolve dependencies; something strange happened.") -- should not happen
-- The third argument is the full log, ending with either the solution or the
-- exhaustiveness and first conflict set.
go :: Progress Message a b
-> Progress Message a b
-> Progress String (Bool, Maybe (ConflictSet QPN)) b
-> Progress String String b
go ms (Step _ ns) (Step x xs) = Step x (go ms ns xs)
go ms r (Step x xs) = Step x (go ms r xs)
go ms _ (Fail (exh, Just cs)) = Fail $
"Could not resolve dependencies:\n" ++
unlines (messages $ showMessages (L.foldr (\ v _ -> v `S.member` cs) True) False ms) ++
(if exh then "Dependency tree exhaustively searched.\n"
else "Backjump limit reached (" ++ currlimit mbj ++
"change with --max-backjumps or try to run with --reorder-goals).\n")
where currlimit (Just n) = "currently " ++ show n ++ ", "
currlimit Nothing = ""
go _ _ (Done s) = Done s
go _ _ (Fail (_, Nothing)) = Fail ("Could not resolve dependencies; something strange happened.") -- should not happen

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

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

continueWith :: m -> Log m a -> Log m a
continueWith :: step -> Progress step fail done -> Progress step fail done
continueWith = Step

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