#
1a9756f6 |
|
09-Sep-2019 |
Qian Ge <qian.ge@data61.csiro.au> |
SMMU: basic driver for init and probing Introducing the driver in kernel for detecting SMMU features and initialise the hardware. Signed-off-by: Oliver Scott <Oliver.Scott@data61.csiro.au>
|
#
5a341610 |
|
01-Aug-2020 |
Stefan O'Rear <sorear@fastmail.com> |
Do not generate data symbols for enums With clang 11 these become bss symbols rather than commons, resulting in multiple definition errors at link time. gcc 10 is likely to expose the same issue. Signed-off-by: Stefan O'Rear <sorear@fastmail.com>
|
#
00a9ba91 |
|
12-May-2020 |
Kent McLeod <Kent.Mcleod@data61.csiro.au> |
aarch32: Move tpidruro from vcpu to tcb context This register is visible to software executing at PL0 but not writeable. Storing it in the VCPU context required custom save/restore handling as it had to be explicitly handled when switching from a VCPU thread to a non-VCPU thread so that it didn't become a channel. It is possible to now update this register via seL4_TCB_WriteRegisters for software executing at PL0. This also fixes a bug where if a vcpu-thread is switched for a non-vcpu-thread and then switched to a different vcpu-thread the original vcpu-thread's copy of this register will get set to 0. 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.
|
#
bddd4054 |
|
27-Jan-2020 |
Alison Felizzi <Alison.Felizzi@data61.csiro.au> |
arm: Added define for VMPIDR and VMPIDR_EL2 Added constant definitions for the VMPIDR (arm32) and VMPIDR_EL2 (arm64) registers. These being vcpu registers that can be written, read, saved and restored. The 'Virtualization Multiprocessor ID Register' (VMPIDR) is needed to program a vcpu's affinity during initialisation. This is currently only exposed on SMP configurations. Co-authored-by: Anna Lyons <anna@gh.st>
|
#
232b0e86 |
|
15-Oct-2019 |
Kent McLeod <Kent.Mcleod@data61.csiro.au> |
arm_hyp: Move PGD definitions out of libsel4 The PGD constants refer to the top level mapping object used by the kernel for its own private mappings. Userlevel cannot create any PGD objects and so these constants don't belong in libsel4.
|
#
71d636f8 |
|
20-Jun-2019 |
Alison Felizzi <Alison.Felizzi@data61.csiro.au> |
arm_hyp: Save and restore vtimer state on switches Added support for reading and writing additional virtual timer registers for vcpu hw read and write accesses. These include the compare value register (CNTV_CVAL) and offset register (CNTV_OFF), each represented as two 32 bit (high and low) registers on aarch32 and as single 64 bit registers on aarch64. Added support for explicitly saving and restoring the virtual timer registers when the vcpu is enabled and disabled. This ensures when the vcpu is switched in and out, the virtual timer registers are restored to a state that is consistent to when it was last run. By default the CNTVOFF register will be updated by the kernel to accumulate the time the VCPU is not running. From the guest this will result in the VCNT register not increasing when the VCPU is suspended. This behavior can be turned off by disabling the KernelArmVtimerUpdateVOffset config option.
|
#
f795e7c0 |
|
23-Jun-2019 |
Alison Felizzi <Alison.Felizzi@data61.csiro.au> |
arm: New virtual PPI event fault type This commit introduces a new fault type, seL4_Fault_VPPIEvent. This change means the kernel can reserve PPI interrupts and virtualise them via delivering the irq to the active vcpu through a specific fault. This enables multiplexing PPI IRQs across multiple VCPUS which requires correctly masking and unmasking the IRQ depending on which VCPU is running. A new VCPU invocation, seL4_ARM_VCPU_AckVPPI is also added for acknowledging the handling of the IRQ. This takes an IRQ as a parameter but will only accept IRQ numbers that are sent as VPPIEvent faults. Co-authored-by: Rafal Kolanski <rafal.kolanski@data61.csiro.au> Co-authored-by: Kent McLeod <Kent.Mcleod@data61.csiro.au>
|
#
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
|
#
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.
|
#
5646f774 |
|
20-Mar-2019 |
Curtis Millar <curtis.millar@data61.csiro.au> |
RFC-3: Update user context for ARM with thread IDs Switched appropriate naming conventions. Was using the aarch64, have switched to aarch64 names. TIPDRURW -> tpidr_el0 TPIDRURO -> tpidrro_el0 TPIDRPRW -> tpidr_el1 Switch TLS register on aarch32 from TPIDURO (tpidrro_el0) to tpidr_ro so that it can be written to from user-land. Thread ID registers tpidr_el0 have been added to the user context for aarch32 and aarch64. Only the thread ID that is writeable from EL0 is saved in the TCB and saved/restored on context switch. Thread IDs that are only changed within a VM (the read-only thread ID for exception level 0 and the thread ID for exception level 1) are stored in the VCPU and saved and stored as part of VM enable/disable. Thread IDs that are only changed with VMs have been separated out into hypervisor code.
|
#
fd83c0a3 |
|
20-Mar-2019 |
Curtis Millar <curtis.millar@data61.csiro.au> |
Replace IPC_BUF_GLOBALS_FRAME with KERNEL_GLOBALS_FRAME The globals frame no longer serves its original purpose of informing a thread of its IPC buffer address, and instead as a virtual implementation of thread ID registers.
|
#
f3fbf855 |
|
29-Apr-2019 |
Anna Lyons <Anna.Lyons@data61.csiro.au> |
libsel4: add seL4_VspaceBits This constant represents the size of the root page table.
|
#
f99f6790 |
|
28-Mar-2019 |
Curtis Millar <curtis.millar@data61.csiro.au> |
Use more robust check for TCB size The complex conditions for the AARCH32 TCB size are updated to better reflect the circumstances in which the TCB will have a particular size.
|
#
142bf9b1 |
|
21-Mar-2019 |
Sylvain Gauthier <sylvain.gauthier@data61.csiro.au> |
More standard constant name, moved ASID constants to arch generic files
|
#
9b646462 |
|
13-Feb-2019 |
Anna Lyons <Anna.Lyons@data61.csiro.au> |
libsel4: consistent definition of seL4_PGDBits Previously seL4_PGDBits was calculated, which is inconstent with the rest of the composite constants in libsel4, and makes size constants harder to parse from the C. This commit makes seL4_PGDBits consistant with other definitions, by making the definition an integer and checking it with a compile time assert.
|
#
723aa0ea |
|
04-Jul-2018 |
Adrian Danis <Adrian.Danis@data61.csiro.au> |
arm: Use TCB version of TPIDRUR[OW] state These registers are part of the 'regular' TCB state and are saved and restored as part of normal thread switching. As such it is conflicting to have a duplicate idea of the value of these registers, especially as it is not kept in sync with the version in the TCB, which is what is actually being loaded into the hardware.
|
#
d6b33211 |
|
22-Mar-2018 |
Yanyan Shen <yanyan.shen@data61.csiro.au> |
arm/hyp: Fix typo TTBRC -> TTBCR
|
#
822ebd7d |
|
22-Feb-2018 |
Yanyan Shen <yanyan.shen@data61.csiro.au> |
arm/hyp: Remove CNTV_CVAL
|
#
81317fb6 |
|
31-Oct-2017 |
Yanyan Shen <yanyan.shen@data61.csiro.au> |
arm/hyp: refactor VCPU states Use an array and constants to replace register names in the VCPU.
|
#
cc9ccb49 |
|
26-Mar-2018 |
Adrian Danis <Adrian.Danis@data61.csiro.au> |
arm: Correct TCB size under multicore
|
#
f5d0b93c |
|
25-Mar-2018 |
Adrian Danis <Adrian.Danis@data61.csiro.au> |
arm: Correct TCB size when using FPU and virtualisation
|
#
f12d6fdc |
|
20-Mar-2018 |
Adrian Danis <Adrian.Danis@data61.csiro.au> |
Increase seL4_TCBBits ready for alignment increase The alignment of the tcb_t portion of a TCB object is going to be increased, this will cause the total TCB size to overflow in some cases. This updates the definition of seL4_TCBBits such that TCBs will be large enough after the alignment change.
|
#
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
|
#
64d576fb |
|
12-Jun-2017 |
Hesham Almatary <hesham.almatary@data61.csiro.au> |
SELFOUR-806: aarch32 - Implement lazy FP save/restore This commit implements lazy FP save/restore mechanism, required for user threads when they use the FPU. The following caveats take place: * Only support synchronous exceptions. No support for asynchronous ones. * VFP opcodes are used instead of normal instructions to discard compiler warnings/errors. * Support is limited to specific ARM subarchitectures we support and tested this commit on. * Disable the FPU by default if users are not using it to avoid channels. * FPU support is not verified yet. * Will not work properly if using a VM that's running besides other VMs/threads that are using the FPU.
|
#
07f94833 |
|
18-Jun-2017 |
Anna Lyons <Anna.Lyons@data61.csiro.au> |
libsel4: fix licenses - some were incorrectly marked GPL (libsel4 is BSD) - update NICTA --> DATA61 etc - fix tags D61 --> DATA61 - update year to 2017
|
#
af1e8762 |
|
31-May-2017 |
Anna Lyons <Anna.Lyons@data61.csiro.au> |
tk1: increase seL4_TCBBits in debug mode Otherwise there is not enough space for tcbName
|
#
9ca253a3 |
|
07-May-2017 |
Anna Lyons <Anna.Lyons@data61.csiro.au> |
SELFOUR-879: expose index and entry constants
|
#
beddca16 |
|
21-Mar-2017 |
Anna Lyons <Anna.Lyons@data61.csiro.au> |
libsel4: Add seL4_FastMessageRegisters This allows benchmarks and utility code to only set registers in the ipc buffer as required.
|
#
2e5ce5a2 |
|
24-Jan-2017 |
Adrian Danis <Adrian.Danis@data61.csiro.au> |
arm: VCPU interface for manipulating banked registers Adds extra fields to the Read/Write VCPU Register invocations to read and write the banked the registers
|
#
191b4465 |
|
22-Jan-2017 |
Adrian Danis <Adrian.Danis@data61.csiro.au> |
arm: Introduce constant for VCPU register
|
#
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
|
#
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.
|
#
8d0ed702 |
|
31-Oct-2016 |
Adrian Danis <Adrian.Danis@data61.csiro.au> |
Use correct seL4_MaxUntypedBits This change uses the seL4_MaxUntypedBits constant in decodeUntypedInvocation when checking the size of the requested allocation. This constant is also changed to be the correct value. The verification team suspects this check is probably unnecessary, but have also resolved not to waste more time investigating.
|
#
7d50c439 |
|
26-Sep-2016 |
Adrian Danis <Adrian.Danis@data61.csiro.au> |
Defined untyped size ranges in libsel4
|
#
bebfcf6d |
|
23-Jun-2016 |
Kofi Doku Atuah <kofi.dokuatuah@nicta.com.au> |
SELFOUR-499: X86, ARM: Add userspace invocations for hardware debugging This commit implements the body of SELFOUR-499. The API exposes the x86 DR0-7 and ARM coprocessor 14 features to userspace by virtualizing them as context- switched registers in the TCB. Implemented as TCB invocations. This feature is only built when CONFIG_HARDWARE_DEBUG_API is selected. * Add low-level support routines for setting, unsetting, getting, enabling and disabling breakpoints. * Add support for single-stepping as well. ^ Single-stepping is not supported on ARMv6 since the hardware doesn't have support. ^ ARM implements single-stepping as instruction breakpoints configured to fault on every instruction -- this is achieved through the "mismatch" mode, which is only supported from ARMv7 onwards. * Also support explicit software break requests, a la "BKPT" and "INT $3". * New invocations: * seL4_TCB_SetBreakpoint(). * seL4_TCB_GetBreakpoint(). * seL4_TCB_UnsetBreakpoint(). * seL4_TCB_ConfigureSingleStepping(). * New constants: ^ Event types: ^ seL4_InstructionBreakpoint. ^ seL4_DataBreakpoint. ^ seL4_SoftwareBreakRequest. ^ Access types: ^ seL4_BreakOnRead. ^ seL4_BreakOnWrite. ^ seL4_BreakOnReadWrite. ^ Exports: ^ seL4_NumHWBreakpoints. ^ seL4_NumExclusiveBreakpoints. ^ seL4_NumExclusiveWatchpoints. ^ seL4_NumDualFunctionMonitors. ^ seL4_FirstBreakpoint. ^ seL4_FirstWatchpoint. ^ seL4_FirstDualFunctionMonitor. See documentation in the seL4 API manual.
|
#
f34f354a |
|
16-Aug-2016 |
Anna Lyons <Anna.Lyons@data61.csiro.au> |
SELFOUR-617: one source of memory object sizes Adds the following constants to libsel4 and uses them in the kernel. seL4_SectionSize (arm) seL4_SuperSectionSize (arm) seL4_HugePageSize (x86 - pae) seL4_LargePageSize (arm) seL4_DataFault seL4_InstructionFault
|
#
5f0ae410 |
|
02-Jun-2016 |
Adrian Danis <Adrian.Danis@data61.csiro.au> |
arm-hyp: Minor cleanups Cleanup some small licensing, whitespace and configuration details
|
#
9ec83284 |
|
24-May-2016 |
Hesham Almatary <Hesham.Almatary@nicta.com.au> |
Fix: move seL4_LogBufferSize to the correct file
|
#
11720f23 |
|
19-May-2016 |
Yanyan Shen <yanyan.shen@nicta.com.au> |
arm-hyp/tk1: fix bugs found during testing
|
#
6523fe40 |
|
21-Feb-2016 |
Adrian Danis <Adrian.Danis@nicta.com.au> |
Correct previous merge
|
#
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
|
#
1a1110a0 |
|
14-Jan-2016 |
amrzar <azarrabi@nicta.com.au> |
Modify Kconfig and Makefile for aach32 as sel4_arch libsel4: updates to include aarch32 as sel4_arch
|