Kernel TLA+ specs

Clone this repo:

Branches

  1. 0b67a9a ctxsw: Add switch_mm() (a.k.a. activate_mm) call in exec_mmap() by Catalin Marinas · 4 months ago master
  2. b22b2b0 ctxsw: Replace some local variables with 'with' statements by Catalin Marinas · 4 months ago
  3. 5b16677 ctxsw: Introduce a task.state variable to track dead threads by Catalin Marinas · 4 months ago
  4. ac7564f ctxsw: Remove the sleep() macro by Catalin Marinas · 4 months ago
  5. 7a7c349 ctxsw: Introduce proc_mm[] to keep track of the current mm on a CPU by Catalin Marinas · 4 months ago
  6. 4e46179 ctxsw: Introduce an IntCall() action by Catalin Marinas · 4 months ago
  7. 0f8cf64 ctxsw: Move 'cpu' into the task structure by Catalin Marinas · 4 months ago
  8. 692d4a8 ctxsw: Re-write the idle thread and interrupt handling by Catalin Marinas · 4 months ago
  9. 464c3a9 check.sh: Add sed script to extract proc_vars from vars by Catalin Marinas · 4 months ago
  10. d431124 arm64kpti: Speculative TLB walking as a separate process by Catalin Marinas · 4 months ago
  11. b99340f Initial commit of the arm64 Linux KPTI model by Catalin Marinas · 8 months ago
  12. 92f30bc qspinlock: Added bounded loop for the pending->locked handovers by Catalin Marinas · 8 months ago
  13. eeee492 Initial commit of the queued spinlocks model by Catalin Marinas · 9 months ago
  14. 36fda4a check.sh: Updated for a lightweight preemption model by Catalin Marinas · 9 months ago
  15. e4312e7 qrwlock: Updated the code path for in-interrupt by Catalin Marinas · 9 months ago
  16. 2049ecd Initial commit of the context_switch() model by Catalin Marinas · 10 months ago
  17. 4329ffe Initial commit of the ticketlock model by Catalin Marinas · 10 months ago
  18. c39435e Initial commit of the qrwlock model by Catalin Marinas · 10 months ago
  19. de0c2f5 Initial commit of the arm64 ASID allocator specs by Catalin Marinas · 11 months ago