Module Thread_pool

module Thread_pool: Thread_pool

module Priority: module type of Linux_ext.Priority  with type t = Linux_ext.Priority.t

type t 

include Invariant.S

val create : max_num_threads:int -> t Core.Std.Or_error.t

val finished_with : t -> unit Core.Std.Or_error.t

val max_num_threads : t -> int

val num_threads : t -> int

val default_priority : t -> Priority.t

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.t

val add_work_for_group : ?priority:Priority.t ->
       ?name:string ->
       t ->
       Work_group.t -> (unit -> unit) -> unit Core.Std.Or_error.t

val finished_with_work_group : t -> Work_group.t -> unit Core.Std.Or_error.t

module Helper_thread: sig .. end

val create_helper_thread : ?priority:Priority.t ->
       ?name:string ->
       t ->
       Work_group.t -> Helper_thread.t Core.Std.Or_error.t

val add_work_for_helper_thread : ?priority:Priority.t ->
       ?name:string ->
       t ->
       Helper_thread.t -> (unit -> unit) -> unit Core.Std.Or_error.t

val finished_with_helper_thread : t -> Helper_thread.t -> unit Core.Std.Or_error.t

val sexp_of_t : t -> Sexplib.Sexp.t

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.

default_priority t returns the priority that will be used for work performed by t, unless that work is added with an overriding priority.

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:

• the thread pool can not guarantee that it can satisfy requests to use 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 < 0
• min_assignable_threads > max_assigned_threads
• max_assigned_threads > max_num_threads t

Exceptions raised by f are silently ignored.

It is an error to call add_work_for_group t work_group after having called finished_with_work_group t work_group.

While the work is run, the name of the thread running the work will be set (via Linux_ext.pr_set_name) to name and the priority of the thread will be set to priority.

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.

default_name t returns the name that will be used for work performed by t, unless that work is added with an overriding name

default_priority t returns the priority that will be used for work performed by t, unless that work is added with an overriding priority.

create_helper_thread ?priority ?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.

When the helper thread runs work, it will be at the helper thread's name and priority, except for work that is added with an overriding priority or name.

add_work_for_helper_thread ?priority ?name t helper_thread f enqueues f on helper_thread's work queue.

Exceptions raised by f are silently ignored.

It is an error to call add_work_for_helper_thread t after finished_with_helper_thread t.

When the helper thread runs f, it will be at the helper thread's name and priority, unless overriden by name or priority.

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.