Thread synchronization overview

The documentation should include all this information that @hargoniX sent me, which covers synchronization tools but not async yet. Some of this is here, but the rest should be added and the overview should be more explicit.

ST.Ref/IO.Ref:

• Mutable memory cells that can be operated from within ST or BaseIO (and friends).
  • In the single threaded case they are simple mutable memory accesses
  • In the multi threaded case they are implemented as spinlocks
• create new one with mkRef
• get: take a local reference to the value from the Ref, increasing its RC.
• set: put a new value into Ref
• swap: atomically replace the current value in the Ref with a new one and return the old value
• take: take the value that is currently inside of the Ref and don't provide a replacement yet
  (can be provided later with set). Crucially unlike get this operation does not increment the
  RC of the value. Notably in the multi threaded case this function leaves the
  spinlock locked until a set happens and should thus be used with caution (hence why it's unsafe)
• ptrEq, check if two Ref point to the same mutable memory location
• modify/modifyGet act like monadic modify/modifyGet, they:
  1. take the value from the Ref
  2. run a function f on it
  3. set the resulting value (and potentially return it)
     Crucially due to the spinlock nature of Ref, f should never run long as this has the potential
     to hang other threads while spinning
• Summary: Use either for mutable memory in single threaded cases or if you are working with very
  short functions operating on a shared multi threaded state. If your functions are not short
  consider one of the mutex variants

Every mutex variant comes in two forms Base and a data carrying variant. The base variant acts like
a classical lock while the data carrying variant has the data it carries with itself explicitly attached.

The most simple variant is just Std.BaseMutex which acts like a normal lock and provides:

• new to create a new one
• lock to lock it, will block the current thread until the BaseMutex is available
  (while technically UB due to the C++ implementation this will just deadlock if
  called multiple times by the same thread without unlocking in between)
• tryLock to try and lock it right now, if it is already taken return false instantly otherwise
  take the lock and return true
• unlock to unlock it

The data carrying variant of Std.BaseMutex is Std.Mutex:

• new to create a new one with a certain initial piece of data associated
• atomically k to run lock the mutex, run k with access to the shared state and unlock it again afterwards
• tryAtomically k to try and lock the mutex, if available act like atomically k and return the
  value as some, if not available return none

Beyond this we have the Std.BaseSharedMutex and Std.SharedMutex. They provide a read-write lock
style functionality that is:

• there may be either up to infinitely many readers working on the shared state at a time
• xor exactly one writer (note that the writer may of course read the data as well as it has
  exclusive access)

Std.BaseSharedMutex:

• new to create a new one
• write to acquire write style access, will block until no writers and other readers are working
• tryWrite to attempt to acquire a write style access, return true if possible without blocking,
  false otherwise
• unlockWrite to relinquish write style access
• same with read/tryRead/unlockRead except that the condition is to block only until no
  writers are working

The data carrying variant is Std.SharedMutex:

• new to create a new one with a certain initial piece of data associated
• atomically k to write lock, run k then unlockWrite
• tryAtomically k like with Std.Mutex except that we take a write lock, note that the two
  functions are intentionally named the same to enable drop-in replacement of a Std.Mutex with a
  SharedMutex
• atomicallyRead k/tryAtomicallyRead k like atomically/tryAtomically but only acquire read
  access and as such also only provide read access to the underlying data

Std.BaseRecursiveMutex and Std.RecursiveMutex are like Std.BaseMutex and Std.Mutex except
that they are reentrant/recursive locks, meaning that multiple calls to lock/atomically from the
same thread will not hang and instead just go through, they must however be met with a matching
amount of unlock when using the BaseRecursiveMutex variant in order to properly unlock again
(mutliple nested atomically of course just do that for you). Note that using this type of lock is
not popular with some people and you should probably try to avoid it in favor of better locking
schemes if possible.

Std.Condvar can be used with a BaseMutex/Mutex to provide a regular condition variable style
primitive, see the documentation at https://leanprover-community.github.io/mathlib4_docs/Std/Sync/Mutex.html#Std.Condvar
for a pretty exact description of the protocol. Condition variables are generally used in situations
where there is one thread that is waiting for a certain kind of condition (involving shared state
guarded by a mutex) to hold and other threads are working this shared state. The waiting thread can
use a condition variable that gets notified by other threads when they think the condition may
be true, the waiting thread then wakes up, locks the mutex, checks the condition and depending on
whether it holds or not unlocks and goes to sleep again or continues on with its work.

Std.Barrier can be used to provide a synchronization point for n threads:

• new creates a new Barrier that acts as a synchronization point to numThreads threads
• calling wait will block numThreads - 1 times before the caller wakes up all other threads and
  they continue together. Notably Std.Barrier is reusable so this type of rendezvous can happen
  multiple times using the same barrier

Channels in lean can be configured along three axis

First closing behavior:

• Std.CloseableChannel which is a channel that may be closed and thus both sending and receiving
  on it may return an error
• Std.Channel cannot be closed and thus sending and receiving can never throw an error

Second buffer size:

• some 0: will create a channel that always acts as a synchronization point, that is every send
  will wait for a corresponding recv to arrive and vice versa
• some n: will create a channel with an internal buffer of size n, while there is less than n
  elements waiting to be receivied a send will never have to wait and can just enqueue its value
  into the buffer
• none: will create an unbounded channel with a (potentially) everygrowing buffer. While this
  means that send can never block, having slightly faster senders than receivers can cause an
  arbitrarily large memory consumption as values pile up. We thus recommend using either a zero
  sized or buffered channel for almost all applications.

Third synchronization mode:

• Std.Channel/Std.CloseableChannel will return IO.Promise
• Std.Channel.Sync/Std.CloseableChannel.Sync will make operations block the current thread if they need to wait

I will only cover the Sync variant here as they are relevant for programming without the async
stack being fully available yet.

A new channel may be created with Std.Channel.Sync.new/Std.CloseableChannel.Sync.new, passing
the capacity to it. For backwards compatability reasons the capacity has a default value of the
(undesirable) none. Both variants then provide functionality to:

• send v a value v, potentially blocking if the buffer size of the channel does not allow this
  right away. Note that CloseableChannel may throw an error here if the channel is already closed
• trySend v a value v, returning true if this was possible right away or giving up and
  returning false otherwise
• recv a value, potentially blocking if none is available right away. Note that CloseableChannel
  may return none if the channel is already closed or gets closed while blocking.
• tryRecv a value, returning some v if a value was available right away or none if not
• a ForIn instance to indefinitely wait on new values on the channel using
  for msg in ch do foo msg. Notably CloseableChannel will eventually abort this loop when the
  channel is closed

Furthermore CloseableChannel offers:

• close to close the channel, note that this is not idempotent and will throw an error if
  called more than once in order to enforce a well behaved cleanup behavior. Beyond this a call to
  close will make all currently blocking recv return none
• isClosed to check if the channel is already closed (note that right after a call to isClosed
  it may of course get closed so this is not sufficient as some sort of atomic check before closing
  the channel)

As for the ordering behavior of the messages in the channel: It generally provides a FIFO style
behavior though of course in the presence of multiple producers/consumers this guarantee does not
mean too much.

important note regarding FBIP: Currently all ways of sharing a mutable state across threads
inherently prevent any in-place updates of datastructures, that is for example access to
Std.Mutex (Array Nat) within atomically will not be updated in place but instead copy.
This is a flaw that may be addressed in the future but for now we recommend not using FBIP
structures with synchronization primitives unless you know exactly what you are doing. (For example
maintaining a Vector of Ref Nat within a Std.Mutex and only updating the Ref will of course
still act in place and not copy Vector all the time as "the access is not really happening to the
Vector")

Start by locating the synchronization overview in the reference manual and compare it with the tools and caveats listed in the issue. Cover the stated Ref, mutex, condition variable, barrier, and synchronous channel behavior, while keeping async coverage out of scope. Done means the overview explicitly describes these APIs, usage guidance, channel variants, and the FBIP warning.