From 5ff263d96f53937adfeaa64f37f2a39c69e4b2fa Mon Sep 17 00:00:00 2001 From: Michael Walker Date: Wed, 26 Aug 2015 22:48:38 +0100 Subject: [PATCH] Rename ThreadAction' to Lookahead --- Test/DejaFu/Deterministic.hs | 2 +- Test/DejaFu/Deterministic/IO.hs | 2 +- Test/DejaFu/Deterministic/Internal.hs | 50 +++---- Test/DejaFu/Deterministic/Internal/Common.hs | 134 +++++++++---------- Test/DejaFu/SCT.hs | 10 +- Test/DejaFu/SCT/Internal.hs | 40 +++--- 6 files changed, 118 insertions(+), 120 deletions(-) diff --git a/Test/DejaFu/Deterministic.hs b/Test/DejaFu/Deterministic.hs index 1c92c64..857046c 100755 --- a/Test/DejaFu/Deterministic.hs +++ b/Test/DejaFu/Deterministic.hs @@ -55,7 +55,7 @@ module Test.DejaFu.Deterministic , Trace , Decision(..) , ThreadAction(..) - , ThreadAction'(..) + , Lookahead(..) , CVarId , CRefId , MaskingState(..) diff --git a/Test/DejaFu/Deterministic/IO.hs b/Test/DejaFu/Deterministic/IO.hs index 0e556c2..12b0a3e 100644 --- a/Test/DejaFu/Deterministic/IO.hs +++ b/Test/DejaFu/Deterministic/IO.hs @@ -59,7 +59,7 @@ module Test.DejaFu.Deterministic.IO , Trace , Decision(..) , ThreadAction(..) - , ThreadAction'(..) + , Lookahead(..) , CVarId , MaskingState(..) , Trace' diff --git a/Test/DejaFu/Deterministic/Internal.hs b/Test/DejaFu/Deterministic/Internal.hs index 755554d..2dea044 100755 --- a/Test/DejaFu/Deterministic/Internal.hs +++ b/Test/DejaFu/Deterministic/Internal.hs @@ -35,7 +35,7 @@ module Test.DejaFu.Deterministic.Internal , Trace , Decision(..) , ThreadAction(..) - , ThreadAction'(..) + , Lookahead(..) , Trace' , showTrace , toTrace @@ -155,30 +155,30 @@ runThreads fixed runstm sched origg origthreads idsrc ref = go idsrc [] Nothing | otherwise = [(if Just t == prior then Continue else SwitchTo t, na) | (t, na) <- runnable', t /= chosen] nextActions t = unsafeToNonEmpty . nextActions' . _continuation . fromJust $ M.lookup t threads - nextActions' (AFork _ _) = [Fork'] - nextActions' (AMyTId _) = [MyThreadId'] - nextActions' (ANew _) = [New'] - nextActions' (APut (c, _) _ k) = Put' c : nextActions' k - nextActions' (ATryPut (c, _) _ _) = [TryPut' c] - nextActions' (AGet (c, _) _) = [Read' c] - nextActions' (ATake (c, _) _) = [Take' c] - nextActions' (ATryTake (c, _) _) = [TryTake' c] - nextActions' (ANewRef _) = [NewRef'] - nextActions' (AReadRef (r, _) _) = [ReadRef' r] - nextActions' (AModRef (r, _) _ _) = [ModRef' r] - nextActions' (AAtom _ _) = [STM'] - nextActions' (AThrow _) = [Throw'] - nextActions' (AThrowTo tid _ k) = ThrowTo' tid : nextActions' k - nextActions' (ACatching _ _ _) = [Catching'] - nextActions' (APopCatching k) = PopCatching' : nextActions' k - nextActions' (AMasking ms _ _) = [SetMasking' False ms] - nextActions' (AResetMask b1 b2 ms k) = (if b1 then SetMasking' else ResetMasking') b2 ms : nextActions' k - nextActions' (ALift _) = [Lift'] - nextActions' (ANoTest _ _) = [NoTest'] - nextActions' (AKnowsAbout _ k) = KnowsAbout' : nextActions' k - nextActions' (AForgets _ k) = Forgets' : nextActions' k - nextActions' (AAllKnown k) = AllKnown' : nextActions' k - nextActions' (AStop) = [Stop'] + nextActions' (AFork _ _) = [WillFork] + nextActions' (AMyTId _) = [WillMyThreadId] + nextActions' (ANew _) = [WillNew] + nextActions' (APut (c, _) _ k) = WillPut c : nextActions' k + nextActions' (ATryPut (c, _) _ _) = [WillTryPut c] + nextActions' (AGet (c, _) _) = [WillRead c] + nextActions' (ATake (c, _) _) = [WillTake c] + nextActions' (ATryTake (c, _) _) = [WillTryTake c] + nextActions' (ANewRef _) = [WillNewRef] + nextActions' (AReadRef (r, _) _) = [WillReadRef r] + nextActions' (AModRef (r, _) _ _) = [WillModRef r] + nextActions' (AAtom _ _) = [WillSTM] + nextActions' (AThrow _) = [WillThrow] + nextActions' (AThrowTo tid _ k) = WillThrowTo tid : nextActions' k + nextActions' (ACatching _ _ _) = [WillCatching] + nextActions' (APopCatching k) = WillPopCatching : nextActions' k + nextActions' (AMasking ms _ _) = [WillSetMasking False ms] + nextActions' (AResetMask b1 b2 ms k) = (if b1 then WillSetMasking else WillResetMasking) b2 ms : nextActions' k + nextActions' (ALift _) = [WillLift] + nextActions' (ANoTest _ _) = [WillNoTest] + nextActions' (AKnowsAbout _ k) = WillKnowsAbout : nextActions' k + nextActions' (AForgets _ k) = WillForgets : nextActions' k + nextActions' (AAllKnown k) = WillAllKnown : nextActions' k + nextActions' (AStop) = [WillStop] -------------------------------------------------------------------------------- -- * Single-step execution diff --git a/Test/DejaFu/Deterministic/Internal/Common.hs b/Test/DejaFu/Deterministic/Internal/Common.hs index dd02f1e..05f7696 100644 --- a/Test/DejaFu/Deterministic/Internal/Common.hs +++ b/Test/DejaFu/Deterministic/Internal/Common.hs @@ -112,17 +112,17 @@ initialIdSource = Id 0 0 0 0 -- attempts to (a) schedule a blocked thread, or (b) schedule a -- nonexistent thread. In either of those cases, the computation will -- be halted. -type Scheduler s = s -> Maybe (ThreadId, ThreadAction) -> NonEmpty (ThreadId, NonEmpty ThreadAction') -> (ThreadId, s) +type Scheduler s = s -> Maybe (ThreadId, ThreadAction) -> NonEmpty (ThreadId, NonEmpty Lookahead) -> (ThreadId, s) -- | One of the outputs of the runner is a @Trace@, which is a log of -- decisions made, alternative decisions (including what action would -- have been performed had that decision been taken), and the action a -- thread took in its step. -type Trace = [(Decision, [(Decision, ThreadAction')], ThreadAction)] +type Trace = [(Decision, [(Decision, Lookahead)], ThreadAction)] -- | Like a 'Trace', but gives more lookahead (where possible) for -- alternative decisions. -type Trace' = [(Decision, [(Decision, NonEmpty ThreadAction')], ThreadAction)] +type Trace' = [(Decision, [(Decision, NonEmpty Lookahead)], ThreadAction)] -- | Throw away information from a 'Trace'' to get just a 'Trace'. toTrace :: Trace' -> Trace @@ -249,78 +249,76 @@ instance NFData ThreadAction where rnf (Read c) = rnf c rnf ta = ta `seq` () --- | A simplified view of the actions that a thread can perform. -data ThreadAction' = - Fork' - -- ^ Start a new thread. - | MyThreadId' - -- ^ Get the 'ThreadId' of the current thread. - | New' - -- ^ Create a new 'CVar'. - | Put' CVarId - -- ^ Put into a 'CVar', possibly waking up some threads. - | TryPut' CVarId - -- ^ Try to put into a 'CVar', possibly waking up some threads. - | Read' CVarId - -- ^ Read from a 'CVar'. - | Take' CVarId - -- ^ Take from a 'CVar', possibly waking up some threads. - | TryTake' CVarId - -- ^ Try to take from a 'CVar', possibly waking up some threads. - | NewRef' - -- ^ Create a new 'CRef'. - | ReadRef' CRefId - -- ^ Read from a 'CRef'. - | ModRef' CRefId - -- ^ Modify a 'CRef'. - | STM' - -- ^ An STM transaction was executed, possibly waking up some +-- | A one-step look-ahead at what a thread will do next. +data Lookahead = + WillFork + -- ^ Will start a new thread. + | WillMyThreadId + -- ^ Will get the 'ThreadId'. + | WillNew + -- ^ Will create a new 'CVar'. + | WillPut CVarId + -- ^ Will put into a 'CVar', possibly waking up some threads. + | WillTryPut CVarId + -- ^ Will try to put into a 'CVar', possibly waking up some threads. + | WillRead CVarId + -- ^ Will read from a 'CVar'. + | WillTake CVarId + -- ^ Will take from a 'CVar', possibly waking up some threads. + | WillTryTake CVarId + -- ^ Will try to take from a 'CVar', possibly waking up some threads. + | WillNewRef + -- ^ Will create a new 'CRef'. + | WillReadRef CRefId + -- ^ Will read from a 'CRef'. + | WillModRef CRefId + -- ^ Will modify a 'CRef'. + | WillSTM + -- ^ Will execute an STM transaction, possibly waking up some -- threads. - | Catching' - -- ^ Register a new exception handler - | PopCatching' - -- ^ Pop the innermost exception handler from the stack. - | Throw' - -- ^ Throw an exception. - | ThrowTo' ThreadId - -- ^ Throw an exception to a thread. - | Killed' - -- ^ Killed by an uncaught exception. - | SetMasking' Bool MaskingState - -- ^ Set the masking state. If 'True', this is being used to set the - -- masking state to the original state in the argument passed to a - -- 'mask'ed function. - | ResetMasking' Bool MaskingState - -- ^ Return to an earlier masking state. If 'True', this is being - -- used to return to the state of the masked block in the argument + | WillCatching + -- ^ Will register a new exception handler + | WillPopCatching + -- ^ Will pop the innermost exception handler from the stack. + | WillThrow + -- ^ Will throw an exception. + | WillThrowTo ThreadId + -- ^ Will throw an exception to a thread. + | WillSetMasking Bool MaskingState + -- ^ Will set the masking state. If 'True', this is being used to + -- set the masking state to the original state in the argument -- passed to a 'mask'ed function. - | Lift' - -- ^ Lift an action from the underlying monad. Note that the + | WillResetMasking Bool MaskingState + -- ^ Will return to an earlier masking state. If 'True', this is + -- being used to return to the state of the masked block in the + -- argument passed to a 'mask'ed function. + | WillLift + -- ^ Will lift an action from the underlying monad. Note that the -- penultimate action in a trace will always be a @Lift@, this is an -- artefact of how the runner works. - | NoTest' - -- ^ A computation annotated with '_concNoTest' was executed in a + | WillNoTest + -- ^ Will execute a computation annotated with '_concNoTest' in a -- single step. - | KnowsAbout' - -- ^ A '_concKnowsAbout' annotation was processed. - | Forgets' - -- ^ A '_concForgets' annotation was processed. - | AllKnown' - -- ^ A '_concALlKnown' annotation was processed. - | Stop' - -- ^ Cease execution and terminate. + | WillKnowsAbout + -- ^ Will process a '_concKnowsAbout' annotation. + | WillForgets + -- ^ Will process a '_concForgets' annotation. + | WillAllKnown + -- ^ Will process a '_concALlKnown' annotation. + | WillStop + -- ^ Will cease execution and terminate. deriving (Eq, Show) -instance NFData ThreadAction' where - rnf (SetMasking' b ms) = b `seq` ms `seq` () - rnf (ResetMasking' b ms) = b `seq` ms `seq` () - rnf (Put' c) = rnf c - rnf (TryPut' c) = rnf c - rnf (Read' c) = rnf c - rnf (Take' c) = rnf c - rnf (TryTake' c) = rnf c - rnf (ReadRef' c) = rnf c - rnf (ModRef' c) = rnf c +instance NFData Lookahead where + rnf (WillSetMasking b ms) = b `seq` ms `seq` () + rnf (WillResetMasking b ms) = b `seq` ms `seq` () + rnf (WillPut c) = rnf c + rnf (WillTryPut c) = rnf c + rnf (WillRead c) = rnf c + rnf (WillTake c) = rnf c + rnf (WillTryTake c) = rnf c + rnf (WillReadRef c) = rnf c + rnf (WillModRef c) = rnf c rnf ta = ta `seq` () -------------------------------------------------------------------------------- diff --git a/Test/DejaFu/SCT.hs b/Test/DejaFu/SCT.hs index 9e4a980..f432798 100755 --- a/Test/DejaFu/SCT.hs +++ b/Test/DejaFu/SCT.hs @@ -128,7 +128,7 @@ sctBounded :: ([Decision] -> Bool) -- the execution so far, the index to insert the -- backtracking point, and the thread to backtrack to. This -- may insert more than one backtracking point. - -> (Maybe (ThreadId, ThreadAction) -> NonEmpty (ThreadId, ThreadAction') -> NonEmpty ThreadId) + -> (Maybe (ThreadId, ThreadAction) -> NonEmpty (ThreadId, Lookahead) -> NonEmpty ThreadId) -- ^ Produce possible scheduling decisions, all will be -- tried. -> (forall t. Conc t a) -> [(Either Failure a, Trace)] @@ -138,7 +138,7 @@ sctBounded bv backtrack initialise c = runIdentity $ sctBoundedM bv backtrack in -- | Variant of 'sctBounded' for computations which do 'IO'. sctBoundedIO :: ([Decision] -> Bool) -> ([BacktrackStep] -> Int -> ThreadId -> [BacktrackStep]) - -> (Maybe (ThreadId, ThreadAction) -> NonEmpty (ThreadId, ThreadAction') -> NonEmpty ThreadId) + -> (Maybe (ThreadId, ThreadAction) -> NonEmpty (ThreadId, Lookahead) -> NonEmpty ThreadId) -> (forall t. ConcIO t a) -> IO [(Either Failure a, Trace)] sctBoundedIO bv backtrack initialise c = sctBoundedM bv backtrack initialise run where run sched s = runConcIO' sched s c @@ -147,7 +147,7 @@ sctBoundedIO bv backtrack initialise c = sctBoundedM bv backtrack initialise run sctBoundedM :: (Functor m, Monad m) => ([Decision] -> Bool) -> ([BacktrackStep] -> Int -> ThreadId -> [BacktrackStep]) - -> (Maybe (ThreadId, ThreadAction) -> NonEmpty (ThreadId, ThreadAction') -> NonEmpty ThreadId) + -> (Maybe (ThreadId, ThreadAction) -> NonEmpty (ThreadId, Lookahead) -> NonEmpty ThreadId) -> (Scheduler SchedState -> SchedState -> m (Either Failure a, SchedState, Trace')) -- ^ Monadic runner, with computation fixed. -> m [(Either Failure a, Trace)] @@ -170,7 +170,7 @@ sctBoundedM bv backtrack initialise run = go initialState where data SchedState = SchedState { _sprefix :: [ThreadId] -- ^ Decisions still to make - , _sbpoints :: Seq (NonEmpty (ThreadId, ThreadAction'), [ThreadId]) + , _sbpoints :: Seq (NonEmpty (ThreadId, Lookahead), [ThreadId]) -- ^ Which threads are runnable at each step, and the alternative -- decisions still to make. , _scvstate :: IntMap Bool @@ -188,7 +188,7 @@ initialSchedState prefix = SchedState -- | BPOR scheduler: takes a list of decisions, and maintains a trace -- including the runnable threads, and the alternative choices allowed -- by the bound-specific initialise function. -bporSched :: (Maybe (ThreadId, ThreadAction) -> NonEmpty (ThreadId, ThreadAction') -> NonEmpty ThreadId) +bporSched :: (Maybe (ThreadId, ThreadAction) -> NonEmpty (ThreadId, Lookahead) -> NonEmpty ThreadId) -> Scheduler SchedState bporSched initialise = force $ \s prior threads -> case _sprefix s of -- If there is a decision available, make it diff --git a/Test/DejaFu/SCT/Internal.hs b/Test/DejaFu/SCT/Internal.hs index 06c0100..906de90 100755 --- a/Test/DejaFu/SCT/Internal.hs +++ b/Test/DejaFu/SCT/Internal.hs @@ -107,7 +107,7 @@ next = go 0 where -- | Produce a list of new backtracking points from an execution -- trace. findBacktrack :: ([BacktrackStep] -> Int -> ThreadId -> [BacktrackStep]) - -> Seq (NonEmpty (ThreadId, ThreadAction'), [ThreadId]) + -> Seq (NonEmpty (ThreadId, Lookahead), [ThreadId]) -> Trace' -> [BacktrackStep] findBacktrack backtrack = go S.empty 0 [] . Sq.viewl where @@ -265,16 +265,16 @@ dependent d1 (_, d2) = cref || cvar || ctvar where ctvar' _ = False -- | Variant of 'dependent' to handle 'ThreadAction''s -dependent' :: ThreadAction -> (ThreadId, ThreadAction') -> Bool -dependent' Lift (_, Lift') = True +dependent' :: ThreadAction -> (ThreadId, Lookahead) -> Bool +dependent' Lift (_, WillLift) = True dependent' (ThrowTo t) (t2, _) = t == t2 dependent' d1 (_, d2) = cref || cvar || ctvar where cref = Just True == ((\(r1, w1) (r2, w2) -> r1 == r2 && (w1 || w2)) <$> cref' d1 <*> cref'' d2) cref' (ReadRef r) = Just (r, False) cref' (ModRef r) = Just (r, True) cref' _ = Nothing - cref'' (ReadRef' r) = Just (r, False) - cref'' (ModRef' r) = Just (r, True) + cref'' (WillReadRef r) = Just (r, False) + cref'' (WillModRef r) = Just (r, True) cref'' _ = Nothing cvar = Just True == ((==) <$> cvar' d1 <*> cvar'' d2) @@ -284,17 +284,17 @@ dependent' d1 (_, d2) = cref || cvar || ctvar where cvar' (Read c) = Just c cvar' (Take c _) = Just c cvar' _ = Nothing - cvar'' (TryPut' c) = Just c - cvar'' (TryTake' c) = Just c - cvar'' (Put' c) = Just c - cvar'' (Read' c) = Just c - cvar'' (Take' c) = Just c + cvar'' (WillTryPut c) = Just c + cvar'' (WillTryTake c) = Just c + cvar'' (WillPut c) = Just c + cvar'' (WillRead c) = Just c + cvar'' (WillTake c) = Just c cvar'' _ = Nothing ctvar = ctvar' d1 && ctvar'' d2 ctvar' (STM _) = True ctvar' _ = False - ctvar'' STM' = True + ctvar'' WillSTM = True ctvar'' _ = False -- * Keeping track of 'CVar' full/empty states @@ -312,18 +312,18 @@ updateCVState cvstate (TryTake c True _) = I.insert c False cvstate updateCVState cvstate _ = cvstate -- | Check if an action will block. -willBlock :: IntMap Bool -> ThreadAction' -> Bool -willBlock cvstate (Put' c) = I.lookup c cvstate == Just True -willBlock cvstate (Take' c) = I.lookup c cvstate == Just False +willBlock :: IntMap Bool -> Lookahead -> Bool +willBlock cvstate (WillPut c) = I.lookup c cvstate == Just True +willBlock cvstate (WillTake c) = I.lookup c cvstate == Just False willBlock _ _ = False -- | Check if a list of actions will block safely (without modifying -- any global state). This allows further lookahead at, say, the -- 'spawn' of a thread (which always starts with 'KnowsAbout'. -willBlockSafely :: IntMap Bool -> [ThreadAction'] -> Bool -willBlockSafely cvstate (KnowsAbout':as) = willBlockSafely cvstate as -willBlockSafely cvstate (Forgets':as) = willBlockSafely cvstate as -willBlockSafely cvstate (AllKnown':as) = willBlockSafely cvstate as -willBlockSafely cvstate (Put' c:_) = willBlock cvstate (Put' c) -willBlockSafely cvstate (Take' c:_) = willBlock cvstate (Take' c) +willBlockSafely :: IntMap Bool -> [Lookahead] -> Bool +willBlockSafely cvstate (WillKnowsAbout:as) = willBlockSafely cvstate as +willBlockSafely cvstate (WillForgets:as) = willBlockSafely cvstate as +willBlockSafely cvstate (WillAllKnown:as) = willBlockSafely cvstate as +willBlockSafely cvstate (WillPut c:_) = willBlock cvstate (WillPut c) +willBlockSafely cvstate (WillTake c:_) = willBlock cvstate (WillTake c) willBlockSafely _ _ = False