Skip to content

Slow (5m) verification of (incomplete) bubble sort #1243

Open
@safinaskar

Description

@safinaskar

I'm continuing to check bubble sort using Prusti. Here is my current (incomplete) attempt:

extern crate prusti_contracts;
use prusti_contracts::*;

fn sort(a: &mut [i32]) {
    if a.len() == 0 {
        return;
    }
    let mut i = 0;
    while i < a.len() - 1 {
        body_invariant!(true);
        body_invariant!(i + 1 <= a.len());
        body_invariant!(a.len() >= 1);
        body_invariant!(i > 0 ==> forall(|k: usize|k < a.len() - i ==> a[k] <= a[a.len() - i]));
        prusti_assume!(forall(|k: usize|(a.len() - i - 1 <= k && k < a.len() - 1) ==> a[k] <= a[k + 1]));
        {
            let mut j = 0;
            while j < a.len() - i - 1 {
                body_invariant!(true);
                body_invariant!(j < a.len());
                body_invariant!(forall(|k: usize|(k < j) ==> (a[k] <= a[j])));
                body_invariant!(i > 0 ==> forall(|k: usize|k < a.len() - i ==> a[k] <= a[a.len() - i]));
                body_invariant!(forall(|k: usize|(a.len() - i <= k && k < a.len() - 1) ==> a[k] <= a[k + 1]));
                if a[j] > a[j + 1] {
                    let sw = a[j];
                    a[j] = a[j + 1];
                    a[j + 1] = sw;
                }
                j += 1;
            }
        }
        prusti_assert!(i > 0 ==> forall(|k: usize|k < a.len() - i ==> a[k] <= a[a.len() - i]));
        prusti_assert!(forall(|k: usize|(a.len() - i <= k && k < a.len() - 1) ==> a[k] <= a[k + 1]));
        i += 1;
    }
}

fn main(){ }

Writing this code was very annoying. I add some assert, then run cargo prusti, then wait minute or two for result, then add another assert etc. In some moment waiting time became unacceptably big, so I switched to AWS instead of local laptop. This made waiting time nearly 2 times lesser, but the time is still big.

Also I tried to switch to arm64 AWS, but time was same as with usual amd64 AWS.

It seems that z3 is not parallel (I see this in htop). I tried to pass parallel.enable=true to z3 command line (via ad-hoc wrapper shell script), but I didn't see any changes.

Now (with the code you see above) my local time is 4m 38s and AWS time is 5m 00s. (But with previous versions of this code AWS is usually 2 times faster than local machine.) And I'm not finished yet this code.

This is simply too big, so I give up. I think Prusti in its current form is not suitable for any practical application.

  • So, is there any way to make Prusti faster? Maybe I missed something? Maybe there is some additional key to make z3 parallel?
  • I also tried to check file prusti-tests/tests/verify_overflow/pass/rosetta/Selection_sort.rs from this repo. It took 41.48s in AWS. This is lesser than 5m 00s, but this is still too big
  • When I run cargo prusti twice in row on same file, it runs nearly instantly. This is good. But any change to file, even small one, such as commenting some assert, causes full recheck. This is bad. Same is true when I use Prusti Assistant vscode extension

I think that if there is no way to make Prusti radically faster (for example, by enabling parallelism), then we should declare defeat. And instead we should use syntax, which precisely specify which assertions based on which. I. e. something like that:

// Here I stole Isabelle syntax a little
prusti_assert!(have x: a + b == c);
prusti_assert!(have y: d + e == f using x);

Yes, this will probably require full rewriting and, of course, is pain for users, but I think this is the only way to go forward assuming that we unable to solve performance problems

Metadata

Metadata

Assignees

No one assigned

    Type

    No type

    Projects

    No projects

    Milestone

    No milestone

    Relationships

    None yet

    Development

    No branches or pull requests

    Issue actions