Commit graph

9 commits

Author SHA1 Message Date
Adrian Danis
0ecff9f393 unsigned int -> word_t 2015-12-10 10:45:21 +11:00
Adrian Danis
2d61910e0f Rename uint32_t -> word_t in any relevant places 2015-12-10 10:45:20 +11:00
Yanyan Shen
9f2d521979 Make cspace address walking 32/64-bit agnostic 2015-12-10 10:45:19 +11:00
Anna Lyons
a99a10408d SELFOUR-279: rename Wait -> Recv, add wrappers for seL4_Poll and seL4_Wait for notification objects.
This commit deprecates seL4_ReplyWait, removes seL4_NBwait completely,
and changes the return type of seL4_Wait to void (seL4_Wait should be
used for notification objects, and seL4_Recv should be used where
seL4_Wait was used previously for endpoints).
2015-11-20 15:28:18 +11:00
Adrian Danis
8743737dae Use CONST instead of PURE in thread functions
As these functions do not read any global state they fit
within the subset of PURE that can be declared as CONST
2015-10-23 15:02:53 +11:00
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
Anna Lyons
d9802d179f Add seL4_NBWait: non blocking wait for notifications and endpoints. 2015-10-21 13:43:39 +11:00
Adrian Danis
97042a0f07 Introduce 'Notification Binding': a new feature which allows a tcb to be bound to a single asynchronous endpoint. 2015-10-09 15:19:58 +11:00
TrusthworthySystems
91b7da8625 Release snapshot 2014-07-18 05:03:59 +10:00