Announcing the release of seL4 15.0.0 with new features, new platforms, and minor fixes.
This is a breaking release.
Changes
- Add runtime domain schedule configuration.
See RFC-20. - libsel4: make thread-local IPC buffer optional (see
LibSel4UseThreadLocals). - The
KernelAllowSMCCallsoption can now be used for verification builds - Update documentation on
seL4_X86_EPT_VMAttributes - Update documentation for
seL4_VMEnter() - Bitfield generator: support for simple arithmetic expressions and new
field_ptrkeyword for reducing the need for
#ifdefin bitfield definitions - Fix: Allow threads to enable the FPU for their own TCB. The API allowed this before, but the change would only take
effect the next time the thread was scheduled.
Platforms
- Add support for Rock3b (AArch64)
- Add support for Banana Pi BPI-F3 (RISC-V)
X86
- Allow user space reads from
VMX_CONTROL_SECONDARY_PROCESSOR_CONTROLS. Previously only writes were allowed. - Do not force 64-bit VCPU mode for
X86_64_VTX_64BIT_GUESTSto enable guests managing their own mode transition, e.g.
for UEFI firmware. - Allow user space reads and writes to
VMX_CONTROL_ENTRY_CONTROLSfield, e.g. for enabling long mode and loading of
certain MSRs on VM Entry. - Allow
CR0.PEandCR0.PGto be cleared if "Unrestricted Guest" mode is supported by the host CPU. This mode allows
guest software to run in unpaged protected mode or in real-address mode. - Skip the boot time clock sync test on Qemu, because timing is too unreliable under simulation
- Improve boot code error reporting on UART
ARM
- Support for choosing between GICv2 and GICv3 on Qemu
- Avoid trapping CPACR_EL1 accesses in hypervisor mode
- Performance improvements for FPU switching
Upgrade Notes
If using domains, replace any custom domain_schedule.c file with initialisation code in user space, or use
corresponding features in user-space frameworks such as Microkit and CAmkES. With MCS, the domain duration is now
configured in timer ticks instead of microseconds.
Full changelog
Refer to the git log in
https://github.com/seL4/seL4 using git log 14.0.0..15.0.0
More details
See the
15.0.0 manual included in the release or ask on the mailing list!