thread safety?

[jwaldmann]

I am seeing spurious errors like

  dead count != deleted
  This problem is often due to a missing call to Cudd_Ref
  or to an extra call to Cudd_RecursiveDeref.
  See the CUDD Programmer's Guide for additional details.Command terminated by signal 6

when using Cudd.Cudd from an executable (linked with cudd-3.0.0) that is compiled with -threaded.

[adamwalker]

My understanding is that Cudd is not thread safe, so I expect that compiling with -threaded will not work. I will add a note to the readme.

[jwaldmann]

I am not sure whether this behaviour is caused by CUDD or by the Haskell bindings.

I thought the purpose of having a manager argument for each CUDD function is that it's safe in the sense that you can have several threads, but each must use a unique manager.

I think that for one manager, access must be sequential. Perhaps the Haskell binding does not guarantee this. Could it be that some finalizers are run concurrently? I understand that the threaded GHC RTS has concurrent GC.

[adamwalker]

I didn't realise you had separate managers. However, since the finalizers are run concurrently (I think they are), I would still expect it to crash as you are seeing.

Perhaps it's possible to lock the finalizers. However, even in that case, how would you guarantee that the finalizers don't run at the same time as non-finalizer CUDD code in your main threads?

It might be possible to have a lock per manager that guards both main-thread operations and finalizers.

I cant really think of a good solution to this problem other than switching to the ST monad based interface with explicit dereferencing.