shuttle

Module scheduler

source
Expand description

Implementations of different scheduling strategies for concurrency testing.

Structs§

  • AnnotationScheduler
    An AnnotationScheduler wraps an inner Scheduler and enables the creation of an annotated schedule (for use with Shuttle Explorer). Without enabling the feature annotation, this wrapper does nothing.
  • DfsScheduler
    A scheduler that performs an exhaustive, depth-first enumeration of all possible schedules.
  • PctScheduler
    A scheduler that implements the Probabilistic Concurrency Testing (PCT) algorithm.
  • RandomDataSource
    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.
  • RandomScheduler
    A scheduler that randomly chooses a runnable task at each context switch.
  • ReplayScheduler
    A scheduler that can replay a chosen schedule deserialized from a string.
  • RoundRobinScheduler
    A round robin scheduler that chooses the next available runnable task at each context switch.
  • Schedule
    A Schedule determines the order in which tasks are to be executed
  • Task
    A Task represents a user-level unit of concurrency. Each task has an id that is unique within the execution, and a state reflecting whether the task is runnable (enabled) or not.
  • TaskId
    A TaskId is a unique identifier for a task. TaskIds are never reused within a single execution.
  • UncontrolledNondeterminismCheckScheduler
    An UncontrolledNondeterminismCheckScheduler checks whether a given program exhibits uncontrolled nondeterminism by wrapping an inner Scheduler, 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 the UncontrolledNondeterminismCheckScheduler, even in the case where the wrapped scheduler is exhaustive.

Traits§

  • DataSource
    A DataSource is an oracle for generating non-deterministic data to return to a task that asks for random values.
  • Scheduler
    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.