mirror of
https://github.com/Z3Prover/z3
synced 2025-04-08 18:31:49 +00:00
Dealt with some concurrency issues due to concurrent GC.
This commit is contained in:
parent
47ac5c0633
commit
5a45711f22
|
@ -3646,7 +3646,7 @@ namespace Microsoft.Z3
|
|||
internal Fixedpoint.DecRefQueue Fixedpoint_DRQ { get { Contract.Ensures(Contract.Result<Fixedpoint.DecRefQueue>() != null); return m_Fixedpoint_DRQ; } }
|
||||
|
||||
|
||||
internal uint refCount = 0;
|
||||
internal int refCount = 0;
|
||||
|
||||
/// <summary>
|
||||
/// Finalizer.
|
||||
|
|
|
@ -19,6 +19,7 @@ Notes:
|
|||
|
||||
using System;
|
||||
using System.Diagnostics.Contracts;
|
||||
using System.Threading;
|
||||
|
||||
namespace Microsoft.Z3
|
||||
{
|
||||
|
@ -50,8 +51,7 @@ namespace Microsoft.Z3
|
|||
|
||||
if (m_ctx != null)
|
||||
{
|
||||
m_ctx.refCount--;
|
||||
if (m_ctx.refCount == 0)
|
||||
if (Interlocked.Decrement(ref m_ctx.refCount) == 0)
|
||||
GC.ReRegisterForFinalize(m_ctx);
|
||||
m_ctx = null;
|
||||
}
|
||||
|
@ -77,7 +77,7 @@ namespace Microsoft.Z3
|
|||
{
|
||||
Contract.Requires(ctx != null);
|
||||
|
||||
ctx.refCount++;
|
||||
Interlocked.Increment(ref ctx.refCount);
|
||||
m_ctx = ctx;
|
||||
}
|
||||
|
||||
|
@ -85,7 +85,7 @@ namespace Microsoft.Z3
|
|||
{
|
||||
Contract.Requires(ctx != null);
|
||||
|
||||
ctx.refCount++;
|
||||
Interlocked.Increment(ref ctx.refCount);
|
||||
m_ctx = ctx;
|
||||
IncRef(obj);
|
||||
m_n_obj = obj;
|
||||
|
|
Loading…
Reference in a new issue