doc: Add guide chapter on async/await#2322
Conversation
parno
left a comment
parno
left a comment
There was a problem hiding this comment.
Thanks for putting this together. I added a variety of mostly minor comments.
I think @Chris-Hawblitzel suggested we hold off on merging this, however, until we're able to try async on some larger examples and work out some of the completeness issues that emerge.
| @@ -0,0 +1,110 @@ | |||
| # Verifying asynchronous code | |||
|
|
|||
| Rust supports writing asynchronous code without manually managing which thread a | |||
There was a problem hiding this comment.
I might rephrase as:
To support writing asynchronous code without manually assigning each task to a specific thread, Rust provides the
asyncandawaitkeywords.
| {{#include ../../../../examples/guide/async_await.rs:basic_async_ensures}} | ||
| ``` | ||
|
|
||
| `result` in the `ensure`s clause refers to the value of the future, |
There was a problem hiding this comment.
I think we want ensures rather than ensures
| assert(result == 42); | ||
| let future = add1(41); | ||
| // ^ This future has not yet executed, so the following | ||
| // assertion would fail; the value of a future can be obtained |
There was a problem hiding this comment.
The first line of the comment says that the assertion will fail, but then it also says that you can use @ to obtain the value, so it sounds a bit contradictory. Maybe it would be clearer to say something like "once the future has executed, the value it computed can be obtained..."?
| // ANCHOR: async_mut | ||
| async fn mutating_arg(x: &mut usize) -> (result: ()) | ||
| requires *old(x) < usize::MAX, | ||
| ensures *x == *old(x) + 1 |
There was a problem hiding this comment.
We'll need to wrap this in final(x) before it goes live.
|
|
||
| *Note*: Technically, Rust guarantees that after creating, but not `await`ing, | ||
| `f`, `*x` will still have value `42`. However, to avoid complex tracking of when | ||
| a future may have started executing, Verus treats this imprecisely and considers |
There was a problem hiding this comment.
Perhaps:
Verus treats this conservatively and considers...
| ``` | ||
|
|
||
| This code runs both futures `add1(42)` and `add1(21)` concurrently and returns | ||
| the value of whichever completes first; the syntax `expr = var => ret` binds |
There was a problem hiding this comment.
I think we want:
the syntax
expr = var => retbinds the final value ofexprto the namevarand then executes expressionret.
|
|
||
| While `verus` does not natively understand how to reason about the code | ||
| generated by the `select!` macro, we can use mechanisms for specifying | ||
| assumptions on external code, such as `#[verifier::external_body]` for |
There was a problem hiding this comment.
Can we update this to:
[#[verifier::external_body](./calling-unverified-from-verified.md)
so the reader can find more info about that attribute?
| - [Memory safety is conditional on verification](./memory-safety.md) | ||
| - [Calling verified code from unverified code](./call-from-unverified-code.md) | ||
|
|
||
| - [Verifying asynchronous code](./async-await.md) |
There was a problem hiding this comment.
Maybe we could list this earlier, perhaps before "Unsafe code & complex ownership"? That portion seems to focus more on specific Rust features.
2 participants
By submitting this pull request, I confirm that my contribution is made under the terms of the MIT license.