Surelock Design #
Surelock prevents deadlocks by breaking the circular-wait Coffman condition via two complementary mechanisms that do not overlap.
It answers: "can my program deadlock?" If the program compiles, it cannot.
Type Lifecycle #
┌ ─ ─ ─ ─ ─ ─ ─ ─ ─ ─ ┐
│ Explicit multi-core
│
│ Locksmith
(forge) │ ┌ ─ ─ ─ ─ ─ ─ ─ ┐
│ │ │ std (default)
▼ │ │
│ KeyVoucher │ KeyHandle
(deliver) │ (claim) │
└ ─ ─ ─ ─ ┼ ─ ─ ─ ─ ─ ┘ └ ─ ─ ─ ┼ ─ ─ ─ ┘
│ │
└────────────┬──────────┘
│
▼
MutexKey
(scope)
│
├───▶ MutexGuard(s)
│ (access)
▼
MutexKey
(subscope)
│
├───▶ MutexGuard(s)
│ (access)
▼
...
Two Mechanisms #
| Mechanism | Granularity | Acquisition | Enforcement |
|---|---|---|---|
LockSet |
Fine | Atomic | By construction |
| Levels | Coarse | Incremental | Compile-time |
Atomically acquire multiple locks: LockSet acquires multiple locks atomically, sorted by monotonic LockId. The order is always consistent across threads -- no cycle can form.
Incremental acquisition / across levels: Level<N> types with LockAfter trait bounds enforce strictly ascending acquisition. The MutexKey is consumed and re-emitted at each level. Wrong-order acquisition is a compile error, not a runtime failure.
Every lock call is either infallible (correct-by-construction) or doesn't compile.
Coffman Condition Analysis #
| Condition | Addressed? | Mechanism |
|---|---|---|
| Mutual exclusion | No | Inherent to mutexes |
| Hold and wait | Within level | LockSet atomic acquisition |
| No preemption | No | Inherent to cooperative locks |
| Circular wait | Yes | LockSet sorts by LockId; levels enforce ascending |
Circular-wait prevention is sufficient on its own to prevent deadlock. Hold-and-wait is present across levels (you hold locks while waiting for more at higher levels) but does not matter because circular wait is broken.
Design Principles #
- Parse, don't validate. The type system encodes ordering invariants directly. Invalid lock orders are unrepresentable, not just checked.
- One mechanism per concern.
LockSethandles same-level ordering. Levels handle cross-level ordering. They do not overlap and need not know about each other. - Static over dynamic. Prefer compile-time enforcement over runtime checks. The only runtime checks are scope uniqueness (
thread_local!onstd) andLocksmithsingleton enforcement (AtomicBool). Lock ordering itself is fully static. no_stdis a first-class target. The core library has no dependency onstd. Thestdfeature adds convenience (StdMutexdefault backend,lock_scope/try_lock_scopeambient entry points,thread_local!scope uniqueness). Onno_std,KeyHandlewithscope(&mut self)provides static nesting prevention withoutthread_local!.- Minimal unsafe surface.
#![deny(unsafe_code)]at the crate level. Only 6 of 15 source files opt in. The public API is fully safe.
Documents #
| Document | Contents |
|---|---|
| comparison/happylock.md | Comparison with happylock |
| comparison/lock_tree.md | Comparison with lock_tree |
| ROADMAP.md | Planned features and design sketches for v2+ |