verify/pass/arrays/{merge,selection_sort}.rs timeout issue
#819
Comments
|
I also observed
|
|
The same for |
|
Where is the timeout set? |
|
I have a running theory of what might be happening: I think the Take for example the post-condition on line 65: prusti-dev/prusti-tests/tests/verify/pass/arrays/selection_sort.rs Lines 60 to 75 in f7f3e1b If I run the test in debug mode with the This is already somewhat tricky, because we don't know for sure (without profiling it first) whether Viper will infer the triggers for both: If I manually add both triggers in the dumped Viper file, it verifies fast in Viper IDE in about 13 seconds on a cold start. If I only add the latter trigger then Viper IDE takes much longer to verify (it timed out after 300 seconds). So at least empirically it looks like Viper correctly infers both triggers in this case (profiling will have to tell us for sure). It gets a lot worse when we enable the 2 optimizations again, now the Viper verification of method Which triggers could Viper possibly choose here out of the possibilities: Would the choice matter a lot for performance? Would this also matter in Viper (I didn't do any profiling yet, I was just trying to eyeball it and then noticed the performance difference when disabling those optimizations). |
|
It seems to me that the transformation from the first to the second quantifier that you reported is doing a lot of unnecessary stuff. I don't see why we would need to move those old expressions out of the quantifier. If I recall correctly those passes are a workaround for an incompleteness of Viper when the old expression is used to identify some If triggers are the cause, I think the proper fix for that example would be to add the triggers
It's always hard to answer this. I opened viperproject/silicon#586.
The first two should be equivalent because the verifier should know
Yes, because |
Just a heads-up: these passes should be gone once I finish my refactorings.
From our Viper experience, we concluded that the user should always write the triggers because inferring the correct ones is impossible. So, if it is clear what triggers to write, we should just add them to the example. |
|
In that case I think the best way forward to fix this performance issue is to add triggers to the test case once #812 is resolved and @vakaras' refactorings land. I think that should solve it and then we won't need to do the profiling. In another comment I alluded to an idea about detecting potential matching loops automatically. I will post a more detailed description later, but at a very high level I'm thinking of two things:
|
I completely agree.
This would definitely improve the user experience. One more idea would be when the user omits triggers, show a warning and in the warning's note tell what triggers were inferred so that the user has some starting point. |
Aurel300
changed the title
prusti-tests/tests/verify/pass/arrays/selection_sort.rs timeout issueverify/pass/arrays/{merge,selection_sort}.rs timeout issue
848: partial fix for #819 r=vakaras a=Pointerbender In issue #819 the `prusti-tests/tests/verify/pass/arrays/selection_sort.rs` test was entirely disabled in anticipation of some future fixes. Those future fixes have not landed yet, but PRs #831 and #844 opened a window for a temporary work-around. I was curious if I could get it to work and was able to achieve a stable test run for `selection_sort` (consistently finishes in under 60 seconds on my PC). The changes I made were to selectively disable the `fix_quantifiers` and `optimize_folding` optimization passes and use wrapper functions for array accesses instead of using array indices directly (those are blocked by #812 for now). I don't consider this a proper fix for #819, but I think it could still be a nice regression test and now that its execution time has stabilized I think it's safe to turn back on. Let's keep #819 open to track implementing a proper fix in the future. Co-authored-by: Pointerbender <[email protected]>
858: add support for array/slice accesses in quantifier triggers r=fpoli a=Pointerbender This PR adds support for using slice/array access in quantifier triggers (issue #812). These are encoded including bound checks, but the bound checks are not needed (nor allowed) inside the triggers. The fix/hack applied here removes those bound checks from the triggers. This seems to fix the encoding problem, but it doesn't appear to be a full solution for `prusti-tests/tests/verify/pass/arrays/selection_sort.rs` (see #819). If I replace all the triggers there with direct array accesses (but not the lookup and the assignment statements in the loop body wrapped in `get`/`set`), then the verification time for this test jumps from 1 minute to 4 minutes on my PC. If I also replace the lookup and assign statements in the loop bodies with direct array accesses, then the verification times out. I suspect this is a matter of adding a few dummy assert statements here and there, but as long as #796 hasn't landed yet this does not seem to improve the situation (it still times out, even with dummy assertions atm). I tried adding `body_invariant`s instead of assert statements, but this also still results in timeouts. For these reasons, I decided not to include the updated version of `selection_sort.rs`. Using a custom pure lookup function such as `get` still yields superior performance over interactions with `lookup_pure` array/slice accesses, even with the fix from this PR, unfortunately :) The test `prusti-tests/tests/verify/pass/issues/issue-812-4.rs` is currently ignored because it triggers a `todo!()` in the new vir high encoder here: https://github.com/viperproject/prusti-dev/blob/66c90d5dae9040eb68b2f0d2689faa480b10e8d6/prusti-viper/src/encoder/mir/pure/specifications/encoder_high.rs#L26-L35 I included the test anyway so that it can be enabled later when that part is implemented during the refactoring. I'd like to investigate deeper what is the best way to trigger the quantifiers (which are snap encoded) from a Viper method body (where Rust statements are not snap encoded, unless routed through a pure Rust function), but I thought I'd first do a check-in first to see if the proposed fix is heading in the right direction and inquire about if there are any other alternatives than #796 or custom pure lookup functions to work-around the performance issues that seem to be caused by the mixed snap/non-snap encoding :) Thanks! Co-authored-by: Pointerbender <[email protected]> Co-authored-by: Federico Poli <[email protected]>
876: use array indices as quantifier triggers for `selection_sort` test r=vakaras a=Pointerbender Now that there is support for array/slice indices in quantifier triggers (#812), I updated the `selection_sort.rs` test case to make use of this. This results in a ~15 second faster verification time 🎉 increasing performance further per #819. Prusti can't verify this test yet when using array assignments instead of `set()`, so there are still 2 calls to `set()` in the test with a FIXME to address these later. Will post a separate comment with some ideas about what that would take. Co-authored-by: Pointerbender <[email protected]>
|
With PR #876 the while i < a.len() {
// ... snipped code and loop body invariants from `selection_sort.rs`
let a_i = a[i];
let a_min = a[min];
a[i] = a_min;
a[min] = a_i;
}But this does work currently: while i < a.len() {
// ... snipped code and loop body invariants from `selection_sort.rs`
let a_i = a[i];
let a_min = a[min];
set(a, i, a_min);
set(a, min, a_i);
}
#[requires(0 <= i && i < 10)]
#[ensures(forall(|j: usize| (0 <= j && j < 10 && j != old(i)) ==> (a[j] == old(a[j])), triggers=[(a[j],)]))]
#[ensures(a[old(i)] == old(v))]
fn set(a: &mut [i32; 10], i: usize, v: i32) {
a[i] = v;
}I suspect that this is because in the first example the array assignments (= these do not use snap encoding) are not triggering the quantifiers from the loop body invariants (= these use snap encoding). In the second example the correct triggering assertions are contained in the post-conditions of At the Viper level, this could probably be fixed by adding a call to The function I was pondering on what it would take to be able to write the first example and have Prusti verify it okay. Some possibilities are:
Would there be any merit to already start investigating one of these options before the refactoring lands? Are there any other interesting options that are not listed above? I would be interested in taking on exploring this further :) Thanks! |
|
Thank you for investigating this! I suspect that the second option would be quite easy to implement and hopefully does not introduce too serious performance problems. So, I personally would vote for it. |
…iperproject#877. remove auxiliary helper function for `selection_sort.rs` viperproject#819. added regression test for viperproject#877.
888: use `old` in trigger for direct array assignments r=vakaras a=Pointerbender This PR experiments with addressing 2 things: 1. It implements the suggested work-around for #877 together with a regression test (the test suite indicated no regressions locally). 2. The `selection_sort.rs` test case was updated to use this fix in order to remove the auxiliary `set` function (#819). Some notes apply to the approach chosen to make `selection_sort.rs` verify: * A "dummy" `body_invariant!(a[0] <= a[i]);` was added to the outer and inner loops in order to correctly trigger the quantifiers. * A change was made in `prusti-viper/src/encoder/foldunfold/mod.rs` to prevent Prusti from running into an encoder error when the `old` expresion was only present in the trigger, but not in the quantifier body. Without this change, `selection_sort.rs` will complain about a fold-unfold error. Since access predicates are not needed when the `old` expression is only present in the trigger, this should be sound (but please do double check this during the peer review). * Without the auxiliary `set` function, the verification time roughly doubled, but it is still well within the `-Pverification_deadline=180` compiler parameter. Execution time now hovers around ~2 minutes on my PC. If the chosen approach sounds good, then this PR can be merged. I'm still a bit suspicious about why the `set` function yields better performance, I could look into this deeper with some guidance (possibly in a separate PR if that makes more sense). For now I came up empty-handed for what could be causing this performance regression (if this happens to be related to how Viper gives hints to Z3 based on the Viper/Silver syntax, then my current experience may not be of much help, but am willing to learn more!). Thanks! p.s. Issue #877 can be left open for now in case we want to file a bug report with the Viper back-end developers to investigate the `old` trigger issue. I posted a ~30 lines example there that hopefully is small enough to investigate. Co-authored-by: Pointerbender <[email protected]>
On commit 7e259b8 from PR #817 the test case
prusti-tests/tests/verify/pass/arrays/selection_sort.rsis reliably failing due to a timeout error during the CI run on Ubuntu. This timeout issue is not reproducible on the Windows or Mac CI runs, nor on my local Ubuntu machine, where the test case is verifying okay. @vakaras pointed out that such a performance issue could very well be due to matching loop.There are a couple of things we could try to investigate this, per the instructions from @fpoli:
After tracking down and fixing the performance issue, we should re-enable the
prusti-tests/tests/verify/pass/arrays/selection_sort.rstest case, as it was ignored for now until this is resolved.The text was updated successfully, but these errors were encountered: