dejafu 0.3.1.1 → 0.3.2.0

raw patch · 26 files changed

+450/−113 lines, 26 filesdep ~dporPVP: major bump suggested

API removals or changes: PVP suggests a major version bump

Dependency ranges changed: dpor

API changes (from Hackage documentation)

Files

• Control/Concurrent/Classy.hs +9/−1
• Control/Concurrent/Classy/CRef.hs +9/−1
• Control/Concurrent/Classy/Chan.hs +9/−1
• Control/Concurrent/Classy/MVar.hs +10/−2
• Control/Concurrent/Classy/QSem.hs +9/−1
• Control/Concurrent/Classy/QSemN.hs +9/−1
• Control/Concurrent/Classy/STM.hs +9/−1
• Control/Concurrent/Classy/STM/TArray.hs +9/−1
• Control/Concurrent/Classy/STM/TBQueue.hs +9/−1
• Control/Concurrent/Classy/STM/TChan.hs +9/−1
• Control/Concurrent/Classy/STM/TMVar.hs +9/−1
• Control/Concurrent/Classy/STM/TQueue.hs +9/−1
• Control/Concurrent/Classy/STM/TVar.hs +9/−1
• Control/Monad/Conc/Class.hs +9/−1
• Control/Monad/STM/Class.hs +9/−1
• Test/DejaFu.hs +9/−1
• Test/DejaFu/Deterministic.hs +9/−1
• Test/DejaFu/Deterministic/Internal.hs +12/−2
• Test/DejaFu/Deterministic/Internal/Common.hs +28/−3
• Test/DejaFu/Deterministic/Internal/Memory.hs +10/−1
• Test/DejaFu/Deterministic/Internal/Threading.hs +10/−1
• Test/DejaFu/Internal.hs +10/−1
• Test/DejaFu/SCT.hs +203/−81
• Test/DejaFu/STM.hs +9/−1
• Test/DejaFu/STM/Internal.hs +11/−2
• dejafu.cabal +3/−3

@@ -1,4 +1,12 @@--- | Classy concurrency.+-- |+-- Module      : Control.Concurrent.Classy+-- Copyright   : (c) 2016 Michael Walker+-- License     : MIT+-- Maintainer  : Michael Walker <mike@barrucadu.co.uk>+-- Stability   : experimental+-- Portability : non-portable+--+-- Classy concurrency. -- -- Concurrency is \"lightweight\", which means that both thread -- creation and context switching overheads are extremely

@@ -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 <mike@barrucadu.co.uk>+-- 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

@@ -1,4 +1,12 @@--- | Unbounded channels.+-- |+-- Module      : Control.Concurrent.Classy.Chan+-- Copyright   : (c) 2016 Michael Walker+-- License     : MIT+-- Maintainer  : Michael Walker <mike@barrucadu.co.uk>+-- 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

@@ -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 <mike@barrucadu.co.uk>+-- 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:

@@ -1,4 +1,12 @@--- | Simple quantity semaphores.+-- |+-- Module      : Control.Concurrent.Classy.QSem+-- Copyright   : (c) 2016 Michael Walker+-- License     : MIT+-- Maintainer  : Michael Walker <mike@barrucadu.co.uk>+-- Stability   : stable+-- Portability : portable+--+-- Simple quantity semaphores. module Control.Concurrent.Classy.QSem   ( -- * Simple Quantity Semaphores     QSem

@@ -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 <mike@barrucadu.co.uk>+-- Stability   : stable+-- Portability : portable+--+-- Quantity semaphores in which each thread may wait for an arbitrary -- \"amount\". module Control.Concurrent.Classy.QSemN   ( -- * General Quantity Semaphores

@@ -1,4 +1,12 @@--- | Classy software transactional memory.+-- |+-- Module      : Control.Concurrent.Classy.STM+-- Copyright   : (c) 2016 Michael Walker+-- License     : MIT+-- Maintainer  : Michael Walker <mike@barrucadu.co.uk>+-- 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

@@ -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 <mike@barrucadu.co.uk>+-- 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

@@ -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 <mike@barrucadu.co.uk>+-- 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.

@@ -1,4 +1,12 @@--- | Transactional channels+-- |+-- Module      : Control.Concurrent.Classy.STM.TChan+-- Copyright   : (c) 2016 Michael Walker+-- License     : MIT+-- Maintainer  : Michael Walker <mike@barrucadu.co.uk>+-- 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

@@ -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 <mike@barrucadu.co.uk>+-- 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

@@ -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 <mike@barrucadu.co.uk>+-- 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

@@ -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 <mike@barrucadu.co.uk>+-- 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

@@ -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 <mike@barrucadu.co.uk>+-- 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

@@ -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 <mike@barrucadu.co.uk>+-- 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

@@ -1,6 +1,14 @@ {-# LANGUAGE RankNTypes #-} --- | Deterministic testing for concurrent computations.+-- |+-- Module      : Test.DejaFu+-- Copyright   : (c) 2016 Michael Walker+-- License     : MIT+-- Maintainer  : Michael Walker <mike@barrucadu.co.uk>+-- 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,

@@ -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 <mike@barrucadu.co.uk>+-- 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

@@ -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 <mike@barrucadu.co.uk>+-- 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(..)

@@ -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 <mike@barrucadu.co.uk>+-- 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.

@@ -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 <mike@barrucadu.co.uk>+-- 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

@@ -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 <mike@barrucadu.co.uk>+-- 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)

@@ -1,6 +1,15 @@ {-# LANGUAGE RankNTypes #-} --- | Dealing with mutable state.+-- |+-- Module      : Test.DejaFu.Internal+-- Copyright   : (c) 2016 Michael Walker+-- License     : MIT+-- Maintainer  : Michael Walker <mike@barrucadu.co.uk>+-- 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)

@@ -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 <mike@barrucadu.co.uk>+-- 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

@@ -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 <mike@barrucadu.co.uk>+-- 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

@@ -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 <mike@barrucadu.co.uk>+-- 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)

@@ -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