Test.DejaFu.SCT.Internal

Internal types and functions for SCT. This module is NOT considered to form part of the public interface of this library.

Exploration

sct

Arguments

:: (MonadDejaFu n, HasCallStack)

=> Settings n a

The SCT settings (Way is ignored)

-> ([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.

sct'

Arguments

:: (MonadDejaFu n, HasCallStack)

=> Settings n a

The SCT settings (Way is ignored)

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

-> IORefId

The first available IORefId

-> n [(Either Condition a, Trace)]

Like sct but given a function to run the computation.

simplifyExecution

Arguments

:: (MonadDejaFu n, HasCallStack)

=> Settings n a

The SCT settings (Way is ignored)

-> ConcurrencyState

The initial concurrency state

-> (forall x. Scheduler x -> x -> n (Either Condition a, x, Trace))

Just run the computation

-> ThreadId

The first available ThreadId

-> IORefId

The first available IORefId

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

replay

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)]

Simplify a trace by permuting adjacent independent actions to reduce context switching.

lexicoNormalForm :: Bool -> MemType -> ConcurrencyState -> [(ThreadId, ThreadAction)] -> [(ThreadId, ThreadAction)]

Put a trace into lexicographic (by thread ID) normal form.

permuteBy :: Bool -> MemType -> ConcurrencyState -> [ThreadId -> ThreadId -> Bool] -> [(ThreadId, ThreadAction)] -> [(ThreadId, ThreadAction)]

Swap adjacent independent actions in the trace if a predicate holds.

dropCommits :: Bool -> MemType -> ConcurrencyState -> [(ThreadId, ThreadAction)] -> [(ThreadId, ThreadAction)]

Throw away commit actions which are followed by a memory barrier.

pullBack :: Bool -> MemType -> ConcurrencyState -> [(ThreadId, ThreadAction)] -> [(ThreadId, ThreadAction)]

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)]

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.

renumber

Arguments

:: MemType

The memory model determines how commit threads are numbered.

-> Int

First free thread ID.

-> Int

First free IORef ID.

-> [(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.

Utilities

toId :: Coercible Id a => Int -> a

Helper function for constructing IDs of any sort.

fromId :: Coercible a Id => a -> Int

Helper function for deconstructing IDs of any sort.