Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Memory blows up on a simple two-dimensional vector example #1226

Closed
Tracked by #1676
zhassan-aws opened this issue May 25, 2022 · 8 comments · Fixed by #1941
Closed
Tracked by #1676

Memory blows up on a simple two-dimensional vector example #1226

zhassan-aws opened this issue May 25, 2022 · 8 comments · Fixed by #1941
Labels
[C] Bug This is a bug. Something isn't working. [E] Performance Track performance improvement (Time / Memory / CPU) T-CBMC Issue related to an existing CBMC issue

Comments

@zhassan-aws
Copy link
Contributor

I tried this code:

#[cfg_attr(kani, kani::proof, kani::unwind(3))]
fn main() {
    let mut v1: Vec<Vec<i32>> = Vec::new();
    v1.push(vec![1, 2]);
    v1.push(vec![3]);

    let v2: Vec<i32> = v1.into_iter().flatten().collect();
    assert_eq!(v2, vec![1, 2, 3]);
}

using the following command line invocation:

kani 2d.rs

with Kani version:

I expected to see this happen: Verification successful

Instead, this happened: Memory usage went up to ~25 GB in about 90 seconds.

@zhassan-aws zhassan-aws added [C] Bug This is a bug. Something isn't working. [E] Performance Track performance improvement (Time / Memory / CPU) labels May 25, 2022
@zhassan-aws
Copy link
Contributor Author

zhassan-aws commented May 25, 2022

An immutable version of the above program doesn't run out of memory, but it doesn't terminate in 1 hour with an unwind value of 6:

#[cfg_attr(kani, kani::proof, kani::unwind(6))]
fn main() {
    let v1: Vec<Vec<i32>> = vec![vec![1, 2], vec![3]];

    let v2: Vec<i32> = v1.into_iter().flatten().collect();
    assert_eq!(v2, vec![1, 2, 3]);
}

If I reduce the unwind value to 5, it finishes in ~25 minutes and uses 7 GB of memory, but an unwinding assertion fails.

EDIT: It terminated in 65 minutes with an unwinding of 6 and used 12.6 GB of memory, but an unwinding assertion still failed.

@tedinski
Copy link
Contributor

tedinski commented May 26, 2022

The probable cause of this is that:

  1. Vec internally uses unions.
  2. That union gets partially initialized because it's not using the largest field.
  3. That means nondet remains in that memory.
  4. So the union value as a whole can't be constant-propagated (because as a whole it still contains nondet)
  5. And ultimately results allocations that cbmc has to treat as being of symbolic size

edited to clarify things a bit

Possible experiments:

  1. Let's try zero-initializing unions and see if that fixes the performance. But this might unsound so we can't merge this...
  2. Maybe we could hack std to zero-initialize unions?

@zhassan-aws
Copy link
Contributor Author

Documenting a couple more results:

  • The immutable version terminated in ~144 minutes with an unwind of 7, but an unwinding assertion still failed. Peak memory usage was 21 GB.
  • With an unwind of 8, it ran out of memory (>30 GB).

@zhassan-aws
Copy link
Contributor Author

For the record, a smaller version of the above program:

#[cfg_attr(kani, kani::proof, kani::unwind(5))]
fn main() {
    let v1: Vec<Vec<i32>> = vec![vec![1], vec![]];

    let v2: Vec<i32> = v1.into_iter().flatten().collect();
    assert_eq!(v2, vec![1]);
}

completes in 34 minutes with a minimum unwind of 5 and uses 6.3GB of memory.

@tautschnig
Copy link
Member

With diffblue/cbmc#7230 on top of diffblue/cbmc@70b7cf7baf735f I get "Verification Time: 74.53128s" when it takes 86.885506s using diffblue/cbmc@70b7cf7baf735f and Kani revision 057926b. These are numbers referring to #1226 (comment). It seems further investigation is necessary here.

@tautschnig
Copy link
Member

Changes to CBMC to be PR'ed, but I have now gotten this down to 2 seconds.

@zhassan-aws
Copy link
Contributor Author

Awesome! Is the PR also related to unions?

@tautschnig
Copy link
Member

My further changes are all extensions to expression simplification, but it's probably necessary to have union field-sensitivity in place as well for otherwise there might just not be anything to propagate (and then simplify).

@tedinski tedinski added the T-CBMC Issue related to an existing CBMC issue label Dec 6, 2022
zhassan-aws added a commit to zhassan-aws/kani that referenced this issue Dec 8, 2022
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
[C] Bug This is a bug. Something isn't working. [E] Performance Track performance improvement (Time / Memory / CPU) T-CBMC Issue related to an existing CBMC issue
Projects
None yet
Development

Successfully merging a pull request may close this issue.

3 participants