History log of /seL4-l4v-10.1.1/seL4/src/kernel/thread.c
Revision Date Author Comments
# 5505266a 03-Apr-2018 Adrian Danis <Adrian.Danis@data61.csiro.au>

Remove irrelavant changes from riscv commit to non riscv arch code


# 83ba0847 20-Feb-2018 Hesham Almatary <hesham.almatary@unsw.edu.au>

[SELFOUR-1156] RISC-V Port

Experimental release that supports both RV32 and RV64


# a0ec0358 06-Nov-2016 Adrian Danis <Adrian.Danis@data61.csiro.au>

SELFOUR-707: always reschedule on setPriority

This fixes a bug where the highest prio thread would not be scheduled
immediately on setPriority by always rescheduling on setPriority if the
target is runnable. It's the most basic fix for verification.


# a32264bf 27-Nov-2017 Bamboo <bamboo@keg.ertos.in.nicta.com.au>

[STYLE_FIX]


# 8028066a 23-Nov-2017 Adrian Danis <Adrian.Danis@data61.csiro.au>

ksSchedulerAction contains candidate thread instead of target thread

Instead of switching to the thread contained in `ksSchedulerAction` on a `schedule` we
instead decide between the 'candidate' contained in `ksSchedulerAction`, the current thread
or potentially neither if the candidate is deemed invalid and the current thread is blocked.

A consequence of this change is that it is no longer meaningful to have a distinction between
`switchIfRequiredTo` and `attemptSwitchTo`. Now both these cases simply identify a candidate,
which may or may not be picked in `schedule`. Part of the distinction of `switchIfRequiredTo`
was to not avoid switching if possible when performing notifications. This is now handled by
prefering the current thread over the candidate if the current thread has not blocked.

This change is largely semantic preserving overall, with the exception of non-blocking
synchronous sends now acting like notifications and also preferring to resume running the
current thread.

The motivation for this change was to make it much easier for verification to show
correspondence between the fastpath changes introduced in the previous commit and the
slowpath scheduler.


# a2409b98 23-Nov-2017 Adrian Danis <Adrian.Danis@data61.csiro.au>

getHighestPrio calculation as a wrapper

Moves the logic from chooseThread into a dedicated helper function


# 57fa0e0f 07-Aug-2017 Hesham Almatary <hesham.almatary@data61.csiro.au>

Share linker.h between architectures


# 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


# b861f284 25-Apr-2017 Adrian Danis <Adrian.Danis@data61.csiro.au>

Move isRunnable from thread.c to thread.h

This helper function is useful beyond just thread.c


# ddeb9783 26-Jan-2017 Adrian Danis <Adrian.Danis@data61.csiro.au>

Simplify conditional

The original conditional is correct due to `seL4_Fault_NullFault` being `0`,
but it is unnecessarily obtuse and generates a warning by some compilers

Closes #57


# b827ad37 15-Jul-2016 Anna Lyons <Anna.Lyons@nicta.com.au>

SELFOUR-413: refactor libsel4 fault API

This is a *breaking API change*

This commit:

* makes seL4_Fault_tag_t common between the kernel and libsel4
* deprecates the existing functions from sel4/messages.h includes
* introduces a new fault API in sel4/faults.h and
* sel4/sel4_arch/faults.h
* deprecates seL4_GetTag(), as the function did not work without
the user calling seL4_SetTag() first (seL4_MessageInfo is passed
in registers and not set in the IPC buffer)
* removes previously deprecated functions (deprecated prior to 3.0.0)
* updates the seL4 manual to reflect the changes


# 7f767494 15-Nov-2016 Adrian Danis <Adrian.Danis@data61.csiro.au>

Revert SELFOUR-242

This reverts commits
3aee0ab7b3ae5ff5294192526fb00823b49048b5
6b6b965528d16c1e4c946fb920fb95060f84424f
a1421832acd19ed5ede71640af82b982708207c2


# 3aee0ab7 14-Nov-2016 Bamboo <bamboo@keg.ertos.in.nicta.com.au>

[STYLE_FIX]


# 6b6b9655 14-May-2016 Rafal Kolanski <rafal.kolanski@nicta.com.au>

SELFOUR-242: port fastpath test to slow path (possibleSwitchTo)

Unless the tests match directly, the fastpath proof becomes hideous.
Upside to this is that slow path now skips scheduler enqueue only to
dequeue the same thread a moment later.


# 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


# 13ad834a 15-Sep-2016 Thomas Sewell <Thomas.Sewell@nicta.com.au>

Generated bitfield proofs: use hrs_mem_update.

This is a technical change to the proof mode of the bitfield
generator included in the seL4 source.

The postconditions of the generated specifications of the
*_ptr_set and *_ptr_new functions now describe the entire new
heap via (new_heap = hrs_mem_update (...) old_heap).
Previously they described the contents of various projections
of the heap, which is less precise.


# 25bb9437 24-Oct-2016 amrzar <azarrabi@nicta.com.au>

SELFOUR-635: support for TCB operations
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


# 7fbde1bb 14-Jun-2016 Adrian Danis <Adrian.Danis@data61.csiro.au>

SELFOUR-287: 32-bit vt-x implementation

This is an implementation of vt-x for x86 kernels running in
ia32 mode.


# 3f9eb7c8 06-Oct-2016 amrzar <azarrabi@nicta.com.au>

SELFOUR-632: implement cores non-architecture dependent structres


# 7336303b 08-Jun-2016 Anna Lyons <Anna.Lyons@nicta.com.au>

SELFOUR-276: Add MCP field to threads.

Where MCP = Maximum Controlled Priority

This commit adds:

* seL4_TCB_SetMCPriority

and changes the arguments to

* seL4_TCB_Configure

As of this commit, a thread cannot create or set a threads
priority (including itself) above its mcp. Previously the kernel
did this check against a threads priority, which prevented a thread
from setting it's own priority down and then up again.


# 09358f9b 23-Jun-2016 Hesham Almatary <Hesham.Almatary@nicta.com.au>

SELFOUR-448 Benchmark: Track thread's CPU utilisation time


# e61a1056 03-Feb-2016 Adrian Danis <Adrian.Danis@nicta.com.au>

SELFOUR-56: Remove diminish rights from IPC

Diminish rights were to prevent a user from sending a writeable
cap over a read only endpoint. It turns out this 'security' can
be worked around without difficulty (by putting caps in a cnode
and sending the cnode) making the current diminish rights
implementation functionally useless.

Removing diminish rights has the benefit of simplifying all the
IPC paths.


# d93699c9 04-Jan-2016 Anna Lyons <Anna.Lyons@nicta.com.au>

SELFOUR-114: remove duplication of seL4_MessageInfo_t, adjust naming to avoid cparser mangling


# 938d5be0 16-Dec-2015 Matthew Fernandez <matthew.fernandez@nicta.com.au>

Remove CLZ indirection via the CLZL macro.


# 0ecff9f3 09-Nov-2015 Adrian Danis <Adrian.Danis@nicta.com.au>

unsigned int -> word_t


# e3e9780a 28-Jun-2015 Adrian Danis <Adrian.Danis@nicta.com.au>

Rename CTZ and CLZ functions to long variants, change parameters from uint32_t to word_t to make compatible between 32 and 64-bit


# a99a1040 09-Nov-2015 Anna Lyons <Anna.Lyons@nicta.com.au>

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).


# 54603123 19-Oct-2015 Anna Lyons <Anna.Lyons@nicta.com.au>

SELFOUR-317: rename async endpoint to notification object, and other
fallout.


# 947135a7 16-Oct-2015 Rafal Kolanski <rafal.kolanski@nicta.com.au>

chooseThread: favour else clause over explicit return

(easier proofs)


# 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.


# d9802d17 08-Oct-2015 Anna Lyons <Anna.Lyons@nicta.com.au>

Add seL4_NBWait: non blocking wait for notifications and endpoints.


# 97042a0f 17-Jul-2014 Adrian Danis <Adrian.Danis@nicta.com.au>

Introduce 'Notification Binding': a new feature which allows a tcb to be bound to a single asynchronous endpoint.


# d0525de6 14-May-2015 Thomas Sewell <Thomas.Sewell@nicta.com.au>

Strengthen doReplyTransfer->cteDeleteOne assertion.


# b0e9e468 26-Apr-2015 Thomas Sewell <Thomas.Sewell@nicta.com.au>

Ghost assertions for cteDeleteOne.


# 91b7da86 17-Jul-2014 TrusthworthySystems <gatekeeper@sel4.systems>

Release snapshot