Module 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