seL4 Version 12.1.0 Release
Announcing the release of
seL4 12.1.0 with the following changes:
12.1.0 2021-06-10: SOURCE COMPATIBLE
- 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.
#pragma onceto the autoconf headers.
- Improved the manual:
- Corrected descriptions of CNode addressing.
- Documented initial thread’s SMMU caps.
- Improved libsel4:
- Removed redundant
HAVE_AUTOCONFheader guards in libsel4.
- Added missing
macros.h#include in libsel4.
- Added checks to use
_Static_assert()in libsel4 if it is available.
- Unified definitions in
PRI_sel4_wordfor printing word types.
- Unified seL4 type definitions.
- Removed redundant
- Added specific
printfformatting for seL4_Word.
- Changed some variables to use
BOOT_DATAto save space in the ELF file.
- Replaced the
capDL()function with a generic
debug_capDLfunction that is intended to be implemented by all architectures.
printfs stack usage.
ksnprintf()corner case handling.
- Fixed NULL
printfoutput wrapper handling.
- Cleaned up the printing API implementation.
- Changed code to pass buffer to
- Refactored the kernel console handling.
- Added support for
SEL4_PRIu_wordin the kernel.
- Changed various
printfconversion specifiers to use
- 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_Configurewhich 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
- 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
- Added call to
updateTimestampin 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.
- Removed a redundant de-reference for
- 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.
- 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
#definefor 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.
- 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_tby value for binary verification purposes.
slot_range_tfor binary verification purposes.
DONT_TRANSLATEtag 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.
traps.Sso that syscalls and fastpath checks were done after interrupts and exceptions checks to avoid exceptions being interpreted as null-syscalls.
- Added support for
- Fixed a register bug in the assembly entry point for SMP with regards to the elfloader passing HART and core IDs.
- 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
printfconversion 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.
Refer to the git log in
git log 12.0.0..12.1.0
See the 12.1.0 manual included in the release or ask on the mailing list!