Kani-Compiler slow for PROST w/ PropProof.

[YoshikiTakashima]

I tried this code:

git clone https://github.com/YoshikiTakashima/propproof.git propproof
cd propproof; git submodule update --init

using the following command line invocation:

git clone https://github.com/tokio-rs/prost.git  2037251cc50e25247972d5c1131905de3064016c
cd prost;
mkdir .cargo; echo "paths =[\"/Users/ytakashl/propproof\"]" > .cargo/config.toml
cargo kani -p prost --tests

with Kani version: faa4086e6d7be8fa2a363d6c7d7c0f46607a6429

I expected to see this happen: It should finish compiling and start verifying

Instead, this happened: Kani gets stuck building prost and does not proceed to verification. I've left it for 30m, but still stuck.

[YoshikiTakashima]

If you turn off propproof, then the compile goes through.

However, there are 10+ harnesses that can be unblocked if we can use it with propproof. Customer is already integrated in prost-types, a sub-library of prost.

[celinval]

Question, is this any different from the proptest feature branch from Kani repo?

[YoshikiTakashima]

@celinval Sorry for the late reply. There is some diff (my branch has BTreeSet optimizations I was hoping to clean up) but. I don't think that's critical to this bug. It does replicate with features/proptest

[celinval]

I had to make a few changes to the instructions... here is what I'm running.

cd /tmp
mkdir issue-2505
cd issue-2505
git clone -b features/proptest --depth 1 [email protected]:model-checking/kani.git propproof
pushd propproof
git submodule update --init
popd

git clone https://github.com/tokio-rs/prost.git
cd prost
git checkout  2037251cc50e25247972d5c1131905de3064016c
mkdir .cargo; echo "paths =[\"/tmp/issue-2505/propproof\"]" > .cargo/config.toml
cargo kani -p prost --tests

For future reference, please try to make the steps easy to reproduce in other developer machines.

[celinval]

Just some notes... The command above is trying to compile 405 harnesses. In my machine, building just the package using the main branch (commit a6e516e294a) in release mode took 16m 40s. The codegen for each harness is taking about 2-3s each.

Besides that, Kani is still running goto-cc for each harness, which is taking about 1.5s for each harness.

Here is a few things we can do to improve the time:

1. Parallelize some of the work done in the compiler. I experimented with adding a thread to write the goto files, and compilation went down to 12m 06s.
2. We could try some different heuristics to group the harness by module or by similar reachability graphs.

[celinval]

That said, can we instead follow similar approach to Bolero? For bolero, users still need to annotate the tests that they want to use as proof. I believe this is cleaner than keeping the list up-to-date inside Cargo.toml or requiring user to explicitly pass which harness to use.

Note that users would still be able to use assess to try to run all tests with Kani.

[celinval]

@YoshikiTakashima just following up here. Is this approach feasible for propproof?

[celinval]

@carolynzech I expect automatic harness generation to hit this issue. Generating code on a per-harness base might hit scalability issues depending on the number of harnesses.

[AlexanderPortland]

I tested the parallelization change introduced in #4236 on the workflow above, and it seems to improve the compile time of prost by 45%!

Note that the baseline for my testing runs was significantly faster than described above (which I would chalk up largely to other optimizations since '23 and differing hardware), but this seems like enough of an improvement that I've marked that change as resolving this issue!