| This repository contains formal TLA+ specs of different algorithms used |
| in the Linux kernel. So far it only contains asidalloc.tla (see below). |
| |
| The TLA+ Tools need to be installed (together with a Java runtime): |
| |
| https://lamport.azurewebsites.net/tla/tools.html (pre-built) |
| |
| or: |
| |
| https://github.com/tlaplus/tlaplus/tree/master/tlatools (source) |
| |
| The graphical TLA Toolbox is not required. |
| |
| CLASSPATH in check.sh needs to point to the TLA+ Tools installation |
| directory. |
| |
| |
| 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. |
