seL4/include
Stephen Sherratt 62727e30a2 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.
2015-10-21 18:52:44 +11:00
..
api Add seL4_NBWait: non blocking wait for notifications and endpoints. 2015-10-21 13:43:39 +11:00
arch Added a wordRadix constant to x86 kernel. 2015-10-21 18:33:16 +11:00
fastpath Refactor ARM and ia32 fastpath to use a common code base 2015-08-21 08:34:08 +10:00
kernel Using bitfields to track for which priorities there exist non-empty ready queues. 2015-10-21 18:52:44 +11:00
machine generate warnings for incorrect format strings for kprintf, bring stdint.h 2015-09-30 12:31:39 +10:00
model Using bitfields to track for which priorities there exist non-empty ready queues. 2015-10-21 18:52:44 +11:00
object Add seL4_NBWait: non blocking wait for notifications and endpoints. 2015-10-21 13:43:39 +11:00
plat Removed CONFIG_BENCHMARK config option. All checks for '#ifdef CONFIG_BENCHMARK' replaced with '#if CONFIG_MAX_NUM_TRACE_POINTS > 0'. 2015-09-03 11:39:31 +10:00
api.h Release snapshot 2014-07-18 05:03:59 +10:00
assert.h Release snapshot 2014-07-18 05:03:59 +10:00
basic_types.h split the types header into basic and compound to resolve circular dependencies 2015-04-15 11:57:08 +10:00
benchmark.h Trivial: style 2015-09-08 12:46:09 +10:00
bootinfo.h ia32: Large commit that implements PAE paging for x86 2015-01-28 12:11:51 +11:00
compound_types.h split the types header into basic and compound to resolve circular dependencies 2015-04-15 11:57:08 +10:00
config.h Removed CONFIG_BENCHMARK config option. All checks for '#ifdef CONFIG_BENCHMARK' replaced with '#if CONFIG_MAX_NUM_TRACE_POINTS > 0'. 2015-09-03 11:39:31 +10:00
machine.h Release snapshot 2014-07-18 05:03:59 +10:00
Makefile Release snapshot 2014-07-18 05:03:59 +10:00
object.h Release snapshot 2014-07-18 05:03:59 +10:00
stdarg.h Release snapshot 2014-07-18 05:03:59 +10:00
stdint.h generate warnings for incorrect format strings for kprintf, bring stdint.h 2015-09-30 12:31:39 +10:00
string.h Add ability to set a human readable thread name when running kernel in debug mode 2015-05-14 09:32:58 +10:00
types.h ia32: added the option to disable prefetchers 2015-04-15 14:38:55 +10:00
util.h ia32: Ensure multiboot structs are packed 2015-05-28 12:09:12 +10:00