History log of /seL4-l4v-master/seL4/libsel4/include/sel4/types.h
Revision Date Author Comments
# 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.


# 735b154a 01-Dec-2019 maybe-sybr <58414429+maybe-sybr@users.noreply.github.com>

Use autoconf definition for `RetypeMaxObjects` def

Relates to #168. The definition for `seL4_UntypedRetypeMaxObjects` lives
in the UAPI `types.h` but appears to have no link to the value actually
used by the kernel, which is configurable. This change sets the UAPI
definition to the generated definition from the kernel config steps and
defaults to the previous fixed value if, for some reason, the configured
definition is not available.


# 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.


# 2a707168 02-Oct-2017 Adrian Danis <Adrian.Danis@data61.csiro.au>

libsel4: Make guard and badge definitions mode specific

The definitions of guard and badge sizes is going to be changed for 64-bit platforms,
this change provides an easy way of providing different definitions


# 8108c811 02-Oct-2017 Adrian Danis <Adrian.Danis@data61.csiro.au>

libsel4: Remove bitfield type unifying Guard and Badge construction

Using the bitfield generator to treat guards and badges as a union type can be convenient,
but it requires reserving a bit in the data for the bitfield run time type information.
This type information is not needed by the kernel as it knows implicitly whether the passed
data is a badge or a guard based on the kind of cap being operated on. However, with the
type information present we cannot pass a word sized piece of data to the kernel.

The solution here is to go back to using a plain seL4_Word as the type for invocations
that want a capdata and let the user either construct a badge as a plain word, or use
the seL4_CNode_CapData bitfield for constructing a guard, although they have to manually extract
the word representation out of it.


# 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


# 2fea9a0f 18-Jul-2016 Anna Lyons <Anna.Lyons@nicta.com.au>

SELFOUR-567: use seL4_CapRights_t from libsel4

This change

* changes seL4_CapRights from the kernel to be seL4_CapRights_t in
libsel4
* deprecates the duplicated seL4_CapRights in libsel4, which is
now the bitfield generated type seL4_CapRights_t.
* fixes all usages in kernel and libsel4

Impact: for verification, this will require the type to change name
from cap_rights to seL4_CapRights_t.
This is a breaking libsel4 API change, although most code uses
seL4_AllRights or similar constants, which will not break
at a source level as these constants have been updated.


# 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


# 33a771d3 12-Jul-2016 Anna Lyons <Anna.Lyons@nicta.com.au>

Split fault types into arch/generic

Prior to this commit faults were separate
per architecture. This commit extracts the common
fault types and introduces arch specific faults,
reducing code duplication across architectures.


# f72d02f6 11-Oct-2016 Adrian Danis <Adrian.Danis@data61.csiro.au>

arm/libsel4: Update VCPU fault definitions

With the introduction of debug faults the numbers for VCPU faults
got changed, this commit updates them accordingly


# 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.


# fb19c78e 24-Aug-2016 Hesham Almatary <hesham.almatary@data61.csiro.au>

Benchmark: Share trace point log structure with the user


# da0c39f4 14-Aug-2016 Stephen Sherratt <Stephen.Sherratt@data61.csiro.au>

libsel4: Tidied comments and moved compound rights


# 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


# e619975c 04-Jan-2016 Anna Lyons <Anna.Lyons@nicta.com.au>

SELFOUR-114: make IPC buffer definition accessible to the kernel


# 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


# 44a522dc 18-Aug-2015 Adrian Danis <Adrian.Danis@nicta.com.au>

libsel4: Generate libsel4 definitions from the current ARCH as well as the SEL4_ARCH


# 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.


# 4b3ac0e8 07-Sep-2015 Stephen Sherratt <Stephen.Sherratt@nicta.com.au>

Surrounding benchmarking definitions with "#if CONFIG_MAX_NUM_TRACE_POINTS > 0".


# 4c2554dc 26-Aug-2015 Stephen Sherratt <Stephen.Sherratt@nicta.com.au>

Added support for using multiple tracepoints at the same time.


# e653f8f6 09-Jul-2015 Wink Saville <wink@saville.com>

Streamline libsel4 and remove its libc dependencies.

There are now separate libs for benchmark, assert, printf, putchar
start/stop:

libs/libsel4benchmark
libs/libsel4assert
libs/libsel4printf
libs/libsel4putchar
libs/libsel4startstop

The primary changes are introducing sel4/sel4.h and removing std* types
plus porting assert and IO code from the kernel to libsel4assert,
libsel4printf, libsel4putchar.

This means the code within libsel4 and the newlibs do not overload any
typical libc entities. Instead the libraries use types like
seL4_Uint32 ... instead of uint32_t. And printf is now seL4_Printf and
assert is seL4_Assert ....

Finally, the only file modified that effects kernel code is
kernel/tools/bitfield_gen.py. It needed to be modified as it generates
files for both kernel and user space. And for user space the generated code
(types_gen.h) needed to use the new types and asserts. The changes should
not change what is generated for the kernel and I did a comparison of
kernel_final.{c|s} before and after my change and the only differences
were time stamps.

Bug: #15 Streamline kernel/libsel4 and remove its libc dependencies


# 3775341b 03-Mar-2015 Matthew Fernandez <matthew.fernandez@nicta.com.au>

libsel4: Remove unused right seL4_Transfer_Mint.


# 91b7da86 17-Jul-2014 TrusthworthySystems <gatekeeper@sel4.systems>

Release snapshot