index
:
kernel/git/cmarinas/kernel-tla.git
master
Kernel TLA+ specs
Catalin Marinas
about
summary
refs
log
tree
commit
diff
stats
log msg
author
committer
range
Age
Commit message (
Expand
)
Author
Files
Lines
2021-09-10
asidalloc: Fix inadvertently removed line from UniqueASIDActiveTask
HEAD
master
Catalin Marinas
1
-17
/
+19
2021-08-05
asidalloc: Model PTEs and an asynchronous try_to_unmap_one() call
Catalin Marinas
2
-108
/
+263
2020-10-15
fpsimd: Termination added by PlusCal
Catalin Marinas
1
-2
/
+5
2020-10-15
Add fpsimd.tla to README
Catalin Marinas
1
-0
/
+5
2020-10-15
Change check.sh to use the TLA+ tools wrapper scripts
Catalin Marinas
2
-20
/
+13
2019-09-20
fpsimd: Add SVE support
Catalin Marinas
1
-82
/
+275
2019-08-21
fpsimd: Initial support for the kernel FPSIMD state tracking
Catalin Marinas
2
-0
/
+830
2019-08-20
check.sh: Update variable parsing/splitting to use awk
Catalin Marinas
3
-10
/
+91
2019-03-01
check.sh: Remove the java.activation module option
Catalin Marinas
1
-1
/
+3
2019-02-07
Fix check.sh to deal with single-line 'vars' definition
Catalin Marinas
1
-1
/
+4
2019-01-18
check.sh: Fix typo
Catalin Marinas
1
-1
/
+1
2018-10-01
check.sh: Add java option so that TLC still works with Java 10
Catalin Marinas
1
-1
/
+1
2018-10-01
check.sh: Remove the tlc -cleanup option
Catalin Marinas
1
-1
/
+1
2018-08-10
ctxsw: Add switch_mm() (a.k.a. activate_mm) call in exec_mmap()
Catalin Marinas
1
-4
/
+8
2018-08-10
ctxsw: Replace some local variables with 'with' statements
Catalin Marinas
1
-157
/
+107
2018-08-10
ctxsw: Introduce a task.state variable to track dead threads
Catalin Marinas
1
-103
/
+114
2018-08-10
ctxsw: Remove the sleep() macro
Catalin Marinas
1
-7
/
+2
2018-08-10
ctxsw: Introduce proc_mm[] to keep track of the current mm on a CPU
Catalin Marinas
1
-0
/
+9
2018-08-10
ctxsw: Introduce an IntCall() action
Catalin Marinas
1
-5
/
+8
2018-08-10
ctxsw: Move 'cpu' into the task structure
Catalin Marinas
1
-92
/
+87
2018-08-10
ctxsw: Re-write the idle thread and interrupt handling
Catalin Marinas
2
-249
/
+327
2018-08-07
check.sh: Add sed script to extract proc_vars from vars
Catalin Marinas
1
-0
/
+5
2018-08-02
arm64kpti: Speculative TLB walking as a separate process
Catalin Marinas
2
-106
/
+72
2018-04-16
Initial commit of the arm64 Linux KPTI model
Catalin Marinas
3
-0
/
+1567
2018-04-13
qspinlock: Added bounded loop for the pending->locked handovers
Catalin Marinas
2
-37
/
+73
2018-03-28
Initial commit of the queued spinlocks model
Catalin Marinas
3
-0
/
+600
2018-03-28
check.sh: Updated for a lightweight preemption model
Catalin Marinas
1
-2
/
+5
2018-03-28
qrwlock: Updated the code path for in-interrupt
Catalin Marinas
1
-15
/
+15
2018-02-19
Initial commit of the context_switch() model
Catalin Marinas
3
-0
/
+599
2018-02-09
Initial commit of the ticketlock model
Catalin Marinas
3
-0
/
+231
2018-02-09
Initial commit of the qrwlock model
Catalin Marinas
3
-0
/
+493
2018-01-04
Initial commit of the arm64 ASID allocator specs
Catalin Marinas
5
-0
/
+1440