package coq
Install
Dune Dependency
Authors
Maintainers
Sources
sha256=583471c8ed4f227cb374ee8a13a769c46579313d407db67a82d202ee48300e4b
doc/coq-core.stm/AsyncTaskQueue/index.html
Module AsyncTaskQueueSource
This file provides an API for defining and managing a queue of tasks to be done by external workers.
A queue of items of type task is maintained, then for each task, a request is generated, then sent to a worker using marshalling.
The workers will then eventually return a result, using marshalling again: ____ ____ ____ ________ | T1 | T2 | T3 | => request => | Worker | |____|____|____| <= response <= |________| | Master Proc. | \--------------/
Thus request and response must be safely marshallable.
Operations for managing the task queue are provide, see below for more details.
The Task module type defines an abstract message-processing queue.
cancel_switch to be flipped to true by anyone to signal the task is not relevant anymore. When the STM performs an undo/edit-at, it crawls the document and flips these flags (the Qed node carries a pointer to the flag IIRC).
Client-side functor. MakeQueue T creates a task queue for task T
Server-side functor. MakeWorker T creates the server task dispatcher.