2015-06-19 18:50:51 +03:00
|
|
|
{-# LANGUAGE Rank2Types #-}
|
|
|
|
|
2015-02-01 04:21:42 +03:00
|
|
|
-- | Systematic testing for concurrent computations.
|
2015-01-31 18:50:54 +03:00
|
|
|
module Test.DejaFu.SCT
|
2015-07-17 00:32:30 +03:00
|
|
|
( -- * Bounded Partial-order Reduction
|
|
|
|
|
|
|
|
-- | We can characterise the state of a concurrent computation by
|
|
|
|
-- considering the ordering of dependent events. This is a partial
|
|
|
|
-- order: independent events can be performed in any order without
|
|
|
|
-- affecting the result, and so are /not/ ordered.
|
|
|
|
--
|
|
|
|
-- Partial-order reduction is a technique for computing these
|
|
|
|
-- partial orders, and only testing one total order for each
|
|
|
|
-- partial order. This cuts down the amount of work to be done
|
|
|
|
-- significantly. /Bounded/ partial-order reduction is a further
|
|
|
|
-- optimisation, which only considers schedules within some bound.
|
|
|
|
--
|
|
|
|
-- This module provides both a generic function for BPOR, and also
|
|
|
|
-- a pre-emption bounding BPOR runner, which is used by the
|
|
|
|
-- "Test.DejaFu" module.
|
|
|
|
|
|
|
|
sctPreBound
|
|
|
|
, sctPreBoundIO
|
|
|
|
|
|
|
|
, BacktrackStep(..)
|
|
|
|
, sctBounded
|
|
|
|
, sctBoundedIO
|
|
|
|
|
|
|
|
-- * Utilities
|
|
|
|
, tidOf
|
|
|
|
, tidTag
|
|
|
|
, decisionOf
|
|
|
|
, activeTid
|
|
|
|
, preEmpCount
|
2015-07-20 17:19:51 +03:00
|
|
|
, initialCVState
|
|
|
|
, updateCVState
|
|
|
|
, willBlock
|
2015-07-17 00:32:30 +03:00
|
|
|
) where
|
|
|
|
|
|
|
|
import Control.Applicative ((<$>), (<*>))
|
2015-07-17 17:34:52 +03:00
|
|
|
import Control.DeepSeq (force)
|
2015-07-20 17:19:51 +03:00
|
|
|
import Data.Maybe (maybeToList)
|
2015-06-19 18:50:51 +03:00
|
|
|
import Test.DejaFu.Deterministic
|
|
|
|
import Test.DejaFu.Deterministic.IO (ConcIO, runConcIO)
|
2015-07-17 00:32:30 +03:00
|
|
|
import Test.DejaFu.SCT.Internal
|
2015-06-19 18:50:51 +03:00
|
|
|
|
|
|
|
-- * Pre-emption bounding
|
|
|
|
|
|
|
|
-- | An SCT runner using a pre-emption bounding scheduler.
|
2015-07-17 00:32:30 +03:00
|
|
|
sctPreBound :: Int -> (forall t. Conc t a) -> [(Either Failure a, Trace)]
|
|
|
|
sctPreBound pb = sctBounded (pbBv pb) pbBacktrack pbInitialise
|
2015-06-19 18:50:51 +03:00
|
|
|
|
|
|
|
-- | Variant of 'sctPreBound' for computations which do 'IO'.
|
2015-07-17 00:32:30 +03:00
|
|
|
sctPreBoundIO :: Int -> (forall t. ConcIO t a) -> IO [(Either Failure a, Trace)]
|
|
|
|
sctPreBoundIO pb = sctBoundedIO (pbBv pb) pbBacktrack pbInitialise
|
|
|
|
|
|
|
|
-- | Check if a schedule is in the bound.
|
|
|
|
pbBv :: Int -> [Decision] -> Bool
|
|
|
|
pbBv pb ds = preEmpCount ds <= pb
|
|
|
|
|
|
|
|
-- | Add a backtrack point, and also conservatively add one prior to
|
|
|
|
-- the most recent transition before that point. This may result in
|
|
|
|
-- the same state being reached multiple times, but is needed because
|
|
|
|
-- of the artificial dependency imposed by the bound.
|
|
|
|
pbBacktrack :: [BacktrackStep] -> Int -> ThreadId -> [BacktrackStep]
|
2015-07-17 17:34:52 +03:00
|
|
|
pbBacktrack bs i tid = backtrack True (backtrack False bs i tid) (maximum js) tid where
|
|
|
|
js = 0:[j | ((_,(t1,_)), (j,(t2,_))) <- (zip <*> tail) . zip [0..] $ tidTag (fst . _decision) 0 bs, t1 /= t2, j < i]
|
2015-07-17 00:32:30 +03:00
|
|
|
|
2015-07-17 17:34:52 +03:00
|
|
|
backtrack c (b:bs) 0 t
|
|
|
|
| t `elem` _runnable b = b { _backtrack = (if any ((==t) . fst) $ _backtrack b then id else (++[(t,c)])) $ _backtrack b } : bs
|
|
|
|
| otherwise = b { _backtrack = [(t,c) | t <- _runnable b] } : bs
|
|
|
|
backtrack c (b:bs) n t = b : backtrack c bs (n-1) t
|
|
|
|
backtrack _ [] _ _ = error "Ran out of schedule whilst backtracking!"
|
2015-07-17 00:32:30 +03:00
|
|
|
|
|
|
|
-- | Pick a new thread to run. Choose the current thread if available,
|
|
|
|
-- otherwise add all runnable threads.
|
|
|
|
pbInitialise :: Maybe (ThreadId, a) -> NonEmpty (ThreadId, b) -> NonEmpty ThreadId
|
|
|
|
pbInitialise prior threads@((next, _):|rest) = case prior of
|
|
|
|
Just (tid, _)
|
|
|
|
| any (\(t, _) -> t == tid) $ toList threads -> tid:|[]
|
|
|
|
_ -> next:|map fst rest
|
|
|
|
|
|
|
|
-- * BPOR
|
|
|
|
|
|
|
|
-- | SCT via BPOR.
|
2015-06-19 18:50:51 +03:00
|
|
|
--
|
|
|
|
-- Schedules are generated by running the computation with a
|
|
|
|
-- deterministic scheduler with some initial list of decisions, after
|
2015-07-17 00:32:30 +03:00
|
|
|
-- which the supplied function is called. At each step of execution,
|
|
|
|
-- possible-conflicting actions are looked for, if any are found,
|
|
|
|
-- \"backtracking points\" are added, to cause the events to happen in
|
|
|
|
-- a different order in a future execution.
|
2015-06-19 18:50:51 +03:00
|
|
|
--
|
2015-07-17 00:32:30 +03:00
|
|
|
-- Note that unlike with non-bounded partial-order reduction, this may
|
|
|
|
-- do some redundant work as the introduction of a bound can make
|
|
|
|
-- previously non-interfering events interfere with each other.
|
|
|
|
sctBounded :: ([Decision] -> Bool)
|
|
|
|
-- ^ Check if a prefix trace is within the bound.
|
|
|
|
-> ([BacktrackStep] -> Int -> ThreadId -> [BacktrackStep])
|
|
|
|
-- ^ Add a new backtrack point, this takes the history of
|
|
|
|
-- the execution so far, the index to insert the
|
|
|
|
-- backtracking point, and the thread to backtrack to. This
|
|
|
|
-- may insert more than one backtracking point.
|
|
|
|
-> (Maybe (ThreadId, ThreadAction) -> NonEmpty (ThreadId, ThreadAction') -> NonEmpty ThreadId)
|
|
|
|
-- ^ Produce possible scheduling decisions, all will be
|
|
|
|
-- tried.
|
|
|
|
-> (forall t. Conc t a) -> [(Either Failure a, Trace)]
|
|
|
|
sctBounded bv backtrack initialise c = go initialState where
|
|
|
|
go bpor = case next bpor of
|
2015-07-17 17:34:52 +03:00
|
|
|
Just (sched, conservative, bpor') ->
|
2015-07-17 00:32:30 +03:00
|
|
|
-- Run the computation
|
2015-07-20 17:19:51 +03:00
|
|
|
let (res, (_, bs, _), trace) = runConc (bporSched initialise) (initialSchedState sched) c
|
2015-07-17 00:32:30 +03:00
|
|
|
-- Identify the backtracking points
|
2015-07-17 17:34:52 +03:00
|
|
|
bpoints = findBacktrack backtrack bs trace
|
2015-07-17 00:32:30 +03:00
|
|
|
-- Add new nodes to the tree
|
2015-07-17 17:34:52 +03:00
|
|
|
bpor'' = grow conservative trace bpor'
|
2015-07-17 00:32:30 +03:00
|
|
|
-- Add new backtracking information
|
|
|
|
bpor''' = todo bv bpoints bpor''
|
|
|
|
-- Loop
|
|
|
|
in (res, trace) : go bpor'''
|
|
|
|
|
|
|
|
Nothing -> []
|
2015-06-19 18:50:51 +03:00
|
|
|
|
|
|
|
-- | Variant of 'sctBounded' for computations which do 'IO'.
|
2015-07-17 00:32:30 +03:00
|
|
|
sctBoundedIO :: ([Decision] -> Bool)
|
|
|
|
-> ([BacktrackStep] -> Int -> ThreadId -> [BacktrackStep])
|
|
|
|
-> (Maybe (ThreadId, ThreadAction) -> NonEmpty (ThreadId, ThreadAction') -> NonEmpty ThreadId)
|
|
|
|
-> (forall t. ConcIO t a) -> IO [(Either Failure a, Trace)]
|
|
|
|
sctBoundedIO bv backtrack initialise c = go initialState where
|
|
|
|
go bpor = case next bpor of
|
2015-07-17 17:34:52 +03:00
|
|
|
Just (sched, conservative, bpor') -> do
|
2015-07-20 17:19:51 +03:00
|
|
|
(res, (_, bs, _), trace) <- runConcIO (bporSched initialise) (initialSchedState sched) c
|
2015-07-17 00:32:30 +03:00
|
|
|
|
2015-07-17 17:34:52 +03:00
|
|
|
let bpoints = findBacktrack backtrack bs trace
|
|
|
|
let bpor'' = grow conservative trace bpor'
|
2015-07-17 00:32:30 +03:00
|
|
|
let bpor''' = todo bv bpoints bpor''
|
|
|
|
|
|
|
|
((res, trace):) <$> go bpor'''
|
|
|
|
|
|
|
|
Nothing -> return []
|
|
|
|
|
2015-07-20 17:19:51 +03:00
|
|
|
-- | Initial scheduler state for a given prefix
|
|
|
|
initialSchedState :: [ThreadId] -> ([ThreadId], [(NonEmpty (ThreadId, ThreadAction'), [ThreadId])], [(ThreadId, Bool)])
|
|
|
|
initialSchedState prefix = (prefix, [], initialCVState)
|
|
|
|
|
2015-07-17 00:32:30 +03:00
|
|
|
-- | BPOR scheduler: takes a list of decisions, and maintains a trace
|
|
|
|
-- including the runnable threads, and the alternative choices allowed
|
|
|
|
-- by the bound-specific initialise function.
|
|
|
|
bporSched :: (Maybe (ThreadId, ThreadAction) -> NonEmpty (ThreadId, ThreadAction') -> NonEmpty ThreadId)
|
2015-07-20 17:19:51 +03:00
|
|
|
-> Scheduler ([ThreadId], [(NonEmpty (ThreadId, ThreadAction'), [ThreadId])], [(ThreadId, Bool)])
|
2015-07-17 00:32:30 +03:00
|
|
|
bporSched initialise = force sched where
|
|
|
|
-- If there is a decision available, make it
|
2015-07-20 17:19:51 +03:00
|
|
|
sched (d:ds, bs, cvstate) prior threads =
|
|
|
|
let cvstate' = maybe cvstate (updateCVState cvstate . snd) prior
|
|
|
|
in (d, (ds, bs ++ [(threads, [])], cvstate'))
|
2015-07-17 00:32:30 +03:00
|
|
|
|
|
|
|
-- Otherwise query the initialise function for a list of possible
|
|
|
|
-- choices, and make one of them arbitrarily (recording the others).
|
2015-07-20 17:19:51 +03:00
|
|
|
sched ([], bs, cvstate) prior threads =
|
|
|
|
let choices = initialise prior threads
|
|
|
|
cvstate' = maybe cvstate (updateCVState cvstate . snd) prior
|
|
|
|
choices' = [t
|
|
|
|
| t <- toList choices
|
|
|
|
, a <- maybeToList $ lookup t (toList threads)
|
|
|
|
, not $ willBlock cvstate' a
|
|
|
|
]
|
|
|
|
in case choices' of
|
|
|
|
(next:rest) -> (next, ([], bs ++ [(threads, rest)], cvstate'))
|
|
|
|
|
|
|
|
-- TODO: abort the execution here.
|
|
|
|
[] -> case choices of
|
|
|
|
(next:|_) -> (next, ([], bs ++ [(threads, [])], cvstate'))
|