IO.Async.Loop.Posix

A pool of a fixed number of worker threads, each operating on its own
work queue.

Idle threads will try and take work packages from other threads
(work-stealing).

Each thread is responsible for scheduling and running an arbitrary number
of `Fiber`s, as well as taking care of registered timers, signal handlers,
and file polling.

Reexports

Definitions

0 Task : Type

Totality: total
Visibility: public export

record Poll : Type

Totality: total
Visibility: export
Constructor: 

W : (size : Nat) -> Fin size -> IORef Bool -> IORef (Queue Task) -> IArray size Poll -> Poller -> IORef Nat -> Timer -> Sighandler -> Mutex -> Condition -> Poll

Projections:

.alive : Poll -> IORef Bool

  Reference indicating whether the pool is still alive

.cond : Poll -> Condition

  Condition used for sleeping

.lock : Poll -> Mutex

  Mutex used for sleeping

.me : ({rec:0} : Poll) -> Fin (size {rec:0})

  Index of the worker thread corresponding to this state

.poller : Poll -> Poller

  The state used for polling file descriptors

.queue : Poll -> IORef (Queue Task)

  Work queue of this worker

.signals : Poll -> Sighandler

  State for the signal handler

.size : Poll -> Nat

  Number of worker threads in the pool

.stealers : Poll -> IORef Nat

  Remaining number of stealers. To reduce contention,
  not all idle workers will be allowed to steal work
  at the same time

.timer : Poll -> Timer

  State for schedule actions

.workers : ({rec:0} : Poll) -> IArray (size {rec:0}) Poll

  Work queues of all worker threads

Hints:

EventLoop Poll

PollH Poll

SignalH Poll

TimerH Poll

record ThreadPool : Type

  A fixed-size pool of `n` physical worker threads.
  
  Tasks are submited to the worker threads in round-robin
  fashion: A new task is submitted to the next worker in line,
  restarting at the beginning when reaching the last worker.

Totality: total
Visibility: export
Constructor: 

TP : (size : Nat) -> Vect size ThreadID -> ThreadID -> Vect (S size) Poll -> ThreadPool

Projections:

.ids : ({rec:0} : ThreadPool) -> Vect (size {rec:0}) ThreadID

.pollid : ThreadPool -> ThreadID

.size : ThreadPool -> Nat

.workers : ({rec:0} : ThreadPool) -> Vect (S (size {rec:0})) Poll

app : Subset Nat IsSucc -> List Signal -> IO1 Poller -> Async Poll [] () -> IO ()

  Starts an epoll-based event loop and runs the given async
  program to completion.
  
  `n`    : Number of threads to use
  `sigs` : The signals to block while running the program.
           These are typically the ones dealt with as part of `prog`
  `prog` : The program to run

Visibility: export

asyncThreads : IO (Subset Nat IsSucc)

  Reads environment variable `IDRIS2_ASYNC_THREADS` and returns
  the number of threads to use. Default: 2.

Totality: total
Visibility: export

simpleApp : {default [SIGINT] sigs : List Signal} -> Has SIGINT sigs => Async Poll [] () -> IO ()

  Simplified version of `app`.
  
  This uses the posix-compatible `poll` call for polling files. For
  a faster poller - especially when polling hundreds or thousands of
  file descriptors at a time - consider using `IO.Async.Loop.Epoll.epollApp`.
  
  We use environment variable `IDRIS2_ASYNC_THREADS` to determine the
  number of threads to use (default: 2) and cancel the running program
  on receiving `SIGINT`.
  
  By default, only `SIGINT` is masked, to handle other signals
  within your program, give `{sigs = [...]}` as the first
  argument. One of the signals must be SIGINT, which is enforced by
  the `Has SIGINT sigs` constraint.

Visibility: export