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
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
On the MCS kernel, Arch_migrateTCB is called in multiple places.
This commit moves the common code that is required when migrating a TCB
to a top level function to reduce boiler plate.
- 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.
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
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.
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
This will update TCB invocations to consider multicore environment, this may include:
- adds the affinity invocation to transfer TCB between different cores and update TCB structure for core ID
- checking the thread/core state before performing TCB operation, e.g. deleting the runnable TCB, etc
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
- 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
- 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
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.
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.
