#
036ffc18 |
|
08-Sep-2020 |
Mitchell Buckley <mitchell.buckley@data61.csiro.au> |
mcs: update commitTime It is possible for consumed time to be larger than domain time. Signed-off-by: Mitchell Buckley <mitchell.buckley@data61.csiro.au>
|
#
4522d895 |
|
03-Sep-2020 |
Matthew Brecknell <Matthew.Brecknell@data61.csiro.au> |
mcs: return pointer from `refill_head` and others A previous commit produced some build errors, since it converted the `REFILL_HEAD` and `REFILL_TAIL` macros to functions returning `refill_t`, and the results were used as lvalues. This commit returns pointers instead, and also converts `REFILL_INDEX` to a function. Signed-off-by: Matthew Brecknell <Matthew.Brecknell@data61.csiro.au>
|
#
0fbf2f7d |
|
24-Jul-2019 |
Curtis Millar <curtis.millar@data61.csiro.au> |
mcs: Don't pass capacity through calls The capacity does not need to be passed as an argument to refill_check_budget as all information that it was being used for can be dertermined from the usage directly. Signed-off-by: Curtis Millar <curtis.millar@data61.csiro.au>
|
#
d5d54a0d |
|
21-Nov-2019 |
Curtis Millar <curtis.millar@data61.csiro.au> |
introduce isStopped and change isBlocked This changes the semantics if `isBlocked` to not include the 'inactive' state when it returns true. The old semantics for isBlocked are provided by `isStopped`. Signed-off-by: Curtis Millar <curtis.millar@data61.csiro.au>
|
#
512a0200 |
|
19-Mar-2020 |
Qian Ge <qian.ge@data61.csiro.au> |
replacing all ifndef with pargma once All the kernel header files now use pargma once rather than the ifndef, as the pre-processed C files do not change while header files are protected with pargma once. This will also solve any naming issues caused by ifndef.
|
#
79da0792 |
|
01-Mar-2020 |
Gerwin Klein <gerwin.klein@data61.csiro.au> |
Convert license tags to SPDX identifiers This commit also converts our own copyright headers to directly use SPDX, but leaves all other copyright header intact, only adding the SPDX ident. As far as possible this commit also merges multiple Data61 copyright statements/headers into one for consistency.
|
#
c25e5445 |
|
22-Aug-2019 |
Curtis Millar <curtis.millar@data61.csiro.au> |
mcs: Don't rollback time when not rescheduling This allows ksCurTime to be monotonically increasing making proofs much easier to construct.
|
#
b33d4680 |
|
09-May-2019 |
Anna Lyons <Anna.Lyons@data61.csiro.au> |
mcs: Avoid charging invalid scheduling contexts ChargeBudget can be called after a preemption, but the preemption may have deleted the scheduling context. Do not charge scheduling contexts that have been deleted (check scRefillMax).
|
#
86e50d07 |
|
09-May-2019 |
Anna Lyons <Anna.Lyons@data61.csiro.au> |
mcs: Avoid missing a timer tick Preemption can be via the timer interrupt. In this case we need to update the timestamp so we can reprogram the timer for the next timeout and guarantee it is in the future, otherwise we will end up setting a timeout in the past.
|
#
b358a1c5 |
|
09-May-2019 |
Anna Lyons <Anna.Lyons@data61.csiro.au> |
trivial: move isSchedulable to header
|
#
257a62c7 |
|
18-Mar-2019 |
Anna Lyons <Anna.Lyons@data61.csiro.au> |
mcs: explicitly use ksCurSC - in refill_[budget|split]_check. - This simplifies the code and the proofs.
|
#
483f0ae2 |
|
07-Jun-2018 |
Anna Lyons <Anna.Lyons@data61.csiro.au> |
mcs: SchedControlConfigure: charge correct core Previously this code would incorrectly call chargeBudget twice, where it was intended to be charging a specific core.
|
#
a38e62f2 |
|
28-Feb-2018 |
Anna Lyons <Anna.Lyons@data61.csiro.au> |
mcs: timeout exceptions - Add seL4_TCB_SetTimeoutEndpoint - implement timeout exceptions
|
#
96798066 |
|
17-May-2017 |
Anna Lyons <Anna.Lyons@data61.csiro.au> |
mcs: avoid rolling back time if acted upon Otherwise strange things can happen where threads are in the future.
|
#
9253704d |
|
26-Apr-2017 |
Anna Lyons <Anna.Lyons@data61.csiro.au> |
mcs: update refills based on spec This is a list of fixes that came up while working on the verification spec for the mcs changes. - trigger a timer tick if we are unable to split a refill due to the refill list being full. - make refill_ordered more useful - pull the thread out of the scheduler before updating it - simplify refill logic at verifications request - Add unused to refill_sum - Don't refill_split_check if consumed is empty - sched_control: fix double increment bug - sched-control: charge before reconfiguring ksCurSC - Charge round robin threads differently Sporadic server refill rules do not behave correctly for round robin threads, instead, change the logic. Round robin threads have 2 refills: current and next.
|
#
554f812d |
|
08-Nov-2016 |
Anna Lyons <Anna.Lyons@data61.csiro.au> |
mcs: scheduling context donation over ipc After this commit, threads blocked on an endpoint can recieve a scheduling context from the thread that wakes the blocked thread.
|
#
34c1f920 |
|
03-Nov-2016 |
Anna Lyons <Anna.Lyons@data61.csiro.au> |
mcs: add periodic scheduling This commit adds periodic scheduling with sporadic servers.
|
#
71244499 |
|
31-Oct-2016 |
Anna Lyons <Anna.Lyons@data61.csiro.au> |
mcs: tickless scheduler implementation This changes the budget/remaining fields in scheduling contexts to contain timer ticks, not number of abstract sel4ticks. seL4_SchedControl_Configure now takes microseconds, not ticks. This commit is plat-independant - the platform and arch specific timer code follows in later commits.
|
#
7c1a7053 |
|
31-Jan-2018 |
Adrian Danis <Adrian.Danis@data61.csiro.au> |
SELFOUR-1198: correct restart PC Fixes a case where a thread can go from Running->Inactive->Restart and use a restart PC that is out of date. An out of date restart PC occurs when a thread was transitioned to running after being in a blocked state, but was never scheduled and so did not execute the traps code that updates the restart PC. A 'more correct' fix would be to update the restart PC when a thread is first transitioned to Running, but this results in lots of unnecessary update as * Frequently immediately schedule a thread after it is transitioned to running, making the update to restart PC completely redundant as it gets immediately overwritten * Rarely suspend threads making all the updates a 'high' cost for fixing an infrequent operation As a result this solution lazily fixes the restart PC only when we enter a state where we might need a correct restart PC, which currently in the kernel is only when we go from Running->Inactive, which can only happen in `suspend`
|
#
d0930f67 |
|
18-Mar-2019 |
Anna Lyons <Anna.Lyons@data61.csiro.au> |
style: consistently attach return type Add attach-return-type to astyle
|
#
3df00ea4 |
|
22-Apr-2018 |
Thibaut Perami <thibaut.perami@data61.csiro.au> |
SELFOUR-6: Add GrantReply to the rights system. GrantReply is a new access right added to endpoint capabilities, which allows seL4_Call to be used on those capabilities (specifically, it allows reply caps *only* to be granted across endpoints). Prior to the addition of GrantReply, endpoint capabilities required the Grant access right, which allowed any arbitrary capabilitiy to be transferred over an endpoint. Using GrantReply, systems can now be constructed where threads using seL4_Call over an endpoint do not need to be in the same security subsystem.
|
#
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
|
#
8639dbca |
|
06-Nov-2017 |
Adrian Danis <Adrian.Danis@data61.csiro.au> |
Abstractly declare a threads registers have changed This removes an #ifdef for x86-64 that was in generic code by declaring the generic mechanism that is being used as an Arch_ function
|
#
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.
|
#
780b13da |
|
23-Nov-2017 |
Adrian Danis <Adrian.Danis@data61.csiro.au> |
Provide isHighestPrio helper
|
#
d40868b9 |
|
23-Nov-2017 |
Adrian Danis <Adrian.Danis@data61.csiro.au> |
Invert priority order of scheduler bitmap Provides better cache performance for high priority threads
|
#
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
|
#
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
|
#
cc685301 |
|
23-Nov-2016 |
Adrian Danis <Adrian.Danis@data61.csiro.au> |
Remove unneeded usages of `VISIBLE` Using `VISIBLE` where it is not needed limits the ability for the compiler to optimize, especially when using whole program optimizations
|
#
7f767494 |
|
15-Nov-2016 |
Adrian Danis <Adrian.Danis@data61.csiro.au> |
Revert SELFOUR-242 This reverts commits 3aee0ab7b3ae5ff5294192526fb00823b49048b5 6b6b965528d16c1e4c946fb920fb95060f84424f a1421832acd19ed5ede71640af82b982708207c2
|
#
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
|
#
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.
|
#
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.
|
#
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).
|
#
8743737d |
|
22-Oct-2015 |
Adrian Danis <Adrian.Danis@nicta.com.au> |
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
|
#
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.
|
#
91b7da86 |
|
17-Jul-2014 |
TrusthworthySystems <gatekeeper@sel4.systems> |
Release snapshot
|