Bugfix for concurrent garbage collection in Java API.

Relates to Z3Prover#205 and Z3Prover#245
wintersteiger · Oct 14, 2015 · 6263252 · 6263252
1 parent 2d2ec38
commit 6263252
Show file tree

Hide file tree

Showing 2 changed files with 34 additions and 19 deletions.
diff --git a/src/api/java/Context.java b/src/api/java/Context.java
@@ -18,6 +18,7 @@
 package com.microsoft.z3;
 
 import java.util.Map;
+import java.util.concurrent.atomic.AtomicInteger;
 
 import com.microsoft.z3.enumerations.Z3_ast_print_mode;
 
@@ -3761,36 +3762,50 @@ public IDecRefQueue getOptimizeDRQ()
         return m_Optimize_DRQ;
     }
 
-    protected long m_refCount = 0;
+    protected AtomicInteger m_refCount = new AtomicInteger(0);
 
     /**
      * Finalizer.
+     * @throws Throwable 
      **/
-    protected void finalize()
+    protected void finalize() throws Throwable
     {
-        dispose();
-
-        if (m_refCount == 0)
-        {
-            try
+        try {            
+            dispose();
+
+            if (m_refCount.get() == 0)
             {
-                Native.delContext(m_ctx);
-            } catch (Z3Exception e)
+                try
+                {
+                    Native.delContext(m_ctx);
+                } catch (Z3Exception e)
+                {
+                    // OK.
+                }
+                m_ctx = 0;
+                System.out.println("> disposed OK.");
+            } 
+            else if (m_refCount.get() < 0)
+                System.out.println("XXX negative ref count");
+            else
             {
-                // OK.
+                System.out.println("XXX context not disposed");
             }
-            m_ctx = 0;
-        } 
-        /*
-        else
-            CMW: re-queue the finalizer? */
+        }
+        catch (Throwable t) {
+            throw t;
+        }
+        finally {
+            super.finalize();
+        }
     }
 
     /**
      * Disposes of the context.
      **/
     public void dispose()
     {
+        System.out.println("> context disposing.");
         m_AST_DRQ.clear(this);
         m_ASTMap_DRQ.clear(this);
         m_ASTVector_DRQ.clear(this);

diff --git a/src/api/java/Z3Object.java b/src/api/java/Z3Object.java
@@ -43,8 +43,8 @@ public void dispose()
         }
 
         if (m_ctx != null)
-        {
-            m_ctx.m_refCount--;
+        {            
+            m_ctx.m_refCount.decrementAndGet();
             m_ctx = null;
         }
     }
@@ -54,13 +54,13 @@ public void dispose()
 
     Z3Object(Context ctx)
     {
-        ctx.m_refCount++;
+        ctx.m_refCount.incrementAndGet();
         m_ctx = ctx;
     }
 
     Z3Object(Context ctx, long obj)
     {
-        ctx.m_refCount++;
+        ctx.m_refCount.incrementAndGet();
         m_ctx = ctx;
         incRef(obj);
         m_n_obj = obj;