Merge pull request #114 from input-output-hk/coot/refactor-io-sim-por Refactor I… - input-output-hk/io-sim@892076e1 - Cardano Updates

Home / Input Output / io-sim / 892076e1

View on GitHub

File Changes

m

cabal.project

+1/-1

    d4a35cd3121aa00d18544bb0ac01c3e1691d618f462c46129271bccf39f7e8ee

index-state:

-

  , hackage.haskell.org 2023-03-25T12:00:00Z

+

  , hackage.haskell.org 2023-09-20T00:00:00Z

  , cardano-haskell-packages 2022-11-15T17:30:00Z

-- TODO: early ghc-9.6 support

m

io-sim/CHANGELOG.md

+30/-0

# Revsion history of io-sim

+

## next

+

+

### Breaking changes

+

+

#### Breaking changes

+

+

* Renamed `ThreadId` to `IOSimThreadId` to avoid a clash with `ThreadId`

+

  associated type family of `MonadFork`.  It makes it much simpler to paste

+

  failing `ScheduleControl` in `ghci` or tests.

+

* `BlockedReason` was modified: `BlockedOnOther` was removed, in favour of `BlockedOnDelay` and `BlockOnThrowTo`.

+

* The `Failure` type (for example returned by `runSim`) now also contains

+

  a constructor for internal failures.  This improved error reporting when

+

  there's a bug in `IOSimPOR`.  Currently it's only used by some of the

+

  assertions in `IOSimPOR`.

+

+

#### Non breaking changes

+

+

* Refactored the internal API to avoid `unsafePerformIO`.

+

* Fixed bugs which lead to discovery of schedules which are impossible to run.

+

* Added haddocks, refactored the code base to improve readability.

+

* Fixed reported `step` in `EventTxWakup`

+

* Added debugging information schedule, (`explorationDebugLevel` option).

+

  Mostly useful for debugging `IOSimPOR` itself.  This information will

+

  contains `Effect`, discovered races and schedules.

+

* Addded or improved pretty printers for `SimTrace`.  Among other changes,

+

  a racy `StepId`: `(RacyThreadId [1,2], 2)`, is now pretty printed as `Thread

+

  {1,2}.2`, a non racy step is printed as `Thread [1,2].2`.

+

* Fixed trace of calls to the `deschedule` function.

+

* Exposed `Timeout` type as part of the `newTimeout` API.

+

## 1.2.0.0

### Breaking changes

m

io-sim/io-sim.cabal

+2/-2

                       containers,

                       deepseq,

                       nothunks,

-

                       parallel,

                       psqueues          >=0.2 && <0.3,

                       strict-stm       ^>=1.2,

                       si-timers        ^>=1.2,

                       containers,

                       io-classes,

                       io-sim,

-

                       parallel,

                       QuickCheck,

                       si-timers,

                       strict-stm,

                       tasty-hunit,

                       time

  ghc-options:         -fno-ignore-asserts

+

                       -rtsopts

+

                       -- -threaded

benchmark bench

  import:              warnings

m

io-sim/src/Control/Monad/IOSim.hs

+240/-146

+

{-# LANGUAGE BangPatterns        #-}

+

{-# LANGUAGE LambdaCase          #-}

{-# LANGUAGE ExplicitNamespaces  #-}

{-# LANGUAGE NamedFieldPuns      #-}

{-# LANGUAGE RankNTypes          #-}

{-# LANGUAGE ScopedTypeVariables #-}

{-# LANGUAGE TupleSections       #-}

{-# OPTIONS_GHC -Wno-name-shadowing #-}

+

{-# OPTIONS_GHC -Wno-unrecognised-pragmas #-}

+

module Control.Monad.IOSim

  ( -- * Simulation monad

    IOSim

    -- ** Explore races using /IOSimPOR/

    -- $iosimpor

  , exploreSimTrace

+

  , exploreSimTraceST

  , controlSimTrace

+

  , controlSimTraceST

  , ScheduleMod (..)

  , ScheduleControl (..)

    -- *** Exploration options

  , SimEvent (..)

  , SimEventType (..)

  , ThreadLabel

+

  , IOSimThreadId (..)

  , Labelled (..)

    -- ** Dynamic Tracing

  , traceM

  , EventlogEvent (..)

  , EventlogMarker (..)

    -- * Low-level API

+

  , Timeout

  , newTimeout

  , readTimeout

  , cancelTimeout

import           Prelude

import           Data.Bifoldable

+

import           Data.Bifunctor (first)

import           Data.Dynamic (fromDynamic)

+

import           Data.Functor (void)

import           Data.List (intercalate)

+

import           Data.Maybe (catMaybes)

import           Data.Set (Set)

import qualified Data.Set as Set

import           Data.Typeable (Typeable)

import           Data.List.Trace (Trace (..))

+

import qualified Data.List.Trace as Trace

import           Control.Exception (throw)

import           Control.Monad.ST.Lazy

+

import           Data.STRef.Lazy

import           Control.Monad.Class.MonadThrow as MonadThrow

import           Control.Monad.IOSim.Internal (runSimTraceST)

import           Control.Monad.IOSim.Types

-

import           Control.Monad.IOSimPOR.Internal (controlSimTraceST)

+

import qualified Control.Monad.IOSimPOR.Internal as IOSimPOR (controlSimTraceST)

import           Control.Monad.IOSimPOR.QuickCheckUtils

import           Test.QuickCheck

-

-

import           Data.IORef

import           System.IO.Unsafe

+

import qualified Debug.Trace as Debug

selectTraceEvents

                    Deadlock      _   threads -> throw (FailureDeadlock threads)

                    MainReturn    _ _ _       -> []

                    Loop                      -> error "Impossible: selectTraceEvents _ TraceLoop{}"

+

                    InternalError msg         -> throw (FailureInternal msg)

              ( \ b acc -> b : acc )

[]

-- unsafe, of course, since that function may return different results

-- at different times.

-

detachTraceRaces :: SimTrace a -> (() -> [ScheduleControl], SimTrace a)

-

detachTraceRaces trace = unsafePerformIO $ do

-

  races <- newIORef []

-

  let readRaces ()  = concat . reverse . unsafePerformIO $ readIORef races

-

      saveRaces r t = unsafePerformIO $ do

-

                        modifyIORef races (r:)

-

                        return t

-

  let go (SimTrace a b c d trace)      = SimTrace a b c d $ go trace

-

      go (SimPORTrace a b c d e trace) = SimPORTrace a b c d e $ go trace

-

      go (TraceRacesFound r trace)     = saveRaces r $ go trace

-

      go t                             = t

-

  return (readRaces, go trace)

+

-- | Detach discovered races.  This is written in `ST` monad to support

+

-- simulations which do not terminate, in which case we will only detach races

+

-- up to the point we evaluated the simulation.

+

--

+

detachTraceRacesST :: forall a s. SimTrace a -> ST s (ST s [ScheduleControl], SimTrace a)

+

detachTraceRacesST trace0 = do

+

  races <- newSTRef []

+

  let readRaces :: ST s [ScheduleControl]

+

      readRaces = concat . reverse <$> readSTRef races

+

+

      saveRaces :: [ScheduleControl] -> ST s ()

+

      saveRaces rs = modifySTRef races (rs:)

+

+

      go :: SimTrace a -> ST s (SimTrace a)

+

      go (SimTrace a b c d trace)      = SimTrace a b c d <$> go trace

+

      go (SimPORTrace _ _ _ _ EventRaces {} trace)

+

                                       = go trace

+

      go (SimPORTrace a b c d e trace) = SimPORTrace a b c d e <$> go trace

+

      go (TraceRacesFound rs trace)    = saveRaces rs >> go trace

+

      go t                             = return t

+

+

  trace <- go trace0

+

  return (readRaces, trace)

+

+

+

-- | Like `detachTraceRacesST`, but it doesn't expose discovered races.

+

--

+

detachTraceRaces :: forall a. SimTrace a -> SimTrace a

+

detachTraceRaces = Trace.filter (\a -> case a of

+

                                         SimPOREvent { seType = EventRaces {} } -> False

+

                                         SimRacesFound {} -> False

+

                                         _                -> True)

-- | Select all the traced values matching the expected type. This relies on

-- the sim's dynamic trace facility.

       FailureException SomeException

       -- | The threads all deadlocked.

-

     | FailureDeadlock ![Labelled ThreadId]

+

     | FailureDeadlock ![Labelled IOSimThreadId]

       -- | The main thread terminated normally but other threads were still

       -- alive, and strict shutdown checking was requested.

       -- See 'runSimStrictShutdown'.

-

     | FailureSloppyShutdown [Labelled ThreadId]

+

     | FailureSloppyShutdown [Labelled IOSimThreadId]

       -- | An exception was thrown while evaluation the trace.

       -- This could be an internal assertion failure of `io-sim` or an

       -- unhandled exception in the simulation.

     | FailureEvaluation SomeException

+

+

       -- | An internal failure of the simulator.

+

--

+

       -- Please open an issue at

+

       -- <https://github.com/input-output-hk/io-sim/issues>.

+

     | FailureInternal String

  deriving Show

instance Exception Failure where

             , intercalate ", " (show `map` threads)

             , ">>"

-

    displayException (FailureEvaluation err) = "evaluation error:" ++ displayException  err

+

    displayException (FailureEvaluation err) =

+

      concat [ "<<evaluation error: "

+

             , displayException  err

+

             , ">>"

+

+

    displayException (FailureInternal msg) =

+

      concat [ "<<internal failure: "

+

             , msg

+

             , ">>\n"

+

             , "please report the issue at\n"

+

             , "https://github.com/input-output-hk/io-sim/issues"

+

-- | 'IOSim' is a pure monad.

-- | Like 'runSim' but fail when the main thread terminates if there are other

-- threads still running or blocked. If one is trying to follow a strict thread

-

-- cleanup policy then this helps testing for that.

+

-- clean-up policy then this helps testing for that.

--

runSimStrictShutdown :: forall a. (forall s. IOSim s a) -> Either Failure a

runSimStrictShutdown mainAction = traceResult True (runSimTrace mainAction)

    go (TraceMainException _ e _)       = pure $ Left (FailureException e)

    go (TraceDeadlock   _   threads)    = pure $ Left (FailureDeadlock threads)

    go TraceLoop{}                      = error "Impossible: traceResult TraceLoop{}"

+

    go (TraceInternalError msg)         = pure $ Left (FailureInternal msg)

-- | Turn 'SimTrace' into a list of timestamped events.

m

io-sim/src/Control/Monad/IOSim/CommonTypes.hs

+65/-9

{-# LANGUAGE DeriveAnyClass             #-}

{-# LANGUAGE DeriveGeneric              #-}

{-# LANGUAGE DerivingStrategies         #-}

+

{-# LANGUAGE DerivingVia                #-}

{-# LANGUAGE GADTs                      #-}

{-# LANGUAGE GeneralizedNewtypeDeriving #-}

{-# LANGUAGE ScopedTypeVariables        #-}

-- | Common types shared between `IOSim` and `IOSimPOR`.

--

-

module Control.Monad.IOSim.CommonTypes where

+

module Control.Monad.IOSim.CommonTypes

+

  ( IOSimThreadId (..)

+

  , ppIOSimThreadId

+

  , StepId

+

  , ppStepId

+

  , childThreadId

+

  , setRacyThread

+

  , TVarId (..)

+

  , TimeoutId (..)

+

  , ClockId (..)

+

  , VectorClock (..)

+

  , ppVectorClock

+

  , unTimeoutId

+

  , ThreadLabel

+

  , TVarLabel

+

  , TVar (..)

+

  , SomeTVar (..)

+

  , Deschedule (..)

+

  , ThreadStatus (..)

+

  , BlockedReason (..)

+

    -- * Utils

+

  , ppList

+

  ) where

import           Control.DeepSeq (NFData (..))

import           Control.Monad.Class.MonadSTM (TraceValue)

import           Control.Monad.ST.Lazy

import           NoThunks.Class

+

import           Data.List (intercalate, intersperse)

import           Data.Map (Map)

+

import qualified Data.Map as Map

import           Data.STRef.Lazy

import           Data.Set (Set)

import           GHC.Generics

+

import           Quiet

-- | A thread id.

-- `Control.Monad.Class.MonadTest.exploreRaces` was

-- executed in it or it's a thread forked by a racy thread.

--

-

data ThreadId = RacyThreadId [Int]

-

              | ThreadId     [Int]    -- non racy threads have higher priority

+

data IOSimThreadId =

+

    -- | A racy thread (`IOSimPOR` only), shown in the trace with curly braces,

+

    -- e.g. `Thread {2,3}`.

+

    RacyThreadId [Int]

+

    -- | A non racy thread.  They have higher priority than racy threads in

+

    -- `IOSimPOR` scheduler.

+

  | ThreadId     [Int]

  deriving stock    (Eq, Ord, Show, Generic)

  deriving anyclass NFData

  deriving anyclass NoThunks

+

ppIOSimThreadId :: IOSimThreadId -> String

+

ppIOSimThreadId (RacyThreadId as) = "Thread {"++ intercalate "," (map show as) ++"}"

+

ppIOSimThreadId     (ThreadId as) = "Thread " ++ show as

-

childThreadId :: ThreadId -> Int -> ThreadId

+

childThreadId :: IOSimThreadId -> Int -> IOSimThreadId

childThreadId (RacyThreadId is) i = RacyThreadId (is ++ [i])

childThreadId (ThreadId     is) i = ThreadId     (is ++ [i])

-

setRacyThread :: ThreadId -> ThreadId

+

setRacyThread :: IOSimThreadId -> IOSimThreadId

setRacyThread (ThreadId is)      = RacyThreadId is

setRacyThread tid@RacyThreadId{} = tid

+

-- | Execution step in `IOSimPOR` is identified by the thread id and

+

-- a monotonically increasing number (thread specific).

+

--

+

type StepId = (IOSimThreadId, Int)

+

+

ppStepId :: (IOSimThreadId, Int) -> String

+

ppStepId (tid, step) | step < 0

+

                     = concat [ppIOSimThreadId tid, ".-"]

+

ppStepId (tid, step) = concat [ppIOSimThreadId tid, ".", show step]

+

newtype TVarId      = TVarId    Int   deriving (Eq, Ord, Enum, Show)

newtype TimeoutId   = TimeoutId Int   deriving (Eq, Ord, Enum, Show)

newtype ClockId     = ClockId   [Int] deriving (Eq, Ord, Show)

-

newtype VectorClock = VectorClock { getVectorClock :: Map ThreadId Int }

-

  deriving Show

+

newtype VectorClock = VectorClock { getVectorClock :: Map IOSimThreadId Int }

+

  deriving Generic

+

  deriving Show via Quiet VectorClock

+

+

ppVectorClock :: VectorClock -> String

+

ppVectorClock (VectorClock m) = "VectorClock " ++ "[" ++ concat (intersperse ", " (ppStepId <$> Map.toList m)) ++ "]"

unTimeoutId :: TimeoutId -> Int

unTimeoutId (TimeoutId a) = a

       -- To avoid duplicates efficiently, the operations rely on a copy of the

       -- thread Ids represented as a set.

--

-

       tvarBlocked :: !(STRef s ([ThreadId], Set ThreadId)),

+

       tvarBlocked :: !(STRef s ([IOSimThreadId], Set IOSimThreadId)),

       -- | The vector clock of the current value.

--

  deriving (Eq, Show)

data BlockedReason = BlockedOnSTM

-

                   | BlockedOnOther

+

                   | BlockedOnDelay

+

                   | BlockedOnThrowTo

  deriving (Eq, Show)

+

+

--

+

-- Utils

+

--

+

+

ppList :: (a -> String) -> [a] -> String

+

ppList pp as = "[" ++ concat (intersperse ", " (map pp as)) ++ "]"

m

io-sim/src/Control/Monad/IOSim/Internal.hs

+26/-26

  , TimeoutException (..)

  , EventlogEvent (..)

  , EventlogMarker (..)

-

  , ThreadId

+

  , IOSimThreadId

  , ThreadLabel

  , Labelled (..)

  , SimTrace

--

data Thread s a = Thread {

-

    threadId      :: !ThreadId,

+

    threadId      :: !IOSimThreadId,

    threadControl :: !(ThreadControl s a),

    threadStatus  :: !ThreadStatus,

    threadMasking :: !MaskingState,

    -- other threads blocked in a ThrowTo to us because we are or were masked

-

    threadThrowTo :: ![(SomeException, Labelled ThreadId)],

+

    threadThrowTo :: ![(SomeException, Labelled IOSimThreadId)],

    threadClockId :: !ClockId,

    threadLabel   ::  Maybe ThreadLabel,

    threadNextTId :: !Int

labelledTVarId :: TVar s a -> ST s (Labelled TVarId)

labelledTVarId TVar { tvarId, tvarLabel } = (Labelled tvarId) <$> readSTRef tvarLabel

-

labelledThreads :: Map ThreadId (Thread s a) -> [Labelled ThreadId]

+

labelledThreads :: Map IOSimThreadId (Thread s a) -> [Labelled IOSimThreadId]

labelledThreads threadMap =

    -- @Map.foldr'@ (and alikes) are not strict enough, to not ratain the

    -- original thread map we need to evaluate the spine of the list.

     -- ^ `newTimeout` timer.

     | TimerRegisterDelay !(TVar s Bool)

     -- ^ `registerDelay` timer.

-

     | TimerThreadDelay !ThreadId !TimeoutId

-

     -- ^ `threadDelay` timer run by `ThreadId` which was assigned the given

+

     | TimerThreadDelay !IOSimThreadId !TimeoutId

+

     -- ^ `threadDelay` timer run by `IOSimThreadId` which was assigned the given

     -- `TimeoutId` (only used to report in a trace).

-

     | TimerTimeout !ThreadId !TimeoutId !(TMVar (IOSim s) ThreadId)

-

     -- ^ `timeout` timer run by `ThreadId` which was assigned the given

+

     | TimerTimeout !IOSimThreadId !TimeoutId !(TMVar (IOSim s) IOSimThreadId)

+

     -- ^ `timeout` timer run by `IOSimThreadId` which was assigned the given

     -- `TimeoutId` (only used to report in a trace).

-- | Internal state.

--

data SimState s a = SimState {

-

       runqueue :: !(Deque ThreadId),

+

       runqueue :: !(Deque IOSimThreadId),

       -- | All threads other than the currently running thread: both running

       -- and blocked threads.

-

       threads  :: !(Map ThreadId (Thread s a)),

+

       threads  :: !(Map IOSimThreadId (Thread s a)),

       -- | current time

       curTime  :: !Time,

       -- | ordered list of timers and timeouts

      let !expiry  = d `addTime` time

          !timers' = PSQ.insert nextTmid expiry (TimerThreadDelay tid nextTmid) timers

          !thread' = thread { threadControl = ThreadControl (Return ()) (DelayFrame nextTmid k ctl) }

-

      !trace <- deschedule (Blocked BlockedOnOther) thread' simstate { timers   = timers'

+

      !trace <- deschedule (Blocked BlockedOnDelay) thread' simstate { timers   = timers'

                                                                     , nextTmid = succ nextTmid }

      return (SimTrace time tid tlbl (EventThreadDelay nextTmid expiry) trace)

          -- exception and the source thread id to the pending async exceptions.

          let adjustTarget t = t { threadThrowTo = (e, Labelled tid tlbl) : threadThrowTo t }

              threads'       = Map.adjust adjustTarget tid' threads

-

          !trace <- deschedule (Blocked BlockedOnOther) thread' simstate { threads = threads' }

+

          !trace <- deschedule (Blocked BlockedOnThrowTo) thread' simstate { threads = threads' }

          return $ SimTrace time tid tlbl (EventThrowTo e tid')

                 $ SimTrace time tid tlbl EventThrowToBlocked

-

                 $ SimTrace time tid tlbl (EventDeschedule (Blocked BlockedOnOther))

+

                 $ SimTrace time tid tlbl (EventDeschedule (Blocked BlockedOnThrowTo))

                 $ trace

        else do

          -- The target thread has async exceptions unmasked, or is masked but

    timeoutSTMAction TimerThreadDelay{}       = return ()

    timeoutSTMAction TimerTimeout{}           = return ()

-

unblockThreads :: Bool -> [ThreadId] -> SimState s a -> ([ThreadId], SimState s a)

+

unblockThreads :: Bool -> [IOSimThreadId] -> SimState s a -> ([IOSimThreadId], SimState s a)

unblockThreads !onlySTM !wakeup !simstate@SimState {runqueue, threads} =

    -- To preserve our invariants (that threadBlocked is correct)

    -- we update the runqueue and threads together here

    !unblocked = [ tid

                 | tid <- wakeup

                 , case Map.lookup tid threads of

-

                    Just Thread { threadStatus = ThreadBlocked BlockedOnOther }

-

                      -> not onlySTM

                    Just Thread { threadStatus = ThreadBlocked BlockedOnSTM }

                      -> True

+

                    Just Thread { threadStatus = ThreadBlocked _ }

+

                      -> not onlySTM

                    _ -> False

    -- and in which case we mark them as now running

-- receive a 'ThreadKilled' exception.

--

forkTimeoutInterruptThreads :: forall s a.

-

                               [(ThreadId, TimeoutId, TMVar (IOSim s) ThreadId)]

+

                               [(IOSimThreadId, TimeoutId, TMVar (IOSim s) IOSimThreadId)]

                            -> SimState s a

                            -> ST s (SimState s a)

forkTimeoutInterruptThreads timeoutExpired simState =

  where

    -- we launch a thread responsible for throwing an AsyncCancelled exception

    -- to the thread which timeout expired

-

    throwToThread :: [(Thread s a, TMVar (IOSim s) ThreadId)]

+

    throwToThread :: [(Thread s a, TMVar (IOSim s) IOSimThreadId)]

    (simState', throwToThread) = List.mapAccumR fn simState timeoutExpired

      where

        fn :: SimState s a

-

           -> (ThreadId, TimeoutId, TMVar (IOSim s) ThreadId)

-

           -> (SimState s a, (Thread s a, TMVar (IOSim s) ThreadId))

+

           -> (IOSimThreadId, TimeoutId, TMVar (IOSim s) IOSimThreadId)

+

           -> (SimState s a, (Thread s a, TMVar (IOSim s) IOSimThreadId))

        fn state@SimState { threads } (tid, tmid, lock) =

          let t = case tid `Map.lookup` threads of

                    Just t' -> t'

          | p == p' -> collectAll (k:ks) p (x:xs) psq'

        _           -> (reverse ks, p, reverse xs, psq)

-

traceMany :: [(Time, ThreadId, Maybe ThreadLabel, SimEventType)]

+

traceMany :: [(Time, IOSimThreadId, Maybe ThreadLabel, SimEventType)]

          -> SimTrace a -> SimTrace a

traceMany []                      trace = trace

traceMany ((time, tid, tlbl, event):ts) trace =

    SimTrace time tid tlbl event (traceMany ts trace)

-

lookupThreadLabel :: ThreadId -> Map ThreadId (Thread s a) -> Maybe ThreadLabel

+

lookupThreadLabel :: IOSimThreadId -> Map IOSimThreadId (Thread s a) -> Maybe ThreadLabel

lookupThreadLabel tid threads = join (threadLabel <$> Map.lookup tid threads)

execAtomically :: forall s a c.

                  Time

-

               -> ThreadId

+

               -> IOSimThreadId

               -> Maybe ThreadLabel

               -> TVarId

               -> StmA s a

-- Blocking and unblocking on TVars

--

-

readTVarBlockedThreads :: TVar s a -> ST s [ThreadId]

+

readTVarBlockedThreads :: TVar s a -> ST s [IOSimThreadId]

readTVarBlockedThreads TVar{tvarBlocked} = fst <$> readSTRef tvarBlocked

-

blockThreadOnTVar :: ThreadId -> TVar s a -> ST s ()

+

blockThreadOnTVar :: IOSimThreadId -> TVar s a -> ST s ()

blockThreadOnTVar tid TVar{tvarBlocked} = do

    (tids, tidsSet) <- readSTRef tvarBlocked

    when (tid `Set.notMember` tidsSet) $ do

-- the var writes that woke them.

--

threadsUnblockedByWrites :: [SomeTVar s]

-

                         -> ST s ([ThreadId], Map ThreadId (Set (Labelled TVarId)))

+

                         -> ST s ([IOSimThreadId], Map IOSimThreadId (Set (Labelled TVarId)))

threadsUnblockedByWrites written = do

  !tidss <- sequence

             [ (,) <$> labelledTVarId tvar <*> readTVarBlockedThreads tvar

m

io-sim/src/Control/Monad/IOSim/InternalTypes.hs

+3/-3

import           Control.Concurrent.Class.MonadSTM

import           Control.Monad.Class.MonadThrow (MaskingState (..))

-

import           Control.Monad.IOSim.Types (IOSim (..), SimA (..), ThreadId, TimeoutId)

+

import           Control.Monad.IOSim.Types (IOSim (..), SimA (..), IOSimThreadId, TimeoutId)

import           GHC.Exts (oneShot)

             -> !(ControlStack s c a)

             -> ControlStack s b a

  TimeoutFrame :: TimeoutId

-

               -> TMVar (IOSim s) ThreadId

+

               -> TMVar (IOSim s) IOSimThreadId

               -> (Maybe b -> SimA s c)

               -> !(ControlStack s c a)

               -> ControlStack s b a

  | DelayFrame' TimeoutId ControlStackDash

  deriving Show

-

data IsLocked = NotLocked | Locked !ThreadId

+

data IsLocked = NotLocked | Locked !IOSimThreadId

  deriving (Eq, Show)

-- | Unsafe method which removes a timeout.

m

io-sim/src/Control/Monad/IOSim/Types.hs

+158/-90

{-# LANGUAGE ExistentialQuantification  #-}

{-# LANGUAGE FlexibleInstances          #-}

{-# LANGUAGE GADTSyntax                 #-}

+

{-# LANGUAGE LambdaCase                 #-}

{-# LANGUAGE MultiParamTypeClasses      #-}

{-# LANGUAGE NamedFieldPuns             #-}

{-# LANGUAGE NumericUnderscores         #-}

  , traceSTM

  , liftST

  , SimA (..)

-

  , StepId

  , STMSim

  , STM (..)

  , runSTM

  , setCurrentTime

  , unshareClock

  , ScheduleControl (..)

+

  , isDefaultSchedule

  , ScheduleMod (..)

  , ExplorationOptions (..)

  , ExplorationSpec

  , EventlogEvent (..)

  , EventlogMarker (..)

  , SimEventType (..)

+

  , ppSimEventType

  , SimEvent (..)

  , SimResult (..)

  , SimTrace

-

  , Trace.Trace (SimTrace, SimPORTrace, TraceMainReturn, TraceMainException, TraceDeadlock, TraceRacesFound, TraceLoop)

+

  , Trace.Trace (SimTrace, SimPORTrace, TraceMainReturn, TraceMainException, TraceDeadlock, TraceRacesFound, TraceLoop, TraceInternalError)

  , ppTrace

  , ppTrace_

  , ppSimEvent

import           Control.Monad.Class.MonadAsync hiding (Async)

import qualified Control.Monad.Class.MonadAsync as MonadAsync

import           Control.Monad.Class.MonadEventlog

-

import           Control.Monad.Class.MonadFork hiding (ThreadId)

-

import qualified Control.Monad.Class.MonadFork as MonadFork

+

import           Control.Monad.Class.MonadFork

import           Control.Monad.Class.MonadST

import           Control.Monad.Class.MonadSTM.Internal (MonadInspectSTM (..),

                     MonadLabelledSTM (..), MonadSTM, MonadTraceSTM (..),

                  SimA s a -> (e -> SimA s a) -> (a -> SimA s b) -> SimA s b

  Evaluate     :: a -> (a -> SimA s b) -> SimA s b

-

  Fork         :: IOSim s () -> (ThreadId -> SimA s b) -> SimA s b

-

  GetThreadId  :: (ThreadId -> SimA s b) -> SimA s b

-

  LabelThread  :: ThreadId -> String -> SimA s b -> SimA s b

+

  Fork         :: IOSim s () -> (IOSimThreadId -> SimA s b) -> SimA s b

+

  GetThreadId  :: (IOSimThreadId -> SimA s b) -> SimA s b

+

  LabelThread  :: IOSimThreadId -> String -> SimA s b -> SimA s b

  Atomically   :: STM  s a -> (a -> SimA s b) -> SimA s b

-

  ThrowTo      :: SomeException -> ThreadId -> SimA s a -> SimA s a

+

  ThrowTo      :: SomeException -> IOSimThreadId -> SimA s a -> SimA s a

  SetMaskState :: MaskingState  -> IOSim s a -> (a -> SimA s b) -> SimA s b

  GetMaskState :: (MaskingState -> SimA s b) -> SimA s b

blockUninterruptible a = IOSim (SetMaskState MaskedUninterruptible a)

instance MonadThread (IOSim s) where

-

  type ThreadId (IOSim s) = ThreadId

+

  type ThreadId (IOSim s) = IOSimThreadId

  myThreadId       = IOSim $ oneShot $ \k -> GetThreadId k

  labelThread t l  = IOSim $ oneShot $ \k -> LabelThread t l (k ())

        MVarEmpty _ _ -> pure Nothing

        MVarFull x _  -> pure (Just x)

-

data Async s a = Async !ThreadId (STM s (Either SomeException a))

+

data Async s a = Async !IOSimThreadId (STM s (Either SomeException a))

instance Eq (Async s a) where

    Async tid _ == Async tid' _ = tid == tid'

    -- | Used when using `IOSim`.

  = SimEvent {

      seTime        :: !Time,

-

      seThreadId    :: !ThreadId,

+

      seThreadId    :: !IOSimThreadId,

      seThreadLabel :: !(Maybe ThreadLabel),

      seType        :: !SimEventType

    -- | Only used for /IOSimPOR/

  | SimPOREvent {

      seTime        :: !Time,

-

      seThreadId    :: !ThreadId,

+

      seThreadId    :: !IOSimThreadId,

      seStep        :: !Int,

      seThreadLabel :: !(Maybe ThreadLabel),

      seType        :: !SimEventType

           -> Int -- ^ width of thread label

           -> SimEvent

           -> String

-

ppSimEvent timeWidth tidWidth tLabelWidth SimEvent {seTime, seThreadId, seThreadLabel, seType} =

+

+

ppSimEvent timeWidth tidWidth tLabelWidth SimEvent {seTime = Time time, seThreadId, seThreadLabel, seType} =

    printf "%-*s - %-*s %-*s - %s"

           timeWidth

-

           (show seTime)

+

           (show time)

           tidWidth

-

           (show seThreadId)

+

           (ppIOSimThreadId seThreadId)

           tLabelWidth

           threadLabel

-

           (show seType)

+

           (ppSimEventType seType)

  where

    threadLabel = fromMaybe "" seThreadLabel

-

ppSimEvent timeWidth tidWidth tLableWidth SimPOREvent {seTime, seThreadId, seStep, seThreadLabel, seType} =

+

+

ppSimEvent timeWidth tidWidth tLableWidth SimPOREvent {seTime = Time time, seThreadId, seStep, seThreadLabel, seType} =

    printf "%-*s - %-*s %-*s - %s"

           timeWidth

-

           (show seTime)

+

           (show time)

           tidWidth

-

           (show (seThreadId, seStep))

+

           (ppStepId (seThreadId, seStep))

           tLableWidth

           threadLabel

-

           (show seType)

+

           (ppSimEventType seType)

  where

    threadLabel = fromMaybe "" seThreadLabel

+

ppSimEvent _ _ _ (SimRacesFound controls) =

    "RacesFound "++show controls

+

-- | A result type of a simulation.

data SimResult a

-

    = MainReturn    !Time a             ![Labelled ThreadId]

+

    = MainReturn    !Time a             ![Labelled IOSimThreadId]

    -- ^ Return value of the main thread.

-

    | MainException !Time SomeException ![Labelled ThreadId]

+

    | MainException !Time SomeException ![Labelled IOSimThreadId]

    -- ^ Exception thrown by the main thread.

-

    | Deadlock      !Time               ![Labelled ThreadId]

+

    | Deadlock      !Time               ![Labelled IOSimThreadId]

    -- ^ Deadlock discovered in the simulation.  Deadlocks are discovered if

    -- simply the simulation cannot do any progress in a given time slot and

    -- there's no event which would advance the time.

    | Loop

    -- ^ Only returned by /IOSimPOR/ when a step execution took longer than

    -- 'explorationStepTimelimit` was exceeded.

+

    | InternalError String

    deriving (Show, Functor)

-- | A type alias for 'IOSim' simulation trace.  It comes with useful pattern

      $ tr

+

+

-- | Trace each event using 'Debug.trace'; this is useful when a trace ends with

-- a pure error, e.g. an assertion.

--

        . Trace.toList

-

pattern SimTrace :: Time -> ThreadId -> Maybe ThreadLabel -> SimEventType -> SimTrace a

+

pattern SimTrace :: Time -> IOSimThreadId -> Maybe ThreadLabel -> SimEventType -> SimTrace a

                 -> SimTrace a

pattern SimTrace time threadId threadLabel traceEvent trace =

    Trace.Cons (SimEvent time threadId threadLabel traceEvent)

               trace

-

pattern SimPORTrace :: Time -> ThreadId -> Int -> Maybe ThreadLabel -> SimEventType -> SimTrace a

+

pattern SimPORTrace :: Time -> IOSimThreadId -> Int -> Maybe ThreadLabel -> SimEventType -> SimTrace a

                    -> SimTrace a

pattern SimPORTrace time threadId step threadLabel traceEvent trace =

    Trace.Cons (SimPOREvent time threadId step threadLabel traceEvent)

    Trace.Cons (SimRacesFound controls)

               trace

-

pattern TraceMainReturn :: Time -> a -> [Labelled ThreadId]

+

pattern TraceMainReturn :: Time -> a -> [Labelled IOSimThreadId]

                        -> SimTrace a

pattern TraceMainReturn time a threads = Trace.Nil (MainReturn time a threads)

-

pattern TraceMainException :: Time -> SomeException -> [Labelled ThreadId]

+

pattern TraceMainException :: Time -> SomeException -> [Labelled IOSimThreadId]

                           -> SimTrace a

pattern TraceMainException time err threads = Trace.Nil (MainException time err threads)

m

io-sim/src/Control/Monad/IOSimPOR/Internal.hs

+272/-235

{-# LANGUAGE MultiParamTypeClasses     #-}

{-# LANGUAGE NamedFieldPuns            #-}

{-# LANGUAGE RankNTypes                #-}

+

-- only used to construct records if its clear to do so

+

{-# LANGUAGE RecordWildCards           #-}

{-# LANGUAGE ScopedTypeVariables       #-}

{-# LANGUAGE TypeFamilies              #-}

  , TimeoutException (..)

  , EventlogEvent (..)

  , EventlogMarker (..)

-

  , ThreadId

+

  , IOSimThreadId

  , ThreadLabel

  , Labelled (..)

  , SimTrace

--

data Thread s a = Thread {

-

    threadId      :: !ThreadId,

+

    threadId      :: !IOSimThreadId,

    threadControl :: !(ThreadControl s a),

    threadStatus  :: !ThreadStatus,

    threadMasking :: !MaskingState,

    -- other threads blocked in a ThrowTo to us because we are or were masked

-

    threadThrowTo :: ![(SomeException, Labelled ThreadId, VectorClock)],

+

    threadThrowTo :: ![(SomeException, Labelled IOSimThreadId, VectorClock)],

    threadClockId :: !ClockId,

    threadLabel   :: Maybe ThreadLabel,

    threadNextTId :: !Int,

    ThreadDone -> True

    _          -> False

-

threadStepId :: Thread s a -> (ThreadId, Int)

+

threadStepId :: Thread s a -> (IOSimThreadId, Int)

threadStepId Thread{ threadId, threadStep } = (threadId, threadStep)

-

isRacyThreadId :: ThreadId -> Bool

+

isRacyThreadId :: IOSimThreadId -> Bool

isRacyThreadId (RacyThreadId _) = True

isRacyThreadId _                = True

-

isNotRacyThreadId :: ThreadId -> Bool

+

isNotRacyThreadId :: IOSimThreadId -> Bool

isNotRacyThreadId (ThreadId _) = True

isNotRacyThreadId _            = False

bottomVClock :: VectorClock

bottomVClock = VectorClock Map.empty

-

insertVClock :: ThreadId -> Int -> VectorClock -> VectorClock

+

insertVClock :: IOSimThreadId -> Int -> VectorClock -> VectorClock

insertVClock tid !step (VectorClock m) = VectorClock (Map.insert tid step m)

leastUpperBoundVClock :: VectorClock -> VectorClock -> VectorClock

labelledTVarId :: TVar s a -> ST s (Labelled TVarId)

labelledTVarId TVar { tvarId, tvarLabel } = Labelled tvarId <$> readSTRef tvarLabel

-

labelledThreads :: Map ThreadId (Thread s a) -> [Labelled ThreadId]

+

labelledThreads :: Map IOSimThreadId (Thread s a) -> [Labelled IOSimThreadId]

labelledThreads threadMap =

    -- @Map.foldr'@ (and alikes) are not strict enough, to not retain the

    -- original thread map we need to evaluate the spine of the list.

     -- ^ `newTimeout` timer.

     | TimerRegisterDelay !(TVar s Bool)

     -- ^ `registerDelay` timer.

-

     | TimerThreadDelay !ThreadId !TimeoutId

-

     -- ^ `threadDelay` timer run by `ThreadId` which was assigned the given

+

     | TimerThreadDelay !IOSimThreadId !TimeoutId

+

     -- ^ `threadDelay` timer run by `IOSimThreadId` which was assigned the given

     -- `TimeoutId` (only used to report in a trace).

-

     | TimerTimeout !ThreadId !TimeoutId !(TMVar (IOSim s) ThreadId)

-

     -- ^ `timeout` timer run by `ThreadId` which was assigned the given

+

     | TimerTimeout !IOSimThreadId !TimeoutId !(TMVar (IOSim s) IOSimThreadId)

+

     -- ^ `timeout` timer run by `IOSimThreadId` which was assigned the given

     -- `TimeoutId` (only used to report in a trace).

-

type RunQueue = OrdPSQ (Down ThreadId) (Down ThreadId) ()

+

type RunQueue   = OrdPSQ (Down IOSimThreadId) (Down IOSimThreadId) ()

type Timeouts s = OrdPSQ TimeoutId Time (TimerCompletionInfo s)

-- | Internal state.

       runqueue         :: !RunQueue,

       -- | All threads other than the currently running thread: both running

       -- and blocked threads.

-

       threads          :: !(Map ThreadId (Thread s a)),

+

       threads          :: !(Map IOSimThreadId (Thread s a)),

       -- | current time

       curTime          :: !Time,

       -- | ordered list of timers and timeouts

      (Right thread0@Thread { threadMasking = maskst' }, timers'') -> do

        -- We found a suitable exception handler, continue with that

        -- We record a step, in case there is no exception handler on replay.

-

        let thread'  = stepThread thread0

-

            control' = advanceControl (threadStepId thread0) control

-

            races'   = updateRacesInSimState thread0 simstate

+

        let (thread', eff)  = stepThread thread0

+

            control'        = advanceControl (threadStepId thread0) control

+

            races'          = updateRaces thread0 simstate

        trace <- schedule thread' simstate{ races = races',

                                            control = control',

                                            timers = timers'' }

        return (SimPORTrace time tid tstep tlbl (EventThrow e) $

-

                SimPORTrace time tid tstep tlbl (EventMask maskst') trace)

+

                SimPORTrace time tid tstep tlbl (EventMask maskst') $

+

                SimPORTrace time tid tstep tlbl (EventEffect vClock eff) $

+

                SimPORTrace time tid tstep tlbl (EventRaces races')

+

                trace)

      (Left isMain, timers'')

        -- We unwound and did not find any suitable exception handler, so we

      let expiry  = d `addTime` time

          timers' = PSQ.insert nextTmid expiry (TimerThreadDelay tid nextTmid) timers

          thread' = thread { threadControl = ThreadControl (Return ()) (DelayFrame nextTmid k ctl) }

-

      trace <- deschedule (Blocked BlockedOnOther) thread'

+

      trace <- deschedule (Blocked BlockedOnDelay) thread'

                          simstate { timers   = timers',

                                     nextTmid = succ nextTmid }

      return (SimPORTrace time tid tstep tlbl (EventThreadDelay nextTmid expiry) trace)

          thread'' = Thread { threadId      = tid'

                            , threadControl = ThreadControl (runIOSim a)

                                                            ForkFrame

-

                            , threadStatus  = ThreadRunning

+

                            , threadStatus  = ThreadRunning

                            , threadMasking = threadMasking thread

                            , threadThrowTo = []

                            , threadClockId = threadClockId thread

          return $

            SimPORTrace time tid tstep tlbl (EventTxCommitted written' created' (Just effect')) $

            traceMany

-

              [ (time, tid', tstep, tlbl', EventTxWakeup vids')

+

              [ (time, tid', (-1), tlbl', EventTxWakeup vids')

              | tid' <- unblocked

              , let tlbl' = lookupThreadLabel tid' threads

              , let Just vids' = Set.toList <$> Map.lookup tid' wokeby ] $

          let adjustTarget t =

                t { threadThrowTo = (e, Labelled tid tlbl, vClock) : threadThrowTo t }

              threads'       = Map.adjust adjustTarget tid' threads

-

          trace <- deschedule (Blocked BlockedOnOther) thread' simstate { threads = threads' }

+

          trace <- deschedule (Blocked BlockedOnThrowTo) thread' simstate { threads = threads' }

          return $ SimPORTrace time tid tstep tlbl (EventThrowTo e tid')

                 $ SimPORTrace time tid tstep tlbl EventThrowToBlocked

-

                 $ SimPORTrace time tid tstep tlbl (EventDeschedule (Blocked BlockedOnOther))

+

                 $ SimPORTrace time tid tstep tlbl (EventDeschedule (Blocked BlockedOnThrowTo))

                 $ trace

        else do

          -- The target thread has async exceptions unmasked, or is masked but

deschedule :: Deschedule -> Thread s a -> SimState s a -> ST s (SimTrace a)

-

deschedule Yield thread@Thread { threadId = tid }

-

                 simstate@SimState{runqueue, threads, control} =

+

deschedule Yield thread@Thread { threadId     = tid,

+

                                 threadStep   = tstep,

+

                                 threadLabel  = tlbl,

+

                                 threadVClock = vClock }

+

                 simstate@SimState{runqueue,

+

                                   threads,

+

                                   curTime  = time,

+

                                   control } =

    -- We don't interrupt runnable threads anywhere else.

    -- We do it here by inserting the current thread into the runqueue in priority order.

-

    let thread'   = stepThread thread

-

        runqueue' = insertThread thread' runqueue

-

        threads'  = Map.insert tid thread' threads

-

        control'  = advanceControl (threadStepId thread) control in

+

    let (thread', eff) = stepThread thread

+

        runqueue'      = insertThread thread' runqueue

+

        threads'       = Map.insert tid thread' threads

+

        control'       = advanceControl (threadStepId thread) control

+

        races'         = updateRaces thread simstate in

+

+

    SimPORTrace time tid tstep tlbl (EventEffect vClock eff) .

+

    SimPORTrace time tid tstep tlbl (EventRaces races') <$>

    reschedule simstate { runqueue = runqueue',

                          threads  = threads',

-

                          races    = updateRacesInSimState thread simstate,

+

                          races    = races',

                          control  = control' }

deschedule Interruptable thread@Thread {

                        simstate@SimState{ curTime = time, threads } = do

m

io-sim/src/Control/Monad/IOSimPOR/QuickCheckUtils.hs

+10/-30

+

{-# LANGUAGE BangPatterns #-}

+

{-# OPTIONS_GHC -Wno-name-shadowing #-}

module Control.Monad.IOSimPOR.QuickCheckUtils where

-

import           Control.Parallel

+

import           Control.Monad.ST.Lazy

import           Test.QuickCheck.Gen

import           Test.QuickCheck.Property

-

-- Take the conjunction of several properties, in parallel This is a

-

-- modification of code from Test.QuickCheck.Property, to run non-IO

-

-- properties in parallel. It also takes care NOT to label its result

-

-- as an IO property (using IORose), unless one of its arguments is

-

-- itself an IO property. This is needed to permit parallel testing.

-

conjoinPar :: TestableNoCatch prop => [prop] -> Property

-

conjoinPar = conjoinSpeculate speculate

-

  where

-

  -- speculation tries to evaluate each Rose tree in parallel, to WHNF

-

  -- This will not perform any IO, but should evaluate non-IO properties

-

  -- completely.

-

  speculate [] = []

-

  speculate (rose:roses) = roses' `par` rose' `pseq` (rose':roses')

-

    where rose' = case rose of

-

                    MkRose result _ -> let ans = maybe True id $ ok result in ans `pseq` rose

-

                    IORose _        -> rose

-

          roses' = speculate roses

-

-- We also need a version of conjoin that is sequential, but does not

-- label its result as an IO property unless one of its arguments

-- is. Consequently it does not catch exceptions in its arguments.

+

+

conjoinNoCatchST :: TestableNoCatch prop => [ST s prop] -> ST s Property

+

conjoinNoCatchST sts = do

+

    ps <- sequence sts

+

    return $ conjoinNoCatch ps

+

conjoinNoCatch :: TestableNoCatch prop => [prop] -> Property

conjoinNoCatch = conjoinSpeculate id

        classes = classes result ++ classes r,

        tables = tables result ++ tables r }

-

-- |&&| is a replacement for .&&. that evaluates its arguments in

-

-- parallel. |&&| does NOT label its result as an IO property, unless

-

-- one of its arguments is--which .&&. does. This means that using

-

-- .&&. inside an argument to conjoinPar limits parallelism, while

-

-- |&&| does not.

-

-

infixr 1 |&&|

-

-

(|&&|) :: TestableNoCatch prop => prop -> prop -> Property

-

p |&&| q = conjoinPar [p, q]

-- .&&| is a sequential, but parallelism-friendly version of .&&., that

-- tests its arguments in sequence, but does not label its result as

  propertyNoCatch = MkProperty . return . MkProp . return

instance TestableNoCatch Prop where

-

  propertyNoCatch p = MkProperty . return $ p

+

  propertyNoCatch = MkProperty . return

instance TestableNoCatch prop => TestableNoCatch (Gen prop) where

  propertyNoCatch mp = MkProperty $ do p <- mp; unProperty (againNoCatch $ propertyNoCatch p)

m

io-sim/src/Control/Monad/IOSimPOR/Types.hs

+181/-18

-

module Control.Monad.IOSimPOR.Types where

+

{-# LANGUAGE NamedFieldPuns #-}

+

module Control.Monad.IOSimPOR.Types

+

  ( -- * Effects

+

    Effect (..)

+

  , readEffects

+

  , writeEffects

+

  , forkEffect

+

  , throwToEffect

+

  , wakeupEffects

+

  , onlyReadEffect

+

  , racingEffects

+

  , ppEffect

+

    -- * Schedules

+

  , ScheduleControl (..)

+

  , isDefaultSchedule

+

  , ScheduleMod (..)

+

    -- * Steps

+

  , StepId

+

  , ppStepId

+

  , Step (..)

+

  , StepInfo (..)

+

    -- * Races

+

  , Races (..)

+

  , noRaces

+

  ) where

import qualified Data.List as List

import           Data.Set (Set)

-- Effects

--

-

-- | An `Effect` aggregates effects performed by a thread.  Only used by

-

-- *IOSimPOR*.

+

-- | An `Effect` aggregates effects performed by a thread in a given

+

-- execution step.  Only used by *IOSimPOR*.

--

data Effect = Effect {

    effectReads  :: !(Set TVarId),

    effectWrites :: !(Set TVarId),

-

    effectForks  :: !(Set ThreadId),

-

    effectThrows :: ![ThreadId],

-

    effectWakeup :: ![ThreadId]

+

    effectForks  :: !(Set IOSimThreadId),

+

    effectThrows :: ![IOSimThreadId],

+

    effectWakeup :: !(Set IOSimThreadId)

-

  deriving (Eq, Show)

+

  deriving (Show, Eq)

+

+

ppEffect :: Effect -> String

+

ppEffect Effect { effectReads, effectWrites, effectForks, effectThrows, effectWakeup } =

+

  concat $ [ "Effect { " ]

+

        ++ [ "reads = "  ++ show effectReads  ++ ", " | not (null effectReads)  ]

+

        ++ [ "writes = " ++ show effectWrites ++ ", " | not (null effectWrites) ]

+

        ++ [ "forks = "  ++ ppList ppIOSimThreadId (Set.toList effectForks)  ++ ", " | not (null effectForks)  ]

+

        ++ [ "throws = " ++ ppList ppIOSimThreadId             effectThrows  ++ ", " | not (null effectThrows) ]

+

        ++ [ "wakeup = " ++ ppList ppIOSimThreadId (Set.toList effectWakeup) ++ ", " | not (null effectWakeup) ]

+

        ++ [ "}" ]

+

instance Semigroup Effect where

  Effect r w s ts wu <> Effect r' w' s' ts' wu' =

-

    Effect (r <> r') (w <> w') (s <> s') (ts ++ ts') (wu++wu')

+

    Effect (r <> r') (w <> w') (s <> s') (ts ++ ts') (wu <> wu')

instance Monoid Effect where

-

  mempty = Effect Set.empty Set.empty Set.empty [] []

+

  mempty = Effect Set.empty Set.empty Set.empty [] Set.empty

+

+

--

+

-- Effect smart constructors

+

--

-- readEffect :: SomeTVar s -> Effect

-- readEffect r = mempty{effectReads = Set.singleton $ someTvarId r }

writeEffects :: [SomeTVar s] -> Effect

writeEffects rs = mempty{effectWrites = Set.fromList (map someTvarId rs)}

-

forkEffect :: ThreadId -> Effect

-

forkEffect tid = mempty{effectForks = Set.singleton $ tid}

+

forkEffect :: IOSimThreadId -> Effect

+

forkEffect tid = mempty{effectForks = Set.singleton tid}

-

throwToEffect :: ThreadId -> Effect

+

throwToEffect :: IOSimThreadId -> Effect

throwToEffect tid = mempty{ effectThrows = [tid] }

-

wakeupEffects :: [ThreadId] -> Effect

-

wakeupEffects tids = mempty{effectWakeup = tids}

+

wakeupEffects :: [IOSimThreadId] -> Effect

+

wakeupEffects tids = mempty{effectWakeup = Set.fromList tids}

+

+

--

+

-- Utils

+

--

someTvarId :: SomeTVar s -> TVarId

someTvarId (SomeTVar r) = tvarId r

onlyReadEffect :: Effect -> Bool

onlyReadEffect e = e { effectReads = effectReads mempty } == mempty

+

-- | Check if two effects race.  The two effects are assumed to come from

+

-- different threads, from steps which do not wake one another, see

+

-- `racingSteps`.

+

--

racingEffects :: Effect -> Effect -> Bool

racingEffects e e' =

-

      effectThrows e       `intersectsL` effectThrows e'

-

   || effectReads  e       `intersects`  effectWrites e'

-

   || effectWrites e       `intersects`  effectReads  e'

-

   || effectWrites e       `intersects`  effectWrites e'

+

+

       -- both effects throw to the same threads

+

       effectThrows e `intersectsL` effectThrows e'

+

+

       -- concurrent reads & writes of the same TVars

+

    || effectReads  e `intersects`  effectWrites e'

+

    || effectWrites e `intersects`  effectReads  e'

+

+

       -- concurrent writes to the same TVars

+

    || effectWrites e `intersects`  effectWrites e'

+

  where

    intersects :: Ord a => Set a -> Set a -> Bool

    intersects a b = not $ a `Set.disjoint` b

    intersectsL :: Eq a => [a] -> [a] -> Bool

    intersectsL a b = not $ null $ a `List.intersect` b

+

+

+

---

+

--- Schedules

+

---

+

+

-- | Modified execution schedule.

+

--

+

data ScheduleControl = ControlDefault

+

                     -- ^ default scheduling mode

+

                     | ControlAwait [ScheduleMod]

+

                     -- ^ if the current control is 'ControlAwait', the normal

+

                     -- scheduling will proceed, until the thread found in the

+

                     -- first 'ScheduleMod' reaches the given step.  At this

+

                     -- point the thread is put to sleep, until after all the

+

                     -- steps are followed.

+

                     | ControlFollow [StepId] [ScheduleMod]

+

                     -- ^ follow the steps then continue with schedule

+

                     -- modifications.  This control is set by 'followControl'

+

                     -- when 'controlTargets' returns true.

+

  deriving (Eq, Ord, Show)

+

+

+

isDefaultSchedule :: ScheduleControl -> Bool

+

isDefaultSchedule ControlDefault        = True

+

isDefaultSchedule (ControlFollow [] []) = True

+

isDefaultSchedule _                     = False

+

+

-- | A schedule modification inserted at given execution step.

+

--

+

data ScheduleMod = ScheduleMod{

+

    -- | Step at which the 'ScheduleMod' is activated.

+

    scheduleModTarget    :: StepId,

+

    -- | 'ScheduleControl' at the activation step.  It is needed by

+

    -- 'extendScheduleControl' when combining the discovered schedule with the

+

    -- initial one.

+

    scheduleModControl   :: ScheduleControl,

+

    -- | Series of steps which are executed at the target step.  This *includes*

+

    -- the target step, not necessarily as the last step.

+

    scheduleModInsertion :: [StepId]

+

+

  deriving (Eq, Ord)

+

+

+

instance Show ScheduleMod where

+

  showsPrec d (ScheduleMod tgt ctrl insertion) =

+

    showParen (d>10) $

+

      showString "ScheduleMod " .

+

      showsPrec 11 tgt .

+

      showString " " .

+

      showsPrec 11 ctrl .

+

      showString " " .

+

      showsPrec 11 insertion

+

+

--

+

-- Steps

+

--

+

+

data Step = Step {

+

    stepThreadId :: !IOSimThreadId,

+

    stepStep     :: !Int,

+

    stepEffect   :: !Effect,

+

    stepVClock   :: !VectorClock

+

+

  deriving Show

+

+

m

io-sim/test/Main.hs

+1/-1

tests :: TestTree

tests =

-

  testGroup "IO Sim"

+

  testGroup "io-sim-tests"

  [ Test.Control.Concurrent.Class.MonadMVar.tests

  , Test.Control.Monad.IOSim.tests

  , Test.Control.Monad.IOSimPOR.tests

m

io-sim/test/Test/Control/Monad/IOSim.hs

+1/-1

tests :: TestTree

tests =

-

  testGroup "IO simulator"

+

  testGroup "IOSim"

  [ testProperty "read/write graph (IO)"    prop_stm_graph_io

  , testProperty "read/write graph (IOSim)" (withMaxSuccess 1000 prop_stm_graph_sim)

  , testGroup "timeouts"

m

io-sim/test/Test/Control/Monad/IOSimPOR.hs

+180/-113

-

{-# LANGUAGE DeriveGeneric       #-}

-

{-# LANGUAGE FlexibleContexts    #-}

-

{-# LANGUAGE LambdaCase          #-}

-

{-# LANGUAGE RankNTypes          #-}

-

{-# LANGUAGE ScopedTypeVariables #-}

+

{-# LANGUAGE DeriveGeneric         #-}

+

{-# LANGUAGE FlexibleContexts      #-}

+

{-# LANGUAGE LambdaCase            #-}

+

{-# LANGUAGE RankNTypes            #-}

+

{-# LANGUAGE PartialTypeSignatures #-}

+

{-# LANGUAGE ScopedTypeVariables   #-}

{-# OPTIONS_GHC -Wno-unused-top-binds #-}

{-# OPTIONS_GHC -Wno-incomplete-uni-patterns #-}

module Test.Control.Monad.IOSimPOR (tests) where

import           Data.Fixed (Micro)

-

import           Data.Foldable (foldl')

+

import           Data.Foldable (foldl', traverse_)

import           Data.Functor (($>))

-

import           Data.IORef

import qualified Data.List as List

import           Data.Map (Map)

import qualified Data.Map as Map

+

import           Data.STRef.Lazy

import           System.Exit

import           System.IO.Error (ioeGetErrorString, isUserError)

-

import           System.IO.Unsafe

import           Control.Exception (ArithException (..), AsyncException)

import           Control.Monad

import           Control.Monad.Fix

-

import           Control.Parallel

+

import           Control.Monad.ST.Lazy (ST, runST)

-

import           Control.Monad.Class.MonadFork

import           Control.Concurrent.Class.MonadSTM

+

import           Control.Monad.Class.MonadAsync

+

import           Control.Monad.Class.MonadFork

import           Control.Monad.Class.MonadSay

import           Control.Monad.Class.MonadTest

import           Control.Monad.Class.MonadThrow

import           Test.QuickCheck

import           Test.Tasty (TestTree, testGroup)

import           Test.Tasty.QuickCheck

+

import qualified Data.List.Trace as Trace

tests :: TestTree

tests =

-

  testGroup "IO simulator POR"

-

  [ testProperty "propSimulates"    propSimulates

-

  , testProperty "propExploration"  propExploration

-

  -- , testProperty "propPermutations" propPermutations

+

  testGroup "IOSimPOR"

+

  [ testGroup "schedule exploration"

+

    [ testProperty "propSimulates"    propSimulates

+

    , testProperty "propExploration"  propExploration

+

    , testGroup "issue113"

+

      [ testProperty "wakeup"         unit_issue113_wakeup

+

      , testProperty "racy"           unit_issue113_racy

+

      , testProperty "nonDep"         unit_issue113_nonDep

+

+

    -- , testProperty "propPermutations" propPermutations

+

  , testGroup "IO simulator properties"

    [ testProperty "read/write graph (IOSim)" (withMaxSuccess 1000 prop_stm_graph_sim)

    , testGroup "timeouts"

sortTasks (x:xs)         = (x:) <$> sortTasks xs

sortTasks []             = []

-

interpret :: forall s. TVar (IOSim s) Int -> TVar (IOSim s) [ThreadId (IOSim s)] -> Task -> IOSim s (ThreadId (IOSim s))

-

interpret r t (Task steps) = forkIO $ do

-

    context <- atomically $ do

+

data Compare = AreEqual | AreNotEqual

+

  deriving Show

+

+

instance Arbitrary Compare where

+

  arbitrary = frequency [(8, pure AreEqual),

+

                         (2, pure AreNotEqual)]

+

+

  shrink AreEqual    = []

+

  shrink AreNotEqual = [AreEqual]

+

+

+

interpret :: forall s.

+

             Compare

+

          -> TVar (IOSim s) Int

+

          -> TVar (IOSim s) [ThreadId (IOSim s)]

+

          -> (Int, Task)

+

          -> IOSim s (Async (IOSim s) ())

+

interpret cmp r t (tlbl, Task steps) = async $ do

+

    labelThisThread (show tlbl)

+

    (ts, timer) <- atomically $ do

      ts <- readTVar t

-

      when (null ts) retry

+

      check (not (null ts))

      timer <- newTVar Nothing

      return (ts,timer)

-

    mapM_ (interpretStep context) steps

-

  where interpretStep _ (WhenSet m n) = atomically $ do

-

          a <- readTVar r

-

          when (a/=m) retry

-

          writeTVar r n

-

        interpretStep (ts,_) (ThrowTo i) = throwTo (ts !! i) (ExitFailure 0)

-

        interpretStep _      (Delay i)   = threadDelay (fromIntegral i)

-

        interpretStep (_,timer) (Timeout tstep) = do

-

          timerVal <- atomically $ readTVar timer

-

          case (timerVal,tstep) of

-

            (_,NewTimeout n)            -> do tout <- newTimeout (fromIntegral n)

-

                                              atomically $ writeTVar timer (Just tout)

-

            (Just tout,CancelTimeout)   -> cancelTimeout tout

-

            (Just tout,AwaitTimeout)    -> atomically $ awaitTimeout tout >> return ()

-

            (Nothing,_)                 -> return ()

-

-

runTasks :: [Task] -> IOSim s (Int,Int)

-

runTasks tasks = do

+

    mapM_ (interpretStep ts timer) steps

+

  where

+

    compareFn = case cmp of

+

      AreEqual    -> (==)

+

      AreNotEqual -> (/=)

+

    interpretStep :: [ThreadId (IOSim s)]

+

                  -> TVar (IOSim s) (Maybe (Timeout s))

+

                  -> Step

+

                  -> IOSim s ()

+

    interpretStep _ _ (WhenSet m n) = atomically $ do

+

      readTVar r >>= check . compareFn m

+

      writeTVar r n

+

    interpretStep ts _     (ThrowTo i) = throwTo (ts !! i) (ExitFailure 0)

+

    interpretStep _  _     (Delay i)   = threadDelay (fromIntegral i)

+

    interpretStep _  timer (Timeout tstep) = do

+

      timerVal <- readTVarIO timer

+

      case (timerVal,tstep) of

+

        (_,NewTimeout n)          -> do tout <- newTimeout (fromIntegral n)

+

                                        atomically $ writeTVar timer (Just tout)

+

        (Just tout,CancelTimeout) -> cancelTimeout tout

+

        (Just tout,AwaitTimeout)  -> atomically $ awaitTimeout tout >> return ()

+

        (Nothing,_)               -> return ()

+

+

runTasks :: Compare -> [Task] -> IOSim s (Int,Int)

+

runTasks cmp tasks = do

  let m = maximum [maxTaskValue t | Task t <- tasks]

-

  r  <- atomically $ newTVar m

-

  t  <- atomically $ newTVar []

+

  r  <- newTVarIO m

+

  traceTVarIO r (\_ a -> return (TraceString (show a)))

+

  t  <- newTVarIO []

  exploreRaces

-

  ts <- mapM (interpret r t) tasks

-

  atomically $ writeTVar t ts

-

  threadDelay 1000000000  -- allow the SUT threads to run

-

  a  <- atomically $ readTVar r

+

  ts <- mapM (interpret cmp r t) (zip [1..] tasks)

+

  atomically $ writeTVar t (asyncThreadId <$> ts)

+

  traverse_ wait ts -- allow the SUT threads to run

+

  a  <- readTVarIO r

  return (m,a)

maxTaskValue :: [Step] -> Int

maxTaskValue (WhenSet m _:_) = m

maxTaskValue (_:t)           = maxTaskValue t

maxTaskValue []              = 0

-

propSimulates :: Tasks -> Property

-

propSimulates (Tasks tasks) =

-

  any (not . null . (\(Task steps)->steps)) tasks ==>

-

    let Right (m,a) = runSim (runTasks tasks) in

-

    m>=a

-

-

propExploration :: Tasks -> Property

-

propExploration (Tasks tasks) =

-

  -- Debug.trace ("\nTasks:\n"++ show tasks) $

+

propSimulates :: Compare -> Shrink2 Tasks -> Property

+

propSimulates cmp (Shrink2 (Tasks tasks)) =

  any (not . null . (\(Task steps)->steps)) tasks ==>

-

    traceNoDuplicates $ \addTrace ->

-

    --traceCounter $ \addTrace ->

-

    exploreSimTrace id (runTasks tasks) $ \_ trace ->

-

    --Debug.trace (("\nTrace:\n"++) . splitTrace . noExceptions $ show trace) $

-

    addTrace trace $

-

    counterexample (splitTrace . noExceptions $ show trace) $

+

    let trace = runSimTrace (runTasks cmp tasks) in

    case traceResult False trace of

-

      Right (m,a) -> property $ m>=a

-

      Left e      -> counterexample (show e) False

+

      Right (m,a) -> property (m >= a)

+

      Left (FailureInternal msg)

+

                  -> counterexample msg False

+

      Left x      -> counterexample (ppTrace trace)

+

                   $ counterexample (show x) True

+

+

-- NOTE: This property needs to be executed sequentially, otherwise it fails

+

-- undeterministically, which `exploreSimTraceST` does.

+

--

+

propExploration :: Compare -> (Shrink2 Tasks) -> Property

m

strict-mvar/test/Test/Control/Concurrent/Class/MonadMVar/Strict/WHNF.hs

+0/-1

{-# OPTIONS_GHC -Wno-unrecognised-pragmas #-}

-

{-# HLINT ignore "Use camelCase" #-}

-- | Test whether functions on 'StrictMVar's correctly force values to WHNF

-- before they are put inside the 'StrictMVar'.

Yesterday's Report

Friday, December 1, 2023

606 commits in 72 repos

New Repo Discovered

Thu, 30 Nov 23 15:26:13 +0000 · cf-cip-frontend

JavaScript · No license

New Releases

Fri, 01 Dec 23 15:57:24 +0000 · Cardano Node 8.7.1-pre cardano-node Fri, 01 Dec 23 14:10:59 +0000 · lace-extension 1.7.1 lace Thu, 30 Nov 23 16:12:11 +0000 · Unstable Development Builds mithril Thu, 30 Nov 23 14:25:10 +0000 · PRISM Wallet SDK TypeScript v3.1.0 atala-prism-wallet-sdk-ts Thu, 30 Nov 23 14:21:39 +0000 · Atala PRISM Wallet SDK KMM v2.6.0 atala-prism-wallet-sdk-kmm Thu, 30 Nov 23 10:20:53 +0000 · v0.1.1 adahandle-resolver

3,913 commits this week Nov 25, 2023 - Dec 02, 2023

Showing 25 of 3913 recent commits.