dejafu-0.5.0.0: Systematic testing for Haskell concurrency.

Copyright (c) 2016 Michael Walker MIT Michael Walker experimental GeneralizedNewtypeDeriving None Haskell2010

Test.DejaFu.SCT

Description

Systematic testing for concurrent computations.

Synopsis

# Running Concurrent Programs

data Way g Source #

How to explore the possible executions of a concurrent program.

Constructors

 Systematically Bounds Systematically explore all executions within the bounds. Randomly g Int Explore a fixed number of random executions, with the given PRNG.

Instances

 Eq g => Eq (Way g) Source # Methods(==) :: Way g -> Way g -> Bool #(/=) :: Way g -> Way g -> Bool # Ord g => Ord (Way g) Source # Methodscompare :: Way g -> Way g -> Ordering #(<) :: Way g -> Way g -> Bool #(<=) :: Way g -> Way g -> Bool #(>) :: Way g -> Way g -> Bool #(>=) :: Way g -> Way g -> Bool #max :: Way g -> Way g -> Way g #min :: Way g -> Way g -> Way g # Read g => Read (Way g) Source # MethodsreadsPrec :: Int -> ReadS (Way g) #readList :: ReadS [Way g] #readPrec :: ReadPrec (Way g) # Show g => Show (Way g) Source # MethodsshowsPrec :: Int -> Way g -> ShowS #show :: Way g -> String #showList :: [Way g] -> ShowS #

Arguments

 :: (MonadRef r n, RandomGen g) => Way g How to run the concurrent program. -> MemType The memory model to use for non-synchronised CRef operations. -> Conc n r a The computation to run many times. -> n [(Either Failure a, Trace)]

Explore possible executions of a concurrent program.

• If the Way is Systematically, sctBound is used.
• If the Way is Randomly, sctRandom is used.

Arguments

 :: (MonadRef r n, RandomGen g, Ord a) => Way g How to run the concurrent program. -> MemType The memory model to use for non-synchronised CRef operations. -> Conc n r a The computation to run many times. -> n (Set (Either Failure a))

Return the set of results of a concurrent program.

# Bounded Partial-order Reduction

We can characterise the state of a concurrent computation by considering the ordering of dependent events. This is a partial order: independent events can be performed in any order without affecting the result, and so are not ordered.

Partial-order reduction is a technique for computing these partial orders, and only testing one total order for each partial order. This cuts down the amount of work to be done significantly. Bounded partial-order reduction is a further optimisation, which only considers schedules within some bound.

This module provides a combination pre-emption, fair, and length bounding runner:

• Pre-emption + fair bounding is useful for programs which use loop/yield control flows but are otherwise terminating.
• Pre-emption, fair + length bounding is useful for non-terminating programs, and used by the testing functionality in Test.DejaFu.

See Bounded partial-order reduction, K. Coons, M. Musuvathi, K. McKinley for more details.

data Bounds Source #

Constructors

 Bounds Fields

Instances

 Source # Methods(==) :: Bounds -> Bounds -> Bool #(/=) :: Bounds -> Bounds -> Bool # Source # Methods(<) :: Bounds -> Bounds -> Bool #(<=) :: Bounds -> Bounds -> Bool #(>) :: Bounds -> Bounds -> Bool #(>=) :: Bounds -> Bounds -> Bool #max :: Bounds -> Bounds -> Bounds #min :: Bounds -> Bounds -> Bounds # Source # Methods Source # MethodsshowsPrec :: Int -> Bounds -> ShowS #showList :: [Bounds] -> ShowS #

No bounds enabled. This forces the scheduler to just use partial-order reduction and sleep sets to prune the search space. This will ONLY work if your computation always terminates!

Arguments

 :: MonadRef r n => MemType The memory model to use for non-synchronised CRef operations. -> Bounds The combined bounds. -> Conc n r a The computation to run many times -> n [(Either Failure a, Trace)]

SCT via BPOR.

Schedules are generated by running the computation with a deterministic scheduler with some initial list of decisions. At each step of execution, possible-conflicting actions are looked for, if any are found, "backtracking points" are added, to cause the events to happen in a different order in a future execution.

Note that unlike with non-bounded partial-order reduction, this may do some redundant work as the introduction of a bound can make previously non-interfering events interfere with each other.

## Pre-emption Bounding

BPOR using pre-emption bounding. This adds conservative backtracking points at the prior context switch whenever a non-conervative backtracking point is added, as alternative decisions can influence the reachability of different states.

See the BPOR paper for more details.

newtype PreemptionBound Source #

Constructors

 PreemptionBound Int

Instances

 Source # Methods Source # Methods Source # Methods Source # Methods Source # Methods Source # Methods Source # Methods Source # MethodsshowList :: [PreemptionBound] -> ShowS #

Arguments

 :: MonadRef r n => MemType The memory model to use for non-synchronised CRef operations. -> PreemptionBound The maximum number of pre-emptions to allow in a single execution -> Conc n r a The computation to run many times -> n [(Either Failure a, Trace)]

An SCT runner using a pre-emption bounding scheduler.

## Fair Bounding

BPOR using fair bounding. This bounds the maximum difference between the number of yield operations different threads have performed.

See the BPOR paper for more details.

newtype FairBound Source #

Constructors

 FairBound Int

Instances

 Source # MethodsenumFrom :: FairBound -> [FairBound] # Source # Methods Source # Methods Source # Methods Source # Methods Source # Methods Source # Methods Source # MethodsshowList :: [FairBound] -> ShowS #

Arguments

 :: MonadRef r n => MemType The memory model to use for non-synchronised CRef operations. -> FairBound The maximum difference between the number of yield operations performed by different threads. -> Conc n r a The computation to run many times -> n [(Either Failure a, Trace)]

An SCT runner using a fair bounding scheduler.

## Length Bounding

BPOR using length bounding. This bounds the maximum length (in terms of primitive actions) of an execution.

newtype LengthBound Source #

Constructors

 LengthBound Int

Instances

 Source # Methods Source # Methods Source # Methods Source # Methods Source # Methods Source # Methods Source # Methods Source # MethodsshowList :: [LengthBound] -> ShowS #

Arguments

 :: MonadRef r n => MemType The memory model to use for non-synchronised CRef operations. -> LengthBound The maximum length of a schedule, in terms of primitive actions. -> Conc n r a The computation to run many times -> n [(Either Failure a, Trace)]

An SCT runner using a length bounding scheduler.

# Random Scheduling

By greatly sacrificing completeness, testing of a large concurrent system can be greatly sped-up. Counter-intuitively, random scheduling has better bug-finding behaviour than just executing a program "for real" many times. This is perhaps because a random scheduler is more chaotic than the real scheduler.

Arguments

 :: (MonadRef r n, RandomGen g) => MemType The memory model to use for non-synchronised CRef operations. -> g The random number generator. -> Int The number of executions to perform. -> Conc n r a The computation to run many times. -> n [(Either Failure a, Trace)]

SCT via random scheduling.

Schedules are generated by assigning to each new thread a random weight. Threads are then scheduled by a weighted random selection.

This is not guaranteed to find all distinct results.