Vectorise DPOR backtracking

This shaves off 6 seconds.

dejafu/Test/DejaFu/SCT.hs

@@ -29,6 +29,7 @@ import qualified Data.Map.Strict                   as M
 import           Data.Maybe                        (fromMaybe)
 import           Data.Set                          (Set)
 import qualified Data.Set                          as S
+import qualified Data.Vector                       as V
 
 import           Test.DejaFu.Conc
 import           Test.DejaFu.Internal
@@ -225,19 +226,24 @@ cBacktrack :: Bounds -> BacktrackFunc
 cBacktrack (Bounds (Just _) _) bs =
     backtrackAt (\_ _ -> False) bs . concatMap addConservative
   where
+    lbs = V.toList bs
+
     addConservative o@(i, _, tid) = o : case conservative i of
       Just j  -> [(j, True, tid)]
       Nothing -> []
 
     -- index of conservative point
-    conservative i = go (reverse (take (i-1) bs)) (i-1) where
+    conservative i = go (i-2) where
-      go _ (-1) = Nothing
+      go j
-      go (b1:rest@(b2:_)) j
+        | j < 1 = Nothing
-        | bcktThreadid b1 /= bcktThreadid b2
+        | otherwise =
-          && not (isCommitRef $ bcktAction b1)
+          let b1 = bs V.! j
-          && not (isCommitRef $ bcktAction b2) = Just j
+              b2 = bs V.! (j-1)
-        | otherwise = go rest (j-1)
+          in if bcktThreadid b1 /= bcktThreadid b2
-      go _ _ = Nothing
+                && not (isCommitRef $ bcktAction b1)
+                && not (isCommitRef $ bcktAction b2)
+             then Just (j+1)
+             else go (j-1)
 cBacktrack _ bs = backtrackAt (\_ _ -> False) bs
 
 -------------------------------------------------------------------------------

dejafu/Test/DejaFu/SCT/Internal/DPOR.hs

@@ -25,11 +25,12 @@ import           Data.List.NonEmpty   (toList)
 import           Data.Map.Strict      (Map)
 import qualified Data.Map.Strict      as M
 import           Data.Maybe           (isJust, isNothing, listToMaybe,
-                                       maybeToList)
+                                       mapMaybe, maybeToList)
 import           Data.Sequence        (Seq, (|>))
 import qualified Data.Sequence        as Sq
 import           Data.Set             (Set)
 import qualified Data.Set             as S
+import qualified Data.Vector          as V
 import           GHC.Generics         (Generic)
 import           GHC.Stack            (HasCallStack)
 
@@ -246,7 +247,7 @@ findBacktrackSteps
   -> Trace
   -- ^ The execution trace.
   -> [BacktrackStep]
-findBacktrackSteps safeIO memtype backtrack boundKill state0 = go state0 S.empty initialThread [] . F.toList where
+findBacktrackSteps safeIO memtype backtrack boundKill state0 = go state0 S.empty initialThread V.empty . F.toList where
   -- Walk through the traces one step at a time, building up a list of
   -- new backtracking points.
   go state allThreads tid bs ((e,i):is) ((d,_,a):ts) =
@@ -260,32 +261,33 @@ findBacktrackSteps safeIO memtype backtrack boundKill state0 = go state0 S.empty
           , bcktBacktracks = M.fromList $ map (\i' -> (i', False)) i
           , bcktState      = state
           }
-        bs' = doBacktrack killsEarly allThreads' e (bs++[this])
+        bs' = doBacktrack killsEarly allThreads' e (V.snoc bs this)
         runnable = S.fromList (M.keys $ bcktRunnable this)
         allThreads' = allThreads `S.union` runnable
         killsEarly = null ts && boundKill
     in go state' allThreads' tid' bs' is ts
-  go _ _ _ bs _ _ = bs
+  go _ _ _ bs _ _ = V.toList bs
 
   -- Find the prior actions dependent with this one and add
   -- backtracking points.
   doBacktrack killsEarly allThreads enabledThreads bs =
-    let tagged = reverse $ zip [0..] bs
+    let idxs   = [ (i, False, u)
-        idxs   = [ (i, False, u)
                  | (u, n) <- enabledThreads
                  , v <- S.toList allThreads
                  , u /= v
-                 , i <- maybeToList (findIndex u n v tagged)]
+                 , i <- maybeToList (findIndex u n v (V.length bs - 1))]
 
         findIndex u n v = go' where
           {-# INLINE go' #-}
-          go' ((i,b):rest)
+          go' (-1) = Nothing
+          go' i =
+            let b = bs V.! i
             -- If this is the final action in the trace and the
             -- execution was killed due to nothing being within bounds
             -- (@killsEarly == True@) assume worst-case dependency.
-            | bcktThreadid b == v && (killsEarly || isDependent b) = Just i
+            in if bcktThreadid b == v && (killsEarly || isDependent b)
-            | otherwise = go' rest
+               then Just i
-          go' [] = Nothing
+               else go' (i-1)
 
           {-# INLINE isDependent #-}
           isDependent b
@@ -392,7 +394,7 @@ type IncrementalBoundFunc k
 -- backtracking points, and then use @backtrackAt@ to do the actual
 -- work.
 type BacktrackFunc
-  = [BacktrackStep] -> [(Int, Bool, ThreadId)] -> [BacktrackStep]
+  = V.Vector BacktrackStep -> [(Int, Bool, ThreadId)] -> V.Vector BacktrackStep
 
 -- | Add a backtracking point. If the thread isn't runnable, add all
 -- runnable threads. If the backtracking point is already present,
@@ -405,29 +407,21 @@ backtrackAt :: HasCallStack
 backtrackAt toAll bs0 = backtrackAt' . nubBy ((==) `on` fst') . sortOn fst' where
   fst' (x,_,_) = x
 
-  backtrackAt' ((i,c,t):is) = go i bs0 i c t is
+  backtrackAt' is = bs0 V.// mapMaybe go is
-  backtrackAt' [] = bs0
 
-  go i0 (b:bs) 0 c tid is
+  go (i,c,t) =
-    -- If the backtracking point is already present, don't re-add it,
+    let b = bs0 V.! i
-    -- UNLESS this would force it to backtrack (it's conservative)
+    in if not (toAll t b) && t `M.member` bcktRunnable b
-    -- where before it might not.
+       -- If the backtracking point is already present, don't re-add
-    | not (toAll tid b) && tid `M.member` bcktRunnable b =
+       -- it, UNLESS this would force it to backtrack (it's
-      let val = M.lookup tid $ bcktBacktracks b
+       -- conservative) where before it might not.
-          b' = if isNothing val || (val == Just False && c)
+       then
-            then b { bcktBacktracks = backtrackTo tid c b }
+         let val = M.lookup t $ bcktBacktracks b
-            else b
+         in if isNothing val || (val == Just False && c)
-      in b' : case is of
+            then Just (i, b { bcktBacktracks = backtrackTo t c b })
-        ((i',c',t'):is') -> go i' bs (i'-i0-1) c' t' is'
+            else Nothing
-        [] -> bs
+       -- Otherwise just backtrack to everything runnable.
-    -- Otherwise just backtrack to everything runnable.
+       else Just (i, b { bcktBacktracks = backtrackAll c b })
-    | otherwise =
-      let b' = b { bcktBacktracks = backtrackAll c b }
-      in b' : case is of
-        ((i',c',t'):is') -> go i' bs (i'-i0-1) c' t' is'
-        [] -> bs
-  go i0 (b:bs) i c tid is = b : go i0 bs (i-1) c tid is
-  go _ [] _ _ _ _ = fatal "ran out of schedule whilst backtracking!"
 
   -- Backtrack to a single thread
   backtrackTo tid c = M.insert tid c . bcktBacktracks

dejafu/dejafu.cabal

@@ -68,6 +68,7 @@ library
                      , profunctors       >=4.0 && <6
                      , random            >=1.0 && <1.2
                      , transformers      >=0.5 && <0.6
+                     , vector
   -- hs-source-dirs:      
   default-language:    Haskell2010
   ghc-options:         -Wall