| Copyright | (c) 2018--2020 Michael Walker |
|---|---|
| License | MIT |
| Maintainer | Michael Walker <mike@barrucadu.co.uk> |
| Stability | experimental |
| Portability | BangPatterns, FlexibleContexts, LambdaCase, RankNTypes |
| Safe Haskell | Safe-Inferred |
| Language | Haskell2010 |
Test.DejaFu.SCT.Internal
Description
Internal types and functions for SCT. This module is NOT considered to form part of the public interface of this library.
Synopsis
- sct :: (MonadDejaFu n, HasCallStack) => Settings n a -> ([ThreadId] -> s) -> (s -> Maybe t) -> (ConcurrencyState -> (Scheduler g -> g -> n (Either Condition a, g, Trace)) -> s -> t -> n (s, Maybe (Either Condition a, Trace))) -> Program pty n a -> n [(Either Condition a, Trace)]
- sct' :: (MonadDejaFu n, HasCallStack) => Settings n a -> ConcurrencyState -> s -> (s -> Maybe t) -> (s -> t -> n (s, Maybe (Either Condition a, Trace))) -> (forall x. Scheduler x -> x -> n (Either Condition a, x, Trace)) -> ThreadId -> IORefId -> n [(Either Condition a, Trace)]
- simplifyExecution :: (MonadDejaFu n, HasCallStack) => Settings n a -> ConcurrencyState -> (forall x. Scheduler x -> x -> n (Either Condition a, x, Trace)) -> ThreadId -> IORefId -> Either Condition a -> Trace -> n (Either Condition a, Trace)
- replay :: MonadDejaFu n => (forall x. Scheduler x -> x -> n (Either Condition a, x, Trace)) -> [(ThreadId, ThreadAction)] -> n (Either Condition a, [(ThreadId, ThreadAction)], Trace)
- simplify :: Bool -> MemType -> ConcurrencyState -> [(ThreadId, ThreadAction)] -> [(ThreadId, ThreadAction)]
- lexicoNormalForm :: Bool -> MemType -> ConcurrencyState -> [(ThreadId, ThreadAction)] -> [(ThreadId, ThreadAction)]
- permuteBy :: Bool -> MemType -> ConcurrencyState -> [ThreadId -> ThreadId -> Bool] -> [(ThreadId, ThreadAction)] -> [(ThreadId, ThreadAction)]
- dropCommits :: Bool -> MemType -> ConcurrencyState -> [(ThreadId, ThreadAction)] -> [(ThreadId, ThreadAction)]
- pullBack :: Bool -> MemType -> ConcurrencyState -> [(ThreadId, ThreadAction)] -> [(ThreadId, ThreadAction)]
- pushForward :: Bool -> MemType -> ConcurrencyState -> [(ThreadId, ThreadAction)] -> [(ThreadId, ThreadAction)]
- renumber :: MemType -> Int -> Int -> [(ThreadId, ThreadAction)] -> [(ThreadId, ThreadAction)]
- toId :: Coercible Id a => Int -> a
- fromId :: Coercible a Id => a -> Int
Exploration
Arguments
| :: (MonadDejaFu n, HasCallStack) | |
| => Settings n a | The SCT settings ( |
| -> ([ThreadId] -> s) | Initial state |
| -> (s -> Maybe t) | State predicate |
| -> (ConcurrencyState -> (Scheduler g -> g -> n (Either Condition a, g, Trace)) -> s -> t -> n (s, Maybe (Either Condition a, Trace))) | Run the computation and update the state |
| -> Program pty n a | |
| -> n [(Either Condition a, Trace)] |
General-purpose SCT function.
Arguments
| :: (MonadDejaFu n, HasCallStack) | |
| => Settings n a | The SCT settings ( |
| -> ConcurrencyState | The initial concurrency state |
| -> s | Initial state |
| -> (s -> Maybe t) | State predicate |
| -> (s -> t -> n (s, Maybe (Either Condition a, Trace))) | Run the computation and update the state |
| -> (forall x. Scheduler x -> x -> n (Either Condition a, x, Trace)) | Just run the computation |
| -> ThreadId | The first available |
| -> IORefId | The first available |
| -> n [(Either Condition a, Trace)] |
Like sct but given a function to run the computation.
Arguments
| :: (MonadDejaFu n, HasCallStack) | |
| => Settings n a | The SCT settings ( |
| -> ConcurrencyState | The initial concurrency state |
| -> (forall x. Scheduler x -> x -> n (Either Condition a, x, Trace)) | Just run the computation |
| -> ThreadId | The first available |
| -> IORefId | The first available |
| -> Either Condition a | The expected result |
| -> Trace | |
| -> n (Either Condition a, Trace) |
Given a result and a trace, produce a more minimal trace.
In principle, simplification is semantics preserving and can be done without needing to execute the computation again. However, there are two good reasons to do so:
- It's a sanity check that there are no bugs.
- It's easier to generate a reduced sequence of scheduling decisions and let dejafu generate the full trace, than to generate a reduced trace directly
Unlike shrinking in randomised property-testing tools like QuickCheck or Hedgehog, we only run the test case once, at the end, rather than after every simplification step.
Arguments
| :: MonadDejaFu n | |
| => (forall x. Scheduler x -> x -> n (Either Condition a, x, Trace)) | Run the computation |
| -> [(ThreadId, ThreadAction)] | The reduced sequence of scheduling decisions |
| -> n (Either Condition a, [(ThreadId, ThreadAction)], Trace) |
Replay an execution.
Schedule simplification
simplify :: Bool -> MemType -> ConcurrencyState -> [(ThreadId, ThreadAction)] -> [(ThreadId, ThreadAction)] Source #
Simplify a trace by permuting adjacent independent actions to reduce context switching.
lexicoNormalForm :: Bool -> MemType -> ConcurrencyState -> [(ThreadId, ThreadAction)] -> [(ThreadId, ThreadAction)] Source #
Put a trace into lexicographic (by thread ID) normal form.
permuteBy :: Bool -> MemType -> ConcurrencyState -> [ThreadId -> ThreadId -> Bool] -> [(ThreadId, ThreadAction)] -> [(ThreadId, ThreadAction)] Source #
Swap adjacent independent actions in the trace if a predicate holds.
dropCommits :: Bool -> MemType -> ConcurrencyState -> [(ThreadId, ThreadAction)] -> [(ThreadId, ThreadAction)] Source #
Throw away commit actions which are followed by a memory barrier.
pullBack :: Bool -> MemType -> ConcurrencyState -> [(ThreadId, ThreadAction)] -> [(ThreadId, ThreadAction)] Source #
Attempt to reduce context switches by "pulling" thread actions back to a prior execution of that thread.
Simple example, say we have [(tidA, act1), (tidB, act2), (tidA,
act3)], where act2 and act3 are independent. In this case
pullBack will swap them, giving the sequence [(tidA, act1),
(tidA, act3), (tidB, act2)]. It works for arbitrary separations.
pushForward :: Bool -> MemType -> ConcurrencyState -> [(ThreadId, ThreadAction)] -> [(ThreadId, ThreadAction)] Source #
Attempt to reduce context switches by "pushing" thread actions forward to a future execution of that thread.
This is kind of the opposite of pullBack, but there are cases
where one applies but not the other.
Simple example, say we have [(tidA, act1), (tidB, act2), (tidA,
act3)], where act1 and act2 are independent. In this case
pushForward will swap them, giving the sequence [(tidB, act2),
(tidA, act1), (tidA, act3)]. It works for arbitrary separations.
Arguments
| :: MemType | The memory model determines how commit threads are numbered. |
| -> Int | First free thread ID. |
| -> Int | First free |
| -> [(ThreadId, ThreadAction)] | |
| -> [(ThreadId, ThreadAction)] |
Re-number threads and IORefs.
Permuting forks or newIORefs makes the existing numbering invalid, which then causes problems for scheduling. Just re-numbering threads isn't enough, as IORef IDs are used to determine commit thread IDs.
Renumbered things will not fix their names, so don't rely on those at all.