Expand description
Implementations of different scheduling strategies for concurrency testing.
Structs§
- A scheduler that performs an exhaustive, depth-first enumeration of all possible schedules.
- A scheduler that implements the Probabilistic Concurrency Testing (PCT) algorithm.
- A
RandomDataSource
generates non-deterministic data from a random number generator, and arranges to re-seed that RNG on each new execution to enable deterministic replay. - A scheduler that randomly chooses a runnable task at each context switch.
- A scheduler that can replay a chosen schedule deserialized from a string.
- A round robin scheduler that chooses the next available runnable task at each context switch.
- A
Schedule
determines the order in which tasks are to be executed - A
TaskId
is a unique identifier for a task.TaskId
s are never reused within a single execution. - An
UncontrolledNondeterminismCheckScheduler
checks whether a given program exhibits uncontrolled nondeterminism by wrapping an innerScheduler
, and, for each schedule generated by that scheduler, replaying the schedule once. When doing the replay, we check that the schedule is still valid and that the set of runnable tasks is the same at each step. Violations of these checks means that the program exhibits nondeterminism which is not under Shuttle’s control. Note that the opposite is not true — there are no guarantees that the program under test does not have uncontrolled nondeterminism if it passes a run of theUncontrolledNondeterminismCheckScheduler
, even in the case where the wrappedscheduler
is exhaustive.
Traits§
- A
DataSource
is an oracle for generating non-deterministic data to return to a task that asks for random values. - A
Scheduler
is an oracle that decides the order in which to execute concurrent tasks and the data to return to calls for random values.