CHANGES

<!-- SPDX-License-Identifier: CC-BY-SA-4.0 -->

# Revision History for seL4

<!--
    Document maintainers: Wrap lines in this file at 120 characters.

    Kernel engineers: When making changes to code (rather than documentation or comments) in the kernel repository,
    include a change item entry here, at the end of the list for the upcoming release, describing the change, and
    evaluate whether the compatibility breakage level must be promoted as a consequence.  As some rules of thumb:
    * If the change affects only the sources of the kernel (`src/`, `/include`), it is a BINARY-COMPATIBLE change.
    * If the change adds visible C preprocessor or language symbols in `libsel4/`, it is a BINARY-COMPATIBLE change.
    * If the change alters existing symbol definitions, types, or implementations in `libsel4/`, it is a
      SOURCE-COMPATIBLE change.
    * Otherwise, it is BREAKING.
-->

The following is a high-level description of changes to the seL4 kernel project, grouped by release.  It is aimed at
engineers who desire a summary of changes in more coarse-grained form than the Git commit history.  Each release
description indicates whether it is SOURCE-COMPATIBLE, BINARY-COMPATIBLE, or BREAKING relative to the previous release.

Further information about [seL4 releases](https://docs.sel4.systems/sel4_release/) is available.

---
Upcoming release: BREAKING

## Changes

### Security-relevant Changes

* Fixed a kernel-crashing NULL pointer dereference when injecting an IRQ for a non-associated VCPU on SMP
  configurations. This can be triggered from user-level by any thread that has access to or can create non-associated
  VCPU objects. While HYP+SMP is not a verified configuration and is not thoroughly tested, it is generally assumed to
  be working. If you are using this configuration, it is strongly recommended to upgrade.

  * Affected configurations: only unverified HYP+SMP configurations on Arm platforms are affected.
  * Affected versions: seL4 versions 12.0.0 and 12.1.0.
  * Exploitability: Any thread that can create or that has access to an unassociated VCPU can cause the crash. In static
    systems, only the system initialiser thread can create VCPUs and the standard capDL system initialiser will not
    trigger the issue. VMMs could have the authority to dissociate an existing VCPU from a TCB if they have both
    capabilities. That is, a malicious VMM could cause a crash, but generally VMMs are trusted, albeit not verified
    code. Guest VMs generally do not have sufficient authority to exploit this vulnerability.
  * Severity: Critical. This crashes the entire system.

### Other Changes

* Added support for the ARM Cortex A55
* Added support for the ODroid C4
* Added support for the Avnet MaaXBoard
* Added support for arm_hyp on qemu-arm-virt platfrom with cortex-a15 CPU
* Added support for qemu-riscv-virt
* Added support for the Pine64 Star64
* Rename libsel4 config option ENABLE_SMP_SUPPORT to CONFIG_ENABLE_SMP_SUPPORT to be namespace compliant.
* Rename libsel4 config option AARCH64_VSPACE_S2_START_L1 to CONFIG_AARCH64_VSPACE_S2_START_L1 to be namespace
  compliant.
* Remove imx31/kzm platform support. This platform is being removed as it is sufficiently old and unused.
* Remove ARM1136JF_S and ARMv6 support. This architecture version is being removed as it is sufficiently old and
  unused. See [RFC-8](https://sel4.atlassian.net/browse/RFC-8).
* Remove ARMv6 specific configs: KernelGlobalsFrame and KernelDangerousCodeInjectionOnUndefInstr. This removes the
  constant seL4_GlobalsFrame from libsel4 as well as the IPC buffer in GlobalsFrame caveat from CAVEATS-generic.md
* Implement KernelArmExportPTMRUser and KernelArmExportVTMRUser options for Arm generic timer use access on aarch32.
* Removed obsolete define `HAVE_AUTOCONF`
* Removed user address space reserved slots restriction on 40bit PA platforms when KernelArmHypervisorSupport is set.
  This change is reflected in the definition of the seL4_UserTop constant that holds the largest user virtual address.
* aarch32 VM fault messages now deliver original (untranslated) faulting IP in a hypervisor context, matching
  aarch64 behaviour.
* Correct the minimum size of a scheduling context. This changes the value of `seL4_MinSchedContextBits`.
* Remove the ability for user-space on RISC-V platforms to access the core-local interrupt controller (CLINT). The
  CLINT contains memory-mapped registers that the kernel depends on for timer interrupts and hence should not be
  accessible by user-space.
* AArch64: remove VSpace object types, seL4_ARM_PageDirectory and seL4_ARM_PageUpperDirectory
  The functionality previously provided by these types will be provided by the existing seL4_ARM_PageTable object type.
  This allows for a simpler API and enables a smaller kernel implementation that will be easier to verify.
  libsel4 provides a source compatibility translation that maps the old libsel4 names and constants the new ones in
  <sel4/sel4_arch/deprecated.h>. There are some exceptional cases where kernel behavior has changed:
  - A Page directory and page table are now the same kind of object and can be mapped at any page table level.
    If the lookup for the provided address stops at a slot that can map a page directory, it will map the object as a
    page directory. If there already is a page directory mapped, the lookup will proceed to the next level and it will
    map as a page table instead of returning an error.
* Add configuration option `KernelRiscvUseClintMtime` for faster access of hardware timestamp on RISC-V platforms.
  The configuration option is not enabled by default as it requires access to the CLINT which depends on the platform
  and whether the M-mode firmware allows S-mode to access the CLINT. For example, newer versions of OpenSBI (1.0 and above)
  do not allow direct access of the CLINT.
* Added SMC Capability (smc_cap) and SMC forwarding for aarch64 platforms. See
  [RFC-9](https://sel4.atlassian.net/browse/RFC-9).
* Arm+Hyp: Enabled access to seL4_VCPUReg_VMPIDR and seL4_VCPUReg_VMPIDR_EL2 for all hyp configurations.
  Previously this register was only accessible for SMP kernel configurations. Non-SMP configurations can still require
  access when wanting to control the value of MPIDR that the guest reads.
  Note that the initial value for new seL4_ARM_VCPUs for this register is 0 which isn't a legal value for MPIDR_EL1 on
  AArch64. It may be necessary for the register to be explicitly initialized by user level before launching a thread
  associated with the new seL4_ARM_VCPU.

## Upgrade Notes

* The change in `seL4_MinSchedContextBits` can lead to failure where code previously created
  scheduling contexts with size `seL4_MinSchedContextBits` and expected more than the 2 minimum
  refills to be available for that size. Either use a larger size (the previous value 8 of
  `seL4_MinSchedContextBits`) in retyping, or request fewer refills.

---
12.1.0 2021-06-10: SOURCE COMPATIBLE

## Changes

* Moved kernel configuration header to libsel4.
* Improved benchmarking:
  - Made the kernel log buffer to be derived from cmake config.
  - Added x86_64 kernel log buffer.
  - Implemented RISC-V benchmark timestamping.
  - Implemented benchmark log buffer for RISC-V.
* Moved cap functions out of inline to make changing cap bitfields less noisy.
* Removed weak definition of the __sel4_ipc_buffer variable which was causing large thread local storages to be
  required.
* Prepared the bitfield generator for Isabelle 2021.
* Made a number of improvements to the CMake build scripts.
* Added pre-processor 'include guards' for auto-generated files.
* Added missing CONFIG_PLAT_IMX7 pre-processor '#define's.
* Added `#pragma once` to the autoconf headers.
* Removed `HAVE_AUTOCONF` guards in `sel4/config.h`.
* Improved the manual:
  - Corrected descriptions of CNode addressing.
  - Documented initial thread's SMMU caps.
* Improved libsel4:
  - Removed redundant `HAVE_AUTOCONF` header guards in libsel4.
  - Added missing `macros.h` #include in libsel4.
  - Cleaned-up `macros.h` in libsel4.
  - Added checks to use `_Static_assert()` in libsel4 if it is available.
  - Unified definitions in `simple_types.h` in libsel4.
  - Added `printf` format specifier `PRI_sel4_word` for printing word types.
  - Unified seL4 type definitions.
* Added specific `printf` formatting for seL4_Word.
* Changed some variables to use `BOOT_BSS` instead of `BOOT_DATA` to save space in the ELF file.
* Replaced the `capDL()` function with a generic `debug_capDL` function that is intended to be implemented by all
  architectures.
* Reduced `printf`s stack usage.
* Fixed `ksnprintf()` corner case handling.
* Fixed NULL `printf` output wrapper handling.
* Cleaned up the printing API implementation.
* Changed code to pass buffer to `printf` output channel.
* Refactored the kernel console handling.
* Added support for `PRIu64` and `SEL4_PRIu_word` in the kernel.
* Changed various `printf` conversion specifiers to use `SEL4_PRIx_word` specifiers.

### MCS

* Fixed a physical counter access issue on MCS on EL2.
* Added MCS support for the ZynqMP.
* Changed invokeSchedControl_Configure to always produce a scheduling context that is active and has configured
  refills.
* Prevented the binding of scheduling contexts to blocked TCBs.
* Fixed conversions of ticks to microseconds on aarch64.
* Added an additional sporadic flag to `seL4_SchedControl_Configure` which allows the option to create a sporadic
  scheduling context.
* Added explicit checks to not unblock the current scheduling context.
* Fixed MCS and aarch64 VCPU interrupt interaction.
* Renamed MCS kernel configuration option `KernelStaticMaxBudgetUs` to `KernelStaticMaxPeriodUs`.
* Added check to make sure that the current thread will not yield to multiple threads.
* Added check to account for an inactive scheduling context at preemption.
* Deferred charging time budget in a preempted invocation.
* Added code to update `ksDomainTime` in `updateTimestamp`.
* Added call to `updateTimestamp` in a preemption point.
* Added code to clear ksConsume when charging time to a revoked scheduling context.
* Added code to cancel IPC when finalising reply caps.
* Fixed a dereference of a scheduling context after it's removed from the associated TCB.
* Added MCS to the preprocess check.

### x86

* Removed a redundant de-reference for `seL4_X86DangerousRDMSR` in ia32.
* Added a config option to set the frequency of the TSC.
* Optimized the boot image size for x86_64.
* Removed the PT_PHDR segment from the linker script to work around an issue in a variant of syslinux that treats a
  PT_PHDR segment as distinct from a PT_LOAD segment.

### Arm

* FPU ownership is now also given away on thread deletion instead of only on FPU exception.
* Added basic build support for A35 core.
* Fixed read/write of the VCPU CPACR register.
* Fixed invalidation of the VIPI I-cache in hypervisor mode.
* Removed duplicate interrupts for the zynqmp in its DTS.
* Updated device definitions for the exynos5.
* Added Raspberry Pi 4 support.
* Updated Ethernet interrupts in the ZynqMP.
* Added i.MX6 Nitrogen6_SoloX support.
* Fixed CMake configurations for the ZynqMP and the Ultra96.
* Fixed the platform `#define` for the i.MX6 Nitrogen6_SoloX.
* Fixed I-cache invalidation on aarch64 SMP.
* Fixed the usage of KernelPaddrUserTop on Arm platforms.
* Added support for the i.MX low-power UART.
* Added an option to ignore SErrors which is enabled on default for the TX2.

### RISC-V

* Added PLIC driver and updated the DTS for the Ariane.
* Merged the PLIC drivers for the Ariane and the Hifive.
* Updated default timer frequency for the Ariane.
* Map devices with large pages on 32 and 64-bit kernel.
* Replaced mentions of BBL with OpenSBI.
* Added definitions of the KernelOpenSBIPlatform variable for RISC-V platforms.
* Removed instances of passing `extra_caps_t` by value for binary verification purposes.
* Removed `slot_range_t` for binary verification purposes.
* Removed `DONT_TRANSLATE` tag on 'read_sip' for binary verification purposes.
* Added more efficient clz and ctz implementations to substitute the lack of machine instructions to count leading and
  trailing zeroes.
* Updated kernel bootstrap message to be the same as the one on Arm.
* Added some fastpath improvements for RISC-V.
* Added extra snippets of code to track kernel entries for RISC-V.
* Added a configuration guard for fastpath on RISC-V.
* Reorganised `traps.S` so that syscalls and fastpath checks were done after interrupts and exceptions checks to avoid
  exceptions being interpreted as null-syscalls.
* Added support for `riscv64-elf-` toolchain.
* Fixed a register bug in the assembly entry point for SMP with regards to the elfloader passing HART and core IDs.

## Upgrade Notes

* Scheduling contexts can now be configured as constant-bandwidth or sporadic server.
  - Constant bandwidth observes a continuous constant bandwidth of budget/period.
  - Sporadic server behaves as described by Sprunt et. al.
  - In an overcommitted system, sporadic preserves accumulated time.
* There are new `PRIx` and `SEL4_PRIx` `printf` conversion specifiers that can now be used inside the kernel.
* x86_64 kernel binaries are now smaller and may be structured differently compared to previous kernel binaries.
* Kernel entry benchmarking can now be done on RISC-V.
* AUTOCONF_INCLUDED is no longer defined. The seL4 build system has stopped
  using autoconf a long time ago and this define has been kept for compatibility
  since then. It is no longer used anywhere by now, so it can be removed.

---
12.0.0 2020-10-30: BREAKING
## Changes


* Update licensing to reflect project transfer to seL4 Foundation. SPDX tags are now used to identify the licenses for
  each file in the project. Generally, kernel-level code is licensed under GPLv2 and user-level code under the 2-clause
  BSD license.
* Update contribution guidelines:
  * the seL4 foundation requires DCO process instead of a CLA
* Functional correctness verification for the RISC-V 64-bit HiFive Unleashed platform configuration
  (RISCV64_verified.cmake with no fastpath or FPU enabled)
* Update caveats file:
  - The recycle operation has been removed
  - More detail on what versions are verified
  - Update comments on real time use of seL4
* Improve seL4 manual.
  - Fix aarch64 seL4_ARM_PageDirectory object API docs:
    seL4_ARM_PageDirectory_Map is passed a vspace cap not an upper page directory cap.
  - Increase documentation coverage for Arm object invocations
  - Rework introduction of system calls in Kernel Services and Objects chapter.
  - Improve discussion of Receive and Wait syscall behaviour between MCS and non-MCS systems.
  - Explicitly mention grantreply rights in the exceptions section.
  - Document schedcontext size_bits meaning.
  - Remove metion of system criticality.
  - Add SchedContext to object size discussion.
  - Fix initial thread's CNode guard size.
  - Update BootInfo struct table.
  - Update padding field in UntypedDesc table
* Update seL4_DebugSnapshot to provide a CapDL dump of the capability layout of
  a running system for Arm, x86_64 and riscv32 configurations.
* KernelBenchmarksTrackUtilisation:
  - Add feature support for SMP configurations
  - For each thread also track number of times scheduled, number of kernel entries and amount of cycles spent inside the
    kernel and also add core-wide totals for each.
* Add 2 new benchmark utilization syscalls
  - seL4_BenchmarkDumpAllThreadsUtilisation: Prints a JSON formatted record of total and per-thread utilisation
    statistics about the system. This currently includes a thread's total cycles scheduled, total number of times
    scheduled, total cycles spent in the kernel and total number of times entering the kernel and then totals of each
    for all threads on the current core.
  - seL4_BenchmarkResetAllThreadsUtilisation: Resets the current counts of every user thread on the current core.
* Added seL4_DebugPutString libsel4 function for printing a null-terminated string via calling seL4_DebugPutChar().
* Introduced a new config flag, KernelInvocationReportErrorIPC, to enable userError format strings to be written to
  the IPC buffer. Another config bool has been introduced to toggle printing the error out and this can also be set at
  runtime. LibSel4PrintInvocationErrors is a libsel4 config used to print any kernel error messages reported in the IPC
  buffer.
* Repair barriers in clh_lock_acquire (SMP kernel lock). Strengthen the clh_lock_acquire to use release on the
  atomic_exchange that makes the node public. Otherwise, (on ARM & RISCV) the store to the node value which sets its
  state to CLHState_Pending can become visible some time after the node is visible. In that window of time, the next
  thread which attempts to acquire the lock will still see the old state (CLHState_Granted) and enters the critical
  section, leading to a mutual exclusion violation.
* Replace all #ifdef header guards with #pragma once directives in libsel4 header files
* gcc.cmake:
  - Add option for coloured gcc output. Setting GCC_COLORS in the environment will result in -fdiagnostics-color=always
    being provided to gcc. Ordinarily gcc would suppress coloured output when ninja redirects its stderr during normal
    builds.
  - Remember CROSS_COMPILER_PREFIX across CMake invocations. The variable would become unset in certain contexts.
  - Add support for Arm cross-compilers on Red Hat distros.
* Fastpath optimisation:
  - Reorganise the code layout on Arm.
  - bitfield_gen: explicit branch predictions.
  - Optimize instruction cache access for fastpath.
* Extend Clang support to all kernel configurations. Support targets LLVM versions between 9 and 11.
* hardware_gen.py: Add elfloader output target for hardware_gen script. This generates header files describing the
  platform's CPU configuration as well as device information such as compatibility strings and memory regions to the
  elfloader that are consistent with the kernel's own definitions.
* Fix bootinfo allocation bug when user image pushed against page directory boundary. The bootinfo is mapped in at the
  end of the user image in the initial thread's vspace. The kernel initialisation code wasn't calculating the
  bootinfo size correctly which could lead to a kernel fault when trying to map the bootinfo in when the parent page
  table object hadn't been allocated.
* Use autoconf definition for `RetypeMaxObjects` in <sel4/types.h>. This ensures that the definition stays consistent
  with what the kernel is configured with.
* Fix up timers and clock frequencies
  - Remove beaglebone kernel timer prescaling. Previously the timer frequency was incorrectly set to to half (12MHz) its
    configured frequency (24MHz).
  - Set TX1 kernel timer frequency config to 12MHz and not 19.2MHz as this is the standard frequency of the input clock
    source (m_clock).
  - Set KZM kernel timer frequency config to 35MHz and not 18.6MHz based on sampling the timer frequency.
  - imx31: add missing dts entry for the epit2 timer.
  - Set non-mcs i.MX6 kernel timer frequency config to 498MHz and not 400MHz as this is based on the frequency of the
    input clock source (PLL1)
  - Zynq7000: Set kernel timer frequency to 320MHz.
  - Qemu-arm-virt: Set kernel timer frequency to 6.25MHz.
* Do not generate data symbols for enums in libsel4 as they end up as bss symbols and cause linker errors on newer
  compiler versions.
* Update padding field definition in seL4_UntypedDesc to make the struct word aligned. Previously, this struct wasn't
  correctly word aligned on 64-bit platforms. This change removes the padding1 and padding2 fields and replaces them
  with a padding field that is a variable number of bytes depending on the platform.
* Add GitHub actions scripts. These scripts replicate internal CI checks directly on GitHub

### MCS

* Stop scheduling contexts from being bound to tcb's that already have scheduling contexts.
* Fix x86 `KERNEL_TIMER_IRQ` definition. Previously, MCS preemption point handling would check the wrong interrupt on
  x86 platforms.
* smp: tcb affinity modification bug. When changing the affinity of a thread on a remote core, the reschedule
  operation wasn't being performed.
* Allow `replyGrant` for fault handlers. The MCS kernel so far insisted on full grant rights for fault handler caps,
  but replyGrant is sufficient and consistent with the default kernel config.
* All scheduling contexts compare their time with time in assigned core instead of currently executing core.
* Prevent recursion on timeout faults by suspending a passive server that receives a timeout fault.
* Add KernelStaticMaxBudgetUs to bound the time the user provides to configure scheduling contexts to avoid malicious
  or erroneous overflows of the scheduling math. Make the default max period/budget 1 hour.
* rockpro64: enable mcs configurations

### Arm

* arm: Add seL4_BenchmarkFlushL1Caches syscall to manually flush L1 caches in benchmark configurations.
* New fault type when running in Arm hypervisor mode: seL4_Fault_VPPIEvent
    - The kernel can keep track of IRQ state for each VCPU for a reduced set of PPI IRQs and deliver IRQ events as
      VCPU faults for these interrupt numbers.
    - Additionally a new VCPU invocation is introduced: seL4_ARM_VCPU_AckVPPI.
      This is used to acknowledge a virtual PPI that was delivered as a fault.
* Virtualise Arm Timer and VTimer interrupts to support sharing across VCPUs.
  - A VCPU will now save and restore VTimer registers for the generic timer and also deliver a VTimer IRQ via a
    seL4_Fault_VPPIEvent fault. This enables multiple VCPUs bound to the same physical core to share this device.
* Build config option for whether WFE/WFI traps on VCPUs when running in Arm hypervisor mode
* Arm: Add VMPIDR and VMPIDR_EL2 registers to VCPU objects for programming a VCPU's 'Virtualization Multiprocessor
  ID Register' on aarch32 and aarch64.
* Arm, vcpu, smp: Remote IPI call support for VIRQS. Injecting a VIRQ into a vcpu running on a different core will
  IPI the remote core to perform the IRQ injection.
* zynqmp: Disable hardware debug APIs as the platform doesn't support kernel hardware debug API.
* zynqmp: Add support for aarch32 hyp
* Gicv3: include cluster id when sending ipis.
* qemu-arm-virt:
  - Generate platform dtb based on KernelMaxNumNodes config value.
  - Reserve the first 512MiB of Ram as device untyped for use in virtualization configurations.

#### Aarch32

* Moved TPIDRURO (PL0 Read-Only Thread ID register) to TCB register context from VCPU registers. This means
  changes to this register from user level have to go via seL4_TCB_Write Registers instead of seL4_ARM_VCPU_WriteRegs.
* aarch32: Restrict cache flush operation address range in hyp mode. It's required that cache flushing in hyp mode
  is performed through the kernel window mapping as the kernel is unable to flush addresses outside of this mapping
  without causing an access fault.
* arm_hyp: Move PGD definitions out of libsel4 as they don't correspond to any public interfaces and are only used
  internally by the kernel to manage its own address space.

#### Aarch64

* aarch64: Fix a bug where saving ELR_EL1 when managing a VCPU object was reading from ELR_EL1 instead of writing to it.
* aarch64: Fix a bug where saving FAR_EL1 when managing a VCPU object was only writing to the low 32 bits of the 64-bit
  FAR_EL1 register.
* aarch64: Add missing faults to seL4_getArchFault. seL4_getArchFault is a libsel4 helper that constructs fault messages
  out of the IPC buffer message registers but it wasn't aware of all possible fault types.
* aarch64,vcpu: Add CNTKCTL_EL1 register to `vcpu_t`. This register tracks timer delegation to EL0 from EL1 and
  needs to be switched for different VCPUs.
* aarch64: Adds missing vcpu cases for some aarch64-specific functions on capabilities.
* cortex-a53,hyp: Reduce seL4_UserTop when on a cortex-a53 platform and KernelArmHypervisorSupport is set.
  - This is because the kernel uses the last slot in the top level VSpace object for storing the assigned VMID and so
    any addresses that are addressed by the final slot are not accessible. This would apply to any CPU that have 40bit
    stage 2 translation input address.
* Arm SMMUv2 kernel API and TX2 smmuv2 driver. This supports using an SMMU to provide address translation and memory
  protection for device memory access to platforms that implement a compatible Arm SMMUv2 System mmu. The kernel
  implementation supports using an SMMU to restrict memory access of VM guest pass-through devices, or for isolating
  devices and their drivers' memory accesses to the rest of a running system.

### x86

* Fix printf typo in `apic_init`.
* x86_64: Fix PCID feature constant to use the correct bit.
* Fix interrupt flag reset upon nested interrupt resume, `c_nested_interrupt`. This fixes an issue where ia32 kernels
  would crash if receiving a nested interrupt.

### RISC-V

* Functional correctness of seL4/RISCV now formally verified at the C level.
* Hifive: Enable seL4_IRQControl_GetTrigger object method. This method allocates an IRQ handler by ID and whether it is
  level or edge triggered. Note: HiFive PLIC interrupts are all positive-level triggered.
* Add search for additonal gcc riscv toolchains if the first one cannot be found.
* Add support for rocketchip soc. Support Rocketchip SoC maps to Xilinx ZC706 board and ZCU102 board
* Add support for polarfire soc.
* Clear reservation state on slowpath exit as the RISC-V ISA manual requires supervisor code to execute a dummy sc
  instruction to clear reservations "during a preemptive context switch".
* Pass DTB through to userlevel in extra bootinfo fields similar to on Arm.
* Use full width of scause to prevent large exception numbers to be misinterpreted as syscalls.
* Fix page map bug.
  - Previously, it was possible in decodeRISCVFrameInvocation for the rwx rights of the new PTE to become 000 after
    masking with cap rights. This would turn the frame PTE into a page table PTE instead, and allow the user to create
    almost arbitrary mappings, including to kernel data and code. The defect was discovered in the C verification of the
    RISC-V port.
* Remove seL4_UserException_FLAGS. This field was unused and was never set to anything by the kernel.
* Add FPU config options for RISCV
  - Two options, KernelRiscvExtD and KernelRiscvExtF, are added to represent the D and F floating-point extensions.
    KernelHaveFPU is enabled when the floating-point extensions are enabled. The compiler ABI will also be changed to
    lp64d for hardfloat builds.
* Add RISCV64_MCS_verified.cmake config for in-progress MCS verification
* riscv32: Remove incorrectly provided constants for 512MiB 'huge pages' which is not part of the specification.
* riscv: Lower .boot alignment to 4KiB. This makes the final kernel image more compact.

## Upgrade Notes

* The project's licensing updates don't change the general licensing availability of the sources.
  More information can be found: https://github.com/seL4/seL4/blob/master/LICENSE.md
* Any references to the padding1 or padding2 fields in seL4_UntypedDesc require updating to
  the new padding field. It is expected that these fields are unused.
* Any platforms that have had changed kernel timer frequencies will see different scheduling
  behavior as kernel timer ticks will occur at different times as kernel ticks are configured
  in microseconds but then converted to timer ticks via the timer frequency. Any time-sensitive
  programs may need to be re-calibrated.
* Any riscv32 programs that were using the constants RISCVGigaPageBits or seL4_HugePageBits will
  see a compilation error as the constants have been deleted as they aren't supported in the riscv32 spec.
* Any riscv programs that refer to the seL4_UserException_FLAGS field will need to remove this reference. This field was
  never initialised by the kernel previously and has now been removed.
* Any riscv programs using the LR/SC atomics instructions will see reservations invalidated after kernel entries. It is
  expected that this will not require any changes as reservations becoming invalid is normal behavior.
* On cortex-a53 platforms when KernelArmHypervisorSupport is set have 1 less GiB of virtual memory addresses available
  or 2GiB less on TX2 with the SMMU feature enabled. This is captured by the change in definition of the seL4_UserTop
  constant that holds the larges virtual address accessible by user level.
* On aarch32 the TPIDRURO register(PL0 Read-Only Thread ID register) has been removed from the VCPU object and added to
  the TCB object. A VCPU is typically bound to a TCB so after updating the access, a thread with a VCPU attached will
  still support having a TPIDRURO managed.
* On Arm hypervisor configurations, PPI virtual timer interrupts are now delivered via seL4_Fault_VPPIEvent faults and
  it is not possible to allocate an interrupt handler for these interrupts using the normal interrupt APIs. A VPPI
  interrupt is received via receiving a fault message on a VCPU fault handler, and acknowledged by an invocation on
  the VCPU object. VPPI interrupts that target a particular VCPU can only be generated while the VCPU thread is
  executing.

---
11.0.0 2019-11-19: BREAKING

## Changes

* Add GrantReply access right for endpoint capabilities.
 - seL4_Call is permitted on endpoints with either the Grant or the GrantReply access rights.
 - Capabilities can only be transferred in a reply message if receiver's endpoint capability has the Grant right.
* `seL4_CapRights_new` now takes 4 parameters
* seL4_CapRightsBits added to libsel4. seL4_CapRightsBits is the number of bits
 to encode seL4_CapRights.
* `seL4_UserTop` added
  - a new constant in libsel4 that contains the first virtual address unavailable to
    user level.
* Add Kernel log buffer to aarch64
* Support added for Aarch64 hypervisor mode (EL2) for Nvidia TX1 and TX2. This is not verified.
* Support for generating ARM machine header files (memory regions and interrupts) based on a device tree.
* Support added for ARM kernel serial driver to be linked in at build time based on the device tree compatibility string.
* Support added for compiling verified configurations of the kernel with Clang 7.
* RISC-V: handle all faults
  - Pass all non-VM faults as user exceptions.
* arm-hyp: pass ESR in handleUserLevelFault
* aarch64: return ESR as part of user level fault
* Created new seL4_nbASIDPoolsBits constant to keep track of max nb of ASID pools.
* Support added for Hardkernel ODROID-C2.
* Added extended bootinfo header for device tree (SEL4_BOOTINFO_HEADER_FDT).
* Support added for passing a device tree from the bootloader to the root task on ARM.
* Add seL4_VSpaceBits, the size of the top level page table.
* The root cnode size is now a minimum of 4K.
* Hifive board support and RISC-V external interrupt support via a PLIC driver.
* Update seL4_FaultType size to 4bits.
* Fix seL4_MappingFailedLookupLevel() for EPTs on x86.
    - add SEL4_MAPING_LOOKUP_NO_[EPTPDPT, EPTPD, EPTPT] which now correspond to
      the value returned by seL4_MappingFailedLookupLevel on X86 EPT mapping calls.
* BeagleBone Black renamed from am335x to am335x-boneblack.
* Supported added for BeagleBone Blue (am335x-boneblue).
* Remove IPC Buffer register in user space on all platforms
* Add managed TLS register for all platforms
* Add configurable system call allowing userspace to set TLS register without capability on all platforms.
* Non-hyp support added for Arm GICv3 interrupt controller.
* Add initial support for i.MX8M boards.
  - Support for i.MX8M Quad evk AArch64 EL2 and EL1, AArch32 smode only is accessible via the imx8mq-evk platform.
  - Support for i.MX8M Mini evk AArch64 EL2 and EL1, AArch32 smode only is accessible via the imx8mm-evk platform.
* Add FVP platform with fixed configuration. This currently assumes A57 configuration described in tools/dts/fvp.dts.
* Arm SMP invocation IRQControl_GetTriggerCore added
  - Used to route a specify which core an IRQ should be delivered on.
* Kernel log buffer: Specify on which core an IRQ was delivered.
* Add new seL4_DebugSendIPI syscall to send arbitrary SGIs on ARM when SMP and DEBUG_BUILD are activated.
* Support for aarch64-hyp configurations with 40-bit physical addresses (PA) added.
    - The aarch64 api now refers to VSpaces rather than PageGlobalDirectories,
      as depending on the PA the top level translation structure can change.
    - all `seL4_ARM_PageGlobalDirectory` invocations are now `seL4_ARM_VSpace` invocations.
    - new constants 'seL4_ARM_VSpaceObject` and `seL4_VSpaceIndexBits`.
* Merged MCS kernel feature.
  - this is not verified and is under active verification.
  - The goals of the MCS kernel is to provide strong temporal isolation and a basis for reasoning about time.
* Moved aarch64 kernel window
    - aarch64 kernel window is now placed at 0, meaning the kernel can access memory
      below where the kernel image is mapped.
* aarch64: Moved TPIDRRO_EL0 (EL0 Read-Only Thread ID register) to TCB register context from VCPU registers. This means
  changes to this register from user level have to go via seL4_TCB_Write Registers instead of seL4_ARM_VCPU_WriteRegs.
* Merge ARCH_Page_Remap functionality into ARCH_Page_Map. Remap was used for updating the mapping attributes of a page
  without changing its virtual address. Now ARCH_Page_Map can be performed on an existing mapping to achieve the same
  result. The ARCH_Page_Remap invocation has been removed from all configurations.
* riscv64: Experimental SMP support for RISCV64 on HiFive.
* Support added for QEMU ARM virt platform, with 3 CPUs: cortex-a15, cortex-a53 and cortex-a57
    - PLATFORM=qemu-arm-virt
    - ARM_CPU={cortex-a15, cortex-a53, cortex-a57}
    - QEMU_MEMORY=1024 (default)
* Support added for rockpro64.
* RISCV: Add support for Ariane SoC
* Unify device untyped initialisation across x86, Arm and RISC-V
  - Access to the entire physical address range is made available via untypes.
  - The kernel reserves regions that user level is not able to access and doesn't hand out untypeds for it.
  - Ram memory is part of this reservation and is instead handed out as regular Untypeds.
  - Memory reserved for use by the kernel or other reserved regions are not accessible via any untypeds.
  - Devices used by the kernel are also not accessible via any untypeds.

## Upgrade Notes

* Usages of Endpoints can now use seL4_Call without providing Grant rights by downgrading the Grant to GrantReply
* The kernel no longer reserves a register for holding the address of a thread's IPC buffer. It is now expected that the
  location of the IPC buffer is stored in a __thread local variable and a thread register is used to refer to each
  thread's thread local variables. The sel4runtime is an seL4 runtime that provides program entry points that setup
  the IPC buffer address and serves as a reference for how the IPC buffer is expected to be accessed.
* All `seL4_ARM_PageGlobalDirectory` invocations need to be replaced with `seL4_ARM_VSpace`.
* Usages of ARCH_Page_Remap can be replaced with ARCH_Page_Map and require the original mapping address to be provided.
* Device untypeds are provided to user level in different sizes which may require more initial processing to break them
  down for each device they refer to.

---
10.1.1 2018-11-12: BINARY COMPATIBLE

## Changes
 * Remove theoretical uninitialised variable use in infer_cpu_gic_id for binary translation validation

## Upgrade Notes
 * 10.1.0 has a known broken test in the proofs.  10.1.1 fixes this test.

---
10.1.0 2018-11-07: SOURCE COMPATIBLE

## Changes

 * structures in the boot info are not declared 'packed'
    - these were previously packed (in the GCC attribute sense)
    - some field lengths are tweaked to avoid padding
    - this is a source-compatible change
 * ARM platforms can now set the trigger of an IRQ Handler capability
     - seL4_IRQControl_GetTrigger allows users to obtain an IRQ Handler capability
       and set the trigger (edge or level) in the interrupt controller.
 * Initial support for NVIDIA Jetson TX2 (ARMv8a, Cortex A57)
 * AARCH64 support added for raspberry pi 3 platform.
 * Code generation now use jinja2 instead of tempita.
 * AARCH32 HYP support added for running multiple ARM VMs
 * AARCH32 HYP VCPU registers updated.
 * A new invocation for setting TLSBase on all platforms.
     - seL4_TCB_SetTLSBase
 * Kbuild/Kconfig/Makefile build system removed.

---
10.0.0 2018-05-28: BREAKING

- Final version of the kernel  which supports integration with Kbuild based projects
- Future versions, including this one, provide a CMake based build system

For more information see https://docs.sel4.systems/Developing/Building.

## Changes

 * x86 IO ports now have an explicit IOPortControl capability to gate their creation. IOPort capabilities  may now only
   be created through the IOPortControl capability that is passed to the rootserver. Additionally IOPort capabilities
   may not be derived to have smaller ranges and the IOPortControl will not issue overlapping IOPorts
 * 32-bit support added for the initial prototype RISC-V architecture port

## Upgrade Notes

 * A rootserver must now create IOPort capabilities from the provided IOPortControl capability. As IOPorts can not
   have their ranges further restricted after creation it must create capabilities with the final desired granularity,
   remembering that since ranges cannot overlap you cannot issue a larger and smaller range that have any IO ports
   in common.

---
9.0.1 2018-04-18: BINARY COMPATIBLE

## Changes
 * On 64-bit architectures, the `label` field of `seL4_MessageInfo` is now 52 bits wide. User-level programs
   which use any of the following functions may break, if the program relies on these functions to mask the
   `label` field to the previous width of 20 bits.
     - `seL4_MessageInfo_new`
     - `seL4_MessageInfo_get_label`
     - `seL4_MessageInfo_set_label`
 * Initial prototype RISC-V architecture port. This port currently only supports running in 64-bit mode without FPU or
   or multicore support on the Spike simulation platform. There is *no verification* for this platform.

## Upgrade Notes
---
9.0.0 2018-04-11: BREAKING

= Changes =
 * Debugging option on x86 for syscall interface to read/write MSRs (this is an, equally dangerous, alternative to
   dangerous code injection)
 * Mitigation for Meltdown (https://meltdownattack.com) on x86-64 implemented. Mitigation is via a form of kernel
   page table isolation through the use of a Static Kernel Image with Microstate (SKIM) window that is used for
   trapping to and from the kernel address space. This can be enabled/disabled through the build configuration
   depending on whether you are running on vulnerable hardware or not.
 * Mitigation for Spectre (https://spectreattack.com) on x86 against the kernel implemented. Default is software
   mitigation and is the best performing so users need to do nothing. This does *not* prevent user processes from
   exploiting each other.
 * x86 configuration option for performing branch prediction barrier on context switch to prevent Spectre style
   attacks between user processes using the indirect branch predictor
 * x86 configuration option for flushing the RSB on context switch to prevent Spectre style attacks between user
   processes using the RSB
 * Define extended bootinfo header for the x86 TSC frequency
 * x86 TSC frequency exported in extended bootinfo header
 * `archInfo` is no longer a member of the bootinfo struct. Its only use was for TSC frequency on x86, which
   can now be retrieved through the extended bootinfo
 * Invocations to set thread priority and maximum control priority (MCP) have changed.
     - For both invocations, users must now provide a TCB capability `auth`
     - The requested MCP/priority is checked against the MCP of the `auth` capability.
     - Previous behavior checked against the invoked TCB, which could be subject to the confused deputy
       problem.
 * seL4_TCB_Configure no longer takes prio, mcp as an argument. Instead these fields must be set separately
   with seL4_TCB_SetPriority and seL4_TCB_SetMCPriority.
 * seL4_TCB_SetPriority and seL4_TCB_SetMCPriority now take seL4_Word instead of seL4_Uint8.
       - seL4_MaxPrio remains at 255.
 * seL4_TCB_SetSchedParams is a new method where MCP and priority can be set in the same sytsem call.
 * Size of the TCB object is increased for some build configurations

= Upgrade notes =
 * seL4_TCB_Configure calls that set priority should be changed to explicitly call seL4_TCB_SetSchedParams
   or SetPriority
 * seL4_TCB_Configure calls that set MCP should be changed to explicitly call seL4_TCB_SetSchedParams
   or seL4_TCB_SetMCPriority

---
8.0.0 2018-01-17

= Changes =
 * Support for additional zynq platform Zynq UltraScale+ MPSoC (Xilinx ZCU102, ARMv8a, Cortex A53)
 * Support for multiboot2 bootloaders on x86 (contributed change from Genode Labs)
 * Deprecate seL4_CapData_t type and functions related to it
 * A fastpath improvement means that when there are two runnable threads and the target thread is the highest priority
in the scheduler, the fastpath will be hit. Previously the fastpath would not be used on IPC from a high priority
thread to a low priority thread.
 * As a consequence of the above change, scheduling behaviour has changed in the case where a non-blocking IPC is sent
between two same priority threads: the sender will be scheduled, rather than the destination.
 * Benchmarking support for armv8/aarch64 is now available.
 * Additional x86 extra bootinfo type for retrieving frame buffer information from multiboot 2
 * Debugging option to export x86 Performance-Monitoring Counters to user level

= Upgrade notes =
 * seL4_CapData_t should be replaced with just seL4_Word. Construction of badges should just be `x` instead of
   `seL4_CapData_Badge_new(x)` and guards should be `seL4_CNode_CapData_new(x, y)` instead of
   `seL4_CapData_Guard_new(x, y)`
 * Code that relied on non-blocking IPC to switch between threads of the same priority may break.

---
7.0.0 2017-09-05

= Changes =
 * Support for building standalone ia32 kernel added
 * ia32: Set sensible defaults for FS and GS selectors
 * aarch64: Use tpidrro_el0 for IPC buffer instead of tpidr_el0
 * More seL4 manual documentation added for aarch64 object invocations
 * Default NUM_DOMAINS set to 16 for x86-64 standalone builds
 * libsel4: Return seL4_Error in invocation stubs in 8fb06eecff9 ''' This is a source code level breaking change '''
 * Add a CMake based build system
 * x86: Increase TCB size for debug builds
 * libsel4: x86: Remove nested struct declarations ''' This is a source code level breaking change '''
 * Bugfix: x86: Unmap pages when delete non final frame caps

= Upgrade notes =
 * This release is not source compatible with previous releases.
 * seL4 invocations that previously returned long now return seL4_Error which is an enum. Our libraries have already
   been updated to reflect this change, but in other places where seL4 invocations are used directly, the return types
   will need to be updated to reflect this change.
 * On x86 some structs in the Bootinfo have been rearranged. This only affects seL4_VBEModeInfoBlock_t which is used if
   VESA BIOS Extensions (VBE) information is being used.

= Known issues =
 * One of our tests is non-deterministicly becoming unresponsive on the SMP release build on the Sabre IMX.6 platform,
   which is a non verified configuration of the kernel.  We are working on fixing this problem, and will likely do a
   point release once it is fixed.

---
For previous releases see https://docs.sel4.systems/sel4_release/