Release 12.0.0

Update VERSION
Update CHANGES

Signed-off-by: Oliver Scott <Oliver.Scott@data61.csiro.au>

trivial: update changes file

Some of the changes from the last release should have
been in the 12.0.0 release.

Signed-off-by: Oliver Scott <Oliver.Scott@data61.csiro.au>

aarch64,cortex-a53,hyp: Reduce seL4_UserTop value

This ensures that no frames can be mapped that would overwrite the
currently stored VMID for the vspace.

Signed-off-by: Kent McLeod <kent@kry10.com>

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>

Release docs owned by Data61 under CC-BY-SA-4.0

CC-BY-SA-4.0 is a more appropriate license for documentation than BSD
or GPL.

arm: Configure traps on vcpu WFE/WFI calls

Configure the ability to trap on vcpu WFE/WFI calls. If enabled,
user-level would need to schedule a future interrupt when a given
vcpu invokes a WFE/WFI instruction. This otherwise leaving the
vcpu in a disabled state. An application can choose to
disable the trap if it doesn't want to handle the instruction and
schedule a future interrupt.

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.

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>

CHANGES: improve introduction

Recast introductory paragraphs to better describe the document and
characterise the intended audience.

Move information intended for document maintainers and kernel engineers
to a comment. Add guidance for engineers so they better know when and
how to update this document. (Thanks to Kent for the discussion!)

The `docs/sel4_release` page is not a set of release notes per se, more
like a feature grid and release history; describe it differently.

Style document title as a top-level heading.

Release 11.0.0

Update VERSION
Update CHANGES

Update CHANGES with changes since last release

Try to add all missing changes that affect the seL4 interface.

add support for rockpro64

Kernel support for 64 bit rockpro board.
Dts was taken from the linux kernel.

Updated CHANGES file

Updated CHANGES file to add virt support.

trivial: Update CHANGES

SELFOUR-161: Merge Page_Remap with Page_Map

- Remove Remap function from seL4 API for arm, x86, riscv and the
respective invocation implementation.
- Update Map as replacement for Remap
- Update manual

This allows a change of rights if the frame being mapped is already
mapped in at the given vaddr. To map a page to a different address,
unmap it first.

Co-authored-by: Hesham Almatary <hesham.almatary@data61.csiro.au>
Co-authored-by: Anna Lyons <Anna.Lyons@data61.csiro.au>
Co-authored-by: Victor Phan <Victor.Phan@data61.csiro.au>
Co-authored-by: Kent McLeod <Kent.Mcleod@data61.csiro.au>

aarch64: Move tpidrro_el0 from vcpu to tcb context

This register is visible to software executing at EL0 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 EL0.

This also fixes a potential 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.

aarch64: allow access to memory below physBase

On aarch64 physBase is the constant that points to the bottom of
physical memory (RAM).

Prior to this change the kernel window was mapped directly to physBase,
which is usually not a 0 paddr. As a consequence the kernel could not
access any memory below physBase.

This change fixes this issue by mapping the start of the kernel window
to 0 in the physical address space.

- add new constant PADDR_LOAD, the location of the kernel image in the
physical address space.
- add new constant PADDR_BASE, the start of the physical address space
(0).
- add new constant KERNEL_ELF_BASE, the location of the kernel image in
kernel virtual memory.

A consequence of this change is that on aarch64, the kernelBase constant
now points to the start of the kernel window in virtual memory, but
*not* to the start of the kernel image as these are now different.

mcs: Update CHANGES file

Adds that mcs was merged into the changes file. More detailed release
notes will be included in the next release version.

cortex-53: enable virtualization extensions

This is possible now that the kernel supports 40 bit PAs.

[SMP/Debug] New syscall to send arbitrary SGIs

Created a new syscall, seL4_DebugSendIPI for ARM to send arbitrary SGIs
(software generated interrupts) to arbitrary cores. As SGIs are
specifically PPIs (private interrupts), this syscall effectively allows
to trigger PPIs on arbitrary cores, for debug/testing purposes.

aarch64: Add initial Arm FVP platform config

This platform assumes 2 clusters of A57 processors as described in
tools/dts/fvp.dts. This configuration is for running on FVP simulators.

Add initial i.MX8M Quad evk 64-bit Support

This adds support for the 64-bit i.MX8M Quad evaluation kit.
Currently only AArch64 EL1 is supported.

trivial: Update CHANGES for GICv3

Update CHANGES to reflect RFC-3 Changes.

trivial: CHANGES: document am335x updates

x86/ept: return correct MappingFailedLookupLevel

Prior to this change, seL4_MappingFailedLookupLevel() would retrun '22'
after any failed EPT mapping operation. This change fixes this to return
the correct amount of unresolved bits in the address.

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.

libsel4: add seL4_VspaceBits

This constant represents the size of the root page table.

ARM: optionally pass bootloader DTB to userspace

We now support receiving a DTB from the ELF loader and passing it on
to userspace in extra bootinfo. We still support booting without a DTB,
though - the device tree address is set to zero in the boot code and no
extra bootinfo region is provided.

add FDT extended bootinfo type

FDT is not platform specific (and used on RISC-V and ARM), so this
bootinfo type isn't either.

Add Odroid-C2 support

Add support for the Hardkernel Odroid-C2 board.

Co-Authored-By: Anna Lyons <Anna.Lyons@data61.csiro.au>

Updated CHANGES with Clang support

serial-refactor: Refactor kernel serial drivers

Have added a drivers/serial folder to kernel, where all serial drivers
will be kept. The point is to have the the dts parsed and generate cmake
to include the right uart.c file prefixed with the compatibility.
Have removed all io.c from plat and includes from plat/config.cmake and
updated CHANGES file.

hardware_gen: pull interrupts from DTS

This adds support for extracting interrupt numbers from DTS
to the hardware header file generator, so that the majority
of the per-platform interrupt listings can be removed.

arm: generate memory region tables from dts

This change adds infrastructure to automatically generate the
physBase macro, the avail_p_regs array, and the dev_p_regs array
based on a device tree. Platforms can opt-in to using this
by adding DTS files to the KernelDTSList variable.

The Python script uses the hardware.yml file to determine which
devices in the device tree are of interest to the kernel and should
be hidden from userspace and instead mapped into the kernel. Note that
currently the kernel mappings are not (yet) generated, however most
of the infrastructure needed to make that happen is present.

Update CHANGES with details of Aarch64-hyp

Add seL4_UserTop and move kernelBase to the arch level

- seL4_UserTop is a new constant which represents the top of virtual
memory available to user level
- this commit also rationalises several constants (USER_TOP, kernelBase)
and moves them to the arch level, such that ports only need to define
seL4_UserTop.

libsel4: add seL4_CapRightsBits

SELFOUR-6: Add GrantReply to the rights system.

GrantReply is a new access right added to endpoint capabilities, which
allows seL4_Call to be used on those capabilities (specifically, it
allows reply caps *only* to be granted across endpoints).

Prior to the addition of GrantReply, endpoint capabilities required the
Grant access right, which allowed any arbitrary capabilitiy to be
transferred over an endpoint. Using GrantReply, systems can now be
constructed where threads using seL4_Call over an endpoint do not need to be in the same
security subsystem.

Release 10.1.1

Update VERSION
Update CHANGES

Release 10.1.0

Update VERSION
Update CHANGES

CHANGES: update for upcoming release

Add notes for changes missed during development.

TX2: Add initial TX2 support

See CHANGES and https://docs.sel4.systems/Hardware/ for more information

SELFOUR-1491: add seL4_IRQCOntrol_GetTrigger

Add a new invocation which allows an irq handler capability to be
obtained with a specific trigger method (edge or level). Obtaining
this capability modifies the GIC state.

Drop SEL4_PACKED from types used by seL4.

It has become clear that the 'packed' GCC attribute affects the
memory semantics of C in a way that the verification tools do not
understand. The bootinfo types are used by kernel boot code (not
currently verified, but covered by binary verification) and should
not use this attribute.

This is a source-compatible but not binary-compatible change.

Release 10.0.0

Update VERSION
Update CHANGES

CHANGES: Add missing word `create`

CHANGES: Add note about new build system

CHANGES: Add riscv-32 support to CHANGES file

x86: Document IOPortControl in CHANGES

Release 9.0.1

Update VERSION
Update CHANGES

Revert "Release 9.0.1"

This reverts commit 77e157a98432d564ba173551e8f70032227cd9d9.

Release 9.0.1

Update VERSION
Update CHANGES

riscv: Document architecture in CHANGES

update CHANGES for `label` field of `seL4_MessageInfo`

docsite: Update url

Release 9.0.0

Update VERSION
Update CHANGES

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.

SELFOUR-331: add seL4_TCB_SetSchedParams

This allows the prio and mcp to be set in one system call.

Change prio, mcp to seL4_Word from Uint8_t

Although seL4_MaxPrio does fit into 8 bits, making
the argument 8 bits is not saving us anything.

SELFOUR-1016: Require auth cap to set prio/mcp

This fixes confused deputy problem when setting priorities/mcps.

Remove archInfo from bootinfo

With extended bootinfo providing a more flexible and extensible form of archInfo this
member can be retired.

x86: Store TSC frequency in extended bootinfo header

x86: Define tsc frequency bootinfo header

x86: Config option for RSB flush on context switch

This option can be enabled to prevent a user from performing a Spectre like attack on
another user through polluting the RSB.

x86: Config option for branch prediction barrier on context switch

This option can be enabled to prevent a user from performing a Spectre like attack on
another user through polluting the indirect branch predictor.

x86: Implement IBRS based Spectre mitigations

Provides the ability to enable the IBRS hardware Spectre mitigation strategies, as well
as completes the software mitigation by disabling jump tables in compilation. The
hardware mitigations are largely provided "for completeness" in the hopes that they
eventually become less expensive. For the moment there is no reason to turn on any
beyond STIBP if running in multicore

Document x86-64 Meltdown change

Move changes to correct section

The dangerous MSR interface was not in the 8.0.0 release and so should have been
listed in the upcoming release section

x86: Dangerous read/write MSR interface

Provides a syscall interface for reading and writing arbitrary MSR values. This is
being introduced as an alternative to the DebugRun, as the main purpose of debug run
is for modifying the performance monitoring events via read/write MSR.

Update VERSION file to 8.0.0-dev

Release 8.0.0

Update version file
Update release notes

x86: Document PMC export in CHANGES

x86: Describe mbi2 framebuffer support in CHANGES

Update release notes for latest changes

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.

x86: Update changes file for multiboot2 changes

Clarify how the upcoming release notes in the CHANGES file work

Update CHANGES file to be wordwrapped

Updates CHANGES file for added zynq platform

Add CHANGES file

The purpose of this file is to track changes as they are made to the
kernel in order make writing release notes easier and tracking source or
binary level API breakages.