dejafu-1.5.1.0: A library for unit-testing concurrent programs.

Copyright(c) 2018 Michael Walker
LicenseMIT
MaintainerMichael Walker <mike@barrucadu.co.uk>
Stabilityexperimental
PortabilityBangPatterns, FlexibleContexts, LambdaCase, RankNTypes
Safe HaskellNone
LanguageHaskell2010

Test.DejaFu.SCT.Internal

Contents

Description

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

Synopsis

Exploration

sct Source #

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' Source #

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 Source #

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 Source #

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

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

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

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

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

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

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

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

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

renumber Source #

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 Source #

Helper function for constructing IDs of any sort.

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

Helper function for deconstructing IDs of any sort.