You signed in with another tab or window. Reload to refresh your session.You signed out in another tab or window. Reload to refresh your session.You switched accounts on another tab or window. Reload to refresh your session.Dismiss alert
It appears that when using In_thread.Helper_thread, in spite of what is indicated by the docs:
create uses a thread from Async's thread pool, reserving that thread for exclusive use by the helper thread until the helper thread is no longer used (specifically, finalized and is finished with all its work), at which point the thread is made available for general use by the pool.
helper threads are in fact never finalized and never made available for general use by the pool.
The reason for this seems to be that Thread_pool.Thread.t's type state, when in Helper mode, references the Helper_thread.t (and thus the Helper_thread cannot be finalized), and the only way that a Thread can leave Helper mode is through maybe_finish_helper_thread, which only does something if the state of the helper thread is Finishing, which is only the case if finished_with_helper_thread is called, which only happens when the In_thread.Helper_thread is finalized (which it can't be because it's in Helper mode, a catch-22).
If In_thread.Helper_thread exposed a call to finished_with_helper_thread, then the user could at least manually free up the thread. Or you can work around it by using Thread_pool directly instead of using In_thread, but then you have to reimplement In_thread.run, a non-trivial function. Otherwise, there is probably a way around the catch so that it gets properly gc'd but I don't have a solution right off.
The text was updated successfully, but these errors were encountered:
I think this issue actually still exists. I've been meaning to write a test case to demonstrate it but haven't had a chance yet. I'll share the results here when I do.
It appears that when using In_thread.Helper_thread, in spite of what is indicated by the docs:
helper threads are in fact never finalized and never made available for general use by the pool.
The reason for this seems to be that Thread_pool.Thread.t's type state, when in
Helper mode, references the Helper_thread.t (and thus the Helper_thread cannot be finalized), and the only way that a Thread can leave
Helper mode is through maybe_finish_helper_thread, which only does something if the state of the helper thread isFinishing, which is only the case if finished_with_helper_thread is called, which only happens when the In_thread.Helper_thread is finalized (which it can't be because it's in
Helper mode, a catch-22).If In_thread.Helper_thread exposed a call to finished_with_helper_thread, then the user could at least manually free up the thread. Or you can work around it by using Thread_pool directly instead of using In_thread, but then you have to reimplement In_thread.run, a non-trivial function. Otherwise, there is probably a way around the catch so that it gets properly gc'd but I don't have a solution right off.
The text was updated successfully, but these errors were encountered: