{-# LANGUAGE Rank2Types #-}

-- | Systematic testing for concurrent computations.
module Test.DejaFu.SCT
  ( -- * 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
  ) where

import Control.Applicative ((<$>), (<*>))
import Control.Arrow (first)
import Control.DeepSeq (NFData(..), force)
import Data.List (nub)
import Data.Map (Map)
import Data.Maybe (mapMaybe, fromJust)
import Test.DejaFu.Deterministic
import Test.DejaFu.Deterministic.IO (ConcIO, runConcIO)
import Test.DejaFu.SCT.Internal

import qualified Data.Map as M

-- * Pre-emption bounding

-- | An SCT runner using a pre-emption bounding scheduler.
sctPreBound :: Int -> (forall t. Conc t a) -> [(Either Failure a, Trace)]
sctPreBound pb = sctBounded (pbBv pb) pbBacktrack pbInitialise

-- | Variant of 'sctPreBound' for computations which do 'IO'.
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]
pbBacktrack bs i tid = backtrack (backtrack 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]

  backtrack (b:bs) 0 t
    | t `elem` _runnable b = b { _backtrack = nub $ t : _backtrack b } : bs
    | otherwise = b { _backtrack = _runnable b } : bs
  backtrack (b:bs) n t = b : backtrack bs (n-1) t
  backtrack [] _ _ = error "Ran out of schedule whilst backtracking!"

-- | 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.
--
-- Schedules are generated by running the computation with a
-- deterministic scheduler with some initial list of decisions, after
-- 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.
--
-- 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
    Just (sched, bpor') ->
      -- Run the computation
      let (res, (_, bs), trace) = runConc (bporSched initialise) (sched, []) c
      -- Identify the backtracking points
          bpoints = findBacktrack False backtrack bs trace
      -- Add new nodes to the tree
          bpor''  = grow trace bpor'
      -- Add new backtracking information
          bpor''' = todo bv bpoints bpor''
      -- Loop
      in (res, trace) : go bpor'''

    Nothing -> []

-- | Variant of 'sctBounded' for computations which do 'IO'.
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
    Just (sched, bpor') -> do
      (res, (_, bs), trace) <- runConcIO (bporSched initialise) (sched, []) c

      let bpoints = findBacktrack True backtrack bs trace
      let bpor''  = grow trace bpor'
      let bpor''' = todo bv bpoints bpor''

      ((res, trace):) <$> go bpor'''

    Nothing -> return []

-- | 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)
          -> Scheduler ([ThreadId], [(NonEmpty (ThreadId, ThreadAction'), [ThreadId])])
bporSched initialise = force sched where
  -- If there is a decision available, make it
  sched (d:ds, bs) _ threads = (d, (ds, bs ++ [(threads, [])]))

  -- Otherwise query the initialise function for a list of possible
  -- choices, and make one of them arbitrarily (recording the others).
  sched ([], bs) prior threads = case initialise prior threads of
    (next:|rest) -> (next, ([], bs ++ [(threads, rest)]))