diff --git a/Control/Concurrent/Classy.hs b/Control/Concurrent/Classy.hs --- a/Control/Concurrent/Classy.hs +++ b/Control/Concurrent/Classy.hs @@ -1,4 +1,12 @@ --- | Classy concurrency. +-- | +-- Module : Control.Concurrent.Classy +-- Copyright : (c) 2016 Michael Walker +-- License : MIT +-- Maintainer : Michael Walker +-- Stability : experimental +-- Portability : non-portable +-- +-- Classy concurrency. -- -- Concurrency is \"lightweight\", which means that both thread -- creation and context switching overheads are extremely diff --git a/Control/Concurrent/Classy/CRef.hs b/Control/Concurrent/Classy/CRef.hs --- a/Control/Concurrent/Classy/CRef.hs +++ b/Control/Concurrent/Classy/CRef.hs @@ -1,4 +1,12 @@ --- | Mutable references in a concurrency monad. +-- | +-- Module : Control.Concurrent.Classy.CRef +-- Copyright : (c) 2016 Michael Walker +-- License : MIT +-- Maintainer : Michael Walker +-- Stability : stable +-- Portability : portable +-- +-- Mutable references in a concurrency monad. -- -- __Deviations:__ There is no @Eq@ instance for @MonadConc@ the -- @CRef@ type. Furthermore, the @mkWeakIORef@ function is not diff --git a/Control/Concurrent/Classy/Chan.hs b/Control/Concurrent/Classy/Chan.hs --- a/Control/Concurrent/Classy/Chan.hs +++ b/Control/Concurrent/Classy/Chan.hs @@ -1,4 +1,12 @@ --- | Unbounded channels. +-- | +-- Module : Control.Concurrent.Classy.Chan +-- Copyright : (c) 2016 Michael Walker +-- License : MIT +-- Maintainer : Michael Walker +-- Stability : stable +-- Portability : portable +-- +-- Unbounded channels. -- -- __Deviations:__ @Chan@ as defined here does not have an @Eq@ -- instance, this is because the @MonadConc@ @MVar@ type does not have diff --git a/Control/Concurrent/Classy/MVar.hs b/Control/Concurrent/Classy/MVar.hs --- a/Control/Concurrent/Classy/MVar.hs +++ b/Control/Concurrent/Classy/MVar.hs @@ -1,5 +1,13 @@ --- | An @'MVar' t@ is mutable location that is either empty or contains a --- value of type @t@. It has two fundamental operations: 'putMVar' +-- | +-- Module : Control.Concurrent.Classy.MVar +-- Copyright : (c) 2016 Michael Walker +-- License : MIT +-- Maintainer : Michael Walker +-- Stability : stable +-- Portability : portable +-- +-- An @'MVar' t@ is mutable location that is either empty or contains +-- a value of type @t@. It has two fundamental operations: 'putMVar' -- which fills an 'MVar' if it is empty and blocks otherwise, and -- 'takeMVar' which empties an 'MVar' if it is full and blocks -- otherwise. They can be used in multiple different ways: diff --git a/Control/Concurrent/Classy/QSem.hs b/Control/Concurrent/Classy/QSem.hs --- a/Control/Concurrent/Classy/QSem.hs +++ b/Control/Concurrent/Classy/QSem.hs @@ -1,4 +1,12 @@ --- | Simple quantity semaphores. +-- | +-- Module : Control.Concurrent.Classy.QSem +-- Copyright : (c) 2016 Michael Walker +-- License : MIT +-- Maintainer : Michael Walker +-- Stability : stable +-- Portability : portable +-- +-- Simple quantity semaphores. module Control.Concurrent.Classy.QSem ( -- * Simple Quantity Semaphores QSem diff --git a/Control/Concurrent/Classy/QSemN.hs b/Control/Concurrent/Classy/QSemN.hs --- a/Control/Concurrent/Classy/QSemN.hs +++ b/Control/Concurrent/Classy/QSemN.hs @@ -1,4 +1,12 @@ --- | Quantity semaphores in which each thread may wait for an arbitrary +-- | +-- Module : Control.Concurrent.Classy.QSemN +-- Copyright : (c) 2016 Michael Walker +-- License : MIT +-- Maintainer : Michael Walker +-- Stability : stable +-- Portability : portable +-- +-- Quantity semaphores in which each thread may wait for an arbitrary -- \"amount\". module Control.Concurrent.Classy.QSemN ( -- * General Quantity Semaphores diff --git a/Control/Concurrent/Classy/STM.hs b/Control/Concurrent/Classy/STM.hs --- a/Control/Concurrent/Classy/STM.hs +++ b/Control/Concurrent/Classy/STM.hs @@ -1,4 +1,12 @@ --- | Classy software transactional memory. +-- | +-- Module : Control.Concurrent.Classy.STM +-- Copyright : (c) 2016 Michael Walker +-- License : MIT +-- Maintainer : Michael Walker +-- Stability : experimental +-- Portability : non-portable +-- +-- Classy software transactional memory. module Control.Concurrent.Classy.STM ( module Control.Monad.STM.Class , module Control.Concurrent.Classy.STM.TVar diff --git a/Control/Concurrent/Classy/STM/TArray.hs b/Control/Concurrent/Classy/STM/TArray.hs --- a/Control/Concurrent/Classy/STM/TArray.hs +++ b/Control/Concurrent/Classy/STM/TArray.hs @@ -1,6 +1,14 @@ {-# LANGUAGE FlexibleInstances, MultiParamTypeClasses #-} --- | TArrays: transactional arrays, for use in STM-like monads. +-- | +-- Module : Control.Concurrent.Classy.STM. +-- Copyright : (c) 2016 Michael Walker +-- License : MIT +-- Maintainer : Michael Walker +-- Stability : stable +-- Portability : FlexibleInstances, MultiParamTypeClasses +-- +-- TArrays: transactional arrays, for use in STM-like monads. -- -- __Deviations:__ @TArray@ as defined here does not have an @Eq@ -- instance, this is because the @MonadSTM@ @TVar@ type does not have diff --git a/Control/Concurrent/Classy/STM/TBQueue.hs b/Control/Concurrent/Classy/STM/TBQueue.hs --- a/Control/Concurrent/Classy/STM/TBQueue.hs +++ b/Control/Concurrent/Classy/STM/TBQueue.hs @@ -1,4 +1,12 @@ --- | 'TBQueue' is a bounded version of 'TQueue'. The queue has a maximum +-- | +-- Module : Control.Concurrent.Classy.STM.TBQueue +-- Copyright : (c) 2016 Michael Walker +-- License : MIT +-- Maintainer : Michael Walker +-- Stability : stable +-- Portability : portable +-- +-- 'TBQueue' is a bounded version of 'TQueue'. The queue has a maximum -- capacity set when it is created. If the queue already contains the -- maximum number of elements, then 'writeTBQueue' blocks until an -- element is removed from the queue. diff --git a/Control/Concurrent/Classy/STM/TChan.hs b/Control/Concurrent/Classy/STM/TChan.hs --- a/Control/Concurrent/Classy/STM/TChan.hs +++ b/Control/Concurrent/Classy/STM/TChan.hs @@ -1,4 +1,12 @@ --- | Transactional channels +-- | +-- Module : Control.Concurrent.Classy.STM.TChan +-- Copyright : (c) 2016 Michael Walker +-- License : MIT +-- Maintainer : Michael Walker +-- Stability : stable +-- Portability : portable +-- +-- Transactional channels -- -- __Deviations:__ @TChan@ as defined here does not have an @Eq@ -- instance, this is because the @MonadSTM@ @TVar@ type does not have diff --git a/Control/Concurrent/Classy/STM/TMVar.hs b/Control/Concurrent/Classy/STM/TMVar.hs --- a/Control/Concurrent/Classy/STM/TMVar.hs +++ b/Control/Concurrent/Classy/STM/TMVar.hs @@ -1,4 +1,12 @@ --- | Transactional @MVar@s, for use with 'MonadSTM'. +-- | +-- Module : Control.Concurrent.Classy.STM.TMVar +-- Copyright : (c) 2016 Michael Walker +-- License : MIT +-- Maintainer : Michael Walker +-- Stability : stable +-- Portability : portable +-- +-- Transactional @MVar@s, for use with 'MonadSTM'. -- -- __Deviations:__ @TMVar@ as defined here does not have an @Eq@ -- instance, this is because the @MonadSTM@ @TVar@ type does not have diff --git a/Control/Concurrent/Classy/STM/TQueue.hs b/Control/Concurrent/Classy/STM/TQueue.hs --- a/Control/Concurrent/Classy/STM/TQueue.hs +++ b/Control/Concurrent/Classy/STM/TQueue.hs @@ -1,4 +1,12 @@ --- | A 'TQueue' is like a 'TChan', with two important differences: +-- | +-- Module : Control.Concurrent.Classy.STM.TQueue +-- Copyright : (c) 2016 Michael Walker +-- License : MIT +-- Maintainer : Michael Walker +-- Stability : stable +-- Portability : portable +-- +-- A 'TQueue' is like a 'TChan', with two important differences: -- -- * it has faster throughput than both 'TChan' and 'Chan' (although -- the costs are amortised, so the cost of individual operations diff --git a/Control/Concurrent/Classy/STM/TVar.hs b/Control/Concurrent/Classy/STM/TVar.hs --- a/Control/Concurrent/Classy/STM/TVar.hs +++ b/Control/Concurrent/Classy/STM/TVar.hs @@ -1,4 +1,12 @@ --- | Transactional variables, for use with 'MonadSTM'. +-- | +-- Module : Control.Concurrent.Classy.STM.TVar +-- Copyright : (c) 2016 Michael Walker +-- License : MIT +-- Maintainer : Michael Walker +-- Stability : stable +-- Portability : portable +-- +-- Transactional variables, for use with 'MonadSTM'. -- -- __Deviations:__ There is no @Eq@ instance for @MonadSTM@ the @TVar@ -- type. Furthermore, the @newTVarIO@ and @mkWeakTVar@ functions are diff --git a/Control/Monad/Conc/Class.hs b/Control/Monad/Conc/Class.hs --- a/Control/Monad/Conc/Class.hs +++ b/Control/Monad/Conc/Class.hs @@ -4,7 +4,15 @@ {-# LANGUAGE TemplateHaskell #-} {-# LANGUAGE TypeFamilies #-} --- | This module captures in a typeclass the interface of concurrency +-- | +-- Module : Control.Monad.Conc.Class +-- Copyright : (c) 2016 Michael Walker +-- License : MIT +-- Maintainer : Michael Walker +-- Stability : experimental +-- Portability : CPP, FlexibleContexts, RankNTypes, TemplateHaskell, TypeFamilies +-- +-- This module captures in a typeclass the interface of concurrency -- monads. -- -- __Deviations:__ An instance of @MonadCoonc@ is not required to be diff --git a/Control/Monad/STM/Class.hs b/Control/Monad/STM/Class.hs --- a/Control/Monad/STM/Class.hs +++ b/Control/Monad/STM/Class.hs @@ -3,7 +3,15 @@ {-# LANGUAGE TemplateHaskell #-} {-# LANGUAGE TypeFamilies #-} --- | This module provides an abstraction over 'STM', which can be used +-- | +-- Module : Control.Monad.STM.Class +-- Copyright : (c) 2016 Michael Walker +-- License : MIT +-- Maintainer : Michael Walker +-- Stability : experimental +-- Portability : CPP, RankNTypes, TemplateHaskell, TypeFamilies +-- +-- This module provides an abstraction over 'STM', which can be used -- with 'MonadConc'. -- -- This module only defines the 'STM' class; you probably want to diff --git a/Test/DejaFu.hs b/Test/DejaFu.hs --- a/Test/DejaFu.hs +++ b/Test/DejaFu.hs @@ -1,6 +1,14 @@ {-# LANGUAGE RankNTypes #-} --- | Deterministic testing for concurrent computations. +-- | +-- Module : Test.DejaFu +-- Copyright : (c) 2016 Michael Walker +-- License : MIT +-- Maintainer : Michael Walker +-- Stability : experimental +-- Portability : RankNTypes +-- +-- Deterministic testing for concurrent computations. -- -- As an example, consider this program, which has two locks and a -- shared variable. Two threads are spawned, which claim the locks, diff --git a/Test/DejaFu/Deterministic.hs b/Test/DejaFu/Deterministic.hs --- a/Test/DejaFu/Deterministic.hs +++ b/Test/DejaFu/Deterministic.hs @@ -5,7 +5,15 @@ {-# LANGUAGE TypeFamilies #-} {-# LANGUAGE TypeSynonymInstances #-} --- | Deterministic traced execution of concurrent computations. +-- | +-- Module : Test.DejaFu.Deterministic +-- Copyright : (c) 2016 Michael Walker +-- License : MIT +-- Maintainer : Michael Walker +-- Stability : experimental +-- Portability : FlexibleInstances, GeneralizedNewtypeDeriving, MultiParamTypeClasses, RankNTypes, TypeFamilies, TypeSynonymInstances +-- +-- Deterministic traced execution of concurrent computations. -- -- This works by executing the computation on a single thread, calling -- out to the supplied scheduler after each step to determine which diff --git a/Test/DejaFu/Deterministic/Internal.hs b/Test/DejaFu/Deterministic/Internal.hs --- a/Test/DejaFu/Deterministic/Internal.hs +++ b/Test/DejaFu/Deterministic/Internal.hs @@ -1,8 +1,17 @@ {-# LANGUAGE RankNTypes #-} {-# LANGUAGE ScopedTypeVariables #-} --- | Concurrent monads with a fixed scheduler: internal types and --- functions. +-- | +-- Module : Test.DejaFu.Deterministic.Internal +-- Copyright : (c) 2016 Michael Walker +-- License : MIT +-- Maintainer : Michael Walker +-- Stability : experimental +-- Portability : RankNTypes, ScopedTypeVariables +-- +-- Concurrent monads with a fixed scheduler: internal types and +-- functions. This module is NOT considered to form part of the public +-- interface of this library. module Test.DejaFu.Deterministic.Internal ( -- * Execution runFixed @@ -42,6 +51,7 @@ , preEmpCount , showTrace , showFail + , tvarsOf -- * Synchronised and Unsynchronised Actions , ActionType(..) diff --git a/Test/DejaFu/Deterministic/Internal/Common.hs b/Test/DejaFu/Deterministic/Internal/Common.hs --- a/Test/DejaFu/Deterministic/Internal/Common.hs +++ b/Test/DejaFu/Deterministic/Internal/Common.hs @@ -1,17 +1,28 @@ {-# LANGUAGE ExistentialQuantification #-} {-# LANGUAGE RankNTypes #-} --- | Common types and utility functions for deterministic execution of --- 'MonadConc' implementations. +-- | +-- Module : Test.DejaFu.Deterministic.Internal.Common +-- Copyright : (c) 2016 Michael Walker +-- License : MIT +-- Maintainer : Michael Walker +-- Stability : experimental +-- Portability : ExistentialQuantification, RankNTypes +-- +-- Common types and utility functions for deterministic execution of +-- 'MonadConc' implementations. This module is NOT considered to form +-- part of the public interface of this library. module Test.DejaFu.Deterministic.Internal.Common where import Control.DeepSeq (NFData(..)) import Control.Exception (Exception, MaskingState(..)) import Data.Dynamic (Dynamic) import Data.Map.Strict (Map) -import Data.Maybe (mapMaybe) +import Data.Maybe (fromMaybe, mapMaybe) import Data.List (sort, nub, intercalate) import Data.List.NonEmpty (NonEmpty, fromList) +import Data.Set (Set) +import qualified Data.Set as S import Test.DejaFu.Internal import Test.DPOR (Decision(..), Trace) @@ -762,6 +773,20 @@ cvarOf (SynchronisedRead c) = Just c cvarOf (SynchronisedWrite c) = Just c cvarOf _ = Nothing + +-- | Get the 'TVar's affected. +tvarsOf :: ThreadAction -> Set TVarId +tvarsOf act = S.fromList $ case act of + STM trc _ -> concatMap tvarsOf' trc + BlockedSTM trc -> concatMap tvarsOf' trc + _ -> [] + + where + tvarsOf' (TRead tv) = [tv] + tvarsOf' (TWrite tv) = [tv] + tvarsOf' (TOrElse ta tb) = concatMap tvarsOf' (ta ++ fromMaybe [] tb) + tvarsOf' (TCatch ta tb) = concatMap tvarsOf' (ta ++ fromMaybe [] tb) + tvarsOf' _ = [] -- | Throw away information from a 'ThreadAction' and give a -- simplified view of what is happening. diff --git a/Test/DejaFu/Deterministic/Internal/Memory.hs b/Test/DejaFu/Deterministic/Internal/Memory.hs --- a/Test/DejaFu/Deterministic/Internal/Memory.hs +++ b/Test/DejaFu/Deterministic/Internal/Memory.hs @@ -1,7 +1,16 @@ {-# LANGUAGE BangPatterns #-} {-# LANGUAGE GADTs #-} --- | Operations over @CRef@s and @MVar@s +-- | +-- Module : Test.DejaFu.Deterministic.Internal.Memory +-- Copyright : (c) 2016 Michael Walker +-- License : MIT +-- Maintainer : Michael Walker +-- Stability : experimental +-- Portability : BangPatterns, GADTs +-- +-- Operations over @CRef@s and @MVar@s. This module is NOT considered +-- to form part of the public interface of this library. -- -- Relaxed memory operations over @CRef@s are implemented with an -- explicit write buffer: one per thread for TSO, and one per diff --git a/Test/DejaFu/Deterministic/Internal/Threading.hs b/Test/DejaFu/Deterministic/Internal/Threading.hs --- a/Test/DejaFu/Deterministic/Internal/Threading.hs +++ b/Test/DejaFu/Deterministic/Internal/Threading.hs @@ -1,7 +1,16 @@ {-# LANGUAGE ExistentialQuantification #-} {-# LANGUAGE RankNTypes #-} --- | Operations and types for threads. +-- | +-- Module : Test.DejaFu.Deterministic.Internal.Threading +-- Copyright : (c) 2016 Michael Walker +-- License : MIT +-- Maintainer : Michael Walker +-- Stability : experimental +-- Portability : ExistentialQuantification, RankNTypes +-- +-- Operations and types for threads. This module is NOT considered to +-- form part of the public interface of this library. module Test.DejaFu.Deterministic.Internal.Threading where import Control.Exception (Exception, MaskingState(..), SomeException, fromException) diff --git a/Test/DejaFu/Internal.hs b/Test/DejaFu/Internal.hs --- a/Test/DejaFu/Internal.hs +++ b/Test/DejaFu/Internal.hs @@ -1,6 +1,15 @@ {-# LANGUAGE RankNTypes #-} --- | Dealing with mutable state. +-- | +-- Module : Test.DejaFu.Internal +-- Copyright : (c) 2016 Michael Walker +-- License : MIT +-- Maintainer : Michael Walker +-- Stability : experimental +-- Portability : RankNTypes +-- +-- Dealing with mutable state. This module is NOT considered to form +-- part of the public interface of this library. module Test.DejaFu.Internal where import Control.Monad.ST (ST) diff --git a/Test/DejaFu/SCT.hs b/Test/DejaFu/SCT.hs --- a/Test/DejaFu/SCT.hs +++ b/Test/DejaFu/SCT.hs @@ -1,6 +1,15 @@ +{-# LANGUAGE CPP #-} {-# LANGUAGE RankNTypes #-} --- | Systematic testing for concurrent computations. +-- | +-- Module : Test.DejaFu.SCT +-- Copyright : (c) 2016 Michael Walker +-- License : MIT +-- Maintainer : Michael Walker +-- Stability : experimental +-- Portability : CPP, RankNTypes +-- +-- Systematic testing for concurrent computations. module Test.DejaFu.SCT ( -- * Bounded Partial-order Reduction @@ -22,9 +31,7 @@ -- See /Bounded partial-order reduction/, K. Coons, M. Musuvathi, -- K. McKinley for more details. - BacktrackStep(..) - - , sctBounded + sctBounded , sctBoundedIO -- * Combination Bounds @@ -88,14 +95,22 @@ , defaultLengthBound , sctLengthBound , sctLengthBoundIO + + -- * Backtracking + + , BacktrackStep(..) + , BacktrackFunc ) where +import Control.DeepSeq (NFData(..)) +import Control.Exception (MaskingState(..)) import Data.Functor.Identity (Identity(..), runIdentity) import Data.Map.Strict (Map) import qualified Data.Map.Strict as M import Data.Maybe (isJust, fromJust) +import qualified Data.Set as S import Test.DPOR ( DPOR(..), dpor - , BacktrackStep(..), backtrackAt + , BacktrackFunc, BacktrackStep(..), backtrackAt , BoundFunc, (&+&), trueBound , PreemptionBound(..), defaultPreemptionBound, preempBacktrack , FairBound(..), defaultFairBound, fairBound, fairBacktrack @@ -157,11 +172,7 @@ -- corresponding to enabled bound functions. -- -- If no bounds are enabled, just backtrack to the given point. -cBacktrack :: Bounds - -> [BacktrackStep ThreadId ThreadAction Lookahead s] - -> Int - -> ThreadId - -> [BacktrackStep ThreadId ThreadAction Lookahead s] +cBacktrack :: Bounds -> BacktrackFunc ThreadId ThreadAction Lookahead s cBacktrack (Bounds Nothing Nothing Nothing) bs i t = backtrackAt (const False) False bs i t cBacktrack (Bounds pb fb lb) bs i t = lBack . fBack $ pBack bs where pBack backs = if isJust pb then pBacktrack backs i t else backs @@ -193,13 +204,7 @@ -- 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. -pBacktrack :: [BacktrackStep ThreadId ThreadAction Lookahead s] - -- ^ The current backtracking points. - -> Int - -- ^ The point to backtrack to. - -> ThreadId - -- ^ The thread to backtrack to. - -> [BacktrackStep ThreadId ThreadAction Lookahead s] +pBacktrack :: BacktrackFunc ThreadId ThreadAction Lookahead s pBacktrack = preempBacktrack isCommitRef -- | Pre-emption bound function. This is different to @preempBound@ in @@ -235,13 +240,7 @@ -- | Add a backtrack point. If the thread isn't runnable, or performs -- a release operation, add all runnable threads. -fBacktrack :: [BacktrackStep ThreadId ThreadAction Lookahead s] - -- ^ The current backtracking points. - -> Int - -- ^ The point to backtrack to. - -> ThreadId - -- ^ The thread to backtrack to. - -> [BacktrackStep ThreadId ThreadAction Lookahead s] +fBacktrack :: BacktrackFunc ThreadId ThreadAction Lookahead s fBacktrack = fairBacktrack willRelease ------------------------------------------------------------------------------- @@ -284,7 +283,7 @@ -- ^ The memory model to use for non-synchronised @CRef@ operations. -> BoundFunc ThreadId ThreadAction Lookahead -- ^ Check if a prefix trace is within the bound - -> ([BacktrackStep ThreadId ThreadAction Lookahead CRState] -> Int -> ThreadId -> [BacktrackStep ThreadId ThreadAction Lookahead CRState]) + -> BacktrackFunc ThreadId ThreadAction Lookahead DepState -- ^ 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 @@ -296,7 +295,7 @@ -- | Variant of 'sctBounded' for computations which do 'IO'. sctBoundedIO :: MemType -> BoundFunc ThreadId ThreadAction Lookahead - -> ([BacktrackStep ThreadId ThreadAction Lookahead CRState] -> Int -> ThreadId -> [BacktrackStep ThreadId ThreadAction Lookahead CRState]) + -> BacktrackFunc ThreadId ThreadAction Lookahead DepState -> ConcIO a -> IO [(Either Failure a, Trace ThreadId ThreadAction Lookahead)] sctBoundedIO memtype bf backtrack c = sctBoundedM memtype bf backtrack run where run memty sched s = runConcIO sched memty s c @@ -305,17 +304,21 @@ sctBoundedM :: Monad m => MemType -> ([(Decision ThreadId, ThreadAction)] -> (Decision ThreadId, Lookahead) -> Bool) - -> ([BacktrackStep ThreadId ThreadAction Lookahead CRState] -> Int -> ThreadId -> [BacktrackStep ThreadId ThreadAction Lookahead CRState]) + -> BacktrackFunc ThreadId ThreadAction Lookahead DepState -> (forall s. MemType -> Scheduler ThreadId ThreadAction Lookahead s -> s -> m (Either Failure a, s, Trace ThreadId ThreadAction Lookahead)) -- ^ Monadic runner, with computation fixed. -> m [(Either Failure a, Trace ThreadId ThreadAction Lookahead)] sctBoundedM memtype bf backtrack run = dpor didYield willYield - initialCRState - updateCRState + initialDepState + updateDepState (dependent memtype) (dependent' memtype) +#if MIN_VERSION_dpor(0,2,0) + -- dpor-0.2 knows about daemon threads. + (\_ (t, l) _ -> t == initialThread && case l of WillStop -> True; _ -> False) +#endif initialThread (>=initialThread) bf @@ -348,51 +351,92 @@ -- Dependency function -- | Check if an action is dependent on another. -dependent :: MemType -> CRState -> (ThreadId, ThreadAction) -> (ThreadId, ThreadAction) -> Bool +dependent :: MemType -> DepState -> (ThreadId, ThreadAction) -> (ThreadId, ThreadAction) -> Bool -- This is basically the same as 'dependent'', but can make use of the -- additional information in a 'ThreadAction' to make different -- decisions in a few cases: -- --- - Firstly, @SetNumCapabilities@ and @GetNumCapabilities@ are NOT --- dependent IF the value read is the same as the value --- written. 'dependent'' can not see the value read (as it hasn't --- happened yet!), and so is more pessimistic here. +-- - @SetNumCapabilities@ and @GetNumCapabilities@ are NOT dependent +-- IF the value read is the same as the value written. 'dependent'' +-- can not see the value read (as it hasn't happened yet!), and so +-- is more pessimistic here. -- --- - Secondly, the @isBlock@ / @isBarrier@ case in 'dependent'' is --- NOT a sound optimisation when dealing with a 'ThreadAction' that --- has been converted to a 'Lookahead'. I'm not entirely sure why, --- which makes me question whether the \"optimisation\" is sound as --- it is. +-- - When masked interruptible, a thread can only be interrupted when +-- actually blocked. 'dependent'' has to assume that all +-- potentially-blocking operations can block, and so is more +-- pessimistic in this case. +-- +-- - The @isBlock@ / @isBarrier@ case in 'dependent'' is NOT a sound +-- optimisation when dealing with a 'ThreadAction' that has been +-- converted to a 'Lookahead'. I'm not entirely sure why, which +-- makes me question whether the \"optimisation\" is sound as it +-- is. +-- +-- - Dependency of STM transactions can be /greatly/ improved here, +-- as the 'Lookahead' does not know which @TVar@s will be touched, +-- and so has to assume all transactions are dependent. dependent _ _ (_, SetNumCapabilities a) (_, GetNumCapabilities b) = a /= b -dependent memtype buf (t1, a1) (t2, a2) = case rewind a2 of - Just l2 | not (isBlock a1 && isBarrier (simplify' l2)) -> - dependent' memtype buf (t1, a1) (t2, l2) - _ -> dependentActions memtype buf (simplify a1) (simplify a2) +dependent _ ds (_, ThrowTo t) (t2, a) = t == t2 && canInterrupt ds t2 a +dependent memtype ds (t1, a1) (t2, a2) = case rewind a2 of + Just l2 + | isSTM a1 && isSTM a2 + -> not . S.null $ tvarsOf a1 `S.intersection` tvarsOf a2 + | not (isBlock a1 && isBarrier (simplify' l2)) -> + dependent' memtype ds (t1, a1) (t2, l2) + _ -> dependentActions memtype ds (simplify a1) (simplify a2) --- | Variant of 'dependent' to handle 'ThreadAction''s -dependent' :: MemType -> CRState -> (ThreadId, ThreadAction) -> (ThreadId, Lookahead) -> Bool -dependent' _ _ (_, Lift) (_, WillLift) = True -dependent' _ _ (_, ThrowTo t) (t2, WillStop) | t == t2 = False -dependent' _ _ (t2, Stop) (_, WillThrowTo t) | t == t2 = False -dependent' _ _ (_, ThrowTo t) (t2, _) = t == t2 -dependent' _ _ (t2, _) (_, WillThrowTo t) = t == t2 -dependent' _ _ (_, STM _ _) (_, WillSTM) = True -dependent' _ _ (_, GetNumCapabilities a) (_, WillSetNumCapabilities b) = a /= b -dependent' _ _ (_, SetNumCapabilities _) (_, WillGetNumCapabilities) = True -dependent' _ _ (_, SetNumCapabilities a) (_, WillSetNumCapabilities b) = a /= b --- This is safe because, if the thread blocks anyway, a context switch --- will occur anyway so there's no point pre-empting the action. --- --- UNLESS the pre-emption would possibly allow for a different relaxed --- memory stage. -dependent' _ _ (_, a1) (_, l2) | isBlock a1 && isBarrier (simplify' l2) = False -dependent' memtype buf (_, a1) (_, l2) = dependentActions memtype buf (simplify a1) (simplify' l2) + where + isSTM (STM _ _) = True + isSTM (BlockedSTM _) = True + isSTM _ = False +-- | Variant of 'dependent' to handle 'Lookahead'. +dependent' :: MemType -> DepState -> (ThreadId, ThreadAction) -> (ThreadId, Lookahead) -> Bool +dependent' memtype ds (t1, a1) (t2, l2) = case (a1, l2) of +#if MIN_VERSION_dpor(0,2,0) + -- dpor-0.2 handles this case, woo. +#else + -- Because Haskell threads are daemonised, when the initial thread + -- stops all child threads do too, this imposes a dependency. + (Stop, _) | t1 == initialThread -> True + (_, WillStop) | t2 == initialThread -> True +#endif + + -- Worst-case assumption: all IO is dependent. + (Lift, WillLift) -> True + + -- Throwing an exception is only dependent with actions in that + -- thread and if the actions can be interrupted. We can also + -- slightly improve on that by not considering interrupting the + -- normal termination of a thread: it doesn't make a difference. + (ThrowTo t, WillStop) | t == t2 -> False + (Stop, WillThrowTo t) | t == t1 -> False + (ThrowTo t, _) -> t == t2 && canInterruptL ds t2 l2 + (_, WillThrowTo t) -> t == t1 && canInterrupt ds t1 a1 + + -- Another worst-case: assume all STM is dependent. + (STM _ _, WillSTM) -> True + + -- This is a bit pessimistic: Set/Get are only dependent if the + -- value set is not the same as the value that will be got, but we + -- can't know that here. 'dependent' optimises this case. + (GetNumCapabilities a, WillSetNumCapabilities b) -> a /= b + (SetNumCapabilities _, WillGetNumCapabilities) -> True + (SetNumCapabilities a, WillSetNumCapabilities b) -> a /= b + + -- Don't impose a dependency if the other thread will immediately + -- block already. This is safe because a context switch will occur + -- anyway so there's no point pre-empting the action UNLESS the + -- pre-emption would possibly allow for a different relaxed memory + -- stage. + _ | isBlock a1 && isBarrier (simplify' l2) -> False + | otherwise -> dependentActions memtype ds (simplify a1) (simplify' l2) + -- | Check if two 'ActionType's are dependent. Note that this is not -- sufficient to know if two 'ThreadAction's are dependent, without -- being so great an over-approximation as to be useless! -dependentActions :: MemType -> CRState -> ActionType -> ActionType -> Bool -dependentActions memtype buf a1 a2 = case (a1, a2) of +dependentActions :: MemType -> DepState -> ActionType -> ActionType -> Bool +dependentActions memtype ds a1 a2 = case (a1, a2) of -- Unsynchronised reads and writes are always dependent, even under -- a relaxed memory model, as an unsynchronised write gives rise to -- a commit, which synchronises. @@ -404,13 +448,13 @@ -- empty. -- -- See [RMMVerification], lemma 5.25. - (UnsynchronisedWrite r1, _) | same crefOf && isCommit a2 r1 && isBuffered buf r1 -> False - (_, UnsynchronisedWrite r2) | same crefOf && isCommit a1 r2 && isBuffered buf r2 -> False + (UnsynchronisedWrite r1, _) | same crefOf && isCommit a2 r1 && isBuffered ds r1 -> False + (_, UnsynchronisedWrite r2) | same crefOf && isCommit a1 r2 && isBuffered ds r2 -> False -- Unsynchronised reads where a memory barrier would flush a -- buffered write - (UnsynchronisedRead r1, _) | isBarrier a2 -> isBuffered buf r1 && memtype /= SequentialConsistency - (_, UnsynchronisedRead r2) | isBarrier a1 -> isBuffered buf r2 && memtype /= SequentialConsistency + (UnsynchronisedRead r1, _) | isBarrier a2 -> isBuffered ds r1 && memtype /= SequentialConsistency + (_, UnsynchronisedRead r2) | isBarrier a1 -> isBuffered ds r2 && memtype /= SequentialConsistency (_, _) -- Two actions on the same CRef where at least one is synchronised @@ -426,26 +470,104 @@ ------------------------------------------------------------------------------- -- Dependency function state -type CRState = Map CRefId Bool +data DepState = DepState + { depCRState :: Map CRefId Bool + -- ^ Keep track of which @CRef@s have buffered writes. + , depMaskState :: Map ThreadId MaskingState + -- ^ Keep track of thread masking states. If a thread isn't present, + -- the masking state is assumed to be @Unmasked@. This nicely + -- provides compatibility with dpor-0.1, where the thread IDs are + -- not available. + } --- | Initial global 'CRef buffer state. -initialCRState :: CRState -initialCRState = M.empty +instance NFData DepState where + -- Cheats: 'MaskingState' has no 'NFData' instance. + rnf ds = rnf (depCRState ds, M.keys (depMaskState ds)) +-- | Initial dependency state. +initialDepState :: DepState +initialDepState = DepState M.empty M.empty + -- | Update the 'CRef' buffer state with the action that has just -- happened. -updateCRState :: CRState -> ThreadAction -> CRState -updateCRState crstate (CommitRef _ r) = M.delete r crstate -updateCRState crstate (WriteRef r) = M.insert r True crstate -updateCRState crstate ta - | isBarrier $ simplify ta = initialCRState - | otherwise = crstate +#if MIN_VERSION_dpor(0,2,0) +updateDepState :: DepState -> (ThreadId, ThreadAction) -> DepState +updateDepState depstate (tid, act) = DepState + { depCRState = updateCRState act $ depCRState depstate + , depMaskState = updateMaskState tid act $ depMaskState depstate + } +#else +updateDepState :: DepState -> ThreadAction -> DepState +updateDepState depstate act = depstate + { depCRState = updateCRState act $ depCRState depstate } +#endif +-- | Update the 'CRef' buffer state with the action that has just +-- happened. +updateCRState :: ThreadAction -> Map CRefId Bool -> Map CRefId Bool +updateCRState (CommitRef _ r) = M.delete r +updateCRState (WriteRef r) = M.insert r True +updateCRState ta + | isBarrier $ simplify ta = const M.empty + | otherwise = id + +-- | Update the thread masking state with the action that has just +-- happened. +updateMaskState :: ThreadId -> ThreadAction -> Map ThreadId MaskingState -> Map ThreadId MaskingState +updateMaskState tid (Fork tid2) = \masks -> case M.lookup tid masks of + -- A thread inherits the masking state of its parent. + Just ms -> M.insert tid2 ms masks + Nothing -> masks +updateMaskState tid (SetMasking _ ms) = M.insert tid ms +updateMaskState tid (ResetMasking _ ms) = M.insert tid ms +updateMaskState _ _ = id + -- | Check if a 'CRef' has a buffered write pending. --- --- If the state is @Unknown@, this assumes @True@. -isBuffered :: CRState -> CRefId -> Bool -isBuffered crstate r = M.findWithDefault False r crstate +isBuffered :: DepState -> CRefId -> Bool +isBuffered depstate r = M.findWithDefault False r (depCRState depstate) + +-- | Check if an exception can interrupt a thread (action). +canInterrupt :: DepState -> ThreadId -> ThreadAction -> Bool +canInterrupt depstate tid act + -- If masked interruptible, blocked actions can be interrupted. + | isMaskedInterruptible depstate tid = case act of + BlockedPutVar _ -> True + BlockedReadVar _ -> True + BlockedTakeVar _ -> True + BlockedSTM _ -> True + BlockedThrowTo _ -> True + _ -> False + -- If masked uninterruptible, nothing can be. + | isMaskedUninterruptible depstate tid = False + -- If no mask, anything can be. + | otherwise = True + +-- | Check if an exception can interrupt a thread (lookahead). +canInterruptL :: DepState -> ThreadId -> Lookahead -> Bool +canInterruptL depstate tid lh + -- If masked interruptible, actions which can block may be + -- interrupted. + | isMaskedInterruptible depstate tid = case lh of + WillPutVar _ -> True + WillReadVar _ -> True + WillTakeVar _ -> True + WillSTM -> True + WillThrowTo _ -> True + _ -> False + -- If masked uninterruptible, nothing can be. + | isMaskedUninterruptible depstate tid = False + -- If no mask, anything can be. + | otherwise = True + +-- | Check if a thread is masked interruptible. +isMaskedInterruptible :: DepState -> ThreadId -> Bool +isMaskedInterruptible depstate tid = + M.lookup tid (depMaskState depstate) == Just MaskedInterruptible + +-- | Check if a thread is masked uninterruptible. +isMaskedUninterruptible :: DepState -> ThreadId -> Bool +isMaskedUninterruptible depstate tid = + M.lookup tid (depMaskState depstate) == Just MaskedUninterruptible ------------------------------------------------------------------------------- -- Utilities diff --git a/Test/DejaFu/STM.hs b/Test/DejaFu/STM.hs --- a/Test/DejaFu/STM.hs +++ b/Test/DejaFu/STM.hs @@ -2,7 +2,15 @@ {-# LANGUAGE RankNTypes #-} {-# LANGUAGE TypeFamilies #-} --- | A 'MonadSTM' implementation, which can be run on top of 'IO' or +-- | +-- Module : Test.DejaFu.STM +-- Copyright : (c) 2016 Michael Walker +-- License : MIT +-- Maintainer : Michael Walker +-- Stability : experimental +-- Portability : GeneralizedNewtypeDeriving, RankNTypes, TypeFamilies +-- +-- A 'MonadSTM' implementation, which can be run on top of 'IO' or -- 'ST'. module Test.DejaFu.STM ( -- * The @STMLike@ Monad diff --git a/Test/DejaFu/STM/Internal.hs b/Test/DejaFu/STM/Internal.hs --- a/Test/DejaFu/STM/Internal.hs +++ b/Test/DejaFu/STM/Internal.hs @@ -1,8 +1,17 @@ {-# LANGUAGE ExistentialQuantification #-} {-# LANGUAGE RankNTypes #-} --- | 'MonadSTM' testing implementation, internal types and --- definitions. +-- | +-- Module : Test.DejaFu.STM.Internal +-- Copyright : (c) 2016 Michael Walker +-- License : MIT +-- Maintainer : Michael Walker +-- Stability : experimental +-- Portability : ExistentialQuantification, RankNTypes +-- +-- 'MonadSTM' testing implementation, internal types and +-- definitions. This module is NOT considered to form part of the +-- public interface of this library. module Test.DejaFu.STM.Internal where import Control.Exception (Exception, SomeException, fromException, toException) diff --git a/dejafu.cabal b/dejafu.cabal --- a/dejafu.cabal +++ b/dejafu.cabal @@ -2,7 +2,7 @@ -- documentation, see http://haskell.org/cabal/users-guide/ name: dejafu -version: 0.3.1.1 +version: 0.3.2.0 synopsis: Overloadable primitives for testable, potentially non-deterministic, concurrency. description: @@ -75,7 +75,7 @@ source-repository this type: git location: https://github.com/barrucadu/dejafu.git - tag: dejafu-0.3.1.1 + tag: dejafu-0.3.2.0 library exposed-modules: Control.Monad.Conc.Class @@ -113,7 +113,7 @@ , array >=0.5 && <0.6 , atomic-primops >=0.8 && <0.9 , containers >=0.5 && <0.6 - , dpor >=0.1 && <0.2 + , dpor >=0.1 && <0.3 , deepseq >=1.3 && <1.5 , exceptions >=0.7 && <0.9 , monad-control >=1.0 && <1.1