Module kani::futures

source ·
Expand description

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


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


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


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


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