History log of /seL4-l4v-10.1.1/seL4/libsel4/sel4_arch_include/aarch32/sel4/sel4_arch/constants.h
Revision Date Author Comments
# 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