Performance issue when calling Native.delContext()

[hernanponcedeleon]

We noticed performance issues when calling Native.delContext() (it can take up to 4 min for big formulae). This was experienced when switching from Z3 Java API to JavaSMT in our Java application.

Using Z3 Java API, closing the context was immediate, we only experienced this through JavaSMT. This looked strange since JavaSMT directly calls Native.delContext(context).

The reason is related to the use of phantom references mentioned here #648; Z3's own Java API seems to it use by default, but JavaSTM does not. When configured to use phantom references, JavaSMT calls decRef() for all created formula instances before calling delContext(). It seems that this manual calling of decRef() and the associated cleanup is more efficient than the cleanup that Z3 does in delContext() if the formula instances still exist.

There is a (probable better) explanation by @PhilippWendler in sosy-lab/java-smt#236.

While this is not a problem when using Z3 throw the Java API, it might cause issues in languages without GC.

[NikolajBjorner]

file against JavaSMT

[hernanponcedeleon]

Sorry if the description was not clear, but the issue is actually with Native.delContext(context) (I just noticed when using JavaSMT).

While the issue does not happen when using directly Z3's Java API (because as I mentioned it already uses phantom references) I believe others Z3's APIs may suffer this performance problem if the clean up is only done when calling delContext().

[NikolajBjorner]

If your application maintains lots of references to expressions built using the old context you can't delete the context until these are released. I can't fix bugs in other code bases.

[PhilippWendler]

Maybe I can clear this up. Of course, nobody is asking about other code bases here.

What we found out is that Native.delContext() (which just calls Z3_del_context) takes a lot of time if references have not been cleaned up before with decRef(). Iterating over all references, calling decRef(), and afterwards calling delContext() is much faster than calling delContext() alone. (In one example, doing all of the former was instantaneous whereas the latter took 20s.)

This was surprising to us and unintuitive. It would be obvious if delContext() took a little bit more time if there are still some references to clean them up, but it should not take much longer than cleaning up everything manually. Is this really the desired behavior of Z3?

Or does your last comment mean that it is actually not allowed to call delete the context if there are still some references? In this case, it would be great if

• this requirement would be documented in the API docs for Z3_del_context
• delContext() / Z3_del_context would fail instead of just take more time if it were violated.

But more convenient would be if Z3_del_context could just clean up everything as fast as if it were done manually.

[wintersteiger]

The functions in Native.java are just forwards to the C API, so the same constraints apply when using them. There may be Java/JNI bottleneck somewhere, but I wouldn't know where to start looking. There may also be a concurrency issue, i.e. taking and releasing a lock on the context for every Z3_dec_ref could be expensive.