#
0c32e252 |
|
27-Aug-2020 |
Sylvain Gauthier <sylvain.gauthier@data61.csiro.au> |
fix TCB_PTR_DEBUG_PTR debug macro The base pointer is wrong, and it creates some nasty corruption down the line (only affects debug builds). Signed-off-by: Sylvain Gauthier <sylvain.gauthier@data61.csiro.au>
|
#
15e615ad |
|
21-Jul-2020 |
Kent McLeod <Kent.Mcleod@data61.csiro.au> |
tcb_t: Add ascii diagram of tcb object layout Now that debug_tcb_t is also located in a tcb object, add a diagram for clarity. Signed-off-by: Kent McLeod <Kent.Mcleod@data61.csiro.au>
|
#
9d9bb994 |
|
16-Jul-2020 |
Kent McLeod <Kent.Mcleod@data61.csiro.au> |
debug: create debug_tcb_t struct Special debug variables that were previously stored at the end of the tcb_t struct often cause the struct to get too large for the power-of-2 sized untyped object definition. This change moves these variables into a new structure named debug_tcb_t that is located between the TCB CNode and the tcb_t struct within a tcb kernel object. Because tcb_t needs to be stored on a power-of-2 aligned boundary and the TCB CNode only contains < 5 slots, there is easily > 512 bytes of unused data in every tcb object. The kernel verification needs to be sure that objects don't overlap in memory and so this space can't be easily used in a release build at the moment, but for debug configurations using it shouldn't be an issue. Signed-off-by: Kent McLeod <Kent.Mcleod@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.
|
#
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
|
#
c405ef53 |
|
28-Feb-2018 |
Anna Lyons <Anna.Lyons@data61.csiro.au> |
mcs: install fault endpoint into tcb cnode - seL4_TCB_Configure no longer takes a fault endpoint. - seL4_TCB_SetSpace takes a cap in the callers cspace for the fault endpoint, not the target tcbs. - seL4_TCB_SetSchedParams now also takes a fault endpoint as above. This change installs the fault endpoint cap into the tcb cnode first validating it. This means either of the functions that set it will now return an error if the cap is not either a null cap or an endpoint with send and grant rights. Significantly, the cap passed to the function should be in the callers cspace, not the target tcbs.
|
#
106b893e |
|
23-May-2017 |
Anna Lyons <Anna.Lyons@data61.csiro.au> |
mcs: configurable scheduling context size This allows users to define custom amounts of refills without increasing the scheduling context size system wide. also add libsel4 functions for refill size
|
#
a22cb3d1 |
|
23-Nov-2016 |
Anna Lyons <Anna.Lyons@data61.csiro.au> |
mcs: associate scheduling context + ntfn This commit allows scheduling contexts to be bound to notification objects. When a passive server receives a notification it will receive the scheduling context from the notification. When the server blocks the scheduling context is returned.
|
#
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.
|
#
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.
|
#
01c7e62c |
|
28-Mar-2019 |
Curtis Millar <curtis.millar@data61.csiro.au> |
Update size comments to reflect the size better This changes the comments regarding the size of the TCB to be more generally accurate to help manually determine the size of the TCB for different configurations.
|
#
142bf9b1 |
|
21-Mar-2019 |
Sylvain Gauthier <sylvain.gauthier@data61.csiro.au> |
More standard constant name, moved ASID constants to arch generic files
|
#
f6e5e218 |
|
20-Mar-2019 |
Kent McLeod <Kent.Mcleod@data61.csiro.au> |
Remove symlinked libsel4 files from include dir These files can be included normally using libsel4 include paths. This removes situations where the same file is available under different include paths due to symlinking into different directory structures.
|
#
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
|
#
8bf7c55d |
|
05-Dec-2018 |
Edward Pierzchalski <ed.pierzchalski@data61.csiro.au> |
Dedup user_data and user_data_device definitions. These are reasonably expected to exist on every platform by the UMM type generator. They also had identical definitions, so we consolidate them.
|
#
7641e438 |
|
06-Mar-2018 |
Adrian Danis <Adrian.Danis@data61.csiro.au> |
Refactor logic for cap revocability in cteInsert into new function with arch case Revocability of a cap, with respect to its parent, is a general property on caps and makes sense to be abstracted. This allows for the addition of an arch case without further complicating the cteInsert function itself.
|
#
b942a504 |
|
26-Mar-2018 |
Bruce Mitchener <bruce.mitchener@gmail.com> |
Fix trivial comment typos.
|
#
bce62b4e |
|
21-Mar-2018 |
Adrian Danis <Adrian.Danis@data61.csiro.au> |
Check that TCB object is not larger than necessary
|
#
a2a2d9b9 |
|
20-Mar-2018 |
Adrian Danis <Adrian.Danis@data61.csiro.au> |
Define tcb_t as half the TCB object size A TCB object has two objects inside it, the cnode object and the 'actual tcb object'. For simplicity of verification we would like the tcb_t portion of the object to also be size aligned instead of just just being offset by the size of the cnode.
|
#
f5abc878 |
|
20-Mar-2018 |
Adrian Danis <Adrian.Danis@data61.csiro.au> |
Rename TCB_SIZE_BITS to TCB_CNODE_SIZE_BITS This definition is used as the size of the cnode portion of the TCB object (and not the tcb_t) portion and so this provides a much less confusing name.
|
#
d2644e8a |
|
26-Oct-2017 |
Adrian Danis <Adrian.Danis@data61.csiro.au> |
Declare and check IPC buffer size Adds a named constant of the IPC buffer size bits that can be used when checking the size/alignment of an IPC buffer. This constant has a compile time assertion to ensure it corresponds to the actual IPC buffer
|
#
18db5302 |
|
24-Oct-2017 |
Adrian Danis <Adrian.Danis@data61.csiro.au> |
Abstract zombie word radixes Zombie caps perform bit packing that relied on the log2(wordBits), which was being hard coded to 5. Whilst 5 is the correct value on 32-bit platforms, it is incorrect on 64-bit ones. This changes the previously hardcoded 5 to be the, already existing, wordRadix definition.
|
#
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
|
#
8c7081c9 |
|
31-May-2017 |
Anna Lyons <Anna.Lyons@data61.csiro.au> |
trivial: use BIT in compile asserts in structures.h
|
#
bb5ecb1b |
|
29-May-2017 |
Anna Lyons <Anna.Lyons@data61.csiro.au> |
SELFOUR-880: add seL4_DebugDumpScheduler - when CONFIG_DEBUG is enabled, track all threads - when CONFIG_PRINTING is enabled, provide seL4_DebugDumpScheduler which allows the user to dump the state of the kernel scheduler.
|
#
9ca253a3 |
|
07-May-2017 |
Anna Lyons <Anna.Lyons@data61.csiro.au> |
SELFOUR-879: expose index and entry constants
|
#
2f866d91 |
|
10-Jan-2017 |
Hesham Almatary <hesham.almatary@data61.csiro.au> |
Benchmark: Define benchmark_util_t in a separate file to avoid circular dependency
|
#
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
|
#
bdf10bb4 |
|
22-Nov-2016 |
Adrian Danis <Adrian.Danis@data61.csiro.au> |
Refactor includes so trace point support builds benchmark.h requires a definition of KS_LOG_PPTR, but its previous placement in machine.h resulted in a circular include. This commit factors out KS_LOG_PPTR and related definitions to a separate header, creates the corresponding header for x86, and prevents circular includes in the x86 builds
|
#
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.
|
#
f050e6a9 |
|
20-Oct-2016 |
amrzar <azarrabi@nicta.com.au> |
implement layout of ipi interrupt handling
|
#
5f7fa2fc |
|
19-Oct-2016 |
Hesham Almatary <hesham.almatary@data61.csiro.au> |
Benchmark: Pack arch-independent benchmark-related files into separate directories
|
#
2d462d4a |
|
17-Oct-2016 |
amrzar <azarrabi@nicta.com.au> |
add basic api for setting affinity
|
#
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.
|
#
d97603bd |
|
14-Jul-2016 |
Hesham Almatary <hesham.almatary@data61.csiro.au> |
SELFOUR-566: Decouble seL4_DebugNameThread from CONFIG_PRINTING
|
#
09358f9b |
|
23-Jun-2016 |
Hesham Almatary <Hesham.Almatary@nicta.com.au> |
SELFOUR-448 Benchmark: Track thread's CPU utilisation time
|
#
8541b873 |
|
20-Jun-2016 |
Hesham Almatary <Hesham.Almatary@nicta.com.au> |
SELFOUR-516 Remove EXPECTED_TCB_SIZE
|
#
fd2f5ec8 |
|
15-Jun-2016 |
Adrian Danis <Adrian.Danis@data61.csiro.au> |
Explicitly check if a capability is physical or not Previously the return value of cap_get_capPtr was compared to 0 in sameRegionAs to emulate a check in the abstract specification that tests if the cap is a physical cap or not. Overloading 0 results in a scenario where a legitimate deviceUntyped's children do not get considered to be children because they have a capPtr of 0. This change adds and explicit function that returns whether or not a capability is physical or not, and uses that in sameRegionAs
|
#
1287590e |
|
16-May-2016 |
Adrian Danis <Adrian.Danis@data61.csiro.au> |
Correct separation of printing and debug builds Fixes some build issues with 541289a32603cee8242b5360b05e8f0c52795433 as well as further allowing debugging (via the capdl interface) to happen when printing is turned off.
|
#
cfcaf49c |
|
31-Jan-2016 |
Adrian Danis <Adrian.Danis@nicta.com.au> |
SELFOUR-399: object sizes and globals frame addr should come from the same source
|
#
0ecff9f3 |
|
09-Nov-2015 |
Adrian Danis <Adrian.Danis@nicta.com.au> |
unsigned int -> word_t
|
#
2d61910e |
|
09-Nov-2015 |
Adrian Danis <Adrian.Danis@nicta.com.au> |
Rename uint32_t -> word_t in any relevant places
|
#
e2c6dbca |
|
05-Nov-2015 |
Adrian Danis <Adrian.Danis@nicta.com.au> |
Cast to word_t instead of 'int' to be compatible with both 32 and 64 bit applications
|
#
d58d4f3e |
|
26-Jun-2015 |
Adrian Danis <Adrian.Danis@nicta.com.au> |
Use word_t for zombie pointers to be 64-bit compatible
|
#
fee26a88 |
|
02-Jun-2015 |
Adrian Danis <Adrian.Danis@nicta.com.au> |
Change casting from int->long to be compatible with both 32 and 64 bit compilations
|
#
a72e0468 |
|
09-Nov-2015 |
Adrian Danis <Adrian.Danis@nicta.com.au> |
Move object size definitions to arch specific headers The size of these objects cannot be considered a common constant as they will be different in the upcoming 64-bit ports
|
#
88d73db0 |
|
15-Oct-2015 |
Anna Lyons <Anna.Lyons@nicta.com.au> |
refactor tcb_t to remove duplication between x86 and arm header files
|
#
54603123 |
|
19-Oct-2015 |
Anna Lyons <Anna.Lyons@nicta.com.au> |
SELFOUR-317: rename async endpoint to notification object, and other fallout.
|
#
f86435c0 |
|
02-Jun-2015 |
Adrian Danis <Adrian.Danis@nicta.com.au> |
Refactor some common elements across arm and x86 structures.h files. This change purely changes the ordering of C symbols, as well as adding some extra checking
|
#
91b7da86 |
|
17-Jul-2014 |
TrusthworthySystems <gatekeeper@sel4.systems> |
Release snapshot
|