Massive performance regression in 4.15.4.0 apparently due to lock contention

[emeryberger]

Performance with solver.set(threads=multiprocessing.cpu_count()) (where solver is either generic or QF_IDL) is catastrophic on 4.15.4.0 (it barely progresses), and totally fine on 4.15.3.0 and earlier (runs in seconds). Setting the number of threads to 1 "solves" the problem but this seems like a bad solution. The culprit appears to be lock contention.

Thread 14 (Thread 0x7f8f93fff640 (LWP 20201) "python3"):
#0  0x00007f9003370540 in __lll_lock_wait () from /lib64/libc.so.6
#1  0x00007f90033766d2 in pthread_mutex_lock@@GLIBC_2.2.5 () from /lib64/libc.so.6
#2  0x00007f8f9a7680ca in verbose_lock() () from /home/emerydb/venv-python-3.12/lib/python3.12/site-packages/z3/lib/libz3.so
#3  0x00007f8f9aff1f05 in smt::theory_diff_logic<smt::rdl_ext>::found_non_diff_logic_expr(expr*) () from /home/emerydb/venv-python-3.12/lib/python3.12/site-packages/z3/lib/libz3.so
#4  0x00007f8f9affebf5 in smt::theory_diff_logic<smt::rdl_ext>::internalize_atom(app*, bool) () from /home/emerydb/venv-python-3.12/lib/python3.12/site-packages/z3/lib/libz3.so
#5  0x00007f8f9aede7cd in smt::context::internalize_theory_atom(app*, bool) () from /home/emerydb/venv-python-3.12/lib/python3.12/site-packages/z3/lib/libz3.so
#6  0x00007f8f9aee91bb in smt::context::internalize_formula(expr*, bool) () from /home/emerydb/venv-python-3.12/lib/python3.12/site-packages/z3/lib/libz3.so
#7  0x00007f8f9aee884a in smt::context::internalize_formula_core(app*, bool) () from /home/emerydb/venv-python-3.12/lib/python3.12/site-packages/z3/lib/libz3.so
#8  0x00007f8f9aee884a in smt::context::internalize_formula_core(app*, bool) () from /home/emerydb/venv-python-3.12/lib/python3.12/site-packages/z3/lib/libz3.so
#9  0x00007f8f9aec6251 in smt::context::assert_default(expr*, app*) () from /home/emerydb/venv-python-3.12/lib/python3.12/site-packages/z3/lib/libz3.so
#10 0x00007f8f9b43e58a in smt::context::internalize_assertion(expr*, app*, unsigned int) [clone .constprop.1] () from /home/emerydb/venv-python-3.12/lib/python3.12/site-packages/z3/lib/libz3.so
#11 0x00007f8f9b454d7c in smt::context::internalize_assertions() [clone .constprop.2] () from /home/emerydb/venv-python-3.12/lib/python3.12/site-packages/z3/lib/libz3.so
#12 0x00007f8f9aec81c1 in smt::context::init_assumptions(ref_vector<expr, ast_manager> const&) () from /home/emerydb/venv-python-3.12/lib/python3.12/site-packages/z3/lib/libz3.so
#13 0x00007f8f9b455060 in smt::context::check(unsigned int, expr* const*, bool) [clone .constprop.1] () from /home/emerydb/venv-python-3.12/lib/python3.12/site-packages/z3/lib/libz3.so
#14 0x00007f8f9af031bd in std::thread::_State_impl<std::thread::_Invoker<std::tuple<smt::parallel::operator()(ref_vector<expr, ast_manager> const&)::{lambda()#1}> > >::_M_run() () from /home/emerydb/venv-python-3.12/lib/python3.12/site-packages/z3/lib/libz3.so
#15 0x00007f8f9b532f40 in execute_native_thread_routine () from /home/emerydb/venv-python-3.12/lib/python3.12/site-packages/z3/lib/libz3.so
#16 0x00007f90033732ea in start_thread () from /lib64/libc.so.6
#17 0x00007f90033f8500 in clone3 () from /lib64/libc.so.6

[NikolajBjorner]

FYI - @ilanashapiro

[ilanashapiro]

Hi @emeryberger, would it be possible to share the example you ran this on where you experienced the deadlock? I will try to repro it on my system. thank you so much!

[emeryberger]

Unfortunately I cannot share it. (It is on the road to being open sourced but not yet there.) it isn’t a deadlock, though, AFAICT - just catastrophic contention.

[ilanashapiro]

@emeryberger Thanks for bringing this up -- I am trying to see if I can benchmark this and isolate the issue, it may be due to fairly massive clause sharing amongst threads for certain problems. I will update when I have more details