Parameter MakeWorker.1-T
type task
Main description of a task. Elements are stored in the "master" process, and then converted into a request.
type competence
competence
stores the information about what kind of work a worker has completed / has available.
type worker_status
=
|
Fresh
|
Old of competence
A worker_status is:
`Fresh
when a worker is born.
`Old of competence
: When a worker ends a job it can either die (and be replaced by a fresh new worker) or hang there as an`Old
worker. In such case some data can be carried by the`Old
constructor, typically used to implementrequest_of_task
.
This allows to implement both one-shot workers and "persistent" ones. E.g. par: is implement using workers that don't "reboot". Proof workers do reboot mainly because the vm has some C state that cannot be cleared, so you have a real memory leak if you don't reboot the worker.
type request
Type of input and output data for workers.
The data must be marshallable as it send through the network using
Marshal
.
Master API, it is run by the master, on a thread
val request_of_task : worker_status -> task -> request option
request_of_task status t
takes thestatus
of the worker and a taskt
and creates the correspondingSome request
to be sent to the worker or it is not valid anymoreNone
.
val task_match : worker_status -> task -> bool
task_match status tid
Allows to discard tasks based on the worker status.
val use_response : worker_status -> task -> response -> [ `Stay of competence * task list | `End ]
use_response status t out
For a response
out
to a taskt
withstatus
we can choose to end the worker of to keep it alive with some data and immediately inject extra tasks in the queue.For example, the proof worker runs a proof and finds an error, the response signals that, e.g.
ReponseError {state = 34; msg = "oops"}
When the manager uses such a response he can tell the worker to stay there and inject into the queue an extra task requesting state 33 (to implement efficient proof repair).
val on_marshal_error : string -> task -> unit
on_marshal_error err_msg tid
notifies of marshaling failure.
val on_task_cancellation_or_expiration_or_slave_death : task option -> unit
on_task_cancellation_or_expiration_or_slave_death tid
These functions are meant to parametrize the worker manager on the actions to be taken when things go wrong or are cancelled (you can kill a worker in CoqIDE, or using kill -9...)
E.g. master can decide to inhabit the (delegate) Future.t with a closure (to be run in master), i.e. make the document still checkable. This is what I do for marshaling errors.
val forward_feedback : Feedback.feedback -> unit
forward_feedback fb
sends fb to all the workers.
Worker API, it is run by worker, on a different fresh process
val name_of_task : task -> string
debugging
val name_of_request : request -> string