10. Synchronous Multithreading

Felix provides a simple but model of synchronous threading. It is especially designed so this threading is extremely fast and lightweight. Millions of threads can easily be supported on desktop machines, and contest switching times are roughly the same time as subroutine calling.

Synchronous threads are sometimes called fibres. Sets of such threads fibrate a single pre-emptive thread. Each fibre is guarranteed to interleave execution serially within the same pre-emptive thread, so that no low level synchronisation primitives are required to ensure data is accessed atomically. You should not that at high levels of abstraction, context switches may still occur within what logically must be treated as an atomic operation: mutual exclusion is still required. However we do not provide any locking primitives for fibres. Instead, the sole synchronisation primitive consists of an object called a schannel, together with two functions, read and write, which purport to read or write data from or to the channel.

In fact, synchronous channels are not buffers and never hold or transmit any data, rather they are are used to synchronise and control flow in one or more fibres.

A fibre is created by the spawn_fthread procedure which accepts a procedure of type

  1 -> 0
as an argument. It is typically used like:
  spawn_fthread { thread_routine; .. };
It is unspecified whether the spawned routine or the spawning routine resumes execution first.

A bidirectional synchronous channel and associated read and write operations have types:

  fun mk_schannel[t]: unit -> schannel[t];
  proc read: &t * schannel[t];
  proc write: schannel[t] * t;