search

AeneasVerif / charon

Interface with the rustc compiler for the purpose of program verification
Apache License 2.0
92 stars 15 forks source link

Unbounded memory consumption on large projects? #191

Open RaitoBezarius opened 4 months ago

RaitoBezarius commented 4 months ago
  1. Clone https://github.com/cloudflare/boringtun
  2. Run charon (tested ed5047fd07e6c6aa8e7b9f352637f91977adacbe) in the boringtun crate
  3. Observe unbounded memory consumption without any hope of finishing?

I tested this on a 256GB RAM machine (fairly beefy), it went up to 210GB of RES until I killed it, and it was stuck doing the "99%" thing at the Rust level.

On a 64GB RAM machine, it locked it up, but it seems to be adapting under memory pressure (?).

I observed this "unbounded" memory consumption on https://github.com/tvlfyi/tvix (crate: nix-compat), but it gets stopped by the fact there's Hax errors beforehand.

sonmarcho commented 4 months ago

This might be related to https://github.com/AeneasVerif/charon/issues/93

Nadrieril commented 1 day ago

Possibly fixed by https://github.com/AeneasVerif/charon/pull/421