Add async/await examples from tokio's test to a new "slow" test suite #1332

fzaiser · 2022-07-05T16:10:02Z

I went through the tokio's test suite and identified a couple of test cases that don't use a lot of I/O (or replace it with a mock) so that they seem like a reasonable target for Kani.

Description of changes:

No changes to how Kani works, this only adds tests that are ignored for now.

Testing:

How is this change tested? No change of functionality, just adding 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.

zhassan-aws · 2022-07-05T16:55:46Z

The tests have very few comments making it difficult to understand what they're doing. Can you add some comments, at least for the ones for which you have an idea what the purpose of the test is?

tests/cargo-kani/kani-tokio/src/io_write.rs

fzaiser · 2022-08-09T15:29:06Z

The tests compile under Kani now, but they take a very long time. I stopped the first harness (io_chain.rs) after two hours.

adpaco-aws · 2022-08-10T15:13:50Z

The tests compile under Kani now, but they take a very long time. I stopped the first harness (io_chain.rs) after two hours.

I saw you're using [kani::unwind(32)] for all harnesses. Have you tried using the minimum required for each harness?

fzaiser · 2022-08-10T15:35:08Z

I saw you're using [kani::unwind(32)] for all harnesses. Have you tried using the minimum required for each harness?

@adpaco-aws I will try this, but it's hard to know upfront what the necessary limit will be. Maybe I should try a smaller limit and successively increase it until it passes.

fzaiser · 2022-08-11T22:00:30Z

Progress report

Successful verification: 5 harnesses (basic_usage_fuse, basic_usage_once, empty_box_slice, empty_string, empty_vec)

Failed verification:

9 harnesses: too low unwinding bound (basic_usage_empty, empty_unit, issue_4435, merge_sync_streams, read_buf, read_exact, read, take, write_cursor)

4 harnesses: missing functions (empty, writ_buf_err, async_block, async_fn)

 Check 3880: _ZN3std3sys4unix4rand19hashmap_random_keys17hdd863e684c97ac1dE.1
  - Status: FAILURE
  - Description: "assertion"
  - Location: Unknown File in function _ZN3std3sys4unix4rand19hashmap_random_keys17hdd863e684c97ac1dE
 Check 4474: _ZN3std2io5error5Error4_new17ha2be3d29de30fdd1E.1
  - Status: FAILURE
  - Description: "assertion"
  - Location: Unknown File in function _ZN3std2io5error5Error4_new17ha2be3d29de30fdd1E

missing epoll: 2 harnesses (async_block, async_fn)

Check 5050: epoll_create1.1
 - Status: FAILURE
 - Description: "assertion"
 - Location: Unknown File in function epoll_create1

1 harness: unreachable code (empty)

Check 1375: std::thread::local::lazy::LazyKeyInner::<std::cell::Cell<(u64, u64)>>::get.unreachable.1
 - Status: FAILURE
 - Description: "unreachable code"
 - Location: ~/.rustup/toolchains/nightly-2022-07-19-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/library/core/src/option.rs:627:15 in function std::thread::local::lazy::LazyKeyInner::<std::cell::Cell<(u64, u64)>>::get

rest: timed out or hit Type mismatch for FnDefStruct #1499

I will increase the unwinding bound for the ones with too low a bound.

fzaiser · 2022-08-12T16:58:05Z

Progress report after raising the unwind bound for some tests

Successful verification: 13 harnesses (basic_usage_fuse, basic_usage_once, empty_box_slice, empty_string, empty_vec, basic_usage_empty, empty_unit, issue_4435, read_exact, read, take, write_cursor, empty_result)

Failed verification:

4 harnesses: missing functions (empty, writ_buf_err, async_block, async_fn)

 Check 3880: _ZN3std3sys4unix4rand19hashmap_random_keys17hdd863e684c97ac1dE.1
  - Status: FAILURE
  - Description: "assertion"
  - Location: Unknown File in function _ZN3std3sys4unix4rand19hashmap_random_keys17hdd863e684c97ac1dE
 Check 4474: _ZN3std2io5error5Error4_new17ha2be3d29de30fdd1E.1
  - Status: FAILURE
  - Description: "assertion"
  - Location: Unknown File in function _ZN3std2io5error5Error4_new17ha2be3d29de30fdd1E

missing epoll: 2 harnesses (async_block, async_fn)

Check 5050: epoll_create1.1
 - Status: FAILURE
 - Description: "assertion"
 - Location: Unknown File in function epoll_create1

~~1 harness: memcmp invalid pointer (empty_result) see Investigate failed check in memcmp #1489~~ fixed

1 harness: unreachable code (empty)

Check 1375: std::thread::local::lazy::LazyKeyInner::<std::cell::Cell<(u64, u64)>>::get.unreachable.1
 - Status: FAILURE
 - Description: "unreachable code"
 - Location: ~/.rustup/toolchains/nightly-2022-07-19-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/library/core/src/option.rs:627:15 in function std::thread::local::lazy::LazyKeyInner::<std::cell::Cell<(u64, u64)>>::get

rest: timed out or hit Type mismatch for FnDefStruct #1499

celinval

Can you publish a PR for the examples that are already working?

fzaiser · 2022-09-06T04:01:08Z

So the regresion tests pass now, but they take between 120 min (ubuntu-20.04) and 204 min (macos-11). It probably makes more sense to have those in a separate "slow" test suite.

As an alternative, we could add them as a compile-only test suite, which should be faster.

danielsn · 2022-09-06T15:29:05Z

I'd support adding a "slow" test suite, and running it nightly.

I'm not sure how many concurrent runners we get at the free tier. If its sufficient, we could also make it a "non-required" test so we would get information if it failed, but it wouldn't block work on PRs.

tests/cargo-kani/kani-tokio/src/tokio/io_chain.rs

fzaiser · 2022-09-08T17:15:55Z

I've added a new slow test suite as suggested.

fzaiser · 2022-09-08T20:07:21Z

Another idea that @adpaco-aws mentioned is to run the slow tests after merging into main. But for now, I think the most important thing is to get the tests into main at all.

danielsn

Can you have tracking issue comments for the disabled tests?

danielsn · 2022-09-08T20:45:26Z

.github/workflows/slow-tests.yml

+name: Kani's slow tests
+on:
+  schedule:
+    - cron: "30 5 * * *"


Comment explaining what this means

.github/workflows/slow-tests.yml

danielsn · 2022-09-08T20:47:56Z

tests/slow/tokio-proofs/src/tokio/io_copy.rs

+use std::pin::Pin;
+use std::task::{Context, Poll};
+
+#[cfg(disabled)]


Why disabled?

I wanted to disable them, but wanted to keep the code to allow them to be enabled later, so I added a #[cfg] attribute. Not sure what your question is.

I'll add a comment explaining why each test is disabled.

danielsn

Approved modulo comments

fzaiser · 2022-09-13T14:16:42Z

CI seems to have failed due to network issues, retrying

fzaiser · 2022-09-14T01:09:15Z

@danielsn I don't have rights to merge anymore. Can you merge it for me please?

fzaiser · 2022-09-16T02:01:26Z

Results of the slow test suite can be seen here: https://github.com/model-checking/kani/actions/workflows/slow-tests.yml

fzaiser requested a review from a team as a code owner July 5, 2022 16:10

fzaiser assigned danielsn Jul 5, 2022

fzaiser assigned fzaiser and unassigned danielsn Jul 12, 2022

fzaiser marked this pull request as draft July 22, 2022 15:23

fzaiser force-pushed the tokio-tests branch from 6051a48 to 237ee74 Compare July 22, 2022 19:49

celinval reviewed Jul 25, 2022

View reviewed changes

tests/cargo-kani/kani-tokio/src/io_write.rs Outdated Show resolved Hide resolved

fzaiser force-pushed the tokio-tests branch from 237ee74 to 22c54bd Compare August 9, 2022 15:27

fzaiser force-pushed the tokio-tests branch from 22c54bd to 721c340 Compare August 9, 2022 15:37

fzaiser mentioned this pull request Aug 10, 2022

Investigate failed check in memcmp #1489

Closed

celinval reviewed Sep 1, 2022

View reviewed changes

fzaiser added 4 commits September 5, 2022 16:40

Make tokio tests compile with Kani

05f8be2

Add expected file

0e8bb43

Lower unwind bound

3eb02a9

Raise unwind bounds for some tests

c043528

fzaiser force-pushed the tokio-tests branch from 1433738 to c043528 Compare September 5, 2022 20:40

fzaiser added 2 commits September 5, 2022 16:51

Disable tests that hit bugs or take too long

8531340

Disable failing tests

187424b

fzaiser marked this pull request as ready for review September 6, 2022 15:24

danielsn reviewed Sep 6, 2022

View reviewed changes

tests/cargo-kani/kani-tokio/src/tokio/io_chain.rs Outdated Show resolved Hide resolved

fzaiser added 2 commits September 8, 2022 12:09

Add a "slow" test suite

8d458ff

Add Github action to run slow tests every night

0a222a7

fzaiser changed the title ~~Add async/await examples from tokio test suite~~ Add async/await examples from tokio's test to a new "slow" test suite Sep 8, 2022

Merge branch 'main' into tokio-tests

ae3ea5d

Fix tests and expected

2c509e3

danielsn reviewed Sep 9, 2022

View reviewed changes

danielsn approved these changes Sep 9, 2022

View reviewed changes

fanzier and others added 2 commits September 12, 2022 23:09

Address review comments

0b948d9

Merge branch 'main' into tokio-tests

6fb3363

fanzier and others added 2 commits September 13, 2022 10:20

Rerun CI

7dd90b8

Merge branch 'main' into tokio-tests

989de54

danielsn merged commit a2ecd4b into model-checking:main Sep 14, 2022

Add async/await examples from tokio's test to a new "slow" test suite #1332

Add async/await examples from tokio's test to a new "slow" test suite #1332

Uh oh!

Conversation

fzaiser commented Jul 5, 2022 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Description of changes:

Testing:

Checklist

Uh oh!

zhassan-aws commented Jul 5, 2022

Uh oh!

Uh oh!

fzaiser commented Aug 9, 2022

Uh oh!

adpaco-aws commented Aug 10, 2022

Uh oh!

fzaiser commented Aug 10, 2022

Uh oh!

fzaiser commented Aug 11, 2022

Progress report

Uh oh!

fzaiser commented Aug 12, 2022 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Progress report after raising the unwind bound for some tests

Uh oh!

celinval left a comment

Choose a reason for hiding this comment

Uh oh!

fzaiser commented Sep 6, 2022

Uh oh!

danielsn commented Sep 6, 2022

Uh oh!

Uh oh!

fzaiser commented Sep 8, 2022

Uh oh!

fzaiser commented Sep 8, 2022

Uh oh!

danielsn left a comment

Choose a reason for hiding this comment

Uh oh!

danielsn Sep 8, 2022

Choose a reason for hiding this comment

Uh oh!

fzaiser Sep 13, 2022

Choose a reason for hiding this comment

Uh oh!

Uh oh!

danielsn Sep 8, 2022

Choose a reason for hiding this comment

Uh oh!

fzaiser Sep 9, 2022

Choose a reason for hiding this comment

Uh oh!

fzaiser Sep 9, 2022

Choose a reason for hiding this comment

Uh oh!

fzaiser Sep 13, 2022

Choose a reason for hiding this comment

Uh oh!

danielsn left a comment

Choose a reason for hiding this comment

Uh oh!

fzaiser commented Sep 13, 2022

Uh oh!

fzaiser commented Sep 14, 2022

Uh oh!

fzaiser commented Sep 16, 2022 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

6 participants

fzaiser commented Jul 5, 2022 •

edited

Loading

fzaiser commented Aug 12, 2022 •

edited

Loading

fzaiser commented Sep 16, 2022 •

edited

Loading