Module kani::futures

This module contains functions to work with futures (and async/.await) in Kani.

Structs

• JoinHandle
  Result of spawning a task.
• RoundRobin
  Keeps cycling through the tasks in a deterministic order

Enums

• SchedulingAssumption
  Indicates to the scheduler whether it can kani::assume that the returned task is running.

Traits

• SchedulingStrategy
  Trait that determines the possible sequence of tasks scheduling for a harness.

Functions

• block_on
  A very simple executor: it polls the future in a busy loop until completion
• block_on_with_spawn
  Polls the given future and the tasks it may spawn until all of them complete
• spawn
  Spawns a task on the current global executor (which is set by block_on_with_spawn)
• yield_now
  Suspends execution of the current future, to allow the scheduler to poll another future