Adding Concurrency/Parallelism in Query Mode

[doyougnu]

Hey Levent,

This is a feature request that I am more than willing to submit a pull request for. I've been messing around with using monad-control in combination with sbv's query mode to try to spin up several z3 instances concurrently. Here is the overview of how I've been thinking about this:

1. Start a symbolic computation and do some symbolic computation
2. in (1) enter query mode

3. The user can then call a new function like forkQ :: Query a -> Query b -> Query (a,b) which will:

   1. will take two more query computations,
   2. clone the query state and the symbolic state,
   3. Spawn two threads and set the states in the query and symbolic monad from 2
   4. concurrently compute both computations, blocking until they both return (just like concurrently in Control.Concurrent.Async.

   A crucial constraint is that the query computations are independent and are not expected to communicate with one another. Rather, they are concurrently finding two solutions to a related problem. I suspect there should be performance benefits because the second query computation does not have to wait for the first one to terminate, as it must in single threaded mode.

Adding the ability to fork off threads in query mode theoretically simple to do by using monad-control with the following type class instances:

instance MonadBase b m => MonadBase b (I.QueryT m) where
  liftBase = lift . liftBase

instance MonadTransControl I.QueryT where
  type StT I.QueryT a = StT (ReaderT I.State) a
  liftWith = defaultLiftWith I.QueryT I.runQueryT
  restoreT = defaultRestoreT I.QueryT

instance MonadBaseControl b m => MonadBaseControl b (I.QueryT m) where
  type StM (I.QueryT m) a = ComposeSt I.QueryT m a
  liftBaseWith            = defaultLiftBaseWith
  restoreM                = defaultRestoreM

instance MonadBase b m => MonadBase b (Ts.SymbolicT m) where
  liftBase = lift . liftBase

instance MonadTransControl Ts.SymbolicT where
  type StT Ts.SymbolicT a = StT (ReaderT I.State) a
  liftWith = defaultLiftWith Ts.SymbolicT Ts.runSymbolicT
  restoreT = defaultRestoreT Ts.SymbolicT

instance MonadBaseControl b m => MonadBaseControl b (Ts.SymbolicT m) where
  type StM (Ts.SymbolicT m) a = ComposeSt Ts.SymbolicT m a
  liftBaseWith                = defaultLiftBaseWith
  restoreM                    = defaultRestoreM

and now one can call forkIO or concurrently by "unlifting":

import Control.Monad.Trans.Control (control)
import Control.Concurrent.Async (concurrently)

forkQ :: Query a -> Query b -> Query (a, b)
forkQ a b = control $ \runInIO ->
                        runInIO $ liftIO $
                        concurrently (runInIO $! a) (runInIO $! b)

this should capture the queryState in QueryT transformer, and then reconstruct the transformer after running the inner two computations in IO. If there are more layers between IO and QueryT then it should unlift appropriately.

But in my experimentation this isn't working. It seems as though there is only ever one z3 instance that is spawned rather than one z3 instance for each thread, which is my desired behavior (and I think is required for sound results). So I tried to thread the State in SymbolicT and QueryT manually but I did not see any ability to do something like setQueryEnv :: MonadQuery m => State -> m ()or setSymbolicEnv :: MonadSymbolic m => State -> m () in the source code.

So I'm stuck on 3.2 above because I am unsure how to spawn a new z3 instance and supply it with a state I am trying to thread through.

Any help appreciated.

[LeventErkok]

I suspect you only get one instance of z3 because the solver connection starts at the very beginning when the symbolic computation starts. Once your query is executing, the instance of z3 is already running. To implement what you want, I think one would need to change how runQuery stuff works to allow for multiple spawnings of the solver as necessary.

However, I'd recommend thinking this approach through: It occurs to me that sharing the symbolic computation part might be optimizing for the wrong thing: In my experience, for big problems, the symbolic computation part is hardly the problem. So, why bother trying to save that work? I think you should seriously consider just duplicating that part, and simply using good old GHC concurrency to attack the problem. You can even make those queries talk to each other via shared concurrency if needed, which I think would lead to a much more scalable system. So, I'd think twice and make sure the bottleneck is really the symbolic computation instead of the actual solving time. I think you'll find it's the latter that costs you more, not the former.

[doyougnu]

Hey Levent,

Your recommendations were spot on. Not only did duplicating the symbolic computation part lead to a a more simple implementation but also simplified a ton of extra logistics I was forced into doing.

For anyone else who might stumble upon this here is my method:

1. Perform the symbolic computation to get a Symbolic a
2. Spin up a bunch of threads with calls to runSMT in them
3. I'm using Control.Concurrent.Chan's and so each thread blocks on a channel, with the channel passing a Query a. My Threads don't need to talk to each other so I have them write out to a result channel. But each thread will receive a Query a and then run a z3 instance like this:

worker :: Symbolic a -> Chan (MyState, Query a) -> IO ThreadId
worker symbolicProp requestChan =
  forkIO $ forever $ do
  (st, qry) <- readChan requestChan
  runSMT $! do prop' <- prop
                 query $! St.evalStateT qry st

I have to carry some extra state around and so I just thread that through with the channel, and each Query a computation can write out to my channels like this:

...
-- deep in my query computation
         chan' <- gets workerChan
         st <- get
         -- once I have found a new query problem I write it out to the channel
         liftIO $! writeChan chan' (st, newQueryProblem)
-- then I simply continue with the query computation I'm working on
...

According to my benchmarks this scales up well. As Levent stated, loading the z3 instance with the Symbolic a computation is non-dominating, although I do not have evidence to actually make that claim.

4. In main I spin up listener threads to block, waiting for n results, which is however many the user want.

As always thanks for the great help,

Jeff

[LeventErkok]

Fantastic! I think there's a re-usable combinator here that would be a very welcome addition to the SBV library. (Along the lines of proveWithAll/proveWithAny and their sat friends.) The exact API might take a bit of experimenting to figure out, but I'd strongly recommend pursuing it and sending a pull-request.

I'm re-opening this ticket: We can close it when that PR comes, or if you find out that there isn't really a good API in there for generic usage.

[doyougnu]

Closing this issue after PR #504 merge.

[LeventErkok]

Fantastic. Thanks!