Performance issues with colibri2 installed

[filipeom]

Some performance issues noticed when colibri2 is installed. Probably due to additional start up costs?

STAT:                                                                                                                                                                                          
provers      │z3              │smtml-z3        │smtml-bitwuzla                                                                                                                                 
─────────────┼─────────┬──────┼─────────┬──────┼─────────┬──────                                                                                                                               
             │number   │2820  │number   │2820  │number   │2820                                                                                                                                 
             ├─────────┼──────┼─────────┼──────┼─────────┼──────                                                                                                                               
             │total    │51.8s │total    │54.9s │total    │29.5s                                                                                                                                
sat          ├─────────┼──────┼─────────┼──────┼─────────┼──────                                                                                                                               
             │mean     │0.020s│mean     │0.020s│mean     │0.011s                                                                                                                               
             ├─────────┼──────┼─────────┼──────┼─────────┼──────                                                                                                                               
             │deviation│0.003s│deviation│0.002s│deviation│0.001s                                                                                                                               
─────────────┼─────────┼──────┼─────────┼──────┼─────────┼──────                                                                                                                               
             │number   │1728  │number   │1728  │number   │1728                                                                                                                                 
             ├─────────┼──────┼─────────┼──────┼─────────┼──────
             │total    │26.5s │total    │33s   │total    │17.5s
unsat        ├─────────┼──────┼─────────┼──────┼─────────┼──────
             │mean     │0.015s│mean     │0.019s│mean     │0.010s
             ├─────────┼──────┼─────────┼──────┼─────────┼──────
             │deviation│0.001s│deviation│0.001s│deviation│0.000s
─────────────┼─────────┴──────┼─────────┴──────┼─────────┴──────
sat+unsat    │4548            │4548            │4548
─────────────┼────────────────┼────────────────┼────────────────
errors       │0               │0               │0
─────────────┼────────────────┼────────────────┼────────────────
valid_proof  │0               │0               │0
─────────────┼────────────────┼────────────────┼────────────────
invalid_proof│0               │0               │0
─────────────┼────────────────┼────────────────┼────────────────
unknown      │0               │0               │0
─────────────┼────────────────┼────────────────┼────────────────
timeout      │0               │0               │0
─────────────┼────────────────┼────────────────┼────────────────
memory       │0               │0               │0
─────────────┼────────────────┼────────────────┼────────────────
total        │4548            │4548            │4548
─────────────┼────────────────┼────────────────┼────────────────
total_time   │1m18.3s         │1m27.0s         │47s

With colibri2 installed:

STAT:                                                                                                                                                                                          
provers      │z3              │smtml-z3         │smtml-colibri2  │smtml-bitwuzla                                                                                                               
─────────────┼─────────┬──────┼─────────┬───────┼─────────┬──────┼─────────┬──────                                                                                                             
             │number   │2820  │number   │2820   │number   │2290  │number   │2820                                                                                                               
             ├─────────┼──────┼─────────┼───────┼─────────┼──────┼─────────┼──────                                                                                                             
             │total    │52.2s │total    │1m13.6s│total    │39.9s │total    │47.9s                                                                                                              
sat          ├─────────┼──────┼─────────┼───────┼─────────┼──────┼─────────┼──────                                                                                                             
             │mean     │0.019s│mean     │0.026s │mean     │0.017s│mean     │0.017s                                                                                                             
             ├─────────┼──────┼─────────┼───────┼─────────┼──────┼─────────┼──────                                                                                                             
             │deviation│0.001s│deviation│0.000s │deviation│0.002s│deviation│0.000s                                                                                                             
─────────────┼─────────┼──────┼─────────┼───────┼─────────┼──────┼─────────┼──────                                                                                                             
             │number   │1728  │number   │1728   │number   │1116  │number   │1728                                                                                                               
             ├─────────┼──────┼─────────┼───────┼─────────┼──────┼─────────┼──────                                                                                                             
             │total    │26.8s │total    │44.5s  │total    │17.7s │total    │28.7s                                                                                                              
unsat        ├─────────┼──────┼─────────┼───────┼─────────┼──────┼─────────┼──────                                                                                                             
             │mean     │0.015s│mean     │0.026s │mean     │0.016s│mean     │0.017s                                                                                                             
             ├─────────┼──────┼─────────┼───────┼─────────┼──────┼─────────┼──────                                                                                                             
             │deviation│0.001s│deviation│0.001s │deviation│0.000s│deviation│0.000s                                                                                                             
─────────────┼─────────┴──────┼─────────┴───────┼─────────┴──────┼─────────┴──────
sat+unsat    │4548            │4548             │3406            │4548
─────────────┼────────────────┼─────────────────┼────────────────┼────────────────
errors       │0               │0                │686             │0
─────────────┼────────────────┼─────────────────┼────────────────┼────────────────
valid_proof  │0               │0                │0               │0
─────────────┼────────────────┼─────────────────┼────────────────┼────────────────
invalid_proof│0               │0                │0               │0
─────────────┼────────────────┼─────────────────┼─────────┬──────┼────────────────
             │                │                 │number   │456   │
             │                │                 ├─────────┼──────┤
             │                │                 │total    │15s   │
unknown      │0               │0                ├─────────┼──────┤0
             │                │                 │mean     │0.035s│
             │                │                 ├─────────┼──────┤
             │                │                 │deviation│0.008s│
─────────────┼────────────────┼─────────────────┼─────────┴──────┼────────────────
timeout      │0               │0                │0               │0
─────────────┼────────────────┼─────────────────┼────────────────┼────────────────
memory       │0               │0                │0               │0
─────────────┼────────────────┼─────────────────┼────────────────┼────────────────
total        │4548            │4548             │4548            │4548
─────────────┼────────────────┼─────────────────┼────────────────┼────────────────
total_time   │1m19s           │1m58.2s          │57.6s           │1m16.6s

[hra687261]

I can look into it, how do I reproduce this?

[filipeom]

I can look into it, how do I reproduce this?

Great! There's been a couple changes. So I'll try to be as thorough as possible when describing how to reproduce this.

1. Setup benchmarking environment

• Checkout datasets:

  $ git submodule update --init

• Install missing dependencies:

  $ opam install . --deps-only --with-test

• Ensure only Z3 is installed

  $ opam remove cvc5 colibri2 bitwuzla-cxx # remove other solvers, if necessary
  $ opam install z3 # install z3, if necessary

• Build and install smtml:

  $ dune build && dune install

2. Reproducing the first results

• With only z3 installed run benchpress using:

  $ cd bench
  $ benchpress run -c benchpress.sexp data/collections-c -p z3 -p smtml-z3

3. Reproducing the second results

• Install colibri2 and run benchpress using the following commands:

  $ cd .. 
  $ opam install colibri2
  $ dune build && dune install
  $ cd bench
  $ benchpress run -c benchpress.sexp data/collections-c -p z3 -p smtml-z3 -p smtml-colibri2

4. Verifying the performance hit (optional)

• This last step is optional but just to:

  $ cd .. 
  $ opam remove colibri2
  $ dune build && dune install

• Then, repeat steps 2. and 3. to verify the slowdown

Summary

I think the slowdown is probably due to us creating some terms at the top level of the module, which is going to have a startup cost and will end up accumulating across multiple benchmarks.

It would be good if we could somehow reduce this, but we can probably account for the startup cost by running an empty benchmark and then adjusting the runtimes by subtracting the startup time.

[hra687261]

Thanks for the detailed response!
After looking into it, it turns out that there are errors (some from Colibri2 mapping, some from Colibri2)
#214 fixes some of them, 12 are left, but I'll need to update Colibri2 to fix them, I'll do it in a separate PR

[filipeom]

Thanks for #216. Do you also have any insights why the time for smtml-z3 jumped from 1m27.0 to 1m58.2s and likewise the time for smtml-bitwuzla went from 47s to 57.6s when I installed colibri2?

[hra687261]

I am not sure tbh. but there is some weird behavior that I am seeing.
When installing smtml with colibri2 and running tests, it seems that record_backtrace is the to true (it can be seen when testing with idontexist.smt2), but it isn't by default in Colibri2, so I don't know why installing it sets it to true. It seems that combining z3 and colibri2, for some reason sets the backtrace recording.
Edit: I'll try to find what takes up the additional time.

(Also there are still unknown in the bench marks, but that's just colibri2 lacking in reasoning power, will see if I can easily do something about it)

[hra687261]

I'm not sure what happens when both z3 and colibri2 are installed together, but that's when the performance issue occurs, it also seems to occur with smtml-z3 and not z3. It could have something to do with their dependencies? The following results illustrate that:

When z3, colibri2 and bitwuzla are installed:

STAT:
provers      │z3     │smtml-z3│smtml-colibri2│smtml-bitwuzla
─────────────┼───────┼────────┼──────────────┼──────────────
sat          │2820   │2820    │2774          │2820
─────────────┼───────┼────────┼──────────────┼──────────────
unsat        │1728   │1728    │1216          │1728
─────────────┼───────┼────────┼──────────────┼──────────────
sat+unsat    │4548   │4548    │3990          │4548
─────────────┼───────┼────────┼──────────────┼──────────────
errors       │0      │0       │0             │0
─────────────┼───────┼────────┼──────────────┼──────────────
valid_proof  │0      │0       │0             │0
─────────────┼───────┼────────┼──────────────┼──────────────
invalid_proof│0      │0       │0             │0
─────────────┼───────┼────────┼──────────────┼──────────────
unknown      │0      │0       │558           │0
─────────────┼───────┼────────┼──────────────┼──────────────
timeout      │0      │0       │0             │0
─────────────┼───────┼────────┼──────────────┼──────────────
memory       │0      │0       │0             │0
─────────────┼───────┼────────┼──────────────┼──────────────
total        │4548   │4548    │4548          │4548
─────────────┼───────┼────────┼──────────────┼──────────────
total_time   │2m38.5s│3m59.6s │2m15.1s       │2m32.1s
ANALYSIS:
provers      │z3  │smtml-z3│smtml-colibri2│smtml-bitwuzla
─────────────┼────┼────────┼──────────────┼──────────────
improved     │4548│4548    │3990          │4548
─────────────┼────┼────────┼──────────────┼──────────────
ok           │0   │0       │558           │0
─────────────┼────┼────────┼──────────────┼──────────────
disappoint   │0   │0       │0             │0
─────────────┼────┼────────┼──────────────┼──────────────
bad          │0   │0       │0             │0
─────────────┼────┼────────┼──────────────┼──────────────
valid proof  │0   │0       │0             │0
─────────────┼────┼────────┼──────────────┼──────────────
invalid proof│0   │0       │0             │0
─────────────┼────┼────────┼──────────────┼──────────────
errors       │0   │0       │0             │0
─────────────┼────┼────────┼──────────────┼──────────────
total        │4548│4548    │4548          │4548

When z3 and bitwuzla are installed:

STAT:
provers      │z3     │smtml-z3│smtml-bitwuzla
─────────────┼───────┼────────┼──────────────
sat          │2820   │2820    │2820
─────────────┼───────┼────────┼──────────────
unsat        │1728   │1728    │1728
─────────────┼───────┼────────┼──────────────
sat+unsat    │4548   │4548    │4548
─────────────┼───────┼────────┼──────────────
errors       │0      │0       │0
─────────────┼───────┼────────┼──────────────
valid_proof  │0      │0       │0
─────────────┼───────┼────────┼──────────────
invalid_proof│0      │0       │0
─────────────┼───────┼────────┼──────────────
unknown      │0      │0       │0
─────────────┼───────┼────────┼──────────────
timeout      │0      │0       │0
─────────────┼───────┼────────┼──────────────
memory       │0      │0       │0
─────────────┼───────┼────────┼──────────────
total        │4548   │4548    │4548
─────────────┼───────┼────────┼──────────────
total_time   │2m34.2s│3m9.2s  │1m39.0s
ANALYSIS:
provers      │z3  │smtml-z3│smtml-bitwuzla
─────────────┼────┼────────┼──────────────
improved     │4548│4548    │4548
─────────────┼────┼────────┼──────────────
ok           │0   │0       │0
─────────────┼────┼────────┼──────────────
disappoint   │0   │0       │0
─────────────┼────┼────────┼──────────────
bad          │0   │0       │0
─────────────┼────┼────────┼──────────────
valid proof  │0   │0       │0
─────────────┼────┼────────┼──────────────
invalid proof│0   │0       │0
─────────────┼────┼────────┼──────────────
errors       │0   │0       │0
─────────────┼────┼────────┼──────────────
total        │4548│4548    │4548

When colibri2 and bitwuzla are installed:

STAT:
provers      │smtml-colibri2│smtml-bitwuzla
─────────────┼──────────────┼──────────────
sat          │2774          │2820
─────────────┼──────────────┼──────────────
unsat        │1216          │1728
─────────────┼──────────────┼──────────────
sat+unsat    │3990          │4548
─────────────┼──────────────┼──────────────
errors       │0             │0
─────────────┼──────────────┼──────────────
valid_proof  │0             │0
─────────────┼──────────────┼──────────────
invalid_proof│0             │0
─────────────┼──────────────┼──────────────
unknown      │558           │0
─────────────┼──────────────┼──────────────
timeout      │0             │0
─────────────┼──────────────┼──────────────
memory       │0             │0
─────────────┼──────────────┼──────────────
total        │4548          │4548
─────────────┼──────────────┼──────────────
total_time   │1m20.7s       │1m34.5s
ANALYSIS:
provers      │smtml-colibri2│smtml-bitwuzla
─────────────┼──────────────┼──────────────
improved     │3990          │4548
─────────────┼──────────────┼──────────────
ok           │558           │0
─────────────┼──────────────┼──────────────
disappoint   │0             │0
─────────────┼──────────────┼──────────────
bad          │0             │0
─────────────┼──────────────┼──────────────
valid proof  │0             │0
─────────────┼──────────────┼──────────────
invalid proof│0             │0
─────────────┼──────────────┼──────────────
errors       │0             │0
─────────────┼──────────────┼──────────────
total        │4548          │4548

[filipeom]

it also seems to occur with smtml-z3 and not z3. It could have something to do with their dependencies?

Yeah, I agree it might be something related with the dependencies. But, I don't think we will have time to address this for the submission on friday so we're currently evaluating solvers in separate opam switches so that their dependencies don't interfere with each other.