[ANN] linear-locks: locking primitives free of deadlocks

Announcements
1

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.

18 Likes
2

This is a cool idea, but I don’t think it really requires LinearTypes. Sketch:

-- Compile-time proof tokens.
type (<) :: k -> k -> ZeroBitType

(~) :: l < m -> m < n -> l < n

-- Newtype over IO, annotated by "lock level" and "acquisition level".
type Scoped :: k -> k -> Type -> Type

run :: (forall k (l :: k). Scoped l l b) -> IO b

fork :: Scoped l a () -> Scoped l a ThreadId

-- Newtype over MVar, annotated by level.
type Lock :: k -> Type -> Type

-- Create a new lock level and corresponding lock.
new
  :: b
  -> (forall m. l < m -> Lock m b -> Scoped m a r)
  -> Scoped l a r

-- Given that the acquisition level is less than the level of the lock,
-- acquire it in a scope of the corresponding acquisition level.
with
  :: a < m
  -> Lock m b
  -> (b -> Scoped l m (b, r))
  -> Scoped l a r
1 Like