From da09c2268a6d3f1572043d798132e2753a7c3ea6 Mon Sep 17 00:00:00 2001 From: Michael Walker Date: Sat, 8 Apr 2017 10:34:30 +0100 Subject: [PATCH] Inline the findSchedulePrefix predicate. The function is only used in one place, with a constant predicate. There was no point in it being a parameter. --- dejafu/Test/DejaFu/SCT.hs | 5 +---- dejafu/Test/DejaFu/SCT/Internal.hs | 12 +++--------- 2 files changed, 4 insertions(+), 13 deletions(-) diff --git a/dejafu/Test/DejaFu/SCT.hs b/dejafu/Test/DejaFu/SCT.hs index a1302e9..8d45861 100755 --- a/dejafu/Test/DejaFu/SCT.hs +++ b/dejafu/Test/DejaFu/SCT.hs @@ -332,7 +332,7 @@ sctBound :: MonadRef r n sctBound memtype cb conc = go initialState where -- Repeatedly run the computation gathering all the results and -- traces into a list until there are no schedules remaining to try. - go dp = case nextPrefix dp of + go dp = case findSchedulePrefix dp of Just (prefix, conservative, sleep) -> do (res, s, trace) <- runConcurrent scheduler memtype @@ -348,9 +348,6 @@ sctBound memtype cb conc = go initialState where Nothing -> pure [] - -- Find the next schedule prefix. - nextPrefix = findSchedulePrefix (>=initialThread) - -- The DPOR scheduler. scheduler = dporSched memtype (cBound cb) diff --git a/dejafu/Test/DejaFu/SCT/Internal.hs b/dejafu/Test/DejaFu/SCT/Internal.hs index 26fd1fa..2a29c56 100644 --- a/dejafu/Test/DejaFu/SCT/Internal.hs +++ b/dejafu/Test/DejaFu/SCT/Internal.hs @@ -116,18 +116,12 @@ initialState = DPOR -- to-do set. The intent is to put the system into a new state when -- executed with this initial sequence of scheduling decisions. findSchedulePrefix - :: (ThreadId -> Bool) - -- ^ Some partitioning function, applied to the to-do decisions. If - -- there is an identifier which passes the test, it will be used, - -- rather than any which fail it. This allows a very basic way of - -- domain-specific prioritisation between otherwise equal choices, - -- which may be useful in some cases. - -> DPOR + :: DPOR -> Maybe ([ThreadId], Bool, Map ThreadId ThreadAction) -findSchedulePrefix predicate = listToMaybe . go where +findSchedulePrefix = listToMaybe . go where go dpor = let prefixes = here dpor : map go' (M.toList $ dporDone dpor) - in case concatPartition (\(t:_,_,_) -> predicate t) prefixes of + in case concatPartition (\(t:_,_,_) -> t >= initialThread) prefixes of ([], choices) -> choices (choices, _) -> choices