aboutsummaryrefslogtreecommitdiffstats
AgeCommit message (Expand)AuthorFilesLines
2021-09-10asidalloc: Fix inadvertently removed line from UniqueASIDActiveTaskHEADmasterCatalin Marinas1-17/+19
2021-08-05asidalloc: Model PTEs and an asynchronous try_to_unmap_one() callCatalin Marinas2-108/+263
2020-10-15fpsimd: Termination added by PlusCalCatalin Marinas1-2/+5
2020-10-15Add fpsimd.tla to READMECatalin Marinas1-0/+5
2020-10-15Change check.sh to use the TLA+ tools wrapper scriptsCatalin Marinas2-20/+13
2019-09-20fpsimd: Add SVE supportCatalin Marinas1-82/+275
2019-08-21fpsimd: Initial support for the kernel FPSIMD state trackingCatalin Marinas2-0/+830
2019-08-20check.sh: Update variable parsing/splitting to use awkCatalin Marinas3-10/+91
2019-03-01check.sh: Remove the java.activation module optionCatalin Marinas1-1/+3
2019-02-07Fix check.sh to deal with single-line 'vars' definitionCatalin Marinas1-1/+4
2019-01-18check.sh: Fix typoCatalin Marinas1-1/+1
2018-10-01check.sh: Add java option so that TLC still works with Java 10Catalin Marinas1-1/+1
2018-10-01check.sh: Remove the tlc -cleanup optionCatalin Marinas1-1/+1
2018-08-10ctxsw: Add switch_mm() (a.k.a. activate_mm) call in exec_mmap()Catalin Marinas1-4/+8
2018-08-10ctxsw: Replace some local variables with 'with' statementsCatalin Marinas1-157/+107
2018-08-10ctxsw: Introduce a task.state variable to track dead threadsCatalin Marinas1-103/+114
2018-08-10ctxsw: Remove the sleep() macroCatalin Marinas1-7/+2
2018-08-10ctxsw: Introduce proc_mm[] to keep track of the current mm on a CPUCatalin Marinas1-0/+9
2018-08-10ctxsw: Introduce an IntCall() actionCatalin Marinas1-5/+8
2018-08-10ctxsw: Move 'cpu' into the task structureCatalin Marinas1-92/+87
2018-08-10ctxsw: Re-write the idle thread and interrupt handlingCatalin Marinas2-249/+327
2018-08-07check.sh: Add sed script to extract proc_vars from varsCatalin Marinas1-0/+5
2018-08-02arm64kpti: Speculative TLB walking as a separate processCatalin Marinas2-106/+72
2018-04-16Initial commit of the arm64 Linux KPTI modelCatalin Marinas3-0/+1567
2018-04-13qspinlock: Added bounded loop for the pending->locked handoversCatalin Marinas2-37/+73
2018-03-28Initial commit of the queued spinlocks modelCatalin Marinas3-0/+600
2018-03-28check.sh: Updated for a lightweight preemption modelCatalin Marinas1-2/+5
2018-03-28qrwlock: Updated the code path for in-interruptCatalin Marinas1-15/+15
2018-02-19Initial commit of the context_switch() modelCatalin Marinas3-0/+599
2018-02-09Initial commit of the ticketlock modelCatalin Marinas3-0/+231
2018-02-09Initial commit of the qrwlock modelCatalin Marinas3-0/+493
2018-01-04Initial commit of the arm64 ASID allocator specsCatalin Marinas5-0/+1440