package coq
Install
dune-project
Dependency
Authors
Maintainers
Sources
sha256=3cbfc1e1a72b16d4744f5b64ede59586071e31d9c11c811a0372060727bfd9c3
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.