seL4 Version 6.0.0 Release
Announcing the release of
seL4 6.0.0 with the following changes:
ARM 32-bit SMP
- Works (and tested) only on Sabre/ARM with up to 4 cores.
- Using the big kernel lock (same as x86 implementation).
- Boot core is assumed to have an ID of 0.
- Kernel bootstraps and initialises data structures only on the boot core.
- Root task proceeds on the boot core.
- Cores are assumed to have linear IDes.
ARM IPI caveats:
- Reserving the first two per-core SGIs for seL4’s IPI operations: 0 to do a remote call, 1 to reschedule.
- Relying on GIC.
- Reschedule IPIs are sent when migrating a thread.
- Remote call IPIs are sent if TLB and/or cache maintenance operations are required.
- Remote FPU operations (when migrating threads that use HW FPU).
ARMv7 32-bit support is added to implement a lazy FP save/restore mechanism, required for user threads when they use the FPU. The following caveats exist:
- Only support synchronous exceptions. No support for asynchronous ones.
- VFP opcodes are used instead of normal instructions to discard compiler warnings/errors.
- Support is limited to specific ARM subarchitectures we support and tested this feature on.
- Disable the FPU by default if users are not using it to avoid channels.
- FPU support is not verified yet.
- Will not work properly if using a VM that’s running alongside other VMs/threads that are using the FPU.
- Any trapped FPU instruction (e.g. traps that need support code or deprecated vectored VFP operations) are forwarded to the user as a fault.
- aarch32 - Implement lazy FP save/restore
- ARM SMP support
- x86: Split large structs into portions (See upgrade notes below)
- License fixups
- This release is not source compatible with previous releases.
seL4_DebugDumpSchedulerhas had its only argument removed as it was unused.
- On x86 some structs in the Bootinfo have been rearranged. This
seL4_VBEModeInfoBlock_twhich is used if VESA BIOS Extensions (VBE) information is being used.
git log 5.2.0..6.0.0 in
See the 6.0.0 manual included in the release or ask on the mailing list!