Trait kani::futures::SchedulingStrategy

source · 
pub trait SchedulingStrategy {
    // Required method
    fn pick_task(&mut self, num_tasks: usize) -> (usize, SchedulingAssumption);
}
Expand description

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

If your harness spawns several tasks, Kani’s scheduler has to decide in what order to poll them. This order may depend on the needs of your verification goal. For example, you sometimes may wish to verify all possible schedulings, i.e. a nondeterministic scheduling strategy.

Nondeterministic scheduling strategies can be very slow to verify because they require Kani to check a large number of permutations of tasks. So if you want to verify a harness that uses spawn, but don’t care about concurrency issues, you can simply use a deterministic scheduling strategy, such as RoundRobin, which polls each task in turn.

Finally, you have the option of providing your own scheduling strategy by implementing this trait. This can be useful, for example, if you want to verify that things work correctly for a very specific task ordering.

Required Methods§

source

fn pick_task(&mut self, num_tasks: usize) -> (usize, SchedulingAssumption)

Picks the next task to be scheduled whenever the scheduler needs to pick a task to run next, and whether it can be assumed that the picked task is still running

Tasks are numbered 0..num_tasks. For example, if pick_task(4) returns (2, CanAssumeRunning) than it picked the task with index 2 and allows Kani to assume that this task is still running. This is useful if the task is chosen nondeterministicall (kani::any()) and allows the verifier to discard useless execution branches (such as polling a completed task again).

As a rule of thumb: if the scheduling strategy picks the next task nondeterministically (using kani::any()), return CanAssumeRunning, otherwise CannotAssumeRunning. When returning CanAssumeRunning, the scheduler will then assume that the picked task is still running, which cuts off “useless” paths where a completed task is polled again. It is even necessary to make things terminate if nondeterminism is involved: if we pick the task nondeterministically, and don’t have the restriction to still running tasks, we could poll the same task over and over again.

However, for most deterministic scheduling strategies, e.g. the round robin scheduling strategy, assuming that the picked task is still running is generally not possible because if that task has ended, we are saying assume(false) and the verification effectively stops (which is undesirable, of course). In such cases, return CannotAssumeRunning instead.

Implementors§