Kernel TLA+ specs

Clone this repo:

Branches

  1. 4bb8559 qspinlock: Split set_locked() into its own atomic step by Catalin Marinas · 3 months ago master
  2. 98c219b asidalloc: Guard flush_tlb_all() speculative reload on a mapped PTE by Catalin Marinas · 3 months ago
  3. 6866821 ctxsw: Avoid mmgrab()/mmdrop() pair on kernel->kernel context switch by Catalin Marinas · 3 months ago
  4. 5f13982 asidalloc: Fix inadvertently removed line from UniqueASIDActiveTask by Catalin Marinas · 5 years ago
  5. 50c387f asidalloc: Model PTEs and an asynchronous try_to_unmap_one() call by Catalin Marinas · 5 years ago
  6. 0278eff fpsimd: Termination added by PlusCal by Catalin Marinas · 6 years ago
  7. 49bc145 Add fpsimd.tla to README by Catalin Marinas · 6 years ago
  8. 7d90d07 Change check.sh to use the TLA+ tools wrapper scripts by Catalin Marinas · 6 years ago
  9. efdeef9 fpsimd: Add SVE support by Catalin Marinas · 7 years ago
  10. b62ac94 fpsimd: Initial support for the kernel FPSIMD state tracking by Catalin Marinas · 7 years ago
  11. fd5db28 check.sh: Update variable parsing/splitting to use awk by Catalin Marinas · 7 years ago
  12. ffaaad7 check.sh: Remove the java.activation module option by Catalin Marinas · 8 years ago
  13. 3192561 Fix check.sh to deal with single-line 'vars' definition by Catalin Marinas · 8 years ago
  14. fc4503b check.sh: Fix typo by Catalin Marinas · 8 years ago
  15. cc63c04 check.sh: Add java option so that TLC still works with Java 10 by Catalin Marinas · 8 years ago
  16. 3a1aacf check.sh: Remove the tlc -cleanup option by Catalin Marinas · 8 years ago
  17. 0b67a9a ctxsw: Add switch_mm() (a.k.a. activate_mm) call in exec_mmap() by Catalin Marinas · 8 years ago
  18. b22b2b0 ctxsw: Replace some local variables with 'with' statements by Catalin Marinas · 8 years ago
  19. 5b16677 ctxsw: Introduce a task.state variable to track dead threads by Catalin Marinas · 8 years ago
  20. ac7564f ctxsw: Remove the sleep() macro by Catalin Marinas · 8 years ago