search

runtimeverification / haskell-backend

The symbolic execution engine powering the K Framework
BSD 3-Clause "New" or "Revised" License
204 stars 39 forks source link

Z3 zombie processes during long proofs #3959

Open jberthold opened 1 week ago

jberthold commented 1 week ago

During longer proofs, a number of z3 processes accumulate as zombie children of the kore-rpc-bosoter server.

Example:

$ ps auxw | grep kore-rpc-booster | sed -e 's/jost  *\([0-9]*\) .*$/\1/' | while read pid; do pstree $pid; done
kore-rpc-booste─┬─51*[z3]
                ├─z3───{z3}
                └─6*[{kore-rpc-booste}]
kore-rpc-booste─┬─51*[z3]
                └─6*[{kore-rpc-booste}]

A code inspection did not unearth any immediate reason for that - possibly the reasons lie within the smtlib-backends-process library.

jberthold commented 6 days ago

Experiments on branch https://github.com/runtimeverification/haskell-backend/compare/3959-z3-zombies did not provide an immediate remedy . The root cause appears to lie in lazy I/O delaying the process termination until server shut-down for some reason.

Using the SMTLib.Backends.Z3 backend produced a SEGFAULT in the llvm-integration test (branch is tagged and pushed)