Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Add kani::spawn and an executor to the Kani library #1659

Merged
merged 46 commits into from
Jul 6, 2023
Merged
Show file tree
Hide file tree
Changes from 12 commits
Commits
Show all changes
46 commits
Select commit Hold shift + click to select a range
c95f710
Add kani::spawn and an executor to the Kani library
fzaiser Sep 5, 2022
1e626b8
Add test
fzaiser Sep 9, 2022
13c01b8
Merge branch 'main' into spawn-lib
fzaiser Sep 9, 2022
2006673
Merge branch 'main' into spawn-lib
fzaiser Oct 31, 2022
b36737b
Address review comments
fzaiser Oct 31, 2022
6fe4f8e
Check bound of num_tasks
fzaiser Oct 31, 2022
0d529f6
Improve documentation and remove unnecessary code
fzaiser Nov 1, 2022
7fd9a5b
Merge branch 'main' into spawn-lib
fzaiser Nov 1, 2022
31d8115
Fix clippy
fzaiser Nov 1, 2022
c7f5a73
Introduce enum for scheduling assumption and improve docs
fzaiser Nov 4, 2022
1db9f81
Disable proof harness to improve CI times
fzaiser Nov 4, 2022
f51186a
Merge branch 'main' into spawn-lib
fzaiser Nov 4, 2022
e65595e
Merge branch 'main' into spawn-lib
fzaiser Nov 7, 2022
9ababc9
Remove nondeterministic harness
fzaiser Nov 8, 2022
6f2ad12
Use the exact same code in manual_spawn.rs and spawn.rs to reproduce …
fzaiser Nov 9, 2022
b4b205e
Merge branch 'main' into spawn-lib
fzaiser Dec 16, 2022
4601765
Fix formatting
fzaiser Dec 16, 2022
cf6af18
Fix submodule
fzaiser Dec 16, 2022
7f88bd1
Use vectors instead of arrays
fzaiser Dec 16, 2022
ffe2374
Fix clippy
fzaiser Dec 16, 2022
71e9ab1
Fix test
fzaiser Dec 16, 2022
2806c40
Make the GLOBAL_EXECUTOR an option.
fzaiser Dec 16, 2022
2b44665
Merge branch 'main' into spawn-lib
fzaiser Dec 16, 2022
3c24fe3
Fix test
fzaiser Dec 20, 2022
eb9a260
Merge branch 'main' into spawn-lib
fzaiser Dec 20, 2022
c6c08ed
Merge branch 'main' into spawn-lib
fzaiser Dec 22, 2022
f6eb352
Remove nondeterministic scheduling strategy
fzaiser Dec 23, 2022
269a080
Merge branch 'main' into spawn-lib
fzaiser Dec 23, 2022
d51ccd0
Merge branch 'main' into spawn-lib
fzaiser Feb 13, 2023
333e51a
Select harness using flags instead of commenting
fzaiser Feb 13, 2023
351ee66
Merge branch 'main' into spawn-lib
fzaiser Feb 13, 2023
fdfb45b
Fix test
fzaiser Feb 13, 2023
2e38a6a
Fix test
fzaiser Feb 13, 2023
a24c117
Merge branch 'main' into spawn-lib
fzaiser Feb 14, 2023
54abbe3
Add additional checks to round-robin test
fzaiser Feb 14, 2023
0bbd42a
Remove manual tests
fzaiser Feb 14, 2023
2ac7346
Rename method to `block_on_with_spawn`
fzaiser Feb 15, 2023
07b4330
Merge branch 'main' into spawn-lib
fzaiser Feb 15, 2023
baed1d1
Update doc comments and add a check
fzaiser Feb 15, 2023
bc948a7
Merge branch 'main' into spawn-lib
fzaiser Jun 23, 2023
ff3f99b
Add unstable attributes
fzaiser Jun 23, 2023
e432a1a
Add -Z async-lib flag
fzaiser Jun 23, 2023
1b8ff44
Merge branch 'main' into spawn-lib
fzaiser Jun 25, 2023
407c435
Merge branch 'main' into spawn-lib
fzaiser Jul 5, 2023
00c64d5
Add reason to unstable APIs
celinval Jul 6, 2023
fd477f8
Merge branch 'main' into spawn-lib
celinval Jul 6, 2023
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
227 changes: 227 additions & 0 deletions library/kani/src/futures.rs
Original file line number Diff line number Diff line change
Expand Up @@ -15,6 +15,9 @@ use std::{
/// Whereas a clever executor like `block_on` in `futures` or `tokio` would interact with the OS scheduler
/// to be woken up when a resource becomes available, this is not supported by Kani.
/// As a consequence, this function completely ignores the waker infrastructure and just polls the given future in a busy loop.
///
/// Note that spawn is not supported with this function. Use [`spawnable_block_on`] if you need it.
// TODO: Give an error if spawn is used in the future passed to this function.
pub fn block_on<T>(mut fut: impl Future<Output = T>) -> T {
let waker = unsafe { Waker::from_raw(NOOP_RAW_WAKER) };
let cx = &mut Context::from_waker(&waker);
Expand All @@ -41,3 +44,227 @@ const NOOP_RAW_WAKER: RawWaker = {

RawWaker::new(std::ptr::null(), &RawWakerVTable::new(clone_waker, noop, noop, noop))
};

static mut GLOBAL_EXECUTOR: Scheduler = Scheduler::new();
const MAX_TASKS: usize = 16;
fzaiser marked this conversation as resolved.
Show resolved Hide resolved

type BoxFuture = Pin<Box<dyn Future<Output = ()> + Sync + 'static>>;

/// Indicates to the scheduler whether it can `kani::assume` that the returned task is running.
///
/// This is useful if the task was picked nondeterministically using `kani::any()`.
/// For more information, see [`SchedulingStrategy`].
pub enum SchedulingAssumption {
CanAssumeRunning,
CannotAssumeRunning,
}

/// 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,
/// provided by [`NondeterministicScheduling`].
///
/// However, this one may poll the same task over and over, which is often undesirable.
/// To ensure some "fairness" in how the tasks are picked, there is [`NondetFairScheduling`].
/// This is probably what you want when verifying a harness under nondeterministic schedulings.
///
/// 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.
pub trait SchedulingStrategy {
fzaiser marked this conversation as resolved.
Show resolved Hide resolved
/// 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
fzaiser marked this conversation as resolved.
Show resolved Hide resolved
///
/// 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.
fn pick_task(&mut self, num_tasks: usize) -> (usize, SchedulingAssumption);
}

/// Keeps cycling through the tasks in a deterministic order
#[derive(Default)]
pub struct RoundRobin {
index: usize,
}

impl SchedulingStrategy for RoundRobin {
#[inline]
fn pick_task(&mut self, num_tasks: usize) -> (usize, SchedulingAssumption) {
self.index = (self.index + 1) % num_tasks;
(self.index, SchedulingAssumption::CannotAssumeRunning)
}
}

/// Picks the next task nondeterministically
#[derive(Default)]
pub struct NondeterministicScheduling;

impl SchedulingStrategy for NondeterministicScheduling {
fn pick_task(&mut self, num_tasks: usize) -> (usize, SchedulingAssumption) {
let index = crate::any();
crate::assume(index < num_tasks);
(index, SchedulingAssumption::CanAssumeRunning)
}
}

/// A restricted form of nondeterministic scheduling to have some fairness.
///
/// Each task has a counter that is increased when it is scheduled.
/// If a task has reached a provided limit, it cannot be scheduled anymore until all other tasks have reached the limit too,
/// at which point all the counters are reset to zero.
pub struct NondetFairScheduling {
counters: [u8; MAX_TASKS],
limit: u8,
}

impl NondetFairScheduling {
#[inline]
pub fn new(limit: u8) -> Self {
Self { counters: [limit; MAX_TASKS], limit }
}
}

impl SchedulingStrategy for NondetFairScheduling {
fn pick_task(&mut self, num_tasks: usize) -> (usize, SchedulingAssumption) {
if self.counters[0..num_tasks] == [0; MAX_TASKS][0..num_tasks] {
self.counters = [self.limit; MAX_TASKS];
}
let index = crate::any();
crate::assume(index < num_tasks);
crate::assume(self.counters[index] > 0);
self.counters[index] -= 1;
(index, SchedulingAssumption::CanAssumeRunning)
}
}

pub(crate) struct Scheduler {
/// Using a Vec instead of an array makes the runtime jump from 40s to almost 10min if using Vec::with_capacity and leads to out of memory with Vec::new (even with 64 GB RAM).
tasks: [Option<BoxFuture>; MAX_TASKS],
num_tasks: usize,
num_running: usize,
}

impl Scheduler {
/// Creates a scheduler with an empty task list
#[inline]
pub(crate) const fn new() -> Scheduler {
const INIT: Option<BoxFuture> = None;
Scheduler { tasks: [INIT; MAX_TASKS], num_tasks: 0, num_running: 0 }
}

/// Adds a future to the scheduler's task list, returning a JoinHandle
pub(crate) fn spawn<F: Future<Output = ()> + Sync + 'static>(&mut self, fut: F) -> JoinHandle {
let index = self.num_tasks;
self.tasks[index] = Some(Box::pin(fut));
assert!(self.num_tasks < MAX_TASKS, "tried to spawn more than {MAX_TASKS} tasks");
self.num_tasks += 1;
self.num_running += 1;
JoinHandle { index }
}

/// Runs the scheduler with the given scheduling plan until all tasks have completed
fn run(&mut self, mut scheduling_plan: impl SchedulingStrategy) {
let waker = unsafe { Waker::from_raw(NOOP_RAW_WAKER) };
fzaiser marked this conversation as resolved.
Show resolved Hide resolved
let cx = &mut Context::from_waker(&waker);
while self.num_running > 0 {
let (index, assumption) = scheduling_plan.pick_task(self.num_tasks);
let task = &mut self.tasks[index];
if let Some(fut) = task.as_mut() {
match fut.as_mut().poll(cx) {
std::task::Poll::Ready(()) => {
self.num_running -= 1;
let _prev = task.take();
}
std::task::Poll::Pending => (),
}
} else if let SchedulingAssumption::CanAssumeRunning = assumption {
crate::assume(false); // useful so that we can assume that a nondeterministically picked task is still running
}
}
}

/// Polls the given future and the tasks it may spawn until all of them complete
fn block_on<F: Future<Output = ()> + Sync + 'static>(
&mut self,
fut: F,
scheduling_plan: impl SchedulingStrategy,
) {
self.spawn(fut);
self.run(scheduling_plan);
}
}

/// Result of spawning a task.
///
/// If you `.await` a JoinHandle, this will wait for the spawned task to complete.
pub struct JoinHandle {
index: usize,
}

impl Future for JoinHandle {
type Output = ();

fn poll(self: Pin<&mut Self>, cx: &mut Context<'_>) -> std::task::Poll<Self::Output> {
if unsafe { GLOBAL_EXECUTOR.tasks[self.index].is_some() } {
std::task::Poll::Pending
} else {
cx.waker().wake_by_ref(); // For completeness. But Kani currently ignores wakers.
std::task::Poll::Ready(())
}
}
}

pub fn spawn<F: Future<Output = ()> + Sync + 'static>(fut: F) -> JoinHandle {
unsafe { GLOBAL_EXECUTOR.spawn(fut) }
}

/// Polls the given future and the tasks it may spawn until all of them complete
///
/// Contrary to [`block_on`], this allows `spawn`ing other futures
pub fn spawnable_block_on<F: Future<Output = ()> + Sync + 'static>(
fut: F,
scheduling_plan: impl SchedulingStrategy,
) {
unsafe {
GLOBAL_EXECUTOR.block_on(fut, scheduling_plan);
}
}

/// Suspends execution of the current future, to allow the scheduler to poll another future
///
/// Specifically, it returns a future that
pub fn yield_now() -> impl Future<Output = ()> {
struct YieldNow {
yielded: bool,
}

impl Future for YieldNow {
type Output = ();

fn poll(mut self: Pin<&mut Self>, cx: &mut Context<'_>) -> std::task::Poll<Self::Output> {
if self.yielded {
cx.waker().wake_by_ref(); // For completeness. But Kani currently ignores wakers.
std::task::Poll::Ready(())
} else {
self.yielded = true;
std::task::Poll::Pending
}
}
}

YieldNow { yielded: false }
}
5 changes: 4 additions & 1 deletion library/kani/src/lib.rs
Original file line number Diff line number Diff line change
Expand Up @@ -14,7 +14,10 @@ pub mod vec;
pub use arbitrary::Arbitrary;
#[cfg(feature = "concrete_playback")]
pub use concrete_playback::concrete_playback_run;
pub use futures::block_on;
pub use futures::{
block_on, spawn, spawnable_block_on, yield_now, NondetFairScheduling,
NondeterministicScheduling, RoundRobin,
};

/// Creates an assumption that will be valid after this statement run. Note that the assumption
/// will only be applied for paths that follow the assumption. If the assumption doesn't hold, the
Expand Down
50 changes: 50 additions & 0 deletions tests/kani/AsyncAwait/spawn.rs
Original file line number Diff line number Diff line change
@@ -0,0 +1,50 @@
// Copyright Kani Contributors
// SPDX-License-Identifier: Apache-2.0 OR MIT
//
// compile-flags: --edition 2018
// kani-flags: --enable-unstable --mir-linker
fzaiser marked this conversation as resolved.
Show resolved Hide resolved

//! This file tests the executor and spawn infrastructure from the Kani library.

use std::sync::{
atomic::{AtomicI64, Ordering},
Arc,
};

#[kani::proof]
#[kani::unwind(4)]
fn deterministic_schedule() {
fzaiser marked this conversation as resolved.
Show resolved Hide resolved
let x = Arc::new(AtomicI64::new(0)); // Surprisingly, Arc verified faster than Rc
let x2 = x.clone();
kani::spawnable_block_on(
async move {
let x3 = x2.clone();
kani::spawn(async move {
x3.fetch_add(1, Ordering::Relaxed);
fzaiser marked this conversation as resolved.
Show resolved Hide resolved
});
kani::yield_now().await;
x2.fetch_add(1, Ordering::Relaxed);
fzaiser marked this conversation as resolved.
Show resolved Hide resolved
},
kani::RoundRobin::default(),
);
assert_eq!(x.load(Ordering::Relaxed), 2);
}

// #[kani::proof]
// #[kani::unwind(4)]
fn nondeterministic_schedule() {
let x = Arc::new(AtomicI64::new(0)); // Surprisingly, Arc verified faster than Rc
let x2 = x.clone();
kani::spawnable_block_on(
async move {
let x3 = x2.clone();
kani::spawn(async move {
x3.fetch_add(1, Ordering::Relaxed);
});
kani::yield_now().await;
x2.fetch_add(1, Ordering::Relaxed);
},
kani::NondetFairScheduling::new(2),
);
assert_eq!(x.load(Ordering::Relaxed), 2);
}