module Thread_pool:sig..end
add_work_for_group to
submit work to it. Work is done first-come-first-served by available threads in the
pool. Any of the available threads in the pool could be used to do work submitted to
the pool (except helper threads, see below).
A thread pool starts with no threads. As work is added, the thread pool creates new
threads to do the work, up to the maximum number of allowed threads,
max_num_threads, supplied to create. Thread-pool threads never die. They just
get created up until max_num_threads is reached and then live forever, doing work.
Each thread in the pool is in a loop, waiting for a piece of work, running the thunk,
and then repeating. It may be that all the threads in the pool are not doing
anything, but in this case, the threads still exist, and are simply blocked waiting
for work.
Sometimes one wants work to run in a dedicated thread, e.g. some C libraries require
this. To do this, use Helper_thread, see below.
All of the functions exposed by this module are thread safe; they synchronize using
a mutex on the thread pool.
type t
val invariant : t -> unitval create : max_num_threads:int -> t Core.Std.Or_error.tcreate ~max_num_threads returns a new thread pool. It is an error if
max_num_threads < 1.val finished_with : t -> unit Core.Std.Or_error.tfinished_with t destroys all the threads in t, and makes t no longer usable.
It is an error to call finished_with if the thread pool has unfinished work or
unfinished helper threads. It is an error to call any other operation on t after
calling finished_with t.
val max_num_threads : t -> intmax_num_threads t returns the maximum number of threads that t is allowed to
create.val num_threads : t -> intnum_threads t returns the number of threads that the pool t has created.module Work_group:sig..end
val create_work_group : ?min_assignable_threads:int ->
?max_assigned_threads:int ->
t -> Work_group.t Core.Std.Or_error.tcreate_work_group t ~min_assignable_threads ~max_assigned_threads creates a new
work group.
The thread pool does not internally refer to the Work_group.t it returns. So, it is
OK for client code to use a finalizer to detect it becoming unused.
It is an error if any of the following are true:
min_assignable_threads, i.e. the number of threads reserved by other work groups
plus min_assignable_threads is greater than max_num_threads.min_assignable_threads < 0min_assignable_threads > max_assigned_threadsmax_assigned_threads > max_num_threads tval add_work_for_group : ?name:string ->
t ->
Work_group.t -> (unit -> unit) -> unit Core.Std.Or_error.tadd_work_for_group t work_group f enqueues f to be done by some thread in the
pool, subject to the thread-usage limits of work_group.
It is an error to call add_work_for_group t work_group after having called
finished_with_work_group t work_group.
val finished_with_work_group : t -> Work_group.t -> unit Core.Std.Or_error.tfinished_with_work_group t work_group informs thread pool t that the work_group
will no longer be used.
It is an error to call finished_with_work_group work_group if work_group has
unfinished work or has helper_threads for which finished_with_helper_thread hasn't
yet been called.
module Helper_thread:sig..end
val create_helper_thread : ?name:string ->
t ->
Work_group.t -> Helper_thread.t Core.Std.Or_error.tcreate_helper_thread ?name t work_group creates a new helper thread that is part of
work_group, i.e. until finished_with_helper_thread is called, the helper thread
counts as one of the threads assigned to the work_group.
The thread pool does not internally refer to the Helper_thread.t it returns. So, it
is OK for client code to use a finalizer to detect it becoming unused.
It is an error if no threads are available.
val add_work_for_helper_thread : ?name:string ->
t ->
Helper_thread.t -> (unit -> unit) -> unit Core.Std.Or_error.tadd_work_for_helper_thread t f enqueues f on helper thread t's work queue.
It is an error to call add_work_for_helper_thread t after
finished_with_helper_thread t.
val finished_with_helper_thread : t -> Helper_thread.t -> unit Core.Std.Or_error.tfinished_with_helper_thread t helper_thread returns the helper thread to the
general thread pool.
It is an error to call finished_with_helper_thread if the helper thread has
unfinished work.
val sexp_of_t : t -> Sexplib.Sexp.tval ounit_tests : unit -> OUnit.testcreate ~max_num_threads returns a new thread pool. It is an error if
max_num_threads < 1.finished_with t destroys all the threads in t, and makes t no longer usable.
It is an error to call finished_with if the thread pool has unfinished work or
unfinished helper threads. It is an error to call any other operation on t after
calling finished_with t.
max_num_threads t returns the maximum number of threads that t is allowed to
create.
num_threads t returns the number of threads that the pool t has created.
Each piece of work in the thread pool is associated with a "work group", which is
used to control the number of threads used for work in the group. When a thread is
performing work for a work group, it is said to be "assigned" to that work group.
Each work group has two optional limits: min_assignable_threads and
max_assigned_threads.
The thread pool guarantees that requests to have threads assigned to this work group
will be met by at least min_assignable_threads threads. The thread pool will
never assign more than max_assigned_threads to the work group. The thread pool
does not actually reserve specific threads for the work group. It uses the same set
of threads for all work groups. Over time, a single thread may do work for
different groups. Work groups are just an accounting mechanism to make sure the
number of threads from the global pool that are being used for each work group meet
the requirements of that group.
Each work group has its own dedicated work queue. If a client requests to do some
work in a group, and that group already has min_assignable_threads threads
assigned to it, and there are no other available threads or the group already has
max_assigned_threads assigned to it, then the work will be placed on the work
group's queue, and will be handled in the future when threads become available to
the group.
If multiple work groups have work waiting to be done, the thread pool will
round-robin among them as threads become available.
create_work_group t ~min_assignable_threads ~max_assigned_threads creates a new
work group.
The thread pool does not internally refer to the Work_group.t it returns. So, it is
OK for client code to use a finalizer to detect it becoming unused.
It is an error if any of the following are true:
min_assignable_threads, i.e. the number of threads reserved by other work groups
plus min_assignable_threads is greater than max_num_threads.min_assignable_threads < 0min_assignable_threads > max_assigned_threadsmax_assigned_threads > max_num_threads tadd_work_for_group t work_group f enqueues f to be done by some thread in the
pool, subject to the thread-usage limits of work_group.
It is an error to call add_work_for_group t work_group after having called
finished_with_work_group t work_group.
finished_with_work_group t work_group informs thread pool t that the work_group
will no longer be used.
It is an error to call finished_with_work_group work_group if work_group has
unfinished work or has helper_threads for which finished_with_helper_thread hasn't
yet been called.
A helper thread is a thread with its own dedicated work queue. Work added for the
helper thread is guaranteed to be run by that thread. The helper thread only runs
work explicitly supplied to it.
create_helper_thread ?name t work_group creates a new helper thread that is part of
work_group, i.e. until finished_with_helper_thread is called, the helper thread
counts as one of the threads assigned to the work_group.
The thread pool does not internally refer to the Helper_thread.t it returns. So, it
is OK for client code to use a finalizer to detect it becoming unused.
It is an error if no threads are available.
add_work_for_helper_thread t f enqueues f on helper thread t's work queue.
It is an error to call add_work_for_helper_thread t after
finished_with_helper_thread t.
finished_with_helper_thread t helper_thread returns the helper thread to the
general thread pool.
It is an error to call finished_with_helper_thread if the helper thread has
unfinished work.