Use several SMT solvers in parallel #180
Conversation
There was a problem hiding this comment.
As @Niols pointed out, PureSMT is not so pure anymore, so we might want to change its name ...
Also note GitHub's code previewing doesn't necessarily encapsulate all the relevant code so I recommend reading this in the "Files changed" tab.
| runActions Fail = return Fail | ||
| runActions (Yield x l) = Yield x <$> runActions l | ||
| runActions (Weight w l) = Weight w <$> runActions l | ||
| runActions (Action a) = a >>= runActions |
There was a problem hiding this comment.
We switch from WeightedList === WeightedListT Identity to WeightedListT IO but the latter isn't an instance of the Traversable class required by mapConcurrently, hence we need a function to convert it back to a WeightedList (which is Traversable).
|
|
||
| runSymEvalRaw :: | ||
| (SymEvalConstr lang) => | ||
| SymEvalEnv lang -> | ||
| SymEvalSt lang -> | ||
| SymEval lang a -> | ||
| WeightedList (a, SymEvalSt lang) | ||
| WeightedListT IO (a, SymEvalSt lang) |
There was a problem hiding this comment.
A SymEval is now a function which returns a WeightedListT IO hence we change the type here accordingly.
| @@ -174,20 +177,20 @@ runSymEvalWorker :: | |||
| PrtOrderedDefs lang -> | |||
| SymEvalSt lang -> | |||
| SymEval lang a -> | |||
| WeightedList (Path lang a) | |||
| IO (WeightedList (Path lang a)) | |||
There was a problem hiding this comment.
Since we get a WeightedListT IO from running the computations inside the SymEval monad, we need an additional IO computation to get a WeightedList.
| let solvers = SymEvalSolvers (sharedSolve . CheckPath) (sharedSolve . CheckProperty) | ||
| workers <- PureSMT.initAll (optsPureSMT opts) solverCtx | ||
| let asyncSolver :: forall t res. Traversable t => t (SolverProblem lang res) -> IO (t res) | ||
| asyncSolver = PureSMT.solve workers |
There was a problem hiding this comment.
The split between PureSMT.initAll and PureSMT.solve is reflected here.
| solvPair <- runSymEvalRaw (SymEvalEnv defs solvers opts) st' f | ||
| let paths = uncurry (path $ shouldStop opts) solvPair | ||
| return paths | ||
| solvPairs <- ListT.runActions $ runSymEvalRaw (SymEvalEnv defs solvers asyncSolver opts) st' f |
There was a problem hiding this comment.
We use runActions to convert from WeightedListT IO a to IO (WeightedList a).
| IncorrectnessResult lang | ||
| runIncorrectnessLogic opts prog parms = | ||
| runIdentity $ execIncorrectnessLogic (proveAny opts isCounter) prog parms | ||
| IO (IncorrectnessResult lang) |
There was a problem hiding this comment.
Same comment, it seems adding the IO wrapper here is enough for the code to compile.
| solveOpts :: forall domain res. Options -> Solve domain => Ctx domain -> Problem domain res -> res | ||
| solveOpts opts ctx = unsafePerformIO $ do | ||
| -- we end up with a list of MVars, which we will protect in another MVar. | ||
| allProcs <- initAll @domain opts ctx >>= newMStack |
There was a problem hiding this comment.
Since we're propagating IO back into Pirouette's core, there's no need to call initAll when calling solveOpts, so I split these two functions.
| r <- solveProblem @domain problem solver | ||
| return r | ||
| pushMStack ms allProcs | ||
| solve :: forall domain res t. Solve domain => MStack (MVar X.Solver) -> Traversable t => t (Problem domain res) -> IO (t res) |
There was a problem hiding this comment.
The solve function now only takes as input the pool of worker and the problems to solve. The solver options are used when creating the pool of worker inside initAll.
| where | ||
| nWorkers :: Int | ||
| nWorkers = maybe numCapabilities ensurePos (numWorkers opts) |
There was a problem hiding this comment.
numCapabilties is only evaluated at compile time and the result may differ from what's actually available at run time, hence getNumCapabilities is preferred.
| initAll :: forall domain. Options -> Solve domain => Ctx domain -> IO (MStack (MVar X.Solver)) | ||
| initAll opts ctx = | ||
| newMStack =<< do | ||
| nWorkers <- ensurePos <$> maybe getNumCapabilities return (numWorkers opts) |
There was a problem hiding this comment.
Note that getNumCapabilities evaluates to 1 on my laptop, so I actually had to override numWorkers to get multiple workers. setNumCapabilities might also be need to tell Haskell we're running things in parallel.
The purpose of this PR is to describe my implementation of parallelism inside Pirouette. It is not fully working, and is based on the
niols/just-be-bourrinbranch which implements checking for satisfiability at every node instead of every leaf of the symbolic execution tree. I'll comment my change in subsequent messages.