| This repository contains formal TLA+ specs of different algorithms used |
| in the Linux kernel. |
| |
| The recommended way to enable the checking of these specs is to use the |
| TLA+ wrapper scripts: |
| |
| $ git clone https://github.com/pmer/tla-bin.git |
| $ ./download_or_update_tla.sh |
| $ ./install.sh $PREFIX |
| |
| The TLA+ Tools can also be downloaded directly from: |
| |
| https://lamport.azurewebsites.net/tla/tools.html |
| |
| A Java runtime is required. |
| |
| asidalloc.tla |
| ------------- |
| |
| Model of the ASID allocator used by the arm64 kernel port (and arm): |
| arch/arm64/mm/context.c |
| |
| To run a full check of the current configuration: |
| |
| ./check.sh asidalloc |
| |
| Note that, depending on your hardware, it may take over two days to |
| complete in the current configuration. You can reduce the number of |
| tasks in asidalloc.cfg (4 tasks should complete in less than an hour). |
| |
| To run in simulation mode (quicker at finding bugs but it may not |
| explore all corner cases): |
| |
| ./check.sh asidalloc -simulate -depth 300 |
| |
| qrwlock.tla |
| ----------- |
| |
| Model of the queued read-write locks implemented in the kernel. The |
| model is generic and avoids specific architecture instructions (e.g. |
| LDXR/STXR or LDADD as on arm64). |
| |
| ticketlock.tla |
| -------------- |
| |
| Model of the ticket spinlock implementation as on arm64 but avoiding |
| specific arm64 instructions. |
| |
| ctxsw.tla |
| --------- |
| |
| Model of the Linux kernel context_switch() function together with |
| exit_mm() and exec_mmap(), aimed at checking the mm_struct.mm_users and |
| mm_count handling. |
| |
| qspinlock.tla |
| ------------- |
| |
| Model of the Linux queued spinlock implementation, modified to avoid |
| cmpxchg() loops which cannot guarantee forward progress. |
| |
| arm64kpti.tla |
| ------------- |
| |
| Model of the arm64 Linux KPTI support, checking the TLB separation |
| (page table and ASIDs) between user, kernel, EFI mapping and idmap. |
| |
| fpsimd.tla |
| ---------- |
| |
| Model of the FPSIMD/SVE register state saving and restoring. |
