Implement kani::spawn

[fzaiser]

For asynchronous code, it's important to be able to spawn tasks. Since tokio::spawn or something similar will be difficult to support, we should provide our own version that is optimized for Kani. Part of #1393

[soareschen]

I tried to implement a basic async task scheduler similar to #1659. However I ran into performance issues that the non-deterministic execution of even just two simple async tasks are taking way too long time.

I identified the cause of the problem being from the dynamic dispatch of Future::poll() from a Pin<Box<dyn Future>>. I tried replacing the non-deterministic task scheduling with two hardcoded Pin<Box<impl Future>> tasks made of distinct opaque types. With that the solver gains at least 10x performance improvement, as compared to the same code that uses Pin<Box<dyn Future>>.

Does this have to do with the use of dynamic dispatch in dyn traits not working well with symbolic execution? If so, I'm not sure if we could implement general purpose async task spawners and schedulers in Kani without significant sacrifice on performance.

[tedinski]

Could you try with --restrict-vtable? (This feature was never fully finished, but it helps a lot with dynamic dispatch, sometimes.)

[fzaiser]

@tedinski I just tried this option on manual_spawn.rs, and both with and without the flag, it took between 61 and 62s. If I understand correctly, --restrict-vtable, narrows the choice of pointer targets to those of a type that implements the trait (here Future). Since all spawned futures are dyn Future, --restrict-vtable does not help CBMC to narrow down the possible future types.