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

Copyright (c) 2018--2019 Michael Walker MIT Michael Walker experimental BangPatterns, FlexibleContexts, LambdaCase, RankNTypes None 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

# Exploration

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.

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.

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.

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 a trace by permuting adjacent independent actions to reduce context switching.

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

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

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

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.

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 IORef ID. -> [(ThreadId, ThreadAction)] -> [(ThreadId, ThreadAction)]

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

Helper function for constructing IDs of any sort.

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

Helper function for deconstructing IDs of any sort.