#
4ee1f90a |
|
14-Aug-2020 |
Miki Tanaka <miki.tanaka@data61.csiro.au> |
mcs: add tcb argument to reply_unlink reply_unlink takes a reply and remove the link between that reply and its tcb. This link always exists at the call site and the tcb information is always avaialble, or can be made available. This commit adds this tcb as an extra argument to aid varification. Signed-off-by: Miki Tanaka <miki.tanaka@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>
|
#
b181184d |
|
01-Sep-2020 |
Edward Pierzchalski <ed.pierzchalski@data61.csiro.au> |
mcs: change REFILL_HEAD, REFILL_TAIL to functions SimplExportAndRefine can't handle the level of pointer arithmetic being performed by `REFILL_INDEX` if it's literally inlined into a function, however it *can* handle that arithmetic if it's in a separate function. Signed-off-by: Edward Pierzchalski <ed.pierzchalski@data61.csiro.au>
|
#
4bd328f8 |
|
23-Jul-2020 |
Kent McLeod <Kent.Mcleod@data61.csiro.au> |
mcs: Guard handleTimeout for RoundRobin threads RoundRobin threads cannot run out of budget and so cannot generate timeout faults. They instead get appended to the end of the scheduler queue. Signed-off-by: Kent McLeod <Kent.Mcleod@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>
|
#
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.
|
#
d09914aa |
|
04-Jul-2017 |
Anna Lyons <Anna.Lyons@data61.csiro.au> |
kernel: attempt direct switch on set prio Prior to this commit the kernel would always trigger a full reschedule on setPriority. This change allows the kernel to attempt a direct switch, avoiding invoking the scheduler. - Move location of setPriority call to after any cap deletion This makes the proof easier as setPriority now changes ksSchedulerAction, which is required to be ResumeCurrentThread or ChooseNewThread by the cap delete functions. - Update to attempt direct switch on set prio.
|
#
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.
|
#
acdf0be5 |
|
09-May-2019 |
Anna Lyons <Anna.Lyons@data61.csiro.au> |
mcs: Fix potential crash on preemption Preemption can be triggered due to a revoke operation, which may have deleted one or both of the current thread and current scheduling context. Don't manipulate the current thread if it is no longer valid and just charge the SC iff it is valid and the thread is not. This was discovered during verification.
|
#
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).
|
#
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.
|
#
52dd8f09 |
|
30-Apr-2019 |
Anna Lyons <Anna.Lyons@data61.csiro.au> |
mcs: Avoid removing the SC of the current thread If the scheduling context is changed on the currently running thread this causes issues if the operation triggers a preemption. This change makes the proofs easier, and also makes sense for the api, as users wishing to suspend the current thread should just use Suspend.
|
#
f1113460 |
|
05-Feb-2019 |
Anna Lyons <Anna.Lyons@data61.csiro.au> |
mcs: Fix setPriority When setting a thread priority, we need to check if it is in the scheduler before putting it back in the scheduler, otherwise we do not know enough about the scheduling context to know that the thread is active.
|
#
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.
|
#
f103ac22 |
|
30-Nov-2017 |
Anna Lyons <Anna.Lyons@data61.csiro.au> |
mcs: Refactor replies to solve revoke problems Before this change, we set the replyObject in the thread state on recv with no back pointer such that stray pointers would be left in the thread state when a reply object was completed. The new semantics are clearer and fix this problem by doing the following: - tcb->tcbReply is removed and the thread state field is always used, this was unneccessary duplication previously - the thread state value is set to the reply object only when the thread is in BlockedOnReply or BlockedOnRecv - the reply contains a back pointer, replyTCB, which points to that thread - if a thread has its reply removed, it must be set to ThreadState_Inactive. - deletion is easy in the blockedOnRecv case, we just unlink the reply and the tcb. - deletion is complicated for blockedOnReply. If we are deleing a tcb, we remove the actual reply object and the call chain is broken. If we are deleting a reply, we maintain the call chain by moving the tcb to the next reply. - we refactor the reply object interface to solve the above. * reply_clear: removes the reply from any connections (tcb, sc) * reply_unlink: just unlinks the tcb and reply, and sets the thread state to inactive * reply_remove: removes the reply from the call chain * reply_remove_tcb: removes the exact reply that a tcb is bound to, as we are removing that tcb. Breaks the call chain.
|
#
2329cd81 |
|
14-Mar-2017 |
Anna Lyons <Anna.Lyons@data61.csiro.au> |
mcs: add seL4_SchedContext_YieldTo Implement seL4_SchedContext_YieldTo, which allows users to manipulate the scheduling queues up to their MCP and can be used for user level scheduling.
|
#
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.
|
#
e04cba09 |
|
22-Nov-2016 |
Anna Lyons <Anna.Lyons@data61.csiro.au> |
mcs: update to build on SMP Before this commit SMP + MCS did not build.
|
#
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.
|
#
5fe1890a |
|
06-Nov-2016 |
Anna Lyons <Anna.Lyons@data61.csiro.au> |
mcs: order EP and NTFN queues Previously IPC signal queues were FIFO, as of this change they are ordered by priority (FIFO for same prio threads).
|
#
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.
|
#
952134d1 |
|
27-Oct-2016 |
Anna Lyons <Anna.Lyons@data61.csiro.au> |
mcs: Add a scheduling context object This is the first part of the seL4 MCS. This commit: * adds a scheduling context object. Threads without scheduling context objects cannot be scheduled. * replaces tcbTimeSlice with the scheduling context object * adds seL4_SchedControl caps for each core * adds seL4_SchedControl_Configure which allows users to configure amount of ticks a scheduling context has, and set a core for the scheduling context. * adds seL4_SchedContext_Bind, Unbind and UnbindObject, which allows a tcb to be bound to a scheduling context.
|
#
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`
|
#
306453e3 |
|
18-Mar-2019 |
Anna Lyons <Anna.Lyons@data61.csiro.au> |
style: set min-conditional-indent to 0 Given we use braces all the time conditional indents do not make code cleaner.
|
#
d0930f67 |
|
18-Mar-2019 |
Anna Lyons <Anna.Lyons@data61.csiro.au> |
style: consistently attach return type Add attach-return-type to astyle
|
#
761006e0 |
|
18-Mar-2019 |
Anna Lyons <Anna.Lyons@data61.csiro.au> |
style: consistently align pointer with name Run astyle with align-pointer=name
|
#
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.
|
#
cfcf95c7 |
|
09-Nov-2018 |
Anna Lyons <Anna.Lyons@data61.csiro.au> |
x86-vtx: call timer tick in VM threads x86 virtualisation adds an extra runnable state which requires the timer tick to be executed. Prior to this change threads running as VMs on x86 would not be preempted by the round-robin scheduler.
|
#
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
|