Configuring standalone kernel builds (such as those used by verification)
has been done in a completely different way to how the kernel is
configured for project builds. As the kernel gains additional options
it becomes difficult to maintain standalone kernel builds without
tediously exporting these additional options, such tedious work is
what autoconf.h is meant to address
The new configuration strategy requires a include/plat/PLAT/autoconf.h
file to exist for any platform that wants to hae standalone builds
performed on it. This configuration also becomes the *verified*
configuration, and makes it clear for projects to build the kernel
in the verified configuration.
Create new function "clz" which invokes __builtin_clz
Tell the C parser to not try translate it (DONT_TRANSLATE), but instead
to trust the spec we provide (FNSPEC+MODIFIES).
Squashed the fix by Anna Lyons:
rearrange CLZ in util.h and s/__builtin__clz/__builtin_clz/
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.
IA32 is 32bit version of the x86 architecture. Whilst only IA32
is supported, much of the code is generic x86. Using a generic
x86 architecture will aid in future 64bit support
