From 6263252bf5b07e81fe97da378b799a018e5221c8 Mon Sep 17 00:00:00 2001 From: "Christoph M. Wintersteiger" Date: Wed, 14 Oct 2015 12:42:27 +0100 Subject: [PATCH 1/4] Bugfix for concurrent garbage collection in Java API. Relates to #205 and #245 --- src/api/java/Context.java | 45 +++++++++++++++++++++++++------------- src/api/java/Z3Object.java | 8 +++---- 2 files changed, 34 insertions(+), 19 deletions(-) diff --git a/src/api/java/Context.java b/src/api/java/Context.java index 0955f79ca..7d4afdf71 100644 --- a/src/api/java/Context.java +++ b/src/api/java/Context.java @@ -18,6 +18,7 @@ Notes: package com.microsoft.z3; import java.util.Map; +import java.util.concurrent.atomic.AtomicInteger; import com.microsoft.z3.enumerations.Z3_ast_print_mode; @@ -3761,29 +3762,42 @@ public class Context extends IDisposable 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(); + } } /** @@ -3791,6 +3805,7 @@ public class Context extends IDisposable **/ 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 index 877e22cac..c9ed810fa 100644 --- a/src/api/java/Z3Object.java +++ b/src/api/java/Z3Object.java @@ -43,8 +43,8 @@ public class Z3Object extends IDisposable } if (m_ctx != null) - { - m_ctx.m_refCount--; + { + m_ctx.m_refCount.decrementAndGet(); m_ctx = null; } } @@ -54,13 +54,13 @@ public class Z3Object extends IDisposable 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; From e312b47be6365fd9b193a5a6e0acb4d8d7dde93e Mon Sep 17 00:00:00 2001 From: "Christoph M. Wintersteiger" Date: Wed, 14 Oct 2015 12:43:09 +0100 Subject: [PATCH 2/4] Bugfix for object finalization in Java API. Relates to #205 and #245 --- src/api/java/AST.java | 15 +++++++-------- src/api/java/Constructor.java | 13 +++++++++++-- src/api/java/ConstructorList.java | 13 +++++++++++-- src/api/java/Z3Object.java | 13 +++++++++++-- 4 files changed, 40 insertions(+), 14 deletions(-) diff --git a/src/api/java/AST.java b/src/api/java/AST.java index 6b5493bf9..dc73c7ae7 100644 --- a/src/api/java/AST.java +++ b/src/api/java/AST.java @@ -33,7 +33,7 @@ public class AST extends Z3Object implements Comparable { AST casted = null; - try + try { casted = AST.class.cast(o); } catch (ClassCastException e) @@ -41,13 +41,12 @@ public class AST extends Z3Object implements Comparable return false; } - return - (this == casted) || - (this != null) && - (casted != null) && - (getContext().nCtx() == casted.getContext().nCtx()) && - (Native.isEqAst(getContext().nCtx(), getNativeObject(), casted.getNativeObject())); -} + return (this == casted) || + (this != null) && + (casted != null) && + (getContext().nCtx() == casted.getContext().nCtx()) && + (Native.isEqAst(getContext().nCtx(), getNativeObject(), casted.getNativeObject())); + } /** * Object Comparison. diff --git a/src/api/java/Constructor.java b/src/api/java/Constructor.java index 2ceaddcff..26b33ed35 100644 --- a/src/api/java/Constructor.java +++ b/src/api/java/Constructor.java @@ -80,11 +80,20 @@ public class Constructor extends Z3Object /** * Destructor. + * @throws Throwable * @throws Z3Exception on error **/ - protected void finalize() + protected void finalize() throws Throwable { - Native.delConstructor(getContext().nCtx(), getNativeObject()); + try { + Native.delConstructor(getContext().nCtx(), getNativeObject()); + } + catch (Throwable t) { + throw t; + } + finally { + super.finalize(); + } } private int n = 0; diff --git a/src/api/java/ConstructorList.java b/src/api/java/ConstructorList.java index 2b3aa94e2..82b119513 100644 --- a/src/api/java/ConstructorList.java +++ b/src/api/java/ConstructorList.java @@ -24,11 +24,20 @@ public class ConstructorList extends Z3Object { /** * Destructor. + * @throws Throwable * @throws Z3Exception on error **/ - protected void finalize() + protected void finalize() throws Throwable { - Native.delConstructorList(getContext().nCtx(), getNativeObject()); + try { + Native.delConstructorList(getContext().nCtx(), getNativeObject()); + } + catch (Throwable t) { + throw t; + } + finally { + super.finalize(); + } } ConstructorList(Context ctx, long obj) diff --git a/src/api/java/Z3Object.java b/src/api/java/Z3Object.java index c9ed810fa..473cb5403 100644 --- a/src/api/java/Z3Object.java +++ b/src/api/java/Z3Object.java @@ -25,10 +25,19 @@ public class Z3Object extends IDisposable { /** * Finalizer. + * @throws Throwable **/ - protected void finalize() + protected void finalize() throws Throwable { - dispose(); + try { + dispose(); + } + catch (Throwable t) { + throw t; + } + finally { + super.finalize(); + } } /** From bae3a76c8ab73ed7ac9d6255a853e9aa26f15792 Mon Sep 17 00:00:00 2001 From: "Christoph M. Wintersteiger" Date: Wed, 14 Oct 2015 12:52:16 +0100 Subject: [PATCH 3/4] Removed unnecessary debug output. --- src/api/java/Context.java | 7 ------- 1 file changed, 7 deletions(-) diff --git a/src/api/java/Context.java b/src/api/java/Context.java index 7d4afdf71..3897ec50a 100644 --- a/src/api/java/Context.java +++ b/src/api/java/Context.java @@ -3783,14 +3783,7 @@ public class Context extends IDisposable // OK. } m_ctx = 0; - System.out.println("> disposed OK."); } - else if (m_refCount.get() < 0) - System.out.println("XXX negative ref count"); - else - { - System.out.println("XXX context not disposed"); - } } catch (Throwable t) { throw t; From b66f34f0d265a6c0c186f61671e6ece98280b54d Mon Sep 17 00:00:00 2001 From: "Christoph M. Wintersteiger" Date: Wed, 14 Oct 2015 12:53:18 +0100 Subject: [PATCH 4/4] Removed unnecessary debug output. --- src/api/java/Context.java | 1 - 1 file changed, 1 deletion(-) diff --git a/src/api/java/Context.java b/src/api/java/Context.java index 3897ec50a..8b7157181 100644 --- a/src/api/java/Context.java +++ b/src/api/java/Context.java @@ -3798,7 +3798,6 @@ public class Context extends IDisposable **/ public void dispose() { - System.out.println("> context disposing."); m_AST_DRQ.clear(this); m_ASTMap_DRQ.clear(this); m_ASTVector_DRQ.clear(this);