seL4 Version 6.0.0 Release
Announcing the release of seL4 6.0.0
with the following changes:
Highlights
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).
ARM 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.
Changes
- aarch32 - Implement lazy FP save/restore
- ARM SMP support
- add
seL4_DebugDumpScheduler
debug syscall - x86: Split large structs into portions (See upgrade notes below)
- License fixups
Upgrade notes
- This release is not source compatible with previous releases.
seL4_DebugDumpScheduler
has had its only argument removed as it was unused.- 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.
Full changelog
Use git log 5.2.0..6.0.0
in
https://github.com/seL4/seL4
More details
See the 6.0.0 manual included in the release or ask on the mailing list!