model-checking
BLOCKED: Add kani::spawn and an executor to the Kani library
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:
Blocked on #1588: This cannot currently be merged because linking the Kani library is broken (just like the standard library).
Testing:
-
How is this change tested? Additional regression tests.
-
Is this a refactor change? No.
Checklist
- [x] Each commit message has a non-empty body, explaining why the change was made
- [x] Methods or procedures are documented
- [x] Regression or unit tests are included, or existing tests cover the modified code
- [x] 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.
With the MIR linker, this is no longer blocked! Ready for review @danielsn @celinval
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 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.
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?
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.
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.
@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.
Hm, seems like CI still runs out of memory. I'm not sure what to do about that. Any ideas?
Can you run it locally and measure the memory consumption so we have an idea on how bad the problem is?
Can you run it locally and measure the memory consumption so we have an idea on how bad the problem is?
@celinval, I just tried that with the second harness (the nondeterministic one) completely removed, so #1855 does not apply. It OOMed after 1 hour, maximum resident set size was about 15 GB. (My computer has 16 GB RAM, so it took up almost all the available memory.)
Should I open a bug about this? It makes no sense to me that it would take so much longer just because the code is in the Kani library instead of the same file. What do you think? cc @danielsn
Can you run it locally and measure the memory consumption so we have an idea on how bad the problem is?
@celinval, I just tried that with the second harness (the nondeterministic one) completely removed, so #1855 does not apply. It OOMed after 1 hour, maximum resident set size was about 15 GB. (My computer has 16 GB RAM, so it took up almost all the available memory.)
Should I open a bug about this? It makes no sense to me that it would take so much longer just because the code is in the Kani library instead of the same file. What do you think? cc @danielsn
Sure. You can open a bug.
The test is passing! Now that vectors are faster, I want to change this to use vectors instead of arrays before merging.
@danielsn @celinval This should be ready for another round of review. Note that we now use vectors instead of arrays because they have gotten fast enough. Two questions to decide before merging:
- The scheduling strategies
NondeterministicSchedulingandNondetFairSchedulingare currently untested (commented out inspawn.rsandmanual_spawn.rs) because they take too long. (I stopped them after half an hour and taking 15 GB of RAM.) Should we make them private given that they're untested? I would prefer to leave them in (and maybe hide their documentation), so users can still experiment with them if they absolutely want to. - Should we remove
manual_spawn.rs? Since the two versions now take almost no time (but see #1876), it may be redundant to have both.
Our libraries don't usually have much logic into them, so there's not much to test. In these news APIs, I think we should test the scheduler logic. We should either have proofs for them or just concrete tests. An error in the scheduler could result in a soundness issue, right?
@celinval: There is a proof harness using the scheduler (with the RoundRobin strategy) in spawn.rs. What additional tests or properties to prove do you have in mind?
The two nondeterministic scheduling strategies can only be tested in Kani proof harnesses, not in unit tests (because they use kani::any()). But even simple proof harnesses using them take a long time and lots of RAM. Altogether, this means they should not be included if you want them to be tested. Did I understand this correctly? (Another option to consider would be to include them, but hide their documentation. So users could still experiment with them, but we'd consider them "unstable".)
Can you take advantage of the concrete playback infrastructure for injecting concrete values for testing purpose?
I do worry about the scalability. If we can't write simple harnesses with the nondeterministic strategies, what value do we get from adding them to the Kani library at this point?
That's a good point. I have removed the nondeterministic scheduling strategies. No only the RoundRobin strategy is included. (And there's a test for it.)
That's a good point. I have removed the nondeterministic scheduling strategies. No only the
RoundRobinstrategy is included. (And there's a test for it.)
But wouldn't the non-deterministic schedules be required for soundness? They might be impractical right now, but perhaps there is a way to make them tractable in future?
That's a good point. I have removed the nondeterministic scheduling strategies. No only the
RoundRobinstrategy is included. (And there's a test for it.)But wouldn't the non-deterministic schedules be required for soundness? They might be impractical right now, but perhaps there is a way to make them tractable in future?
Users can still create non-deterministic schedules and I think we should still keep an implementation in our benchmarks to know when they become practical, so we know it's time to add them.
I just don't think they should be in the Kani library until then. Specially since it cannot be tested at all today.
@celinval Thanks for your patience. Please take another look when you have time.
@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.
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!
@fzaiser I created https://github.com/model-checking/kani/pull/2281 to get some feedback. Feel free to add comments there, but it should be a very quick change (famous last words).
I created https://github.com/model-checking/kani/pull/2373 to add the unstable attribute and I'm planning to create another one to enforce the opt-in model.
Once https://github.com/model-checking/kani/pull/2373 is merged, I believe you can just tag the public APIs from this PR as unstable and we can merge these changes.