mirror of
https://github.com/barrucadu/dejafu.git
synced 2024-12-18 19:11:37 +03:00
Rename ThreadAction' to Lookahead
This commit is contained in:
Michael Walker
parent
a1144610b2
commit
5ff263d96f
@ -55,7 +55,7 @@ module Test.DejaFu.Deterministic
|
||||
, Trace
|
||||
, Decision(..)
|
||||
, ThreadAction(..)
|
||||
, ThreadAction'(..)
|
||||
, Lookahead(..)
|
||||
, CVarId
|
||||
, CRefId
|
||||
, MaskingState(..)
|
||||
|
||||
@ -59,7 +59,7 @@ module Test.DejaFu.Deterministic.IO
|
||||
, Trace
|
||||
, Decision(..)
|
||||
, ThreadAction(..)
|
||||
, ThreadAction'(..)
|
||||
, Lookahead(..)
|
||||
, CVarId
|
||||
, MaskingState(..)
|
||||
, Trace'
|
||||
|
||||
@ -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
|
||||
|
||||
@ -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` ()
|
||||
|
||||
--------------------------------------------------------------------------------
|
||||
|
||||
@ -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
|
||||
|
||||
@ -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
|
||||
|
||||
Loading…
Reference in New Issue
Block a user