Infrastructure · Primitives
Mutex
Ownership-based mutual exclusion
Definition
Mechanism
An ownership-bearing Lock for a shared Resource. An Actor that successfully acquires it becomes the sole owner and may enter the protected section. Only the owner may release it; another contender becomes owner only through a later successful acquisition after release.
Preconditions
- A shared Resource and protected section exist.
- All contenders use the same mutex state.
Postconditions
- A successful acquisition yields exactly one owner.
- Non-owners do not enter the protected section.
- Release removes the former owner's protected access.
Invariants
- Exclusivity: at most one Actor owns the mutex at a time.
- Acquire-before-access: an Actor enters the protected section only after successful acquisition.
- Owner-only release: only the current owner may perform an ordinary release.
- Release-after-use: the owner releases the mutex after leaving the protected section.
Risks
Failure modes
Deadlock
contenders form a wait cycle and no acquisition can complete.
Orphaned ownership
an owner fails without release, leaving the mutex unavailable.
Starvation
a contender is repeatedly denied under the selected acquisition policy.
Ownership violation
a non-owner releases the mutex or enters the protected section.
Caution
Exclusive access — starvation enables denial of service.
Relationships
Builds on
Accepts
A capability-bearing entity
Extends
Physics
Mutual exclusion enforcement
Nothing in this library builds on this pattern yet.
Reference