search

epfl-lara / ScalaZ3

DSL in Scala for Constraint Solving with Z3 SMT Solver
Apache License 2.0
122 stars 34 forks source link

GC cannot collect unused AST nodes/Z3Object instances #44

Open mtappler opened 9 years ago

mtappler commented 9 years ago

Hello,

as far as I can tell, the garbage collector can only collect AST nodes, when the corresponding Context is deleted. This seams to be true for other Z3Object subclasses as well, but I am mentioning AST nodes explicitly, because this is the greatest issue for me.

The reason is that Z3Object instances get added to a Z3RefCountQueue object once they are created and this queue is not cleared until the context, which created the objects, is deleted. Hence, there is always a reference to an object, which might not be needed at all.

This became an issue while I was using Scala^Z3 for symbolic execution. During such executions I build lots of formulas for unsatisfiable paths, which are not needed in subsequent steps. Since this led to severe problems regarding memory consumption, I had to switch to the Java-API, which is included in the master branch of Z3 at Codeplex (https://z3.codeplex.com/SourceControl/latest).

This API circumvents this problem by not keeping references from the context to the objects it created and overwrites Object.finalize() to get the reference counting in the C-API work correctly. So, the garbage collector can collect all formulas for unsatisfiable paths and the reference count of objects gets decremented correctly by the finalizer.

I think this should also work for this API.

colder commented 9 years ago

We tried at some point to use finalize but it turned up to be highly unreliable for our needs. We (tried to) follow instead of C# api which uses a free-buffer that should periodically be checked and cleared. We relied more on a lot of small solvers that we end up freeing manually, so this might explain why the current way has worked out better than relying on finalize for us.

I will have a look at the alternative again.

mtappler commented 9 years ago

I see. What exactly do you mean, when you say that finalize turned out to be unreliable? In my application, memory consumption rises from symbolic execution to symbolic execution, although it should not. More precisely, native heap size increases continuously.

Maybe this behaviour is also caused by unreliable finalize behaviour, which does not correctly decrement reference counters.