Kernel TLA+ Specifications

Kernel TLA+ Specifications

Formal TLA+ specifications of Linux kernel synchronization algorithms.

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.

Formal Methods
Key facts
Maturity
Support
C4DT
Inactive
Lab
Active
  • Technical

Robust Scalable Systems Software Lab

Robust Scalable Systems Software Lab
Sanidhya Kashyap

Prof. Sanidhya Kashyap

We focus on building systems with performance, efficiency, and robustness. We try to build practical systems by understanding the intricacies of existing layers in both software and hardware; and revisiting the design in a principled manner. Our research contributions have been published in top academic conferences, and have made great impacts on real-world programs, such as the Linux kernel.

This page was last edited on 2026-03-03.