From fcb2f7cab1e2e2043f9059167c5fb66cd3d81001 Mon Sep 17 00:00:00 2001
From: Daniel Matichuk <dmatichuk@galois.com>
Date: Thu, 24 Oct 2024 15:56:29 -0700
Subject: [PATCH] Experimenting with some limited parallelism in simple cases

---
 src/Pate/Monad.hs                       | 54 ++++++++++++++++++++++++-
 src/Pate/Verification/StrongestPosts.hs |  7 +++-
 src/Pate/Verification/Widening.hs       |  2 +-
 3 files changed, 59 insertions(+), 4 deletions(-)

diff --git a/src/Pate/Monad.hs b/src/Pate/Monad.hs
index 09318010..2426dd4e 100644
--- a/src/Pate/Monad.hs
+++ b/src/Pate/Monad.hs
@@ -106,7 +106,10 @@ module Pate.Monad
   , withSharedEnvEmit
   , module PME
   , atPriority, currentPriority, thisPriority
-  , concretizeWithSolverBatch
+  , concretizeWithSolverBatch 
+  , withFreshSolver
+  , forkBins
+  , withForkedSolver
   )
   where
 
@@ -1611,3 +1614,52 @@ equivalenceContext = withValid $ do
   PA.SomeValidArch d <- CMR.asks envValidArch
   stackRegion <- CMR.asks (PMC.stackRegion . PME.envCtx)
   return $ PEq.EquivContext (PA.validArchDedicatedRegisters d) stackRegion (\x -> x)
+
+
+-- | Run the given continuation with a fresh solver process (without affecting the
+--   current solver process). The new process will inherit the current assumption
+--   context.
+withFreshSolver ::
+  EquivM_ sym arch a ->
+  EquivM sym arch a
+withFreshSolver f = do
+  vcfg <- CMR.asks envConfig
+  let solver = PC.cfgSolver vcfg
+  PSo.Sym n sym _ <- CMR.asks envValidSym
+  asm <- currentAsm
+  PSo.withOnlineSolver solver Nothing sym $ \bak ->
+    CMR.local (\env -> env {envValidSym = PSo.Sym n sym bak, envCurrentFrame = mempty }) $ 
+      withAssumptionSet asm $ f
+
+-- | Run the given computation in a forked thread with a fresh solver process.
+--   This is non-blocking and the current solver process is left unmodified.
+withForkedSolver ::
+  EquivM_ sym arch () ->
+  EquivM sym arch ()
+withForkedSolver f = do
+  thistid <- IO.liftIO $ IO.myThreadId
+  _ <- IO.withRunInIO $ \runInIO -> 
+    IO.forkFinally (runInIO $ withFreshSolver f)
+      (\case Left err -> IO.throwTo thistid err; Right () -> return ())
+  return ()
+
+-- | Similar to 'forBins' but runs the 'Patched' process in a separate thread
+--   concurrently with a fresh solver process.
+forkBins ::
+   (forall bin. PBi.WhichBinaryRepr bin -> EquivM_ sym arch (f bin)) ->
+   EquivM sym arch (PPa.PatchPair f)
+forkBins f = do
+  (resO, resP) <- do
+    thistid <- IO.liftIO $ IO.myThreadId
+    outVar2 <- IO.liftIO $ IO.newEmptyMVar
+    _ <- IO.withRunInIO $ \runInIO -> 
+      IO.forkFinally (runInIO $ withFreshSolver $ (PPa.catchPairErr (Just <$> f PBi.PatchedRepr) (return Nothing)))
+        (\case Left err -> IO.throwTo thistid err; Right a -> IO.putMVar outVar2 a)
+    resO <- PPa.catchPairErr (Just <$> f PBi.OriginalRepr) (return Nothing)
+    resP <- IO.liftIO $ IO.readMVar outVar2
+    return (resO, resP)
+  case (resO, resP) of
+    (Just vO, Just vP) -> return $ PPa.PatchPair vO vP
+    (Nothing, Just vP) -> return $ PPa.PatchPairPatched vP
+    (Just vO, Nothing) -> return $ PPa.PatchPairOriginal vO
+    (Nothing, Nothing) -> PPa.throwPairErr
diff --git a/src/Pate/Verification/StrongestPosts.hs b/src/Pate/Verification/StrongestPosts.hs
index 8197d59d..530e79c0 100644
--- a/src/Pate/Verification/StrongestPosts.hs
+++ b/src/Pate/Verification/StrongestPosts.hs
@@ -1319,8 +1319,11 @@ getTracesForPred ::
   EquivM sym arch (Maybe (CE.TraceEvents sym arch), Maybe (CE.TraceEvents sym arch))
 getTracesForPred scope bundle dom p = withSym $ \sym -> do
   not_p <- liftIO $ W4.notPred sym p
-  p_pretty <- PSi.applySimpStrategy PSi.prettySimplifier p
-  withTracing @"expr" (Some p_pretty) $ do
+  -- p_pretty <- withTracing @"debug" "simplifier" $ PSi.applySimpStrategy PSi.prettySimplifier p
+  withTracing @"message" "Traces" $ do
+    withTracing @"message" "Condition" $ withForkedSolver $ do
+      p_pretty <- withTracing @"debug" "simplifier" $ PSi.applySimpStrategy PSi.prettySimplifier p
+      emitTrace @"expr" (Some p_pretty)
     mtraceT <- withTracing @"message" "With condition assumed" $ 
       withSatAssumption (PAS.fromPred p) $ do
         traceT <- getSomeGroundTrace scope bundle dom Nothing
diff --git a/src/Pate/Verification/Widening.hs b/src/Pate/Verification/Widening.hs
index 0df285a1..10b48c94 100644
--- a/src/Pate/Verification/Widening.hs
+++ b/src/Pate/Verification/Widening.hs
@@ -1652,7 +1652,7 @@ getInitalAbsDomainVals bundle preDom = withTracing @"debug" "getInitalAbsDomainV
   getConcreteRange <- PAD.mkGetAbsRange (\es -> TFC.fmapFC (PAD.extractAbsRange sym) <$> concretizeWithSolverBatch es)
   
   eqCtx <- equivalenceContext
-  PPa.forBins $ \bin -> do
+  forkBins $ \bin -> do
     out <- PPa.get bin (PS.simOut bundle)
     pre <- PPa.get bin (PAD.absDomVals preDom)