[ANN] linear-locks: locking primitives free of deadlocks
linear-locks provides locking primitives that are statically guaranteed not to lead to deadlocks.
It achieves this by breaking one of the Coffman conditions for deadlocks: the "circular wait" condition. linear-locks ensures locks are always acquired in a consistent order.
tl;dr: Each lock is assigned a "level", tracked at the type level. When you enter a "lock scope", you're given a key that can acquire locks of level 0 or above. When you acquire a lock of level n, the key is consumed and you're given a new key of level n+1, capable of acquiring locks of level n+1 or above. This ensures locks are always acquired in order of increasing level, preventing circular waits.
The package ports the ideas of the Surelock Rust crate to Linear Haskel. As such, it relies heavily on LinearTypes and is meant to be used with linear-base. Keys are linearly typed to ensure they cannot be reused and do not escape the "lock scope". "Guards" (which represent ownership over acquired locks) are also linearly typed to ensure they are (1) always released and (2) cannot be used after being released.