$ git log --pretty=format:'%h %s (%cs)%d'
5f13982 asidalloc: Fix inadvertently removed line from UniqueASIDActiveTask (2021-09-10)
(HEAD -> master)
50c387f asidalloc: Model PTEs and an asynchronous try_to_unmap_one() call (2021-08-05)
0278eff fpsimd: Termination added by PlusCal (2020-10-15)
49bc145 Add fpsimd.tla to README (2020-10-15)
7d90d07 Change check.sh to use the TLA+ tools wrapper scripts (2020-10-15)
efdeef9 fpsimd: Add SVE support (2019-09-20)
b62ac94 fpsimd: Initial support for the kernel FPSIMD state tracking (2019-08-21)
fd5db28 check.sh: Update variable parsing/splitting to use awk (2019-08-20)
ffaaad7 check.sh: Remove the java.activation module option (2019-03-01)
3192561 Fix check.sh to deal with single-line 'vars' definition (2019-02-07)
...
$ git cat-file blob HEAD:README
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.
# heads (aka `branches'):
$ git for-each-ref --sort=-creatordate refs/heads \
--format='%(HEAD) %(refname:short) %(subject) (%(creatordate:short))'
* master asidalloc: Fix inadvertently removed line from UniqueASIDActiveTask (2021-09-10)
# tags:
$ git for-each-ref --sort=-creatordate refs/tags \
--format='%(refname:short) %(subject) (%(creatordate:short))'
# no tags, yet...
# associated public inboxes:
# (number on the left is used for dev purposes)
1 lkml
1 linux-m68k
git clone https://80x24.org/lore/pub/scm/linux/kernel/git/cmarinas/kernel-tla.git