Pool of parallel workers that can both receive tasks from the master process and start doing tasks on their own. Unix pipes are used for communication, all while refreshing a task bar periodically.
Due to ondemand analysis, workers may do tasks unprompted (eg, when analysing a procedure, a process will typically end up analysing all its callees). Thus, children need to update the main process (which is in charge of the task bar) whenever they start analysing a new procedure, and whenever they resume analysing a previous procedure. This is more complicated than what, eg, `ParMap` can handle because of the bidirectional flow between children and parents.
The children send "Ready" or "I'm working on task <some string>" messages that are used to respectively send them more tasks ("Do x") or update the task bar with the description provided by the child.
See also ProcessPoolState
type (_, _, _) t A ('work, 'final) t process pool accepts tasks of type 'work and produces an array of results of type 'final. 'work and 'final will be marshalled over a Unix pipe.
val create : jobs:int -> child_prelude:(unit -> unit) -> f:('work -> 'result option -> child_epilogue:(unit -> 'final ) -> tasks:(unit -> ('work , 'result ) TaskGenerator.t -> ('work , 'final , 'result ) t Create a new pool of processes running jobs jobs in parallel
val run : (_ , 'final , 'result ) t -> 'final optionIStdlib.IStd .Array.tuse the processes in the given process pool to run all the given tasks in parallel and return the results of the epilogues