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

fzaiser · 2022-09-08T20:53:34Z

Description of changes:

This adds an executor (scheduler for async futures) to the Kani library, thus supporting kani::spawn as a replacement for tokio::spawn.

It also includes kani::yield_now which is similar to tokio::yield_now.

Resolved issues:

Resolves #1504

Call-outs:

Testing:

How is this change tested? Additional regression tests.
Is this a refactor change? No.

Checklist

Each commit message has a non-empty body, explaining why the change was made
Methods or procedures are documented
Regression or unit tests are included, or existing tests cover the modified code
My PR is restricted to a single feature or bugfix

By submitting this pull request, I confirm that my contribution is made under the terms of the Apache 2.0 and MIT licenses.

celinval

More tests please! :)

library/kani/src/futures.rs

tests/kani/AsyncAwait/spawn.rs

library/kani/src/futures.rs

fzaiser · 2022-09-17T02:49:19Z

~~TODO: add check that the number of tasks is less than MAX_TASKS.~~ Done

fzaiser · 2022-10-31T16:49:56Z

With the MIR linker, this is no longer blocked! Ready for review @danielsn @celinval

fzaiser · 2022-11-01T11:42:29Z

The latest CI run failed for spawn.rs: CBMC failed with status 137. Exit code 137 means that it ran out of memory, I think.

@celinval: could this be related to the new linker? If the scheduling code is in the same file, like in manual_spawn.rs, everything finishes quickly. (#1818 seems to be related?)

celinval · 2022-11-02T20:12:28Z

Yes,

The latest CI run failed for spawn.rs: CBMC failed with status 137. Exit code 137 means that it ran out of memory, I think.

@celinval: could this be related to the new linker? If the scheduling code is in the same file, like in manual_spawn.rs, everything finishes quickly. (#1818 seems to be related?)

Yes, the main purpose of the new linker was to get rid of the undefined symbols from the standard library. Fixing this issue meant that some models got bigger and harder to process.

fzaiser · 2022-11-03T10:56:57Z

Yes, the main purpose of the new linker was to get rid of the undefined symbols from the standard library. Fixing this issue meant that some models got bigger and harder to process.

@celinval That makes sense. What I don't get is that it works fine if all the scheduling code is in the same file, see manual_spawn.rs. This file uses the same code that this PR puts into the Kani library, but puts that code directly into the file with the harness. That seems to verify much more quickly, which does not make sense to me. Do you know why?

celinval · 2022-11-03T18:20:56Z

Yes, the main purpose of the new linker was to get rid of the undefined symbols from the standard library. Fixing this issue meant that some models got bigger and harder to process.

@celinval That makes sense. What I don't get is that it works fine if all the scheduling code is in the same file, see manual_spawn.rs. This file uses the same code that this PR puts into the Kani library, but puts that code directly into the file with the harness. That seems to verify much more quickly, which does not make sense to me. Do you know why?

I see. Let me take a look, but it is possible that moving the file into a different crate changed how rustc optimizes the code.

celinval · 2022-11-03T18:56:09Z

I looked at the issue you mentioned, and I think the difference is due to the second harness in spawn.rs (nondeterministic_schedule). If you remove it, the time and problem size is basically the same independent on the location of the scheduling code.

The interesting thing is that the time is pretty bad even if you run --harness deterministic_schedule. That's probably because we perform reachability analysis for all harnesses at the same time, instead of doing them separately. My guess is that CBMC slicer is not smart enough to prune the closures out of the model due to a more conservative pointer analysis.

You can see a similar effect with the --legacy-linker by just moving the scheduling code to spawn.rs. If you run kani --harness deterministic_schedule --legacy-linker with and without the second harness co-located in spawn.rs, the times are drastically different. In my machine, Kani verification succeeds after 70ish seconds if you remove the second harness, but it doesn't finish under 5min if you add the second one.

fzaiser · 2022-11-04T16:21:37Z

@celinval Thanks for that investigation. I've removed the nondeterministic test for now to make CI (hopefully) pass. I've also converted a bool to an enum and improved the documentation.

fzaiser · 2022-11-04T17:27:13Z

Hm, seems like CI still runs out of memory. I'm not sure what to do about that. Any ideas?

celinval · 2022-11-04T19:35:30Z

Can you run it locally and measure the memory consumption so we have an idea on how bad the problem is?

tests/kani/AsyncAwait/spawn.rs

fzaiser · 2023-02-15T02:44:52Z

@celinval I renamed the function spawnable_block_on to block_on_with_spawn as I think this name is clearer. ("spawnable" sounds like "can be spawned" instead of "can spawn")

If you don't have any other concerns, this should be ready to be merged.

fzaiser · 2023-02-27T09:51:50Z

@danielsn @celinval friendly reminder :)

celinval · 2023-02-28T16:36:07Z

@dsn @celinval friendly reminder :)

Sorry about that. Let me take a look

celinval · 2023-03-01T00:29:14Z

Hi @fzaiser, I think this is good to go, except that I think we should add a mechanism to guard this code under a unstable flag. Let me just sketch something quick and we can merge this. Thanks!

celinval · 2023-03-08T02:09:50Z

@fzaiser I created #2281 to get some feedback. Feel free to add comments there, but it should be a very quick change (famous last words).

celinval · 2023-04-13T23:57:39Z

I created #2373 to add the unstable attribute and I'm planning to create another one to enforce the opt-in model.

Once #2373 is merged, I believe you can just tag the public APIs from this PR as unstable and we can merge these changes.

celinval · 2023-05-04T22:57:33Z

Hi @fzaiser, I just wanted to let you know that we have merged the unstable API code, so you should be good to go. Please tag all public functions in this PR as unstable.

Kani compiler used to generate one `goto-program` for all harnesses in one crate. In some cases, this actually had a negative impact on the harness verification time. This was first reported in #1659 The main changes were done in the compiler's module `compiler_interface` and the module `project` from the driver. The compiler will now gather all the harnesses beforehand and it will perform reachability + codegen steps for each harness. All files related to a harness `goto-program` will follow the naming convention bellow: ``` <BASE_NAME>_<MANGLED_NAME>.<EXTENSION> ``` This applies to symtab / goto / type_map / restriction files. The metadata file is still generated once per target crate, and its name is still the same (`<BASE_NAME>.kani-metadata.json`). On the driver side, the way we process the artifacts have changed. The driver will now read the metadata for each crate, and collect all artifacts based on the symtab goto file that is recorded in the metadata of each harness. These changes do not apply for `--function`. We still keep all artifacts based on the crate's `<BASE_NAME>` and we have a separate logic to handle that. Fixing this is captured by #2129.

fzaiser · 2023-06-23T14:29:13Z

@celinval This should be good to go :) Could you please merge this if you're happy with it?

fzaiser · 2023-06-23T15:36:55Z

I'm not sure what the perf-benchcomp failure is about. Could it be spurious? Any ideas?

zhassan-aws · 2023-06-23T18:29:43Z

I'm not sure what the perf-benchcomp failure is about. Could it be spurious? Any ideas?

Yes, this is most likely spurious due to variance in performance. The perf-benchcomp workflow is not blocking for merges.

celinval

Thanks! Can you please add a reason to the unstable attribute? It could be something "recently added" or something like "experimental API". @adpaco-aws any suggestion?

adpaco-aws · 2023-07-05T17:56:54Z

Thanks! Can you please add a reason to the unstable attribute? It could be something "recently added" or something like "experimental API". @adpaco-aws any suggestion?

I'd suggest "experimental async support/library" or something along those lines.

Also, thanks @fzaiser for persistence on this one!

fzaiser · 2023-07-10T11:06:19Z

@celinval Thanks for reviewing and making the final changes for the merge! 🎉

…unctions (#1661) Instead of having to manually wrap the code in `kani::spawnable_block_on` as in #1659, this PR allows `#[kani::proof]` to be applied to harnesses that use `spawn` as well. For this to happen, the user has to specify a scheduling strategy. Co-authored-by: Celina G. Val <celinval@amazon.com>

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

c95f710

fzaiser requested a review from a team as a code owner September 8, 2022 20:53

fzaiser changed the title ~~Add kani::spawn and an executor to the Kani library~~ BLOCKED: Add kani::spawn and an executor to the Kani library Sep 9, 2022

fzaiser added 2 commits September 9, 2022 00:17

Add test

1e626b8

Merge branch 'main' into spawn-lib

13c01b8

fzaiser mentioned this pull request Sep 9, 2022

Allow specifying the scheduling strategy in #[kani_proof] for async functions #1661

Merged

4 tasks

celinval reviewed Sep 14, 2022

View reviewed changes

fzaiser mentioned this pull request Sep 16, 2022

Replace manual spawning code in test case by kani::spawn library once it's merged #1685

Open

fzaiser added 3 commits October 31, 2022 16:11

Merge branch 'main' into spawn-lib

2006673

Address review comments

b36737b

Check bound of num_tasks

6fe4f8e

fzaiser changed the title ~~BLOCKED: Add kani::spawn and an executor to the Kani library~~ Add kani::spawn and an executor to the Kani library Oct 31, 2022

fzaiser added 3 commits November 1, 2022 11:43

Improve documentation and remove unnecessary code

0d529f6

Merge branch 'main' into spawn-lib

7fd9a5b

Fix clippy

31d8115

fzaiser mentioned this pull request Nov 1, 2022

Kani's slow tests are failing #1818

Closed

fzaiser added 3 commits November 4, 2022 16:04

Introduce enum for scheduling assumption and improve docs

c7f5a73

Disable proof harness to improve CI times

1db9f81

Merge branch 'main' into spawn-lib

f51186a

celinval reviewed Nov 4, 2022

View reviewed changes

tests/kani/AsyncAwait/spawn.rs Outdated Show resolved Hide resolved

Update doc comments and add a check

baed1d1

celinval mentioned this pull request Mar 7, 2023

Create mechanism to enable / disable APIs #2279

Open

fzaiser mentioned this pull request Mar 13, 2023

RFC: Unstable APIs #2281

Merged

4 tasks

celinval mentioned this pull request May 12, 2023

Perform reachability analysis on a per-harness basis #2439

Merged

4 tasks

fzaiser mentioned this pull request Jun 23, 2023

Tracking issue for Kani's unstable async library, feature async-lib #2559

Open

fzaiser and others added 3 commits June 23, 2023 14:16

Merge branch 'main' into spawn-lib

bc948a7

Add unstable attributes

ff3f99b

Add -Z async-lib flag

e432a1a

fzaiser added 2 commits June 25, 2023 15:20

Merge branch 'main' into spawn-lib

1b8ff44

Merge branch 'main' into spawn-lib

407c435

celinval approved these changes Jul 5, 2023

View reviewed changes

celinval added 2 commits July 6, 2023 10:23

Add reason to unstable APIs

00c64d5

Merge branch 'main' into spawn-lib

fd477f8

celinval enabled auto-merge (squash) July 6, 2023 17:24

celinval merged commit 2be57b4 into model-checking:main Jul 6, 2023

adpaco-aws mentioned this pull request Aug 11, 2023

Add async-lib unstable flag to slow tokio test #2675

Merged

4 tasks

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

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

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

fzaiser commented Sep 8, 2022 •

edited

Loading

celinval left a comment

fzaiser commented Sep 17, 2022 •

edited

Loading

fzaiser commented Oct 31, 2022

fzaiser commented Nov 1, 2022 •

edited

Loading

celinval commented Nov 2, 2022

fzaiser commented Nov 3, 2022

celinval commented Nov 3, 2022

celinval commented Nov 3, 2022

fzaiser commented Nov 4, 2022

fzaiser commented Nov 4, 2022

celinval commented Nov 4, 2022

fzaiser commented Feb 15, 2023 •

edited

Loading

fzaiser commented Feb 27, 2023 •

edited

Loading

celinval commented Feb 28, 2023

celinval commented Mar 1, 2023

celinval commented Mar 8, 2023

celinval commented Apr 13, 2023

celinval commented May 4, 2023 •

edited

Loading

fzaiser commented Jun 23, 2023

fzaiser commented Jun 23, 2023

zhassan-aws commented Jun 23, 2023

celinval left a comment

adpaco-aws commented Jul 5, 2023

fzaiser commented Jul 10, 2023

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

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

Conversation

fzaiser commented Sep 8, 2022 • edited Loading

Description of changes:

Resolved issues:

Call-outs:

Testing:

Checklist

celinval left a comment

Choose a reason for hiding this comment

fzaiser commented Sep 17, 2022 • edited Loading

fzaiser commented Oct 31, 2022

fzaiser commented Nov 1, 2022 • edited Loading

celinval commented Nov 2, 2022

fzaiser commented Nov 3, 2022

celinval commented Nov 3, 2022

celinval commented Nov 3, 2022

fzaiser commented Nov 4, 2022

fzaiser commented Nov 4, 2022

celinval commented Nov 4, 2022

fzaiser commented Feb 15, 2023 • edited Loading

fzaiser commented Feb 27, 2023 • edited Loading

celinval commented Feb 28, 2023

celinval commented Mar 1, 2023

celinval commented Mar 8, 2023

celinval commented Apr 13, 2023

celinval commented May 4, 2023 • edited Loading

fzaiser commented Jun 23, 2023

fzaiser commented Jun 23, 2023

zhassan-aws commented Jun 23, 2023

celinval left a comment

Choose a reason for hiding this comment

adpaco-aws commented Jul 5, 2023

fzaiser commented Jul 10, 2023

fzaiser commented Sep 8, 2022 •

edited

Loading

fzaiser commented Sep 17, 2022 •

edited

Loading

fzaiser commented Nov 1, 2022 •

edited

Loading

fzaiser commented Feb 15, 2023 •

edited

Loading

fzaiser commented Feb 27, 2023 •

edited

Loading

celinval commented May 4, 2023 •

edited

Loading