Changes

• All Arm platforms supported by seL4 now have a verified configuration.
• Added: build exports an invocations_all.json file with syscall invocation numbers.
• Added option for suppressing generation of config output files in build process
• Added --skip-unchanged option to build process to prevent time stamp update for config output files when these files did not change.
• Added recording of disabled options in build system config output files. Before, options that were hidden from the CMake GUI due to unsatisfied config_choice conditions were not recorded. After this change, these hidden options are recorded as disabled.
• Added build system support for Qemu >= 10
• Change fault based FPU context switching to a TCB flag based approach: New system call seL4_TCB_SetFlags and new flag seL4_TCBFlag_fpuDisabled. See RFC-18.
• Multiple SMP related bugs fixed.
• Change point of cache flush from untyped reset to retype. The kernel now flushes the cache only for those object types where a flush is necessary, and only when the object is retyped, not when the untyped cap is reset. This reduces overall need for flushing and delays it to the point of use. This speeds up boot time significantly.
• Fixed kernel reply protocol for yieldTo (MCS). The kernel would previously for the yieldTo call:
  • return messages with length field set to 0, even though they had content;
  • generate a reply for send-only invocations of the system call;
  • incorrectly indicate success/failure in some circumstances. While these were all incorrect, they would be unlikely to be observed through normal use of libsel4.
• Fixed TCB_SetSchedParams to match the API reference. TCB_SetSchedParams previously had more lenient checks. Used new checks for simplifying the implementation.
• Fixed error indication for SetTimeoutEndpoint and improve error message
• Fixed: when the domain scheduler is used, avoid touching cross-domain state for VCPUs and FPU. Flush VCPU and FPU state on domain switch.
• Enable building with clang-18 and clang-20 (untested in CI).
• Improve error message in build system for when invalid platform parameter is provided.
• Improve boot printing: print half-open regions as [a..b)

Platforms

• Added support for the i.MX93 SoC
• Added support for the Cheshire platform
• Added support for the HiFive Premier P550 platform
• Fixed imx8mq board timer frequency
• Removed the default settings KernelArmVtimerUpdateVOffset and KernelArmDisableWFIWFETraps from the platform tqma8xqp1gb, since they are project specific settings, not platform settings. Add set(KernelArmVtimerUpdateVOffset OFF) and set(KernelArmDisableWFIWFETraps ON) to your project settings to get the same configuration as before if you are using tqma8xqp1gb.

Arm

• Support SGIs (software generated interrupts) on platforms with GICv2 or GICv3 in non-SMP configurations. SGIs are intended for signalling other cores when seL4 is used in a multi-kernel setup. On Arm, this is implemented with a new capability SGISignal, which can be created from IRQControl capabilities with the new IRQ control invocation ARMIRQIssueSGISignal for a specific IRQ and target core. The resulting SGISignal capability can be invoked like a notification capability that supports only signal/send. SGIs can be received by IRQ notification objects on the target core like other IRQs.

  See also RFC-17

• Added config option for selecting which thread ID register is used for Kernel TLS syscalls and invocations. KernelArmTLSReg can be used to select either tpidru or tpidruro as the TLS register used for seL4_TCB_SetTLSBase and seL4_SetTLSBase operations. This config option's default value is tpidru which is what the register that the kernel currently uses for the TLS register for aarch32 and aarch64 platforms.

• Fixed: under some circumstances, writes by a VMM to VCPU timer registers could have been reverted by the kernel to their previous state. This was triggered when:

  • a VCPU thread was running,
  • the VCPU was then disabled but remained active by switching to a non-VCPU thread,
  • that VCPU thread had the VCPU cap and performed the timer register writes,
  • and execution then switched back to the VCPU thread.

  This was found by Alison Felizzi and independently by Ryan Barry during the integrity proofs for AArch64 hyp mode.

• Fixed: under some circumstances, seL4_VCPUReg_CPACR is saved twice to the current VCPU. The value of this register may change between saves, causing the latter save to unintentionally grant EL0/1 access to the FPU.

  1. A thread with an active current VCPU switches to a thread without a VCPU. The current VCPU is disabled. 1.1. seL4_VCPUReg_CPACR is saved to the current VCPU. 1.2. enableFpuEL01 updates the register, enabling FPU access in EL0 and EL1.
  2. The thread without a VCPU switches to a thread with a different VCPU to the first 2.1. All registers from seL4_VCPUReg_TTBR0 to seL4_VCPUReg_SPSR_EL1 are saved. This range includes seL4_VCPUReg_CPACR, which overwrites the previously saved value and grants FPU access at EL0 and EL1.

• Fixed: on aarch32 configurations with hypervisor support, CNTKCTL was not saved and restored alongside other virtual timer registers. seL4_VCPUReg_CNTKCTL has been introduced to mirror seL4_VCPUReg_CNTKCTL_EL1 from aarch64.

• Fixed VGIC and VPPI maintenance handling on MCS, which allowed a thread to simultaneously be blocked and in the release queue.

• Added port of debug API to AArch64.

• Added implementation of Split EOI mode for GICv3 for improved interrupt performance.

• Added aarch64-elf- as valid AArch64 toolchain prefix.

X86

• Fixed XSAVES option for FPU. It is now possible to enable this for newer x86 CPUs.
• Fixed: avoid use-after-free if a VCPU with active FPU state gets deleted.

RISC-V

• Fixed: TCB size on RISC-V 32-bit when FPU is enabled
• Changed default cmake options KernelRiscvExtF and KernelRiscvExtD from OFF to ON. Except for RISCV32 with LLVM clang enabled will default both to OFF.
• Fixed: off-by-1 write for PLIC IRQ priorities. Effect so far only observed on Qemu.
• Added: catch s-mode traps and halt in debug mode. For debugging only.
• Added riscv-none-elf- as valid RISC-V toolchain prefix
• Changed treatment of SBI memory: instead of special in-kernel treatment, SBI memory is now a reserved region in the device tree and can therefore be adjusted per platform.

Upgrade Notes

Set seL4_TCBFlag_fpuDisabled (with the seL4_TCB_SetFlags invocation of TCB capabilities) for tasks not using the FPU to retain the old context switch performance. The -mgeneral-regs-only option may be needed to stop the compiler from issuing SIMD instructions to speed up integer operations.

Full changelog

Refer to the git log in https://github.com/seL4/seL4 using git log 13.0.0..14.0.0

More details

See the 14.0.0 manual included in the release or ask on the mailing list!