Tracking issue for async/await in Kani (feature `async-lib`)

[fzaiser]

Requested feature: async/await Use case: to support popular libraries like tokio Link to relevant documentation (Rust reference, Nomicon, RFC):

• async/await primer
• RFC proposing async/await (partially outdated)

Test case

use std::{
    future::Future,
    pin::Pin,
    task::{Context, RawWaker, RawWakerVTable, Waker},
};

#[kani::proof]
fn main() {
    let result = block_on(async { 42 }, 1);
    assert_eq!(result, Some(42));
}

fn block_on<F: Future>(mut fut: F, limit: usize) -> Option<<F as Future>::Output> {
    let waker = unsafe { Waker::from_raw(NOOP_RAW_WAKER) };
    let cx = &mut Context::from_waker(&waker);
    for _ in 0..limit {
        let pinned = unsafe { Pin::new_unchecked(&mut fut) };
        match pinned.poll(cx) {
            std::task::Poll::Ready(res) => return Some(res),
            std::task::Poll::Pending => continue,
        }
    }
    None
}

const NOOP_RAW_WAKER: RawWaker = {
    unsafe fn clone_waker(_: *const ()) -> RawWaker {
        NOOP_RAW_WAKER
    }
    unsafe fn wake(_: *const ()) {}
    unsafe fn wake_by_ref(_: *const ()) {}
    unsafe fn drop_waker(_: *const ()) {}
    RawWaker::new(
        std::ptr::null(),
        &RawWakerVTable::new(clone_waker, wake, wake_by_ref, drop_waker),
    )
};

Progress

This issue is to track progress on the implementation:

• [x] support generators (PR #1378)
• [x] support async/await (PR #1414)
• [x] add kani::block_on to a new kani::futures library (PR #1427)
• [x] allow #[kani::async_proof] on async functions (no need for poll_repeat in the above example). This could be later extended to allow different runtimes. (PR #1430)
• [ ] https://github.com/model-checking/kani/issues/1663: add tests from popular libraries: futures-rs, async_std, tokio
• [ ] think about how to support task spawning, e.g. tokio::spawn
• [ ] https://github.com/model-checking/kani/issues/1482
• [ ] https://github.com/model-checking/kani/issues/1517

[vrindisbacher]

Hi! I was super excited to see this awesome piece of work. However, it seems like active development on this has stopped. Is that correct? I started using Kani with some async stuff and this worked pretty well. Specifically, I was able to use kani on a nontrivial example using kani::block_on, but using just .await didn't work so well.

[tautschnig]

Hi! I was super excited to see this awesome piece of work. However, it seems like active development on this has stopped. Is that correct? I started using Kani with some async stuff and this worked pretty well. Specifically, I was able to use kani on a nontrivial example using kani::block_on, but using just .await didn't work so well.

It is true that no one that I know of has been able to prioritise working on this. Any contributions would be appreciated, as is feedback that makes this a higher priority!