#
1f82755e |
|
03-Nov-2020 |
Kent McLeod <kent@kry10.com> |
boot: Allocate init bookkeeping structs in bss ndks_boot, rootserver and rootserver_mem don't contain any non-zero init values and can be moved to bss so they don't take up space in the ELF. ndks_boot contains a sparse struct that is > 4MiB on x86_64 and so this change allows the x86_64 ELF to return to < 200KiB. Signed-off-by: Kent McLeod <kent@kry10.com>
|
#
707af364 |
|
02-Sep-2020 |
Matthew Brecknell <Matthew.Brecknell@data61.csiro.au> |
boot: initialise root server domain The domain of the root server was previously implicitly initialised to zero. In the case that the first slot in the domain schedule has a domain ID other than zero, this might be incorrect. Here, we explicitly initialise the domain of the root server to the domain ID in the first slot of the domain schedule. Signed-off-by: Matthew Brecknell <Matthew.Brecknell@data61.csiro.au>
|
#
96456c6a |
|
06-May-2020 |
Curtis Millar <curtis.millar@data61.csiro.au> |
trivial: fix header files Signed-off-by: Curtis Millar <curtis.millar@data61.csiro.au>
|
#
ba5540fa |
|
02-Apr-2020 |
Curtis Millar <curtis.millar@data61.csiro.au> |
mcs: Configure idle SC based on target core Every SC in the system must be configured based on the actual core on which it will run and all time comparisons for that SC must be made relative to that core. When creating SCs for the system idle threads those SCs must be configured for their target cores. Signed-off-by: Curtis Millar <curtis.millar@data61.csiro.au>
|
#
1d419f69 |
|
12-Dec-2019 |
Curtis Millar <curtis.millar@data61.csiro.au> |
mcs: SC time relative to assigned core The starting and ready times for any SC should be relative to the core on which the SC is running rather than the current core. 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.
|
#
335b4497 |
|
17-Jul-2019 |
Edward Pierzchalski <ed.pierzchalski@data61.csiro.au> |
Make padding word-size independent An unfortunate hack that lets us specify padding within one `sizeof(seL4_Word)`-sized chunk of a struct, indpendently of the size of a word.
|
#
e97554e5 |
|
13-Dec-2019 |
Kent McLeod <Kent.Mcleod@data61.csiro.au> |
Fix calculate_extra_bi_size_bits implementation This function returns the size_bits for an allocation covering the size of the extra boot info region. Previously it was incorrectly handling rounding up the result of CLZL.
|
#
b5c56244 |
|
07-Oct-2019 |
Simon Shields <simon.shields@data61.csiro.au> |
Create device untypeds at boot for all arches Currently on x86 device untypeds are generated by passing the entire address space minus any parts that are reserved by the kernel or that are "real" memory (e.g. kernel image, physical RAM). On ARM and RISC-V, device untypeds were generated at compile-time from a device tree. This patch moves ARM and RISC-V to use the same approach as x86, and moves the code from x86 into a common location that's shared between the three architectures. Co-Authored-By: Anna Lyons <anna@gh.st>
|
#
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
|
#
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.
|
#
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.
|
#
b6417f21 |
|
20-Mar-2019 |
Curtis Millar <curtis.millar@data61.csiro.au> |
Remove platform IPC buffer register. This removes the assumption that each platform sotres the IPC buffer address in a platform-specific register. The IPC buffer address is instead stored in a thread-local variable in libsel4 which must be initialised by the runtime.
|
#
cb7cbd84 |
|
30-May-2019 |
Anna Lyons <Anna.Lyons@data61.csiro.au> |
boot: allocate rootserver objects last This change allows us to know, from just the kernel and dtb, where user level untyped objects start being allocated from. - allocate rootserver objects from last available freemem region. - move create_rootserver_objects call into init_freemem.
|
#
4a3685df |
|
04-Jun-2019 |
Japheth Lim <Japheth.Lim@data61.csiro.au> |
ARM boot: abort if out of freemem slots This fails early if the build process failed to calculate a suitable MAX_NUM_FREEMEM_REG.
|
#
e42700a4 |
|
04-Jun-2019 |
Japheth Lim <Japheth.Lim@data61.csiro.au> |
ARM boot: MAX_NUM_FREEMEM_REG++ for new allocator Previously, the boot allocator would do dynamic calculations to minimise fragmentation, then throw away the smallest regions. With the new boot allocator, we can reasonably predict that fragmentation will create at most one extra region, so this commit adds one freemem slot for ARM.
|
#
8586b7f2 |
|
07-May-2019 |
Anna Lyons <Anna.Lyons@data61.csiro.au> |
boot: refactor allocation of rootserver objects Prior to this change, the boot process would dynamically allocate memory for root server objects based on the order of initialisation. Allocation was a best-fit algorithm. This change preallocates all memory for root server objects to an aligned untyped just after the user image. By allocating the objects in order of size, allocation is greatly simplified and the ability to reproduce the allocation offline based on the kernel and user image sizes is increased.
|
#
5fac9e81 |
|
29-Apr-2019 |
Anna Lyons <Anna.Lyons@data61.csiro.au> |
config: make root cnode size 4k minimum The previous minimum (4) was actually too small to fit more than 1 capability, which would not allow the kernel to boot. A 4K minimum means on 32-bit, an 8 size is the minimum (256 slots) and on 64-bit, 7 (128 slots). In addition to being a more practical minimum, this also allows for simplification of the boot code for future commits.
|
#
210c5c21 |
|
28-May-2019 |
Japheth Lim <Japheth.Lim@data61.csiro.au> |
boot: revert binary verification workaround in init_freemem The toolchain has been tweaked to accept the original code, so the workaround is no longer required. This reverts commit d0d97779cbf0bbf54bab26b2274ae435908d5ab6.
|
#
d0d97779 |
|
13-May-2019 |
Matthew Brecknell <Matthew.Brecknell@data61.csiro.au> |
boot: avoid array access in init_freemem This works around an issue in the binary correctness proofs. The `if` conditions become assumptions when proving refinement of the branches. Currently, a simplification step is slow when these assumptions contain certain modes of array access. The slowdown apparently becomes dramatically worse when multiple such assumptions are present, such as in the final `else` branch. Hopefully, this limitation can be addressed in future work.
|
#
0c4da6fb |
|
09-May-2019 |
Anna Lyons <Anna.Lyons@data61.csiro.au> |
boot: use static array rather than stack array Binary verification cannot parse the instructions produced by the stack array, likely because none of the existing kernel code declares arrays on the stack. Given all boot code and data is unmapped, wiped and made available to the user after boot, moving the array to static data isn't a problem.
|
#
d967aa0d |
|
11-Apr-2019 |
Anna Lyons <Anna.Lyons@data61.csiro.au> |
boot: pass the c-parser - use constant array size on stack - cast arrays to pointers to match function return types
|
#
e3a83035 |
|
10-Apr-2019 |
Anna Lyons <Anna.Lyons@data61.csiro.au> |
boot: consolidate init_freemem init_freemem sets up available regions of memory for the hardware that seL4 is booting on. Previously this function was duplicated across architectures, with minor duplication. This change provides a top-level init_freemem suitable for all architectures. - arm/riscv: change get_avail_p_reg to return whole p_reg array - update all architectures to use new init_freemem. - wrap init_freemem calls with arch_init_freemem for each arch, where arch_init_freemem sets up the available and reserved regions of memory which are passed to init_freemem.
|
#
69339d42 |
|
09-Apr-2019 |
Jasper Lowell <jasper.lowell@data61.csiro.au> |
Boot code: Statically allocate idle thread The idle thread is not managed at user-level and so it can instead be statically allocated. This simplifies the boot code and increments towards being easier to formally verify.
|
#
a6b4cf73 |
|
09-Apr-2019 |
Anna Lyons <Anna.Lyons@data61.csiro.au> |
boot: allocate irq cnode statically The memory used for the irq cnode is never available to the user. As a result this memory can be allocated statically, simplifying the bootcode. - remove allocation of irq cnode - add static init - generate irq cnode size from cmake for arm - add static constants for riscv, x86 as there is no variability at the moment.
|
#
b7c053f9 |
|
25-Nov-2018 |
Simon Shields <simon.shields@data61.csiro.au> |
Add support for extra bootinfo larger than a page The current code may not always allocate enough - change the logic to over-allocate memory rather than under-allocate.
|
#
7fc45c4e |
|
18-Mar-2019 |
Anna Lyons <Anna.Lyons@data61.csiro.au> |
style: set code width to 120
|
#
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
|
#
3d10ef0c |
|
18-Mar-2019 |
Anna Lyons <Anna.Lyons@data61.csiro.au> |
style: correct parenthesis padding Use astyle's unpad-paren to unpad all parentheses that are not included by pad-header, pad-oper, and pad-comma.
|
#
e5bb6745 |
|
09-Dec-2018 |
Anna Lyons <Anna.Lyons@data61.csiro.au> |
Calculate IRQ_CNODE_BITS from maxIRQ IRQ_CNODE_BITS is determined by the maxIRQ on the platform. Calculate this value from maxIRQ instead of hardcoding for each platform.
|
#
f6a88c6b |
|
12-Aug-2018 |
Thomas Sewell <Thomas.Sewell@data61.csiro.au> |
Retire boot_ctzl. This was a workaround for a problem that was properly fixed in f8606c86 however the boot_ctzl version somehow persisted.
|
#
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
|
#
9f3fc38c |
|
15-Feb-2018 |
Anna Lyons <Anna.Lyons@data61.csiro.au> |
Assign correct affinity to idle thread
|
#
61f8f4d0 |
|
09-Jan-2018 |
Adrian Danis <Adrian.Danis@data61.csiro.au> |
Avoid repeatedly appending idle threads to debug list Each node calls `init_core_state` and so can be relied upon to append their own idle thread. Having every core enqueue all the cores idle threads is not correct as it will result in attempting to enqueue a thread more than once.
|
#
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
|
#
318ead8f |
|
17-Jun-2017 |
Hesham Almatary <hesham.almatary@data61.csiro.au> |
Call Arch_setTCBIPCBuffer from kernel/boot.c
|
#
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.
|
#
ac9ea516 |
|
16-May-2017 |
Anna Lyons <Anna.Lyons@data61.csiro.au> |
SELFOUR-880: name the idle thread
|
#
3b2b64a0 |
|
01-May-2017 |
Kent McLeod <Kent.Mcleod@data61.csiro.au> |
SELFOUR-864: Fix alignment calculation
|
#
f42d6363 |
|
15-Mar-2017 |
Anna Lyons <Anna.Lyons@data61.csiro.au> |
refactor: initialise common core state in one place
|
#
c4395425 |
|
26-Feb-2017 |
Adrian Danis <Adrian.Danis@data61.csiro.au> |
Remove assumption on 32-bit memory offsets On 64-bit platforms physical address could be >2^32 offset from a virtual address. This changes offsets to match the word size of the target architecture
|
#
f8606c86 |
|
20-Feb-2017 |
Adrian Danis <Adrian.Danis@data61.csiro.au> |
Provide spec for CTZL Provides a spec for the __builtin_ctzl function and changes existing code to use this wrapper
|
#
0a93c3a2 |
|
15-Feb-2017 |
Bamboo <bamboo@keg.ertos.in.nicta.com.au> |
[STYLE_FIX]
|
#
c574f4fc |
|
13-Feb-2017 |
Adrian Danis <Adrian.Danis@data61.csiro.au> |
Helper for allocating the extra boot info region
|
#
7836f76c |
|
12-Feb-2017 |
Adrian Danis <Adrian.Danis@data61.csiro.au> |
Extend bootinfo to support potentially arbitrary additional structures This provides a future proof interface for extending the bootinfo region with additional kinds of optional architecture and platform specific information. The basic idea is to report the size of a region directly following the bootinfo frame, which is made up of a series of 'chunks'. Each chunk has an identifier (describing what it is) and a length, allowing unknown chunks to be skipped in favor of examining the remaining of the chunks.
|
#
f3d62531 |
|
26-Jan-2017 |
Adrian Danis <Adrian.Danis@data61.csiro.au> |
Use same constant for clearing and allocating bootinfo frame Closes #56
|
#
f658276a |
|
03-Aug-2016 |
Thomas Sewell <Thomas.Sewell@nicta.com.au> |
Remove many DONT_TRANSLATE markers. The vast majority of the DONT_TRANSLATE markers in the kernel are used to hide __asm__ statements and builtin functions (e.g. __builtin_unreachable ()) from the C-to-Isabelle parser. The parser now supports underscore identifiers and many __asm__ statements, and the builtin functions are prototyped, meaning the vast majority of the DONT_TRANSLATE markers can be dropped. The remaining markers cover functions that must be treated specially.
|
#
198a8305 |
|
21-Nov-2016 |
Bamboo <bamboo@keg.ertos.in.nicta.com.au> |
[STYLE_FIX]
|
#
e78cdf9b |
|
27-Jul-2016 |
Adrian Danis <Adrian.Danis@data61.csiro.au> |
SELFOUR-553: Support alternate IPC buffer locations without globals frame This commit adds support for using the ThreadID registers of the ARM MPCore platforms for storing the address of the IPC buffer instead of the globals frame. The choice of using the user readable/writeable ThreadID register is chosen, even though it means the user cannot use it for its own purposes, as it leaves room in the future for doing TLS support in the user read only register, where compilers expect it.
|
#
828a14d8 |
|
07-Nov-2016 |
Adrian Danis <Adrian.Danis@data61.csiro.au> |
SELFOUR-222: Configure IRQ cnode size per platform
|
#
03c71b63 |
|
16-May-2016 |
Thomas Sewell <Thomas.Sewell@nicta.com.au> |
SELFOUR-444: Preemptible zeroing for retype. Change to the order of operations and timing behaviour of invokeUntyped_Retype. The Retype operation now zeroes the entire range of the Untyped cap (if it is being used for the first time) before installing any objects. This avoids the need for long-running initialisation of large objects, whose initial contents are always zero. The initial zeroing phase is preemptible, and may take multiple timeslices to complete.
|
#
2d462d4a |
|
17-Oct-2016 |
amrzar <azarrabi@nicta.com.au> |
add basic api for setting affinity
|
#
1887ae9d |
|
13-Oct-2016 |
amrzar <azarrabi@nicta.com.au> |
Update SMP idle thread handling
|
#
7d50c439 |
|
26-Sep-2016 |
Adrian Danis <Adrian.Danis@data61.csiro.au> |
Defined untyped size ranges in libsel4
|
#
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.
|
#
8e77cdb5 |
|
21-Sep-2016 |
Adrian Danis <Adrian.Danis@data61.csiro.au> |
SELFOUR-421: Add padding for untyped in bootinfo
|
#
d507b2d3 |
|
09-Feb-2016 |
Adrian Danis <Adrian.Danis@nicta.com.au> |
SELFOUR-421 Introduce explicit device frames and untypeds Kernel objects cannot be created from device untypeds, with the exception of frames, which do not get zeroed and cannot be used as an IPC buffer. Device untypeds additionally cannot be used in the construction of ASID pools. This then changes the API to the rootserver (i.e. bootinfo) to send device untypeds instead of device frames. On ARM these device untypeds are the same as the previously exported device frame regions. On x86 PCI scanning is removed and all physical memory addresses (that are not important for kernel integrity) are released to the user. In order to have bits in the frame and untyped caps on ARM the number of software ASIDs had to be reduced from 2^18 to 2^17, and the maximum untyped size reduced from 2^31 to 2^30
|
#
d97603bd |
|
14-Jul-2016 |
Hesham Almatary <hesham.almatary@data61.csiro.au> |
SELFOUR-566: Decouble seL4_DebugNameThread from CONFIG_PRINTING
|
#
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.
|
#
289bf92b |
|
05-Jan-2016 |
Anna Lyons <Anna.Lyons@nicta.com.au> |
SELFOUR-114: remove bootinfo.h duplication
|
#
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
|
#
3439c6bd |
|
28-Jun-2015 |
Adrian Danis <Adrian.Danis@nicta.com.au> |
Do not switch to the the root thread until after cpu initialization is done
|
#
c58b2a3d |
|
16-Dec-2015 |
Matthew Fernandez <matthew.fernandez@nicta.com.au> |
Remove `boot_clzl`. This function seemed to exist for the sole reason of being able to mark the CLZ operation as DONT_TRANSLATE. This is no longer necessary as the underlying `clzl` function is now marked DONT_TRANSLATE.
|
#
1c7efe17 |
|
16-Dec-2015 |
Matthew Fernandez <matthew.fernandez@nicta.com.au> |
Fix missing include. This file uses macros like `CLZL` that are defined in util.h.
|
#
1b34ed08 |
|
14-Jun-2015 |
Adrian Danis <Adrian.Danis@nicta.com.au> |
x86: Define a KERNEL_BASE_OFFSET for translating the kernel image region This definition is different to BASE_OFFSET in that it is only meant to apply to the kernel image portion of the kernel window, and doesn't assume that the entire window can be translated by a single offset
|
#
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
|
#
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
|
#
d685d7f1 |
|
05-Nov-2015 |
Adrian Danis <Adrian.Danis@nicta.com.au> |
Use wordBits instead of constant 32
|
#
88d73db0 |
|
15-Oct-2015 |
Anna Lyons <Anna.Lyons@nicta.com.au> |
refactor tcb_t to remove duplication between x86 and arm header files
|
#
952e5a27 |
|
13-May-2015 |
Adrian Danis <Adrian.Danis@nicta.com.au> |
Add ability to set a human readable thread name when running kernel in debug mode
|
#
4f12acd2 |
|
25-Feb-2015 |
Matthew Fernandez <matthew.fernandez@nicta.com.au> |
ARM: Map the initial thread's IPC buffer and boot info as non-executable. Note that this also required some irrelevant x86 changes to match function arguments.
|
#
af0f3b36 |
|
15-Jan-2015 |
Adrian Danis <Adrian.Danis@nicta.com.au> |
ia32: Large commit that implements PAE paging for x86 This commit involves the PAE paging itself, refactoring the vspace code to extra what is common between PAE and 32bit paging, as well as some renaming to not call the root paging structure a PD
|
#
6d31d460 |
|
20-Oct-2014 |
Matthew Fernandez <matthew.fernandez@nicta.com.au> |
trivial: Standardise on 32-bit unsigned variables for domain values. Domains are unnecessarily treated explicitly as 8-bit values within boot info. Though there are existing proof constraints that limit the maximum domain value to 8 bits, most of the code would permit domain values up to 32 bits. The maximum value is unnecessarily constrained in boot info, a restriction which this commit removes. Closes VER-341
|
#
04106920 |
|
16-Oct-2014 |
Adrian Danis <Adrian.Danis@nicta.com.au> |
Derive a new IPC buffer cap when inserting into the initial threads TCB to remove mapping information For any other thread setting the IPC buffer via TCB_Configure will result in a derived capability being installed that does not have mapping information. This leads to a expected behaviour that setting a new IPC buffer (even if it is the same as the current one), will not perform an unmapping.
|
#
91b7da86 |
|
17-Jul-2014 |
TrusthworthySystems <gatekeeper@sel4.systems> |
Release snapshot
|