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

:: (MonadConc n, HasCallStack)

=> Settings n a

The SCT settings (Way is ignored)

-> ([ThreadId] -> s)

Initial state

-> (s -> Maybe t)

State predicate

-> ((Scheduler g -> g -> n (Either Failure a, g, Trace)) -> s -> t -> n (s, Maybe (Either Failure a, Trace)))

Run the computation and update the state

-> ConcT n a

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

General-purpose SCT function.

sct'

Arguments

:: (MonadConc n, HasCallStack)

=> Settings n a

The SCT settings (Way is ignored)

-> s

Initial state

-> (s -> Maybe t)

State predicate

-> (s -> t -> n (s, Maybe (Either Failure a, Trace)))

Run the computation and update the state

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

Just run the computation

-> ThreadId

The first available ThreadId

-> CRefId

The first available CRefId

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

Like sct but given a function to run the computation.

simplifyExecution

Arguments

:: (MonadConc n, HasCallStack)

=> Settings n a

The SCT settings (Way is ignored)

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

Just run the computation

-> ThreadId

The first available ThreadId

-> CRefId

The first available CRefId

-> Either Failure a

The expected result

-> Trace

-> n (Either Failure 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

:: MonadConc n

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

Run the computation

-> [(ThreadId, ThreadAction)]

The reduced sequence of scheduling decisions

-> n (Either Failure a, [(ThreadId, ThreadAction)], Trace)

Replay an execution.

Schedule simplification

simplify :: MemType -> [(ThreadId, ThreadAction)] -> [(ThreadId, ThreadAction)]

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

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

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

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

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

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

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

pullBack :: MemType -> [(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 :: MemType -> [(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 CRef ID.

-> [(ThreadId, ThreadAction)]

-> [(ThreadId, ThreadAction)]

Re-number threads and CRefs.

Permuting forks or newCRefs makes the existing numbering invalid, which then causes problems for scheduling. Just re-numbering threads isn't enough, as CRef 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.