Formal TLA+ specifications of Linux kernel synchronization primitives: ASID allocator, queued RW locks, ticket spinlock, context switching, queued spinlock, arm64 KPTI, and FPSIMD/SVE state saving. Includes TLC model checker scripts for both simulation and exhaustive verification.
This page was last edited on 2026-03-03.
This page was last edited on 2026-03-03.