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.