#
a00c2c16 |
|
17-Sep-2020 |
Curtis Millar <curtis.millar@data61.csiro.au> |
Make kernel log buffer derived from cmake config This removes the explicit CMake configuration for the kernel log buffer and replaces it with a #define that is enabled for the required configurations. Signed-off-by: Curtis Millar <curtis@curtism.me>
|
#
88a7d138 |
|
13-Jul-2020 |
Kent McLeod <Kent.Mcleod@data61.csiro.au> |
KernelBenchmarksTrackUtilisation: Add more stats For each thread also track number of times scheduled, number of kernel entries and amount of cycles spent inside the kernel. Also add core-wide totals for each. Signed-off-by: Kent McLeod <Kent.Mcleod@data61.csiro.au>
|
#
4eccea54 |
|
13-Jul-2020 |
Kent McLeod <Kent.Mcleod@data61.csiro.au> |
KernelBenchmarksTrackUtilisation: Fix for SMP Create per-node global definitions for utilization variables. This enables the tracking to more cleanly work on SMP configurations. As resetting and starting the counters via SysBenchmarkResetLog only updates the counters of the current thread and idle thread on the current node it was not possible to accurately record utilization statistics across multiple nodes. Now each node can have its tracking independently started, stopped and queried. It is possible to add additional syscalls in the future for doing this for all nodes in a single syscall. Signed-off-by: Kent McLeod <Kent.Mcleod@data61.csiro.au>
|
#
512a0200 |
|
19-Mar-2020 |
Qian Ge <qian.ge@data61.csiro.au> |
replacing all ifndef with pargma once All the kernel header files now use pargma once rather than the ifndef, as the pre-processed C files do not change while header files are protected with pargma once. This will also solve any naming issues caused by ifndef.
|
#
79da0792 |
|
01-Mar-2020 |
Gerwin Klein <gerwin.klein@data61.csiro.au> |
Convert license tags to SPDX identifiers This commit also converts our own copyright headers to directly use SPDX, but leaves all other copyright header intact, only adding the SPDX ident. As far as possible this commit also merges multiple Data61 copyright statements/headers into one for consistency.
|
#
0de7fc11 |
|
18-Dec-2019 |
Kent McLeod <Kent.Mcleod@data61.csiro.au> |
Revert "Cache FPU enable state on all platforms" This reverts commit 186180cf309b365b45c162f7a1f5931f0fc05d7c.
|
#
186180cf |
|
11-Jul-2019 |
Curtis Millar <curtis.millar@data61.csiro.au> |
Cache FPU enable state on all platforms This change broadens the caching of the FPU enable/disable bit from arm to all platforms to ensure that on x86 time is not wasted on the fastpath disabling or enabling an already disabled/enabled FPU.
|
#
04e51d40 |
|
27-Nov-2019 |
Curtis Millar <curtis.millar@data61.csiro.au> |
Revert the recent changes to Faster FPU switch These changes need to be reverted until we can properly test the changes with all of our hardware online (currently we cannot test on x86 hardware). This reverts commit a0aeec3b304d16909619bc847197df221c73a0c4. This reverts commit af0fdc82c23f1e7e3f1e568f6987f5afd0d2150a. This reverts commit a190a14ecaae688a6b40dd0a699b8f49c2c0631e.
|
#
e9b90f9f |
|
11-Jul-2019 |
Curtis Millar <curtis.millar@data61.csiro.au> |
Cache FPU enable state on all platforms This change broadens the caching of the FPU enable/disable bit from arm to all platforms to ensure that on x86 time is not wasted on the fastpath disabling or enabling an already disabled/enabled FPU.
|
#
106b893e |
|
23-May-2017 |
Anna Lyons <Anna.Lyons@data61.csiro.au> |
mcs: configurable scheduling context size This allows users to define custom amounts of refills without increasing the scheduling context size system wide. also add libsel4 functions for refill size
|
#
34c1f920 |
|
03-Nov-2016 |
Anna Lyons <Anna.Lyons@data61.csiro.au> |
mcs: add periodic scheduling This commit adds periodic scheduling with sporadic servers.
|
#
71244499 |
|
31-Oct-2016 |
Anna Lyons <Anna.Lyons@data61.csiro.au> |
mcs: tickless scheduler implementation This changes the budget/remaining fields in scheduling contexts to contain timer ticks, not number of abstract sel4ticks. seL4_SchedControl_Configure now takes microseconds, not ticks. This commit is plat-independant - the platform and arch specific timer code follows in later commits.
|
#
952134d1 |
|
27-Oct-2016 |
Anna Lyons <Anna.Lyons@data61.csiro.au> |
mcs: Add a scheduling context object This is the first part of the seL4 MCS. This commit: * adds a scheduling context object. Threads without scheduling context objects cannot be scheduled. * replaces tcbTimeSlice with the scheduling context object * adds seL4_SchedControl caps for each core * adds seL4_SchedControl_Configure which allows users to configure amount of ticks a scheduling context has, and set a core for the scheduling context. * adds seL4_SchedContext_Bind, Unbind and UnbindObject, which allows a tcb to be bound to a scheduling context.
|
#
a6157d5d |
|
18-Jul-2019 |
Sylvain Gauthier <sylvain.gauthier@data61.csiro.au> |
[SMP] Abstracted IRQ indexing to handle PPIs irq_t is now a "virtual" interrupt type that encapsulates the information of the core in case of a private interrupt. There is a couple of macros that need to be defined on the interrupt controller level to translate between virtual and hardware IRQs.
|
#
69339d42 |
|
09-Apr-2019 |
Jasper Lowell <jasper.lowell@data61.csiro.au> |
Boot code: Statically allocate idle thread The idle thread is not managed at user-level and so it can instead be statically allocated. This simplifies the boot code and increments towards being easier to formally verify.
|
#
1c6c06dc |
|
23-Apr-2019 |
Matthew Brecknell <Matthew.Brecknell@data61.csiro.au> |
boot: implement intStateIRQNode as an array It turns out that verifying this is easier than if intStateIRQNode is a pointer that is statically initialised to point to another array.
|
#
570c1a65 |
|
05-Jan-2018 |
Adrian Danis <Adrian.Danis@data61.csiro.au> |
Compile time abstraction for calling getCurrentCPUIndex This defines a CURRENT_CPU_INDEX() macro that resolves to a constant 0 in the absence of SMP, or a call to getCurrentCPUIndex in the presence of SMP. This provides a way to use per-core data structures, without additional guards, in a way that is nearly invisible to verification
|
#
8576758a |
|
06-Nov-2017 |
Anna Lyons <Anna.Lyons@data61.csiro.au> |
Define SchedulerAction_ChooseNewThread as 1 1 is never a valid tcb, and ~0 on x64 results in 0x00000000FFFFFFFF, which could be a valid tcb.
|
#
c6e4cc3e |
|
23-Nov-2017 |
Adrian Danis <Adrian.Danis@data61.csiro.au> |
Correct L2 bitmap size calculation and put it in one place This corrects the calculation of the L2 bitmap size to correctly handle cases where the requested num priorities is not a clean multiple of the wordBits
|
#
ee28936d |
|
18-Jun-2017 |
Hesham Almatary <hesham.almatary@data61.csiro.au> |
SMP: Introduce ENABLE_SMP_SUPPORT - Make it more readable and less confusing compared to the 'CONFIG_MAX_NUM_NODES > 1' check
|
#
40c61e5c |
|
18-Jun-2017 |
Anna Lyons <Anna.Lyons@data61.csiro.au> |
Fix licenses (the rest)
|
#
bb5ecb1b |
|
29-May-2017 |
Anna Lyons <Anna.Lyons@data61.csiro.au> |
SELFOUR-880: add seL4_DebugDumpScheduler - when CONFIG_DEBUG is enabled, track all threads - when CONFIG_PRINTING is enabled, provide seL4_DebugDumpScheduler which allows the user to dump the state of the kernel scheduler.
|
#
0707ae87 |
|
23-Feb-2017 |
amrzar <azarrabi@nicta.com.au> |
Move arch independent functions to generic files and HAVE_FPU config
|
#
ae8f2c99 |
|
23-Feb-2017 |
amrzar <azarrabi@nicta.com.au> |
x86: move current active FPU owner to node state
|
#
323e60a7 |
|
23-Feb-2017 |
amrzar <azarrabi@nicta.com.au> |
x86: define number of restore since switch as node state
|
#
eccaae51 |
|
20-Feb-2017 |
Adrian Danis <Adrian.Danis@data61.csiro.au> |
s/D61/DATA61/ in license headers for consistency
|
#
48d17e1f |
|
16-Jan-2017 |
Hesham Almatary <hesham.almatary@data61.csiro.au> |
ARM/SMP: Prepare for ARM SMP adding stubs Currently building ARM/SMP is broken. This commit: 1- Makes it possible to build ARM/SMP with stubs. Run-time SMP for ARM DOES NOT WORK. 2- Can be a reference for future SMP targets to follow in order to layout/add the minimal required files and functions needed to support SMP. 3- Builds for Sabre only. In order to support other platforms, ipi interrupt ID should be defined in machine.h
|
#
53c6b524 |
|
12-Jan-2017 |
Hesham Almatary <hesham.almatary@data61.csiro.au> |
SMP: Abstract architecture/platform independent parts of smp.h and ipi.h This commit is a re-arrangement of SMP directory structure to make it easier for other architectures/platforms (in general) and ARM (in particular) to add SMP support. * new include/smp directory to act as a centralised container of "shared" architecture-independent SMP headers. This makes it clearer what's needed for other architecture/platform to support SMP. * Each platform can define its own unique ipi.[h|c] that make sense, since ipi implementation is SoC/platform dependent.
|
#
cc685301 |
|
23-Nov-2016 |
Adrian Danis <Adrian.Danis@data61.csiro.au> |
Remove unneeded usages of `VISIBLE` Using `VISIBLE` where it is not needed limits the ability for the compiler to optimize, especially when using whole program optimizations
|
#
7f767494 |
|
15-Nov-2016 |
Adrian Danis <Adrian.Danis@data61.csiro.au> |
Revert SELFOUR-242 This reverts commits 3aee0ab7b3ae5ff5294192526fb00823b49048b5 6b6b965528d16c1e4c946fb920fb95060f84424f a1421832acd19ed5ede71640af82b982708207c2
|
#
a1421832 |
|
15-Feb-2016 |
Anna Lyons <Anna.Lyons@nicta.com.au> |
SELFOUR-242: invert bitfield scheduler & optimise This commit does the following: * invert the bit field scheduler for better cache performance for high priority threads * peeks into the bitfield scheduler to allow fastpath to be leveraged when IPC occurs from lo --> hi priority threads if correct
|
#
63649f26 |
|
19-Oct-2016 |
Adrian Danis <Adrian.Danis@data61.csiro.au> |
Remove arch/machine.h include from statedata.h statedata.h gets included from arch/machine.h, and statedata does not require any of the machine.h definitions. As a result of removing this various other, previously missing, includes need to be added
|
#
b90238d0 |
|
19-Oct-2016 |
Adrian Danis <Adrian.Danis@data61.csiro.au> |
Replace #pragma once with include guards
|
#
3f9eb7c8 |
|
06-Oct-2016 |
amrzar <azarrabi@nicta.com.au> |
SELFOUR-632: implement cores non-architecture dependent structres
|
#
2cbc7123 |
|
28-Sep-2016 |
amrzar <azarrabi@nicta.com.au> |
SELFOUR-630:preliminary booting application processors - update core detection code and Kconfig file - update kernel stack managment so that BSP does not use boot stack before IPI APs - move arch dependant data to a single structure - add cache line size to Kconfig - add cpu indexing and apic id mapping - boot APs to halting state - add guard for kernel stack if there is only one core
|
#
4044e204 |
|
21-Sep-2016 |
Adrian Danis <Adrian.Danis@data61.csiro.au> |
Revert "Merge pull request #358 in SEL4/sel4 from ~AZARRABI/sel4:multicore to master" This reverts commit ce2f666bb811c5e4c779829fcb09d5a189ebcdbb, reversing changes made to dc183f96b81f2344d7d0d910fc430f924eaae940.
|
#
8ffc3531 |
|
21-Sep-2016 |
Adrian Danis <Adrian.Danis@data61.csiro.au> |
Revert "[STYLE_FIX]" This reverts commit d29f743bbcc3acff2f61b40dedb4fe0839db38b8.
|
#
d29f743b |
|
21-Sep-2016 |
Bamboo <bamboo@keg.ertos.in.nicta.com.au> |
[STYLE_FIX]
|
#
fbc071b4 |
|
12-Sep-2016 |
amrzar <azarrabi@nicta.com.au> |
SELFOUR-630:preliminary booting application processors - update core detection code and Kconfig file - update kernel stack managment so that BSP does not use boot stack before IPI APs - move arch dependant data to a single structure - add cache line size to Kconfig - add cpu indexing and apic id mapping - boot APs to halting state - add guard for kernel stack if there is only one core
|
#
16c34811 |
|
31-Jul-2016 |
Hesham Almatary <hesham.almatary@data61.csiro.au> |
SELFOUR-518: User-level log buffer Remove global ksLog and use KS_LOG_PPTR instead Benchmark - Log buffer: use global page table
|
#
c5b6a6a5 |
|
06-Jun-2016 |
Anna Lyons <Anna.Lyons@nicta.com.au> |
Refactor duplicated code in hardware.h One copy to rule them all.
|
#
bbdf7a89 |
|
23-May-2016 |
Adrian Danis <Adrian.Danis@data61.csiro.au> |
Mark tlbLockCount as visible so it is not discarded This variable is referenced in assembler and needs to not get discarded by the optimizer prior to linking.
|
#
b9a7f3c9 |
|
05-May-2016 |
Felix Kam <felix.kam@nicta.com.au> |
Make lockTLBEntry comply with the decompiler lockTLBEntry, an assembly function, had tlb_lock_count as a symbol that needed to be placed sufficiently close to be loaded and stored with offset-from-pc addressing. When assembled, the symbol would turn up between functions, as opposed to within a literal pool (it's a variable, not a constant) or the .bss / data sections. The decompiler doesn't handle that use case, and likely won't. This change turns tlb_lock_count into a C global variable (so that it will be placed in the .bss / data sections), and splits lockTLBEntry into two parts so the critical section will still fit in a 64-byte aligned region, and therefore be guaranteed to live within a single page.
|
#
0ecff9f3 |
|
09-Nov-2015 |
Adrian Danis <Adrian.Danis@nicta.com.au> |
unsigned int -> word_t
|
#
2d61910e |
|
09-Nov-2015 |
Adrian Danis <Adrian.Danis@nicta.com.au> |
Rename uint32_t -> word_t in any relevant places
|
#
62727e30 |
|
15-Jun-2015 |
Stephen Sherratt <stephen.sherratt@nicta.com.au> |
Using bitfields to track for which priorities there exist non-empty ready queues. Background seL4 organizes threads into ready queues, of which there is one for each domain, for each priority level. The ready queue for a given domain/priority combination can be found by indexing the array `ksReadyQueues` with "domain*num_priorities + priority". Current scheduler implementation To find the non-empty ready queue with the maximum priority for the current domain, seL4 iterates through `ksReadyQueues`, starting with the element corresponding to the current domain and maximum possible priority, and decrementing the priority until a non-empty queue is found. This is problematic in cases where the only ready threads have low priorities, as iterating through many elements of an array effectively flushes the cache. Changes in this patch This patch replaces the iteration with a lookup into a table of bitfields per domain. Using bitfields allows the kernel to determine the highest priority level with a non-empty ready queue for the current domain by counting the leading zeroes in bitfields. This removes the negative cache effects of iterating through an array. Implementation details For each domain, a multilevel table of bitfields is maintained which stores the priority levels within that domain for which there exist ready threads. On a 32-bit architecture, the top level of the table is a 32-bit bitfield where if the ith bit is set, there is at least 1 priority level in [i*32..i*32+31] with a non-empty ready queue. The positions of bits in this bitfield are used as indices into the second level table, which is an array of 32-bit bitfields. The ith bit of the jth bitfield in this array set to 1, indicates that priority level j*32+i has a non-empty ready queue.
|
#
91b7da86 |
|
17-Jul-2014 |
TrusthworthySystems <gatekeeper@sel4.systems> |
Release snapshot
|